MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR z y x)
    (RULES
      f(x,f(y,z)) -> f(f(x,y),f(x,z))
      f(f(x,y),z) -> f(f(x,z),f(y,z))
      f(f(x,y),f(y,z)) -> y
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (VAR z y x)
    (RULES
      f(x,f(y,z)) -> f(f(x,y),f(x,z))
      f(f(x,y),z) -> f(f(x,z),f(y,z))
      f(f(x,y),f(y,z)) -> y
    )

(VAR x)
(CONDITION 
f(a,a) == x, a == x
)

Optimized the infeasibility problem if possible.

(CONDITION 
a == f(a,a)
)

This is not ultra-RL and deterministic.


MAYBE