MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y z)
    (RULES
      or(0,x) -> x
      or(x,0) -> x
      or(1,x) -> 1
      or(x,1) -> 1
      or(x,not(x)) -> 1
      or(not(x),x) -> 1
      and(0,x) -> 0
      and(x,0) -> 0
      and(1,x) -> x
      and(x,1) -> x
      and(x,not(x)) -> 0
      and(not(x),x) -> 0
      not(1) -> 0
      not(0) -> 1
      implies(x,y) -> 1 | not(x) == 1
      implies(x,y) -> 1 | y == 1
      implies(x,y) -> 0 | x == 1, y == 0
      f(x) -> f(0) | implies(x,0) == y, implies(x,y) == z, implies(z,0) == 1
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y z)
    (RULES
      or(0,x) -> x
      or(x,0) -> x
      or(1,x) -> 1
      or(x,1) -> 1
      or(x,not(x)) -> 1
      or(not(x),x) -> 1
      and(0,x) -> 0
      and(x,0) -> 0
      and(1,x) -> x
      and(x,1) -> x
      and(x,not(x)) -> 0
      and(not(x),x) -> 0
      not(1) -> 0
      not(0) -> 1
      implies(x,y) -> 1 | not(x) == 1
      implies(x,y) -> 1 | y == 1
      implies(x,y) -> 0 | x == 1, y == 0
      f(x) -> f(0) | implies(x,0) == y, implies(x,y) == z, implies(z,0) == 1
    )

(VAR z y x)
(CONDITION 
implies(x,0) == y, implies(x,y) == z, implies(z,0) == 1
)

Optimized the infeasibility problem if possible.

(VAR z y x)
(CONDITION 
implies(x,0) == y, implies(x,y) == z, implies(z,0) == 1
)

This is not ultra-RL and deterministic.


MAYBE