(ignored inputs)COMMENT from Ex.7 of \cite{OO04} Rewrite Rules: [ f(i(?x),g(a)) -> f(j(?x,?x),g(b)), b -> a, i(?x) -> j(?x,?x) ] Apply Direct Methods... Inner CPs: [ f(j(?x_1,?x_1),g(a)) = f(j(?x_1,?x_1),g(b)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth&Bendix Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/67.trs: Success(CR) (0 msec.)