(ignored inputs)COMMENT from p.814 of \cite{Hue80}
Rewrite Rules:
   [ H(F(?x,?y)) -> F(H(R(?x)),?y),
     F(?x,K(?y,?z)) -> G(P(?y),Q(?z,?x)),
     H(Q(?x,?y)) -> Q(?x,H(R(?y))),
     Q(?x,H(R(?y))) -> H(Q(?x,?y)),
     H(G(?x,?y)) -> G(?x,H(?y)) ]
Apply Direct Methods...
Inner CPs:
   [ H(G(P(?y_1),Q(?z_1,?x_1))) = F(H(R(?x_1)),K(?y_1,?z_1)),
     H(H(Q(?x_3,?y_3))) = Q(?x_3,H(R(H(R(?y_3))))) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
Strongly Closed
Direct Methods: CR

Final result: CR
/local-scratch/hzankl/2012/cops2012/48.trs: Success(CR)
(94 msec.)