MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          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))
          GETNODEFROMEDGE(0(),E(z0,z1)) -> c20()
          GETNODEFROMEDGE(S(0()),E(z0,z1)) -> c19()
          GETNODEFROMEDGE(S(S(z0)),E(z1,z2)) -> c18()
          GOAL(z0,z1,z2) -> c30(REACH(z0,z1,z2))
          MEMBER(z0,Cons(z1,z2)) -> c23(MEMBER[ITE](eqEdge(z0,z1),z0,Cons(z1,z2)),EQEDGE(z0,z1))
          MEMBER(z0,Nil()) -> c24()
          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))
          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()
      - Weak TRS:
          !EQ(0(),0()) -> True()
          !EQ(0(),S(z0)) -> False()
          !EQ(S(z0),0()) -> False()
          !EQ(S(z0),S(z1)) -> !EQ(z0,z1)
          !EQ'(0(),0()) -> c3()
          !EQ'(0(),S(z0)) -> c1()
          !EQ'(S(z0),0()) -> c2()
          !EQ'(S(z0),S(z1)) -> c(!EQ'(z0,z1))
          AND(False(),False()) -> c4()
          AND(False(),True()) -> c6()
          AND(True(),False()) -> c5()
          AND(True(),True()) -> c7()
          EQEDGE[ITE](False(),z0,z1,z2,z3) -> c16()
          EQEDGE[ITE](True(),z0,z1,z2,z3) -> c17()
          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()
          VIA[ITE](False(),z0,z1,Cons(z2,z3),z4) -> c9(VIA(z0,z1,z3,z4))
          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[LET](z0,z1,Cons(z2,z3),z4,Cons(z5,z6)) -> c11()
          VIA[LET](z0,z1,Cons(z2,z3),z4,Nil()) -> c10(VIA(z0,z1,z3,z4))
          and(False(),False()) -> False()
          and(False(),True()) -> False()
          and(True(),False()) -> False()
          and(True(),True()) -> True()
          eqEdge(E(z0,z1),E(z2,z3)) -> eqEdge[Ite](and(!EQ(z0,z2),!EQ(z1,z3)),z2,z3,z0,z1)
          eqEdge[Ite](False(),z0,z1,z2,z3) -> False()
          eqEdge[Ite](True(),z0,z1,z2,z3) -> True()
          getNodeFromEdge(0(),E(z0,z1)) -> z0
          getNodeFromEdge(S(0()),E(z0,z1)) -> z0
          getNodeFromEdge(S(S(z0)),E(z1,z2)) -> z2
          goal(z0,z1,z2) -> reach(z0,z1,z2)
          member(z0,Cons(z1,z2)) -> member[Ite](eqEdge(z0,z1),z0,Cons(z1,z2))
          member(z0,Nil()) -> False()
          member[Ite](False(),z0,Cons(z1,z2)) -> member(z0,z2)
          member[Ite](True(),z0,z1) -> True()
          notEmpty(Cons(z0,z1)) -> True()
          notEmpty(Nil()) -> False()
          reach(z0,z1,z2) -> reach[Ite](member(E(z0,z1),z2),z0,z1,z2)
          reach[Ite](False(),z0,z1,z2) -> via(z0,z1,z2,z2)
          reach[Ite](True(),z0,z1,z2) -> Cons(E(z0,z1),Nil())
          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()
          via[Ite](False(),z0,z1,Cons(z2,z3),z4) -> via(z0,z1,z3,z4)
          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[Let](z0,z1,Cons(z2,z3),z4,Cons(z5,z6)) -> Cons(z2,Cons(z5,z6))
          via[Let](z0,z1,Cons(z2,z3),z4,Nil()) -> via(z0,z1,z3,z4)
      - Signature:
          {!EQ/2,!EQ'/2,AND/2,EQEDGE/2,EQEDGE[ITE]/5,GETNODEFROMEDGE/2,GOAL/3,MEMBER/2,MEMBER[ITE]/3,NOTEMPTY/1
          ,REACH/3,REACH[ITE]/4,VIA/4,VIA[ITE]/5,VIA[LET]/5,and/2,eqEdge/2,eqEdge[Ite]/5,getNodeFromEdge/2,goal/3
          ,member/2,member[Ite]/3,notEmpty/1,reach/3,reach[Ite]/4,via/4,via[Ite]/5,via[Let]/5} / {0/0,Cons/2,E/2
          ,False/0,Nil/0,S/1,True/0,c/1,c1/0,c10/1,c11/0,c12/1,c13/0,c14/1,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0
          ,c21/2,c22/0,c23/2,c24/0,c25/3,c26/3,c27/0,c28/0,c29/2,c3/0,c30/1,c4/0,c5/0,c6/0,c7/0,c8/2,c9/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {!EQ,!EQ',AND,EQEDGE,EQEDGE[ITE],GETNODEFROMEDGE,GOAL
          ,MEMBER,MEMBER[ITE],NOTEMPTY,REACH,REACH[ITE],VIA,VIA[ITE],VIA[LET],and,eqEdge,eqEdge[Ite],getNodeFromEdge
          ,goal,member,member[Ite],notEmpty,reach,reach[Ite],via,via[Ite],via[Let]} and constructors {0,Cons,E,False
          ,Nil,S,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30
          ,c4,c5,c6,c7,c8,c9}
  + Applied Processor:
      Sum {left = someStrategy, right = someStrategy}
  + Details:
      None
MAYBE