MAYBE

Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y x2)
    (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)
      gcd(x,x) -> x
      gcd(s(x),0) -> s(x)
      gcd(0,s(y)) -> s(y)
      gcd(s(x),s(y)) -> gcd(m(x,y),s(y)) | lt(y,x) == true
      gcd(s(x),s(y)) -> gcd(s(x),m(y,x)) | lt(x,y) == true
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y x2)
    (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)
      gcd(x,x) -> x
      gcd(s(x),0) -> s(x)
      gcd(0,s(y)) -> s(y)
      gcd(s(x),s(y)) -> gcd(m(x,y),s(y)) | lt(y,x) == true
      gcd(s(x),s(y)) -> gcd(s(x),m(y,x)) | lt(x,y) == true
    )

(VAR x2)
(CONDITION 
lt(x2,x2) == true
)

Optimized the infeasibility problem if possible.

(VAR x2)
(CONDITION 
lt(x2,x2) == true
)

This is not ultra-RL and deterministic.


MAYBE