MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          and(false(),y) -> false()
          and(true(),y) -> y
          eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
          eq(apply(t,s),lambda(x,t)) -> false()
          eq(apply(t,s),var(l)) -> false()
          eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
          eq(cons(t,l),nil()) -> false()
          eq(lambda(x,t),apply(t,s)) -> false()
          eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
          eq(lambda(x,t),var(l)) -> false()
          eq(nil(),cons(t,l)) -> false()
          eq(nil(),nil()) -> true()
          eq(var(l),apply(t,s)) -> false()
          eq(var(l),lambda(x,t)) -> false()
          eq(var(l),var(l')) -> eq(l,l')
          if(false(),var(k),var(l')) -> var(l')
          if(true(),var(k),var(l')) -> var(k)
          ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
          ren(x,y,lambda(z,t)) -> lambda(var(cons(x,cons(y,cons(lambda(z,t),nil()))))
                                        ,ren(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)))
          ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
      - Signature:
          {and/2,eq/2,if/3,ren/3} / {apply/2,cons/2,false/0,lambda/2,nil/0,true/0,var/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {and,eq,if,ren} and constructors {apply,cons,false,lambda
          ,nil,true,var}
  + Applied Processor:
      NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE