YES (ignored inputs)COMMENT [17] Example 7 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama Rewrite Rules: [ f(i(?x),g(a)) -> f(j(?x,?x),g(b)), b -> a, i(?x) -> j(?x,?x) ] Apply Direct Methods... Inner CPs: [ f(j(?x_1,?x_1),g(a)) = f(j(?x_1,?x_1),g(b)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Combined result: CR 67.trs: Success(CR) (0 msec.)