NO

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

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