MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          cadr(cons(x,cons(y,l))) -> y
          car(cons(x,l)) -> x
          cddr(cons(x,cons(y,l))) -> l
          cddr(cons(x,nil())) -> nil()
          cddr(nil()) -> nil()
          if(false(),b,l) -> if2(b,l)
          if(true(),b,l) -> s(0())
          if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))
          if2(true(),l) -> car(l)
          ifplus(false(),x,y) -> s(plus(p(x),y))
          ifplus(true(),x,y) -> y
          iftimes(false(),x,y) -> plus(y,times(p(x),y))
          iftimes(true(),x,y) -> 0()
          isZero(0()) -> true()
          isZero(s(x)) -> false()
          p(0()) -> 0()
          p(s(x)) -> x
          plus(x,y) -> ifplus(isZero(x),x,y)
          prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
          shorter(cons(x,l),0()) -> false()
          shorter(cons(x,l),s(y)) -> shorter(l,y)
          shorter(nil(),y) -> true()
          times(x,y) -> iftimes(isZero(x),x,y)
      - Signature:
          {cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2} / {0/0
          ,cons/2,false/0,nil/0,s/1,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {cadr,car,cddr,if,if2,ifplus,iftimes,isZero,p,plus,prod
          ,shorter,times} and constructors {0,cons,false,nil,s,true}
  + Applied Processor:
      MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = NoUArgs, miURules = NoURules, miSelector = Nothing}
  + Details:
      Incompatible
MAYBE