MAYBE Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR y x x1) (RULES f(x,y) -> g(x) | c(g(x)) == c(a) f(x,y) -> h(x) | c(h(x)) == c(a) g(s(x)) -> x h(s(x)) -> x b -> b ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR y x x1) (RULES f(x,y) -> g(x) | g(x) == a f(x,y) -> h(x) | h(x) == a g(s(x)) -> x h(s(x)) -> x b -> b ) (VAR x1) (CONDITION c(g(x1)) == c(a), c(h(x1)) == c(a) ) Optimized the infeasibility problem if possible. (VAR x1) (CONDITION g(x1) == a, h(x1) == a ) This is not ultra-RL and deterministic. MAYBE