MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR y x r q z w)
    (RULES
      div(x,y) -> pair(0,y) | greater(y,x) == true
      div(x,y) -> pair(s(q),r) | leq(y,x) == true, div(m(x,y),y) == pair(q,r)
      m(x,0) -> x
      m(0,y) -> 0
      m(s(x),s(y)) -> m(x,y)
      greater(s(x),s(y)) -> greater(x,y)
      greater(s(x),0) -> true
      leq(s(x),s(y)) -> leq(x,y)
      leq(0,x) -> true
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR y x r q z w)
    (RULES
      div(x,y) -> pair(0,y) | greater(y,x) == true
      div(x,y) -> pair(s(q),r) | leq(y,x) == true, div(m(x,y),y) == pair(q,r)
      m(x,0) -> x
      m(0,y) -> 0
      m(s(x),s(y)) -> m(x,y)
      greater(s(x),s(y)) -> greater(x,y)
      greater(s(x),0) -> true
      leq(s(x),s(y)) -> leq(x,y)
      leq(0,x) -> true
    )

(VAR z y w x)
(CONDITION 
leq(x,w) == true, div(m(w,x),x) == pair(y,z), greater(x,w) == true
)

Optimized the infeasibility problem if possible.

(VAR z y w x)
(CONDITION 
leq(x,w) == true, div(m(w,x),x) == pair(y,z), greater(x,w) == true
)

This is not ultra-RL and deterministic.


MAYBE