NO (ignored inputs)COMMENT reduction failed Rewrite Rules: [ f(g(f(?x))) -> ?x, f(g(?x)) -> g(f(?x)) ] Apply Direct Methods... Inner CPs: [ f(g(g(f(?x_1)))) = g(?x_1), f(g(?x)) = g(f(?x)) ] Outer CPs: [ ?x = g(f(f(?x))) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Combined result: not CR /tmp/fileG0oxEH.trs: Success(not CR) (3 msec.)