(ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z061 Rewrite Rules: [ b(b(c(a(b(c(?x)))))) -> a(b(b(c(b(c(a(?x))))))) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Linear Development Closed Direct Methods: CR Combined result: CR 941.trs: Success(CR) YES (39 msec.)