WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            flattensort(t) -> insertionsort(flatten(t))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1} / {'0/0,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0
            ,dd/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt,'compare,'less,append,append'1,flatten,flatten'1
            ,flattensort,insert,insert'1,insert'2,insertionsort,insertionsort'1} and constructors {'0,'EQ,'GT,'LT,'false
            ,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          'cklt#('EQ()) -> c_1()
          'cklt#('GT()) -> c_2()
          'cklt#('LT()) -> c_3()
          'compare#('0(),'0()) -> c_4()
          'compare#('0(),'neg(y)) -> c_5()
          'compare#('0(),'pos(y)) -> c_6()
          'compare#('0(),'s(y)) -> c_7()
          'compare#('neg(x),'0()) -> c_8()
          'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
          'compare#('neg(x),'pos(y)) -> c_10()
          'compare#('pos(x),'0()) -> c_11()
          'compare#('pos(x),'neg(y)) -> c_12()
          'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
          'compare#('s(x),'0()) -> c_14()
          'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
          'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y))
          append#(l1,l2) -> c_17(append'1#(l1,l2))
          append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
          append'1#(nil(),l2) -> c_19()
          flatten#(t) -> c_20(flatten'1#(t))
          flatten'1#(leaf()) -> c_21()
          flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                           ,append#(flatten(t1),flatten(t2))
                                           ,flatten#(t1)
                                           ,flatten#(t2))
          flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
          insert#(x,l) -> c_24(insert'1#(l,x))
          insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
          insert'1#(nil(),x) -> c_26()
          insert'2#('false(),x,y,ys) -> c_27()
          insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
          insertionsort#(l) -> c_29(insertionsort'1#(l))
          insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
          insertionsort'1#(nil()) -> c_31()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            'cklt#('EQ()) -> c_1()
            'cklt#('GT()) -> c_2()
            'cklt#('LT()) -> c_3()
            'compare#('0(),'0()) -> c_4()
            'compare#('0(),'neg(y)) -> c_5()
            'compare#('0(),'pos(y)) -> c_6()
            'compare#('0(),'s(y)) -> c_7()
            'compare#('neg(x),'0()) -> c_8()
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('neg(x),'pos(y)) -> c_10()
            'compare#('pos(x),'0()) -> c_11()
            'compare#('pos(x),'neg(y)) -> c_12()
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'0()) -> c_14()
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y))
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            append'1#(nil(),l2) -> c_19()
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(leaf()) -> c_21()
            flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                             ,append#(flatten(t1),flatten(t2))
                                             ,flatten#(t1)
                                             ,flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'1#(nil(),x) -> c_26()
            insert'2#('false(),x,y,ys) -> c_27()
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
            insertionsort'1#(nil()) -> c_31()
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            flattensort(t) -> insertionsort(flatten(t))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,3,4,5,6,7,8,10,11,12,14,19,21,26,27,31}
        by application of
          Pre({1,2,3,4,5,6,7,8,10,11,12,14,19,21,26,27,31}) = {9,13,15,16,17,20,24,25,29}.
        Here rules are labelled as follows:
          1: 'cklt#('EQ()) -> c_1()
          2: 'cklt#('GT()) -> c_2()
          3: 'cklt#('LT()) -> c_3()
          4: 'compare#('0(),'0()) -> c_4()
          5: 'compare#('0(),'neg(y)) -> c_5()
          6: 'compare#('0(),'pos(y)) -> c_6()
          7: 'compare#('0(),'s(y)) -> c_7()
          8: 'compare#('neg(x),'0()) -> c_8()
          9: 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
          10: 'compare#('neg(x),'pos(y)) -> c_10()
          11: 'compare#('pos(x),'0()) -> c_11()
          12: 'compare#('pos(x),'neg(y)) -> c_12()
          13: 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
          14: 'compare#('s(x),'0()) -> c_14()
          15: 'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
          16: 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y))
          17: append#(l1,l2) -> c_17(append'1#(l1,l2))
          18: append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
          19: append'1#(nil(),l2) -> c_19()
          20: flatten#(t) -> c_20(flatten'1#(t))
          21: flatten'1#(leaf()) -> c_21()
          22: flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                               ,append#(flatten(t1),flatten(t2))
                                               ,flatten#(t1)
                                               ,flatten#(t2))
          23: flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
          24: insert#(x,l) -> c_24(insert'1#(l,x))
          25: insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
          26: insert'1#(nil(),x) -> c_26()
          27: insert'2#('false(),x,y,ys) -> c_27()
          28: insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
          29: insertionsort#(l) -> c_29(insertionsort'1#(l))
          30: insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
          31: insertionsort'1#(nil()) -> c_31()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y))
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                             ,append#(flatten(t1),flatten(t2))
                                             ,flatten#(t1)
                                             ,flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
        - Weak DPs:
            'cklt#('EQ()) -> c_1()
            'cklt#('GT()) -> c_2()
            'cklt#('LT()) -> c_3()
            'compare#('0(),'0()) -> c_4()
            'compare#('0(),'neg(y)) -> c_5()
            'compare#('0(),'pos(y)) -> c_6()
            'compare#('0(),'s(y)) -> c_7()
            'compare#('neg(x),'0()) -> c_8()
            'compare#('neg(x),'pos(y)) -> c_10()
            'compare#('pos(x),'0()) -> c_11()
            'compare#('pos(x),'neg(y)) -> c_12()
            'compare#('s(x),'0()) -> c_14()
            append'1#(nil(),l2) -> c_19()
            flatten'1#(leaf()) -> c_21()
            insert'1#(nil(),x) -> c_26()
            insert'2#('false(),x,y,ys) -> c_27()
            insertionsort'1#(nil()) -> c_31()
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            flattensort(t) -> insertionsort(flatten(t))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('s(x),'0()) -> c_14():26
             -->_1 'compare#('pos(x),'neg(y)) -> c_12():25
             -->_1 'compare#('pos(x),'0()) -> c_11():24
             -->_1 'compare#('neg(x),'pos(y)) -> c_10():23
             -->_1 'compare#('neg(x),'0()) -> c_8():22
             -->_1 'compare#('0(),'s(y)) -> c_7():21
             -->_1 'compare#('0(),'pos(y)) -> c_6():20
             -->_1 'compare#('0(),'neg(y)) -> c_5():19
             -->_1 'compare#('0(),'0()) -> c_4():18
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('s(x),'0()) -> c_14():26
             -->_1 'compare#('pos(x),'neg(y)) -> c_12():25
             -->_1 'compare#('pos(x),'0()) -> c_11():24
             -->_1 'compare#('neg(x),'pos(y)) -> c_10():23
             -->_1 'compare#('neg(x),'0()) -> c_8():22
             -->_1 'compare#('0(),'s(y)) -> c_7():21
             -->_1 'compare#('0(),'pos(y)) -> c_6():20
             -->_1 'compare#('0(),'neg(y)) -> c_5():19
             -->_1 'compare#('0(),'0()) -> c_4():18
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
             -->_1 'compare#('s(x),'0()) -> c_14():26
             -->_1 'compare#('pos(x),'neg(y)) -> c_12():25
             -->_1 'compare#('pos(x),'0()) -> c_11():24
             -->_1 'compare#('neg(x),'pos(y)) -> c_10():23
             -->_1 'compare#('neg(x),'0()) -> c_8():22
             -->_1 'compare#('0(),'s(y)) -> c_7():21
             -->_1 'compare#('0(),'pos(y)) -> c_6():20
             -->_1 'compare#('0(),'neg(y)) -> c_5():19
             -->_1 'compare#('0(),'0()) -> c_4():18
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          4:S:'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y))
             -->_2 'compare#('s(x),'0()) -> c_14():26
             -->_2 'compare#('pos(x),'neg(y)) -> c_12():25
             -->_2 'compare#('pos(x),'0()) -> c_11():24
             -->_2 'compare#('neg(x),'pos(y)) -> c_10():23
             -->_2 'compare#('neg(x),'0()) -> c_8():22
             -->_2 'compare#('0(),'s(y)) -> c_7():21
             -->_2 'compare#('0(),'pos(y)) -> c_6():20
             -->_2 'compare#('0(),'neg(y)) -> c_5():19
             -->_2 'compare#('0(),'0()) -> c_4():18
             -->_1 'cklt#('LT()) -> c_3():17
             -->_1 'cklt#('GT()) -> c_2():16
             -->_1 'cklt#('EQ()) -> c_1():15
             -->_2 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_2 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_2 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          5:S:append#(l1,l2) -> c_17(append'1#(l1,l2))
             -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):6
             -->_1 append'1#(nil(),l2) -> c_19():27
          
          6:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
             -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5
          
          7:S:flatten#(t) -> c_20(flatten'1#(t))
             -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                                    ,append#(flatten(t1),flatten(t2))
                                                    ,flatten#(t1)
                                                    ,flatten#(t2)):8
             -->_1 flatten'1#(leaf()) -> c_21():28
          
          8:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                               ,append#(flatten(t1),flatten(t2))
                                               ,flatten#(t1)
                                               ,flatten#(t2))
             -->_4 flatten#(t) -> c_20(flatten'1#(t)):7
             -->_3 flatten#(t) -> c_20(flatten'1#(t)):7
             -->_2 append#(l1,l2) -> c_17(append'1#(l1,l2)):5
             -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5
          
          9:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
             -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):13
             -->_2 flatten#(t) -> c_20(flatten'1#(t)):7
          
          10:S:insert#(x,l) -> c_24(insert'1#(l,x))
             -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):11
             -->_1 insert'1#(nil(),x) -> c_26():29
          
          11:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
             -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):12
             -->_1 insert'2#('false(),x,y,ys) -> c_27():30
             -->_2 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)):4
          
          12:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
             -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10
          
          13:S:insertionsort#(l) -> c_29(insertionsort'1#(l))
             -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):14
             -->_1 insertionsort'1#(nil()) -> c_31():31
          
          14:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
             -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):13
             -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10
          
          15:W:'cklt#('EQ()) -> c_1()
             
          
          16:W:'cklt#('GT()) -> c_2()
             
          
          17:W:'cklt#('LT()) -> c_3()
             
          
          18:W:'compare#('0(),'0()) -> c_4()
             
          
          19:W:'compare#('0(),'neg(y)) -> c_5()
             
          
          20:W:'compare#('0(),'pos(y)) -> c_6()
             
          
          21:W:'compare#('0(),'s(y)) -> c_7()
             
          
          22:W:'compare#('neg(x),'0()) -> c_8()
             
          
          23:W:'compare#('neg(x),'pos(y)) -> c_10()
             
          
          24:W:'compare#('pos(x),'0()) -> c_11()
             
          
          25:W:'compare#('pos(x),'neg(y)) -> c_12()
             
          
          26:W:'compare#('s(x),'0()) -> c_14()
             
          
          27:W:append'1#(nil(),l2) -> c_19()
             
          
          28:W:flatten'1#(leaf()) -> c_21()
             
          
          29:W:insert'1#(nil(),x) -> c_26()
             
          
          30:W:insert'2#('false(),x,y,ys) -> c_27()
             
          
          31:W:insertionsort'1#(nil()) -> c_31()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          31: insertionsort'1#(nil()) -> c_31()
          29: insert'1#(nil(),x) -> c_26()
          30: insert'2#('false(),x,y,ys) -> c_27()
          28: flatten'1#(leaf()) -> c_21()
          27: append'1#(nil(),l2) -> c_19()
          15: 'cklt#('EQ()) -> c_1()
          16: 'cklt#('GT()) -> c_2()
          17: 'cklt#('LT()) -> c_3()
          18: 'compare#('0(),'0()) -> c_4()
          19: 'compare#('0(),'neg(y)) -> c_5()
          20: 'compare#('0(),'pos(y)) -> c_6()
          21: 'compare#('0(),'s(y)) -> c_7()
          22: 'compare#('neg(x),'0()) -> c_8()
          23: 'compare#('neg(x),'pos(y)) -> c_10()
          24: 'compare#('pos(x),'0()) -> c_11()
          25: 'compare#('pos(x),'neg(y)) -> c_12()
          26: 'compare#('s(x),'0()) -> c_14()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y))
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                             ,append#(flatten(t1),flatten(t2))
                                             ,flatten#(t1)
                                             ,flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            flattensort(t) -> insertionsort(flatten(t))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          4:S:'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y))
             -->_2 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_2 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_2 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          5:S:append#(l1,l2) -> c_17(append'1#(l1,l2))
             -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):6
          
          6:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
             -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5
          
          7:S:flatten#(t) -> c_20(flatten'1#(t))
             -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                                    ,append#(flatten(t1),flatten(t2))
                                                    ,flatten#(t1)
                                                    ,flatten#(t2)):8
          
          8:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                               ,append#(flatten(t1),flatten(t2))
                                               ,flatten#(t1)
                                               ,flatten#(t2))
             -->_4 flatten#(t) -> c_20(flatten'1#(t)):7
             -->_3 flatten#(t) -> c_20(flatten'1#(t)):7
             -->_2 append#(l1,l2) -> c_17(append'1#(l1,l2)):5
             -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):5
          
          9:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
             -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):13
             -->_2 flatten#(t) -> c_20(flatten'1#(t)):7
          
          10:S:insert#(x,l) -> c_24(insert'1#(l,x))
             -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):11
          
          11:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
             -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):12
             -->_2 'less#(x,y) -> c_16('cklt#('compare(x,y)),'compare#(x,y)):4
          
          12:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
             -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10
          
          13:S:insertionsort#(l) -> c_29(insertionsort'1#(l))
             -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):14
          
          14:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
             -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):13
             -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):10
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          'less#(x,y) -> c_16('compare#(x,y))
* Step 5: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                             ,append#(flatten(t1),flatten(t2))
                                             ,flatten#(t1)
                                             ,flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            flattensort(t) -> insertionsort(flatten(t))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          'cklt('EQ()) -> 'false()
          'cklt('GT()) -> 'false()
          'cklt('LT()) -> 'true()
          'compare('0(),'0()) -> 'EQ()
          'compare('0(),'neg(y)) -> 'GT()
          'compare('0(),'pos(y)) -> 'LT()
          'compare('0(),'s(y)) -> 'LT()
          'compare('neg(x),'0()) -> 'LT()
          'compare('neg(x),'neg(y)) -> 'compare(y,x)
          'compare('neg(x),'pos(y)) -> 'LT()
          'compare('pos(x),'0()) -> 'GT()
          'compare('pos(x),'neg(y)) -> 'GT()
          'compare('pos(x),'pos(y)) -> 'compare(x,y)
          'compare('s(x),'0()) -> 'GT()
          'compare('s(x),'s(y)) -> 'compare(x,y)
          'less(x,y) -> 'cklt('compare(x,y))
          append(l1,l2) -> append'1(l1,l2)
          append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
          append'1(nil(),l2) -> l2
          flatten(t) -> flatten'1(t)
          flatten'1(leaf()) -> nil()
          flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
          insert(x,l) -> insert'1(l,x)
          insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
          insert'1(nil(),x) -> dd(x,nil())
          insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
          insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
          insertionsort(l) -> insertionsort'1(l)
          insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
          insertionsort'1(nil()) -> nil()
          'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
          'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
          'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
          'less#(x,y) -> c_16('compare#(x,y))
          append#(l1,l2) -> c_17(append'1#(l1,l2))
          append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
          flatten#(t) -> c_20(flatten'1#(t))
          flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                           ,append#(flatten(t1),flatten(t2))
                                           ,flatten#(t1)
                                           ,flatten#(t2))
          flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
          insert#(x,l) -> c_24(insert'1#(l,x))
          insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
          insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
          insertionsort#(l) -> c_29(insertionsort'1#(l))
          insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
* Step 6: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                             ,append#(flatten(t1),flatten(t2))
                                             ,flatten#(t1)
                                             ,flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          flatten#(t) -> c_20(flatten'1#(t))
          flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                           ,append#(flatten(t1),flatten(t2))
                                           ,flatten#(t1)
                                           ,flatten#(t2))
          flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
          insertionsort#(l) -> c_29(insertionsort'1#(l))
          insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
        and a lower component
          'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
          'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
          'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
          'less#(x,y) -> c_16('compare#(x,y))
          append#(l1,l2) -> c_17(append'1#(l1,l2))
          append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
          insert#(x,l) -> c_24(insert'1#(l,x))
          insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
          insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
        Further, following extension rules are added to the lower component.
          flatten#(t) -> flatten'1#(t)
          flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
          flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
          flatten'1#(node(l,t1,t2)) -> flatten#(t1)
          flatten'1#(node(l,t1,t2)) -> flatten#(t2)
          flattensort#(t) -> flatten#(t)
          flattensort#(t) -> insertionsort#(flatten(t))
          insertionsort#(l) -> insertionsort'1#(l)
          insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
          insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                             ,append#(flatten(t1),flatten(t2))
                                             ,flatten#(t1)
                                             ,flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:flatten#(t) -> c_20(flatten'1#(t))
             -->_1 flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                                    ,append#(flatten(t1),flatten(t2))
                                                    ,flatten#(t1)
                                                    ,flatten#(t2)):2
          
          2:S:flatten'1#(node(l,t1,t2)) -> c_22(append#(l,append(flatten(t1),flatten(t2)))
                                               ,append#(flatten(t1),flatten(t2))
                                               ,flatten#(t1)
                                               ,flatten#(t2))
             -->_4 flatten#(t) -> c_20(flatten'1#(t)):1
             -->_3 flatten#(t) -> c_20(flatten'1#(t)):1
          
          3:S:flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
             -->_1 insertionsort#(l) -> c_29(insertionsort'1#(l)):4
             -->_2 flatten#(t) -> c_20(flatten'1#(t)):1
          
          4:S:insertionsort#(l) -> c_29(insertionsort'1#(l))
             -->_1 insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs)):5
          
          5:S:insertionsort'1#(dd(x,xs)) -> c_30(insert#(x,insertionsort(xs)),insertionsort#(xs))
             -->_2 insertionsort#(l) -> c_29(insertionsort'1#(l)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
          insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          append(l1,l2) -> append'1(l1,l2)
          append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
          append'1(nil(),l2) -> l2
          flatten(t) -> flatten'1(t)
          flatten'1(leaf()) -> nil()
          flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
          flatten#(t) -> c_20(flatten'1#(t))
          flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
          flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
          insertionsort#(l) -> c_29(insertionsort'1#(l))
          insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
** Step 6.a:3: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
        - Weak TRS:
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_20) = {1},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1,2},
          uargs(c_29) = {1},
          uargs(c_30) = {1}
        
        Following symbols are considered usable:
          {'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2#
          ,insertionsort#,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [0]                           
                       p('EQ) = [0]                           
                       p('GT) = [0]                           
                       p('LT) = [0]                           
                     p('cklt) = [0]                           
                  p('compare) = [0]                           
                    p('false) = [0]                           
                     p('less) = [0]                           
                      p('neg) = [1] x1 + [0]                  
                      p('pos) = [1] x1 + [0]                  
                        p('s) = [1] x1 + [0]                  
                     p('true) = [0]                           
                    p(append) = [0]                           
                  p(append'1) = [0]                           
                        p(dd) = [1] x1 + [0]                  
                   p(flatten) = [0]                           
                 p(flatten'1) = [0]                           
               p(flattensort) = [0]                           
                    p(insert) = [0]                           
                  p(insert'1) = [0]                           
                  p(insert'2) = [0]                           
             p(insertionsort) = [0]                           
           p(insertionsort'1) = [0]                           
                      p(leaf) = [0]                           
                       p(nil) = [0]                           
                      p(node) = [1] x1 + [1] x2 + [1] x3 + [2]
                    p('cklt#) = [0]                           
                 p('compare#) = [0]                           
                    p('less#) = [0]                           
                   p(append#) = [0]                           
                 p(append'1#) = [0]                           
                  p(flatten#) = [4] x1 + [4]                  
                p(flatten'1#) = [4] x1 + [4]                  
              p(flattensort#) = [6] x1 + [13]                 
                   p(insert#) = [1] x1 + [0]                  
                 p(insert'1#) = [2] x2 + [1]                  
                 p(insert'2#) = [1] x1 + [1] x2 + [0]         
            p(insertionsort#) = [0]                           
          p(insertionsort'1#) = [0]                           
                       p(c_1) = [2]                           
                       p(c_2) = [8]                           
                       p(c_3) = [1]                           
                       p(c_4) = [0]                           
                       p(c_5) = [1]                           
                       p(c_6) = [2]                           
                       p(c_7) = [1]                           
                       p(c_8) = [0]                           
                       p(c_9) = [2] x1 + [0]                  
                      p(c_10) = [0]                           
                      p(c_11) = [0]                           
                      p(c_12) = [4]                           
                      p(c_13) = [1] x1 + [1]                  
                      p(c_14) = [1]                           
                      p(c_15) = [0]                           
                      p(c_16) = [1] x1 + [1]                  
                      p(c_17) = [0]                           
                      p(c_18) = [4]                           
                      p(c_19) = [2]                           
                      p(c_20) = [1] x1 + [0]                  
                      p(c_21) = [1]                           
                      p(c_22) = [1] x1 + [1] x2 + [2]         
                      p(c_23) = [1] x1 + [1] x2 + [9]         
                      p(c_24) = [0]                           
                      p(c_25) = [1]                           
                      p(c_26) = [1]                           
                      p(c_27) = [0]                           
                      p(c_28) = [0]                           
                      p(c_29) = [8] x1 + [0]                  
                      p(c_30) = [8] x1 + [0]                  
                      p(c_31) = [0]                           
        
        Following rules are strictly oriented:
        flatten'1#(node(l,t1,t2)) = [4] l + [4] t1 + [4] t2 + [12] 
                                  > [4] t1 + [4] t2 + [10]         
                                  = c_22(flatten#(t1),flatten#(t2))
        
        
        Following rules are (at-least) weakly oriented:
                       flatten#(t) =  [4] t + [4]                                 
                                   >= [4] t + [4]                                 
                                   =  c_20(flatten'1#(t))                         
        
                   flattensort#(t) =  [6] t + [13]                                
                                   >= [4] t + [13]                                
                                   =  c_23(insertionsort#(flatten(t)),flatten#(t))
        
                 insertionsort#(l) =  [0]                                         
                                   >= [0]                                         
                                   =  c_29(insertionsort'1#(l))                   
        
        insertionsort'1#(dd(x,xs)) =  [0]                                         
                                   >= [0]                                         
                                   =  c_30(insertionsort#(xs))                    
        
** Step 6.a:4: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
        - Weak DPs:
            flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
        - Weak TRS:
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_20) = {1},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1,2},
          uargs(c_29) = {1},
          uargs(c_30) = {1}
        
        Following symbols are considered usable:
          {'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2#
          ,insertionsort#,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [0]                  
                       p('EQ) = [0]                  
                       p('GT) = [0]                  
                       p('LT) = [0]                  
                     p('cklt) = [0]                  
                  p('compare) = [0]                  
                    p('false) = [0]                  
                     p('less) = [0]                  
                      p('neg) = [1] x1 + [0]         
                      p('pos) = [1] x1 + [0]         
                        p('s) = [1] x1 + [0]         
                     p('true) = [0]                  
                    p(append) = [0]                  
                  p(append'1) = [0]                  
                        p(dd) = [1] x1 + [1] x2 + [0]
                   p(flatten) = [0]                  
                 p(flatten'1) = [14] x1 + [0]        
               p(flattensort) = [0]                  
                    p(insert) = [0]                  
                  p(insert'1) = [0]                  
                  p(insert'2) = [0]                  
             p(insertionsort) = [0]                  
           p(insertionsort'1) = [0]                  
                      p(leaf) = [0]                  
                       p(nil) = [0]                  
                      p(node) = [1] x1 + [1] x3 + [2]
                    p('cklt#) = [0]                  
                 p('compare#) = [0]                  
                    p('less#) = [0]                  
                   p(append#) = [8] x2 + [0]         
                 p(append'1#) = [2] x2 + [0]         
                  p(flatten#) = [0]                  
                p(flatten'1#) = [0]                  
              p(flattensort#) = [1] x1 + [9]         
                   p(insert#) = [0]                  
                 p(insert'1#) = [1] x1 + [1] x2 + [1]
                 p(insert'2#) = [2]                  
            p(insertionsort#) = [0]                  
          p(insertionsort'1#) = [0]                  
                       p(c_1) = [1]                  
                       p(c_2) = [1]                  
                       p(c_3) = [0]                  
                       p(c_4) = [1]                  
                       p(c_5) = [4]                  
                       p(c_6) = [4]                  
                       p(c_7) = [0]                  
                       p(c_8) = [0]                  
                       p(c_9) = [8] x1 + [0]         
                      p(c_10) = [1]                  
                      p(c_11) = [0]                  
                      p(c_12) = [8]                  
                      p(c_13) = [2] x1 + [1]         
                      p(c_14) = [2]                  
                      p(c_15) = [1]                  
                      p(c_16) = [2] x1 + [1]         
                      p(c_17) = [1] x1 + [0]         
                      p(c_18) = [1] x1 + [0]         
                      p(c_19) = [1]                  
                      p(c_20) = [1] x1 + [0]         
                      p(c_21) = [8]                  
                      p(c_22) = [1] x1 + [8] x2 + [0]
                      p(c_23) = [1] x1 + [4] x2 + [1]
                      p(c_24) = [1]                  
                      p(c_25) = [1] x1 + [2] x2 + [1]
                      p(c_26) = [8]                  
                      p(c_27) = [1]                  
                      p(c_28) = [1] x1 + [0]         
                      p(c_29) = [1] x1 + [0]         
                      p(c_30) = [2] x1 + [0]         
                      p(c_31) = [4]                  
        
        Following rules are strictly oriented:
        flattensort#(t) = [1] t + [9]                                 
                        > [1]                                         
                        = c_23(insertionsort#(flatten(t)),flatten#(t))
        
        
        Following rules are (at-least) weakly oriented:
                       flatten#(t) =  [0]                            
                                   >= [0]                            
                                   =  c_20(flatten'1#(t))            
        
         flatten'1#(node(l,t1,t2)) =  [0]                            
                                   >= [0]                            
                                   =  c_22(flatten#(t1),flatten#(t2))
        
                 insertionsort#(l) =  [0]                            
                                   >= [0]                            
                                   =  c_29(insertionsort'1#(l))      
        
        insertionsort'1#(dd(x,xs)) =  [0]                            
                                   >= [0]                            
                                   =  c_30(insertionsort#(xs))       
        
** Step 6.a:5: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
        - Weak DPs:
            flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
        - Weak TRS:
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(append) = {1,2},
            uargs(dd) = {2},
            uargs(insertionsort#) = {1},
            uargs(c_20) = {1},
            uargs(c_22) = {1,2},
            uargs(c_23) = {1,2},
            uargs(c_29) = {1},
            uargs(c_30) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p('0) = [0]                           
                         p('EQ) = [0]                           
                         p('GT) = [0]                           
                         p('LT) = [0]                           
                       p('cklt) = [0]                           
                    p('compare) = [0]                           
                      p('false) = [0]                           
                       p('less) = [0]                           
                        p('neg) = [1] x1 + [0]                  
                        p('pos) = [1] x1 + [0]                  
                          p('s) = [1] x1 + [0]                  
                       p('true) = [0]                           
                      p(append) = [1] x1 + [1] x2 + [0]         
                    p(append'1) = [1] x1 + [1] x2 + [0]         
                          p(dd) = [1] x1 + [1] x2 + [7]         
                     p(flatten) = [1] x1 + [0]                  
                   p(flatten'1) = [1] x1 + [0]                  
                 p(flattensort) = [0]                           
                      p(insert) = [0]                           
                    p(insert'1) = [0]                           
                    p(insert'2) = [0]                           
               p(insertionsort) = [0]                           
             p(insertionsort'1) = [0]                           
                        p(leaf) = [0]                           
                         p(nil) = [0]                           
                        p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
                      p('cklt#) = [0]                           
                   p('compare#) = [0]                           
                      p('less#) = [0]                           
                     p(append#) = [0]                           
                   p(append'1#) = [0]                           
                    p(flatten#) = [2] x1 + [0]                  
                  p(flatten'1#) = [2] x1 + [0]                  
                p(flattensort#) = [3] x1 + [0]                  
                     p(insert#) = [0]                           
                   p(insert'1#) = [0]                           
                   p(insert'2#) = [0]                           
              p(insertionsort#) = [1] x1 + [0]                  
            p(insertionsort'1#) = [1] x1 + [0]                  
                         p(c_1) = [0]                           
                         p(c_2) = [0]                           
                         p(c_3) = [0]                           
                         p(c_4) = [0]                           
                         p(c_5) = [0]                           
                         p(c_6) = [0]                           
                         p(c_7) = [0]                           
                         p(c_8) = [0]                           
                         p(c_9) = [0]                           
                        p(c_10) = [0]                           
                        p(c_11) = [0]                           
                        p(c_12) = [0]                           
                        p(c_13) = [0]                           
                        p(c_14) = [0]                           
                        p(c_15) = [0]                           
                        p(c_16) = [0]                           
                        p(c_17) = [0]                           
                        p(c_18) = [0]                           
                        p(c_19) = [0]                           
                        p(c_20) = [1] x1 + [0]                  
                        p(c_21) = [0]                           
                        p(c_22) = [1] x1 + [1] x2 + [0]         
                        p(c_23) = [1] x1 + [1] x2 + [0]         
                        p(c_24) = [0]                           
                        p(c_25) = [0]                           
                        p(c_26) = [0]                           
                        p(c_27) = [0]                           
                        p(c_28) = [0]                           
                        p(c_29) = [1] x1 + [0]                  
                        p(c_30) = [1] x1 + [0]                  
                        p(c_31) = [0]                           
          
          Following rules are strictly oriented:
          insertionsort'1#(dd(x,xs)) = [1] x + [1] xs + [7]    
                                     > [1] xs + [0]            
                                     = c_30(insertionsort#(xs))
          
          
          Following rules are (at-least) weakly oriented:
                        flatten#(t) =  [2] t + [0]                                 
                                    >= [2] t + [0]                                 
                                    =  c_20(flatten'1#(t))                         
          
          flatten'1#(node(l,t1,t2)) =  [2] l + [2] t1 + [2] t2 + [0]               
                                    >= [2] t1 + [2] t2 + [0]                       
                                    =  c_22(flatten#(t1),flatten#(t2))             
          
                    flattensort#(t) =  [3] t + [0]                                 
                                    >= [3] t + [0]                                 
                                    =  c_23(insertionsort#(flatten(t)),flatten#(t))
          
                  insertionsort#(l) =  [1] l + [0]                                 
                                    >= [1] l + [0]                                 
                                    =  c_29(insertionsort'1#(l))                   
          
                      append(l1,l2) =  [1] l1 + [1] l2 + [0]                       
                                    >= [1] l1 + [1] l2 + [0]                       
                                    =  append'1(l1,l2)                             
          
              append'1(dd(x,xs),l2) =  [1] l2 + [1] x + [1] xs + [7]               
                                    >= [1] l2 + [1] x + [1] xs + [7]               
                                    =  dd(x,append(xs,l2))                         
          
                 append'1(nil(),l2) =  [1] l2 + [0]                                
                                    >= [1] l2 + [0]                                
                                    =  l2                                          
          
                         flatten(t) =  [1] t + [0]                                 
                                    >= [1] t + [0]                                 
                                    =  flatten'1(t)                                
          
                  flatten'1(leaf()) =  [0]                                         
                                    >= [0]                                         
                                    =  nil()                                       
          
           flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]               
                                    >= [1] l + [1] t1 + [1] t2 + [0]               
                                    =  append(l,append(flatten(t1),flatten(t2)))   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 6.a:6: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
        - Weak DPs:
            flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
        - Weak TRS:
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_20) = {1},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1,2},
          uargs(c_29) = {1},
          uargs(c_30) = {1}
        
        Following symbols are considered usable:
          {'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2#
          ,insertionsort#,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [2]                           
                       p('EQ) = [2]                           
                       p('GT) = [0]                           
                       p('LT) = [1]                           
                     p('cklt) = [1] x1 + [1]                  
                  p('compare) = [1] x2 + [2]                  
                    p('false) = [2]                           
                     p('less) = [1] x1 + [1] x2 + [0]         
                      p('neg) = [2]                           
                      p('pos) = [1]                           
                        p('s) = [1]                           
                     p('true) = [0]                           
                    p(append) = [0]                           
                  p(append'1) = [8] x1 + [0]                  
                        p(dd) = [1] x1 + [0]                  
                   p(flatten) = [0]                           
                 p(flatten'1) = [3]                           
               p(flattensort) = [4] x1 + [0]                  
                    p(insert) = [8] x1 + [2] x2 + [4]         
                  p(insert'1) = [2] x1 + [8] x2 + [0]         
                  p(insert'2) = [2] x1 + [8] x2 + [1]         
             p(insertionsort) = [2]                           
           p(insertionsort'1) = [1] x1 + [2]                  
                      p(leaf) = [2]                           
                       p(nil) = [1]                           
                      p(node) = [1] x1 + [1] x2 + [1] x3 + [4]
                    p('cklt#) = [2]                           
                 p('compare#) = [2] x1 + [1] x2 + [2]         
                    p('less#) = [1] x1 + [4] x2 + [2]         
                   p(append#) = [4]                           
                 p(append'1#) = [1] x1 + [2] x2 + [0]         
                  p(flatten#) = [1] x1 + [2]                  
                p(flatten'1#) = [1] x1 + [0]                  
              p(flattensort#) = [8] x1 + [13]                 
                   p(insert#) = [8]                           
                 p(insert'1#) = [1] x1 + [4] x2 + [1]         
                 p(insert'2#) = [1] x1 + [2] x3 + [1] x4 + [2]
            p(insertionsort#) = [0]                           
          p(insertionsort'1#) = [0]                           
                       p(c_1) = [0]                           
                       p(c_2) = [1]                           
                       p(c_3) = [1]                           
                       p(c_4) = [2]                           
                       p(c_5) = [2]                           
                       p(c_6) = [0]                           
                       p(c_7) = [2]                           
                       p(c_8) = [0]                           
                       p(c_9) = [0]                           
                      p(c_10) = [0]                           
                      p(c_11) = [1]                           
                      p(c_12) = [1]                           
                      p(c_13) = [1]                           
                      p(c_14) = [1]                           
                      p(c_15) = [1]                           
                      p(c_16) = [1] x1 + [1]                  
                      p(c_17) = [2] x1 + [2]                  
                      p(c_18) = [8] x1 + [1]                  
                      p(c_19) = [1]                           
                      p(c_20) = [1] x1 + [0]                  
                      p(c_21) = [8]                           
                      p(c_22) = [1] x1 + [1] x2 + [0]         
                      p(c_23) = [1] x1 + [1] x2 + [11]        
                      p(c_24) = [2] x1 + [0]                  
                      p(c_25) = [1] x2 + [1]                  
                      p(c_26) = [0]                           
                      p(c_27) = [8]                           
                      p(c_28) = [1] x1 + [1]                  
                      p(c_29) = [8] x1 + [0]                  
                      p(c_30) = [4] x1 + [0]                  
                      p(c_31) = [1]                           
        
        Following rules are strictly oriented:
        flatten#(t) = [1] t + [2]        
                    > [1] t + [0]        
                    = c_20(flatten'1#(t))
        
        
        Following rules are (at-least) weakly oriented:
         flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [4]               
                                   >= [1] t1 + [1] t2 + [4]                       
                                   =  c_22(flatten#(t1),flatten#(t2))             
        
                   flattensort#(t) =  [8] t + [13]                                
                                   >= [1] t + [13]                                
                                   =  c_23(insertionsort#(flatten(t)),flatten#(t))
        
                 insertionsort#(l) =  [0]                                         
                                   >= [0]                                         
                                   =  c_29(insertionsort'1#(l))                   
        
        insertionsort'1#(dd(x,xs)) =  [0]                                         
                                   >= [0]                                         
                                   =  c_30(insertionsort#(xs))                    
        
** Step 6.a:7: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insertionsort#(l) -> c_29(insertionsort'1#(l))
        - Weak DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
        - Weak TRS:
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_20) = {1},
          uargs(c_22) = {1,2},
          uargs(c_23) = {1,2},
          uargs(c_29) = {1},
          uargs(c_30) = {1}
        
        Following symbols are considered usable:
          {append,append'1,flatten,flatten'1,'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#
          ,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [1]                                    
                       p('EQ) = [8]                                    
                       p('GT) = [1]                                    
                       p('LT) = [0]                                    
                     p('cklt) = [0]                                    
                  p('compare) = [1] x1 + [2] x2 + [1]                  
                    p('false) = [0]                                    
                     p('less) = [1]                                    
                      p('neg) = [1]                                    
                      p('pos) = [0]                                    
                        p('s) = [2]                                    
                     p('true) = [1]                                    
                    p(append) = [1] x1 + [1] x2 + [0]                  
                  p(append'1) = [1] x1 + [1] x2 + [0]                  
                        p(dd) = [1] x2 + [4]                           
                   p(flatten) = [1] x1 + [0]                           
                 p(flatten'1) = [1] x1 + [0]                           
               p(flattensort) = [1] x1 + [4]                           
                    p(insert) = [8]                                    
                  p(insert'1) = [1] x1 + [0]                           
                  p(insert'2) = [1] x1 + [1] x2 + [2] x3 + [1] x4 + [0]
             p(insertionsort) = [1] x1 + [1]                           
           p(insertionsort'1) = [1] x1 + [1]                           
                      p(leaf) = [1]                                    
                       p(nil) = [0]                                    
                      p(node) = [1] x1 + [1] x2 + [1] x3 + [0]         
                    p('cklt#) = [1] x1 + [4]                           
                 p('compare#) = [1] x1 + [2] x2 + [1]                  
                    p('less#) = [2] x1 + [0]                           
                   p(append#) = [1] x2 + [0]                           
                 p(append'1#) = [4]                                    
                  p(flatten#) = [0]                                    
                p(flatten'1#) = [0]                                    
              p(flattensort#) = [4] x1 + [8]                           
                   p(insert#) = [2]                                    
                 p(insert'1#) = [4] x1 + [1]                           
                 p(insert'2#) = [1] x1 + [2] x2 + [2]                  
            p(insertionsort#) = [1] x1 + [2]                           
          p(insertionsort'1#) = [1] x1 + [0]                           
                       p(c_1) = [4]                                    
                       p(c_2) = [2]                                    
                       p(c_3) = [1]                                    
                       p(c_4) = [1]                                    
                       p(c_5) = [4]                                    
                       p(c_6) = [0]                                    
                       p(c_7) = [1]                                    
                       p(c_8) = [1]                                    
                       p(c_9) = [1] x1 + [0]                           
                      p(c_10) = [0]                                    
                      p(c_11) = [4]                                    
                      p(c_12) = [0]                                    
                      p(c_13) = [2] x1 + [0]                           
                      p(c_14) = [1]                                    
                      p(c_15) = [4] x1 + [1]                           
                      p(c_16) = [1] x1 + [1]                           
                      p(c_17) = [1]                                    
                      p(c_18) = [2] x1 + [0]                           
                      p(c_19) = [2]                                    
                      p(c_20) = [1] x1 + [0]                           
                      p(c_21) = [0]                                    
                      p(c_22) = [2] x1 + [8] x2 + [0]                  
                      p(c_23) = [4] x1 + [1] x2 + [0]                  
                      p(c_24) = [2] x1 + [1]                           
                      p(c_25) = [1] x1 + [1] x2 + [1]                  
                      p(c_26) = [2]                                    
                      p(c_27) = [1]                                    
                      p(c_28) = [1] x1 + [0]                           
                      p(c_29) = [1] x1 + [1]                           
                      p(c_30) = [1] x1 + [2]                           
                      p(c_31) = [2]                                    
        
        Following rules are strictly oriented:
        insertionsort#(l) = [1] l + [2]              
                          > [1] l + [1]              
                          = c_29(insertionsort'1#(l))
        
        
        Following rules are (at-least) weakly oriented:
                       flatten#(t) =  [0]                                         
                                   >= [0]                                         
                                   =  c_20(flatten'1#(t))                         
        
         flatten'1#(node(l,t1,t2)) =  [0]                                         
                                   >= [0]                                         
                                   =  c_22(flatten#(t1),flatten#(t2))             
        
                   flattensort#(t) =  [4] t + [8]                                 
                                   >= [4] t + [8]                                 
                                   =  c_23(insertionsort#(flatten(t)),flatten#(t))
        
        insertionsort'1#(dd(x,xs)) =  [1] xs + [4]                                
                                   >= [1] xs + [4]                                
                                   =  c_30(insertionsort#(xs))                    
        
                     append(l1,l2) =  [1] l1 + [1] l2 + [0]                       
                                   >= [1] l1 + [1] l2 + [0]                       
                                   =  append'1(l1,l2)                             
        
             append'1(dd(x,xs),l2) =  [1] l2 + [1] xs + [4]                       
                                   >= [1] l2 + [1] xs + [4]                       
                                   =  dd(x,append(xs,l2))                         
        
                append'1(nil(),l2) =  [1] l2 + [0]                                
                                   >= [1] l2 + [0]                                
                                   =  l2                                          
        
                        flatten(t) =  [1] t + [0]                                 
                                   >= [1] t + [0]                                 
                                   =  flatten'1(t)                                
        
                 flatten'1(leaf()) =  [1]                                         
                                   >= [0]                                         
                                   =  nil()                                       
        
          flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]               
                                   >= [1] l + [1] t1 + [1] t2 + [0]               
                                   =  append(l,append(flatten(t1),flatten(t2)))   
        
** Step 6.a:8: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            flatten#(t) -> c_20(flatten'1#(t))
            flatten'1#(node(l,t1,t2)) -> c_22(flatten#(t1),flatten#(t2))
            flattensort#(t) -> c_23(insertionsort#(flatten(t)),flatten#(t))
            insertionsort#(l) -> c_29(insertionsort'1#(l))
            insertionsort'1#(dd(x,xs)) -> c_30(insertionsort#(xs))
        - Weak TRS:
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/2,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/1,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
        - Weak DPs:
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> flatten#(t)
            flattensort#(t) -> insertionsort#(flatten(t))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          append#(l1,l2) -> c_17(append'1#(l1,l2))
          append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
          flatten#(t) -> flatten'1#(t)
          flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
          flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
          flatten'1#(node(l,t1,t2)) -> flatten#(t1)
          flatten'1#(node(l,t1,t2)) -> flatten#(t2)
          flattensort#(t) -> flatten#(t)
          flattensort#(t) -> insertionsort#(flatten(t))
          insert#(x,l) -> c_24(insert'1#(l,x))
          insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
          insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
          insertionsort#(l) -> insertionsort'1#(l)
          insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
          insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        and a lower component
          'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
          'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
          'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
          'less#(x,y) -> c_16('compare#(x,y))
        Further, following extension rules are added to the lower component.
          append#(l1,l2) -> append'1#(l1,l2)
          append'1#(dd(x,xs),l2) -> append#(xs,l2)
          flatten#(t) -> flatten'1#(t)
          flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
          flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
          flatten'1#(node(l,t1,t2)) -> flatten#(t1)
          flatten'1#(node(l,t1,t2)) -> flatten#(t2)
          flattensort#(t) -> flatten#(t)
          flattensort#(t) -> insertionsort#(flatten(t))
          insert#(x,l) -> insert'1#(l,x)
          insert'1#(dd(y,ys),x) -> 'less#(y,x)
          insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
          insert'2#('true(),x,y,ys) -> insert#(x,ys)
          insertionsort#(l) -> insertionsort'1#(l)
          insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
          insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
*** Step 6.b:1.a:1: RemoveHeads WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
        - Weak DPs:
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> flatten#(t)
            flattensort#(t) -> insertionsort#(flatten(t))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:append#(l1,l2) -> c_17(append'1#(l1,l2))
           -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):2
        
        2:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
           -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1
        
        3:S:insert#(x,l) -> c_24(insert'1#(l,x))
           -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):4
        
        4:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
           -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):5
        
        5:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
           -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3
        
        6:W:flatten#(t) -> flatten'1#(t)
           -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):10
           -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):9
           -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):8
           -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):7
        
        7:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
           -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1
        
        8:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
           -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1
        
        9:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1)
           -->_1 flatten#(t) -> flatten'1#(t):6
        
        10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2)
           -->_1 flatten#(t) -> flatten'1#(t):6
        
        11:W:flattensort#(t) -> flatten#(t)
           -->_1 flatten#(t) -> flatten'1#(t):6
        
        12:W:flattensort#(t) -> insertionsort#(flatten(t))
           -->_1 insertionsort#(l) -> insertionsort'1#(l):13
        
        13:W:insertionsort#(l) -> insertionsort'1#(l)
           -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):15
           -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):14
        
        14:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
           -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3
        
        15:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
           -->_1 insertionsort#(l) -> insertionsort'1#(l):13
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(11,flattensort#(t) -> flatten#(t))]
*** Step 6.b:1.a:2: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
        - Weak DPs:
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> insertionsort#(flatten(t))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:append#(l1,l2) -> c_17(append'1#(l1,l2))
             -->_1 append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2)):2
          
          2:S:append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
             -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1
          
          3:S:insert#(x,l) -> c_24(insert'1#(l,x))
             -->_1 insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x)):4
          
          4:S:insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys),'less#(y,x))
             -->_1 insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys)):5
          
          5:S:insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
             -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3
          
          6:W:flatten#(t) -> flatten'1#(t)
             -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):10
             -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):9
             -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):8
             -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):7
          
          7:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
             -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1
          
          8:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
             -->_1 append#(l1,l2) -> c_17(append'1#(l1,l2)):1
          
          9:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1)
             -->_1 flatten#(t) -> flatten'1#(t):6
          
          10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2)
             -->_1 flatten#(t) -> flatten'1#(t):6
          
          12:W:flattensort#(t) -> insertionsort#(flatten(t))
             -->_1 insertionsort#(l) -> insertionsort'1#(l):13
          
          13:W:insertionsort#(l) -> insertionsort'1#(l)
             -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):15
             -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):14
          
          14:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
             -->_1 insert#(x,l) -> c_24(insert'1#(l,x)):3
          
          15:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
             -->_1 insertionsort#(l) -> insertionsort'1#(l):13
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys))
*** Step 6.b:1.a:3: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
        - Weak DPs:
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> insertionsort#(flatten(t))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_17) = {1},
          uargs(c_18) = {1},
          uargs(c_24) = {1},
          uargs(c_25) = {1},
          uargs(c_28) = {1}
        
        Following symbols are considered usable:
          {append,append'1,flatten,flatten'1,'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#
          ,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [0]                           
                       p('EQ) = [0]                           
                       p('GT) = [0]                           
                       p('LT) = [0]                           
                     p('cklt) = [5] x1 + [0]                  
                  p('compare) = [1] x2 + [3]                  
                    p('false) = [4]                           
                     p('less) = [0]                           
                      p('neg) = [0]                           
                      p('pos) = [0]                           
                        p('s) = [1] x1 + [0]                  
                     p('true) = [0]                           
                    p(append) = [1] x1 + [1] x2 + [0]         
                  p(append'1) = [1] x1 + [1] x2 + [0]         
                        p(dd) = [1] x2 + [1]                  
                   p(flatten) = [1] x1 + [0]                  
                 p(flatten'1) = [1] x1 + [0]                  
               p(flattensort) = [1] x1 + [4]                  
                    p(insert) = [2] x1 + [0]                  
                  p(insert'1) = [4]                           
                  p(insert'2) = [2] x1 + [4] x2 + [2]         
             p(insertionsort) = [0]                           
           p(insertionsort'1) = [0]                           
                      p(leaf) = [4]                           
                       p(nil) = [1]                           
                      p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
                    p('cklt#) = [4] x1 + [1]                  
                 p('compare#) = [1] x1 + [1] x2 + [0]         
                    p('less#) = [0]                           
                   p(append#) = [4] x1 + [1]                  
                 p(append'1#) = [4] x1 + [0]                  
                  p(flatten#) = [4] x1 + [4]                  
                p(flatten'1#) = [4] x1 + [4]                  
              p(flattensort#) = [5] x1 + [0]                  
                   p(insert#) = [0]                           
                 p(insert'1#) = [0]                           
                 p(insert'2#) = [0]                           
            p(insertionsort#) = [4] x1 + [0]                  
          p(insertionsort'1#) = [4] x1 + [0]                  
                       p(c_1) = [2]                           
                       p(c_2) = [1]                           
                       p(c_3) = [0]                           
                       p(c_4) = [4]                           
                       p(c_5) = [1]                           
                       p(c_6) = [0]                           
                       p(c_7) = [0]                           
                       p(c_8) = [1]                           
                       p(c_9) = [1]                           
                      p(c_10) = [1]                           
                      p(c_11) = [2]                           
                      p(c_12) = [1]                           
                      p(c_13) = [1]                           
                      p(c_14) = [1]                           
                      p(c_15) = [1]                           
                      p(c_16) = [1]                           
                      p(c_17) = [1] x1 + [0]                  
                      p(c_18) = [1] x1 + [0]                  
                      p(c_19) = [0]                           
                      p(c_20) = [1] x1 + [0]                  
                      p(c_21) = [2]                           
                      p(c_22) = [1] x1 + [1] x3 + [0]         
                      p(c_23) = [2] x1 + [1] x2 + [0]         
                      p(c_24) = [4] x1 + [0]                  
                      p(c_25) = [1] x1 + [0]                  
                      p(c_26) = [1]                           
                      p(c_27) = [0]                           
                      p(c_28) = [1] x1 + [0]                  
                      p(c_29) = [0]                           
                      p(c_30) = [4] x1 + [1] x2 + [0]         
                      p(c_31) = [1]                           
        
        Following rules are strictly oriented:
                append#(l1,l2) = [4] l1 + [1]          
                               > [4] l1 + [0]          
                               = c_17(append'1#(l1,l2))
        
        append'1#(dd(x,xs),l2) = [4] xs + [4]          
                               > [4] xs + [1]          
                               = c_18(append#(xs,l2))  
        
        
        Following rules are (at-least) weakly oriented:
                       flatten#(t) =  [4] t + [4]                               
                                   >= [4] t + [4]                               
                                   =  flatten'1#(t)                             
        
         flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [4]             
                                   >= [4] l + [1]                               
                                   =  append#(l,append(flatten(t1),flatten(t2)))
        
         flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [4]             
                                   >= [4] t1 + [1]                              
                                   =  append#(flatten(t1),flatten(t2))          
        
         flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [4]             
                                   >= [4] t1 + [4]                              
                                   =  flatten#(t1)                              
        
         flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [4]             
                                   >= [4] t2 + [4]                              
                                   =  flatten#(t2)                              
        
                   flattensort#(t) =  [5] t + [0]                               
                                   >= [4] t + [0]                               
                                   =  insertionsort#(flatten(t))                
        
                      insert#(x,l) =  [0]                                       
                                   >= [0]                                       
                                   =  c_24(insert'1#(l,x))                      
        
             insert'1#(dd(y,ys),x) =  [0]                                       
                                   >= [0]                                       
                                   =  c_25(insert'2#('less(y,x),x,y,ys))        
        
         insert'2#('true(),x,y,ys) =  [0]                                       
                                   >= [0]                                       
                                   =  c_28(insert#(x,ys))                       
        
                 insertionsort#(l) =  [4] l + [0]                               
                                   >= [4] l + [0]                               
                                   =  insertionsort'1#(l)                       
        
        insertionsort'1#(dd(x,xs)) =  [4] xs + [4]                              
                                   >= [0]                                       
                                   =  insert#(x,insertionsort(xs))              
        
        insertionsort'1#(dd(x,xs)) =  [4] xs + [4]                              
                                   >= [4] xs + [0]                              
                                   =  insertionsort#(xs)                        
        
                     append(l1,l2) =  [1] l1 + [1] l2 + [0]                     
                                   >= [1] l1 + [1] l2 + [0]                     
                                   =  append'1(l1,l2)                           
        
             append'1(dd(x,xs),l2) =  [1] l2 + [1] xs + [1]                     
                                   >= [1] l2 + [1] xs + [1]                     
                                   =  dd(x,append(xs,l2))                       
        
                append'1(nil(),l2) =  [1] l2 + [1]                              
                                   >= [1] l2 + [0]                              
                                   =  l2                                        
        
                        flatten(t) =  [1] t + [0]                               
                                   >= [1] t + [0]                               
                                   =  flatten'1(t)                              
        
                 flatten'1(leaf()) =  [4]                                       
                                   >= [1]                                       
                                   =  nil()                                     
        
          flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]             
                                   >= [1] l + [1] t1 + [1] t2 + [0]             
                                   =  append(l,append(flatten(t1),flatten(t2))) 
        
*** Step 6.b:1.a:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
        - Weak DPs:
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> insertionsort#(flatten(t))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs('cklt) = {1},
            uargs(append) = {1,2},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert'2) = {1},
            uargs(append#) = {1,2},
            uargs(insert#) = {2},
            uargs(insert'2#) = {1},
            uargs(insertionsort#) = {1},
            uargs(c_17) = {1},
            uargs(c_18) = {1},
            uargs(c_24) = {1},
            uargs(c_25) = {1},
            uargs(c_28) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p('0) = [0]                           
                         p('EQ) = [0]                           
                         p('GT) = [0]                           
                         p('LT) = [0]                           
                       p('cklt) = [1] x1 + [0]                  
                    p('compare) = [0]                           
                      p('false) = [0]                           
                       p('less) = [0]                           
                        p('neg) = [1] x1 + [0]                  
                        p('pos) = [1] x1 + [0]                  
                          p('s) = [1] x1 + [0]                  
                       p('true) = [0]                           
                      p(append) = [1] x1 + [1] x2 + [0]         
                    p(append'1) = [1] x1 + [1] x2 + [0]         
                          p(dd) = [1] x2 + [0]                  
                     p(flatten) = [1] x1 + [0]                  
                   p(flatten'1) = [1] x1 + [0]                  
                 p(flattensort) = [0]                           
                      p(insert) = [1] x2 + [0]                  
                    p(insert'1) = [1] x1 + [0]                  
                    p(insert'2) = [1] x1 + [1] x4 + [0]         
               p(insertionsort) = [2]                           
             p(insertionsort'1) = [2]                           
                        p(leaf) = [0]                           
                         p(nil) = [0]                           
                        p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
                      p('cklt#) = [0]                           
                   p('compare#) = [0]                           
                      p('less#) = [0]                           
                     p(append#) = [1] x1 + [1] x2 + [4]         
                   p(append'1#) = [1] x1 + [1] x2 + [4]         
                    p(flatten#) = [1] x1 + [4]                  
                  p(flatten'1#) = [1] x1 + [4]                  
                p(flattensort#) = [1] x1 + [2]                  
                     p(insert#) = [1] x2 + [0]                  
                   p(insert'1#) = [1] x1 + [0]                  
                   p(insert'2#) = [1] x1 + [1] x4 + [7]         
              p(insertionsort#) = [1] x1 + [2]                  
            p(insertionsort'1#) = [1] x1 + [2]                  
                         p(c_1) = [0]                           
                         p(c_2) = [0]                           
                         p(c_3) = [0]                           
                         p(c_4) = [0]                           
                         p(c_5) = [0]                           
                         p(c_6) = [0]                           
                         p(c_7) = [0]                           
                         p(c_8) = [0]                           
                         p(c_9) = [0]                           
                        p(c_10) = [0]                           
                        p(c_11) = [0]                           
                        p(c_12) = [0]                           
                        p(c_13) = [0]                           
                        p(c_14) = [0]                           
                        p(c_15) = [0]                           
                        p(c_16) = [0]                           
                        p(c_17) = [1] x1 + [0]                  
                        p(c_18) = [1] x1 + [0]                  
                        p(c_19) = [0]                           
                        p(c_20) = [0]                           
                        p(c_21) = [0]                           
                        p(c_22) = [0]                           
                        p(c_23) = [0]                           
                        p(c_24) = [1] x1 + [0]                  
                        p(c_25) = [1] x1 + [0]                  
                        p(c_26) = [0]                           
                        p(c_27) = [0]                           
                        p(c_28) = [1] x1 + [0]                  
                        p(c_29) = [0]                           
                        p(c_30) = [0]                           
                        p(c_31) = [0]                           
          
          Following rules are strictly oriented:
          insert'2#('true(),x,y,ys) = [1] ys + [7]       
                                    > [1] ys + [0]       
                                    = c_28(insert#(x,ys))
          
          
          Following rules are (at-least) weakly oriented:
                      append#(l1,l2) =  [1] l1 + [1] l2 + [4]                     
                                     >= [1] l1 + [1] l2 + [4]                     
                                     =  c_17(append'1#(l1,l2))                    
          
              append'1#(dd(x,xs),l2) =  [1] l2 + [1] xs + [4]                     
                                     >= [1] l2 + [1] xs + [4]                     
                                     =  c_18(append#(xs,l2))                      
          
                         flatten#(t) =  [1] t + [4]                               
                                     >= [1] t + [4]                               
                                     =  flatten'1#(t)                             
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [4]             
                                     >= [1] l + [1] t1 + [1] t2 + [4]             
                                     =  append#(l,append(flatten(t1),flatten(t2)))
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [4]             
                                     >= [1] t1 + [1] t2 + [4]                     
                                     =  append#(flatten(t1),flatten(t2))          
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [4]             
                                     >= [1] t1 + [4]                              
                                     =  flatten#(t1)                              
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [4]             
                                     >= [1] t2 + [4]                              
                                     =  flatten#(t2)                              
          
                     flattensort#(t) =  [1] t + [2]                               
                                     >= [1] t + [2]                               
                                     =  insertionsort#(flatten(t))                
          
                        insert#(x,l) =  [1] l + [0]                               
                                     >= [1] l + [0]                               
                                     =  c_24(insert'1#(l,x))                      
          
               insert'1#(dd(y,ys),x) =  [1] ys + [0]                              
                                     >= [1] ys + [7]                              
                                     =  c_25(insert'2#('less(y,x),x,y,ys))        
          
                   insertionsort#(l) =  [1] l + [2]                               
                                     >= [1] l + [2]                               
                                     =  insertionsort'1#(l)                       
          
          insertionsort'1#(dd(x,xs)) =  [1] xs + [2]                              
                                     >= [2]                                       
                                     =  insert#(x,insertionsort(xs))              
          
          insertionsort'1#(dd(x,xs)) =  [1] xs + [2]                              
                                     >= [1] xs + [2]                              
                                     =  insertionsort#(xs)                        
          
                        'cklt('EQ()) =  [0]                                       
                                     >= [0]                                       
                                     =  'false()                                  
          
                        'cklt('GT()) =  [0]                                       
                                     >= [0]                                       
                                     =  'false()                                  
          
                        'cklt('LT()) =  [0]                                       
                                     >= [0]                                       
                                     =  'true()                                   
          
                 'compare('0(),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'EQ()                                     
          
              'compare('0(),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
              'compare('0(),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
                'compare('0(),'s(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
              'compare('neg(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
           'compare('neg(x),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(y,x)                             
          
           'compare('neg(x),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
              'compare('pos(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
           'compare('pos(x),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
           'compare('pos(x),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(x,y)                             
          
                'compare('s(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
               'compare('s(x),'s(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(x,y)                             
          
                          'less(x,y) =  [0]                                       
                                     >= [0]                                       
                                     =  'cklt('compare(x,y))                      
          
                       append(l1,l2) =  [1] l1 + [1] l2 + [0]                     
                                     >= [1] l1 + [1] l2 + [0]                     
                                     =  append'1(l1,l2)                           
          
               append'1(dd(x,xs),l2) =  [1] l2 + [1] xs + [0]                     
                                     >= [1] l2 + [1] xs + [0]                     
                                     =  dd(x,append(xs,l2))                       
          
                  append'1(nil(),l2) =  [1] l2 + [0]                              
                                     >= [1] l2 + [0]                              
                                     =  l2                                        
          
                          flatten(t) =  [1] t + [0]                               
                                     >= [1] t + [0]                               
                                     =  flatten'1(t)                              
          
                   flatten'1(leaf()) =  [0]                                       
                                     >= [0]                                       
                                     =  nil()                                     
          
            flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]             
                                     >= [1] l + [1] t1 + [1] t2 + [0]             
                                     =  append(l,append(flatten(t1),flatten(t2))) 
          
                         insert(x,l) =  [1] l + [0]                               
                                     >= [1] l + [0]                               
                                     =  insert'1(l,x)                             
          
                insert'1(dd(y,ys),x) =  [1] ys + [0]                              
                                     >= [1] ys + [0]                              
                                     =  insert'2('less(y,x),x,y,ys)               
          
                   insert'1(nil(),x) =  [0]                                       
                                     >= [0]                                       
                                     =  dd(x,nil())                               
          
           insert'2('false(),x,y,ys) =  [1] ys + [0]                              
                                     >= [1] ys + [0]                              
                                     =  dd(x,dd(y,ys))                            
          
            insert'2('true(),x,y,ys) =  [1] ys + [0]                              
                                     >= [1] ys + [0]                              
                                     =  dd(y,insert(x,ys))                        
          
                    insertionsort(l) =  [2]                                       
                                     >= [2]                                       
                                     =  insertionsort'1(l)                        
          
           insertionsort'1(dd(x,xs)) =  [2]                                       
                                     >= [2]                                       
                                     =  insert(x,insertionsort(xs))               
          
              insertionsort'1(nil()) =  [2]                                       
                                     >= [0]                                       
                                     =  nil()                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.a:5: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys))
        - Weak DPs:
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> insertionsort#(flatten(t))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs('cklt) = {1},
            uargs(append) = {1,2},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert'2) = {1},
            uargs(append#) = {1,2},
            uargs(insert#) = {2},
            uargs(insert'2#) = {1},
            uargs(insertionsort#) = {1},
            uargs(c_17) = {1},
            uargs(c_18) = {1},
            uargs(c_24) = {1},
            uargs(c_25) = {1},
            uargs(c_28) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p('0) = [0]                           
                         p('EQ) = [0]                           
                         p('GT) = [0]                           
                         p('LT) = [0]                           
                       p('cklt) = [1] x1 + [0]                  
                    p('compare) = [0]                           
                      p('false) = [0]                           
                       p('less) = [0]                           
                        p('neg) = [1] x1 + [0]                  
                        p('pos) = [1] x1 + [0]                  
                          p('s) = [1] x1 + [0]                  
                       p('true) = [0]                           
                      p(append) = [1] x1 + [1] x2 + [0]         
                    p(append'1) = [1] x1 + [1] x2 + [0]         
                          p(dd) = [1] x2 + [0]                  
                     p(flatten) = [1] x1 + [0]                  
                   p(flatten'1) = [1] x1 + [0]                  
                 p(flattensort) = [0]                           
                      p(insert) = [1] x2 + [0]                  
                    p(insert'1) = [1] x1 + [0]                  
                    p(insert'2) = [1] x1 + [1] x4 + [0]         
               p(insertionsort) = [1] x1 + [0]                  
             p(insertionsort'1) = [1] x1 + [0]                  
                        p(leaf) = [0]                           
                         p(nil) = [0]                           
                        p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
                      p('cklt#) = [0]                           
                   p('compare#) = [0]                           
                      p('less#) = [0]                           
                     p(append#) = [1] x1 + [1] x2 + [0]         
                   p(append'1#) = [1] x1 + [1] x2 + [0]         
                    p(flatten#) = [1] x1 + [0]                  
                  p(flatten'1#) = [1] x1 + [0]                  
                p(flattensort#) = [1] x1 + [0]                  
                     p(insert#) = [1] x2 + [0]                  
                   p(insert'1#) = [1] x1 + [7]                  
                   p(insert'2#) = [1] x1 + [1] x4 + [0]         
              p(insertionsort#) = [1] x1 + [0]                  
            p(insertionsort'1#) = [1] x1 + [0]                  
                         p(c_1) = [0]                           
                         p(c_2) = [0]                           
                         p(c_3) = [0]                           
                         p(c_4) = [0]                           
                         p(c_5) = [0]                           
                         p(c_6) = [0]                           
                         p(c_7) = [0]                           
                         p(c_8) = [0]                           
                         p(c_9) = [0]                           
                        p(c_10) = [0]                           
                        p(c_11) = [0]                           
                        p(c_12) = [0]                           
                        p(c_13) = [0]                           
                        p(c_14) = [0]                           
                        p(c_15) = [0]                           
                        p(c_16) = [0]                           
                        p(c_17) = [1] x1 + [0]                  
                        p(c_18) = [1] x1 + [0]                  
                        p(c_19) = [0]                           
                        p(c_20) = [0]                           
                        p(c_21) = [0]                           
                        p(c_22) = [0]                           
                        p(c_23) = [0]                           
                        p(c_24) = [1] x1 + [0]                  
                        p(c_25) = [1] x1 + [0]                  
                        p(c_26) = [0]                           
                        p(c_27) = [0]                           
                        p(c_28) = [1] x1 + [0]                  
                        p(c_29) = [0]                           
                        p(c_30) = [0]                           
                        p(c_31) = [0]                           
          
          Following rules are strictly oriented:
          insert'1#(dd(y,ys),x) = [1] ys + [7]                      
                                > [1] ys + [0]                      
                                = c_25(insert'2#('less(y,x),x,y,ys))
          
          
          Following rules are (at-least) weakly oriented:
                      append#(l1,l2) =  [1] l1 + [1] l2 + [0]                     
                                     >= [1] l1 + [1] l2 + [0]                     
                                     =  c_17(append'1#(l1,l2))                    
          
              append'1#(dd(x,xs),l2) =  [1] l2 + [1] xs + [0]                     
                                     >= [1] l2 + [1] xs + [0]                     
                                     =  c_18(append#(xs,l2))                      
          
                         flatten#(t) =  [1] t + [0]                               
                                     >= [1] t + [0]                               
                                     =  flatten'1#(t)                             
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]             
                                     >= [1] l + [1] t1 + [1] t2 + [0]             
                                     =  append#(l,append(flatten(t1),flatten(t2)))
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]             
                                     >= [1] t1 + [1] t2 + [0]                     
                                     =  append#(flatten(t1),flatten(t2))          
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]             
                                     >= [1] t1 + [0]                              
                                     =  flatten#(t1)                              
          
           flatten'1#(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]             
                                     >= [1] t2 + [0]                              
                                     =  flatten#(t2)                              
          
                     flattensort#(t) =  [1] t + [0]                               
                                     >= [1] t + [0]                               
                                     =  insertionsort#(flatten(t))                
          
                        insert#(x,l) =  [1] l + [0]                               
                                     >= [1] l + [7]                               
                                     =  c_24(insert'1#(l,x))                      
          
           insert'2#('true(),x,y,ys) =  [1] ys + [0]                              
                                     >= [1] ys + [0]                              
                                     =  c_28(insert#(x,ys))                       
          
                   insertionsort#(l) =  [1] l + [0]                               
                                     >= [1] l + [0]                               
                                     =  insertionsort'1#(l)                       
          
          insertionsort'1#(dd(x,xs)) =  [1] xs + [0]                              
                                     >= [1] xs + [0]                              
                                     =  insert#(x,insertionsort(xs))              
          
          insertionsort'1#(dd(x,xs)) =  [1] xs + [0]                              
                                     >= [1] xs + [0]                              
                                     =  insertionsort#(xs)                        
          
                        'cklt('EQ()) =  [0]                                       
                                     >= [0]                                       
                                     =  'false()                                  
          
                        'cklt('GT()) =  [0]                                       
                                     >= [0]                                       
                                     =  'false()                                  
          
                        'cklt('LT()) =  [0]                                       
                                     >= [0]                                       
                                     =  'true()                                   
          
                 'compare('0(),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'EQ()                                     
          
              'compare('0(),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
              'compare('0(),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
                'compare('0(),'s(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
              'compare('neg(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
           'compare('neg(x),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(y,x)                             
          
           'compare('neg(x),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
              'compare('pos(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
           'compare('pos(x),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
           'compare('pos(x),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(x,y)                             
          
                'compare('s(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
               'compare('s(x),'s(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(x,y)                             
          
                          'less(x,y) =  [0]                                       
                                     >= [0]                                       
                                     =  'cklt('compare(x,y))                      
          
                       append(l1,l2) =  [1] l1 + [1] l2 + [0]                     
                                     >= [1] l1 + [1] l2 + [0]                     
                                     =  append'1(l1,l2)                           
          
               append'1(dd(x,xs),l2) =  [1] l2 + [1] xs + [0]                     
                                     >= [1] l2 + [1] xs + [0]                     
                                     =  dd(x,append(xs,l2))                       
          
                  append'1(nil(),l2) =  [1] l2 + [0]                              
                                     >= [1] l2 + [0]                              
                                     =  l2                                        
          
                          flatten(t) =  [1] t + [0]                               
                                     >= [1] t + [0]                               
                                     =  flatten'1(t)                              
          
                   flatten'1(leaf()) =  [0]                                       
                                     >= [0]                                       
                                     =  nil()                                     
          
            flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]             
                                     >= [1] l + [1] t1 + [1] t2 + [0]             
                                     =  append(l,append(flatten(t1),flatten(t2))) 
          
                         insert(x,l) =  [1] l + [0]                               
                                     >= [1] l + [0]                               
                                     =  insert'1(l,x)                             
          
                insert'1(dd(y,ys),x) =  [1] ys + [0]                              
                                     >= [1] ys + [0]                              
                                     =  insert'2('less(y,x),x,y,ys)               
          
                   insert'1(nil(),x) =  [0]                                       
                                     >= [0]                                       
                                     =  dd(x,nil())                               
          
           insert'2('false(),x,y,ys) =  [1] ys + [0]                              
                                     >= [1] ys + [0]                              
                                     =  dd(x,dd(y,ys))                            
          
            insert'2('true(),x,y,ys) =  [1] ys + [0]                              
                                     >= [1] ys + [0]                              
                                     =  dd(y,insert(x,ys))                        
          
                    insertionsort(l) =  [1] l + [0]                               
                                     >= [1] l + [0]                               
                                     =  insertionsort'1(l)                        
          
           insertionsort'1(dd(x,xs)) =  [1] xs + [0]                              
                                     >= [1] xs + [0]                              
                                     =  insert(x,insertionsort(xs))               
          
              insertionsort'1(nil()) =  [0]                                       
                                     >= [0]                                       
                                     =  nil()                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.a:6: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insert#(x,l) -> c_24(insert'1#(l,x))
        - Weak DPs:
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> insertionsort#(flatten(t))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs('cklt) = {1},
            uargs(append) = {1,2},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert'2) = {1},
            uargs(append#) = {1,2},
            uargs(insert#) = {2},
            uargs(insert'2#) = {1},
            uargs(insertionsort#) = {1},
            uargs(c_17) = {1},
            uargs(c_18) = {1},
            uargs(c_24) = {1},
            uargs(c_25) = {1},
            uargs(c_28) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p('0) = [0]                           
                         p('EQ) = [0]                           
                         p('GT) = [0]                           
                         p('LT) = [0]                           
                       p('cklt) = [1] x1 + [0]                  
                    p('compare) = [0]                           
                      p('false) = [0]                           
                       p('less) = [0]                           
                        p('neg) = [0]                           
                        p('pos) = [1] x1 + [0]                  
                          p('s) = [1] x1 + [0]                  
                       p('true) = [0]                           
                      p(append) = [1] x1 + [1] x2 + [0]         
                    p(append'1) = [1] x1 + [1] x2 + [0]         
                          p(dd) = [1] x2 + [1]                  
                     p(flatten) = [1] x1 + [1]                  
                   p(flatten'1) = [1] x1 + [1]                  
                 p(flattensort) = [0]                           
                      p(insert) = [1] x2 + [1]                  
                    p(insert'1) = [1] x1 + [1]                  
                    p(insert'2) = [1] x1 + [1] x4 + [2]         
               p(insertionsort) = [1] x1 + [4]                  
             p(insertionsort'1) = [1] x1 + [4]                  
                        p(leaf) = [0]                           
                         p(nil) = [0]                           
                        p(node) = [1] x1 + [1] x2 + [1] x3 + [2]
                      p('cklt#) = [0]                           
                   p('compare#) = [0]                           
                      p('less#) = [1] x1 + [0]                  
                     p(append#) = [1] x1 + [1] x2 + [0]         
                   p(append'1#) = [1] x1 + [1] x2 + [0]         
                    p(flatten#) = [4] x1 + [0]                  
                  p(flatten'1#) = [4] x1 + [0]                  
                p(flattensort#) = [1] x1 + [5]                  
                     p(insert#) = [1] x2 + [1]                  
                   p(insert'1#) = [1] x1 + [0]                  
                   p(insert'2#) = [1] x1 + [1] x4 + [1]         
              p(insertionsort#) = [1] x1 + [4]                  
            p(insertionsort'1#) = [1] x1 + [4]                  
                         p(c_1) = [0]                           
                         p(c_2) = [0]                           
                         p(c_3) = [0]                           
                         p(c_4) = [2]                           
                         p(c_5) = [1]                           
                         p(c_6) = [0]                           
                         p(c_7) = [1]                           
                         p(c_8) = [1]                           
                         p(c_9) = [1]                           
                        p(c_10) = [1]                           
                        p(c_11) = [0]                           
                        p(c_12) = [4]                           
                        p(c_13) = [0]                           
                        p(c_14) = [1]                           
                        p(c_15) = [4]                           
                        p(c_16) = [1] x1 + [0]                  
                        p(c_17) = [1] x1 + [0]                  
                        p(c_18) = [1] x1 + [1]                  
                        p(c_19) = [1]                           
                        p(c_20) = [2] x1 + [1]                  
                        p(c_21) = [0]                           
                        p(c_22) = [4] x1 + [1] x2 + [2] x3 + [0]
                        p(c_23) = [4] x2 + [1]                  
                        p(c_24) = [1] x1 + [0]                  
                        p(c_25) = [1] x1 + [0]                  
                        p(c_26) = [2]                           
                        p(c_27) = [1]                           
                        p(c_28) = [1] x1 + [0]                  
                        p(c_29) = [4] x1 + [4]                  
                        p(c_30) = [1]                           
                        p(c_31) = [0]                           
          
          Following rules are strictly oriented:
          insert#(x,l) = [1] l + [1]         
                       > [1] l + [0]         
                       = c_24(insert'1#(l,x))
          
          
          Following rules are (at-least) weakly oriented:
                      append#(l1,l2) =  [1] l1 + [1] l2 + [0]                     
                                     >= [1] l1 + [1] l2 + [0]                     
                                     =  c_17(append'1#(l1,l2))                    
          
              append'1#(dd(x,xs),l2) =  [1] l2 + [1] xs + [1]                     
                                     >= [1] l2 + [1] xs + [1]                     
                                     =  c_18(append#(xs,l2))                      
          
                         flatten#(t) =  [4] t + [0]                               
                                     >= [4] t + [0]                               
                                     =  flatten'1#(t)                             
          
           flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [8]             
                                     >= [1] l + [1] t1 + [1] t2 + [2]             
                                     =  append#(l,append(flatten(t1),flatten(t2)))
          
           flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [8]             
                                     >= [1] t1 + [1] t2 + [2]                     
                                     =  append#(flatten(t1),flatten(t2))          
          
           flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [8]             
                                     >= [4] t1 + [0]                              
                                     =  flatten#(t1)                              
          
           flatten'1#(node(l,t1,t2)) =  [4] l + [4] t1 + [4] t2 + [8]             
                                     >= [4] t2 + [0]                              
                                     =  flatten#(t2)                              
          
                     flattensort#(t) =  [1] t + [5]                               
                                     >= [1] t + [5]                               
                                     =  insertionsort#(flatten(t))                
          
               insert'1#(dd(y,ys),x) =  [1] ys + [1]                              
                                     >= [1] ys + [1]                              
                                     =  c_25(insert'2#('less(y,x),x,y,ys))        
          
           insert'2#('true(),x,y,ys) =  [1] ys + [1]                              
                                     >= [1] ys + [1]                              
                                     =  c_28(insert#(x,ys))                       
          
                   insertionsort#(l) =  [1] l + [4]                               
                                     >= [1] l + [4]                               
                                     =  insertionsort'1#(l)                       
          
          insertionsort'1#(dd(x,xs)) =  [1] xs + [5]                              
                                     >= [1] xs + [5]                              
                                     =  insert#(x,insertionsort(xs))              
          
          insertionsort'1#(dd(x,xs)) =  [1] xs + [5]                              
                                     >= [1] xs + [4]                              
                                     =  insertionsort#(xs)                        
          
                        'cklt('EQ()) =  [0]                                       
                                     >= [0]                                       
                                     =  'false()                                  
          
                        'cklt('GT()) =  [0]                                       
                                     >= [0]                                       
                                     =  'false()                                  
          
                        'cklt('LT()) =  [0]                                       
                                     >= [0]                                       
                                     =  'true()                                   
          
                 'compare('0(),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'EQ()                                     
          
              'compare('0(),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
              'compare('0(),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
                'compare('0(),'s(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
              'compare('neg(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
           'compare('neg(x),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(y,x)                             
          
           'compare('neg(x),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'LT()                                     
          
              'compare('pos(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
           'compare('pos(x),'neg(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
           'compare('pos(x),'pos(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(x,y)                             
          
                'compare('s(x),'0()) =  [0]                                       
                                     >= [0]                                       
                                     =  'GT()                                     
          
               'compare('s(x),'s(y)) =  [0]                                       
                                     >= [0]                                       
                                     =  'compare(x,y)                             
          
                          'less(x,y) =  [0]                                       
                                     >= [0]                                       
                                     =  'cklt('compare(x,y))                      
          
                       append(l1,l2) =  [1] l1 + [1] l2 + [0]                     
                                     >= [1] l1 + [1] l2 + [0]                     
                                     =  append'1(l1,l2)                           
          
               append'1(dd(x,xs),l2) =  [1] l2 + [1] xs + [1]                     
                                     >= [1] l2 + [1] xs + [1]                     
                                     =  dd(x,append(xs,l2))                       
          
                  append'1(nil(),l2) =  [1] l2 + [0]                              
                                     >= [1] l2 + [0]                              
                                     =  l2                                        
          
                          flatten(t) =  [1] t + [1]                               
                                     >= [1] t + [1]                               
                                     =  flatten'1(t)                              
          
                   flatten'1(leaf()) =  [1]                                       
                                     >= [0]                                       
                                     =  nil()                                     
          
            flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [3]             
                                     >= [1] l + [1] t1 + [1] t2 + [2]             
                                     =  append(l,append(flatten(t1),flatten(t2))) 
          
                         insert(x,l) =  [1] l + [1]                               
                                     >= [1] l + [1]                               
                                     =  insert'1(l,x)                             
          
                insert'1(dd(y,ys),x) =  [1] ys + [2]                              
                                     >= [1] ys + [2]                              
                                     =  insert'2('less(y,x),x,y,ys)               
          
                   insert'1(nil(),x) =  [1]                                       
                                     >= [1]                                       
                                     =  dd(x,nil())                               
          
           insert'2('false(),x,y,ys) =  [1] ys + [2]                              
                                     >= [1] ys + [2]                              
                                     =  dd(x,dd(y,ys))                            
          
            insert'2('true(),x,y,ys) =  [1] ys + [2]                              
                                     >= [1] ys + [2]                              
                                     =  dd(y,insert(x,ys))                        
          
                    insertionsort(l) =  [1] l + [4]                               
                                     >= [1] l + [4]                               
                                     =  insertionsort'1(l)                        
          
           insertionsort'1(dd(x,xs)) =  [1] xs + [5]                              
                                     >= [1] xs + [5]                              
                                     =  insert(x,insertionsort(xs))               
          
              insertionsort'1(nil()) =  [4]                                       
                                     >= [0]                                       
                                     =  nil()                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.a:7: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            append#(l1,l2) -> c_17(append'1#(l1,l2))
            append'1#(dd(x,xs),l2) -> c_18(append#(xs,l2))
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> insertionsort#(flatten(t))
            insert#(x,l) -> c_24(insert'1#(l,x))
            insert'1#(dd(y,ys),x) -> c_25(insert'2#('less(y,x),x,y,ys))
            insert'2#('true(),x,y,ys) -> c_28(insert#(x,ys))
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

*** Step 6.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
        - Weak DPs:
            append#(l1,l2) -> append'1#(l1,l2)
            append'1#(dd(x,xs),l2) -> append#(xs,l2)
            flatten#(t) -> flatten'1#(t)
            flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
            flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
            flatten'1#(node(l,t1,t2)) -> flatten#(t1)
            flatten'1#(node(l,t1,t2)) -> flatten#(t2)
            flattensort#(t) -> flatten#(t)
            flattensort#(t) -> insertionsort#(flatten(t))
            insert#(x,l) -> insert'1#(l,x)
            insert'1#(dd(y,ys),x) -> 'less#(y,x)
            insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
            insert'2#('true(),x,y,ys) -> insert#(x,ys)
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          2:S:'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          3:S:'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          4:S:'less#(x,y) -> c_16('compare#(x,y))
             -->_1 'compare#('s(x),'s(y)) -> c_15('compare#(x,y)):3
             -->_1 'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y)):2
             -->_1 'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x)):1
          
          5:W:append#(l1,l2) -> append'1#(l1,l2)
             -->_1 append'1#(dd(x,xs),l2) -> append#(xs,l2):6
          
          6:W:append'1#(dd(x,xs),l2) -> append#(xs,l2)
             -->_1 append#(l1,l2) -> append'1#(l1,l2):5
          
          7:W:flatten#(t) -> flatten'1#(t)
             -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t2):11
             -->_1 flatten'1#(node(l,t1,t2)) -> flatten#(t1):10
             -->_1 flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2)):9
             -->_1 flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2))):8
          
          8:W:flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
             -->_1 append#(l1,l2) -> append'1#(l1,l2):5
          
          9:W:flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
             -->_1 append#(l1,l2) -> append'1#(l1,l2):5
          
          10:W:flatten'1#(node(l,t1,t2)) -> flatten#(t1)
             -->_1 flatten#(t) -> flatten'1#(t):7
          
          11:W:flatten'1#(node(l,t1,t2)) -> flatten#(t2)
             -->_1 flatten#(t) -> flatten'1#(t):7
          
          12:W:flattensort#(t) -> flatten#(t)
             -->_1 flatten#(t) -> flatten'1#(t):7
          
          13:W:flattensort#(t) -> insertionsort#(flatten(t))
             -->_1 insertionsort#(l) -> insertionsort'1#(l):18
          
          14:W:insert#(x,l) -> insert'1#(l,x)
             -->_1 insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys):16
             -->_1 insert'1#(dd(y,ys),x) -> 'less#(y,x):15
          
          15:W:insert'1#(dd(y,ys),x) -> 'less#(y,x)
             -->_1 'less#(x,y) -> c_16('compare#(x,y)):4
          
          16:W:insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
             -->_1 insert'2#('true(),x,y,ys) -> insert#(x,ys):17
          
          17:W:insert'2#('true(),x,y,ys) -> insert#(x,ys)
             -->_1 insert#(x,l) -> insert'1#(l,x):14
          
          18:W:insertionsort#(l) -> insertionsort'1#(l)
             -->_1 insertionsort'1#(dd(x,xs)) -> insertionsort#(xs):20
             -->_1 insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):19
          
          19:W:insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
             -->_1 insert#(x,l) -> insert'1#(l,x):14
          
          20:W:insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
             -->_1 insertionsort#(l) -> insertionsort'1#(l):18
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          12: flattensort#(t) -> flatten#(t)
          7: flatten#(t) -> flatten'1#(t)
          11: flatten'1#(node(l,t1,t2)) -> flatten#(t2)
          10: flatten'1#(node(l,t1,t2)) -> flatten#(t1)
          8: flatten'1#(node(l,t1,t2)) -> append#(l,append(flatten(t1),flatten(t2)))
          9: flatten'1#(node(l,t1,t2)) -> append#(flatten(t1),flatten(t2))
          5: append#(l1,l2) -> append'1#(l1,l2)
          6: append'1#(dd(x,xs),l2) -> append#(xs,l2)
*** Step 6.b:1.b:2: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
        - Weak DPs:
            flattensort#(t) -> insertionsort#(flatten(t))
            insert#(x,l) -> insert'1#(l,x)
            insert'1#(dd(y,ys),x) -> 'less#(y,x)
            insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
            insert'2#('true(),x,y,ys) -> insert#(x,ys)
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_9) = {1},
          uargs(c_13) = {1},
          uargs(c_15) = {1},
          uargs(c_16) = {1}
        
        Following symbols are considered usable:
          {'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2#
          ,insertionsort#,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [1]                           
                       p('EQ) = [0]                           
                       p('GT) = [0]                           
                       p('LT) = [4]                           
                     p('cklt) = [1] x1 + [0]                  
                  p('compare) = [3]                           
                    p('false) = [2]                           
                     p('less) = [0]                           
                      p('neg) = [1] x1 + [0]                  
                      p('pos) = [1] x1 + [0]                  
                        p('s) = [0]                           
                     p('true) = [0]                           
                    p(append) = [0]                           
                  p(append'1) = [0]                           
                        p(dd) = [0]                           
                   p(flatten) = [1]                           
                 p(flatten'1) = [0]                           
               p(flattensort) = [0]                           
                    p(insert) = [2] x2 + [0]                  
                  p(insert'1) = [1] x2 + [0]                  
                  p(insert'2) = [2] x3 + [1]                  
             p(insertionsort) = [2]                           
           p(insertionsort'1) = [0]                           
                      p(leaf) = [0]                           
                       p(nil) = [0]                           
                      p(node) = [0]                           
                    p('cklt#) = [0]                           
                 p('compare#) = [0]                           
                    p('less#) = [1]                           
                   p(append#) = [1] x1 + [0]                  
                 p(append'1#) = [0]                           
                  p(flatten#) = [1] x1 + [0]                  
                p(flatten'1#) = [1] x1 + [0]                  
              p(flattensort#) = [5]                           
                   p(insert#) = [1]                           
                 p(insert'1#) = [1]                           
                 p(insert'2#) = [1]                           
            p(insertionsort#) = [5]                           
          p(insertionsort'1#) = [5]                           
                       p(c_1) = [0]                           
                       p(c_2) = [1]                           
                       p(c_3) = [0]                           
                       p(c_4) = [1]                           
                       p(c_5) = [0]                           
                       p(c_6) = [1]                           
                       p(c_7) = [0]                           
                       p(c_8) = [0]                           
                       p(c_9) = [4] x1 + [0]                  
                      p(c_10) = [1]                           
                      p(c_11) = [1]                           
                      p(c_12) = [1]                           
                      p(c_13) = [2] x1 + [0]                  
                      p(c_14) = [0]                           
                      p(c_15) = [1] x1 + [0]                  
                      p(c_16) = [4] x1 + [0]                  
                      p(c_17) = [1] x1 + [0]                  
                      p(c_18) = [2]                           
                      p(c_19) = [1]                           
                      p(c_20) = [2]                           
                      p(c_21) = [0]                           
                      p(c_22) = [1] x1 + [1] x2 + [1] x3 + [0]
                      p(c_23) = [0]                           
                      p(c_24) = [4] x1 + [0]                  
                      p(c_25) = [0]                           
                      p(c_26) = [0]                           
                      p(c_27) = [4]                           
                      p(c_28) = [2] x1 + [1]                  
                      p(c_29) = [0]                           
                      p(c_30) = [2] x1 + [1] x2 + [0]         
                      p(c_31) = [0]                           
        
        Following rules are strictly oriented:
        'less#(x,y) = [1]                 
                    > [0]                 
                    = c_16('compare#(x,y))
        
        
        Following rules are (at-least) weakly oriented:
        'compare#('neg(x),'neg(y)) =  [0]                         
                                   >= [0]                         
                                   =  c_9('compare#(y,x))         
        
        'compare#('pos(x),'pos(y)) =  [0]                         
                                   >= [0]                         
                                   =  c_13('compare#(x,y))        
        
            'compare#('s(x),'s(y)) =  [0]                         
                                   >= [0]                         
                                   =  c_15('compare#(x,y))        
        
                   flattensort#(t) =  [5]                         
                                   >= [5]                         
                                   =  insertionsort#(flatten(t))  
        
                      insert#(x,l) =  [1]                         
                                   >= [1]                         
                                   =  insert'1#(l,x)              
        
             insert'1#(dd(y,ys),x) =  [1]                         
                                   >= [1]                         
                                   =  'less#(y,x)                 
        
             insert'1#(dd(y,ys),x) =  [1]                         
                                   >= [1]                         
                                   =  insert'2#('less(y,x),x,y,ys)
        
         insert'2#('true(),x,y,ys) =  [1]                         
                                   >= [1]                         
                                   =  insert#(x,ys)               
        
                 insertionsort#(l) =  [5]                         
                                   >= [5]                         
                                   =  insertionsort'1#(l)         
        
        insertionsort'1#(dd(x,xs)) =  [5]                         
                                   >= [1]                         
                                   =  insert#(x,insertionsort(xs))
        
        insertionsort'1#(dd(x,xs)) =  [5]                         
                                   >= [5]                         
                                   =  insertionsort#(xs)          
        
*** Step 6.b:1.b:3: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
        - Weak DPs:
            'less#(x,y) -> c_16('compare#(x,y))
            flattensort#(t) -> insertionsort#(flatten(t))
            insert#(x,l) -> insert'1#(l,x)
            insert'1#(dd(y,ys),x) -> 'less#(y,x)
            insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
            insert'2#('true(),x,y,ys) -> insert#(x,ys)
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_9) = {1},
          uargs(c_13) = {1},
          uargs(c_15) = {1},
          uargs(c_16) = {1}
        
        Following symbols are considered usable:
          {'cklt,'less,append,append'1,flatten,flatten'1,insert,insert'1,insert'2,insertionsort,insertionsort'1
          ,'cklt#,'compare#,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2#
          ,insertionsort#,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [0]                                    
                       p('EQ) = [0]                                    
                       p('GT) = [0]                                    
                       p('LT) = [0]                                    
                     p('cklt) = [0]                                    
                  p('compare) = [0]                                    
                    p('false) = [0]                                    
                     p('less) = [0]                                    
                      p('neg) = [1] x1 + [0]                           
                      p('pos) = [1] x1 + [0]                           
                        p('s) = [1] x1 + [1]                           
                     p('true) = [0]                                    
                    p(append) = [1] x1 + [1] x2 + [0]                  
                  p(append'1) = [1] x1 + [1] x2 + [0]                  
                        p(dd) = [1] x1 + [1] x2 + [1]                  
                   p(flatten) = [1] x1 + [0]                           
                 p(flatten'1) = [1] x1 + [0]                           
               p(flattensort) = [1] x1 + [1]                           
                    p(insert) = [1] x1 + [1] x2 + [1]                  
                  p(insert'1) = [1] x1 + [1] x2 + [1]                  
                  p(insert'2) = [1] x2 + [1] x3 + [1] x4 + [2]         
             p(insertionsort) = [1] x1 + [2]                           
           p(insertionsort'1) = [1] x1 + [2]                           
                      p(leaf) = [0]                                    
                       p(nil) = [0]                                    
                      p(node) = [1] x1 + [1] x2 + [1] x3 + [4]         
                    p('cklt#) = [2] x1 + [0]                           
                 p('compare#) = [1] x1 + [1] x2 + [0]                  
                    p('less#) = [1] x1 + [1] x2 + [5]                  
                   p(append#) = [2] x2 + [2]                           
                 p(append'1#) = [1] x2 + [0]                           
                  p(flatten#) = [2] x1 + [2]                           
                p(flatten'1#) = [0]                                    
              p(flattensort#) = [1] x1 + [7]                           
                   p(insert#) = [1] x1 + [1] x2 + [6]                  
                 p(insert'1#) = [1] x1 + [1] x2 + [6]                  
                 p(insert'2#) = [2] x1 + [1] x2 + [1] x3 + [1] x4 + [6]
            p(insertionsort#) = [1] x1 + [7]                           
          p(insertionsort'1#) = [1] x1 + [7]                           
                       p(c_1) = [2]                                    
                       p(c_2) = [0]                                    
                       p(c_3) = [1]                                    
                       p(c_4) = [4]                                    
                       p(c_5) = [4]                                    
                       p(c_6) = [1]                                    
                       p(c_7) = [4]                                    
                       p(c_8) = [1]                                    
                       p(c_9) = [1] x1 + [0]                           
                      p(c_10) = [1]                                    
                      p(c_11) = [2]                                    
                      p(c_12) = [1]                                    
                      p(c_13) = [1] x1 + [0]                           
                      p(c_14) = [2]                                    
                      p(c_15) = [1] x1 + [0]                           
                      p(c_16) = [1] x1 + [0]                           
                      p(c_17) = [1] x1 + [1]                           
                      p(c_18) = [1] x1 + [1]                           
                      p(c_19) = [2]                                    
                      p(c_20) = [1] x1 + [1]                           
                      p(c_21) = [4]                                    
                      p(c_22) = [1] x1 + [0]                           
                      p(c_23) = [0]                                    
                      p(c_24) = [0]                                    
                      p(c_25) = [2] x1 + [2]                           
                      p(c_26) = [0]                                    
                      p(c_27) = [4]                                    
                      p(c_28) = [0]                                    
                      p(c_29) = [0]                                    
                      p(c_30) = [1] x1 + [1]                           
                      p(c_31) = [0]                                    
        
        Following rules are strictly oriented:
        'compare#('s(x),'s(y)) = [1] x + [1] y + [2] 
                               > [1] x + [1] y + [0] 
                               = c_15('compare#(x,y))
        
        
        Following rules are (at-least) weakly oriented:
        'compare#('neg(x),'neg(y)) =  [1] x + [1] y + [0]                      
                                   >= [1] x + [1] y + [0]                      
                                   =  c_9('compare#(y,x))                      
        
        'compare#('pos(x),'pos(y)) =  [1] x + [1] y + [0]                      
                                   >= [1] x + [1] y + [0]                      
                                   =  c_13('compare#(x,y))                     
        
                       'less#(x,y) =  [1] x + [1] y + [5]                      
                                   >= [1] x + [1] y + [0]                      
                                   =  c_16('compare#(x,y))                     
        
                   flattensort#(t) =  [1] t + [7]                              
                                   >= [1] t + [7]                              
                                   =  insertionsort#(flatten(t))               
        
                      insert#(x,l) =  [1] l + [1] x + [6]                      
                                   >= [1] l + [1] x + [6]                      
                                   =  insert'1#(l,x)                           
        
             insert'1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [7]             
                                   >= [1] x + [1] y + [5]                      
                                   =  'less#(y,x)                              
        
             insert'1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [7]             
                                   >= [1] x + [1] y + [1] ys + [6]             
                                   =  insert'2#('less(y,x),x,y,ys)             
        
         insert'2#('true(),x,y,ys) =  [1] x + [1] y + [1] ys + [6]             
                                   >= [1] x + [1] ys + [6]                     
                                   =  insert#(x,ys)                            
        
                 insertionsort#(l) =  [1] l + [7]                              
                                   >= [1] l + [7]                              
                                   =  insertionsort'1#(l)                      
        
        insertionsort'1#(dd(x,xs)) =  [1] x + [1] xs + [8]                     
                                   >= [1] x + [1] xs + [8]                     
                                   =  insert#(x,insertionsort(xs))             
        
        insertionsort'1#(dd(x,xs)) =  [1] x + [1] xs + [8]                     
                                   >= [1] xs + [7]                             
                                   =  insertionsort#(xs)                       
        
                      'cklt('EQ()) =  [0]                                      
                                   >= [0]                                      
                                   =  'false()                                 
        
                      'cklt('GT()) =  [0]                                      
                                   >= [0]                                      
                                   =  'false()                                 
        
                      'cklt('LT()) =  [0]                                      
                                   >= [0]                                      
                                   =  'true()                                  
        
                        'less(x,y) =  [0]                                      
                                   >= [0]                                      
                                   =  'cklt('compare(x,y))                     
        
                     append(l1,l2) =  [1] l1 + [1] l2 + [0]                    
                                   >= [1] l1 + [1] l2 + [0]                    
                                   =  append'1(l1,l2)                          
        
             append'1(dd(x,xs),l2) =  [1] l2 + [1] x + [1] xs + [1]            
                                   >= [1] l2 + [1] x + [1] xs + [1]            
                                   =  dd(x,append(xs,l2))                      
        
                append'1(nil(),l2) =  [1] l2 + [0]                             
                                   >= [1] l2 + [0]                             
                                   =  l2                                       
        
                        flatten(t) =  [1] t + [0]                              
                                   >= [1] t + [0]                              
                                   =  flatten'1(t)                             
        
                 flatten'1(leaf()) =  [0]                                      
                                   >= [0]                                      
                                   =  nil()                                    
        
          flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [4]            
                                   >= [1] l + [1] t1 + [1] t2 + [0]            
                                   =  append(l,append(flatten(t1),flatten(t2)))
        
                       insert(x,l) =  [1] l + [1] x + [1]                      
                                   >= [1] l + [1] x + [1]                      
                                   =  insert'1(l,x)                            
        
              insert'1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [2]             
                                   >= [1] x + [1] y + [1] ys + [2]             
                                   =  insert'2('less(y,x),x,y,ys)              
        
                 insert'1(nil(),x) =  [1] x + [1]                              
                                   >= [1] x + [1]                              
                                   =  dd(x,nil())                              
        
         insert'2('false(),x,y,ys) =  [1] x + [1] y + [1] ys + [2]             
                                   >= [1] x + [1] y + [1] ys + [2]             
                                   =  dd(x,dd(y,ys))                           
        
          insert'2('true(),x,y,ys) =  [1] x + [1] y + [1] ys + [2]             
                                   >= [1] x + [1] y + [1] ys + [2]             
                                   =  dd(y,insert(x,ys))                       
        
                  insertionsort(l) =  [1] l + [2]                              
                                   >= [1] l + [2]                              
                                   =  insertionsort'1(l)                       
        
         insertionsort'1(dd(x,xs)) =  [1] x + [1] xs + [3]                     
                                   >= [1] x + [1] xs + [3]                     
                                   =  insert(x,insertionsort(xs))              
        
            insertionsort'1(nil()) =  [2]                                      
                                   >= [0]                                      
                                   =  nil()                                    
        
*** Step 6.b:1.b:4: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
        - Weak DPs:
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
            flattensort#(t) -> insertionsort#(flatten(t))
            insert#(x,l) -> insert'1#(l,x)
            insert'1#(dd(y,ys),x) -> 'less#(y,x)
            insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
            insert'2#('true(),x,y,ys) -> insert#(x,ys)
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_9) = {1},
          uargs(c_13) = {1},
          uargs(c_15) = {1},
          uargs(c_16) = {1}
        
        Following symbols are considered usable:
          {append,append'1,flatten,flatten'1,insert,insert'1,insert'2,insertionsort,insertionsort'1,'cklt#,'compare#
          ,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#
          ,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [0]                           
                       p('EQ) = [3]                           
                       p('GT) = [3]                           
                       p('LT) = [1]                           
                     p('cklt) = [5] x1 + [0]                  
                  p('compare) = [3]                           
                    p('false) = [2]                           
                     p('less) = [0]                           
                      p('neg) = [1] x1 + [0]                  
                      p('pos) = [1] x1 + [1]                  
                        p('s) = [1] x1 + [4]                  
                     p('true) = [1]                           
                    p(append) = [1] x1 + [1] x2 + [3]         
                  p(append'1) = [1] x1 + [1] x2 + [3]         
                        p(dd) = [1] x1 + [1] x2 + [1]         
                   p(flatten) = [1] x1 + [0]                  
                 p(flatten'1) = [1] x1 + [0]                  
               p(flattensort) = [0]                           
                    p(insert) = [1] x1 + [1] x2 + [1]         
                  p(insert'1) = [1] x1 + [1] x2 + [1]         
                  p(insert'2) = [1] x2 + [1] x3 + [1] x4 + [2]
             p(insertionsort) = [1] x1 + [0]                  
           p(insertionsort'1) = [1] x1 + [0]                  
                      p(leaf) = [4]                           
                       p(nil) = [4]                           
                      p(node) = [1] x1 + [1] x2 + [1] x3 + [6]
                    p('cklt#) = [4] x1 + [0]                  
                 p('compare#) = [1] x1 + [1] x2 + [0]         
                    p('less#) = [2] x1 + [2] x2 + [2]         
                   p(append#) = [1] x1 + [1] x2 + [1]         
                 p(append'1#) = [1] x1 + [2]                  
                  p(flatten#) = [4]                           
                p(flatten'1#) = [4]                           
              p(flattensort#) = [3] x1 + [4]                  
                   p(insert#) = [2] x1 + [2] x2 + [2]         
                 p(insert'1#) = [2] x1 + [2] x2 + [2]         
                 p(insert'2#) = [2] x2 + [1] x3 + [2] x4 + [4]
            p(insertionsort#) = [2] x1 + [4]                  
          p(insertionsort'1#) = [2] x1 + [2]                  
                       p(c_1) = [1]                           
                       p(c_2) = [2]                           
                       p(c_3) = [1]                           
                       p(c_4) = [0]                           
                       p(c_5) = [2]                           
                       p(c_6) = [0]                           
                       p(c_7) = [0]                           
                       p(c_8) = [1]                           
                       p(c_9) = [1] x1 + [0]                  
                      p(c_10) = [0]                           
                      p(c_11) = [2]                           
                      p(c_12) = [4]                           
                      p(c_13) = [1] x1 + [0]                  
                      p(c_14) = [0]                           
                      p(c_15) = [1] x1 + [5]                  
                      p(c_16) = [2] x1 + [2]                  
                      p(c_17) = [1]                           
                      p(c_18) = [1]                           
                      p(c_19) = [0]                           
                      p(c_20) = [1] x1 + [1]                  
                      p(c_21) = [0]                           
                      p(c_22) = [1] x3 + [1]                  
                      p(c_23) = [2] x1 + [1]                  
                      p(c_24) = [4] x1 + [1]                  
                      p(c_25) = [1] x1 + [4]                  
                      p(c_26) = [2]                           
                      p(c_27) = [2]                           
                      p(c_28) = [1] x1 + [0]                  
                      p(c_29) = [1]                           
                      p(c_30) = [1] x2 + [1]                  
                      p(c_31) = [0]                           
        
        Following rules are strictly oriented:
        'compare#('pos(x),'pos(y)) = [1] x + [1] y + [2] 
                                   > [1] x + [1] y + [0] 
                                   = c_13('compare#(x,y))
        
        
        Following rules are (at-least) weakly oriented:
        'compare#('neg(x),'neg(y)) =  [1] x + [1] y + [0]                      
                                   >= [1] x + [1] y + [0]                      
                                   =  c_9('compare#(y,x))                      
        
            'compare#('s(x),'s(y)) =  [1] x + [1] y + [8]                      
                                   >= [1] x + [1] y + [5]                      
                                   =  c_15('compare#(x,y))                     
        
                       'less#(x,y) =  [2] x + [2] y + [2]                      
                                   >= [2] x + [2] y + [2]                      
                                   =  c_16('compare#(x,y))                     
        
                   flattensort#(t) =  [3] t + [4]                              
                                   >= [2] t + [4]                              
                                   =  insertionsort#(flatten(t))               
        
                      insert#(x,l) =  [2] l + [2] x + [2]                      
                                   >= [2] l + [2] x + [2]                      
                                   =  insert'1#(l,x)                           
        
             insert'1#(dd(y,ys),x) =  [2] x + [2] y + [2] ys + [4]             
                                   >= [2] x + [2] y + [2]                      
                                   =  'less#(y,x)                              
        
             insert'1#(dd(y,ys),x) =  [2] x + [2] y + [2] ys + [4]             
                                   >= [2] x + [1] y + [2] ys + [4]             
                                   =  insert'2#('less(y,x),x,y,ys)             
        
         insert'2#('true(),x,y,ys) =  [2] x + [1] y + [2] ys + [4]             
                                   >= [2] x + [2] ys + [2]                     
                                   =  insert#(x,ys)                            
        
                 insertionsort#(l) =  [2] l + [4]                              
                                   >= [2] l + [2]                              
                                   =  insertionsort'1#(l)                      
        
        insertionsort'1#(dd(x,xs)) =  [2] x + [2] xs + [4]                     
                                   >= [2] x + [2] xs + [2]                     
                                   =  insert#(x,insertionsort(xs))             
        
        insertionsort'1#(dd(x,xs)) =  [2] x + [2] xs + [4]                     
                                   >= [2] xs + [4]                             
                                   =  insertionsort#(xs)                       
        
                     append(l1,l2) =  [1] l1 + [1] l2 + [3]                    
                                   >= [1] l1 + [1] l2 + [3]                    
                                   =  append'1(l1,l2)                          
        
             append'1(dd(x,xs),l2) =  [1] l2 + [1] x + [1] xs + [4]            
                                   >= [1] l2 + [1] x + [1] xs + [4]            
                                   =  dd(x,append(xs,l2))                      
        
                append'1(nil(),l2) =  [1] l2 + [7]                             
                                   >= [1] l2 + [0]                             
                                   =  l2                                       
        
                        flatten(t) =  [1] t + [0]                              
                                   >= [1] t + [0]                              
                                   =  flatten'1(t)                             
        
                 flatten'1(leaf()) =  [4]                                      
                                   >= [4]                                      
                                   =  nil()                                    
        
          flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [6]            
                                   >= [1] l + [1] t1 + [1] t2 + [6]            
                                   =  append(l,append(flatten(t1),flatten(t2)))
        
                       insert(x,l) =  [1] l + [1] x + [1]                      
                                   >= [1] l + [1] x + [1]                      
                                   =  insert'1(l,x)                            
        
              insert'1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [2]             
                                   >= [1] x + [1] y + [1] ys + [2]             
                                   =  insert'2('less(y,x),x,y,ys)              
        
                 insert'1(nil(),x) =  [1] x + [5]                              
                                   >= [1] x + [5]                              
                                   =  dd(x,nil())                              
        
         insert'2('false(),x,y,ys) =  [1] x + [1] y + [1] ys + [2]             
                                   >= [1] x + [1] y + [1] ys + [2]             
                                   =  dd(x,dd(y,ys))                           
        
          insert'2('true(),x,y,ys) =  [1] x + [1] y + [1] ys + [2]             
                                   >= [1] x + [1] y + [1] ys + [2]             
                                   =  dd(y,insert(x,ys))                       
        
                  insertionsort(l) =  [1] l + [0]                              
                                   >= [1] l + [0]                              
                                   =  insertionsort'1(l)                       
        
         insertionsort'1(dd(x,xs)) =  [1] x + [1] xs + [1]                     
                                   >= [1] x + [1] xs + [1]                     
                                   =  insert(x,insertionsort(xs))              
        
            insertionsort'1(nil()) =  [4]                                      
                                   >= [4]                                      
                                   =  nil()                                    
        
*** Step 6.b:1.b:5: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
        - Weak DPs:
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
            flattensort#(t) -> insertionsort#(flatten(t))
            insert#(x,l) -> insert'1#(l,x)
            insert'1#(dd(y,ys),x) -> 'less#(y,x)
            insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
            insert'2#('true(),x,y,ys) -> insert#(x,ys)
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_9) = {1},
          uargs(c_13) = {1},
          uargs(c_15) = {1},
          uargs(c_16) = {1}
        
        Following symbols are considered usable:
          {append,append'1,flatten,flatten'1,insert,insert'1,insert'2,insertionsort,insertionsort'1,'cklt#,'compare#
          ,'less#,append#,append'1#,flatten#,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#
          ,insertionsort'1#}
        TcT has computed the following interpretation:
                        p('0) = [4]                           
                       p('EQ) = [1]                           
                       p('GT) = [2]                           
                       p('LT) = [0]                           
                     p('cklt) = [6]                           
                  p('compare) = [0]                           
                    p('false) = [4]                           
                     p('less) = [2] x1 + [0]                  
                      p('neg) = [1] x1 + [4]                  
                      p('pos) = [1] x1 + [0]                  
                        p('s) = [1] x1 + [0]                  
                     p('true) = [0]                           
                    p(append) = [1] x1 + [1] x2 + [0]         
                  p(append'1) = [1] x1 + [1] x2 + [0]         
                        p(dd) = [1] x1 + [1] x2 + [0]         
                   p(flatten) = [1] x1 + [0]                  
                 p(flatten'1) = [1] x1 + [0]                  
               p(flattensort) = [1] x1 + [1]                  
                    p(insert) = [1] x1 + [1] x2 + [0]         
                  p(insert'1) = [1] x1 + [1] x2 + [0]         
                  p(insert'2) = [1] x2 + [1] x3 + [1] x4 + [0]
             p(insertionsort) = [1] x1 + [0]                  
           p(insertionsort'1) = [1] x1 + [0]                  
                      p(leaf) = [4]                           
                       p(nil) = [2]                           
                      p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
                    p('cklt#) = [4] x1 + [0]                  
                 p('compare#) = [1] x1 + [1] x2 + [0]         
                    p('less#) = [2] x1 + [2] x2 + [0]         
                   p(append#) = [2] x1 + [1] x2 + [0]         
                 p(append'1#) = [1] x2 + [0]                  
                  p(flatten#) = [1] x1 + [1]                  
                p(flatten'1#) = [1] x1 + [0]                  
              p(flattensort#) = [4] x1 + [0]                  
                   p(insert#) = [2] x1 + [2] x2 + [0]         
                 p(insert'1#) = [2] x1 + [2] x2 + [0]         
                 p(insert'2#) = [2] x2 + [2] x4 + [0]         
            p(insertionsort#) = [3] x1 + [0]                  
          p(insertionsort'1#) = [3] x1 + [0]                  
                       p(c_1) = [1]                           
                       p(c_2) = [2]                           
                       p(c_3) = [0]                           
                       p(c_4) = [1]                           
                       p(c_5) = [1]                           
                       p(c_6) = [0]                           
                       p(c_7) = [1]                           
                       p(c_8) = [0]                           
                       p(c_9) = [1] x1 + [0]                  
                      p(c_10) = [2]                           
                      p(c_11) = [0]                           
                      p(c_12) = [2]                           
                      p(c_13) = [1] x1 + [0]                  
                      p(c_14) = [0]                           
                      p(c_15) = [1] x1 + [0]                  
                      p(c_16) = [2] x1 + [0]                  
                      p(c_17) = [4] x1 + [4]                  
                      p(c_18) = [1]                           
                      p(c_19) = [2]                           
                      p(c_20) = [1]                           
                      p(c_21) = [2]                           
                      p(c_22) = [1]                           
                      p(c_23) = [4] x1 + [1] x2 + [2]         
                      p(c_24) = [2] x1 + [0]                  
                      p(c_25) = [1] x1 + [1] x2 + [0]         
                      p(c_26) = [0]                           
                      p(c_27) = [1]                           
                      p(c_28) = [1] x1 + [4]                  
                      p(c_29) = [0]                           
                      p(c_30) = [4] x1 + [0]                  
                      p(c_31) = [0]                           
        
        Following rules are strictly oriented:
        'compare#('neg(x),'neg(y)) = [1] x + [1] y + [8]
                                   > [1] x + [1] y + [0]
                                   = c_9('compare#(y,x))
        
        
        Following rules are (at-least) weakly oriented:
        'compare#('pos(x),'pos(y)) =  [1] x + [1] y + [0]                      
                                   >= [1] x + [1] y + [0]                      
                                   =  c_13('compare#(x,y))                     
        
            'compare#('s(x),'s(y)) =  [1] x + [1] y + [0]                      
                                   >= [1] x + [1] y + [0]                      
                                   =  c_15('compare#(x,y))                     
        
                       'less#(x,y) =  [2] x + [2] y + [0]                      
                                   >= [2] x + [2] y + [0]                      
                                   =  c_16('compare#(x,y))                     
        
                   flattensort#(t) =  [4] t + [0]                              
                                   >= [3] t + [0]                              
                                   =  insertionsort#(flatten(t))               
        
                      insert#(x,l) =  [2] l + [2] x + [0]                      
                                   >= [2] l + [2] x + [0]                      
                                   =  insert'1#(l,x)                           
        
             insert'1#(dd(y,ys),x) =  [2] x + [2] y + [2] ys + [0]             
                                   >= [2] x + [2] y + [0]                      
                                   =  'less#(y,x)                              
        
             insert'1#(dd(y,ys),x) =  [2] x + [2] y + [2] ys + [0]             
                                   >= [2] x + [2] ys + [0]                     
                                   =  insert'2#('less(y,x),x,y,ys)             
        
         insert'2#('true(),x,y,ys) =  [2] x + [2] ys + [0]                     
                                   >= [2] x + [2] ys + [0]                     
                                   =  insert#(x,ys)                            
        
                 insertionsort#(l) =  [3] l + [0]                              
                                   >= [3] l + [0]                              
                                   =  insertionsort'1#(l)                      
        
        insertionsort'1#(dd(x,xs)) =  [3] x + [3] xs + [0]                     
                                   >= [2] x + [2] xs + [0]                     
                                   =  insert#(x,insertionsort(xs))             
        
        insertionsort'1#(dd(x,xs)) =  [3] x + [3] xs + [0]                     
                                   >= [3] xs + [0]                             
                                   =  insertionsort#(xs)                       
        
                     append(l1,l2) =  [1] l1 + [1] l2 + [0]                    
                                   >= [1] l1 + [1] l2 + [0]                    
                                   =  append'1(l1,l2)                          
        
             append'1(dd(x,xs),l2) =  [1] l2 + [1] x + [1] xs + [0]            
                                   >= [1] l2 + [1] x + [1] xs + [0]            
                                   =  dd(x,append(xs,l2))                      
        
                append'1(nil(),l2) =  [1] l2 + [2]                             
                                   >= [1] l2 + [0]                             
                                   =  l2                                       
        
                        flatten(t) =  [1] t + [0]                              
                                   >= [1] t + [0]                              
                                   =  flatten'1(t)                             
        
                 flatten'1(leaf()) =  [4]                                      
                                   >= [2]                                      
                                   =  nil()                                    
        
          flatten'1(node(l,t1,t2)) =  [1] l + [1] t1 + [1] t2 + [0]            
                                   >= [1] l + [1] t1 + [1] t2 + [0]            
                                   =  append(l,append(flatten(t1),flatten(t2)))
        
                       insert(x,l) =  [1] l + [1] x + [0]                      
                                   >= [1] l + [1] x + [0]                      
                                   =  insert'1(l,x)                            
        
              insert'1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]             
                                   >= [1] x + [1] y + [1] ys + [0]             
                                   =  insert'2('less(y,x),x,y,ys)              
        
                 insert'1(nil(),x) =  [1] x + [2]                              
                                   >= [1] x + [2]                              
                                   =  dd(x,nil())                              
        
         insert'2('false(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]             
                                   >= [1] x + [1] y + [1] ys + [0]             
                                   =  dd(x,dd(y,ys))                           
        
          insert'2('true(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]             
                                   >= [1] x + [1] y + [1] ys + [0]             
                                   =  dd(y,insert(x,ys))                       
        
                  insertionsort(l) =  [1] l + [0]                              
                                   >= [1] l + [0]                              
                                   =  insertionsort'1(l)                       
        
         insertionsort'1(dd(x,xs)) =  [1] x + [1] xs + [0]                     
                                   >= [1] x + [1] xs + [0]                     
                                   =  insert(x,insertionsort(xs))              
        
            insertionsort'1(nil()) =  [2]                                      
                                   >= [2]                                      
                                   =  nil()                                    
        
*** Step 6.b:1.b:6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            'compare#('neg(x),'neg(y)) -> c_9('compare#(y,x))
            'compare#('pos(x),'pos(y)) -> c_13('compare#(x,y))
            'compare#('s(x),'s(y)) -> c_15('compare#(x,y))
            'less#(x,y) -> c_16('compare#(x,y))
            flattensort#(t) -> insertionsort#(flatten(t))
            insert#(x,l) -> insert'1#(l,x)
            insert'1#(dd(y,ys),x) -> 'less#(y,x)
            insert'1#(dd(y,ys),x) -> insert'2#('less(y,x),x,y,ys)
            insert'2#('true(),x,y,ys) -> insert#(x,ys)
            insertionsort#(l) -> insertionsort'1#(l)
            insertionsort'1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort'1#(dd(x,xs)) -> insertionsort#(xs)
        - Weak TRS:
            'cklt('EQ()) -> 'false()
            'cklt('GT()) -> 'false()
            'cklt('LT()) -> 'true()
            'compare('0(),'0()) -> 'EQ()
            'compare('0(),'neg(y)) -> 'GT()
            'compare('0(),'pos(y)) -> 'LT()
            'compare('0(),'s(y)) -> 'LT()
            'compare('neg(x),'0()) -> 'LT()
            'compare('neg(x),'neg(y)) -> 'compare(y,x)
            'compare('neg(x),'pos(y)) -> 'LT()
            'compare('pos(x),'0()) -> 'GT()
            'compare('pos(x),'neg(y)) -> 'GT()
            'compare('pos(x),'pos(y)) -> 'compare(x,y)
            'compare('s(x),'0()) -> 'GT()
            'compare('s(x),'s(y)) -> 'compare(x,y)
            'less(x,y) -> 'cklt('compare(x,y))
            append(l1,l2) -> append'1(l1,l2)
            append'1(dd(x,xs),l2) -> dd(x,append(xs,l2))
            append'1(nil(),l2) -> l2
            flatten(t) -> flatten'1(t)
            flatten'1(leaf()) -> nil()
            flatten'1(node(l,t1,t2)) -> append(l,append(flatten(t1),flatten(t2)))
            insert(x,l) -> insert'1(l,x)
            insert'1(dd(y,ys),x) -> insert'2('less(y,x),x,y,ys)
            insert'1(nil(),x) -> dd(x,nil())
            insert'2('false(),x,y,ys) -> dd(x,dd(y,ys))
            insert'2('true(),x,y,ys) -> dd(y,insert(x,ys))
            insertionsort(l) -> insertionsort'1(l)
            insertionsort'1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort'1(nil()) -> nil()
        - Signature:
            {'cklt/1,'compare/2,'less/2,append/2,append'1/2,flatten/1,flatten'1/1,flattensort/1,insert/2,insert'1/2
            ,insert'2/4,insertionsort/1,insertionsort'1/1,'cklt#/1,'compare#/2,'less#/2,append#/2,append'1#/2,flatten#/1
            ,flatten'1#/1,flattensort#/1,insert#/2,insert'1#/2,insert'2#/4,insertionsort#/1,insertionsort'1#/1} / {'0/0
            ,'EQ/0,'GT/0,'LT/0,'false/0,'neg/1,'pos/1,'s/1,'true/0,dd/2,leaf/0,nil/0,node/3,c_1/0,c_2/0,c_3/0,c_4/0
            ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1
            ,c_21/0,c_22/4,c_23/2,c_24/1,c_25/2,c_26/0,c_27/0,c_28/1,c_29/1,c_30/2,c_31/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {'cklt#,'compare#,'less#,append#,append'1#,flatten#
            ,flatten'1#,flattensort#,insert#,insert'1#,insert'2#,insertionsort#,insertionsort'1#} and constructors {'0
            ,'EQ,'GT,'LT,'false,'neg,'pos,'s,'true,dd,leaf,nil,node}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))