YES (ignored inputs)COMMENT submitted by: Akihisa Yamada used by COPS #1278 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 1651.trs: Success(CR) (12 msec.)