(ignored inputs)COMMENT from p.209 of \cite{Der97} Rewrite Rules: [ f(?x) -> g(a), g(?x) -> ?x, h(?x,?x) -> 0, a -> 1 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth&Bendix Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/18.trs: Success(CR) (1 msec.)