KILLED
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).

(0) CpxRelTRS


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
   GETNODEFROMEDGE(S(0), E(z0, z1)) -> c19
   GETNODEFROMEDGE(0, E(z0, z1)) -> c20
   VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
   VIA(z0, z1, Nil, z2) -> c22
   MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
   MEMBER(z0, Nil) -> c24
   EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
   EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
   NOTEMPTY(Cons(z0, z1)) -> c27
   NOTEMPTY(Nil) -> c28
   REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
   GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))

The (relative) TRS S consists of the following rules:

   !EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c1
   !EQ'(S(z0), 0) -> c2
   !EQ'(0, 0) -> c3
   AND(False, False) -> c4
   AND(True, False) -> c5
   AND(False, True) -> c6
   AND(True, True) -> c7
   VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
   VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
   MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
   MEMBER[ITE](True, z0, z1) -> c13
   REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
   REACH[ITE](True, z0, z1, z2) -> c15
   EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
   EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
   via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
   member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
   member[Ite](True, z0, z1) -> True
   reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
   reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
   eqEdge[Ite](False, z0, z1, z2, z3) -> False
   eqEdge[Ite](True, z0, z1, z2, z3) -> True
   getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
   getNodeFromEdge(S(0), E(z0, z1)) -> z0
   getNodeFromEdge(0, E(z0, z1)) -> z0
   via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
   via(z0, z1, Nil, z2) -> Nil
   member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
   member(z0, Nil) -> False
   eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
   goal(z0, z1, z2) -> reach(z0, z1, z2)

Rewrite Strategy: INNERMOST