(ignored inputs)COMMENT from p.811 of \cite{Hue80} Rewrite Rules: [ H(H(?x)) -> K(?x), H(K(?x)) -> K(H(?x)) ] Apply Direct Methods... Inner CPs: [ H(K(H(?x_1))) = K(K(?x_1)), H(K(?x)) = K(H(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth&Bendix Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/45.trs: Success(CR) (6 msec.)