Rewrite Rules: [ F(H(?x),?y) -> G(H(?x)), H(I(?x)) -> I(?x), F(I(?x),?y) -> G(I(?x)) ] Apply Direct Methods... Inner CPs: [ F(I(?x_1),?y) = G(H(I(?x_1))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth&Bendix Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/93.trs: Success(CR) (1 msec.)