NO (ignored inputs)COMMENT Example 6.2.7 of \cite{BN98} Rewrite Rules: [ f(f(?x)) -> g(?x) ] Apply Direct Methods... Inner CPs: [ f(g(?x)) = g(f(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Final result: not CR 7.trs: Success(not CR) (0 msec.)