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