MAYBE Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR x y xs x1) (RULES le(x,0) -> false le(0,s(y)) -> true le(s(x),s(y)) -> le(x,y) min(cons(x,nil)) -> x min(cons(x,xs)) -> x | le(x,min(xs)) == true min(cons(x,xs)) -> min(xs) | le(x,min(xs)) == false ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR x y xs x1) (RULES le(x,0) -> false le(0,s(y)) -> true le(s(x),s(y)) -> le(x,y) min(cons(x,nil)) -> x min(cons(x,xs)) -> x | le(x,min(xs)) == true min(cons(x,xs)) -> min(xs) | le(x,min(xs)) == false ) (VAR x1) (CONDITION le(x1,min(nil)) == false ) Optimized the infeasibility problem if possible. (VAR x1) (CONDITION le(x1,min(nil)) == false ) This is not ultra-RL and deterministic. MAYBE