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