YES
(ignored inputs)COMMENT [Kapur et al. IC 1999] Example 2.2
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ f(g(f(?x))) -> g(f(g(?x))),
     f(c) -> c,
     g(c) -> c ]
Constructors: {c}
Defined function symbols: {f,g}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ f(c) -> c,
     g(c) -> c ]
   [ f(g(f(?x))) -> g(f(g(?x))) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Elem}
Signature:
   [ f : Elem -> Elem,
     g : Elem -> Elem,
     c : Elem ]
Rule Part:
   [ f(c) -> c,
     g(c) -> c ]
Conjecture Part:
   [ f(g(f(?x))) = g(f(g(?x))) ]
Precedence (by weight): {(c,0),(f,2),(g,1)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ f(c) -> c,
     g(c) -> c ]
Conjectures:
   [ f(g(f(?x))) = g(f(g(?x))) ]
STEP 0
ES:
   [ f(g(f(?x))) = g(f(g(?x))) ]
HS:
   [ ]
ES0:
   [ f(g(f(?x))) = g(f(g(?x))) ]
HS0:
   [ ]
ES1:
   [ f(g(f(?x))) = g(f(g(?x))) ]
HS1:
   [ ]
Expand f(g(f(?x))) = g(f(g(?x)))
   [ f(g(c)) = g(f(g(c))) ]
ES2:
   [ c = g(f(g(c))) ]
HS2:
   [ f(g(f(?x))) -> g(f(g(?x))) ]
STEP 1
ES:
   [ c = g(f(g(c))) ]
HS:
   [ f(g(f(?x))) -> g(f(g(?x))) ]
ES0:
   [ c = c ]
HS0:
   [ f(g(f(?x))) -> g(f(g(?x))) ]
ES1:
   [ ]
HS1:
   [ f(g(f(?x))) -> g(f(g(?x))) ]
Conj part consisits of inductive theorems of R0.
examples/additions/elem1.trs: Success(GCR)
(6 msec.)