YES
(ignored inputs)COMMENT translated from Cops 29
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ -(+(?x,-(?x))) -> 0,
     +(?x,-(?x)) -> 0,
     -(+(0,0)) -> 0,
     +(0,0) -> 0,
     -(0) -> 0 ]
Constructors: {0}
Defined function symbols: {+,-}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ +(0,0) -> 0,
     -(0) -> 0 ]
   [ -(+(0,0)) -> 0,
     -(+(?x,-(?x))) -> 0,
     +(?x,-(?x)) -> 0 ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Elem}
Signature:
   [ + : Elem,Elem -> Elem,
     - : Elem -> Elem,
     0 : Elem ]
Rule Part:
   [ +(0,0) -> 0,
     -(0) -> 0 ]
Conjecture Part:
   [ -(+(0,0)) = 0,
     -(+(?x,-(?x))) = 0,
     +(?x,-(?x)) = 0 ]
Precedence (by weight): {(+,0),(-,2),(0,1)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ +(0,0) -> 0,
     -(0) -> 0 ]
Conjectures:
   [ -(+(0,0)) = 0,
     -(+(?x,-(?x))) = 0,
     +(?x,-(?x)) = 0 ]
STEP 0
ES:
   [ -(+(0,0)) = 0,
     -(+(?x,-(?x))) = 0,
     +(?x,-(?x)) = 0 ]
HS:
   [ ]
ES0:
   [ 0 = 0,
     -(+(?x,-(?x))) = 0,
     +(?x,-(?x)) = 0 ]
HS0:
   [ ]
ES1:
   [ -(+(?x,-(?x))) = 0,
     +(?x,-(?x)) = 0 ]
HS1:
   [ ]
Expand +(?x,-(?x)) = 0
   [ +(0,0) = 0 ]
ES2:
   [ 0 = 0,
     -(+(?x,-(?x))) = 0 ]
HS2:
   [ +(?x,-(?x)) -> 0 ]
STEP 1
ES:
   [ 0 = 0,
     -(+(?x,-(?x))) = 0 ]
HS:
   [ +(?x,-(?x)) -> 0 ]
ES0:
   [ 0 = 0,
     0 = 0 ]
HS0:
   [ +(?x,-(?x)) -> 0 ]
ES1:
   [ ]
HS1:
   [ +(?x,-(?x)) -> 0 ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/cr/29.trs: Success(GCR)
(9 msec.)