(ignored inputs)COMMENT from Ex.6 of \cite{OO04} Rewrite Rules: [ f(g(?x,a,b)) -> ?x, g(f(h(c,d)),?x,?y) -> h(k1(?x),k2(?y)), k1(a) -> c, k2(b) -> d, f(h(k1(a),k2(b))) -> f(h(c,d)), f(h(c,k2(b))) -> f(h(c,d)), f(h(k1(a),d)) -> f(h(c,d)) ] Apply Direct Methods... Inner CPs: [ f(h(k1(a),k2(b))) = f(h(c,d)), f(h(c,k2(b))) = f(h(c,d)), f(h(k1(a),d)) = f(h(c,d)), f(h(c,d)) = f(h(c,d)), f(h(c,d)) = f(h(c,d)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth&Bendix Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/66.trs: Success(CR) (1 msec.)