YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(0,0) -> 0,
     +(s(0),?y) -> s(+(0,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     s(s(?x)) -> ?x ]
Constructors: {0,s}
Defined function symbols: {+}
Constructor subsystem:
   [ s(s(?x)) -> ?x ]
Rule part & Conj Part:
   [ s(s(?x)) -> ?x,
     +(0,0) -> 0,
     +(s(0),?y) -> s(+(0,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)) ]
   [ ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ + : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ s(s(?x)) -> ?x,
     +(0,0) -> 0,
     +(s(0),?y) -> s(+(0,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)) ]
Conjecture Part:
   [ ]
Precedence (by weight): {(+,3),(0,1),(s,0)}
Rule part is not confluent.
Check ground confluence of Rule part (R0) by basic RI.
Rules:
   [ s(s(?x)) -> ?x,
     +(0,0) -> 0,
     +(s(0),?y) -> s(+(0,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)) ]
Conjectures:
   [ +(0,?y_2) = +(?y_2,0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
STEP 0
ES:
   [ +(0,?y_2) = +(?y_2,0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS:
   [ ]
ES0:
   [ +(0,?y_2) = +(?y_2,0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS0:
   [ ]
ES1:
   [ +(0,?y_2) = +(?y_2,0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS1:
   [ ]
Expand +(0,?y_2) = +(?y_2,0)
   [ 0 = +(0,0),
     s(+(?y_3,0)) = +(s(?y_3),0),
     +(0,?x_8) = +(s(s(?x_8)),0) ]
ES2:
   [ 0 = +(0,0),
     s(+(?y_3,0)) = +(s(?y_3),0),
     +(0,?x_8) = +(s(s(?x_8)),0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS2:
   [ +(0,?y_2) -> +(?y_2,0) ]
STEP 1
ES:
   [ 0 = +(0,0),
     s(+(?y_3,0)) = +(s(?y_3),0),
     +(0,?x_8) = +(s(s(?x_8)),0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS:
   [ +(0,?y_2) -> +(?y_2,0) ]
ES0:
   [ 0 = 0,
     s(+(?y_3,0)) = +(s(?y_3),0),
     +(0,?x_8) = +(?x_8,0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS0:
   [ +(0,?y_2) -> +(?y_2,0) ]
ES1:
   [ s(+(?y_3,0)) = +(s(?y_3),0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS1:
   [ +(0,?y_2) -> +(?y_2,0) ]
Expand +(s(?y_3),0) = s(+(?y_3,0))
   [ s(+(0,0)) = s(+(0,0)),
     +(?x_5,0) = s(+(s(?x_5),0)) ]
ES2:
   [ s(0) = s(+(0,0)),
     +(?x_5,0) = s(+(s(?x_5),0)),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS2:
   [ +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
STEP 2
ES:
   [ s(0) = s(+(0,0)),
     +(?x_5,0) = s(+(s(?x_5),0)),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS:
   [ +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
ES0:
   [ s(0) = s(0),
     +(?x_5,0) = +(?x_5,0),
     +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS0:
   [ +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
ES1:
   [ +(?x_2,?x) = s(+(s(?x),?x_2)) ]
HS1:
   [ +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
Expand s(+(s(?x),?x_2)) = +(?x_2,?x)
   [ s(s(+(0,?y_4))) = +(?y_4,0),
     s(s(+(?y_5,s(?x)))) = +(s(?y_5),?x),
     s(+(?x_7,?x_6)) = +(?x_6,s(?x_7)),
     s(+(s(?x),?x_10)) = +(s(s(?x_10)),?x) ]
ES2:
   [ +(0,?y_4) = +(?y_4,0),
     s(+(?x,?y_5)) = +(s(?y_5),?x),
     s(+(?x_7,?x_6)) = +(?x_6,s(?x_7)),
     s(+(s(?x),?x_10)) = +(s(s(?x_10)),?x) ]
HS2:
   [ s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
STEP 3
ES:
   [ +(0,?y_4) = +(?y_4,0),
     s(+(?x,?y_5)) = +(s(?y_5),?x),
     s(+(?x_7,?x_6)) = +(?x_6,s(?x_7)),
     s(+(s(?x),?x_10)) = +(s(s(?x_10)),?x) ]
HS:
   [ s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
ES0:
   [ +(0,?y_4) = +(?y_4,0),
     s(+(?x,?y_5)) = +(s(?y_5),?x),
     s(+(?x_7,?x_6)) = s(+(?x_7,?x_6)),
     +(?x_10,?x) = +(?x_10,?x) ]
HS0:
   [ s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
ES1:
   [ s(+(?x,?y_5)) = +(s(?y_5),?x) ]
HS1:
   [ s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
Expand +(s(?y_5),?x) = s(+(?x,?y_5))
   [ s(+(0,?y_7)) = s(+(?y_7,0)),
     s(+(?y_8,s(?y_5))) = s(+(s(?y_8),?y_5)),
     +(?x_10,?x_9) = s(+(?x_9,s(?x_10))),
     +(s(?y_5),?x_13) = s(+(s(s(?x_13)),?y_5)) ]
ES2:
   [ s(+(0,?y_7)) = s(+(?y_7,0)),
     +(?y_5,?y_8) = s(+(s(?y_8),?y_5)),
     +(?x_10,?x_9) = s(+(?x_9,s(?x_10))),
     +(s(?y_5),?x_13) = s(+(s(s(?x_13)),?y_5)) ]
HS2:
   [ +(s(?y_5),?x) -> s(+(?x,?y_5)),
     s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
STEP 4
ES:
   [ s(+(0,?y_7)) = s(+(?y_7,0)),
     +(?y_5,?y_8) = s(+(s(?y_8),?y_5)),
     +(?x_10,?x_9) = s(+(?x_9,s(?x_10))),
     +(s(?y_5),?x_13) = s(+(s(s(?x_13)),?y_5)) ]
HS:
   [ +(s(?y_5),?x) -> s(+(?x,?y_5)),
     s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
ES0:
   [ s(+(0,?y_7)) = s(+(?y_7,0)),
     +(?y_5,?y_8) = +(?y_5,?y_8),
     +(?x_10,?x_9) = +(?x_10,?x_9),
     s(+(?x_13,?y_5)) = s(+(?x_13,?y_5)) ]
HS0:
   [ +(s(?y_5),?x) -> s(+(?x,?y_5)),
     s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
ES1:
   [ ]
HS1:
   [ +(s(?y_5),?x) -> s(+(?x,?y_5)),
     s(+(s(?x),?x_2)) -> +(?x_2,?x),
     +(s(?y_3),0) -> s(+(?y_3,0)),
     +(0,?y_2) -> +(?y_2,0) ]
R0 is ground confluent.
Conjucture part is empty.
examples/additions/plus10.trs: Success(GCR)
(16 msec.)