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