MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          apply(op,v1,v2) -> apply[Ite](eqExp(v1,v2),op,v1,v2)
          checkConstrExp(Bsf(op1,b11,b12),Bsf(op2,b21,b22)) -> True()
          checkConstrExp(Bsf(op1,b11,b12),Eq(eq21,eq22)) -> False()
          checkConstrExp(Bsf(op1,b11,b12),Error(e21,e22)) -> False()
          checkConstrExp(Bsf(op1,b11,b12),F()) -> False()
          checkConstrExp(Bsf(op1,b11,b12),Fun(fn2,fe2)) -> False()
          checkConstrExp(Bsf(op1,b11,b12),ITE(i2,t2,e2)) -> False()
          checkConstrExp(Bsf(op1,b11,b12),T()) -> False()
          checkConstrExp(Bsf(op1,b11,b12),Var(v2)) -> False()
          checkConstrExp(Eq(eq11,eq12),Bsf(op2,b21,b22)) -> False()
          checkConstrExp(Eq(eq11,eq12),Eq(eq21,eq22)) -> True()
          checkConstrExp(Eq(eq11,eq12),Error(e21,e22)) -> False()
          checkConstrExp(Eq(eq11,eq12),F()) -> False()
          checkConstrExp(Eq(eq11,eq12),Fun(fn2,fe2)) -> False()
          checkConstrExp(Eq(eq11,eq12),ITE(i2,t2,e2)) -> False()
          checkConstrExp(Eq(eq11,eq12),T()) -> False()
          checkConstrExp(Eq(eq11,eq12),Var(v2)) -> False()
          checkConstrExp(Error(e11,e12),Bsf(op2,b21,b22)) -> False()
          checkConstrExp(Error(e11,e12),Eq(eq21,eq22)) -> False()
          checkConstrExp(Error(e11,e12),Error(e21,e22)) -> True()
          checkConstrExp(Error(e11,e12),F()) -> False()
          checkConstrExp(Error(e11,e12),Fun(fn2,fe2)) -> False()
          checkConstrExp(Error(e11,e12),ITE(i2,t2,e2)) -> False()
          checkConstrExp(Error(e11,e12),T()) -> False()
          checkConstrExp(Error(e11,e12),Var(v2)) -> False()
          checkConstrExp(F(),Bsf(op2,b21,b22)) -> False()
          checkConstrExp(F(),Eq(eq21,eq22)) -> False()
          checkConstrExp(F(),Error(e21,e22)) -> False()
          checkConstrExp(F(),F()) -> True()
          checkConstrExp(F(),Fun(fn2,fe2)) -> False()
          checkConstrExp(F(),ITE(i2,t2,e2)) -> False()
          checkConstrExp(F(),T()) -> False()
          checkConstrExp(F(),Var(v2)) -> False()
          checkConstrExp(Fun(fn1,fe1),Bsf(op2,b21,b22)) -> False()
          checkConstrExp(Fun(fn1,fe1),Eq(eq21,eq22)) -> False()
          checkConstrExp(Fun(fn1,fe1),Error(e21,e22)) -> False()
          checkConstrExp(Fun(fn1,fe1),F()) -> False()
          checkConstrExp(Fun(fn1,fe1),Fun(fn2,fe2)) -> True()
          checkConstrExp(Fun(fn1,fe1),ITE(i2,t2,e2)) -> False()
          checkConstrExp(Fun(fn1,fe1),T()) -> False()
          checkConstrExp(Fun(fn1,fe1),Var(v2)) -> False()
          checkConstrExp(ITE(i1,t1,e1),Bsf(op2,b21,b22)) -> False()
          checkConstrExp(ITE(i1,t1,e1),Eq(eq21,eq22)) -> False()
          checkConstrExp(ITE(i1,t1,e1),Error(e21,e22)) -> False()
          checkConstrExp(ITE(i1,t1,e1),F()) -> False()
          checkConstrExp(ITE(i1,t1,e1),Fun(fn2,fe2)) -> False()
          checkConstrExp(ITE(i1,t1,e1),ITE(i2,t2,e2)) -> True()
          checkConstrExp(ITE(i1,t1,e1),T()) -> False()
          checkConstrExp(ITE(i1,t1,e1),Var(v2)) -> False()
          checkConstrExp(T(),Bsf(op2,b21,b22)) -> False()
          checkConstrExp(T(),Eq(eq21,eq22)) -> False()
          checkConstrExp(T(),Error(e21,e22)) -> False()
          checkConstrExp(T(),F()) -> False()
          checkConstrExp(T(),Fun(fn2,fe2)) -> False()
          checkConstrExp(T(),ITE(i2,t2,e2)) -> False()
          checkConstrExp(T(),T()) -> True()
          checkConstrExp(T(),Var(v2)) -> False()
          checkConstrExp(Var(v1),Bsf(op2,b21,b22)) -> False()
          checkConstrExp(Var(v1),Eq(eq21,eq22)) -> False()
          checkConstrExp(Var(v1),Error(e21,e22)) -> False()
          checkConstrExp(Var(v1),F()) -> False()
          checkConstrExp(Var(v1),Fun(fn2,fe2)) -> False()
          checkConstrExp(Var(v1),ITE(i2,t2,e2)) -> False()
          checkConstrExp(Var(v1),T()) -> False()
          checkConstrExp(Var(v1),Var(v2)) -> True()
          eeval(Bsf(op,t1,t2),ns,vs,p) -> eeval[Let](Bsf(op,t1,t2),ns,vs,p,eeval(t1,ns,vs,p))
          eeval(Eq(f,s),ns,vs,p) -> eeval[True][Ite](eqExp(eeval(f,ns,vs,p),eeval(s,ns,vs,p)),Eq(f,s),ns,vs,p)
          eeval(Error(e11,e12),ns,vs,p) -> eeval[False][Ite](False(),Error(e11,e12),ns,vs,p)
          eeval(F(),ns,vs,p) -> F()
          eeval(Fun(n,e),ns,vs,p) -> eeval[False][Let](Fun(n,e),ns,vs,p,lookbody(n,p))
          eeval(ITE(i,t,e),ns,vs,p) -> eeval[Ite](checkConstrExp(eeval(i,ns,vs,p),T()),ITE(i,t,e),ns,vs,p)
          eeval(T(),ns,vs,p) -> T()
          eeval(Var(int),ns,vs,p) -> lookvar(int,ns,vs)
          eqExp(Bsf(o1,b11,b12),Bsf(o2,b21,b22)) -> and(True(),and(eqExp(b11,b21),eqExp(b12,b22)))
          eqExp(Bsf(op1,b11,b12),Eq(eq21,eq22)) -> False()
          eqExp(Bsf(op1,b11,b12),Error(e21,e22)) -> False()
          eqExp(Bsf(op1,b11,b12),F()) -> False()
          eqExp(Bsf(op1,b11,b12),Fun(fn2,fe2)) -> False()
          eqExp(Bsf(op1,b11,b12),ITE(i2,t2,e2)) -> False()
          eqExp(Bsf(op1,b11,b12),T()) -> False()
          eqExp(Bsf(op1,b11,b12),Var(v2)) -> False()
          eqExp(Eq(eq11,eq12),Bsf(op2,b21,b22)) -> False()
          eqExp(Eq(eq11,eq12),Eq(eq21,eq22)) -> and(eqExp(eq11,eq21),eqExp(eq12,eq22))
          eqExp(Eq(eq11,eq12),Error(e21,e22)) -> False()
          eqExp(Eq(eq11,eq12),F()) -> False()
          eqExp(Eq(eq11,eq12),Fun(fn2,fe2)) -> False()
          eqExp(Eq(eq11,eq12),ITE(i2,t2,e2)) -> False()
          eqExp(Eq(eq11,eq12),T()) -> False()
          eqExp(Eq(eq11,eq12),Var(v2)) -> False()
          eqExp(Error(e11,e12),Bsf(op2,b21,b22)) -> False()
          eqExp(Error(e11,e12),Eq(eq21,eq22)) -> False()
          eqExp(Error(e11,e12),Error(e21,e22)) -> and(eqExp(e11,e21),eqExp(e12,e22))
          eqExp(Error(e11,e12),F()) -> False()
          eqExp(Error(e11,e12),Fun(fn2,fe2)) -> False()
          eqExp(Error(e11,e12),ITE(i2,t2,e2)) -> False()
          eqExp(Error(e11,e12),T()) -> False()
          eqExp(Error(e11,e12),Var(v2)) -> False()
          eqExp(F(),Bsf(op2,b21,b22)) -> False()
          eqExp(F(),Eq(eq21,eq22)) -> False()
          eqExp(F(),Error(e21,e22)) -> False()
          eqExp(F(),F()) -> True()
          eqExp(F(),Fun(fn2,fe2)) -> False()
          eqExp(F(),ITE(i2,t2,e2)) -> False()
          eqExp(F(),T()) -> False()
          eqExp(F(),Var(v2)) -> False()
          eqExp(Fun(fn1,fe1),Bsf(op2,b21,b22)) -> False()
          eqExp(Fun(fn1,fe1),Eq(eq21,eq22)) -> False()
          eqExp(Fun(fn1,fe1),Error(e21,e22)) -> False()
          eqExp(Fun(fn1,fe1),F()) -> False()
          eqExp(Fun(fn1,fe1),Fun(fn2,fe2)) -> and(!EQ(fn1,fn2),eqExp(fe1,fe2))
          eqExp(Fun(fn1,fe1),ITE(i2,t2,e2)) -> False()
          eqExp(Fun(fn1,fe1),T()) -> False()
          eqExp(Fun(fn1,fe1),Var(v2)) -> False()
          eqExp(ITE(i1,t1,e1),Bsf(op2,b21,b22)) -> False()
          eqExp(ITE(i1,t1,e1),Eq(eq21,eq22)) -> False()
          eqExp(ITE(i1,t1,e1),Error(e21,e22)) -> False()
          eqExp(ITE(i1,t1,e1),F()) -> False()
          eqExp(ITE(i1,t1,e1),Fun(fn2,fe2)) -> False()
          eqExp(ITE(i1,t1,e1),ITE(i2,t2,e2)) -> and(eqExp(i1,i2),and(eqExp(t1,t2),eqExp(e1,e2)))
          eqExp(ITE(i1,t1,e1),T()) -> False()
          eqExp(ITE(i1,t1,e1),Var(v2)) -> False()
          eqExp(T(),Bsf(op2,b21,b22)) -> False()
          eqExp(T(),Eq(eq21,eq22)) -> False()
          eqExp(T(),Error(e21,e22)) -> False()
          eqExp(T(),F()) -> False()
          eqExp(T(),Fun(fn2,fe2)) -> False()
          eqExp(T(),ITE(i2,t2,e2)) -> False()
          eqExp(T(),T()) -> True()
          eqExp(T(),Var(v2)) -> False()
          eqExp(Var(v1),Bsf(op2,b21,b22)) -> False()
          eqExp(Var(v1),Eq(eq21,eq22)) -> False()
          eqExp(Var(v1),Error(e21,e22)) -> False()
          eqExp(Var(v1),F()) -> False()
          eqExp(Var(v1),Fun(fn2,fe2)) -> False()
          eqExp(Var(v1),ITE(i2,t2,e2)) -> False()
          eqExp(Var(v1),T()) -> False()
          eqExp(Var(v1),Var(v2)) -> !EQ(v1,v2)
          eqOps(o1,o2) -> True()
          getBsfFirstTerm(Bsf(op,t1,t2)) -> t1
          getBsfOp(Bsf(op,t1,t2)) -> op
          getBsfSecondTerm(Bsf(op,t1,t2)) -> t2
          getConst(Cst(int)) -> int
          getEqFirst(Eq(f,s)) -> f
          getEqSecond(Eq(f,s)) -> s
          getFuncExp(Fun(n,e)) -> e
          getFuncName(Fun(n,e)) -> n
          getIfFalse(ITE(i,t,e)) -> e
          getIfGuard(ITE(i,t,e)) -> i
          getIfTrue(ITE(i,t,e)) -> t
          getVar(Var(int)) -> int
          lookbody(f,Cons(Fun(n,e),xs)) -> lookbody[Ite](!EQ(f,n),f,Cons(Fun(n,e),xs))
          lookname(f,Cons(Fun(n,e),xs)) -> lookname[Ite](!EQ(f,n),f,Cons(Fun(n,e),xs))
          lookvar(x',Cons(x,xs),vs) -> lookvar[Ite](!EQ(x',x),x',Cons(x,xs),vs)
          run(Cons(Fun(f0,e),xs),input) -> run[Let][Let](Cons(Fun(f0,e),xs),input,f0,lookbody(f0,Cons(Fun(f0,e),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()
          apply[Ite](False(),op,v1,v2) -> F()
          apply[Ite](True(),op,v1,v2) -> T()
          eeval[False][Ite](False(),Fun(n,e),ns,vs,p) -> eeval[False][Let](Fun(n,e),ns,vs,p,lookbody(n,p))
          eeval[False][Ite](True(),Eq(f,s),ns,vs,p) -> eeval[True][Ite](eqExp(eeval(f,ns,vs,p),eeval(s,ns,vs,p))
                                                                       ,Eq(f,s)
                                                                       ,ns
                                                                       ,vs
                                                                       ,p)
          eeval[False][Let](Fun(n,e),ns,vs,p,ef) -> eeval[False][Let][Let](Fun(n,e),ns,vs,p,ef,lookname(n,p))
          eeval[False][Let][Let](Fun(n,e),ns,vs,p,ef,nf) -> eeval[Let][Let][Let](Fun(n,e)
                                                                                ,ns
                                                                                ,vs
                                                                                ,p
                                                                                ,ef
                                                                                ,nf
                                                                                ,eeval(e,ns,vs,p))
          eeval[Ite](False(),ITE(i,t,e),ns,vs,p) -> eeval(e,ns,vs,p)
          eeval[Ite](True(),ITE(i,t,e),ns,vs,p) -> eeval(t,ns,vs,p)
          eeval[Let](Bsf(op,t1,t2),ns,vs,p,v1) -> eeval[Let][Let](Bsf(op,t1,t2),ns,vs,p,v1,eeval(t2,ns,vs,p))
          eeval[Let][Let](Bsf(op,t1,t2),ns,vs,p,v1,v2) -> apply(op,v1,v2)
          eeval[Let][Let][Let](e,ns,vs,p,ef,nf,v) -> eeval(ef,Cons(nf,Nil()),Cons(v,Nil()),p)
          eeval[True][Ite](False(),e,ns,vs,p) -> F()
          eeval[True][Ite](True(),e,ns,vs,p) -> T()
          lookbody[Ite](False(),f,Cons(x,xs)) -> lookbody(f,xs)
          lookbody[Ite](True(),f,Cons(Fun(n,e),xs)) -> e
          lookname[Ite](False(),f,Cons(x,xs)) -> lookname(f,xs)
          lookname[Ite](True(),f,Cons(Fun(n,e),xs)) -> n
          lookvar[Ite](False(),x',Cons(x'',xs'),Cons(x,xs)) -> lookvar(x',xs',xs)
          lookvar[Ite](True(),x',ns,Cons(x,xs)) -> x
          run[Let](p,input,f0,ef,nf) -> eeval(ef,Cons(nf,Nil()),Cons(input,Nil()),p)
          run[Let][Let](p,input,f0,ef) -> run[Let](p,input,f0,ef,lookname(f0,p))
      - Signature:
          {!EQ/2,and/2,apply/3,apply[Ite]/4,checkConstrExp/2,eeval/4,eeval[False][Ite]/5,eeval[False][Let]/5
          ,eeval[False][Let][Let]/6,eeval[Ite]/5,eeval[Let]/5,eeval[Let][Let]/6,eeval[Let][Let][Let]/7
          ,eeval[True][Ite]/5,eqExp/2,eqOps/2,getBsfFirstTerm/1,getBsfOp/1,getBsfSecondTerm/1,getConst/1,getEqFirst/1
          ,getEqSecond/1,getFuncExp/1,getFuncName/1,getIfFalse/1,getIfGuard/1,getIfTrue/1,getVar/1,lookbody/2
          ,lookbody[Ite]/3,lookname/2,lookname[Ite]/3,lookvar/3,lookvar[Ite]/4,run/2,run[Let]/5
          ,run[Let][Let]/4} / {0/0,Bsf/3,Cons/2,Cst/1,Eq/2,Error/2,F/0,False/0,Fun/2,ITE/3,Nil/0,S/1,T/0,True/0,Var/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {!EQ,and,apply,apply[Ite],checkConstrExp,eeval
          ,eeval[False][Ite],eeval[False][Let],eeval[False][Let][Let],eeval[Ite],eeval[Let],eeval[Let][Let]
          ,eeval[Let][Let][Let],eeval[True][Ite],eqExp,eqOps,getBsfFirstTerm,getBsfOp,getBsfSecondTerm,getConst
          ,getEqFirst,getEqSecond,getFuncExp,getFuncName,getIfFalse,getIfGuard,getIfTrue,getVar,lookbody,lookbody[Ite]
          ,lookname,lookname[Ite],lookvar,lookvar[Ite],run,run[Let],run[Let][Let]} and constructors {0,Bsf,Cons,Cst,Eq
          ,Error,F,False,Fun,ITE,Nil,S,T,True,Var}
  + Applied Processor:
      NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE