MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          cond_insTree_t_xs_1(False(),Node(S(x9),Elem(x8),Cons(Node(x7,Elem(x6),x5),x4)),Node(x3,x2,x1),Nil()) ->
            Cons(link#2(Node(S(x9),Elem(x8),Cons(Node(x7,Elem(x6),x5),x4)),Node(x3,x2,x1)),Nil())
          cond_insTree_t_xs_1(True(),Node(S(x10),Elem(x9),Cons(Node(x8,Elem(x7),x6),x5)),Node(x4,x3,x2),x1) ->
            Cons(Node(S(x10),Elem(x9),Cons(Node(x8,Elem(x7),x6),x5)),Cons(Node(x4,x3,x2),x1))
          cond_link_t1_t2_2(False(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) ->
            Node(S(x5),Elem(x2),Cons(Node(x11,Elem(x10),x9),x1))
          cond_link_t1_t2_2(True(),Node(x11,Elem(x10),x9),Node(x8,Elem(x7),x6),x5,Elem(x4),x3,Elem(x2),x1) ->
            Node(S(x5),Elem(x4),Cons(Node(x8,Elem(x7),x6),x3))
          cond_merge_ts1_ts2_2(False()
                              ,Cons(Node(x14,x15,x16),x13)
                              ,Cons(Node(x10,x11,x12),x9)
                              ,Node(x8,x7,x6)
                              ,x5
                              ,Node(x4,x3,x2)
                              ,x1) -> cond_merge_ts1_ts2_3(lt#2(x4,x8)
                                                          ,Cons(Node(x14,x15,x16),x13)
                                                          ,Node(x8,x7,x6)
                                                          ,x5
                                                          ,Node(x4,x3,x2)
                                                          ,x1)
          cond_merge_ts1_ts2_2(True()
                              ,Cons(Node(x14,x15,x16),x13)
                              ,Cons(Node(x10,x11,x12),x9)
                              ,Node(x6,x7,x8)
                              ,x5
                              ,Node(x2,x3,x4)
                              ,x1) -> Cons(Node(x6,x7,x8),merge#2(x5,Cons(Node(x10,x11,x12),x9)))
          cond_merge_ts1_ts2_3(False(),Cons(Node(x10,x11,x12),x9),Node(x6,x7,x8),x5,Node(x2,x3,x4),x1) ->
            insTree#2(link#2(Node(x6,x7,x8),Node(x2,x3,x4)),merge#2(x5,x1))
          cond_merge_ts1_ts2_3(True(),Cons(Node(x10,x11,x12),x9),Node(x6,x7,x8),x5,Node(x2,x3,x4),x1) -> Cons(Node(x2
                                                                                                                  ,x3
                                                                                                                  ,x4)
                                                                                                             ,merge#2(Cons(Node(x10
                                                                                                                               ,x11
                                                                                                                               ,x12)
                                                                                                                          ,x9)
                                                                                                                     ,x1))
          insTree#2(x2,Nil()) -> Cons(x2,Nil())
          insTree#2(Node(S(x10),Elem(x9),Cons(Node(x8,Elem(x7),x6),x5)),Cons(Node(x4,x3,x2),x1)) ->
            cond_insTree_t_xs_1(lt#2(S(x10),x4),Node(S(x10),Elem(x9),Cons(Node(x8,Elem(x7),x6),x5)),Node(x4,x3,x2),x1)
          leq#2(0(),x20) -> True()
          leq#2(S(x24),0()) -> False()
          leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
          link#2(Node(x25,Elem(x8),x17),Node(x13,Elem(x4),x5)) -> cond_link_t1_t2_2(leq#2(x8,x4)
                                                                                   ,Node(x25,Elem(x8),x17)
                                                                                   ,Node(x13,Elem(x4),x5)
                                                                                   ,x25
                                                                                   ,Elem(x8)
                                                                                   ,x17
                                                                                   ,Elem(x4)
                                                                                   ,x5)
          lt#2(0(),0()) -> False()
          lt#2(0(),S(x20)) -> True()
          lt#2(S(x20),0()) -> False()
          lt#2(S(x4),S(x2)) -> lt#2(x4,x2)
          main(x2,x1) -> merge#2(x2,x1)
          merge#2(Cons(x4,x2),Nil()) -> Cons(x4,x2)
          merge#2(Cons(Node(x50,x66,x82),x30),Cons(Node(x24,x32,x40),x14)) -> cond_merge_ts1_ts2_2(lt#2(x50,x24)
                                                                                                  ,Cons(Node(x50
                                                                                                            ,x66
                                                                                                            ,x82)
                                                                                                       ,x30)
                                                                                                  ,Cons(Node(x24
                                                                                                            ,x32
                                                                                                            ,x40)
                                                                                                       ,x14)
                                                                                                  ,Node(x50,x66,x82)
                                                                                                  ,x30
                                                                                                  ,Node(x24,x32,x40)
                                                                                                  ,x14)
          merge#2(Nil(),x2) -> x2
      - Signature:
          {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,cond_merge_ts1_ts2_2/7,cond_merge_ts1_ts2_3/6,insTree#2/2,leq#2/2
          ,link#2/2,lt#2/2,main/2,merge#2/2} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3,S/1,True/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {cond_insTree_t_xs_1,cond_link_t1_t2_2
          ,cond_merge_ts1_ts2_2,cond_merge_ts1_ts2_3,insTree#2,leq#2,link#2,lt#2,main,merge#2} and constructors {0
          ,Cons,Elem,False,Nil,Node,S,True}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE