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