MAYBE Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR x) (RULES a -> a | f(a) == a f(x) -> a | x == b ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR x) (RULES a -> a | f(a) == a f(x) -> a | x == b ) (CONDITION f(a) == a ) Optimized the infeasibility problem if possible. (CONDITION f(a) == a ) This is not ultra-RL and deterministic. The inverted system is ultra-RL and deterministic. MAYBE