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