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