YES (ignored inputs)COMMENT the following rules are removed from the original TRS h ( f ( x ) ) -> h ( g ( x ) ) Rewrite Rules: [ f(?x) -> h(f(?x)), f(?x) -> g(?x), g(?x) -> h(g(?x)) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ h(f(?x)) = g(?x) ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Linear Development Closed Direct Methods: CR Combined result: CR /tmp/file2K1AzJ.trs: Success(CR) (0 msec.)