MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          flatten(leaf()) -> nil()
          flatten(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
          flattensort(t) -> insertionsort(flatten(t))
          if'insert(false(),x,y,ys) -> cons(y,insert(x,ys))
          if'insert(true(),x,y,ys) -> cons(x,cons(y,ys))
          insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys)
          insert(x,nil()) -> cons(x,nil())
          insertionsort(cons(x,xs)) -> insert(x,insertionsort(xs))
          insertionsort(nil()) -> nil()
      - Weak TRS:
          append(cons(x,xs),l2) -> cons(x,append(xs,l2))
          append(nil(),l2) -> l2
          leq(0(),y) -> true()
          leq(s(x),0()) -> false()
          leq(s(x),s(y)) -> leq(x,y)
      - Signature:
          {append/2,flatten/1,flattensort/1,if'insert/4,insert/2,insertionsort/1,leq/2} / {0/0,cons/2,false/0,leaf/0
          ,nil/0,node/3,s/1,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {append,flatten,flattensort,if'insert,insert,insertionsort
          ,leq} and constructors {0,cons,false,leaf,nil,node,s,true}
  + Applied Processor:
      Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT}
  + Details:
      The input can not be schown compatible.
MAYBE