YES
(ignored inputs)COMMENT translated from Cops 160
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Constructors: {0,s}
Defined function symbols: {+}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)) ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ + : Nat,Nat -> Nat,
     0 : Nat,
     s : Nat -> Nat ]
Rule Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)) ]
Conjecture Part:
   [ +(?x,+(?y,?z)) = +(+(?x,?y),?z),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
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:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)) ]
Conjectures:
   [ +(?x,+(?y,?z)) = +(+(?x,?y),?z),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
STEP 0
ES:
   [ +(?x,+(?y,?z)) = +(+(?x,?y),?z),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ ]
ES0:
   [ +(?x,+(?y,?z)) = +(+(?x,?y),?z),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ ]
ES1:
   [ +(?x,+(?y,?z)) = +(+(?x,?y),?z),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ ]
Expand +(?x,+(?y,?z)) = +(+(?x,?y),?z)
   [ +(?x,?x_1) = +(+(?x,?x_1),0),
     +(?x,s(+(?x_2,?y_2))) = +(+(?x,?x_2),s(?y_2)) ]
ES2:
   [ +(?x,?x_1) = +(+(?x,?x_1),0),
     s(+(?x,+(?x_2,?y_2))) = +(+(?x,?x_2),s(?y_2)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ]
STEP 1
ES:
   [ +(?x,?x_1) = +(+(?x,?x_1),0),
     s(+(?x,+(?x_2,?y_2))) = +(+(?x,?x_2),s(?y_2)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ]
ES0:
   [ +(?x,?x_1) = +(?x,?x_1),
     s(+(?x,+(?x_2,?y_2))) = s(+(+(?x,?x_2),?y_2)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ]
ES1:
   [ ]
HS1:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/open/160.trs: Success(GCR)
(10 msec.)