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