(ignored inputs)COMMENT doi:10.1007/978-1-4757-3661-8 [18] Exercise 4.2.2 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama Rewrite Rules: [ b(w(?x)) -> w(w(w(b(?x)))), w(b(?x)) -> b(?x), b(b(?x)) -> w(w(w(w(?x)))), w(w(?x)) -> w(?x) ] Apply Direct Methods... Inner CPs: [ b(b(?x_1)) = w(w(w(b(b(?x_1))))), b(w(?x_3)) = w(w(w(b(w(?x_3))))), w(w(w(w(b(?x))))) = b(w(?x)), w(w(w(w(w(?x_2))))) = b(b(?x_2)), b(w(w(w(b(?x))))) = w(w(w(w(w(?x))))), w(b(?x_1)) = w(b(?x_1)), b(w(w(w(w(?x))))) = w(w(w(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 68.trs: Success(CR) YES (5 msec.)