MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y q n n\' z x4 x2 x1)
    (RULES
      add(0,x) -> x
      add(s(x),y) -> s(add(x,y))
      mult(0,y) -> 0
      mult(s(x),y) -> add(mult(x,y),y)
      lte(0,y) -> true
      lte(s(x),0) -> false
      lte(s(x),s(y)) -> lte(x,y)
      minus(0,s(y)) -> 0
      minus(x,0) -> x
      minus(s(x),s(y)) -> minus(x,y)
      mod(0,y) -> 0
      mod(x,0) -> x
      mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true
      mod(x,s(y)) -> x | lte(s(y),x) == false
      div(0,s(x)) -> 0
      div(s(x),s(y)) -> 0 | lte(s(x),y) == true
      div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q
      power(x,0) -> s(0)
      power(x,n) -> mult(mult(y,y),s(0)) | n == s(n\'), mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y
      power(x,n) -> mult(mult(y,y),x) | n == s(n\'), mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y q n n\' z x4 x2 x1)
    (RULES
      add(0,x) -> x
      add(s(x),y) -> s(add(x,y))
      mult(0,y) -> 0
      mult(s(x),y) -> add(mult(x,y),y)
      lte(0,y) -> true
      lte(s(x),0) -> false
      lte(s(x),s(y)) -> lte(x,y)
      minus(0,s(y)) -> 0
      minus(x,0) -> x
      minus(s(x),s(y)) -> minus(x,y)
      mod(0,y) -> 0
      mod(x,0) -> x
      mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) == true
      mod(x,s(y)) -> x | lte(s(y),x) == false
      div(0,s(x)) -> 0
      div(s(x),s(y)) -> 0 | lte(s(x),y) == true
      div(s(x),s(y)) -> s(q) | lte(s(x),y) == false, div(minus(x,y),s(y)) == q
      power(x,0) -> s(0)
      power(x,n) -> mult(mult(y,y),s(0)) | n == s(n\'), mod(n,s(s(0))) == 0, power(x,div(n,s(s(0)))) == y
      power(x,n) -> mult(mult(y,y),x) | n == s(n\'), mod(n,s(s(0))) == s(z), power(x,div(n,s(s(0)))) == y
    )

(VAR x4 x2 x1)
(CONDITION 
0 == s(x1), mod(0,s(s(0))) == 0, power(x2,div(0,s(s(0)))) == x4
)

Optimized the infeasibility problem if possible.

(VAR x4 x2 x1)
(CONDITION 
0 == s(x1), mod(0,s(s(0))) == 0, power(x2,div(0,s(s(0)))) == x4
)

This is not ultra-RL and deterministic.


MAYBE