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 x7 x3 x2 x1 x6 x4)
    (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 x7 x3 x2 x1 x6 x4)
    (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 x7 x3 x2 x1 x6 x4)
(CONDITION 
get(x4) == tp2(x6,x1), sub(0,x6) == x2, ssp\'(cons(x3,x1),x2) == x7
)

Optimized the infeasibility problem if possible.

(VAR x7 x3 x2 x1 x6 x4)
(CONDITION 
get(x4) == tp2(x6,x1), sub(0,x6) == x2, ssp\'(cons(x3,x1),x2) == x7
)

This is not ultra-RL and deterministic.


MAYBE