YES (ignored inputs)COMMENT cops number: 88 submitted by: Takahito Aoto , Junichi Yoshida , Yoshihito Toyama [27] Example 3.3 Rewrite Rules: [ p(?x) -> q(?x), p(?x) -> r(?x), q(?x) -> s(p(?x)), r(?x) -> s(p(?x)), s(?x) -> f(p(?x)) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ q(?x) = r(?x) ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Linear Development Closed Direct Methods: CR Combined result: CR cops-7GlEbeVR.trs: Success(CR) (31 msec.)