Rewrite Rules: [ F(?x,?x) -> G(?x), A -> B ] 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/101.trs: Success(CR) (1 msec.)