YES Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR x x1) (RULES even(0) -> true even(s(x)) -> false | odd(x) == false even(s(x)) -> true | odd(x) == true odd(0) -> false odd(s(x)) -> false | even(x) == false odd(s(x)) -> true | even(x) == true ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR x x1) (RULES even(0) -> true even(s(x)) -> false | odd(x) == false even(s(x)) -> true | odd(x) == true odd(0) -> false odd(s(x)) -> false | even(x) == false odd(s(x)) -> true | even(x) == true ) (VAR x1) (CONDITION even(x1) == false, even(x1) == true ) Optimized the infeasibility problem if possible. (VAR x1) (CONDITION even(x1) == false, even(x1) == true ) This is ultra-RL and deterministic. This is operationally terminating and confluent. (RTG_of_NARROWINGTREE (START Gamma[even(x1) == false : { e, 1 } & even(x1) == true : { e, 1 }] ) (NONTERMINALS Gamma[even(x1) == false : { e, 1 } & even(x1) == true : { e, 1 }] Gamma[even(x443) == false : { e, 1 }] Gamma[even(x448) == true : { e, 1 }] Gamma[odd(x458) == false : { e, 1 }] Gamma[odd(x464) == true : { e, 1 }] ) (RULES Gamma[even(x1) == false : { e, 1 } & even(x1) == true : { e, 1 }] -> EmptySet Gamma[even(x443) == false : { e, 1 }] -> (Rec(Gamma[odd(x458) == false : { e, 1 }], { x449 -> x458 }) . { x443 -> s(x449) }) Gamma[even(x448) == true : { e, 1 }] -> { x448 -> 0 } Gamma[even(x448) == true : { e, 1 }] -> (Rec(Gamma[odd(x464) == true : { e, 1 }], { x468 -> x464 }) . { x448 -> s(x468) }) Gamma[odd(x458) == false : { e, 1 }] -> { x458 -> 0 } Gamma[odd(x458) == false : { e, 1 }] -> (Rec(Gamma[even(x443) == false : { e, 1 }], { x485 -> x443 }) . { x458 -> s(x485) }) Gamma[odd(x464) == true : { e, 1 }] -> (Rec(Gamma[even(x448) == true : { e, 1 }], { x502 -> x448 }) . { x464 -> s(x502) }) ) ) YES