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),
     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 ]
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),
     minus(s(?x),s(?y)) -> minus(?x,?y),
     minus(p(?x),p(?y)) -> minus(?x,?y) ]
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),
     minus(s(?x),s(?y)) -> minus(?x,?y),
     minus(p(?x),p(?y)) -> minus(?x,?y),
     inv(?x) -> minus(0,?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),
     minus(s(?x),s(?y)) = minus(?x,?y),
     minus(p(?x),p(?y)) = minus(?x,?y) ]
*** 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),
     minus(s(?x),s(?y)) = minus(?x,?y),
     minus(p(?x),p(?y)) = minus(?x,?y) ]
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),
     minus(s(?x),s(?y)) = minus(?x,?y),
     minus(p(?x),p(?y)) = minus(?x,?y) ]
STEP 0
ES:
   [ inv(0) = 0,
     inv(s(?x)) = p(inv(?x)),
     inv(p(?x)) = s(inv(?x)),
     minus(0,?x) = inv(?x),
     minus(s(?x),s(?y)) = minus(?x,?y),
     minus(p(?x),p(?y)) = minus(?x,?y) ]
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),
     p(minus(s(?x),?y)) = minus(?x,?y),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS0:
   [ ]
ES1:
   [ p(minus(s(?x),?y)) = minus(?x,?y),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS1:
   [ ]
Expand p(minus(s(?x),?y)) = minus(?x,?y)
   [ p(s(?x)) = minus(?x,0),
     p(s(minus(s(?x),?y_4))) = minus(?x,p(?y_4)),
     p(p(minus(s(?x),?y_5))) = minus(?x,s(?y_5)) ]
ES2:
   [ ?x = minus(?x,0),
     minus(s(?x),?y_4) = minus(?x,p(?y_4)),
     p(p(minus(s(?x),?y_5))) = minus(?x,s(?y_5)),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS2:
   [ p(minus(s(?x),?y)) -> minus(?x,?y) ]
STEP 1
ES:
   [ ?x = minus(?x,0),
     minus(s(?x),?y_4) = minus(?x,p(?y_4)),
     p(p(minus(s(?x),?y_5))) = minus(?x,s(?y_5)),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS:
   [ p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES0:
   [ ?x = ?x,
     minus(s(?x),?y_4) = s(minus(?x,?y_4)),
     p(minus(?x,?y_5)) = p(minus(?x,?y_5)),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS0:
   [ p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES1:
   [ minus(s(?x),?y_4) = s(minus(?x,?y_4)),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS1:
   [ p(minus(s(?x),?y)) -> minus(?x,?y) ]
Expand minus(s(?x),?y_4) = s(minus(?x,?y_4))
   [ s(?x) = s(minus(?x,0)),
     s(minus(s(?x),?y_8)) = s(minus(?x,p(?y_8))),
     p(minus(s(?x),?y_9)) = s(minus(?x,s(?y_9))) ]
ES2:
   [ s(?x) = s(minus(?x,0)),
     s(minus(s(?x),?y_8)) = s(minus(?x,p(?y_8))),
     minus(?x,?y_9) = s(minus(?x,s(?y_9))),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS2:
   [ minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
STEP 2
ES:
   [ s(?x) = s(minus(?x,0)),
     s(minus(s(?x),?y_8)) = s(minus(?x,p(?y_8))),
     minus(?x,?y_9) = s(minus(?x,s(?y_9))),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS:
   [ minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES0:
   [ s(?x) = s(?x),
     s(s(minus(?x,?y_8))) = s(s(minus(?x,?y_8))),
     minus(?x,?y_9) = minus(?x,?y_9),
     s(minus(p(?x),?y)) = minus(?x,?y) ]
HS0:
   [ minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES1:
   [ s(minus(p(?x),?y)) = minus(?x,?y) ]
HS1:
   [ minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
Expand s(minus(p(?x),?y)) = minus(?x,?y)
   [ s(p(?x)) = minus(?x,0),
     s(s(minus(p(?x),?y_4))) = minus(?x,p(?y_4)),
     s(p(minus(p(?x),?y_5))) = minus(?x,s(?y_5)) ]
ES2:
   [ ?x = minus(?x,0),
     s(s(minus(p(?x),?y_4))) = minus(?x,p(?y_4)),
     minus(p(?x),?y_5) = minus(?x,s(?y_5)) ]
HS2:
   [ s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
STEP 3
ES:
   [ ?x = minus(?x,0),
     s(s(minus(p(?x),?y_4))) = minus(?x,p(?y_4)),
     minus(p(?x),?y_5) = minus(?x,s(?y_5)) ]
HS:
   [ s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES0:
   [ ?x = ?x,
     s(minus(?x,?y_4)) = s(minus(?x,?y_4)),
     minus(p(?x),?y_5) = p(minus(?x,?y_5)) ]
HS0:
   [ s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES1:
   [ minus(p(?x),?y_5) = p(minus(?x,?y_5)) ]
HS1:
   [ s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
Expand minus(p(?x),?y_5) = p(minus(?x,?y_5))
   [ p(?x) = p(minus(?x,0)),
     s(minus(p(?x),?y_9)) = p(minus(?x,p(?y_9))),
     p(minus(p(?x),?y_10)) = p(minus(?x,s(?y_10))) ]
ES2:
   [ p(?x) = p(minus(?x,0)),
     minus(?x,?y_9) = p(minus(?x,p(?y_9))),
     p(minus(p(?x),?y_10)) = p(minus(?x,s(?y_10))) ]
HS2:
   [ minus(p(?x),?y_5) -> p(minus(?x,?y_5)),
     s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
STEP 4
ES:
   [ p(?x) = p(minus(?x,0)),
     minus(?x,?y_9) = p(minus(?x,p(?y_9))),
     p(minus(p(?x),?y_10)) = p(minus(?x,s(?y_10))) ]
HS:
   [ minus(p(?x),?y_5) -> p(minus(?x,?y_5)),
     s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES0:
   [ p(?x) = p(?x),
     minus(?x,?y_9) = minus(?x,?y_9),
     p(p(minus(?x,?y_10))) = p(p(minus(?x,?y_10))) ]
HS0:
   [ minus(p(?x),?y_5) -> p(minus(?x,?y_5)),
     s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
ES1:
   [ ]
HS1:
   [ minus(p(?x),?y_5) -> p(minus(?x,?y_5)),
     s(minus(p(?x),?y)) -> minus(?x,?y),
     minus(s(?x),?y_4) -> s(minus(?x,?y_4)),
     p(minus(s(?x),?y)) -> minus(?x,?y) ]
Conj part consisits of inductive theorems of R0.
new/minus.trs: Success(GCR)
(15 msec.)