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)
 inv(x) -> minus(0(),x)
 inv(minus(x,y)) -> minus(y,x)
 s(p(x)) -> x
 p(s(x)) -> x

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