MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR z2 z1 rest y x x5 x4 x2 x1)
    (RULES
      cons(x,cons(y,rest)) -> cons(z1,cons(z2,rest)) | orient(x,y) == pair(z1,z2)
      cons(x,cons(x,rest)) -> cons(x,rest)
      orient(s(x),s(y)) -> pair(s(z1),s(z2)) | orient(x,y) == pair(z1,z2)
      orient(s(x),0) -> pair(0,s(x))
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR z2 z1 rest y x x5 x4 x2 x1)
    (RULES
      cons(x,cons(y,rest)) -> cons(z1,cons(z2,rest)) | orient(x,y) == pair(z1,z2)
      cons(x,cons(x,rest)) -> cons(x,rest)
      orient(s(x),s(y)) -> pair(s(z1),s(z2)) | orient(x,y) == pair(z1,z2)
      orient(s(x),0) -> pair(0,s(x))
    )

(VAR x5 x4 x2 z2 z1 x1 x)
(CONDITION 
orient(x,x1) == pair(z1,z2), orient(x1,x2) == pair(x4,x5)
)

Optimized the infeasibility problem if possible.

(VAR x5 x4 x2 z2 z1 x1 x)
(CONDITION 
orient(x,x1) == pair(z1,z2), orient(x1,x2) == pair(x4,x5)
)

This is ultra-RL and deterministic.

This is not operationally terminating and confluent.

This is a constructor-based system.

(RTG_of_NARROWINGTREE
(START
  Gamma[orient(x,x1) == pair(z1,z2) : { e, 1 } & orient(x1,x2) == pair(x4,x5) : { e, 1 }]
)
(NONTERMINALS
  Gamma[orient(x,x1) == pair(z1,z2) : { e, 1 } & orient(x1,x2) == pair(x4,x5) : { e, 1 }]
  Gamma[orient(x216,x217) == pair2 : { e, 1 }]
)
(RULES
  Gamma[orient(x,x1) == pair(z1,z2) : { e, 1 } & orient(x1,x2) == pair(x4,x5) : { e, 1 }] -> ((Rec(Gamma[orient(x216,x217) == pair2 : { e, 1 }], { pair1 -> pair2, x1 -> x217, x -> x216 }) & { pair1 -> pair(z1,z2) }) & (Rec(Gamma[orient(x216,x217) == pair2 : { e, 1 }], { pair3 -> pair2, x2 -> x217, x1 -> x216 }) & { pair3 -> pair(x4,x5) }))
  Gamma[orient(x216,x217) == pair2 : { e, 1 }] -> { pair2 -> orient(x216,x217) }
  Gamma[orient(x216,x217) == pair2 : { e, 1 }] -> (((Rec(Gamma[orient(x216,x217) == pair2 : { e, 1 }], { pair4 -> pair2, y10 -> x217, x230 -> x216 }) & { pair4 -> pair(z21,z22) }) & { pair2 -> pair(s(z21),s(z22)) }) . { x217 -> s(y10), x216 -> s(x230) })
  Gamma[orient(x216,x217) == pair2 : { e, 1 }] -> { pair2 -> pair(0,s(x231)), x217 -> 0, x216 -> s(x231) }
)
)

Failed to prove infeasibility of the linearized conditions by means of narrowing trees.

This is not ultra-RL and deterministic.


MAYBE