NO

Problem:
 +(0(),y) -> y
 +(s(0()),y) -> s(y)
 +(s(s(x)),y) -> s(s(+(y,x)))
 +(x,+(y,z)) -> +(+(z,y),x)

Proof:
 Nonconfluence Processor:
  terms: s(s(+(y,x54))) *<- +(s(s(+(0(),x54))),y) ->* s(s(+(+(x54,0()),y)))
  Qed