(ignored inputs)COMMENT from p.816 of \cite{Hue80} 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 ] Apply Direct Methods... Inner CPs: [ F(H(K1(A),K2(B))) = 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/50.trs: Success(CR) (0 msec.)