MAYBE

Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y ys x2 x1)
    (RULES
      lt(x,0) -> false
      lt(0,s(y)) -> true
      lt(s(x),s(y)) -> lt(x,y)
      cons(x,cons(y,ys)) -> cons(y,cons(x,ys)) | lt(x,y) == true
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y ys x2 x1)
    (RULES
      lt(x,0) -> false
      lt(0,s(y)) -> true
      lt(s(x),s(y)) -> lt(x,y)
      cons(x,cons(y,ys)) -> cons(y,cons(x,ys)) | lt(x,y) == true
    )

(VAR x2 x1 x)
(CONDITION 
lt(x,x1) == true, lt(x1,x2) == true
)

Optimized the infeasibility problem if possible.

(VAR x2 x1 x)
(CONDITION 
lt(x,x1) == true, lt(x1,x2) == true
)

This is not ultra-RL and deterministic.

The inverted system is ultra-RL and deterministic.


MAYBE