(ignored inputs)COMMENT Example 4.2.2 of \cite{Ohl94thesis} Rewrite Rules: [ F(?x,?y) -> c(?y), G(?x) -> ?x, f(?x) -> g(?x), g(?x) -> c(?x) ] 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/71.trs: Success(CR) (0 msec.)