MAYBE Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR y x x1) (RULES f(x,y) -> g(s(x)) | c(g(x)) == c(a) f(x,y) -> h(s(x)) | c(h(x)) == c(a) g(s(x)) -> x h(s(x)) -> x ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR y x x1) (RULES f(x,y) -> g(s(x)) | g(x) == a f(x,y) -> h(s(x)) | h(x) == a g(s(x)) -> x h(s(x)) -> x ) (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