MAYBE

Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR xs ys\' v ws y\' w xs\' x\' zs z ys y x4 x3 x2)
    (RULES
      ssp\'(xs,0) -> nil
      ssp\'(cons(y\',ws),v) -> cons(y\',ys\') | sub(v,y\') == w, ssp\'(ws,w) == ys\'
      ssp\'(cons(x\',xs\'),v) -> cons(y\',ys\') | get(xs\') == tp2(y\',zs), sub(v,y\') == w, ssp\'(cons(x\',zs),w) == ys\'
      sub(z,0) -> z
      sub(s(v),s(w)) -> z | sub(v,w) == z
      get(cons(y,ys)) -> tp2(y,ys)
      get(cons(x\',xs\')) -> tp2(y,cons(x\',zs)) | get(xs\') == tp2(y,zs)
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR xs ys\' v ws y\' w xs\' x\' zs z ys y x4 x3 x2)
    (RULES
      ssp\'(xs,0) -> nil
      ssp\'(cons(y\',ws),v) -> cons(y\',ys\') | sub(v,y\') == w, ssp\'(ws,w) == ys\'
      ssp\'(cons(x\',xs\'),v) -> cons(y\',ys\') | get(xs\') == tp2(y\',zs), sub(v,y\') == w, ssp\'(cons(x\',zs),w) == ys\'
      sub(z,0) -> z
      sub(s(v),s(w)) -> z | sub(v,w) == z
      get(cons(y,ys)) -> tp2(y,ys)
      get(cons(x\',xs\')) -> tp2(y,cons(x\',zs)) | get(xs\') == tp2(y,zs)
    )

(VAR x4 x3 x2)
(CONDITION 
get(x2) == tp2(x3,x4)
)

Optimized the infeasibility problem if possible.

(VAR x4 x3 x2)
(CONDITION 
get(x2) == tp2(x3,x4)
)

This is not ultra-RL and deterministic.


MAYBE