YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(0,?y) -> ?y,
     +(p(?x),?y) -> p(+(?x,?y)),
     +(s(?x),?y) -> s(+(?x,?y)) ]
Constructors: {0,p,s}
Defined function symbols: {+}
Constructor subsystem:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Rule part & Conj Part:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(p(?x),?y) -> p(+(?x,?y)),
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)) ]
Rule part & Conj Part:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)) ]
   [ +(0,?y) -> ?y,
     +(p(?x),?y) -> p(+(?x,?y)),
     +(s(?x),?y) -> s(+(?x,?y)) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Int}
Signature:
   [ + : Int,Int -> Int,
     s : Int -> Int,
     p : Int -> Int,
     0 : Int ]
Rule Part:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(p(?x),?y) -> p(+(?x,?y)),
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjecture Part:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)) ]
Precedence (by weight): {(+,2),(0,3),(p,1),(s,0)}
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,
     +(0,?y) -> ?y,
     +(p(?x),?y) -> p(+(?x,?y)),
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjectures:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)) ]
STEP 0
ES:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)) ]
HS:
   [ ]
ES0:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)) ]
HS0:
   [ ]
ES1:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)) ]
HS1:
   [ ]
Expand +(?x,0) = ?x
   [ 0 = 0,
     p(+(?x_4,0)) = p(?x_4),
     s(+(?x_5,0)) = s(?x_5) ]
ES2:
   [ 0 = 0,
     p(+(?x_4,0)) = p(?x_4),
     s(+(?x_5,0)) = s(?x_5),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS2:
   [ +(?x,0) -> ?x ]
STEP 1
ES:
   [ 0 = 0,
     p(+(?x_4,0)) = p(?x_4),
     s(+(?x_5,0)) = s(?x_5),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS:
   [ +(?x,0) -> ?x ]
ES0:
   [ 0 = 0,
     p(?x_4) = p(?x_4),
     s(?x_5) = s(?x_5),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS0:
   [ +(?x,0) -> ?x ]
ES1:
   [ +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS1:
   [ +(?x,0) -> ?x ]
Expand +(?x,p(?y)) = p(+(?x,?y))
   [ p(?y) = p(+(0,?y)),
     p(+(?x_4,p(?y))) = p(+(p(?x_4),?y)),
     s(+(?x_5,p(?y))) = p(+(s(?x_5),?y)) ]
ES2:
   [ p(?y) = p(+(0,?y)),
     p(+(?x_4,p(?y))) = p(+(p(?x_4),?y)),
     s(+(?x_5,p(?y))) = p(+(s(?x_5),?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS2:
   [ +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
STEP 2
ES:
   [ p(?y) = p(+(0,?y)),
     p(+(?x_4,p(?y))) = p(+(p(?x_4),?y)),
     s(+(?x_5,p(?y))) = p(+(s(?x_5),?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS:
   [ +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
ES0:
   [ p(?y) = p(?y),
     p(p(+(?x_4,?y))) = p(p(+(?x_4,?y))),
     +(?x_5,?y) = +(?x_5,?y),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS0:
   [ +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
ES1:
   [ +(?x,s(?y)) = s(+(?x,?y)) ]
HS1:
   [ +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
Expand +(?x,s(?y)) = s(+(?x,?y))
   [ s(?y) = s(+(0,?y)),
     p(+(?x_4,s(?y))) = s(+(p(?x_4),?y)),
     s(+(?x_5,s(?y))) = s(+(s(?x_5),?y)) ]
ES2:
   [ s(?y) = s(+(0,?y)),
     p(+(?x_4,s(?y))) = s(+(p(?x_4),?y)),
     s(+(?x_5,s(?y))) = s(+(s(?x_5),?y)) ]
HS2:
   [ +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
STEP 3
ES:
   [ s(?y) = s(+(0,?y)),
     p(+(?x_4,s(?y))) = s(+(p(?x_4),?y)),
     s(+(?x_5,s(?y))) = s(+(s(?x_5),?y)) ]
HS:
   [ +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
ES0:
   [ s(?y) = s(?y),
     +(?x_4,?y) = +(?x_4,?y),
     s(s(+(?x_5,?y))) = s(s(+(?x_5,?y))) ]
HS0:
   [ +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
ES1:
   [ ]
HS1:
   [ +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(?x,0) -> ?x ]
Conj part consisits of inductive theorems of R0.
examples/additions/int4.trs: Success(GCR)
(20 msec.)