MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x x\'\' x\' y y\'\' y\' x3 x2 x1)
    (RULES
      f(x\',x\'\') -> h(x,f(x,b)) | x\' == x, x\'\' == x
      f(g(y\'),y\'\') -> h(y,f(g(y),a)) | y\' == y, y\'\' == y
      a -> b
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x x\'\' x\' y y\'\' y\' x3 x2 x1)
    (RULES
      f(x\',x\'\') -> h(x,f(x,b)) | x\' == x, x\'\' == x
      f(g(y\'),y\'\') -> h(y,f(g(y),a)) | y\' == y, y\'\' == y
      a -> b
    )

(VAR x3 x2 x x1)
(CONDITION 
g(x1) == x, x2 == x, x1 == x3, x2 == x3
)

Optimized the infeasibility problem if possible.

(VAR x3 x2 x x1)
(CONDITION 
g(x1) == x, x2 == x, x1 == x3, x2 == x3
)

This is not ultra-RL and deterministic.


MAYBE