MAYBE

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR z2 z1 rest y x)
    (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)
    (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 z2 z1 y x)
(CONDITION 
orient(x,y) == pair(z1,z2)
)

Optimized the infeasibility problem if possible.

(VAR z2 z1 y x)
(CONDITION 
orient(x,y) == pair(z1,z2)
)

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,y) == pair(z1,z2) : { e, 1 }]
)
(NONTERMINALS
  Gamma[orient(x,y) == pair(z1,z2) : { e, 1 }]
  Gamma[orient(x216,y5) == pair2 : { e, 1 }]
)
(RULES
  Gamma[orient(x,y) == pair(z1,z2) : { e, 1 }] -> (Rec(Gamma[orient(x216,y5) == pair2 : { e, 1 }], { pair1 -> pair2, y -> y5, x -> x216 }) & { pair1 -> pair(z1,z2) })
  Gamma[orient(x216,y5) == pair2 : { e, 1 }] -> { pair2 -> orient(x216,y5) }
  Gamma[orient(x216,y5) == pair2 : { e, 1 }] -> (((Rec(Gamma[orient(x216,y5) == pair2 : { e, 1 }], { pair3 -> pair2, y7 -> y5, x220 -> x216 }) & { pair3 -> pair(z13,z14) }) & { pair2 -> pair(s(z13),s(z14)) }) . { y5 -> s(y7), x216 -> s(x220) })
  Gamma[orient(x216,y5) == pair2 : { e, 1 }] -> { pair2 -> pair(0,s(x221)), y5 -> 0, x216 -> s(x221) }
)
)

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

This is not ultra-RL and deterministic.


MAYBE