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