YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ 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 ]
Constructors: {0,p,s}
Defined function symbols: {inv,minus}
Constructor subsystem:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Rule part & Conj Part:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     minus(?x,0) -> ?x,
     minus(?x,p(?y)) -> s(minus(?x,?y)),
     minus(?x,s(?y)) -> p(minus(?x,?y)),
     inv(?x) -> minus(0,?x) ]
   [ inv(0) -> 0,
     inv(s(?x)) -> p(inv(?x)),
     inv(p(?x)) -> s(inv(?x)),
     minus(0,?x) -> inv(?x),
     inv(minus(?x,?y)) -> minus(?y,?x) ]
Rule part & Conj Part:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     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) ]
Trying with:
R:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     minus(?x,0) -> ?x,
     minus(?x,p(?y)) -> s(minus(?x,?y)),
     minus(?x,s(?y)) -> p(minus(?x,?y)),
     inv(?x) -> minus(0,?x) ]
E:
   [ inv(0) = 0,
     inv(s(?x)) = p(inv(?x)),
     inv(p(?x)) = s(inv(?x)),
     minus(0,?x) = inv(?x),
     inv(minus(?x,?y)) = minus(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Int}
Signature:
   [ inv : Int -> Int,
     minus : Int,Int -> Int,
     s : Int -> Int,
     p : Int -> Int,
     0 : Int ]
Rule Part:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     minus(?x,0) -> ?x,
     minus(?x,p(?y)) -> s(minus(?x,?y)),
     minus(?x,s(?y)) -> p(minus(?x,?y)),
     inv(?x) -> minus(0,?x) ]
Conjecture Part:
   [ inv(0) = 0,
     inv(s(?x)) = p(inv(?x)),
     inv(p(?x)) = s(inv(?x)),
     minus(0,?x) = inv(?x),
     inv(minus(?x,?y)) = minus(?y,?x) ]
Precedence (by weight): {(0,0),(p,2),(s,4),(inv,7),(minus,6)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     minus(?x,0) -> ?x,
     minus(?x,p(?y)) -> s(minus(?x,?y)),
     minus(?x,s(?y)) -> p(minus(?x,?y)),
     inv(?x) -> minus(0,?x) ]
Conjectures:
   [ inv(0) = 0,
     inv(s(?x)) = p(inv(?x)),
     inv(p(?x)) = s(inv(?x)),
     minus(0,?x) = inv(?x),
     inv(minus(?x,?y)) = minus(?y,?x) ]
STEP 0
ES:
   [ inv(0) = 0,
     inv(s(?x)) = p(inv(?x)),
     inv(p(?x)) = s(inv(?x)),
     minus(0,?x) = inv(?x),
     inv(minus(?x,?y)) = minus(?y,?x) ]
HS:
   [ ]
ES0:
   [ 0 = 0,
     p(minus(0,?x)) = p(minus(0,?x)),
     s(minus(0,?x)) = s(minus(0,?x)),
     minus(0,?x) = minus(0,?x),
     minus(0,minus(?x,?y)) = minus(?y,?x) ]
HS0:
   [ ]
ES1:
   [ minus(0,minus(?x,?y)) = minus(?y,?x) ]
HS1:
   [ ]
Expand minus(0,minus(?x,?y)) = minus(?y,?x)
   [ minus(0,?x_3) = minus(0,?x_3),
     minus(0,s(minus(?x_4,?y_4))) = minus(p(?y_4),?x_4),
     minus(0,p(minus(?x_5,?y_5))) = minus(s(?y_5),?x_5) ]
ES2:
   [ minus(0,?x_3) = minus(0,?x_3),
     p(minus(0,minus(?x_4,?y_4))) = minus(p(?y_4),?x_4),
     s(minus(0,minus(?x_5,?y_5))) = minus(s(?y_5),?x_5) ]
HS2:
   [ minus(0,minus(?x,?y)) -> minus(?y,?x) ]
STEP 1
ES:
   [ minus(0,?x_3) = minus(0,?x_3),
     p(minus(0,minus(?x_4,?y_4))) = minus(p(?y_4),?x_4),
     s(minus(0,minus(?x_5,?y_5))) = minus(s(?y_5),?x_5) ]
HS:
   [ minus(0,minus(?x,?y)) -> minus(?y,?x) ]
ES0:
   [ minus(0,?x_3) = minus(0,?x_3),
     p(minus(?y_4,?x_4)) = minus(p(?y_4),?x_4),
     s(minus(?y_5,?x_5)) = minus(s(?y_5),?x_5) ]
HS0:
   [ minus(0,minus(?x,?y)) -> minus(?y,?x) ]
ES1:
   [ p(minus(?y_4,?x_4)) = minus(p(?y_4),?x_4),
     s(minus(?y_5,?x_5)) = minus(s(?y_5),?x_5) ]
HS1:
   [ minus(0,minus(?x,?y)) -> minus(?y,?x) ]
Expand minus(p(?y_4),?x_4) = p(minus(?y_4,?x_4))
   [ p(?y) = p(minus(?y,0)),
     s(minus(p(?y),?y_4)) = p(minus(?y,p(?y_4))),
     p(minus(p(?y),?y_5)) = p(minus(?y,s(?y_5))) ]
ES2:
   [ p(?y) = p(minus(?y,0)),
     s(minus(p(?y),?y_4)) = p(minus(?y,p(?y_4))),
     p(minus(p(?y),?y_5)) = p(minus(?y,s(?y_5))),
     s(minus(?y_5,?x_5)) = minus(s(?y_5),?x_5) ]
HS2:
   [ minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
STEP 2
ES:
   [ p(?y) = p(minus(?y,0)),
     s(minus(p(?y),?y_4)) = p(minus(?y,p(?y_4))),
     p(minus(p(?y),?y_5)) = p(minus(?y,s(?y_5))),
     s(minus(?y_5,?x_5)) = minus(s(?y_5),?x_5) ]
HS:
   [ minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
ES0:
   [ p(?y) = p(?y),
     minus(?y,?y_4) = minus(?y,?y_4),
     p(p(minus(?y,?y_5))) = p(p(minus(?y,?y_5))),
     s(minus(?y_5,?x_5)) = minus(s(?y_5),?x_5) ]
HS0:
   [ minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
ES1:
   [ s(minus(?y_5,?x_5)) = minus(s(?y_5),?x_5) ]
HS1:
   [ minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
Expand minus(s(?y_5),?x_5) = s(minus(?y_5,?x_5))
   [ s(?y) = s(minus(?y,0)),
     s(minus(s(?y),?y_4)) = s(minus(?y,p(?y_4))),
     p(minus(s(?y),?y_5)) = s(minus(?y,s(?y_5))) ]
ES2:
   [ s(?y) = s(minus(?y,0)),
     s(minus(s(?y),?y_4)) = s(minus(?y,p(?y_4))),
     p(minus(s(?y),?y_5)) = s(minus(?y,s(?y_5))) ]
HS2:
   [ minus(s(?y_5),?x_5) -> s(minus(?y_5,?x_5)),
     minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
STEP 3
ES:
   [ s(?y) = s(minus(?y,0)),
     s(minus(s(?y),?y_4)) = s(minus(?y,p(?y_4))),
     p(minus(s(?y),?y_5)) = s(minus(?y,s(?y_5))) ]
HS:
   [ minus(s(?y_5),?x_5) -> s(minus(?y_5,?x_5)),
     minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
ES0:
   [ s(?y) = s(?y),
     s(s(minus(?y,?y_4))) = s(s(minus(?y,?y_4))),
     minus(?y,?y_5) = minus(?y,?y_5) ]
HS0:
   [ minus(s(?y_5),?x_5) -> s(minus(?y_5,?x_5)),
     minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
ES1:
   [ ]
HS1:
   [ minus(s(?y_5),?x_5) -> s(minus(?y_5,?x_5)),
     minus(p(?y_4),?x_4) -> p(minus(?y_4,?x_4)),
     minus(0,minus(?x,?y)) -> minus(?y,?x) ]
Conj part consisits of inductive theorems of R0.
new/minus2.trs: Success(GCR)
(14 msec.)