NO
Rewrite Rules:
   [ le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     if(le(?x,?y),s(?x),s(?y)) -> s(if(le(?x,?y),?x,?y)) ]
Apply Direct Methods...
Inner CPs:
   [ if(true,s(0),s(?y)) = s(if(le(0,?y),0,?y)),
     if(false,s(s(?x_1)),s(0)) = s(if(le(s(?x_1),0),s(?x_1),0)),
     if(le(?x_2,?y_2),s(s(?x_2)),s(s(?y_2))) = s(if(le(s(?x_2),s(?y_2)),s(?x_2),s(?y_2))) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Final result: not CR
new/le.trs: Success(not CR)
(22 msec.)