YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(0,0) -> 0,
     +(s(?x),?y) -> s(+(?x,?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(?x),?y) -> s(+(?x,?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(?x),?y) -> s(+(?x,?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(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)) ]
Conjectures:
   [ +(?x_1,?y_2) = +(?y_2,?x_1),
     +(?x_2,?x) = +(?x,?x_2) ]
STEP 0
ES:
   [ +(?x_1,?y_2) = +(?y_2,?x_1),
     +(?x_2,?x) = +(?x,?x_2) ]
HS:
   [ ]
ES0:
   [ +(?x_1,?y_2) = +(?y_2,?x_1),
     +(?x_2,?x) = +(?x,?x_2) ]
HS0:
   [ ]
ES1:
   [ +(?x_1,?y_2) = +(?y_2,?x_1),
     +(?x_2,?x) = +(?x,?x_2) ]
HS1:
   [ ]
Expand +(?x_1,?y_2) = +(?y_2,?x_1)
   [ 0 = +(0,0),
     s(+(?x_3,?y_3)) = +(?y_3,s(?x_3)),
     s(+(?y_4,?x_4)) = +(s(?y_4),?x_4) ]
ES2:
   [ 0 = +(0,0),
     s(+(?x_3,?y_3)) = +(?y_3,s(?x_3)),
     s(+(?y_4,?x_4)) = +(s(?y_4),?x_4),
     +(?x_2,?x) = +(?x,?x_2) ]
HS2:
   [ +(?x_1,?y_2) -> +(?y_2,?x_1) ]
STEP 1
ES:
   [ 0 = +(0,0),
     s(+(?x_3,?y_3)) = +(?y_3,s(?x_3)),
     s(+(?y_4,?x_4)) = +(s(?y_4),?x_4),
     +(?x_2,?x) = +(?x,?x_2) ]
HS:
   [ +(?x_1,?y_2) -> +(?y_2,?x_1) ]
ES0:
   [ 0 = 0,
     s(+(?x_3,?y_3)) = s(+(?x_3,?y_3)),
     s(+(?y_4,?x_4)) = s(+(?y_4,?x_4)),
     +(?x_2,?x) = +(?x,?x_2) ]
HS0:
   [ +(?x_1,?y_2) -> +(?y_2,?x_1) ]
ES1:
   [ ]
HS1:
   [ +(?x_1,?y_2) -> +(?y_2,?x_1) ]
R0 is ground confluent.
Conjucture part is empty.
examples/additions/plus9.trs: Success(GCR)
(14 msec.)