NO (ignored inputs)COMMENT submitted by: Akihisa Yamada used by COPS #1277 Rewrite Rules: [ f(f(?x)) -> f(g(f(?x))), f(?x) -> ?x ] Apply Direct Methods... Inner CPs: [ f(?x_1) = f(g(f(?x_1))), f(f(g(f(?x)))) = f(g(f(f(?x)))) ] Outer CPs: [ f(g(f(?x))) = f(?x) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Combined result: not CR 1650.trs: Success(not CR) (0 msec.)