NO

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

Proof:
 Nonconfluence Processor:
  terms: +(x,x45) *<- +(x,s(s(x45))) ->* s(+(s(x45),x))
  Qed