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