MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          append(cons(y(),ys),x) -> cons(y(),append(ys,x))
          append(nil(),x) -> cons(x,nil())
          elem(node(l,x,r)) -> x
          if(false(),false(),n,m,xs,ys) -> listify(m,xs)
          if(false(),true(),n,m,xs,ys) -> listify(n,ys)
          if(true(),b,n,m,xs,ys) -> xs
          isEmpty(empty()) -> true()
          isEmpty(node(l,x,r)) -> false()
          left(empty()) -> empty()
          left(node(l,x,r)) -> l
          listify(n,xs) -> if(isEmpty(n)
                             ,isEmpty(left(n))
                             ,right(n)
                             ,node(left(left(n)),elem(left(n)),node(right(left(n)),elem(n),right(n)))
                             ,xs
                             ,append(xs,n))
          right(empty()) -> empty()
          right(node(l,x,r)) -> r
          toList(n) -> listify(n,nil())
      - Signature:
          {append/2,elem/1,if/6,isEmpty/1,left/1,listify/2,right/1,toList/1} / {cons/2,empty/0,false/0,nil/0,node/3
          ,true/0,y/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {append,elem,if,isEmpty,left,listify,right
          ,toList} and constructors {cons,empty,false,nil,node,true,y}
  + Applied Processor:
      NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE