MAYBE Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR x x1) (RULES f(x) -> A | s(x) == t f(x) -> B | s(x) == t s(a) -> t s(b) -> t a -> c b -> c g(x,x) -> h(x,x) ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR x x1) (RULES f(x) -> A | s(x) == t f(x) -> B | s(x) == t s(a) -> t s(b) -> t a -> c b -> c g(x,x) -> h(x,x) ) (VAR x1) (CONDITION s(x1) == t ) Optimized the infeasibility problem if possible. (VAR x1) (CONDITION s(x1) == t ) This is not ultra-RL and deterministic. MAYBE