NO
(ignored inputs)COMMENT reduction failed
Rewrite Rules:
   [ not(true) -> false,
     not(false) -> true,
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     implies(true,?y) -> ?y,
     implies(false,?y) -> true,
     implies(?x,?y) -> or(not(?x),?y) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ true = true,
     ?y_2 = or(not(true),?y_2),
     true = or(not(false),?y_3) ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), not WCR
Knuth & Bendix
Direct Methods: not CR

Combined result: not CR
/tmp/file7dLIgu.trs: Success(not CR)
(0 msec.)