WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            nub(@l) -> nub#1(@l)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
            ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
            ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          #equal#(@x,@y) -> c_1(#eq#(@x,@y))
          and#(@x,@y) -> c_2(#and#(@x,@y))
          eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
          eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
          eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
          eq#2#(::(@y,@ys)) -> c_6()
          eq#2#(nil()) -> c_7()
          eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
          eq#3#(nil(),@x,@xs) -> c_9()
          nub#(@l) -> c_10(nub#1#(@l))
          nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
          nub#1#(nil()) -> c_12()
          remove#(@x,@l) -> c_13(remove#1#(@l,@x))
          remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
          remove#1#(nil(),@x) -> c_15()
          remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
          remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        Weak DPs
          #and#(#false(),#false()) -> c_18()
          #and#(#false(),#true()) -> c_19()
          #and#(#true(),#false()) -> c_20()
          #and#(#true(),#true()) -> c_21()
          #eq#(#0(),#0()) -> c_22()
          #eq#(#0(),#neg(@y)) -> c_23()
          #eq#(#0(),#pos(@y)) -> c_24()
          #eq#(#0(),#s(@y)) -> c_25()
          #eq#(#neg(@x),#0()) -> c_26()
          #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
          #eq#(#neg(@x),#pos(@y)) -> c_28()
          #eq#(#pos(@x),#0()) -> c_29()
          #eq#(#pos(@x),#neg(@y)) -> c_30()
          #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
          #eq#(#s(@x),#0()) -> c_32()
          #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
          #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                   ,#eq#(@x_1,@y_1)
                                                   ,#eq#(@x_2,@y_2))
          #eq#(::(@x_1,@x_2),nil()) -> c_35()
          #eq#(nil(),::(@y_1,@y_2)) -> c_36()
          #eq#(nil(),nil()) -> c_37()
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            #equal#(@x,@y) -> c_1(#eq#(@x,@y))
            and#(@x,@y) -> c_2(#and#(@x,@y))
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
            eq#2#(::(@y,@ys)) -> c_6()
            eq#2#(nil()) -> c_7()
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
            eq#3#(nil(),@x,@xs) -> c_9()
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
            nub#1#(nil()) -> c_12()
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#1#(nil(),@x) -> c_15()
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak DPs:
            #and#(#false(),#false()) -> c_18()
            #and#(#false(),#true()) -> c_19()
            #and#(#true(),#false()) -> c_20()
            #and#(#true(),#true()) -> c_21()
            #eq#(#0(),#0()) -> c_22()
            #eq#(#0(),#neg(@y)) -> c_23()
            #eq#(#0(),#pos(@y)) -> c_24()
            #eq#(#0(),#s(@y)) -> c_25()
            #eq#(#neg(@x),#0()) -> c_26()
            #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
            #eq#(#neg(@x),#pos(@y)) -> c_28()
            #eq#(#pos(@x),#0()) -> c_29()
            #eq#(#pos(@x),#neg(@y)) -> c_30()
            #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
            #eq#(#s(@x),#0()) -> c_32()
            #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
            #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                     ,#eq#(@x_1,@y_1)
                                                     ,#eq#(@x_2,@y_2))
            #eq#(::(@x_1,@x_2),nil()) -> c_35()
            #eq#(nil(),::(@y_1,@y_2)) -> c_36()
            #eq#(nil(),nil()) -> c_37()
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            nub(@l) -> nub#1(@l)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,6,7,9,12,15}
        by application of
          Pre({1,2,6,7,9,12,15}) = {4,5,8,10,13}.
        Here rules are labelled as follows:
          1: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
          2: and#(@x,@y) -> c_2(#and#(@x,@y))
          3: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
          4: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
          5: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
          6: eq#2#(::(@y,@ys)) -> c_6()
          7: eq#2#(nil()) -> c_7()
          8: eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
          9: eq#3#(nil(),@x,@xs) -> c_9()
          10: nub#(@l) -> c_10(nub#1#(@l))
          11: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
          12: nub#1#(nil()) -> c_12()
          13: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
          14: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
          15: remove#1#(nil(),@x) -> c_15()
          16: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
          17: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
          18: #and#(#false(),#false()) -> c_18()
          19: #and#(#false(),#true()) -> c_19()
          20: #and#(#true(),#false()) -> c_20()
          21: #and#(#true(),#true()) -> c_21()
          22: #eq#(#0(),#0()) -> c_22()
          23: #eq#(#0(),#neg(@y)) -> c_23()
          24: #eq#(#0(),#pos(@y)) -> c_24()
          25: #eq#(#0(),#s(@y)) -> c_25()
          26: #eq#(#neg(@x),#0()) -> c_26()
          27: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
          28: #eq#(#neg(@x),#pos(@y)) -> c_28()
          29: #eq#(#pos(@x),#0()) -> c_29()
          30: #eq#(#pos(@x),#neg(@y)) -> c_30()
          31: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
          32: #eq#(#s(@x),#0()) -> c_32()
          33: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
          34: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                       ,#eq#(@x_1,@y_1)
                                                       ,#eq#(@x_2,@y_2))
          35: #eq#(::(@x_1,@x_2),nil()) -> c_35()
          36: #eq#(nil(),::(@y_1,@y_2)) -> c_36()
          37: #eq#(nil(),nil()) -> c_37()
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak DPs:
            #and#(#false(),#false()) -> c_18()
            #and#(#false(),#true()) -> c_19()
            #and#(#true(),#false()) -> c_20()
            #and#(#true(),#true()) -> c_21()
            #eq#(#0(),#0()) -> c_22()
            #eq#(#0(),#neg(@y)) -> c_23()
            #eq#(#0(),#pos(@y)) -> c_24()
            #eq#(#0(),#s(@y)) -> c_25()
            #eq#(#neg(@x),#0()) -> c_26()
            #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
            #eq#(#neg(@x),#pos(@y)) -> c_28()
            #eq#(#pos(@x),#0()) -> c_29()
            #eq#(#pos(@x),#neg(@y)) -> c_30()
            #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
            #eq#(#s(@x),#0()) -> c_32()
            #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
            #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                     ,#eq#(@x_1,@y_1)
                                                     ,#eq#(@x_2,@y_2))
            #eq#(::(@x_1,@x_2),nil()) -> c_35()
            #eq#(nil(),::(@y_1,@y_2)) -> c_36()
            #eq#(nil(),nil()) -> c_37()
            #equal#(@x,@y) -> c_1(#eq#(@x,@y))
            and#(@x,@y) -> c_2(#and#(@x,@y))
            eq#2#(::(@y,@ys)) -> c_6()
            eq#2#(nil()) -> c_7()
            eq#3#(nil(),@x,@xs) -> c_9()
            nub#1#(nil()) -> c_12()
            remove#1#(nil(),@x) -> c_15()
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            nub(@l) -> nub#1(@l)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {3}
        by application of
          Pre({3}) = {1}.
        Here rules are labelled as follows:
          1: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
          2: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
          3: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
          4: eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
          5: nub#(@l) -> c_10(nub#1#(@l))
          6: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
          7: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
          8: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
          9: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
          10: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
          11: #and#(#false(),#false()) -> c_18()
          12: #and#(#false(),#true()) -> c_19()
          13: #and#(#true(),#false()) -> c_20()
          14: #and#(#true(),#true()) -> c_21()
          15: #eq#(#0(),#0()) -> c_22()
          16: #eq#(#0(),#neg(@y)) -> c_23()
          17: #eq#(#0(),#pos(@y)) -> c_24()
          18: #eq#(#0(),#s(@y)) -> c_25()
          19: #eq#(#neg(@x),#0()) -> c_26()
          20: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
          21: #eq#(#neg(@x),#pos(@y)) -> c_28()
          22: #eq#(#pos(@x),#0()) -> c_29()
          23: #eq#(#pos(@x),#neg(@y)) -> c_30()
          24: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
          25: #eq#(#s(@x),#0()) -> c_32()
          26: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
          27: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                       ,#eq#(@x_1,@y_1)
                                                       ,#eq#(@x_2,@y_2))
          28: #eq#(::(@x_1,@x_2),nil()) -> c_35()
          29: #eq#(nil(),::(@y_1,@y_2)) -> c_36()
          30: #eq#(nil(),nil()) -> c_37()
          31: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
          32: and#(@x,@y) -> c_2(#and#(@x,@y))
          33: eq#2#(::(@y,@ys)) -> c_6()
          34: eq#2#(nil()) -> c_7()
          35: eq#3#(nil(),@x,@xs) -> c_9()
          36: nub#1#(nil()) -> c_12()
          37: remove#1#(nil(),@x) -> c_15()
* Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak DPs:
            #and#(#false(),#false()) -> c_18()
            #and#(#false(),#true()) -> c_19()
            #and#(#true(),#false()) -> c_20()
            #and#(#true(),#true()) -> c_21()
            #eq#(#0(),#0()) -> c_22()
            #eq#(#0(),#neg(@y)) -> c_23()
            #eq#(#0(),#pos(@y)) -> c_24()
            #eq#(#0(),#s(@y)) -> c_25()
            #eq#(#neg(@x),#0()) -> c_26()
            #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
            #eq#(#neg(@x),#pos(@y)) -> c_28()
            #eq#(#pos(@x),#0()) -> c_29()
            #eq#(#pos(@x),#neg(@y)) -> c_30()
            #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
            #eq#(#s(@x),#0()) -> c_32()
            #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
            #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                     ,#eq#(@x_1,@y_1)
                                                     ,#eq#(@x_2,@y_2))
            #eq#(::(@x_1,@x_2),nil()) -> c_35()
            #eq#(nil(),::(@y_1,@y_2)) -> c_36()
            #eq#(nil(),nil()) -> c_37()
            #equal#(@x,@y) -> c_1(#eq#(@x,@y))
            and#(@x,@y) -> c_2(#and#(@x,@y))
            eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
            eq#2#(::(@y,@ys)) -> c_6()
            eq#2#(nil()) -> c_7()
            eq#3#(nil(),@x,@xs) -> c_9()
            nub#1#(nil()) -> c_12()
            remove#1#(nil(),@x) -> c_15()
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            nub(@l) -> nub#1(@l)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
             -->_1 eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)):32
             -->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):2
          
          2:S:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
             -->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)):3
             -->_1 eq#3#(nil(),@x,@xs) -> c_9():35
          
          3:S:eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
             -->_1 and#(@x,@y) -> c_2(#and#(@x,@y)):31
             -->_2 #equal#(@x,@y) -> c_1(#eq#(@x,@y)):30
             -->_3 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
          
          4:S:nub#(@l) -> c_10(nub#1#(@l))
             -->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):5
             -->_1 nub#1#(nil()) -> c_12():36
          
          5:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
             -->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
             -->_1 nub#(@l) -> c_10(nub#1#(@l)):4
          
          6:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
             -->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):7
             -->_1 remove#1#(nil(),@x) -> c_15():37
          
          7:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
             -->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):9
             -->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):8
             -->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
          
          8:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
             -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
          
          9:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
             -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
          
          10:W:#and#(#false(),#false()) -> c_18()
             
          
          11:W:#and#(#false(),#true()) -> c_19()
             
          
          12:W:#and#(#true(),#false()) -> c_20()
             
          
          13:W:#and#(#true(),#true()) -> c_21()
             
          
          14:W:#eq#(#0(),#0()) -> c_22()
             
          
          15:W:#eq#(#0(),#neg(@y)) -> c_23()
             
          
          16:W:#eq#(#0(),#pos(@y)) -> c_24()
             
          
          17:W:#eq#(#0(),#s(@y)) -> c_25()
             
          
          18:W:#eq#(#neg(@x),#0()) -> c_26()
             
          
          19:W:#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
             -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                            ,#eq#(@x_1,@y_1)
                                                            ,#eq#(@x_2,@y_2)):26
             -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
             -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
             -->_1 #eq#(nil(),nil()) -> c_37():29
             -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
             -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
             -->_1 #eq#(#s(@x),#0()) -> c_32():24
             -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
             -->_1 #eq#(#pos(@x),#0()) -> c_29():21
             -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
             -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
             -->_1 #eq#(#neg(@x),#0()) -> c_26():18
             -->_1 #eq#(#0(),#s(@y)) -> c_25():17
             -->_1 #eq#(#0(),#pos(@y)) -> c_24():16
             -->_1 #eq#(#0(),#neg(@y)) -> c_23():15
             -->_1 #eq#(#0(),#0()) -> c_22():14
          
          20:W:#eq#(#neg(@x),#pos(@y)) -> c_28()
             
          
          21:W:#eq#(#pos(@x),#0()) -> c_29()
             
          
          22:W:#eq#(#pos(@x),#neg(@y)) -> c_30()
             
          
          23:W:#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
             -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                            ,#eq#(@x_1,@y_1)
                                                            ,#eq#(@x_2,@y_2)):26
             -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
             -->_1 #eq#(nil(),nil()) -> c_37():29
             -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
             -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
             -->_1 #eq#(#s(@x),#0()) -> c_32():24
             -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
             -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
             -->_1 #eq#(#pos(@x),#0()) -> c_29():21
             -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
             -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
             -->_1 #eq#(#neg(@x),#0()) -> c_26():18
             -->_1 #eq#(#0(),#s(@y)) -> c_25():17
             -->_1 #eq#(#0(),#pos(@y)) -> c_24():16
             -->_1 #eq#(#0(),#neg(@y)) -> c_23():15
             -->_1 #eq#(#0(),#0()) -> c_22():14
          
          24:W:#eq#(#s(@x),#0()) -> c_32()
             
          
          25:W:#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
             -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                            ,#eq#(@x_1,@y_1)
                                                            ,#eq#(@x_2,@y_2)):26
             -->_1 #eq#(nil(),nil()) -> c_37():29
             -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
             -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
             -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
             -->_1 #eq#(#s(@x),#0()) -> c_32():24
             -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
             -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
             -->_1 #eq#(#pos(@x),#0()) -> c_29():21
             -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
             -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
             -->_1 #eq#(#neg(@x),#0()) -> c_26():18
             -->_1 #eq#(#0(),#s(@y)) -> c_25():17
             -->_1 #eq#(#0(),#pos(@y)) -> c_24():16
             -->_1 #eq#(#0(),#neg(@y)) -> c_23():15
             -->_1 #eq#(#0(),#0()) -> c_22():14
          
          26:W:#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                        ,#eq#(@x_1,@y_1)
                                                        ,#eq#(@x_2,@y_2))
             -->_3 #eq#(nil(),nil()) -> c_37():29
             -->_2 #eq#(nil(),nil()) -> c_37():29
             -->_3 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
             -->_2 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
             -->_3 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
             -->_2 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
             -->_3 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                            ,#eq#(@x_1,@y_1)
                                                            ,#eq#(@x_2,@y_2)):26
             -->_2 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                            ,#eq#(@x_1,@y_1)
                                                            ,#eq#(@x_2,@y_2)):26
             -->_3 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
             -->_2 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
             -->_3 #eq#(#s(@x),#0()) -> c_32():24
             -->_2 #eq#(#s(@x),#0()) -> c_32():24
             -->_3 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
             -->_2 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
             -->_3 #eq#(#pos(@x),#neg(@y)) -> c_30():22
             -->_2 #eq#(#pos(@x),#neg(@y)) -> c_30():22
             -->_3 #eq#(#pos(@x),#0()) -> c_29():21
             -->_2 #eq#(#pos(@x),#0()) -> c_29():21
             -->_3 #eq#(#neg(@x),#pos(@y)) -> c_28():20
             -->_2 #eq#(#neg(@x),#pos(@y)) -> c_28():20
             -->_3 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
             -->_2 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
             -->_3 #eq#(#neg(@x),#0()) -> c_26():18
             -->_2 #eq#(#neg(@x),#0()) -> c_26():18
             -->_3 #eq#(#0(),#s(@y)) -> c_25():17
             -->_2 #eq#(#0(),#s(@y)) -> c_25():17
             -->_3 #eq#(#0(),#pos(@y)) -> c_24():16
             -->_2 #eq#(#0(),#pos(@y)) -> c_24():16
             -->_3 #eq#(#0(),#neg(@y)) -> c_23():15
             -->_2 #eq#(#0(),#neg(@y)) -> c_23():15
             -->_3 #eq#(#0(),#0()) -> c_22():14
             -->_2 #eq#(#0(),#0()) -> c_22():14
             -->_1 #and#(#true(),#true()) -> c_21():13
             -->_1 #and#(#true(),#false()) -> c_20():12
             -->_1 #and#(#false(),#true()) -> c_19():11
             -->_1 #and#(#false(),#false()) -> c_18():10
          
          27:W:#eq#(::(@x_1,@x_2),nil()) -> c_35()
             
          
          28:W:#eq#(nil(),::(@y_1,@y_2)) -> c_36()
             
          
          29:W:#eq#(nil(),nil()) -> c_37()
             
          
          30:W:#equal#(@x,@y) -> c_1(#eq#(@x,@y))
             -->_1 #eq#(nil(),nil()) -> c_37():29
             -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
             -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
             -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                            ,#eq#(@x_1,@y_1)
                                                            ,#eq#(@x_2,@y_2)):26
             -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
             -->_1 #eq#(#s(@x),#0()) -> c_32():24
             -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
             -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
             -->_1 #eq#(#pos(@x),#0()) -> c_29():21
             -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
             -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
             -->_1 #eq#(#neg(@x),#0()) -> c_26():18
             -->_1 #eq#(#0(),#s(@y)) -> c_25():17
             -->_1 #eq#(#0(),#pos(@y)) -> c_24():16
             -->_1 #eq#(#0(),#neg(@y)) -> c_23():15
             -->_1 #eq#(#0(),#0()) -> c_22():14
          
          31:W:and#(@x,@y) -> c_2(#and#(@x,@y))
             -->_1 #and#(#true(),#true()) -> c_21():13
             -->_1 #and#(#true(),#false()) -> c_20():12
             -->_1 #and#(#false(),#true()) -> c_19():11
             -->_1 #and#(#false(),#false()) -> c_18():10
          
          32:W:eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
             -->_1 eq#2#(nil()) -> c_7():34
             -->_1 eq#2#(::(@y,@ys)) -> c_6():33
          
          33:W:eq#2#(::(@y,@ys)) -> c_6()
             
          
          34:W:eq#2#(nil()) -> c_7()
             
          
          35:W:eq#3#(nil(),@x,@xs) -> c_9()
             
          
          36:W:nub#1#(nil()) -> c_12()
             
          
          37:W:remove#1#(nil(),@x) -> c_15()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          36: nub#1#(nil()) -> c_12()
          37: remove#1#(nil(),@x) -> c_15()
          35: eq#3#(nil(),@x,@xs) -> c_9()
          30: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
          26: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
                                                       ,#eq#(@x_1,@y_1)
                                                       ,#eq#(@x_2,@y_2))
          25: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
          23: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
          19: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
          14: #eq#(#0(),#0()) -> c_22()
          15: #eq#(#0(),#neg(@y)) -> c_23()
          16: #eq#(#0(),#pos(@y)) -> c_24()
          17: #eq#(#0(),#s(@y)) -> c_25()
          18: #eq#(#neg(@x),#0()) -> c_26()
          20: #eq#(#neg(@x),#pos(@y)) -> c_28()
          21: #eq#(#pos(@x),#0()) -> c_29()
          22: #eq#(#pos(@x),#neg(@y)) -> c_30()
          24: #eq#(#s(@x),#0()) -> c_32()
          27: #eq#(::(@x_1,@x_2),nil()) -> c_35()
          28: #eq#(nil(),::(@y_1,@y_2)) -> c_36()
          29: #eq#(nil(),nil()) -> c_37()
          31: and#(@x,@y) -> c_2(#and#(@x,@y))
          10: #and#(#false(),#false()) -> c_18()
          11: #and#(#false(),#true()) -> c_19()
          12: #and#(#true(),#false()) -> c_20()
          13: #and#(#true(),#true()) -> c_21()
          32: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
          33: eq#2#(::(@y,@ys)) -> c_6()
          34: eq#2#(nil()) -> c_7()
* Step 5: SimplifyRHS WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            nub(@l) -> nub#1(@l)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
             -->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):2
          
          2:S:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
             -->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)):3
          
          3:S:eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
             -->_3 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
          
          4:S:nub#(@l) -> c_10(nub#1#(@l))
             -->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):5
          
          5:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
             -->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
             -->_1 nub#(@l) -> c_10(nub#1#(@l)):4
          
          6:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
             -->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):7
          
          7:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
             -->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):9
             -->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):8
             -->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
          
          8:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
             -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
          
          9:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
             -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
* Step 6: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            nub(@l) -> nub#1(@l)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          #and(#false(),#false()) -> #false()
          #and(#false(),#true()) -> #false()
          #and(#true(),#false()) -> #false()
          #and(#true(),#true()) -> #true()
          #eq(#0(),#0()) -> #true()
          #eq(#0(),#neg(@y)) -> #false()
          #eq(#0(),#pos(@y)) -> #false()
          #eq(#0(),#s(@y)) -> #false()
          #eq(#neg(@x),#0()) -> #false()
          #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
          #eq(#neg(@x),#pos(@y)) -> #false()
          #eq(#pos(@x),#0()) -> #false()
          #eq(#pos(@x),#neg(@y)) -> #false()
          #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
          #eq(#s(@x),#0()) -> #false()
          #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          #eq(::(@x_1,@x_2),nil()) -> #false()
          #eq(nil(),::(@y_1,@y_2)) -> #false()
          #eq(nil(),nil()) -> #true()
          #equal(@x,@y) -> #eq(@x,@y)
          and(@x,@y) -> #and(@x,@y)
          eq(@l1,@l2) -> eq#1(@l1,@l2)
          eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
          eq#1(nil(),@l2) -> eq#2(@l2)
          eq#2(::(@y,@ys)) -> #false()
          eq#2(nil()) -> #true()
          eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
          eq#3(nil(),@x,@xs) -> #false()
          remove(@x,@l) -> remove#1(@l,@x)
          remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
          remove#1(nil(),@x) -> nil()
          remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
          remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
          eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
          eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
          eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
          nub#(@l) -> c_10(nub#1#(@l))
          nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
          remove#(@x,@l) -> c_13(remove#1#(@l,@x))
          remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
          remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
          remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
* Step 7: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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
          nub#(@l) -> c_10(nub#1#(@l))
          nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
        and a lower component
          eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
          eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
          eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
          remove#(@x,@l) -> c_13(remove#1#(@l,@x))
          remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
          remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
          remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        Further, following extension rules are added to the lower component.
          nub#(@l) -> nub#1#(@l)
          nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
          nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:nub#(@l) -> c_10(nub#1#(@l))
             -->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):2
          
          2:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
             -->_1 nub#(@l) -> c_10(nub#1#(@l)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)))
** Step 7.a:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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(#and) = {1,2},
            uargs(::) = {2},
            uargs(and) = {1,2},
            uargs(remove#2) = {1},
            uargs(nub#) = {1},
            uargs(c_10) = {1},
            uargs(c_11) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(#0) = [0]                  
                 p(#and) = [1] x1 + [1] x2 + [0]
                  p(#eq) = [0]                  
               p(#equal) = [0]                  
               p(#false) = [0]                  
                 p(#neg) = [1] x1 + [0]         
                 p(#pos) = [1] x1 + [0]         
                   p(#s) = [1] x1 + [0]         
                p(#true) = [0]                  
                   p(::) = [1] x2 + [0]         
                  p(and) = [1] x1 + [1] x2 + [0]
                   p(eq) = [0]                  
                 p(eq#1) = [0]                  
                 p(eq#2) = [0]                  
                 p(eq#3) = [0]                  
                  p(nil) = [0]                  
                  p(nub) = [0]                  
                p(nub#1) = [0]                  
               p(remove) = [1]                  
             p(remove#1) = [1]                  
             p(remove#2) = [1] x1 + [1]         
                p(#and#) = [0]                  
                 p(#eq#) = [0]                  
              p(#equal#) = [0]                  
                 p(and#) = [0]                  
                  p(eq#) = [0]                  
                p(eq#1#) = [0]                  
                p(eq#2#) = [0]                  
                p(eq#3#) = [0]                  
                 p(nub#) = [1] x1 + [6]         
               p(nub#1#) = [1] x1 + [1]         
              p(remove#) = [0]                  
            p(remove#1#) = [0]                  
            p(remove#2#) = [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) = [1] x1 + [0]         
                 p(c_11) = [1] x1 + [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) = [0]                  
                 p(c_21) = [0]                  
                 p(c_22) = [0]                  
                 p(c_23) = [0]                  
                 p(c_24) = [0]                  
                 p(c_25) = [0]                  
                 p(c_26) = [0]                  
                 p(c_27) = [0]                  
                 p(c_28) = [0]                  
                 p(c_29) = [0]                  
                 p(c_30) = [0]                  
                 p(c_31) = [0]                  
                 p(c_32) = [0]                  
                 p(c_33) = [0]                  
                 p(c_34) = [2] x1 + [1] x2 + [1]
                 p(c_35) = [0]                  
                 p(c_36) = [4]                  
                 p(c_37) = [0]                  
          
          Following rules are strictly oriented:
          nub#(@l) = [1] @l + [6]    
                   > [1] @l + [1]    
                   = c_10(nub#1#(@l))
          
          
          Following rules are (at-least) weakly oriented:
                        nub#1#(::(@x,@xs)) =  [1] @xs + [1]                      
                                           >= [7]                                
                                           =  c_11(nub#(remove(@x,@xs)))         
          
                   #and(#false(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#false(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#true(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                     #and(#true(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                            #eq(#0(),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                        #eq(#0(),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#0(),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(#0(),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#neg(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#neg(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                    #eq(#neg(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#pos(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                          #eq(#s(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#s(@x),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          
                  #eq(::(@x_1,@x_2),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                  #eq(nil(),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(nil(),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                             #equal(@x,@y) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                                and(@x,@y) =  [1] @x + [1] @y + [0]              
                                           >= [1] @x + [1] @y + [0]              
                                           =  #and(@x,@y)                        
          
                               eq(@l1,@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#1(@l1,@l2)                      
          
                      eq#1(::(@x,@xs),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#3(@l2,@x,@xs)                   
          
                           eq#1(nil(),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#2(@l2)                          
          
                          eq#2(::(@y,@ys)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                               eq#2(nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                             remove(@x,@l) =  [1]                                
                                           >= [1]                                
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [1]                                
                                           >= [1]                                
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [1]                                
                                           >= [0]                                
                                           =  nil()                              
          
              remove#2(#false(),@x,@y,@ys) =  [1]                                
                                           >= [1]                                
                                           =  ::(@y,remove(@x,@ys))              
          
               remove#2(#true(),@x,@y,@ys) =  [1]                                
                                           >= [1]                                
                                           =  remove(@x,@ys)                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 7.a:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)))
        - Weak DPs:
            nub#(@l) -> c_10(nub#1#(@l))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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(#and) = {1,2},
            uargs(::) = {2},
            uargs(and) = {1,2},
            uargs(remove#2) = {1},
            uargs(nub#) = {1},
            uargs(c_10) = {1},
            uargs(c_11) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(#0) = [0]                  
                 p(#and) = [1] x1 + [1] x2 + [0]
                  p(#eq) = [0]                  
               p(#equal) = [0]                  
               p(#false) = [0]                  
                 p(#neg) = [1] x1 + [0]         
                 p(#pos) = [1] x1 + [0]         
                   p(#s) = [1] x1 + [0]         
                p(#true) = [0]                  
                   p(::) = [1] x2 + [1]         
                  p(and) = [1] x1 + [1] x2 + [0]
                   p(eq) = [0]                  
                 p(eq#1) = [0]                  
                 p(eq#2) = [0]                  
                 p(eq#3) = [0]                  
                  p(nil) = [1]                  
                  p(nub) = [0]                  
                p(nub#1) = [0]                  
               p(remove) = [1] x2 + [0]         
             p(remove#1) = [1] x1 + [0]         
             p(remove#2) = [1] x1 + [1] x4 + [1]
                p(#and#) = [0]                  
                 p(#eq#) = [0]                  
              p(#equal#) = [0]                  
                 p(and#) = [0]                  
                  p(eq#) = [0]                  
                p(eq#1#) = [0]                  
                p(eq#2#) = [0]                  
                p(eq#3#) = [0]                  
                 p(nub#) = [1] x1 + [0]         
               p(nub#1#) = [1] x1 + [0]         
              p(remove#) = [0]                  
            p(remove#1#) = [0]                  
            p(remove#2#) = [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) = [1] x1 + [0]         
                 p(c_11) = [1] x1 + [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) = [0]                  
                 p(c_21) = [0]                  
                 p(c_22) = [0]                  
                 p(c_23) = [0]                  
                 p(c_24) = [0]                  
                 p(c_25) = [0]                  
                 p(c_26) = [0]                  
                 p(c_27) = [4] x1 + [0]         
                 p(c_28) = [0]                  
                 p(c_29) = [0]                  
                 p(c_30) = [0]                  
                 p(c_31) = [2] x1 + [0]         
                 p(c_32) = [2]                  
                 p(c_33) = [1] x1 + [0]         
                 p(c_34) = [4] x3 + [1]         
                 p(c_35) = [0]                  
                 p(c_36) = [4]                  
                 p(c_37) = [0]                  
          
          Following rules are strictly oriented:
          nub#1#(::(@x,@xs)) = [1] @xs + [1]             
                             > [1] @xs + [0]             
                             = c_11(nub#(remove(@x,@xs)))
          
          
          Following rules are (at-least) weakly oriented:
                                  nub#(@l) =  [1] @l + [0]                       
                                           >= [1] @l + [0]                       
                                           =  c_10(nub#1#(@l))                   
          
                   #and(#false(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#false(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#true(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                     #and(#true(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                            #eq(#0(),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                        #eq(#0(),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#0(),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(#0(),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#neg(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#neg(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                    #eq(#neg(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#pos(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                          #eq(#s(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#s(@x),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          
                  #eq(::(@x_1,@x_2),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                  #eq(nil(),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(nil(),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                             #equal(@x,@y) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                                and(@x,@y) =  [1] @x + [1] @y + [0]              
                                           >= [1] @x + [1] @y + [0]              
                                           =  #and(@x,@y)                        
          
                               eq(@l1,@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#1(@l1,@l2)                      
          
                      eq#1(::(@x,@xs),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#3(@l2,@x,@xs)                   
          
                           eq#1(nil(),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#2(@l2)                          
          
                          eq#2(::(@y,@ys)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                               eq#2(nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                             remove(@x,@l) =  [1] @l + [0]                       
                                           >= [1] @l + [0]                       
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [1] @ys + [1]                      
                                           >= [1] @ys + [1]                      
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [1]                                
                                           >= [1]                                
                                           =  nil()                              
          
              remove#2(#false(),@x,@y,@ys) =  [1] @ys + [1]                      
                                           >= [1] @ys + [1]                      
                                           =  ::(@y,remove(@x,@ys))              
          
               remove#2(#true(),@x,@y,@ys) =  [1] @ys + [1]                      
                                           >= [1] @ys + [0]                      
                                           =  remove(@x,@ys)                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 7.a:4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            nub#(@l) -> c_10(nub#1#(@l))
            nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 7.b:1: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak DPs:
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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
          nub#(@l) -> nub#1#(@l)
          nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
          nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
          remove#(@x,@l) -> c_13(remove#1#(@l,@x))
          remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
          remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
          remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        and a lower component
          eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
          eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
          eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
        Further, following extension rules are added to the lower component.
          nub#(@l) -> nub#1#(@l)
          nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
          nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
          remove#(@x,@l) -> remove#1#(@l,@x)
          remove#1#(::(@y,@ys),@x) -> eq#(@x,@y)
          remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys)
          remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys)
          remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys)
*** Step 7.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak DPs:
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
             -->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):2
          
          2:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
             -->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):4
             -->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):3
          
          3:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
             -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):1
          
          4:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
             -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):1
          
          5:W:nub#(@l) -> nub#1#(@l)
             -->_1 nub#1#(::(@x,@xs)) -> remove#(@x,@xs):7
             -->_1 nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)):6
          
          6:W:nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
             -->_1 nub#(@l) -> nub#1#(@l):5
          
          7:W:nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
             -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
*** Step 7.b:1.a:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak DPs:
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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(#and) = {1,2},
            uargs(::) = {2},
            uargs(and) = {1,2},
            uargs(remove#2) = {1},
            uargs(nub#) = {1},
            uargs(remove#2#) = {1},
            uargs(c_13) = {1},
            uargs(c_14) = {1},
            uargs(c_16) = {1},
            uargs(c_17) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(#0) = [0]                  
                 p(#and) = [1] x1 + [1] x2 + [0]
                  p(#eq) = [0]                  
               p(#equal) = [0]                  
               p(#false) = [0]                  
                 p(#neg) = [1] x1 + [0]         
                 p(#pos) = [1] x1 + [0]         
                   p(#s) = [1] x1 + [0]         
                p(#true) = [0]                  
                   p(::) = [1] x2 + [0]         
                  p(and) = [1] x1 + [1] x2 + [0]
                   p(eq) = [0]                  
                 p(eq#1) = [0]                  
                 p(eq#2) = [0]                  
                 p(eq#3) = [0]                  
                  p(nil) = [0]                  
                  p(nub) = [0]                  
                p(nub#1) = [0]                  
               p(remove) = [0]                  
             p(remove#1) = [0]                  
             p(remove#2) = [1] x1 + [0]         
                p(#and#) = [0]                  
                 p(#eq#) = [0]                  
              p(#equal#) = [0]                  
                 p(and#) = [0]                  
                  p(eq#) = [0]                  
                p(eq#1#) = [1]                  
                p(eq#2#) = [0]                  
                p(eq#3#) = [0]                  
                 p(nub#) = [1] x1 + [0]         
               p(nub#1#) = [0]                  
              p(remove#) = [0]                  
            p(remove#1#) = [0]                  
            p(remove#2#) = [1] x1 + [3]         
                  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) = [1] x1 + [0]         
                 p(c_14) = [1] x1 + [0]         
                 p(c_15) = [0]                  
                 p(c_16) = [1] x1 + [0]         
                 p(c_17) = [1] x1 + [0]         
                 p(c_18) = [0]                  
                 p(c_19) = [0]                  
                 p(c_20) = [0]                  
                 p(c_21) = [0]                  
                 p(c_22) = [0]                  
                 p(c_23) = [0]                  
                 p(c_24) = [0]                  
                 p(c_25) = [0]                  
                 p(c_26) = [0]                  
                 p(c_27) = [0]                  
                 p(c_28) = [0]                  
                 p(c_29) = [0]                  
                 p(c_30) = [0]                  
                 p(c_31) = [0]                  
                 p(c_32) = [0]                  
                 p(c_33) = [0]                  
                 p(c_34) = [0]                  
                 p(c_35) = [0]                  
                 p(c_36) = [0]                  
                 p(c_37) = [0]                  
          
          Following rules are strictly oriented:
          remove#2#(#false(),@x,@y,@ys) = [3]                  
                                        > [0]                  
                                        = c_16(remove#(@x,@ys))
          
           remove#2#(#true(),@x,@y,@ys) = [3]                  
                                        > [0]                  
                                        = c_17(remove#(@x,@ys))
          
          
          Following rules are (at-least) weakly oriented:
                                  nub#(@l) =  [1] @l + [0]                        
                                           >= [0]                                 
                                           =  nub#1#(@l)                          
          
                        nub#1#(::(@x,@xs)) =  [0]                                 
                                           >= [0]                                 
                                           =  nub#(remove(@x,@xs))                
          
                        nub#1#(::(@x,@xs)) =  [0]                                 
                                           >= [0]                                 
                                           =  remove#(@x,@xs)                     
          
                            remove#(@x,@l) =  [0]                                 
                                           >= [0]                                 
                                           =  c_13(remove#1#(@l,@x))              
          
                  remove#1#(::(@y,@ys),@x) =  [0]                                 
                                           >= [3]                                 
                                           =  c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
          
                   #and(#false(),#false()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #and(#false(),#true()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #and(#true(),#false()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                     #and(#true(),#true()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                            #eq(#0(),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                        #eq(#0(),#neg(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#0(),#pos(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                          #eq(#0(),#s(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#neg(@x),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #eq(#neg(@x),#neg(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
                    #eq(#neg(@x),#pos(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#pos(@x),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #eq(#pos(@x),#neg(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #eq(#pos(@x),#pos(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
                          #eq(#s(@x),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#s(@x),#s(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0]                                 
                                           >= [0]                                 
                                           =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) 
          
                  #eq(::(@x_1,@x_2),nil()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                  #eq(nil(),::(@y_1,@y_2)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                          #eq(nil(),nil()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                             #equal(@x,@y) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
                                and(@x,@y) =  [1] @x + [1] @y + [0]               
                                           >= [1] @x + [1] @y + [0]               
                                           =  #and(@x,@y)                         
          
                               eq(@l1,@l2) =  [0]                                 
                                           >= [0]                                 
                                           =  eq#1(@l1,@l2)                       
          
                      eq#1(::(@x,@xs),@l2) =  [0]                                 
                                           >= [0]                                 
                                           =  eq#3(@l2,@x,@xs)                    
          
                           eq#1(nil(),@l2) =  [0]                                 
                                           >= [0]                                 
                                           =  eq#2(@l2)                           
          
                          eq#2(::(@y,@ys)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                               eq#2(nil()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                 
                                           >= [0]                                 
                                           =  and(#equal(@x,@y),eq(@xs,@ys))      
          
                        eq#3(nil(),@x,@xs) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                             remove(@x,@l) =  [0]                                 
                                           >= [0]                                 
                                           =  remove#1(@l,@x)                     
          
                   remove#1(::(@y,@ys),@x) =  [0]                                 
                                           >= [0]                                 
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)       
          
                        remove#1(nil(),@x) =  [0]                                 
                                           >= [0]                                 
                                           =  nil()                               
          
              remove#2(#false(),@x,@y,@ys) =  [0]                                 
                                           >= [0]                                 
                                           =  ::(@y,remove(@x,@ys))               
          
               remove#2(#true(),@x,@y,@ys) =  [0]                                 
                                           >= [0]                                 
                                           =  remove(@x,@ys)                      
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 7.b:1.a:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
        - Weak DPs:
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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(#and) = {1,2},
            uargs(::) = {2},
            uargs(and) = {1,2},
            uargs(remove#2) = {1},
            uargs(nub#) = {1},
            uargs(remove#2#) = {1},
            uargs(c_13) = {1},
            uargs(c_14) = {1},
            uargs(c_16) = {1},
            uargs(c_17) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(#0) = [0]                  
                 p(#and) = [1] x1 + [1] x2 + [0]
                  p(#eq) = [0]                  
               p(#equal) = [0]                  
               p(#false) = [0]                  
                 p(#neg) = [1] x1 + [0]         
                 p(#pos) = [1] x1 + [0]         
                   p(#s) = [1] x1 + [0]         
                p(#true) = [0]                  
                   p(::) = [1] x2 + [0]         
                  p(and) = [1] x1 + [1] x2 + [0]
                   p(eq) = [0]                  
                 p(eq#1) = [0]                  
                 p(eq#2) = [0]                  
                 p(eq#3) = [0]                  
                  p(nil) = [0]                  
                  p(nub) = [0]                  
                p(nub#1) = [0]                  
               p(remove) = [0]                  
             p(remove#1) = [0]                  
             p(remove#2) = [1] x1 + [0]         
                p(#and#) = [0]                  
                 p(#eq#) = [0]                  
              p(#equal#) = [0]                  
                 p(and#) = [0]                  
                  p(eq#) = [0]                  
                p(eq#1#) = [0]                  
                p(eq#2#) = [0]                  
                p(eq#3#) = [0]                  
                 p(nub#) = [1] x1 + [6]         
               p(nub#1#) = [6]                  
              p(remove#) = [5]                  
            p(remove#1#) = [1]                  
            p(remove#2#) = [1] x1 + [7]         
                  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) = [2]                  
                 p(c_13) = [1] x1 + [0]         
                 p(c_14) = [1] x1 + [3]         
                 p(c_15) = [0]                  
                 p(c_16) = [1] x1 + [0]         
                 p(c_17) = [1] x1 + [0]         
                 p(c_18) = [0]                  
                 p(c_19) = [0]                  
                 p(c_20) = [0]                  
                 p(c_21) = [0]                  
                 p(c_22) = [1]                  
                 p(c_23) = [0]                  
                 p(c_24) = [0]                  
                 p(c_25) = [0]                  
                 p(c_26) = [0]                  
                 p(c_27) = [1] x1 + [4]         
                 p(c_28) = [1]                  
                 p(c_29) = [1]                  
                 p(c_30) = [0]                  
                 p(c_31) = [0]                  
                 p(c_32) = [1]                  
                 p(c_33) = [0]                  
                 p(c_34) = [4] x1 + [1] x2 + [1]
                 p(c_35) = [2]                  
                 p(c_36) = [0]                  
                 p(c_37) = [0]                  
          
          Following rules are strictly oriented:
          remove#(@x,@l) = [5]                   
                         > [1]                   
                         = c_13(remove#1#(@l,@x))
          
          
          Following rules are (at-least) weakly oriented:
                                  nub#(@l) =  [1] @l + [6]                        
                                           >= [6]                                 
                                           =  nub#1#(@l)                          
          
                        nub#1#(::(@x,@xs)) =  [6]                                 
                                           >= [6]                                 
                                           =  nub#(remove(@x,@xs))                
          
                        nub#1#(::(@x,@xs)) =  [6]                                 
                                           >= [5]                                 
                                           =  remove#(@x,@xs)                     
          
                  remove#1#(::(@y,@ys),@x) =  [1]                                 
                                           >= [10]                                
                                           =  c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
          
             remove#2#(#false(),@x,@y,@ys) =  [7]                                 
                                           >= [5]                                 
                                           =  c_16(remove#(@x,@ys))               
          
              remove#2#(#true(),@x,@y,@ys) =  [7]                                 
                                           >= [5]                                 
                                           =  c_17(remove#(@x,@ys))               
          
                   #and(#false(),#false()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #and(#false(),#true()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #and(#true(),#false()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                     #and(#true(),#true()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                            #eq(#0(),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                        #eq(#0(),#neg(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#0(),#pos(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                          #eq(#0(),#s(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#neg(@x),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #eq(#neg(@x),#neg(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
                    #eq(#neg(@x),#pos(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#pos(@x),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #eq(#pos(@x),#neg(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                    #eq(#pos(@x),#pos(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
                          #eq(#s(@x),#0()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                        #eq(#s(@x),#s(@y)) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0]                                 
                                           >= [0]                                 
                                           =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) 
          
                  #eq(::(@x_1,@x_2),nil()) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                  #eq(nil(),::(@y_1,@y_2)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                          #eq(nil(),nil()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                             #equal(@x,@y) =  [0]                                 
                                           >= [0]                                 
                                           =  #eq(@x,@y)                          
          
                                and(@x,@y) =  [1] @x + [1] @y + [0]               
                                           >= [1] @x + [1] @y + [0]               
                                           =  #and(@x,@y)                         
          
                               eq(@l1,@l2) =  [0]                                 
                                           >= [0]                                 
                                           =  eq#1(@l1,@l2)                       
          
                      eq#1(::(@x,@xs),@l2) =  [0]                                 
                                           >= [0]                                 
                                           =  eq#3(@l2,@x,@xs)                    
          
                           eq#1(nil(),@l2) =  [0]                                 
                                           >= [0]                                 
                                           =  eq#2(@l2)                           
          
                          eq#2(::(@y,@ys)) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                               eq#2(nil()) =  [0]                                 
                                           >= [0]                                 
                                           =  #true()                             
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                 
                                           >= [0]                                 
                                           =  and(#equal(@x,@y),eq(@xs,@ys))      
          
                        eq#3(nil(),@x,@xs) =  [0]                                 
                                           >= [0]                                 
                                           =  #false()                            
          
                             remove(@x,@l) =  [0]                                 
                                           >= [0]                                 
                                           =  remove#1(@l,@x)                     
          
                   remove#1(::(@y,@ys),@x) =  [0]                                 
                                           >= [0]                                 
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)       
          
                        remove#1(nil(),@x) =  [0]                                 
                                           >= [0]                                 
                                           =  nil()                               
          
              remove#2(#false(),@x,@y,@ys) =  [0]                                 
                                           >= [0]                                 
                                           =  ::(@y,remove(@x,@ys))               
          
               remove#2(#true(),@x,@y,@ys) =  [0]                                 
                                           >= [0]                                 
                                           =  remove(@x,@ys)                      
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 7.b:1.a:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
        - Weak DPs:
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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(#and) = {1,2},
            uargs(::) = {2},
            uargs(and) = {1,2},
            uargs(remove#2) = {1},
            uargs(nub#) = {1},
            uargs(remove#2#) = {1},
            uargs(c_13) = {1},
            uargs(c_14) = {1},
            uargs(c_16) = {1},
            uargs(c_17) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(#0) = [0]                  
                 p(#and) = [1] x1 + [1] x2 + [0]
                  p(#eq) = [0]                  
               p(#equal) = [0]                  
               p(#false) = [0]                  
                 p(#neg) = [0]                  
                 p(#pos) = [0]                  
                   p(#s) = [0]                  
                p(#true) = [0]                  
                   p(::) = [1] x2 + [4]         
                  p(and) = [1] x1 + [1] x2 + [0]
                   p(eq) = [0]                  
                 p(eq#1) = [0]                  
                 p(eq#2) = [0]                  
                 p(eq#3) = [0]                  
                  p(nil) = [1]                  
                  p(nub) = [4] x1 + [4]         
                p(nub#1) = [2] x1 + [4]         
               p(remove) = [1] x2 + [0]         
             p(remove#1) = [1] x1 + [0]         
             p(remove#2) = [1] x1 + [1] x4 + [4]
                p(#and#) = [4] x1 + [1] x2 + [4]
                 p(#eq#) = [4] x1 + [0]         
              p(#equal#) = [4] x1 + [4] x2 + [2]
                 p(and#) = [1] x1 + [1]         
                  p(eq#) = [2] x1 + [4] x2 + [0]
                p(eq#1#) = [1]                  
                p(eq#2#) = [2] x1 + [0]         
                p(eq#3#) = [4] x2 + [1] x3 + [4]
                 p(nub#) = [1] x1 + [1]         
               p(nub#1#) = [1] x1 + [0]         
              p(remove#) = [1] x2 + [1]         
            p(remove#1#) = [1] x1 + [1]         
            p(remove#2#) = [1] x1 + [1] x4 + [4]
                  p(c_1) = [2] x1 + [1]         
                  p(c_2) = [2] x1 + [1]         
                  p(c_3) = [2] x1 + [0]         
                  p(c_4) = [2] x1 + [1]         
                  p(c_5) = [4] x1 + [1]         
                  p(c_6) = [0]                  
                  p(c_7) = [2]                  
                  p(c_8) = [2] x1 + [0]         
                  p(c_9) = [1]                  
                 p(c_10) = [1] x1 + [2]         
                 p(c_11) = [1] x1 + [1] x2 + [1]
                 p(c_12) = [0]                  
                 p(c_13) = [1] x1 + [0]         
                 p(c_14) = [1] x1 + [0]         
                 p(c_15) = [0]                  
                 p(c_16) = [1] x1 + [0]         
                 p(c_17) = [1] x1 + [3]         
                 p(c_18) = [0]                  
                 p(c_19) = [1]                  
                 p(c_20) = [1]                  
                 p(c_21) = [0]                  
                 p(c_22) = [1]                  
                 p(c_23) = [0]                  
                 p(c_24) = [2]                  
                 p(c_25) = [0]                  
                 p(c_26) = [0]                  
                 p(c_27) = [1] x1 + [1]         
                 p(c_28) = [1]                  
                 p(c_29) = [0]                  
                 p(c_30) = [1]                  
                 p(c_31) = [4]                  
                 p(c_32) = [1]                  
                 p(c_33) = [2] x1 + [0]         
                 p(c_34) = [2] x2 + [2] x3 + [2]
                 p(c_35) = [1]                  
                 p(c_36) = [0]                  
                 p(c_37) = [2]                  
          
          Following rules are strictly oriented:
          remove#1#(::(@y,@ys),@x) = [1] @ys + [5]                       
                                   > [1] @ys + [4]                       
                                   = c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
          
          
          Following rules are (at-least) weakly oriented:
                                  nub#(@l) =  [1] @l + [1]                       
                                           >= [1] @l + [0]                       
                                           =  nub#1#(@l)                         
          
                        nub#1#(::(@x,@xs)) =  [1] @xs + [4]                      
                                           >= [1] @xs + [1]                      
                                           =  nub#(remove(@x,@xs))               
          
                        nub#1#(::(@x,@xs)) =  [1] @xs + [4]                      
                                           >= [1] @xs + [1]                      
                                           =  remove#(@x,@xs)                    
          
                            remove#(@x,@l) =  [1] @l + [1]                       
                                           >= [1] @l + [1]                       
                                           =  c_13(remove#1#(@l,@x))             
          
             remove#2#(#false(),@x,@y,@ys) =  [1] @ys + [4]                      
                                           >= [1] @ys + [1]                      
                                           =  c_16(remove#(@x,@ys))              
          
              remove#2#(#true(),@x,@y,@ys) =  [1] @ys + [4]                      
                                           >= [1] @ys + [4]                      
                                           =  c_17(remove#(@x,@ys))              
          
                   #and(#false(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#false(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#true(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                     #and(#true(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                            #eq(#0(),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                        #eq(#0(),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#0(),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(#0(),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#neg(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#neg(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                    #eq(#neg(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#pos(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                          #eq(#s(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#s(@x),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          
                  #eq(::(@x_1,@x_2),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                  #eq(nil(),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(nil(),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                             #equal(@x,@y) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                                and(@x,@y) =  [1] @x + [1] @y + [0]              
                                           >= [1] @x + [1] @y + [0]              
                                           =  #and(@x,@y)                        
          
                               eq(@l1,@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#1(@l1,@l2)                      
          
                      eq#1(::(@x,@xs),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#3(@l2,@x,@xs)                   
          
                           eq#1(nil(),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#2(@l2)                          
          
                          eq#2(::(@y,@ys)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                               eq#2(nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                             remove(@x,@l) =  [1] @l + [0]                       
                                           >= [1] @l + [0]                       
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [1] @ys + [4]                      
                                           >= [1] @ys + [4]                      
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [1]                                
                                           >= [1]                                
                                           =  nil()                              
          
              remove#2(#false(),@x,@y,@ys) =  [1] @ys + [4]                      
                                           >= [1] @ys + [4]                      
                                           =  ::(@y,remove(@x,@ys))              
          
               remove#2(#true(),@x,@y,@ys) =  [1] @ys + [4]                      
                                           >= [1] @ys + [0]                      
                                           =  remove(@x,@ys)                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 7.b:1.a:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
            remove#(@x,@l) -> c_13(remove#1#(@l,@x))
            remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
            remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
            remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

*** Step 7.b:1.b:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
        - Weak DPs:
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
            remove#(@x,@l) -> remove#1#(@l,@x)
            remove#1#(::(@y,@ys),@x) -> eq#(@x,@y)
            remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys)
            remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys)
            remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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_3) = {1},
          uargs(c_4) = {1},
          uargs(c_8) = {1}
        
        Following symbols are considered usable:
          {remove,remove#1,remove#2,#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#,remove#,remove#1#
          ,remove#2#}
        TcT has computed the following interpretation:
                 p(#0) = [0]                  
               p(#and) = [0]                  
                p(#eq) = [4] x1 + [0]         
             p(#equal) = [0]                  
             p(#false) = [0]                  
               p(#neg) = [1] x1 + [0]         
               p(#pos) = [1] x1 + [3]         
                 p(#s) = [1] x1 + [3]         
              p(#true) = [0]                  
                 p(::) = [1] x1 + [1] x2 + [1]
                p(and) = [0]                  
                 p(eq) = [0]                  
               p(eq#1) = [0]                  
               p(eq#2) = [0]                  
               p(eq#3) = [0]                  
                p(nil) = [0]                  
                p(nub) = [1] x1 + [0]         
              p(nub#1) = [0]                  
             p(remove) = [1] x2 + [0]         
           p(remove#1) = [1] x1 + [0]         
           p(remove#2) = [1] x3 + [1] x4 + [1]
              p(#and#) = [1] x2 + [0]         
               p(#eq#) = [0]                  
            p(#equal#) = [1] x1 + [0]         
               p(and#) = [1]                  
                p(eq#) = [6] x1 + [4]         
              p(eq#1#) = [6] x1 + [0]         
              p(eq#2#) = [4]                  
              p(eq#3#) = [1] x2 + [6] x3 + [6]
               p(nub#) = [7] x1 + [7]         
             p(nub#1#) = [7] x1 + [0]         
            p(remove#) = [7] x1 + [5]         
          p(remove#1#) = [7] x2 + [5]         
          p(remove#2#) = [7] x2 + [5]         
                p(c_1) = [1]                  
                p(c_2) = [4]                  
                p(c_3) = [1] x1 + [4]         
                p(c_4) = [1] x1 + [0]         
                p(c_5) = [1]                  
                p(c_6) = [0]                  
                p(c_7) = [2]                  
                p(c_8) = [1] x1 + [0]         
                p(c_9) = [1]                  
               p(c_10) = [0]                  
               p(c_11) = [1] x1 + [1] x2 + [2]
               p(c_12) = [2]                  
               p(c_13) = [2]                  
               p(c_14) = [4] x1 + [4]         
               p(c_15) = [0]                  
               p(c_16) = [1]                  
               p(c_17) = [4] x1 + [1]         
               p(c_18) = [0]                  
               p(c_19) = [1]                  
               p(c_20) = [0]                  
               p(c_21) = [0]                  
               p(c_22) = [1]                  
               p(c_23) = [0]                  
               p(c_24) = [0]                  
               p(c_25) = [0]                  
               p(c_26) = [1]                  
               p(c_27) = [4]                  
               p(c_28) = [0]                  
               p(c_29) = [0]                  
               p(c_30) = [0]                  
               p(c_31) = [1] x1 + [0]         
               p(c_32) = [1]                  
               p(c_33) = [0]                  
               p(c_34) = [2]                  
               p(c_35) = [0]                  
               p(c_36) = [2]                  
               p(c_37) = [2]                  
        
        Following rules are strictly oriented:
        eq#3#(::(@y,@ys),@x,@xs) = [1] @x + [6] @xs + [6]
                                 > [6] @xs + [4]         
                                 = c_8(eq#(@xs,@ys))     
        
        
        Following rules are (at-least) weakly oriented:
                         eq#(@l1,@l2) =  [6] @l1 + [4]                 
                                      >= [6] @l1 + [4]                 
                                      =  c_3(eq#1#(@l1,@l2))           
        
                eq#1#(::(@x,@xs),@l2) =  [6] @x + [6] @xs + [6]        
                                      >= [1] @x + [6] @xs + [6]        
                                      =  c_4(eq#3#(@l2,@x,@xs))        
        
                             nub#(@l) =  [7] @l + [7]                  
                                      >= [7] @l + [0]                  
                                      =  nub#1#(@l)                    
        
                   nub#1#(::(@x,@xs)) =  [7] @x + [7] @xs + [7]        
                                      >= [7] @xs + [7]                 
                                      =  nub#(remove(@x,@xs))          
        
                   nub#1#(::(@x,@xs)) =  [7] @x + [7] @xs + [7]        
                                      >= [7] @x + [5]                  
                                      =  remove#(@x,@xs)               
        
                       remove#(@x,@l) =  [7] @x + [5]                  
                                      >= [7] @x + [5]                  
                                      =  remove#1#(@l,@x)              
        
             remove#1#(::(@y,@ys),@x) =  [7] @x + [5]                  
                                      >= [6] @x + [4]                  
                                      =  eq#(@x,@y)                    
        
             remove#1#(::(@y,@ys),@x) =  [7] @x + [5]                  
                                      >= [7] @x + [5]                  
                                      =  remove#2#(eq(@x,@y),@x,@y,@ys)
        
        remove#2#(#false(),@x,@y,@ys) =  [7] @x + [5]                  
                                      >= [7] @x + [5]                  
                                      =  remove#(@x,@ys)               
        
         remove#2#(#true(),@x,@y,@ys) =  [7] @x + [5]                  
                                      >= [7] @x + [5]                  
                                      =  remove#(@x,@ys)               
        
                        remove(@x,@l) =  [1] @l + [0]                  
                                      >= [1] @l + [0]                  
                                      =  remove#1(@l,@x)               
        
              remove#1(::(@y,@ys),@x) =  [1] @y + [1] @ys + [1]        
                                      >= [1] @y + [1] @ys + [1]        
                                      =  remove#2(eq(@x,@y),@x,@y,@ys) 
        
                   remove#1(nil(),@x) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
        
         remove#2(#false(),@x,@y,@ys) =  [1] @y + [1] @ys + [1]        
                                      >= [1] @y + [1] @ys + [1]        
                                      =  ::(@y,remove(@x,@ys))         
        
          remove#2(#true(),@x,@y,@ys) =  [1] @y + [1] @ys + [1]        
                                      >= [1] @ys + [0]                 
                                      =  remove(@x,@ys)                
        
*** Step 7.b:1.b:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
        - Weak DPs:
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
            remove#(@x,@l) -> remove#1#(@l,@x)
            remove#1#(::(@y,@ys),@x) -> eq#(@x,@y)
            remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys)
            remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys)
            remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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(#and) = {1,2},
            uargs(::) = {2},
            uargs(and) = {1,2},
            uargs(remove#2) = {1},
            uargs(nub#) = {1},
            uargs(remove#2#) = {1},
            uargs(c_3) = {1},
            uargs(c_4) = {1},
            uargs(c_8) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(#0) = [0]                  
                 p(#and) = [1] x1 + [1] x2 + [0]
                  p(#eq) = [0]                  
               p(#equal) = [0]                  
               p(#false) = [0]                  
                 p(#neg) = [1] x1 + [0]         
                 p(#pos) = [1] x1 + [0]         
                   p(#s) = [0]                  
                p(#true) = [0]                  
                   p(::) = [1] x2 + [0]         
                  p(and) = [1] x1 + [1] x2 + [0]
                   p(eq) = [0]                  
                 p(eq#1) = [0]                  
                 p(eq#2) = [0]                  
                 p(eq#3) = [0]                  
                  p(nil) = [0]                  
                  p(nub) = [0]                  
                p(nub#1) = [0]                  
               p(remove) = [0]                  
             p(remove#1) = [0]                  
             p(remove#2) = [1] x1 + [0]         
                p(#and#) = [0]                  
                 p(#eq#) = [0]                  
              p(#equal#) = [0]                  
                 p(and#) = [0]                  
                  p(eq#) = [0]                  
                p(eq#1#) = [1]                  
                p(eq#2#) = [0]                  
                p(eq#3#) = [0]                  
                 p(nub#) = [1] x1 + [0]         
               p(nub#1#) = [0]                  
              p(remove#) = [0]                  
            p(remove#1#) = [0]                  
            p(remove#2#) = [1] x1 + [0]         
                  p(c_1) = [0]                  
                  p(c_2) = [0]                  
                  p(c_3) = [1] x1 + [0]         
                  p(c_4) = [1] x1 + [0]         
                  p(c_5) = [0]                  
                  p(c_6) = [0]                  
                  p(c_7) = [0]                  
                  p(c_8) = [1] x1 + [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) = [0]                  
                 p(c_21) = [0]                  
                 p(c_22) = [0]                  
                 p(c_23) = [0]                  
                 p(c_24) = [0]                  
                 p(c_25) = [0]                  
                 p(c_26) = [0]                  
                 p(c_27) = [0]                  
                 p(c_28) = [0]                  
                 p(c_29) = [0]                  
                 p(c_30) = [0]                  
                 p(c_31) = [0]                  
                 p(c_32) = [0]                  
                 p(c_33) = [0]                  
                 p(c_34) = [0]                  
                 p(c_35) = [0]                  
                 p(c_36) = [0]                  
                 p(c_37) = [0]                  
          
          Following rules are strictly oriented:
          eq#1#(::(@x,@xs),@l2) = [1]                   
                                > [0]                   
                                = c_4(eq#3#(@l2,@x,@xs))
          
          
          Following rules are (at-least) weakly oriented:
                              eq#(@l1,@l2) =  [0]                                
                                           >= [1]                                
                                           =  c_3(eq#1#(@l1,@l2))                
          
                  eq#3#(::(@y,@ys),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  c_8(eq#(@xs,@ys))                  
          
                                  nub#(@l) =  [1] @l + [0]                       
                                           >= [0]                                
                                           =  nub#1#(@l)                         
          
                        nub#1#(::(@x,@xs)) =  [0]                                
                                           >= [0]                                
                                           =  nub#(remove(@x,@xs))               
          
                        nub#1#(::(@x,@xs)) =  [0]                                
                                           >= [0]                                
                                           =  remove#(@x,@xs)                    
          
                            remove#(@x,@l) =  [0]                                
                                           >= [0]                                
                                           =  remove#1#(@l,@x)                   
          
                  remove#1#(::(@y,@ys),@x) =  [0]                                
                                           >= [0]                                
                                           =  eq#(@x,@y)                         
          
                  remove#1#(::(@y,@ys),@x) =  [0]                                
                                           >= [0]                                
                                           =  remove#2#(eq(@x,@y),@x,@y,@ys)     
          
             remove#2#(#false(),@x,@y,@ys) =  [0]                                
                                           >= [0]                                
                                           =  remove#(@x,@ys)                    
          
              remove#2#(#true(),@x,@y,@ys) =  [0]                                
                                           >= [0]                                
                                           =  remove#(@x,@ys)                    
          
                   #and(#false(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#false(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#true(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                     #and(#true(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                            #eq(#0(),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                        #eq(#0(),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#0(),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(#0(),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#neg(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#neg(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                    #eq(#neg(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#pos(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                          #eq(#s(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#s(@x),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          
                  #eq(::(@x_1,@x_2),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                  #eq(nil(),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(nil(),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                             #equal(@x,@y) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                                and(@x,@y) =  [1] @x + [1] @y + [0]              
                                           >= [1] @x + [1] @y + [0]              
                                           =  #and(@x,@y)                        
          
                               eq(@l1,@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#1(@l1,@l2)                      
          
                      eq#1(::(@x,@xs),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#3(@l2,@x,@xs)                   
          
                           eq#1(nil(),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#2(@l2)                          
          
                          eq#2(::(@y,@ys)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                               eq#2(nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                             remove(@x,@l) =  [0]                                
                                           >= [0]                                
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [0]                                
                                           >= [0]                                
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [0]                                
                                           >= [0]                                
                                           =  nil()                              
          
              remove#2(#false(),@x,@y,@ys) =  [0]                                
                                           >= [0]                                
                                           =  ::(@y,remove(@x,@ys))              
          
               remove#2(#true(),@x,@y,@ys) =  [0]                                
                                           >= [0]                                
                                           =  remove(@x,@ys)                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 7.b:1.b:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
        - Weak DPs:
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
            remove#(@x,@l) -> remove#1#(@l,@x)
            remove#1#(::(@y,@ys),@x) -> eq#(@x,@y)
            remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys)
            remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys)
            remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + 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(#and) = {1,2},
            uargs(::) = {2},
            uargs(and) = {1,2},
            uargs(remove#2) = {1},
            uargs(nub#) = {1},
            uargs(remove#2#) = {1},
            uargs(c_3) = {1},
            uargs(c_4) = {1},
            uargs(c_8) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(#0) = [0]                           
                 p(#and) = [1] x1 + [1] x2 + [0]         
                  p(#eq) = [0]                           
               p(#equal) = [0]                           
               p(#false) = [0]                           
                 p(#neg) = [0]                           
                 p(#pos) = [1] x1 + [1]                  
                   p(#s) = [1] x1 + [4]                  
                p(#true) = [0]                           
                   p(::) = [1] x1 + [1] x2 + [4]         
                  p(and) = [1] x1 + [1] x2 + [0]         
                   p(eq) = [0]                           
                 p(eq#1) = [0]                           
                 p(eq#2) = [0]                           
                 p(eq#3) = [0]                           
                  p(nil) = [0]                           
                  p(nub) = [0]                           
                p(nub#1) = [4] x1 + [0]                  
               p(remove) = [1] x2 + [0]                  
             p(remove#1) = [1] x1 + [0]                  
             p(remove#2) = [1] x1 + [1] x3 + [1] x4 + [4]
                p(#and#) = [1] x1 + [0]                  
                 p(#eq#) = [4] x1 + [2] x2 + [0]         
              p(#equal#) = [1] x2 + [4]                  
                 p(and#) = [4] x1 + [1]                  
                  p(eq#) = [1] x1 + [1]                  
                p(eq#1#) = [1] x1 + [0]                  
                p(eq#2#) = [1] x1 + [0]                  
                p(eq#3#) = [1] x2 + [1] x3 + [3]         
                 p(nub#) = [1] x1 + [5]                  
               p(nub#1#) = [1] x1 + [4]                  
              p(remove#) = [1] x1 + [2]                  
            p(remove#1#) = [1] x2 + [2]                  
            p(remove#2#) = [1] x1 + [1] x2 + [2]         
                  p(c_1) = [1] x1 + [1]                  
                  p(c_2) = [1]                           
                  p(c_3) = [1] x1 + [0]                  
                  p(c_4) = [1] x1 + [1]                  
                  p(c_5) = [1] x1 + [0]                  
                  p(c_6) = [4]                           
                  p(c_7) = [1]                           
                  p(c_8) = [1] x1 + [2]                  
                  p(c_9) = [2]                           
                 p(c_10) = [4]                           
                 p(c_11) = [4] x1 + [4]                  
                 p(c_12) = [0]                           
                 p(c_13) = [0]                           
                 p(c_14) = [4] x2 + [4]                  
                 p(c_15) = [0]                           
                 p(c_16) = [1] x1 + [0]                  
                 p(c_17) = [1]                           
                 p(c_18) = [1]                           
                 p(c_19) = [2]                           
                 p(c_20) = [0]                           
                 p(c_21) = [0]                           
                 p(c_22) = [2]                           
                 p(c_23) = [0]                           
                 p(c_24) = [0]                           
                 p(c_25) = [0]                           
                 p(c_26) = [0]                           
                 p(c_27) = [1] x1 + [0]                  
                 p(c_28) = [0]                           
                 p(c_29) = [1]                           
                 p(c_30) = [1]                           
                 p(c_31) = [0]                           
                 p(c_32) = [1]                           
                 p(c_33) = [2]                           
                 p(c_34) = [1] x3 + [1]                  
                 p(c_35) = [1]                           
                 p(c_36) = [0]                           
                 p(c_37) = [0]                           
          
          Following rules are strictly oriented:
          eq#(@l1,@l2) = [1] @l1 + [1]      
                       > [1] @l1 + [0]      
                       = c_3(eq#1#(@l1,@l2))
          
          
          Following rules are (at-least) weakly oriented:
                     eq#1#(::(@x,@xs),@l2) =  [1] @x + [1] @xs + [4]             
                                           >= [1] @x + [1] @xs + [4]             
                                           =  c_4(eq#3#(@l2,@x,@xs))             
          
                  eq#3#(::(@y,@ys),@x,@xs) =  [1] @x + [1] @xs + [3]             
                                           >= [1] @xs + [3]                      
                                           =  c_8(eq#(@xs,@ys))                  
          
                                  nub#(@l) =  [1] @l + [5]                       
                                           >= [1] @l + [4]                       
                                           =  nub#1#(@l)                         
          
                        nub#1#(::(@x,@xs)) =  [1] @x + [1] @xs + [8]             
                                           >= [1] @xs + [5]                      
                                           =  nub#(remove(@x,@xs))               
          
                        nub#1#(::(@x,@xs)) =  [1] @x + [1] @xs + [8]             
                                           >= [1] @x + [2]                       
                                           =  remove#(@x,@xs)                    
          
                            remove#(@x,@l) =  [1] @x + [2]                       
                                           >= [1] @x + [2]                       
                                           =  remove#1#(@l,@x)                   
          
                  remove#1#(::(@y,@ys),@x) =  [1] @x + [2]                       
                                           >= [1] @x + [1]                       
                                           =  eq#(@x,@y)                         
          
                  remove#1#(::(@y,@ys),@x) =  [1] @x + [2]                       
                                           >= [1] @x + [2]                       
                                           =  remove#2#(eq(@x,@y),@x,@y,@ys)     
          
             remove#2#(#false(),@x,@y,@ys) =  [1] @x + [2]                       
                                           >= [1] @x + [2]                       
                                           =  remove#(@x,@ys)                    
          
              remove#2#(#true(),@x,@y,@ys) =  [1] @x + [2]                       
                                           >= [1] @x + [2]                       
                                           =  remove#(@x,@ys)                    
          
                   #and(#false(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#false(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #and(#true(),#false()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                     #and(#true(),#true()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                            #eq(#0(),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                        #eq(#0(),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#0(),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(#0(),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#neg(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#neg(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                    #eq(#neg(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#pos(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#neg(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                    #eq(#pos(@x),#pos(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                          #eq(#s(@x),#0()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                        #eq(#s(@x),#s(@y)) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
          #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
          
                  #eq(::(@x_1,@x_2),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                  #eq(nil(),::(@y_1,@y_2)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                          #eq(nil(),nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                             #equal(@x,@y) =  [0]                                
                                           >= [0]                                
                                           =  #eq(@x,@y)                         
          
                                and(@x,@y) =  [1] @x + [1] @y + [0]              
                                           >= [1] @x + [1] @y + [0]              
                                           =  #and(@x,@y)                        
          
                               eq(@l1,@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#1(@l1,@l2)                      
          
                      eq#1(::(@x,@xs),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#3(@l2,@x,@xs)                   
          
                           eq#1(nil(),@l2) =  [0]                                
                                           >= [0]                                
                                           =  eq#2(@l2)                          
          
                          eq#2(::(@y,@ys)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                               eq#2(nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                             remove(@x,@l) =  [1] @l + [0]                       
                                           >= [1] @l + [0]                       
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [1] @y + [1] @ys + [4]             
                                           >= [1] @y + [1] @ys + [4]             
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [0]                                
                                           >= [0]                                
                                           =  nil()                              
          
              remove#2(#false(),@x,@y,@ys) =  [1] @y + [1] @ys + [4]             
                                           >= [1] @y + [1] @ys + [4]             
                                           =  ::(@y,remove(@x,@ys))              
          
               remove#2(#true(),@x,@y,@ys) =  [1] @y + [1] @ys + [4]             
                                           >= [1] @ys + [0]                      
                                           =  remove(@x,@ys)                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 7.b:1.b:4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
            eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
            eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
            nub#(@l) -> nub#1#(@l)
            nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs))
            nub#1#(::(@x,@xs)) -> remove#(@x,@xs)
            remove#(@x,@l) -> remove#1#(@l,@x)
            remove#1#(::(@y,@ys),@x) -> eq#(@x,@y)
            remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys)
            remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys)
            remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys)
        - Weak TRS:
            #and(#false(),#false()) -> #false()
            #and(#false(),#true()) -> #false()
            #and(#true(),#false()) -> #false()
            #and(#true(),#true()) -> #true()
            #eq(#0(),#0()) -> #true()
            #eq(#0(),#neg(@y)) -> #false()
            #eq(#0(),#pos(@y)) -> #false()
            #eq(#0(),#s(@y)) -> #false()
            #eq(#neg(@x),#0()) -> #false()
            #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
            #eq(#neg(@x),#pos(@y)) -> #false()
            #eq(#pos(@x),#0()) -> #false()
            #eq(#pos(@x),#neg(@y)) -> #false()
            #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
            #eq(#s(@x),#0()) -> #false()
            #eq(#s(@x),#s(@y)) -> #eq(@x,@y)
            #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
            #eq(::(@x_1,@x_2),nil()) -> #false()
            #eq(nil(),::(@y_1,@y_2)) -> #false()
            #eq(nil(),nil()) -> #true()
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            eq#2(::(@y,@ys)) -> #false()
            eq#2(nil()) -> #true()
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            eq#3(nil(),@x,@xs) -> #false()
            remove(@x,@l) -> remove#1(@l,@x)
            remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
            remove#1(nil(),@x) -> nil()
            remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
            remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
        - Signature:
            {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
            ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
            ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
            ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
            ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
            ,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
            ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))