YES
(ignored inputs)COMMENT translated from Cops 139
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?x,?y)),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     -(0) -> 0,
     -(s(?x)) -> p(-(?x)),
     -(p(?x)) -> s(-(?x)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     -(+(?x,?y)) -> +(-(?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,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?x,?y)),
     -(0) -> 0,
     -(s(?x)) -> p(-(?x)),
     -(p(?x)) -> s(-(?x)) ]
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(?x,?y) -> +(?y,?x) ]
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) -> 0,
     -(s(?x)) -> p(-(?x)),
     -(p(?x)) -> s(-(?x)) ]
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?x,?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(?x,?y) -> +(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Int}
Signature:
   [ + : Int,Int -> Int,
     - : Int -> Int,
     0 : Int,
     p : Int -> Int,
     s : Int -> Int ]
Rule Part:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?x,?y)),
     -(0) -> 0,
     -(s(?x)) -> p(-(?x)),
     -(p(?x)) -> s(-(?x)) ]
Conjecture Part:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(?x,?y) = +(?y,?x) ]
Precedence (by weight): {(+,6),(-,5),(0,0),(p,2),(s,4)}
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,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?x,?y)),
     -(0) -> 0,
     -(s(?x)) -> p(-(?x)),
     -(p(?x)) -> s(-(?x)) ]
Conjectures:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(?x,?y) = +(?y,?x) ]
STEP 0
ES:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(?x,?y) = +(?y,?x) ]
HS:
   [ ]
ES0:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(?x,?y) = +(?y,?x) ]
HS0:
   [ ]
ES1:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(?x,?y) = +(?y,?x) ]
HS1:
   [ ]
Expand +(?x,0) = ?x
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     p(+(?x_5,0)) = p(?x_5) ]
ES2:
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     p(+(?x_5,0)) = p(?x_5),
     +(?x,?y) = +(?y,?x),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS2:
   [ +(?x,0) -> ?x ]
STEP 1
ES:
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     p(+(?x_5,0)) = p(?x_5),
     +(?x,?y) = +(?y,?x),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS:
   [ +(?x,0) -> ?x ]
ES0:
   [ 0 = 0,
     s(?x_4) = s(?x_4),
     p(?x_5) = p(?x_5),
     +(?x,?y) = +(?y,?x),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS0:
   [ +(?x,0) -> ?x ]
ES1:
   [ +(?x,?y) = +(?y,?x),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS1:
   [ +(?x,0) -> ?x ]
Expand +(?x,?y) = +(?y,?x)
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
ES2:
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS2:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
STEP 2
ES:
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES0:
   [ ?y_3 = ?y_3,
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS0:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES1:
   [ s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,s(?y)) = s(+(?x,?y)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS1:
   [ +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
Expand +(?y_4,s(?x_4)) = s(+(?x_4,?y_4))
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     p(+(?x_5,s(?x))) = s(+(?x,p(?x_5))) ]
ES2:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     p(+(?x_5,s(?x))) = s(+(?x,p(?x_5))),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
HS2:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
STEP 3
ES:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     p(+(?x_5,s(?x))) = s(+(?x,p(?x_5))),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(?x,s(?y)) = s(+(?x,?y)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
HS:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES0:
   [ s(?x) = s(?x),
     s(s(+(?x,?x_4))) = s(s(+(?x_4,?x))),
     +(?x,?x_5) = s(+(?x,p(?x_5))),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     s(+(?y,?x)) = s(+(?x,?y)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
HS0:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES1:
   [ +(?x,?x_5) = s(+(?x,p(?x_5))),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
HS1:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
Expand s(+(?x,p(?x_5))) = +(?x,?x_5)
   [ s(p(?x_5)) = +(0,?x_5),
     s(s(+(?x_9,p(?x_5)))) = +(s(?x_9),?x_5),
     s(p(+(?x_10,p(?x_5)))) = +(p(?x_10),?x_5) ]
ES2:
   [ ?x_5 = +(0,?x_5),
     s(s(+(?x_9,p(?x_5)))) = +(s(?x_9),?x_5),
     +(?x_10,p(?x_5)) = +(p(?x_10),?x_5),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS2:
   [ s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
STEP 4
ES:
   [ ?x_5 = +(0,?x_5),
     s(s(+(?x_9,p(?x_5)))) = +(s(?x_9),?x_5),
     +(?x_10,p(?x_5)) = +(p(?x_10),?x_5),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS:
   [ s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES0:
   [ ?x_5 = ?x_5,
     s(+(?x_9,?x_5)) = s(+(?x_9,?x_5)),
     +(?x_10,p(?x_5)) = p(+(?x_10,?x_5)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS0:
   [ s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES1:
   [ +(?x_10,p(?x_5)) = p(+(?x_10,?x_5)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)),
     +(?x,p(?y)) = p(+(?x,?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?x),-(?y)) ]
HS1:
   [ s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
Expand +(?x_10,p(?x_5)) = p(+(?x_10,?x_5))
   [ p(?x) = p(+(0,?x)),
     s(+(?x_9,p(?x))) = p(+(s(?x_9),?x)),
     p(+(?x_10,p(?x))) = p(+(p(?x_10),?x)) ]
ES2:
   [ p(?x) = p(+(0,?x)),
     +(?x_9,?x) = p(+(s(?x_9),?x)),
     p(+(?x_10,p(?x))) = p(+(p(?x_10),?x)),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
HS2:
   [ +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
STEP 5
ES:
   [ p(?x) = p(+(0,?x)),
     +(?x_9,?x) = p(+(s(?x_9),?x)),
     p(+(?x_10,p(?x))) = p(+(p(?x_10),?x)),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,p(?y)) = p(+(?x,?y)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
HS:
   [ +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES0:
   [ p(?x) = p(?x),
     +(?x_9,?x) = +(?x_9,?x),
     p(p(+(?x_10,?x))) = p(p(+(?x_10,?x))),
     -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     p(+(?x,?y)) = p(+(?x,?y)),
     p(+(?x_5,?y_5)) = p(+(?y_5,?x_5)) ]
HS0:
   [ +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES1:
   [ -(+(?x,?y)) = +(-(?x),-(?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
Expand +(-(?x),-(?y)) = -(+(?x,?y))
   [ +(0,-(?y)) = -(+(0,?y)),
     +(p(-(?x_6)),-(?y)) = -(+(s(?x_6),?y)),
     +(s(-(?x_7)),-(?y)) = -(+(p(?x_7),?y)) ]
ES2:
   [ -(?y) = -(+(0,?y)),
     p(+(-(?x_6),-(?y))) = -(+(s(?x_6),?y)),
     s(+(-(?x_7),-(?y))) = -(+(p(?x_7),?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
STEP 6
ES:
   [ -(?y) = -(+(0,?y)),
     p(+(-(?x_6),-(?y))) = -(+(s(?x_6),?y)),
     s(+(-(?x_7),-(?y))) = -(+(p(?x_7),?y)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES0:
   [ -(?y) = -(?y),
     p(-(+(?x_6,?y))) = p(-(+(?x_6,?y))),
     s(-(+(?x_7,?y))) = s(-(+(?x_7,?y))),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
Expand +(+(?x,?y),?z) = +(?x,+(?y,?z))
   [ +(?y_3,?z) = +(0,+(?y_3,?z)),
     +(s(+(?x_4,?y_4)),?z) = +(s(?x_4),+(?y_4,?z)),
     +(p(+(?x_5,?y_5)),?z) = +(p(?x_5),+(?y_5,?z)) ]
ES2:
   [ +(?y_3,?z) = +(0,+(?y_3,?z)),
     s(+(+(?x_4,?y_4),?z)) = +(s(?x_4),+(?y_4,?z)),
     p(+(+(?x_5,?y_5),?z)) = +(p(?x_5),+(?y_5,?z)) ]
HS2:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
STEP 7
ES:
   [ +(?y_3,?z) = +(0,+(?y_3,?z)),
     s(+(+(?x_4,?y_4),?z)) = +(s(?x_4),+(?y_4,?z)),
     p(+(+(?x_5,?y_5),?z)) = +(p(?x_5),+(?y_5,?z)) ]
HS:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES0:
   [ +(?y_3,?z) = +(?y_3,?z),
     s(+(+(?x_4,?y_4),?z)) = s(+(?x_4,+(?y_4,?z))),
     p(+(+(?x_5,?y_5),?z)) = p(+(?x_5,+(?y_5,?z))) ]
HS0:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
ES1:
   [ ]
HS1:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(-(?x),-(?y)) -> -(+(?x,?y)),
     +(?x_10,p(?x_5)) -> p(+(?x_10,?x_5)),
     s(+(?x,p(?x_5))) -> +(?x,?x_5),
     +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?x,?y) -> +(?y,?x),
     +(?x,0) -> ?x ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/cr/139.trs: Success(GCR)
(24 msec.)