YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?y,?x)),
     p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> ?x ]
Constructors: {0,p,s}
Defined function symbols: {+}
Constructor subsystem:
   [ p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> ?x ]
Rule part & Conj Part:
   [ p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?y,?x)) ]
   [ ]
Trying with:
R:
   [ p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?y,?x)) ]
E:
   [ ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Int}
Signature:
   [ + : Int,Int -> Int,
     s : Int -> Int,
     p : Int -> Int,
     0 : Int ]
Rule Part:
   [ p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?y,?x)) ]
Conjecture Part:
   [ ]
Precedence (by weight): {(+,3),(0,1),(p,2),(s,0)}
Rule part is not confluent.
Check ground confluence of Rule part (R0) by basic RI.
Rules:
   [ p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?y,?x)) ]
Conjectures:
   [ +(?x_1,?y_3) = +(?y_3,?x_1),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
STEP 0
ES:
   [ +(?x_1,?y_3) = +(?y_3,?x_1),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
HS:
   [ ]
ES0:
   [ +(?x_1,?y_3) = +(?y_3,?x_1),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
HS0:
   [ ]
ES1:
   [ +(?x_1,?y_3) = +(?y_3,?x_1),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
HS1:
   [ ]
Expand +(?x_1,?y_3) = +(?y_3,?x_1)
   [ ?y_5 = +(?y_5,0),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)) ]
ES2:
   [ ?y_5 = +(?y_5,0),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
HS2:
   [ +(?x_1,?y_3) -> +(?y_3,?x_1) ]
STEP 1
ES:
   [ ?y_5 = +(?y_5,0),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
HS:
   [ +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES0:
   [ ?y_5 = +(?y_5,0),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
HS0:
   [ +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES1:
   [ ?y_5 = +(?y_5,0),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     +(?x,?y_4) = p(+(?y_4,s(?x))) ]
HS1:
   [ +(?x_1,?y_3) -> +(?y_3,?x_1) ]
Expand +(?y_5,0) = ?y_5
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     p(+(0,?x_5)) = p(?x_5) ]
ES2:
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     p(?x_5) = p(?x_5),
     +(?x,?y_4) = p(+(?y_4,s(?x))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS2:
   [ +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
STEP 2
ES:
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     p(?x_5) = p(?x_5),
     +(?x,?y_4) = p(+(?y_4,s(?x))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS:
   [ +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES0:
   [ 0 = 0,
     s(?x_4) = s(?x_4),
     p(?x_5) = p(?x_5),
     +(?x,?y_4) = p(+(?y_4,s(?x))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS0:
   [ +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES1:
   [ +(?x,?y_4) = p(+(?y_4,s(?x))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS1:
   [ +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
Expand p(+(?y_4,s(?x))) = +(?x,?y_4)
   [ p(s(?x)) = +(?x,0),
     p(s(+(?x_8,s(?x)))) = +(?x,s(?x_8)),
     p(p(+(s(?x),?x_9))) = +(?x,p(?x_9)) ]
ES2:
   [ ?x = +(?x,0),
     +(?x_8,s(?x)) = +(?x,s(?x_8)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)) ]
HS2:
   [ p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
STEP 3
ES:
   [ ?x = +(?x,0),
     +(?x_8,s(?x)) = +(?x,s(?x_8)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)) ]
HS:
   [ p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES0:
   [ ?x = ?x,
     +(?x_8,s(?x)) = +(?x,s(?x_8)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)) ]
HS0:
   [ p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES1:
   [ +(?x_8,s(?x)) = +(?x,s(?x_8)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)) ]
HS1:
   [ p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
Expand +(?x_8,s(?x)) = +(?x,s(?x_8))
   [ s(?x) = +(?x,s(0)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     p(+(s(?x),?x_13)) = +(?x,s(p(?x_13))) ]
ES2:
   [ s(?x) = +(?x,s(0)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     +(?x,?x_13) = +(?x,s(p(?x_13))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)) ]
HS2:
   [ +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
STEP 4
ES:
   [ s(?x) = +(?x,s(0)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     +(?x,?x_13) = +(?x,s(p(?x_13))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)) ]
HS:
   [ +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES0:
   [ s(?x) = +(?x,s(0)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     +(?x,?x_13) = +(?x,?x_13),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)) ]
HS0:
   [ +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES1:
   [ s(?x) = +(?x,s(0)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)) ]
HS1:
   [ +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
Expand +(?x,s(0)) = s(?x)
   [ s(0) = s(0),
     s(+(?x_4,s(0))) = s(s(?x_4)),
     p(+(s(0),?x_5)) = s(p(?x_5)) ]
ES2:
   [ s(0) = s(0),
     s(+(?x_4,s(0))) = s(s(?x_4)),
     ?x_5 = s(p(?x_5)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))) ]
HS2:
   [ +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
STEP 5
ES:
   [ s(0) = s(0),
     s(+(?x_4,s(0))) = s(s(?x_4)),
     ?x_5 = s(p(?x_5)),
     p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))) ]
HS:
   [ +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES0:
   [ s(0) = s(0),
     s(s(?x_4)) = s(s(?x_4)),
     ?x_5 = ?x_5,
     p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))) ]
HS0:
   [ +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES1:
   [ p(+(?x,?x_9)) = +(?x,p(?x_9)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))) ]
HS1:
   [ +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
Expand +(?x,p(?x_9)) = p(+(?x,?x_9))
   [ p(?x_9) = p(+(0,?x_9)),
     s(+(?x_13,p(?x_9))) = p(+(s(?x_13),?x_9)),
     p(+(p(?x_9),?x_14)) = p(+(p(?x_14),?x_9)) ]
ES2:
   [ p(?x_9) = p(+(0,?x_9)),
     s(+(?x_13,p(?x_9))) = p(+(s(?x_13),?x_9)),
     p(p(+(?x_14,?x_9))) = p(+(p(?x_14),?x_9)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS2:
   [ +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
STEP 6
ES:
   [ p(?x_9) = p(+(0,?x_9)),
     s(+(?x_13,p(?x_9))) = p(+(s(?x_13),?x_9)),
     p(p(+(?x_14,?x_9))) = p(+(p(?x_14),?x_9)),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     p(+(?y_7,?x_7)) = +(?y_7,p(?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS:
   [ +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES0:
   [ p(?x_9) = p(?x_9),
     +(?x_13,?x_9) = +(?x_13,?x_9),
     p(p(+(?x_14,?x_9))) = p(p(+(?x_9,?x_14))),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     p(+(?y_7,?x_7)) = p(+(?y_7,?x_7)),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS0:
   [ +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES1:
   [ s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))),
     s(+(?x_6,?y_6)) = +(?y_6,s(?x_6)) ]
HS1:
   [ +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
Expand +(?y_6,s(?x_6)) = s(+(?x_6,?y_6))
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     p(+(s(?x),?x_5)) = s(+(?x,p(?x_5))) ]
ES2:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     +(?x,?x_5) = s(+(?x,p(?x_5))),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))) ]
HS2:
   [ +(?y_6,s(?x_6)) -> s(+(?x_6,?y_6)),
     +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
STEP 7
ES:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     +(?x,?x_5) = s(+(?x,p(?x_5))),
     s(+(?x_12,s(?x))) = +(?x,s(s(?x_12))) ]
HS:
   [ +(?y_6,s(?x_6)) -> s(+(?x_6,?y_6)),
     +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES0:
   [ s(?x) = s(?x),
     s(s(+(?x,?x_4))) = s(s(+(?x_4,?x))),
     +(?x,?x_5) = +(?x,?x_5),
     s(s(+(?x,?x_12))) = s(s(+(?x_12,?x))) ]
HS0:
   [ +(?y_6,s(?x_6)) -> s(+(?x_6,?y_6)),
     +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
ES1:
   [ ]
HS1:
   [ +(?y_6,s(?x_6)) -> s(+(?x_6,?y_6)),
     +(?x,p(?x_9)) -> p(+(?x,?x_9)),
     +(?x,s(0)) -> s(?x),
     +(?x_8,s(?x)) -> +(?x,s(?x_8)),
     p(+(?y_4,s(?x))) -> +(?x,?y_4),
     +(?y_5,0) -> ?y_5,
     +(?x_1,?y_3) -> +(?y_3,?x_1) ]
R0 is ground confluent.
Conjucture part is empty.
new/int1.trs: Success(GCR)
(18 msec.)