(ignored inputs)COMMENT Example 3.1 of cite{Toy88}
Rewrite Rules:
   [ f(?x) -> g(?x),
     f(?x) -> h(f(?x)),
     h(f(?x)) -> h(g(?x)),
     g(?x) -> h(g(?x)) ]
Apply Direct Methods...
Inner CPs:
   [ h(g(?x)) = h(g(?x)),
     h(h(f(?x_1))) = h(g(?x_1)) ]
Outer CPs:
   [ g(?x) = h(f(?x)) ]
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/86.trs: Success(CR)
(1 msec.)