MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     prec(0) -> 0,
     prec(s(?x)) -> ?x,
     le(?x,?y) -> if(zero(?x),true,le(prec(?x),prec(?y))),
     ge(?x,?y) -> if(zero(?y),true,ge(prec(?x),prec(?y))),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     le(s(?x),s(?y)) -> le(?x,?y),
     ge(s(?x),s(?y)) -> ge(?x,?y) ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,true,false}
Defined function symbols: {ge,if,le,prec,zero}
Constructor subsystem:
   [ ]
no strongly quasi-reducible parts found
new/le-ge.trs: Failure(unknown)
(1598 msec.)