YES (ignored inputs)COMMENT doi:10.1007/BFb0052357 [21] TRS R_1 , attributed to Middeldorp submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama Rewrite Rules: [ f(g(g(?x))) -> a, f(g(h(?x))) -> b, f(h(g(?x))) -> b, f(h(h(?x))) -> c, g(?x) -> h(?x), a -> b, b -> c ] Apply Direct Methods... Inner CPs: [ f(h(g(?x))) = a, f(g(h(?x_4))) = a, f(h(h(?x_1))) = b, f(h(h(?x_4))) = b ] Outer CPs: [ ] Linear (inner) Parallel CPs: [ f(g(h(?x_11))) = a {?x_11}, f(h(g(?x))) = a {?x}, f(h(h(?x))) = b {?x}, f(h(h(?x_5))) = b {?x_5} ] Toyama (Parallel CPs) Direct Methods: CR Combined result: CR 73.trs: Success(CR) (0 msec.)