MAYBE Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR x zs2 zs1 ys y x5 x4 x2 x3 x1) (RULES split(x,nil) -> tp2(nil,nil) split(x,cons(y,ys)) -> tp2(zs1,cons(y,zs2)) | split(x,ys) == tp2(zs1,zs2), le(x,y) == true split(x,cons(y,ys)) -> tp2(cons(y,zs1),zs2) | split(x,ys) == tp2(zs1,zs2), le(x,y) == false le(0,y) -> true le(s(x),0) -> false le(s(x),s(y)) -> le(x,y) ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR x zs2 zs1 ys y x5 x4 x2 x3 x1) (RULES split(x,nil) -> tp2(nil,nil) split(x,cons(y,ys)) -> tp2(zs1,cons(y,zs2)) | split(x,ys) == tp2(zs1,zs2), le(x,y) == true split(x,cons(y,ys)) -> tp2(cons(y,zs1),zs2) | split(x,ys) == tp2(zs1,zs2), le(x,y) == false le(0,y) -> true le(s(x),0) -> false le(s(x),s(y)) -> le(x,y) ) (VAR x5 x4 x2 zs2 zs1 x3 x1) (CONDITION split(x1,x3) == tp2(zs1,zs2), le(x1,x2) == true, split(x1,x3) == tp2(x4,x5), le(x1,x2) == false ) Optimized the infeasibility problem if possible. (VAR x5 x4 x2 zs2 zs1 x3 x1) (CONDITION split(x1,x3) == tp2(zs1,zs2), le(x1,x2) == true, split(x1,x3) == tp2(x4,x5), le(x1,x2) == false ) This is not ultra-RL and deterministic. The inverted system is ultra-RL and deterministic. MAYBE