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