WORST_CASE(?,O(n^1))
* Step 1: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            cond_insTree_t_xs_1(False(),Node(x54,Elem(x8),x38),Node(x30,Elem(x4),x14),Nil()) ->
              Cons(cond_link_t1_t2_2(leq#2(x8,x4)
                                    ,Node(x54,Elem(x8),x38)
                                    ,Node(x30,Elem(x4),x14)
                                    ,x54
                                    ,Elem(x8)
                                    ,x38
                                    ,Elem(x4)
                                    ,x14)
                  ,Nil())
            cond_insTree_t_xs_1(True(),Node(x5,x6,x7),Node(x2,x3,x4),x1) -> Cons(Node(x5,x6,x7),Cons(Node(x2,x3,x4),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))
            leq#2(0(),x20) -> True()
            leq#2(S(x24),0()) -> False()
            leq#2(S(x4),S(x2)) -> leq#2(x4,x2)
            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(x4,Nil()) -> Cons(x4,Nil())
            main(Node(x100,x132,x164),Cons(Node(x48,x64,x80),x28)) -> cond_insTree_t_xs_1(lt#2(x100,x48)
                                                                                         ,Node(x100,x132,x164)
                                                                                         ,Node(x48,x64,x80)
                                                                                         ,x28)
        - Signature:
            {cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,leq#2/2,lt#2/2,main/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,leq#2,lt#2
            ,main} and constructors {0,Cons,Elem,False,Nil,Node,S,True}
    + Applied Processor:
        Ara {minDegree = 1, maxDegree = 2, araTimeout = 5, araRuleShifting = Nothing}
    + Details:
        Signatures used:
        ----------------
          F (TrsFun "0") :: [] -(0)-> "A"(2)
          F (TrsFun "0") :: [] -(0)-> "A"(0)
          F (TrsFun "0") :: [] -(0)-> "A"(1)
          F (TrsFun "Cons") :: ["A"(9) x "A"(0)] -(9)-> "A"(9)
          F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "Cons") :: ["A"(3) x "A"(0)] -(3)-> "A"(3)
          F (TrsFun "Elem") :: ["A"(8)] -(8)-> "A"(8)
          F (TrsFun "Elem") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "Elem") :: ["A"(1)] -(1)-> "A"(1)
          F (TrsFun "Elem") :: ["A"(3)] -(3)-> "A"(3)
          F (TrsFun "False") :: [] -(0)-> "A"(4)
          F (TrsFun "False") :: [] -(0)-> "A"(3)
          F (TrsFun "False") :: [] -(0)-> "A"(15)
          F (TrsFun "Nil") :: [] -(0)-> "A"(0)
          F (TrsFun "Nil") :: [] -(0)-> "A"(9)
          F (TrsFun "Nil") :: [] -(0)-> "A"(15)
          F (TrsFun "Node") :: ["A"(8) x "A"(8) x "A"(0)] -(0)-> "A"(8)
          F (TrsFun "Node") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "Node") :: ["A"(1) x "A"(1) x "A"(0)] -(0)-> "A"(1)
          F (TrsFun "Node") :: ["A"(9) x "A"(9) x "A"(0)] -(0)-> "A"(9)
          F (TrsFun "Node") :: ["A"(6) x "A"(6) x "A"(0)] -(0)-> "A"(6)
          F (TrsFun "S") :: ["A"(2)] -(2)-> "A"(2)
          F (TrsFun "S") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "S") :: ["A"(1)] -(1)-> "A"(1)
          F (TrsFun "True") :: [] -(0)-> "A"(4)
          F (TrsFun "True") :: [] -(0)-> "A"(3)
          F (TrsFun "True") :: [] -(0)-> "A"(15)
          F (TrsFun "cond_insTree_t_xs_1") :: ["A"(4) x "A"(8) x "A"(8) x "A"(0)] -(7)-> "A"(0)
          F (TrsFun "cond_link_t1_t2_2") :: ["A"(3) x "A"(0) x "A"(1) x "A"(0) x "A"(0) x "A"(0) x "A"(3) x "A"(0)] -(0)-> "A"(0)
          F (TrsFun "leq#2") :: ["A"(2) x "A"(0)] -(9)-> "A"(14)
          F (TrsFun "lt#2") :: ["A"(0) x "A"(1)] -(2)-> "A"(9)
          F (TrsFun "main") :: ["A"(9) x "A"(9)] -(14)-> "A"(0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(1)
          "F (TrsFun \"Cons\")_A" :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          "F (TrsFun \"Elem\")_A" :: ["A"(1)] -(1)-> "A"(1)
          "F (TrsFun \"False\")_A" :: [] -(0)-> "A"(1)
          "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1)
          "F (TrsFun \"Node\")_A" :: ["A"(1) x "A"(1) x "A"(0)] -(0)-> "A"(1)
          "F (TrsFun \"S\")_A" :: ["A"(1)] -(1)-> "A"(1)
          "F (TrsFun \"True\")_A" :: [] -(0)-> "A"(1)
        

WORST_CASE(?,O(n^1))