NO

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

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