NO
Rewrite Rules:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x,nil) -> true,
     leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     and(true,true) -> true,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x,?ys)) -> insert(?x,sort(?ys)),
     insert(?x,nil) -> cons(?x,nil),
     insert(?x,cons(?y,?ys)) -> if(le(?x,?y),cons(?x,cons(?y,?ys)),cons(?y,insert(?x,?ys))),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     ordered(sort(?xs)) -> true ]
Apply Direct Methods...
Inner CPs:
   [ ordered(nil) = true,
     ordered(insert(?x_8,sort(?ys_8))) = true ]
Outer CPs:
   [ true = true,
     true = true,
     true = true ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Final result: not CR
new/insert.trs: Success(not CR)
(33 msec.)