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