NO

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

Proof:
 Nonconfluence Processor:
  terms: +(0(),f5()) *<- +(p(s(0())),f5()) ->* +(s(0()),p(f5()))
  Qed
  
  first automaton:
   final states: {11}
   transitions:
    0() -> 13*
    +(13,12) -> 11*
    f5() -> 12*
    12 -> 11*
  
  second automaton:
   final states: {14}
   transitions:
    p(277) -> 14*
    p(15) -> 16*
    0() -> 17*
    +(17,16) -> 107*
    +(18,16) -> 14*
    s(15) -> 277*
    s(107) -> 14*
    s(17) -> 18*
    f5() -> 15*
    16 -> 107*