MAYBE Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari". (CONDITIONTYPE ORIENTED) (VAR x x1) (RULES e(0) -> true e(s(x)) -> true | o(x) == true e(s(x)) -> false | e(x) == true o(0) -> true o(s(x)) -> true | e(x) == true o(s(x)) -> false | o(x) == true ) No "->="-rules. Decomposed conditions and removed infeasible rules if possible. (CONDITIONTYPE ORIENTED) (VAR x x1) (RULES e(0) -> true e(s(x)) -> true | o(x) == true e(s(x)) -> false | e(x) == true o(0) -> true o(s(x)) -> true | e(x) == true o(s(x)) -> false | o(x) == true ) (VAR x1) (CONDITION e(x1) == true, o(x1) == true ) Optimized the infeasibility problem if possible. (VAR x1) (CONDITION e(x1) == true, o(x1) == true ) This is ultra-RL and deterministic. This is not operationally terminating and confluent. This is a constructor-based system. (RTG_of_NARROWINGTREE (START Gamma[e(x1) == true : { e, 1 } & o(x1) == true : { e, 1 }] ) (NONTERMINALS Gamma[e(x1) == true : { e, 1 } & o(x1) == true : { e, 1 }] Gamma[e(x183) == true : { e, 1 }] Gamma[o(x188) == true : { e, 1 }] ) (RULES Gamma[e(x1) == true : { e, 1 } & o(x1) == true : { e, 1 }] -> (Rec(Gamma[e(x183) == true : { e, 1 }], { x1 -> x183 }) & Rec(Gamma[o(x188) == true : { e, 1 }], { x1 -> x188 })) Gamma[e(x183) == true : { e, 1 }] -> { x183 -> 0 } Gamma[e(x183) == true : { e, 1 }] -> (Rec(Gamma[o(x188) == true : { e, 1 }], { x189 -> x188 }) . { x183 -> s(x189) }) Gamma[o(x188) == true : { e, 1 }] -> { x188 -> 0 } Gamma[o(x188) == true : { e, 1 }] -> (Rec(Gamma[e(x183) == true : { e, 1 }], { x207 -> x183 }) . { x188 -> s(x207) }) ) ) Failed to prove infeasibility of the linearized conditions by means of narrowing trees. This is not ultra-RL and deterministic. The inverted system is ultra-RL and deterministic. (RTG_of_NARROWINGTREE (START Gamma[true == o(x1) : { e, 1 } & true == e(x1) : { e, 1 }] ) (NONTERMINALS Gamma[true == o(x1) : { e, 1 } & true == e(x1) : { e, 1 }] Gamma[true == o2 : { e, 1 }] ) (RULES Gamma[true == o(x1) : { e, 1 } & true == e(x1) : { e, 1 }] -> ((Rec(Gamma[true == o2 : { e, 1 }], { o1 -> o2 }) & { o1 -> o(x1) }) & (Rec(Gamma[true == o2 : { e, 1 }], { e1 -> o2 }) & { e1 -> e(x1) })) Gamma[true == o2 : { e, 1 }] -> { o2 -> true } Gamma[true == o2 : { e, 1 }] -> { o2 -> e(0) } Gamma[true == o2 : { e, 1 }] -> ((Rec(Gamma[true == o2 : { e, 1 }], { o3 -> o2 }) & { o3 -> o(x239) }) & { o2 -> e(s(x239)) }) Gamma[true == o2 : { e, 1 }] -> { o2 -> o(0) } Gamma[true == o2 : { e, 1 }] -> ((Rec(Gamma[true == o2 : { e, 1 }], { e2 -> o2 }) & { e2 -> e(x241) }) & { o2 -> o(s(x241)) }) ) ) MAYBE