YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,+(?y,?z)) -> +(+(?z,?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,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ +(?x,+(?y,?z)) -> +(+(?z,?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,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjecture Part:
   [ +(?x,+(?y,?z)) = +(+(?z,?y),?x) ]
Precedence (by weight): {(+,3),(0,2),(s,0)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ s(s(?x)) -> ?x,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjectures:
   [ +(?x,+(?y,?z)) = +(+(?z,?y),?x) ]
STEP 0
ES:
   [ +(?x,+(?y,?z)) = +(+(?z,?y),?x) ]
HS:
   [ ]
ES0:
   [ +(?x,+(?y,?z)) = +(+(?z,?y),?x) ]
HS0:
   [ ]
ES1:
   [ +(?x,+(?y,?z)) = +(+(?z,?y),?x) ]
HS1:
   [ ]
Expand +(?x,+(?y,?z)) = +(+(?z,?y),?x)
   [ +(?x,?y_2) = +(+(?y_2,0),?x),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
ES2:
   [ +(?x,?y_2) = +(+(?y_2,0),?x),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS2:
   [ +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
STEP 1
ES:
   [ +(?x,?y_2) = +(+(?y_2,0),?x),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS:
   [ +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES0:
   [ +(?x,?y_2) = +(+(?y_2,0),?x),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS0:
   [ +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES1:
   [ +(?x,?y_2) = +(+(?y_2,0),?x),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS1:
   [ +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
Expand +(+(?y_2,0),?x) = +(?x,?y_2)
   [ +(0,?x) = +(?x,0),
     +(s(+(?x_5,0)),?x) = +(?x,s(?x_5)) ]
ES2:
   [ ?x = +(?x,0),
     s(+(+(?x_5,0),?x)) = +(?x,s(?x_5)),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS2:
   [ +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
STEP 2
ES:
   [ ?x = +(?x,0),
     s(+(+(?x_5,0),?x)) = +(?x,s(?x_5)),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS:
   [ +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES0:
   [ ?x = +(?x,0),
     s(+(?x,?x_5)) = +(?x,s(?x_5)),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS0:
   [ +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES1:
   [ ?x = +(?x,0),
     s(+(?x,?x_5)) = +(?x,s(?x_5)),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS1:
   [ +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
Expand +(?x,0) = ?x
   [ 0 = 0,
     s(+(?x_3,0)) = s(?x_3) ]
ES2:
   [ 0 = 0,
     s(+(?x_3,0)) = s(?x_3),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x),
     s(+(?x,?x_5)) = +(?x,s(?x_5)) ]
HS2:
   [ +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
STEP 3
ES:
   [ 0 = 0,
     s(+(?x_3,0)) = s(?x_3),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x),
     s(+(?x,?x_5)) = +(?x,s(?x_5)) ]
HS:
   [ +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES0:
   [ 0 = 0,
     s(?x_3) = s(?x_3),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x),
     s(+(?x,?x_5)) = +(?x,s(?x_5)) ]
HS0:
   [ +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES1:
   [ +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x),
     s(+(?x,?x_5)) = +(?x,s(?x_5)) ]
HS1:
   [ +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
Expand +(?x,s(?x_5)) = s(+(?x,?x_5))
   [ s(?x_5) = s(+(0,?x_5)),
     s(+(?x_8,s(?x_5))) = s(+(s(?x_8),?x_5)) ]
ES2:
   [ s(?x_5) = s(+(0,?x_5)),
     s(+(?x_8,s(?x_5))) = s(+(s(?x_8),?x_5)),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS2:
   [ +(?x,s(?x_5)) -> s(+(?x,?x_5)),
     +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
STEP 4
ES:
   [ s(?x_5) = s(+(0,?x_5)),
     s(+(?x_8,s(?x_5))) = s(+(s(?x_8),?x_5)),
     +(?x,s(+(?x_3,?y_3))) = +(+(?y_3,s(?x_3)),?x) ]
HS:
   [ +(?x,s(?x_5)) -> s(+(?x,?x_5)),
     +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES0:
   [ s(?x_5) = s(?x_5),
     +(?x_8,?x_5) = +(?x_8,?x_5),
     s(+(?x,+(?x_3,?y_3))) = s(+(+(?y_3,?x_3),?x)) ]
HS0:
   [ +(?x,s(?x_5)) -> s(+(?x,?x_5)),
     +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
ES1:
   [ ]
HS1:
   [ +(?x,s(?x_5)) -> s(+(?x,?x_5)),
     +(?x,0) -> ?x,
     +(+(?y_2,0),?x) -> +(?x,?y_2),
     +(?x,+(?y,?z)) -> +(+(?z,?y),?x) ]
Conj part consisits of inductive theorems of R0.
examples/additions/plus12.trs: Success(GCR)
(9 msec.)