NO

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

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