MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y r q x4 x3 x2 x1)
    (RULES
      lt(x,0) -> false
      lt(0,s(x)) -> true
      lt(s(x),s(y)) -> lt(x,y)
      m(0,s(y)) -> 0
      m(x,0) -> x
      m(s(x),s(y)) -> m(x,y)
      div(0,s(x)) -> pair(0,0)
      div(s(x),s(y)) -> pair(0,s(x)) | lt(x,y) == true
      div(s(x),s(y)) -> pair(s(q),r) | lt(x,y) == false, div(m(x,y),s(y)) == pair(q,r)
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y r q x4 x3 x2 x1)
    (RULES
      lt(x,0) -> false
      lt(0,s(x)) -> true
      lt(s(x),s(y)) -> lt(x,y)
      m(0,s(y)) -> 0
      m(x,0) -> x
      m(s(x),s(y)) -> m(x,y)
      div(0,s(x)) -> pair(0,0)
      div(s(x),s(y)) -> pair(0,s(x)) | lt(x,y) == true
      div(s(x),s(y)) -> pair(s(q),r) | lt(x,y) == false, div(m(x,y),s(y)) == pair(q,r)
    )

(VAR x4 x3 x2 x1)
(CONDITION 
lt(x1,x2) == true, lt(x1,x2) == false, div(m(x1,x2),s(x2)) == pair(x3,x4)
)

Optimized the infeasibility problem if possible.

(VAR x4 x3 x2 x1)
(CONDITION 
lt(x1,x2) == true, lt(x1,x2) == false, div(m(x1,x2),s(x2)) == pair(x3,x4)
)

This is not ultra-RL and deterministic.


MAYBE