YES (ignored inputs)COMMENT reduction failed Rewrite Rules: [ or(true,true) -> true, or(?x,?y) -> or(?y,?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ true = or(true,true) ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Linear Development Closed Direct Methods: CR Combined result: CR /tmp/filevQhziR.trs: Success(CR) (0 msec.)