MAYBE

Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR n m)
    (RULES
      ack(s(m),s(n)) -> ack(m,ack(s(m),n))
      ack(s(m),O) -> ack(m,s(O))
      ack(O,n) -> s(n)
      isNat(O) -> true
      isNat(s(m)) -> isNat(m)
      isNat(true) -> false
      isNat(false) -> false
      seven -> s(s(s(s(s(s(s(O)))))))
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (VAR n m)
    (RULES
      ack(s(m),s(n)) -> ack(m,ack(s(m),n))
      ack(s(m),O) -> ack(m,s(O))
      ack(O,n) -> s(n)
      isNat(O) -> true
      isNat(s(m)) -> isNat(m)
      isNat(true) -> false
      isNat(false) -> false
      seven -> s(s(s(s(s(s(s(O)))))))
    )

(CONDITION 
isNat(ack(seven,seven)) == true
)

Optimized the infeasibility problem if possible.

(CONDITION 
isNat(ack(seven,seven)) == true
)

This is not ultra-RL and deterministic.

The inverted system is ultra-RL and deterministic.


MAYBE