WORST_CASE(?,O(n^2))
* Step 1: WeightGap WORST_CASE(?,O(n^2))
    + 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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant 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(nub) = {1},
            uargs(remove#2) = {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 + [5]         
                 p(and) = [1] x1 + [1] x2 + [0]
                  p(eq) = [4]                  
                p(eq#1) = [0]                  
                p(eq#2) = [0]                  
                p(eq#3) = [0]                  
                 p(nil) = [0]                  
                 p(nub) = [1] x1 + [0]         
               p(nub#1) = [1] x1 + [0]         
              p(remove) = [0]                  
            p(remove#1) = [0]                  
            p(remove#2) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          eq(@l1,@l2) = [4]          
                      > [0]          
                      = eq#1(@l1,@l2)
          
          
          Following rules are (at-least) weakly oriented:
                   #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#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]                                
                                           >= [4]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                                   nub(@l) =  [1] @l + [0]                       
                                           >= [1] @l + [0]                       
                                           =  nub#1(@l)                          
          
                         nub#1(::(@x,@xs)) =  [1] @xs + [5]                      
                                           >= [5]                                
                                           =  ::(@x,nub(remove(@x,@xs)))         
          
                              nub#1(nil()) =  [0]                                
                                           >= [0]                                
                                           =  nil()                              
          
                             remove(@x,@l) =  [0]                                
                                           >= [0]                                
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [0]                                
                                           >= [4]                                
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [0]                                
                                           >= [0]                                
                                           =  nil()                              
          
              remove#2(#false(),@x,@y,@ys) =  [0]                                
                                           >= [5]                                
                                           =  ::(@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 2: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            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()
            eq(@l1,@l2) -> eq#1(@l1,@l2)
        - 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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant 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(nub) = {1},
            uargs(remove#2) = {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) = [0]                  
                  p(#s) = [1] x1 + [0]         
               p(#true) = [0]                  
                  p(::) = [1] x2 + [7]         
                 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) = [1] x1 + [0]         
               p(nub#1) = [1] x1 + [2]         
              p(remove) = [0]                  
            p(remove#1) = [0]                  
            p(remove#2) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          nub#1(::(@x,@xs)) = [1] @xs + [9]             
                            > [7]                       
                            = ::(@x,nub(remove(@x,@xs)))
          
               nub#1(nil()) = [2]                       
                            > [0]                       
                            = nil()                     
          
          
          Following rules are (at-least) weakly oriented:
                   #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()                           
          
                                   nub(@l) =  [1] @l + [0]                       
                                           >= [1] @l + [2]                       
                                           =  nub#1(@l)                          
          
                             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]                                
                                           >= [7]                                
                                           =  ::(@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 3: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            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)
            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()
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
        - 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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant 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(nub) = {1},
            uargs(remove#2) = {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 + [0]         
                  p(#s) = [1] x1 + [0]         
               p(#true) = [0]                  
                  p(::) = [1] x2 + [0]         
                 p(and) = [1] x1 + [1] x2 + [0]
                  p(eq) = [3]                  
                p(eq#1) = [3]                  
                p(eq#2) = [0]                  
                p(eq#3) = [0]                  
                 p(nil) = [5]                  
                 p(nub) = [1] x1 + [5]         
               p(nub#1) = [5]                  
              p(remove) = [0]                  
            p(remove#1) = [0]                  
            p(remove#2) = [1] x1 + [5]         
          
          Following rules are strictly oriented:
                  eq#1(::(@x,@xs),@l2) = [3]                  
                                       > [0]                  
                                       = eq#3(@l2,@x,@xs)     
          
                       eq#1(nil(),@l2) = [3]                  
                                       > [0]                  
                                       = eq#2(@l2)            
          
          remove#2(#false(),@x,@y,@ys) = [5]                  
                                       > [0]                  
                                       = ::(@y,remove(@x,@ys))
          
           remove#2(#true(),@x,@y,@ys) = [5]                  
                                       > [0]                  
                                       = remove(@x,@ys)       
          
          
          Following rules are (at-least) weakly oriented:
                   #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) =  [3]                                
                                           >= [3]                                
                                           =  eq#1(@l1,@l2)                      
          
                          eq#2(::(@y,@ys)) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                               eq#2(nil()) =  [0]                                
                                           >= [0]                                
                                           =  #true()                            
          
                   eq#3(::(@y,@ys),@x,@xs) =  [0]                                
                                           >= [3]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                                   nub(@l) =  [1] @l + [5]                       
                                           >= [5]                                
                                           =  nub#1(@l)                          
          
                         nub#1(::(@x,@xs)) =  [5]                                
                                           >= [5]                                
                                           =  ::(@x,nub(remove(@x,@xs)))         
          
                              nub#1(nil()) =  [5]                                
                                           >= [5]                                
                                           =  nil()                              
          
                             remove(@x,@l) =  [0]                                
                                           >= [0]                                
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [0]                                
                                           >= [8]                                
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [0]                                
                                           >= [5]                                
                                           =  nil()                              
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            #equal(@x,@y) -> #eq(@x,@y)
            and(@x,@y) -> #and(@x,@y)
            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)
            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()
        - 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()
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> 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} / {#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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant 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(nub) = {1},
            uargs(remove#2) = {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) = [1]                  
              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) = [1] x1 + [0]         
               p(nub#1) = [0]                  
              p(remove) = [0]                  
            p(remove#1) = [0]                  
            p(remove#2) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          #equal(@x,@y) = [1]       
                        > [0]       
                        = #eq(@x,@y)
          
          
          Following rules are (at-least) weakly oriented:
                   #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()                            
          
                                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]                                
                                           >= [1]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                                   nub(@l) =  [1] @l + [0]                       
                                           >= [0]                                
                                           =  nub#1(@l)                          
          
                         nub#1(::(@x,@xs)) =  [0]                                
                                           >= [0]                                
                                           =  ::(@x,nub(remove(@x,@xs)))         
          
                              nub#1(nil()) =  [0]                                
                                           >= [0]                                
                                           =  nil()                              
          
                             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 5: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            and(@x,@y) -> #and(@x,@y)
            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)
            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()
        - 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)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> 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} / {#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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant 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(nub) = {1},
            uargs(remove#2) = {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 + [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) = [1] x1 + [0]         
               p(nub#1) = [0]                  
              p(remove) = [0]                  
            p(remove#1) = [5]                  
            p(remove#2) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          remove#1(::(@y,@ys),@x) = [5]                          
                                  > [0]                          
                                  = remove#2(eq(@x,@y),@x,@y,@ys)
          
               remove#1(nil(),@x) = [5]                          
                                  > [0]                          
                                  = nil()                        
          
          
          Following rules are (at-least) weakly oriented:
                   #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()                           
          
                                   nub(@l) =  [1] @l + [0]                       
                                           >= [0]                                
                                           =  nub#1(@l)                          
          
                         nub#1(::(@x,@xs)) =  [0]                                
                                           >= [0]                                
                                           =  ::(@x,nub(remove(@x,@xs)))         
          
                              nub#1(nil()) =  [0]                                
                                           >= [0]                                
                                           =  nil()                              
          
                             remove(@x,@l) =  [0]                                
                                           >= [5]                                
                                           =  remove#1(@l,@x)                    
          
              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 6: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            and(@x,@y) -> #and(@x,@y)
            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)
            remove(@x,@l) -> remove#1(@l,@x)
        - 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)
            eq(@l1,@l2) -> eq#1(@l1,@l2)
            eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
            eq#1(nil(),@l2) -> eq#2(@l2)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            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} / {#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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant 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(nub) = {1},
            uargs(remove#2) = {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) = [0]                  
                  p(#s) = [1] x1 + [0]         
               p(#true) = [0]                  
                  p(::) = [1] x2 + [0]         
                 p(and) = [1] x1 + [1] x2 + [0]
                  p(eq) = [1]                  
                p(eq#1) = [1]                  
                p(eq#2) = [1]                  
                p(eq#3) = [1]                  
                 p(nil) = [6]                  
                 p(nub) = [1] x1 + [0]         
               p(nub#1) = [1] x1 + [0]         
              p(remove) = [0]                  
            p(remove#1) = [6]                  
            p(remove#2) = [1] x1 + [5]         
          
          Following rules are strictly oriented:
            eq#2(::(@y,@ys)) = [1]     
                             > [0]     
                             = #false()
          
                 eq#2(nil()) = [1]     
                             > [0]     
                             = #true() 
          
          eq#3(nil(),@x,@xs) = [1]     
                             > [0]     
                             = #false()
          
          
          Following rules are (at-least) weakly oriented:
                   #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) =  [1]                                
                                           >= [1]                                
                                           =  eq#1(@l1,@l2)                      
          
                      eq#1(::(@x,@xs),@l2) =  [1]                                
                                           >= [1]                                
                                           =  eq#3(@l2,@x,@xs)                   
          
                           eq#1(nil(),@l2) =  [1]                                
                                           >= [1]                                
                                           =  eq#2(@l2)                          
          
                   eq#3(::(@y,@ys),@x,@xs) =  [1]                                
                                           >= [1]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                                   nub(@l) =  [1] @l + [0]                       
                                           >= [1] @l + [0]                       
                                           =  nub#1(@l)                          
          
                         nub#1(::(@x,@xs)) =  [1] @xs + [0]                      
                                           >= [0]                                
                                           =  ::(@x,nub(remove(@x,@xs)))         
          
                              nub#1(nil()) =  [6]                                
                                           >= [6]                                
                                           =  nil()                              
          
                             remove(@x,@l) =  [0]                                
                                           >= [6]                                
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [6]                                
                                           >= [6]                                
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [6]                                
                                           >= [6]                                
                                           =  nil()                              
          
              remove#2(#false(),@x,@y,@ys) =  [5]                                
                                           >= [0]                                
                                           =  ::(@y,remove(@x,@ys))              
          
               remove#2(#true(),@x,@y,@ys) =  [5]                                
                                           >= [0]                                
                                           =  remove(@x,@ys)                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            and(@x,@y) -> #and(@x,@y)
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            nub(@l) -> nub#1(@l)
            remove(@x,@l) -> remove#1(@l,@x)
        - 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)
            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(nil(),@x,@xs) -> #false()
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            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} / {#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:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant 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(nub) = {1},
            uargs(remove#2) = {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) = [1] x1 + [0]         
               p(#true) = [0]                  
                  p(::) = [1] x2 + [0]         
                 p(and) = [1] x1 + [1] x2 + [1]
                  p(eq) = [1]                  
                p(eq#1) = [0]                  
                p(eq#2) = [0]                  
                p(eq#3) = [0]                  
                 p(nil) = [1]                  
                 p(nub) = [1] x1 + [0]         
               p(nub#1) = [1]                  
              p(remove) = [1]                  
            p(remove#1) = [2]                  
            p(remove#2) = [1] x1 + [1]         
          
          Following rules are strictly oriented:
          and(@x,@y) = [1] @x + [1] @y + [1]
                     > [1] @x + [1] @y + [0]
                     = #and(@x,@y)          
          
          
          Following rules are (at-least) weakly oriented:
                   #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)                         
          
                               eq(@l1,@l2) =  [1]                                
                                           >= [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]                                
                                           >= [2]                                
                                           =  and(#equal(@x,@y),eq(@xs,@ys))     
          
                        eq#3(nil(),@x,@xs) =  [0]                                
                                           >= [0]                                
                                           =  #false()                           
          
                                   nub(@l) =  [1] @l + [0]                       
                                           >= [1]                                
                                           =  nub#1(@l)                          
          
                         nub#1(::(@x,@xs)) =  [1]                                
                                           >= [1]                                
                                           =  ::(@x,nub(remove(@x,@xs)))         
          
                              nub#1(nil()) =  [1]                                
                                           >= [1]                                
                                           =  nil()                              
          
                             remove(@x,@l) =  [1]                                
                                           >= [2]                                
                                           =  remove#1(@l,@x)                    
          
                   remove#1(::(@y,@ys),@x) =  [2]                                
                                           >= [2]                                
                                           =  remove#2(eq(@x,@y),@x,@y,@ys)      
          
                        remove#1(nil(),@x) =  [2]                                
                                           >= [1]                                
                                           =  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 8: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            nub(@l) -> nub#1(@l)
            remove(@x,@l) -> remove#1(@l,@x)
        - 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(nil(),@x,@xs) -> #false()
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            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} / {#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:
        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(#and) = {1,2},
          uargs(::) = {2},
          uargs(and) = {1,2},
          uargs(nub) = {1},
          uargs(remove#2) = {1}
        
        Following symbols are considered usable:
          {#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) = [2] x1 + [2] x2 + [0]
               p(#eq) = [0]                  
            p(#equal) = [0]                  
            p(#false) = [0]                  
              p(#neg) = [1]                  
              p(#pos) = [1]                  
                p(#s) = [1]                  
             p(#true) = [0]                  
                p(::) = [1] x2 + [1]         
               p(and) = [4] x1 + [2] x2 + [0]
                p(eq) = [0]                  
              p(eq#1) = [0]                  
              p(eq#2) = [0]                  
              p(eq#3) = [0]                  
               p(nil) = [0]                  
               p(nub) = [3] x1 + [4]         
             p(nub#1) = [3] x1 + [2]         
            p(remove) = [1] x2 + [0]         
          p(remove#1) = [1] x1 + [0]         
          p(remove#2) = [4] x1 + [1] x4 + [1]
        
        Following rules are strictly oriented:
        nub(@l) = [3] @l + [4]
                > [3] @l + [2]
                = nub#1(@l)   
        
        
        Following rules are (at-least) weakly oriented:
                 #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) =  [4] @x + [2] @y + [0]              
                                         >= [2] @x + [2] @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()                           
        
                       nub#1(::(@x,@xs)) =  [3] @xs + [5]                      
                                         >= [3] @xs + [5]                      
                                         =  ::(@x,nub(remove(@x,@xs)))         
        
                            nub#1(nil()) =  [2]                                
                                         >= [0]                                
                                         =  nil()                              
        
                           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) =  [0]                                
                                         >= [0]                                
                                         =  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)                     
        
* Step 9: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
            remove(@x,@l) -> remove#1(@l,@x)
        - 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(nil(),@x,@xs) -> #false()
            nub(@l) -> nub#1(@l)
            nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
            nub#1(nil()) -> nil()
            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} / {#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:
        NaturalMI {miDimension = 2, miDegree = 2, 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(#and) = {1,2},
          uargs(::) = {2},
          uargs(and) = {1,2},
          uargs(nub) = {1},
          uargs(remove#2) = {1}
        
        Following symbols are considered usable:
          {#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) = [2]                      
                        [0]                      
              p(#and) = [2 0] x1 + [2 0] x2 + [0]
                        [2 0]      [2 1]      [0]
               p(#eq) = [0 0] x2 + [0]           
                        [2 0]      [1]           
            p(#equal) = [0 0] x1 + [0 0] x2 + [0]
                        [0 2]      [2 2]      [2]
            p(#false) = [0]                      
                        [0]                      
              p(#neg) = [1 2] x1 + [2]           
                        [0 1]      [0]           
              p(#pos) = [1 2] x1 + [2]           
                        [0 0]      [0]           
                p(#s) = [1 0] x1 + [3]           
                        [0 0]      [0]           
             p(#true) = [0]                      
                        [0]                      
                p(::) = [1 2] x2 + [0]           
                        [0 1]      [1]           
               p(and) = [2 0] x1 + [2 0] x2 + [0]
                        [2 0]      [2 2]      [0]
                p(eq) = [0]                      
                        [0]                      
              p(eq#1) = [0]                      
                        [0]                      
              p(eq#2) = [0]                      
                        [0]                      
              p(eq#3) = [0]                      
                        [0]                      
               p(nil) = [0]                      
                        [0]                      
               p(nub) = [2 2] x1 + [3]           
                        [0 1]      [0]           
             p(nub#1) = [2 2] x1 + [3]           
                        [0 1]      [0]           
            p(remove) = [1 1] x2 + [1]           
                        [0 1]      [0]           
          p(remove#1) = [1 1] x1 + [0]           
                        [0 1]      [0]           
          p(remove#2) = [1 0] x1 + [1 3] x4 + [1]
                        [0 0]      [0 1]      [1]
        
        Following rules are strictly oriented:
        remove(@x,@l) = [1 1] @l + [1] 
                        [0 1]      [0] 
                      > [1 1] @l + [0] 
                        [0 1]      [0] 
                      = remove#1(@l,@x)
        
        
        Following rules are (at-least) weakly oriented:
                 #and(#false(),#false()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #and(#false(),#true()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #and(#true(),#false()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                   #and(#true(),#true()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                          #eq(#0(),#0()) =  [0]                                
                                            [5]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                      #eq(#0(),#neg(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [5]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#0(),#pos(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [5]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                        #eq(#0(),#s(@y)) =  [0 0] @y + [0]                     
                                            [2 0]      [7]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#neg(@x),#0()) =  [0]                                
                                            [5]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #eq(#neg(@x),#neg(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [5]                     
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [1]                     
                                         =  #eq(@x,@y)                         
        
                  #eq(#neg(@x),#pos(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [5]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#pos(@x),#0()) =  [0]                                
                                            [5]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #eq(#pos(@x),#neg(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [5]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #eq(#pos(@x),#pos(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [5]                     
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [1]                     
                                         =  #eq(@x,@y)                         
        
                        #eq(#s(@x),#0()) =  [0]                                
                                            [5]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#s(@x),#s(@y)) =  [0 0] @y + [0]                     
                                            [2 0]      [7]                     
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [1]                     
                                         =  #eq(@x,@y)                         
        
        #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0 0] @y_2 + [0]                   
                                            [2 4]        [1]                   
                                         >= [0 0] @y_2 + [0]                   
                                            [2 0]        [1]                   
                                         =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
        
                #eq(::(@x_1,@x_2),nil()) =  [0]                                
                                            [1]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                #eq(nil(),::(@y_1,@y_2)) =  [0 0] @y_2 + [0]                   
                                            [2 4]        [1]                   
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                        #eq(nil(),nil()) =  [0]                                
                                            [1]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                           #equal(@x,@y) =  [0 0] @x + [0 0] @y + [0]          
                                            [0 2]      [2 2]      [2]          
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [1]                     
                                         =  #eq(@x,@y)                         
        
                              and(@x,@y) =  [2 0] @x + [2 0] @y + [0]          
                                            [2 0]      [2 2]      [0]          
                                         >= [2 0] @x + [2 0] @y + [0]          
                                            [2 0]      [2 1]      [0]          
                                         =  #and(@x,@y)                        
        
                             eq(@l1,@l2) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  eq#1(@l1,@l2)                      
        
                    eq#1(::(@x,@xs),@l2) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  eq#3(@l2,@x,@xs)                   
        
                         eq#1(nil(),@l2) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  eq#2(@l2)                          
        
                        eq#2(::(@y,@ys)) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                             eq#2(nil()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                 eq#3(::(@y,@ys),@x,@xs) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  and(#equal(@x,@y),eq(@xs,@ys))     
        
                      eq#3(nil(),@x,@xs) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                                 nub(@l) =  [2 2] @l + [3]                     
                                            [0 1]      [0]                     
                                         >= [2 2] @l + [3]                     
                                            [0 1]      [0]                     
                                         =  nub#1(@l)                          
        
                       nub#1(::(@x,@xs)) =  [2 6] @xs + [5]                    
                                            [0 1]       [1]                    
                                         >= [2 6] @xs + [5]                    
                                            [0 1]       [1]                    
                                         =  ::(@x,nub(remove(@x,@xs)))         
        
                            nub#1(nil()) =  [3]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  nil()                              
        
                 remove#1(::(@y,@ys),@x) =  [1 3] @ys + [1]                    
                                            [0 1]       [1]                    
                                         >= [1 3] @ys + [1]                    
                                            [0 1]       [1]                    
                                         =  remove#2(eq(@x,@y),@x,@y,@ys)      
        
                      remove#1(nil(),@x) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  nil()                              
        
            remove#2(#false(),@x,@y,@ys) =  [1 3] @ys + [1]                    
                                            [0 1]       [1]                    
                                         >= [1 3] @ys + [1]                    
                                            [0 1]       [1]                    
                                         =  ::(@y,remove(@x,@ys))              
        
             remove#2(#true(),@x,@y,@ys) =  [1 3] @ys + [1]                    
                                            [0 1]       [1]                    
                                         >= [1 1] @ys + [1]                    
                                            [0 1]       [0]                    
                                         =  remove(@x,@ys)                     
        
* Step 10: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@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(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} / {#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:
        NaturalMI {miDimension = 2, miDegree = 2, 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(#and) = {1,2},
          uargs(::) = {2},
          uargs(and) = {1,2},
          uargs(nub) = {1},
          uargs(remove#2) = {1}
        
        Following symbols are considered usable:
          {#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) = [1]                                 
                        [0]                                 
              p(#and) = [2 0] x1 + [1 0] x2 + [0]           
                        [0 0]      [0 0]      [0]           
               p(#eq) = [0 0] x2 + [0]                      
                        [2 0]      [2]                      
            p(#equal) = [0 0] x2 + [0]                      
                        [2 1]      [2]                      
            p(#false) = [0]                                 
                        [0]                                 
              p(#neg) = [1 2] x1 + [2]                      
                        [0 0]      [1]                      
              p(#pos) = [1 0] x1 + [1]                      
                        [0 0]      [0]                      
                p(#s) = [1 2] x1 + [0]                      
                        [0 1]      [1]                      
             p(#true) = [0]                                 
                        [0]                                 
                p(::) = [0 0] x1 + [1 2] x2 + [0]           
                        [0 1]      [0 1]      [2]           
               p(and) = [2 0] x1 + [1 0] x2 + [0]           
                        [0 0]      [0 2]      [0]           
                p(eq) = [0 1] x2 + [2]                      
                        [0 0]      [0]                      
              p(eq#1) = [0 1] x2 + [2]                      
                        [0 0]      [0]                      
              p(eq#2) = [0 1] x1 + [2]                      
                        [0 0]      [0]                      
              p(eq#3) = [0 1] x1 + [2]                      
                        [0 0]      [0]                      
               p(nil) = [0]                                 
                        [0]                                 
               p(nub) = [2 0] x1 + [2]                      
                        [0 1]      [0]                      
             p(nub#1) = [2 0] x1 + [2]                      
                        [0 1]      [0]                      
            p(remove) = [1 1] x2 + [0]                      
                        [0 1]      [0]                      
          p(remove#1) = [1 1] x1 + [0]                      
                        [0 1]      [0]                      
          p(remove#2) = [1 0] x1 + [0 0] x3 + [1 3] x4 + [0]
                        [0 0]      [0 1]      [0 1]      [2]
        
        Following rules are strictly oriented:
        eq#3(::(@y,@ys),@x,@xs) = [0 1] @y + [0 1] @ys + [4]    
                                  [0 0]      [0 0]       [0]    
                                > [0 1] @ys + [2]               
                                  [0 0]       [0]               
                                = and(#equal(@x,@y),eq(@xs,@ys))
        
        
        Following rules are (at-least) weakly oriented:
                 #and(#false(),#false()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #and(#false(),#true()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #and(#true(),#false()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                   #and(#true(),#true()) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                          #eq(#0(),#0()) =  [0]                                
                                            [4]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                      #eq(#0(),#neg(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [6]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#0(),#pos(@y)) =  [0 0] @y + [0]                     
                                            [2 0]      [4]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                        #eq(#0(),#s(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [2]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#neg(@x),#0()) =  [0]                                
                                            [4]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #eq(#neg(@x),#neg(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [6]                     
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [2]                     
                                         =  #eq(@x,@y)                         
        
                  #eq(#neg(@x),#pos(@y)) =  [0 0] @y + [0]                     
                                            [2 0]      [4]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#pos(@x),#0()) =  [0]                                
                                            [4]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #eq(#pos(@x),#neg(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [6]                     
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                  #eq(#pos(@x),#pos(@y)) =  [0 0] @y + [0]                     
                                            [2 0]      [4]                     
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [2]                     
                                         =  #eq(@x,@y)                         
        
                        #eq(#s(@x),#0()) =  [0]                                
                                            [4]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                      #eq(#s(@x),#s(@y)) =  [0 0] @y + [0]                     
                                            [2 4]      [2]                     
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [2]                     
                                         =  #eq(@x,@y)                         
        
        #eq(::(@x_1,@x_2),::(@y_1,@y_2)) =  [0 0] @y_2 + [0]                   
                                            [2 4]        [2]                   
                                         >= [0]                                
                                            [0]                                
                                         =  #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
        
                #eq(::(@x_1,@x_2),nil()) =  [0]                                
                                            [2]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                #eq(nil(),::(@y_1,@y_2)) =  [0 0] @y_2 + [0]                   
                                            [2 4]        [2]                   
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                        #eq(nil(),nil()) =  [0]                                
                                            [2]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                           #equal(@x,@y) =  [0 0] @y + [0]                     
                                            [2 1]      [2]                     
                                         >= [0 0] @y + [0]                     
                                            [2 0]      [2]                     
                                         =  #eq(@x,@y)                         
        
                              and(@x,@y) =  [2 0] @x + [1 0] @y + [0]          
                                            [0 0]      [0 2]      [0]          
                                         >= [2 0] @x + [1 0] @y + [0]          
                                            [0 0]      [0 0]      [0]          
                                         =  #and(@x,@y)                        
        
                             eq(@l1,@l2) =  [0 1] @l2 + [2]                    
                                            [0 0]       [0]                    
                                         >= [0 1] @l2 + [2]                    
                                            [0 0]       [0]                    
                                         =  eq#1(@l1,@l2)                      
        
                    eq#1(::(@x,@xs),@l2) =  [0 1] @l2 + [2]                    
                                            [0 0]       [0]                    
                                         >= [0 1] @l2 + [2]                    
                                            [0 0]       [0]                    
                                         =  eq#3(@l2,@x,@xs)                   
        
                         eq#1(nil(),@l2) =  [0 1] @l2 + [2]                    
                                            [0 0]       [0]                    
                                         >= [0 1] @l2 + [2]                    
                                            [0 0]       [0]                    
                                         =  eq#2(@l2)                          
        
                        eq#2(::(@y,@ys)) =  [0 1] @y + [0 1] @ys + [4]         
                                            [0 0]      [0 0]       [0]         
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                             eq#2(nil()) =  [2]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #true()                            
        
                      eq#3(nil(),@x,@xs) =  [2]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  #false()                           
        
                                 nub(@l) =  [2 0] @l + [2]                     
                                            [0 1]      [0]                     
                                         >= [2 0] @l + [2]                     
                                            [0 1]      [0]                     
                                         =  nub#1(@l)                          
        
                       nub#1(::(@x,@xs)) =  [0 0] @x + [2 4] @xs + [2]         
                                            [0 1]      [0 1]       [2]         
                                         >= [0 0] @x + [2 4] @xs + [2]         
                                            [0 1]      [0 1]       [2]         
                                         =  ::(@x,nub(remove(@x,@xs)))         
        
                            nub#1(nil()) =  [2]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  nil()                              
        
                           remove(@x,@l) =  [1 1] @l + [0]                     
                                            [0 1]      [0]                     
                                         >= [1 1] @l + [0]                     
                                            [0 1]      [0]                     
                                         =  remove#1(@l,@x)                    
        
                 remove#1(::(@y,@ys),@x) =  [0 1] @y + [1 3] @ys + [2]         
                                            [0 1]      [0 1]       [2]         
                                         >= [0 1] @y + [1 3] @ys + [2]         
                                            [0 1]      [0 1]       [2]         
                                         =  remove#2(eq(@x,@y),@x,@y,@ys)      
        
                      remove#1(nil(),@x) =  [0]                                
                                            [0]                                
                                         >= [0]                                
                                            [0]                                
                                         =  nil()                              
        
            remove#2(#false(),@x,@y,@ys) =  [0 0] @y + [1 3] @ys + [0]         
                                            [0 1]      [0 1]       [2]         
                                         >= [0 0] @y + [1 3] @ys + [0]         
                                            [0 1]      [0 1]       [2]         
                                         =  ::(@y,remove(@x,@ys))              
        
             remove#2(#true(),@x,@y,@ys) =  [0 0] @y + [1 3] @ys + [0]         
                                            [0 1]      [0 1]       [2]         
                                         >= [1 1] @ys + [0]                    
                                            [0 1]       [0]                    
                                         =  remove(@x,@ys)                     
        
* Step 11: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - 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} / {#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:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))