YES Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR x) (RULES a -> a | b == x, c == x b -> d | d == x, e == x c -> d | d == x, e == x ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (VAR x) (VAR x) (CONDITION b == x, c == x ) Optimized the infeasibility problem if possible. (CONDITION c == b ) This is ultra-RL and deterministic. This is operationally terminating and confluent. (RTG_of_NARROWINGTREE (START Gamma[c == b : { e, 1 }] ) (NONTERMINALS Gamma[c == b : { e, 1 }] ) (RULES Gamma[c == b : { e, 1 }] -> EmptySet ) ) YES