NO

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

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