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 d == x, e == x ) Optimized the infeasibility problem if possible. (CONDITION e == d ) This is ultra-RL and deterministic. This is operationally terminating and confluent. (RTG_of_NARROWINGTREE (START Gamma[e == d : { e, 1 }] ) (NONTERMINALS Gamma[e == d : { e, 1 }] ) (RULES Gamma[e == d : { e, 1 }] -> EmptySet ) ) YES