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