YES (ignored inputs)COMMENT the following rules are removed from the original TRS F ( H ( x ) , y ) -> F ( H ( x ) , G ( y ) ) F ( x , I ( y ) ) -> F ( G ( x ) , I ( y ) ) G ( x ) -> x Rewrite Rules: [ W(B(?x)) -> B(?x), W(W(?x)) -> W(?x), B(I(?x)) -> W(?x) ] Apply Direct Methods... Inner CPs: [ W(W(?x_2)) = B(I(?x_2)), W(B(?x)) = W(B(?x)), W(W(?x)) = W(W(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Combined result: CR /tmp/fileEsClfk.trs: Success(CR) (0 msec.)