NO

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

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