MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          atom(Cons(x,xs)) -> xs
          atom(Nil()) -> Nil()
          eqAlph(Div(),Div()) -> True()
          eqAlph(Div(),LPar()) -> False()
          eqAlph(Div(),Minus()) -> False()
          eqAlph(Div(),Mul()) -> False()
          eqAlph(Div(),Plus()) -> False()
          eqAlph(Div(),RPar()) -> False()
          eqAlph(Div(),Val(int2)) -> False()
          eqAlph(LPar(),Div()) -> False()
          eqAlph(LPar(),LPar()) -> True()
          eqAlph(LPar(),Minus()) -> False()
          eqAlph(LPar(),Mul()) -> False()
          eqAlph(LPar(),Plus()) -> False()
          eqAlph(LPar(),RPar()) -> False()
          eqAlph(LPar(),Val(int2)) -> False()
          eqAlph(Minus(),Div()) -> False()
          eqAlph(Minus(),LPar()) -> False()
          eqAlph(Minus(),Minus()) -> True()
          eqAlph(Minus(),Mul()) -> False()
          eqAlph(Minus(),Plus()) -> False()
          eqAlph(Minus(),RPar()) -> False()
          eqAlph(Minus(),Val(int2)) -> False()
          eqAlph(Mul(),Div()) -> False()
          eqAlph(Mul(),LPar()) -> False()
          eqAlph(Mul(),Minus()) -> False()
          eqAlph(Mul(),Mul()) -> True()
          eqAlph(Mul(),Plus()) -> False()
          eqAlph(Mul(),RPar()) -> False()
          eqAlph(Mul(),Val(int2)) -> False()
          eqAlph(Plus(),Div()) -> False()
          eqAlph(Plus(),LPar()) -> False()
          eqAlph(Plus(),Minus()) -> False()
          eqAlph(Plus(),Mul()) -> False()
          eqAlph(Plus(),Plus()) -> True()
          eqAlph(Plus(),RPar()) -> False()
          eqAlph(Plus(),Val(int2)) -> False()
          eqAlph(RPar(),Div()) -> False()
          eqAlph(RPar(),LPar()) -> False()
          eqAlph(RPar(),Minus()) -> False()
          eqAlph(RPar(),Mul()) -> False()
          eqAlph(RPar(),Plus()) -> False()
          eqAlph(RPar(),RPar()) -> True()
          eqAlph(RPar(),Val(int2)) -> False()
          eqAlph(Val(int),Div()) -> False()
          eqAlph(Val(int),LPar()) -> False()
          eqAlph(Val(int),Minus()) -> False()
          eqAlph(Val(int),Mul()) -> False()
          eqAlph(Val(int),Plus()) -> False()
          eqAlph(Val(int),RPar()) -> False()
          eqAlph(Val(int),Val(int2)) -> !EQ(int2,int)
          expr(xs) -> expr[Let](xs,term(xs))
          factor(Cons(Div(),xs)) -> xs
          factor(Cons(LPar(),xs)) -> factor[Ite][True][Let](Cons(LPar(),xs),expr(Cons(LPar(),xs)))
          factor(Cons(Minus(),xs)) -> xs
          factor(Cons(Mul(),xs)) -> xs
          factor(Cons(Plus(),xs)) -> xs
          factor(Cons(RPar(),xs)) -> xs
          factor(Cons(Val(int),xs)) -> xs
          head(Cons(x,xs)) -> x
          member(x,Nil()) -> False()
          member(x',Cons(x,xs)) -> member[Ite][True][Ite](eqAlph(x,x'),x',Cons(x,xs))
          notEmpty(Cons(x,xs)) -> True()
          notEmpty(Nil()) -> False()
          parsexp(xs) -> expr(xs)
          term(xs) -> term[Let](xs,factor(xs))
      - Weak TRS:
          !EQ(0(),0()) -> True()
          !EQ(0(),S(y)) -> False()
          !EQ(S(x),0()) -> False()
          !EQ(S(x),S(y)) -> !EQ(x,y)
          and(False(),False()) -> False()
          and(False(),True()) -> False()
          and(True(),False()) -> False()
          and(True(),True()) -> True()
          expr[Let](xs,Nil()) -> Nil()
          expr[Let](xs',Cons(x,xs)) -> expr[Let][Ite][False][Ite](member(x,Cons(Plus(),Cons(Minus(),Nil())))
                                                                 ,xs'
                                                                 ,Cons(x,xs))
          factor[Ite][True][Let](xs,Nil()) -> factor[Ite][True][Let][Ite](and(False(),eqAlph(head(Nil()),RPar()))
                                                                         ,xs
                                                                         ,Nil())
          factor[Ite][True][Let](xs',Cons(Div(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Div(),xs))
          factor[Ite][True][Let](xs',Cons(LPar(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(LPar(),xs))
          factor[Ite][True][Let](xs',Cons(Minus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Minus(),xs))
          factor[Ite][True][Let](xs',Cons(Mul(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Mul(),xs))
          factor[Ite][True][Let](xs',Cons(Plus(),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Plus(),xs))
          factor[Ite][True][Let](xs',Cons(RPar(),xs)) -> factor[Ite][True][Let][Ite](True(),xs',Cons(RPar(),xs))
          factor[Ite][True][Let](xs',Cons(Val(int),xs)) -> factor[Ite][True][Let][Ite](False(),xs',Cons(Val(int),xs))
          member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs)
          member[Ite][True][Ite](True(),x,xs) -> True()
          term[Let](xs,Nil()) -> Nil()
          term[Let](xs',Cons(x,xs)) -> term[Let][Ite][False][Ite](member(x,Cons(Mul(),Cons(Div(),Nil())))
                                                                 ,xs'
                                                                 ,Cons(x,xs))
      - Signature:
          {!EQ/2,and/2,atom/1,eqAlph/2,expr/1,expr[Let]/2,factor/1,factor[Ite][True][Let]/2,head/1,member/2
          ,member[Ite][True][Ite]/3,notEmpty/1,parsexp/1,term/1,term[Let]/2} / {0/0,Cons/2,Div/0,False/0,LPar/0
          ,Minus/0,Mul/0,Nil/0,Plus/0,RPar/0,S/1,True/0,Val/1,expr[Let][Ite][False][Ite]/3
          ,factor[Ite][True][Let][Ite]/3,term[Let][Ite][False][Ite]/3}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {!EQ,and,atom,eqAlph,expr,expr[Let],factor
          ,factor[Ite][True][Let],head,member,member[Ite][True][Ite],notEmpty,parsexp,term
          ,term[Let]} and constructors {0,Cons,Div,False,LPar,Minus,Mul,Nil,Plus,RPar,S,True,Val
          ,expr[Let][Ite][False][Ite],factor[Ite][True][Let][Ite],term[Let][Ite][False][Ite]}
  + Applied Processor:
      MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = NoUArgs, miURules = NoURules, miSelector = Nothing}
  + Details:
      Incompatible
MAYBE