MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR y x z v u x5 x2 x1 x4)
    (RULES
      last(cons(x,y)) -> x | y == nil
      last(cons(x,y)) -> z | y == cons(u,v), last(y) == z
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR y x z v u x5 x2 x1 x4)
    (RULES
      last(cons(x,y)) -> x | y == nil
      last(cons(x,y)) -> z | y == cons(u,v), last(y) == z
    )

(VAR x5 x2 x1 x4)
(CONDITION 
x4 == nil, x4 == cons(x1,x2), last(x4) == x5
)

Optimized the infeasibility problem if possible.

(VAR x5 x2 x1 x4)
(CONDITION 
x4 == nil, x4 == cons(x1,x2), last(x4) == x5
)

This is not ultra-RL and deterministic.


MAYBE