MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y r n xs r\' x1 x2)
    (RULES
      eq(0,0) -> true
      eq(s(x),0) -> false
      eq(0,s(y)) -> false
      eq(s(x),s(y)) -> eq(x,y)
      lte(0,y) -> true
      lte(s(x),0) -> false
      lte(s(x),s(y)) -> lte(x,y)
      m(0,s(y)) -> 0
      m(x,0) -> x
      m(s(x),s(y)) -> m(x,y)
      mod(0,y) -> 0
      mod(s(x),0) -> 0
      mod(s(x),s(y)) -> mod(m(x,y),s(y)) | lte(y,x) == true
      mod(s(x),s(y)) -> s(x) | lte(y,x) == false
      filter(n,r,nil) -> nil
      filter(n,r,cons(x,xs)) -> cons(x,filter(n,r,xs)) | mod(x,n) == r\', eq(r,r\') == true
      filter(n,r,cons(x,xs)) -> filter(n,r,xs) | mod(x,n) == r\', eq(r,r\') == false
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y r n xs r\' x1 x2)
    (RULES
      eq(0,0) -> true
      eq(s(x),0) -> false
      eq(0,s(y)) -> false
      eq(s(x),s(y)) -> eq(x,y)
      lte(0,y) -> true
      lte(s(x),0) -> false
      lte(s(x),s(y)) -> lte(x,y)
      m(0,s(y)) -> 0
      m(x,0) -> x
      m(s(x),s(y)) -> m(x,y)
      mod(0,y) -> 0
      mod(s(x),0) -> 0
      mod(s(x),s(y)) -> mod(m(x,y),s(y)) | lte(y,x) == true
      mod(s(x),s(y)) -> s(x) | lte(y,x) == false
      filter(n,r,nil) -> nil
      filter(n,r,cons(x,xs)) -> cons(x,filter(n,r,xs)) | mod(x,n) == r\', eq(r,r\') == true
      filter(n,r,cons(x,xs)) -> filter(n,r,xs) | mod(x,n) == r\', eq(r,r\') == false
    )

(VAR x1 x2)
(CONDITION 
lte(x2,x1) == true, lte(x2,x1) == false
)

Optimized the infeasibility problem if possible.

(VAR x1 x2)
(CONDITION 
lte(x2,x1) == true, lte(x2,x1) == false
)

This is not ultra-RL and deterministic.


MAYBE