NO Rewrite Rules: [ W(B(?x)) -> I(?x), B(S(?x)) -> S(?x), W(?x) -> I(?x) ] Apply Direct Methods... Inner CPs: [ W(S(?x_1)) = I(S(?x_1)) ] Outer CPs: [ I(?x) = I(B(?x)) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Final result: not CR 95.trs: Success(not CR) (0 msec.)