(ignored inputs)COMMENT due to A.Middeldorp , R_1 in p.14 of \cite{Oku98} Rewrite Rules: [ f(g(g(?x))) -> a, f(g(h(?x))) -> b, f(h(g(?x))) -> b, f(h(h(?x))) -> c, g(?x) -> h(?x), a -> b, b -> c ] Apply Direct Methods... Inner CPs: [ f(h(g(?x))) = a, f(g(h(?x_4))) = a, f(h(h(?x_1))) = b, f(h(h(?x_4))) = b ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth&Bendix Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/73.trs: Success(CR) (1 msec.)