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