* Step 1: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            __(nil(),X) -> X
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [3]         
                 p(U21) = [1] x1 + [1] x2 + [0]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [2]         
                 p(U41) = [1] x1 + [1] x2 + [0]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [4]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [0]
                 p(U72) = [1] x1 + [0]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [1]
                   p(a) = [0]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [0]                  
                   p(i) = [0]                  
              p(isList) = [1] x1 + [0]         
            p(isNeList) = [1] x1 + [0]         
             p(isNePal) = [1] x1 + [0]         
               p(isPal) = [1] x1 + [0]         
               p(isQid) = [1] x1 + [0]         
               p(n____) = [1] x1 + [1] x2 + [0]
                p(n__a) = [0]                  
                p(n__e) = [7]                  
                p(n__i) = [0]                  
              p(n__nil) = [0]                  
                p(n__o) = [0]                  
                p(n__u) = [0]                  
                 p(nil) = [0]                  
                   p(o) = [0]                  
                  p(tt) = [0]                  
                   p(u) = [0]                  
          
          Following rules are strictly oriented:
                          U11(tt()) = [3]                                
                                    > [0]                                
                                    = tt()                               
          
                          U31(tt()) = [2]                                
                                    > [0]                                
                                    = tt()                               
          
                       U51(tt(),V2) = [1] V2 + [4]                       
                                    > [1] V2 + [0]                       
                                    = U52(isList(activate(V2)))          
          
                        __(X,nil()) = [1] X + [1]                        
                                    > [1] X + [0]                        
                                    = X                                  
          
                          __(X1,X2) = [1] X1 + [1] X2 + [1]              
                                    > [1] X1 + [1] X2 + [0]              
                                    = n____(X1,X2)                       
          
                        __(nil(),X) = [1] X + [1]                        
                                    > [1] X + [0]                        
                                    = X                                  
          
                   activate(n__e()) = [7]                                
                                    > [0]                                
                                    = e()                                
          
          isNePal(n____(I,__(P,I))) = [2] I + [1] P + [1]                
                                    > [1] I + [1] P + [0]                
                                    = U71(isQid(activate(I)),activate(P))
          
                      isQid(n__e()) = [7]                                
                                    > [0]                                
                                    = tt()                               
          
          
          Following rules are (at-least) weakly oriented:
                    U21(tt(),V2) =  [1] V2 + [0]                            
                                 >= [1] V2 + [0]                            
                                 =  U22(isList(activate(V2)))               
          
                       U22(tt()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                    U41(tt(),V2) =  [1] V2 + [0]                            
                                 >= [1] V2 + [0]                            
                                 =  U42(isNeList(activate(V2)))             
          
                       U42(tt()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                       U52(tt()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                       U61(tt()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                     U71(tt(),P) =  [1] P + [0]                             
                                 >= [1] P + [0]                             
                                 =  U72(isPal(activate(P)))                 
          
                       U72(tt()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                       U81(tt()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                   __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [2]             
                                 >= [1] X + [1] Y + [1] Z + [2]             
                                 =  __(X,__(Y,Z))                           
          
                             a() =  [0]                                     
                                 >= [0]                                     
                                 =  n__a()                                  
          
                     activate(X) =  [1] X + [0]                             
                                 >= [1] X + [0]                             
                                 =  X                                       
          
          activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [0]                   
                                 >= [1] X1 + [1] X2 + [1]                   
                                 =  __(X1,X2)                               
          
                activate(n__a()) =  [0]                                     
                                 >= [0]                                     
                                 =  a()                                     
          
                activate(n__i()) =  [0]                                     
                                 >= [0]                                     
                                 =  i()                                     
          
              activate(n__nil()) =  [0]                                     
                                 >= [0]                                     
                                 =  nil()                                   
          
                activate(n__o()) =  [0]                                     
                                 >= [0]                                     
                                 =  o()                                     
          
                activate(n__u()) =  [0]                                     
                                 >= [0]                                     
                                 =  u()                                     
          
                             e() =  [0]                                     
                                 >= [7]                                     
                                 =  n__e()                                  
          
                             i() =  [0]                                     
                                 >= [0]                                     
                                 =  n__i()                                  
          
                       isList(V) =  [1] V + [0]                             
                                 >= [1] V + [3]                             
                                 =  U11(isNeList(activate(V)))              
          
            isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                   
                                 >= [1] V1 + [1] V2 + [0]                   
                                 =  U21(isList(activate(V1)),activate(V2))  
          
                isList(n__nil()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                     isNeList(V) =  [1] V + [0]                             
                                 >= [1] V + [2]                             
                                 =  U31(isQid(activate(V)))                 
          
          isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                   
                                 >= [1] V1 + [1] V2 + [0]                   
                                 =  U41(isList(activate(V1)),activate(V2))  
          
          isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                   
                                 >= [1] V1 + [1] V2 + [4]                   
                                 =  U51(isNeList(activate(V1)),activate(V2))
          
                      isNePal(V) =  [1] V + [0]                             
                                 >= [1] V + [0]                             
                                 =  U61(isQid(activate(V)))                 
          
                        isPal(V) =  [1] V + [0]                             
                                 >= [1] V + [0]                             
                                 =  U81(isNePal(activate(V)))               
          
                 isPal(n__nil()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                   isQid(n__a()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                   isQid(n__i()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                   isQid(n__o()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                   isQid(n__u()) =  [0]                                     
                                 >= [0]                                     
                                 =  tt()                                    
          
                           nil() =  [0]                                     
                                 >= [0]                                     
                                 =  n__nil()                                
          
                             o() =  [0]                                     
                                 >= [0]                                     
                                 =  n__o()                                  
          
                             u() =  [0]                                     
                                 >= [0]                                     
                                 =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Weak TRS:
            U11(tt()) -> tt()
            U31(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__e()) -> e()
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isQid(n__e()) -> tt()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [0]         
                 p(U21) = [1] x1 + [1] x2 + [0]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [0]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [7]
                 p(U52) = [1] x1 + [7]         
                 p(U61) = [1] x1 + [7]         
                 p(U71) = [1] x1 + [1] x2 + [0]
                 p(U72) = [1] x1 + [0]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [0]
                   p(a) = [0]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [0]                  
                   p(i) = [0]                  
              p(isList) = [1] x1 + [0]         
            p(isNeList) = [1] x1 + [0]         
             p(isNePal) = [1] x1 + [0]         
               p(isPal) = [1] x1 + [0]         
               p(isQid) = [1] x1 + [0]         
               p(n____) = [1] x1 + [1] x2 + [0]
                p(n__a) = [5]                  
                p(n__e) = [0]                  
                p(n__i) = [0]                  
              p(n__nil) = [0]                  
                p(n__o) = [0]                  
                p(n__u) = [0]                  
                 p(nil) = [0]                  
                   p(o) = [0]                  
                  p(tt) = [0]                  
                   p(u) = [1]                  
          
          Following rules are strictly oriented:
                 U52(tt()) = [7]   
                           > [0]   
                           = tt()  
          
                 U61(tt()) = [7]   
                           > [0]   
                           = tt()  
          
          activate(n__a()) = [5]   
                           > [0]   
                           = a()   
          
             isQid(n__a()) = [5]   
                           > [0]   
                           = tt()  
          
                       u() = [1]   
                           > [0]   
                           = n__u()
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [0]                            
                                    >= [1] V2 + [0]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [0]                            
                                    >= [1] V2 + [0]                            
                                    =  U42(isNeList(activate(V2)))             
          
                          U42(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [7]                            
                                    >= [1] V2 + [7]                            
                                    =  U52(isList(activate(V2)))               
          
                        U71(tt(),P) =  [1] P + [0]                             
                                    >= [1] P + [0]                             
                                    =  U72(isPal(activate(P)))                 
          
                          U72(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U81(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [0]                   
                                    >= [1] X1 + [1] X2 + [0]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [0]             
                                    >= [1] X + [1] Y + [1] Z + [0]             
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [0]                                     
                                    >= [5]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [0]                   
                                    >= [1] X1 + [1] X2 + [0]                   
                                    =  __(X1,X2)                               
          
                   activate(n__e()) =  [0]                                     
                                    >= [0]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [0]                                     
                                    >= [0]                                     
                                    =  i()                                     
          
                 activate(n__nil()) =  [0]                                     
                                    >= [0]                                     
                                    =  nil()                                   
          
                   activate(n__o()) =  [0]                                     
                                    >= [0]                                     
                                    =  o()                                     
          
                   activate(n__u()) =  [0]                                     
                                    >= [1]                                     
                                    =  u()                                     
          
                                e() =  [0]                                     
                                    >= [0]                                     
                                    =  n__e()                                  
          
                                i() =  [0]                                     
                                    >= [0]                                     
                                    =  n__i()                                  
          
                          isList(V) =  [1] V + [0]                             
                                    >= [1] V + [0]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                   
                                    >= [1] V1 + [1] V2 + [0]                   
                                    =  U21(isList(activate(V1)),activate(V2))  
          
                   isList(n__nil()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [0]                             
                                    >= [1] V + [0]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                   
                                    >= [1] V1 + [1] V2 + [0]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                   
                                    >= [1] V1 + [1] V2 + [7]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [0]                             
                                    >= [1] V + [7]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [0]                     
                                    >= [1] I + [1] P + [0]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [0]                             
                                    >= [1] V + [0]                             
                                    =  U81(isNePal(activate(V)))               
          
                    isPal(n__nil()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                              nil() =  [0]                                     
                                    >= [0]                                     
                                    =  n__nil()                                
          
                                o() =  [0]                                     
                                    >= [0]                                     
                                    =  n__o()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
        - Weak TRS:
            U11(tt()) -> tt()
            U31(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [0]         
                 p(U21) = [1] x1 + [1] x2 + [0]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [4]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [1]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [0]
                 p(U72) = [1] x1 + [0]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [0]
                   p(a) = [0]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [0]                  
                   p(i) = [0]                  
              p(isList) = [1] x1 + [5]         
            p(isNeList) = [1] x1 + [5]         
             p(isNePal) = [1] x1 + [4]         
               p(isPal) = [1] x1 + [0]         
               p(isQid) = [1] x1 + [4]         
               p(n____) = [1] x1 + [1] x2 + [0]
                p(n__a) = [0]                  
                p(n__e) = [0]                  
                p(n__i) = [0]                  
              p(n__nil) = [0]                  
                p(n__o) = [4]                  
                p(n__u) = [0]                  
                 p(nil) = [0]                  
                   p(o) = [0]                  
                  p(tt) = [4]                  
                   p(u) = [0]                  
          
          Following rules are strictly oriented:
              U41(tt(),V2) = [1] V2 + [8]               
                           > [1] V2 + [5]               
                           = U42(isNeList(activate(V2)))
          
               U71(tt(),P) = [1] P + [4]                
                           > [1] P + [0]                
                           = U72(isPal(activate(P)))    
          
          activate(n__o()) = [4]                        
                           > [0]                        
                           = o()                        
          
          isList(n__nil()) = [5]                        
                           > [4]                        
                           = tt()                       
          
               isNeList(V) = [1] V + [5]                
                           > [1] V + [4]                
                           = U31(isQid(activate(V)))    
          
             isQid(n__o()) = [8]                        
                           > [4]                        
                           = tt()                       
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [4]                            
                                    >= [1] V2 + [5]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                          U42(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [5]                            
                                    >= [1] V2 + [5]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                          U72(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                          U81(tt()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [0]                   
                                    >= [1] X1 + [1] X2 + [0]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [0]             
                                    >= [1] X + [1] Y + [1] Z + [0]             
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [0]                                     
                                    >= [0]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [0]                   
                                    >= [1] X1 + [1] X2 + [0]                   
                                    =  __(X1,X2)                               
          
                   activate(n__a()) =  [0]                                     
                                    >= [0]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [0]                                     
                                    >= [0]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [0]                                     
                                    >= [0]                                     
                                    =  i()                                     
          
                 activate(n__nil()) =  [0]                                     
                                    >= [0]                                     
                                    =  nil()                                   
          
                   activate(n__u()) =  [0]                                     
                                    >= [0]                                     
                                    =  u()                                     
          
                                e() =  [0]                                     
                                    >= [0]                                     
                                    =  n__e()                                  
          
                                i() =  [0]                                     
                                    >= [0]                                     
                                    =  n__i()                                  
          
                          isList(V) =  [1] V + [5]                             
                                    >= [1] V + [5]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                   
                                    >= [1] V1 + [1] V2 + [5]                   
                                    =  U21(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                   
                                    >= [1] V1 + [1] V2 + [9]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                   
                                    >= [1] V1 + [1] V2 + [6]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [4]                             
                                    >= [1] V + [4]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [4]                     
                                    >= [1] I + [1] P + [4]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [0]                             
                                    >= [1] V + [4]                             
                                    =  U81(isNePal(activate(V)))               
          
                    isPal(n__nil()) =  [0]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                      isQid(n__a()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [4]                                     
                                    >= [4]                                     
                                    =  tt()                                    
          
                              nil() =  [0]                                     
                                    >= [0]                                     
                                    =  n__nil()                                
          
                                o() =  [0]                                     
                                    >= [4]                                     
                                    =  n__o()                                  
          
                                u() =  [0]                                     
                                    >= [0]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U42(tt()) -> tt()
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
        - Weak TRS:
            U11(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__o()) -> o()
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__o()) -> tt()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [0]         
                 p(U21) = [1] x1 + [1] x2 + [5]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [4]
                 p(U42) = [1] x1 + [2]         
                 p(U51) = [1] x1 + [1] x2 + [0]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [3]
                 p(U72) = [1] x1 + [5]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [0]
                   p(a) = [0]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [7]                  
                   p(i) = [1]                  
              p(isList) = [1] x1 + [2]         
            p(isNeList) = [1] x1 + [4]         
             p(isNePal) = [1] x1 + [7]         
               p(isPal) = [1] x1 + [0]         
               p(isQid) = [1] x1 + [4]         
               p(n____) = [1] x1 + [1] x2 + [0]
                p(n__a) = [0]                  
                p(n__e) = [7]                  
                p(n__i) = [0]                  
              p(n__nil) = [0]                  
                p(n__o) = [4]                  
                p(n__u) = [2]                  
                 p(nil) = [0]                  
                   p(o) = [4]                  
                  p(tt) = [2]                  
                   p(u) = [5]                  
          
          Following rules are strictly oriented:
           U21(tt(),V2) = [1] V2 + [7]             
                        > [1] V2 + [2]             
                        = U22(isList(activate(V2)))
          
              U42(tt()) = [4]                      
                        > [2]                      
                        = tt()                     
          
              U72(tt()) = [7]                      
                        > [2]                      
                        = tt()                     
          
                    i() = [1]                      
                        > [0]                      
                        = n__i()                   
          
             isNePal(V) = [1] V + [7]              
                        > [1] V + [4]              
                        = U61(isQid(activate(V)))  
          
          isQid(n__i()) = [4]                      
                        > [2]                      
                        = tt()                     
          
          isQid(n__u()) = [6]                      
                        > [2]                      
                        = tt()                     
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                          U22(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [6]                            
                                    >= [1] V2 + [6]                            
                                    =  U42(isNeList(activate(V2)))             
          
                       U51(tt(),V2) =  [1] V2 + [2]                            
                                    >= [1] V2 + [2]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                        U71(tt(),P) =  [1] P + [5]                             
                                    >= [1] P + [5]                             
                                    =  U72(isPal(activate(P)))                 
          
                          U81(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [0]                   
                                    >= [1] X1 + [1] X2 + [0]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [0]             
                                    >= [1] X + [1] Y + [1] Z + [0]             
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [0]                                     
                                    >= [0]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [0]                   
                                    >= [1] X1 + [1] X2 + [0]                   
                                    =  __(X1,X2)                               
          
                   activate(n__a()) =  [0]                                     
                                    >= [0]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [7]                                     
                                    >= [7]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [0]                                     
                                    >= [1]                                     
                                    =  i()                                     
          
                 activate(n__nil()) =  [0]                                     
                                    >= [0]                                     
                                    =  nil()                                   
          
                   activate(n__o()) =  [4]                                     
                                    >= [4]                                     
                                    =  o()                                     
          
                   activate(n__u()) =  [2]                                     
                                    >= [5]                                     
                                    =  u()                                     
          
                                e() =  [7]                                     
                                    >= [7]                                     
                                    =  n__e()                                  
          
                          isList(V) =  [1] V + [2]                             
                                    >= [1] V + [4]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [2]                   
                                    >= [1] V1 + [1] V2 + [7]                   
                                    =  U21(isList(activate(V1)),activate(V2))  
          
                   isList(n__nil()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [4]                             
                                    >= [1] V + [4]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [4]                   
                                    >= [1] V1 + [1] V2 + [6]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [4]                   
                                    >= [1] V1 + [1] V2 + [4]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [7]                     
                                    >= [1] I + [1] P + [7]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [0]                             
                                    >= [1] V + [7]                             
                                    =  U81(isNePal(activate(V)))               
          
                    isPal(n__nil()) =  [0]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__a()) =  [4]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [11]                                    
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [8]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                              nil() =  [0]                                     
                                    >= [0]                                     
                                    =  n__nil()                                
          
                                o() =  [4]                                     
                                    >= [4]                                     
                                    =  n__o()                                  
          
                                u() =  [5]                                     
                                    >= [2]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            U22(tt()) -> tt()
            U81(tt()) -> tt()
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__u()) -> u()
            e() -> n__e()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__o()) -> o()
            i() -> n__i()
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [2]         
                 p(U21) = [1] x1 + [1] x2 + [6]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [1]         
                 p(U41) = [1] x1 + [1] x2 + [6]
                 p(U42) = [1] x1 + [4]         
                 p(U51) = [1] x1 + [1] x2 + [3]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [0]
                 p(U72) = [1] x1 + [0]         
                 p(U81) = [1] x1 + [7]         
                  p(__) = [1] x1 + [1] x2 + [1]
                   p(a) = [0]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [0]                  
                   p(i) = [0]                  
              p(isList) = [1] x1 + [4]         
            p(isNeList) = [1] x1 + [3]         
             p(isNePal) = [1] x1 + [4]         
               p(isPal) = [1] x1 + [0]         
               p(isQid) = [1] x1 + [2]         
               p(n____) = [1] x1 + [1] x2 + [1]
                p(n__a) = [5]                  
                p(n__e) = [0]                  
                p(n__i) = [0]                  
              p(n__nil) = [5]                  
                p(n__o) = [0]                  
                p(n__u) = [0]                  
                 p(nil) = [0]                  
                   p(o) = [0]                  
                  p(tt) = [1]                  
                   p(u) = [0]                  
          
          Following rules are strictly oriented:
                   U81(tt()) = [8]  
                             > [1]  
                             = tt() 
          
          activate(n__nil()) = [5]  
                             > [0]  
                             = nil()
          
             isPal(n__nil()) = [5]  
                             > [1]  
                             = tt() 
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [3]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [7]                            
                                    >= [1] V2 + [4]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [1]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [2]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [7]                            
                                    >= [1] V2 + [7]                            
                                    =  U42(isNeList(activate(V2)))             
          
                          U42(tt()) =  [5]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [4]                            
                                    >= [1] V2 + [4]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [1]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [1]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                        U71(tt(),P) =  [1] P + [1]                             
                                    >= [1] P + [0]                             
                                    =  U72(isPal(activate(P)))                 
          
                          U72(tt()) =  [1]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [1]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [1]                   
                                    >= [1] X1 + [1] X2 + [1]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [2]             
                                    >= [1] X + [1] Y + [1] Z + [2]             
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [1]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [0]                                     
                                    >= [5]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [1]                   
                                    >= [1] X1 + [1] X2 + [1]                   
                                    =  __(X1,X2)                               
          
                   activate(n__a()) =  [5]                                     
                                    >= [0]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [0]                                     
                                    >= [0]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [0]                                     
                                    >= [0]                                     
                                    =  i()                                     
          
                   activate(n__o()) =  [0]                                     
                                    >= [0]                                     
                                    =  o()                                     
          
                   activate(n__u()) =  [0]                                     
                                    >= [0]                                     
                                    =  u()                                     
          
                                e() =  [0]                                     
                                    >= [0]                                     
                                    =  n__e()                                  
          
                                i() =  [0]                                     
                                    >= [0]                                     
                                    =  n__i()                                  
          
                          isList(V) =  [1] V + [4]                             
                                    >= [1] V + [5]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                   
                                    >= [1] V1 + [1] V2 + [10]                  
                                    =  U21(isList(activate(V1)),activate(V2))  
          
                   isList(n__nil()) =  [9]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [3]                             
                                    >= [1] V + [3]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [4]                   
                                    >= [1] V1 + [1] V2 + [10]                  
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [4]                   
                                    >= [1] V1 + [1] V2 + [6]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [4]                             
                                    >= [1] V + [2]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [6]                     
                                    >= [1] I + [1] P + [2]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [0]                             
                                    >= [1] V + [11]                            
                                    =  U81(isNePal(activate(V)))               
          
                      isQid(n__a()) =  [7]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [2]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [2]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [2]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [2]                                     
                                    >= [1]                                     
                                    =  tt()                                    
          
                              nil() =  [0]                                     
                                    >= [5]                                     
                                    =  n__nil()                                
          
                                o() =  [0]                                     
                                    >= [0]                                     
                                    =  n__o()                                  
          
                                u() =  [0]                                     
                                    >= [0]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            U22(tt()) -> tt()
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__u()) -> u()
            e() -> n__e()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isPal(V) -> U81(isNePal(activate(V)))
            nil() -> n__nil()
            o() -> n__o()
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            i() -> n__i()
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [5]         
                 p(U21) = [1] x1 + [1] x2 + [2]
                 p(U22) = [1] x1 + [2]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [2]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [0]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [4]
                 p(U72) = [1] x1 + [1]         
                 p(U81) = [1] x1 + [6]         
                  p(__) = [1] x1 + [1] x2 + [1]
                   p(a) = [0]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [4]                  
                   p(i) = [0]                  
              p(isList) = [1] x1 + [0]         
            p(isNeList) = [1] x1 + [2]         
             p(isNePal) = [1] x1 + [2]         
               p(isPal) = [1] x1 + [3]         
               p(isQid) = [1] x1 + [0]         
               p(n____) = [1] x1 + [1] x2 + [1]
                p(n__a) = [1]                  
                p(n__e) = [6]                  
                p(n__i) = [0]                  
              p(n__nil) = [5]                  
                p(n__o) = [0]                  
                p(n__u) = [0]                  
                 p(nil) = [2]                  
                   p(o) = [0]                  
                  p(tt) = [0]                  
                   p(u) = [2]                  
          
          Following rules are strictly oriented:
                       U22(tt()) = [2]                                     
                                 > [0]                                     
                                 = tt()                                    
          
          isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]                   
                                 > [1] V1 + [1] V2 + [2]                   
                                 = U41(isList(activate(V1)),activate(V2))  
          
          isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]                   
                                 > [1] V1 + [1] V2 + [2]                   
                                 = U51(isNeList(activate(V1)),activate(V2))
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [5]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                       U21(tt(),V2) =  [1] V2 + [2]                          
                                    >= [1] V2 + [2]                          
                                    =  U22(isList(activate(V2)))             
          
                          U31(tt()) =  [0]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                       U41(tt(),V2) =  [1] V2 + [2]                          
                                    >= [1] V2 + [2]                          
                                    =  U42(isNeList(activate(V2)))           
          
                          U42(tt()) =  [0]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                       U51(tt(),V2) =  [1] V2 + [0]                          
                                    >= [1] V2 + [0]                          
                                    =  U52(isList(activate(V2)))             
          
                          U52(tt()) =  [0]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                          U61(tt()) =  [0]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                        U71(tt(),P) =  [1] P + [4]                           
                                    >= [1] P + [4]                           
                                    =  U72(isPal(activate(P)))               
          
                          U72(tt()) =  [1]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                          U81(tt()) =  [6]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                        __(X,nil()) =  [1] X + [3]                           
                                    >= [1] X + [0]                           
                                    =  X                                     
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [1]                 
                                    >= [1] X1 + [1] X2 + [1]                 
                                    =  n____(X1,X2)                          
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [2]           
                                    >= [1] X + [1] Y + [1] Z + [2]           
                                    =  __(X,__(Y,Z))                         
          
                        __(nil(),X) =  [1] X + [3]                           
                                    >= [1] X + [0]                           
                                    =  X                                     
          
                                a() =  [0]                                   
                                    >= [1]                                   
                                    =  n__a()                                
          
                        activate(X) =  [1] X + [0]                           
                                    >= [1] X + [0]                           
                                    =  X                                     
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [1]                 
                                    >= [1] X1 + [1] X2 + [1]                 
                                    =  __(X1,X2)                             
          
                   activate(n__a()) =  [1]                                   
                                    >= [0]                                   
                                    =  a()                                   
          
                   activate(n__e()) =  [6]                                   
                                    >= [4]                                   
                                    =  e()                                   
          
                   activate(n__i()) =  [0]                                   
                                    >= [0]                                   
                                    =  i()                                   
          
                 activate(n__nil()) =  [5]                                   
                                    >= [2]                                   
                                    =  nil()                                 
          
                   activate(n__o()) =  [0]                                   
                                    >= [0]                                   
                                    =  o()                                   
          
                   activate(n__u()) =  [0]                                   
                                    >= [2]                                   
                                    =  u()                                   
          
                                e() =  [4]                                   
                                    >= [6]                                   
                                    =  n__e()                                
          
                                i() =  [0]                                   
                                    >= [0]                                   
                                    =  n__i()                                
          
                          isList(V) =  [1] V + [0]                           
                                    >= [1] V + [7]                           
                                    =  U11(isNeList(activate(V)))            
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [1]                 
                                    >= [1] V1 + [1] V2 + [2]                 
                                    =  U21(isList(activate(V1)),activate(V2))
          
                   isList(n__nil()) =  [5]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                        isNeList(V) =  [1] V + [2]                           
                                    >= [1] V + [0]                           
                                    =  U31(isQid(activate(V)))               
          
                         isNePal(V) =  [1] V + [2]                           
                                    >= [1] V + [0]                           
                                    =  U61(isQid(activate(V)))               
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [4]                   
                                    >= [1] I + [1] P + [4]                   
                                    =  U71(isQid(activate(I)),activate(P))   
          
                           isPal(V) =  [1] V + [3]                           
                                    >= [1] V + [8]                           
                                    =  U81(isNePal(activate(V)))             
          
                    isPal(n__nil()) =  [8]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                      isQid(n__a()) =  [1]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                      isQid(n__e()) =  [6]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                      isQid(n__i()) =  [0]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                      isQid(n__o()) =  [0]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                      isQid(n__u()) =  [0]                                   
                                    >= [0]                                   
                                    =  tt()                                  
          
                              nil() =  [2]                                   
                                    >= [5]                                   
                                    =  n__nil()                              
          
                                o() =  [0]                                   
                                    >= [0]                                   
                                    =  n__o()                                
          
                                u() =  [2]                                   
                                    >= [0]                                   
                                    =  n__u()                                
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__u()) -> u()
            e() -> n__e()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isPal(V) -> U81(isNePal(activate(V)))
            nil() -> n__nil()
            o() -> n__o()
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            i() -> n__i()
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [0]         
                 p(U21) = [1] x1 + [1] x2 + [3]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [0]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [4]
                 p(U52) = [1] x1 + [1]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [3]
                 p(U72) = [1] x1 + [1]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [4]
                   p(a) = [2]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [2]                  
                   p(i) = [3]                  
              p(isList) = [1] x1 + [5]         
            p(isNeList) = [1] x1 + [2]         
             p(isNePal) = [1] x1 + [6]         
               p(isPal) = [1] x1 + [4]         
               p(isQid) = [1] x1 + [0]         
               p(n____) = [1] x1 + [1] x2 + [4]
                p(n__a) = [2]                  
                p(n__e) = [2]                  
                p(n__i) = [2]                  
              p(n__nil) = [1]                  
                p(n__o) = [3]                  
                p(n__u) = [2]                  
                 p(nil) = [0]                  
                   p(o) = [3]                  
                  p(tt) = [2]                  
                   p(u) = [2]                  
          
          Following rules are strictly oriented:
                     isList(V) = [1] V + [5]                           
                               > [1] V + [2]                           
                               = U11(isNeList(activate(V)))            
          
          isList(n____(V1,V2)) = [1] V1 + [1] V2 + [9]                 
                               > [1] V1 + [1] V2 + [8]                 
                               = U21(isList(activate(V1)),activate(V2))
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [5]                            
                                    >= [1] V2 + [5]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [2]                            
                                    >= [1] V2 + [2]                            
                                    =  U42(isNeList(activate(V2)))             
          
                          U42(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [6]                            
                                    >= [1] V2 + [6]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [3]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                        U71(tt(),P) =  [1] P + [5]                             
                                    >= [1] P + [5]                             
                                    =  U72(isPal(activate(P)))                 
          
                          U72(tt()) =  [3]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                          U81(tt()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [4]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [4]                   
                                    >= [1] X1 + [1] X2 + [4]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [8]             
                                    >= [1] X + [1] Y + [1] Z + [8]             
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [4]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [2]                                     
                                    >= [2]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [4]                   
                                    >= [1] X1 + [1] X2 + [4]                   
                                    =  __(X1,X2)                               
          
                   activate(n__a()) =  [2]                                     
                                    >= [2]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [2]                                     
                                    >= [2]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [2]                                     
                                    >= [3]                                     
                                    =  i()                                     
          
                 activate(n__nil()) =  [1]                                     
                                    >= [0]                                     
                                    =  nil()                                   
          
                   activate(n__o()) =  [3]                                     
                                    >= [3]                                     
                                    =  o()                                     
          
                   activate(n__u()) =  [2]                                     
                                    >= [2]                                     
                                    =  u()                                     
          
                                e() =  [2]                                     
                                    >= [2]                                     
                                    =  n__e()                                  
          
                                i() =  [3]                                     
                                    >= [2]                                     
                                    =  n__i()                                  
          
                   isList(n__nil()) =  [6]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [2]                             
                                    >= [1] V + [0]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                   
                                    >= [1] V1 + [1] V2 + [5]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                   
                                    >= [1] V1 + [1] V2 + [6]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [6]                             
                                    >= [1] V + [0]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [14]                    
                                    >= [1] I + [1] P + [3]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [4]                             
                                    >= [1] V + [6]                             
                                    =  U81(isNePal(activate(V)))               
          
                    isPal(n__nil()) =  [5]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__a()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [3]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [2]                                     
                                    >= [2]                                     
                                    =  tt()                                    
          
                              nil() =  [0]                                     
                                    >= [1]                                     
                                    =  n__nil()                                
          
                                o() =  [3]                                     
                                    >= [3]                                     
                                    =  n__o()                                  
          
                                u() =  [2]                                     
                                    >= [2]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__u()) -> u()
            e() -> n__e()
            isPal(V) -> U81(isNePal(activate(V)))
            nil() -> n__nil()
            o() -> n__o()
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [0]         
                 p(U21) = [1] x1 + [1] x2 + [1]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [0]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [1]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [2]
                 p(U72) = [1] x1 + [0]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [1]
                   p(a) = [0]                  
            p(activate) = [1] x1 + [0]         
                   p(e) = [0]                  
                   p(i) = [0]                  
              p(isList) = [1] x1 + [1]         
            p(isNeList) = [1] x1 + [0]         
             p(isNePal) = [1] x1 + [0]         
               p(isPal) = [1] x1 + [1]         
               p(isQid) = [1] x1 + [0]         
               p(n____) = [1] x1 + [1] x2 + [1]
                p(n__a) = [0]                  
                p(n__e) = [0]                  
                p(n__i) = [0]                  
              p(n__nil) = [5]                  
                p(n__o) = [1]                  
                p(n__u) = [0]                  
                 p(nil) = [4]                  
                   p(o) = [0]                  
                  p(tt) = [0]                  
                   p(u) = [0]                  
          
          Following rules are strictly oriented:
          isPal(V) = [1] V + [1]              
                   > [1] V + [0]              
                   = U81(isNePal(activate(V)))
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [1]                            
                                    >= [1] V2 + [1]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [0]                            
                                    >= [1] V2 + [0]                            
                                    =  U42(isNeList(activate(V2)))             
          
                          U42(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [1]                            
                                    >= [1] V2 + [1]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        U71(tt(),P) =  [1] P + [2]                             
                                    >= [1] P + [1]                             
                                    =  U72(isPal(activate(P)))                 
          
                          U72(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U81(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [5]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [1]                   
                                    >= [1] X1 + [1] X2 + [1]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [2]             
                                    >= [1] X + [1] Y + [1] Z + [2]             
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [5]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [0]                                     
                                    >= [0]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [0]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [1]                   
                                    >= [1] X1 + [1] X2 + [1]                   
                                    =  __(X1,X2)                               
          
                   activate(n__a()) =  [0]                                     
                                    >= [0]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [0]                                     
                                    >= [0]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [0]                                     
                                    >= [0]                                     
                                    =  i()                                     
          
                 activate(n__nil()) =  [5]                                     
                                    >= [4]                                     
                                    =  nil()                                   
          
                   activate(n__o()) =  [1]                                     
                                    >= [0]                                     
                                    =  o()                                     
          
                   activate(n__u()) =  [0]                                     
                                    >= [0]                                     
                                    =  u()                                     
          
                                e() =  [0]                                     
                                    >= [0]                                     
                                    =  n__e()                                  
          
                                i() =  [0]                                     
                                    >= [0]                                     
                                    =  n__i()                                  
          
                          isList(V) =  [1] V + [1]                             
                                    >= [1] V + [0]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [2]                   
                                    >= [1] V1 + [1] V2 + [2]                   
                                    =  U21(isList(activate(V1)),activate(V2))  
          
                   isList(n__nil()) =  [6]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [0]                             
                                    >= [1] V + [0]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [1]                   
                                    >= [1] V1 + [1] V2 + [1]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [1]                   
                                    >= [1] V1 + [1] V2 + [1]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [0]                             
                                    >= [1] V + [0]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [2]                     
                                    >= [1] I + [1] P + [2]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                    isPal(n__nil()) =  [6]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__a()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [1]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                              nil() =  [4]                                     
                                    >= [5]                                     
                                    =  n__nil()                                
          
                                o() =  [0]                                     
                                    >= [1]                                     
                                    =  n__o()                                  
          
                                u() =  [0]                                     
                                    >= [0]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__u()) -> u()
            e() -> n__e()
            nil() -> n__nil()
            o() -> n__o()
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [0]         
                 p(U21) = [1] x1 + [1] x2 + [1]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [0]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [0]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [6]
                 p(U72) = [1] x1 + [6]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [5]
                   p(a) = [4]                  
            p(activate) = [1] x1 + [1]         
                   p(e) = [0]                  
                   p(i) = [4]                  
              p(isList) = [1] x1 + [5]         
            p(isNeList) = [1] x1 + [4]         
             p(isNePal) = [1] x1 + [4]         
               p(isPal) = [1] x1 + [5]         
               p(isQid) = [1] x1 + [3]         
               p(n____) = [1] x1 + [1] x2 + [3]
                p(n__a) = [3]                  
                p(n__e) = [5]                  
                p(n__i) = [4]                  
              p(n__nil) = [3]                  
                p(n__o) = [6]                  
                p(n__u) = [6]                  
                 p(nil) = [0]                  
                   p(o) = [7]                  
                  p(tt) = [6]                  
                   p(u) = [6]                  
          
          Following rules are strictly oriented:
                       a() = [4]        
                           > [3]        
                           = n__a()     
          
               activate(X) = [1] X + [1]
                           > [1] X + [0]
                           = X          
          
          activate(n__i()) = [5]        
                           > [4]        
                           = i()        
          
          activate(n__u()) = [7]        
                           > [6]        
                           = u()        
          
                       o() = [7]        
                           > [6]        
                           = n__o()     
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [7]                            
                                    >= [1] V2 + [6]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [6]                            
                                    >= [1] V2 + [5]                            
                                    =  U42(isNeList(activate(V2)))             
          
                          U42(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [6]                            
                                    >= [1] V2 + [6]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                        U71(tt(),P) =  [1] P + [12]                            
                                    >= [1] P + [12]                            
                                    =  U72(isPal(activate(P)))                 
          
                          U72(tt()) =  [12]                                    
                                    >= [6]                                     
                                    =  tt()                                    
          
                          U81(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [5]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [5]                   
                                    >= [1] X1 + [1] X2 + [3]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [10]            
                                    >= [1] X + [1] Y + [1] Z + [10]            
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [5]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [4]                   
                                    >= [1] X1 + [1] X2 + [5]                   
                                    =  __(X1,X2)                               
          
                   activate(n__a()) =  [4]                                     
                                    >= [4]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [6]                                     
                                    >= [0]                                     
                                    =  e()                                     
          
                 activate(n__nil()) =  [4]                                     
                                    >= [0]                                     
                                    =  nil()                                   
          
                   activate(n__o()) =  [7]                                     
                                    >= [7]                                     
                                    =  o()                                     
          
                                e() =  [0]                                     
                                    >= [5]                                     
                                    =  n__e()                                  
          
                                i() =  [4]                                     
                                    >= [4]                                     
                                    =  n__i()                                  
          
                          isList(V) =  [1] V + [5]                             
                                    >= [1] V + [5]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [8]                   
                                    >= [1] V1 + [1] V2 + [8]                   
                                    =  U21(isList(activate(V1)),activate(V2))  
          
                   isList(n__nil()) =  [8]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [4]                             
                                    >= [1] V + [4]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [7]                   
                                    >= [1] V1 + [1] V2 + [7]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [7]                   
                                    >= [1] V1 + [1] V2 + [6]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [4]                             
                                    >= [1] V + [4]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [12]                    
                                    >= [1] I + [1] P + [11]                    
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [5]                             
                                    >= [1] V + [5]                             
                                    =  U81(isNePal(activate(V)))               
          
                    isPal(n__nil()) =  [8]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__a()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [8]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [7]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [9]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [9]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                              nil() =  [0]                                     
                                    >= [3]                                     
                                    =  n__nil()                                
          
                                u() =  [6]                                     
                                    >= [6]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 10: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            activate(n____(X1,X2)) -> __(X1,X2)
            e() -> n__e()
            nil() -> n__nil()
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            a() -> n__a()
            activate(X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [0]         
                 p(U21) = [1] x1 + [1] x2 + [2]
                 p(U22) = [1] x1 + [2]         
                 p(U31) = [1] x1 + [0]         
                 p(U41) = [1] x1 + [1] x2 + [0]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [0]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [3]
                 p(U72) = [1] x1 + [0]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [6]
                   p(a) = [6]                  
            p(activate) = [1] x1 + [2]         
                   p(e) = [0]                  
                   p(i) = [6]                  
              p(isList) = [1] x1 + [4]         
            p(isNeList) = [1] x1 + [2]         
             p(isNePal) = [1] x1 + [2]         
               p(isPal) = [1] x1 + [4]         
               p(isQid) = [1] x1 + [0]         
               p(n____) = [1] x1 + [1] x2 + [6]
                p(n__a) = [6]                  
                p(n__e) = [6]                  
                p(n__i) = [6]                  
              p(n__nil) = [4]                  
                p(n__o) = [7]                  
                p(n__u) = [6]                  
                 p(nil) = [5]                  
                   p(o) = [7]                  
                  p(tt) = [6]                  
                   p(u) = [7]                  
          
          Following rules are strictly oriented:
          activate(n____(X1,X2)) = [1] X1 + [1] X2 + [8]
                                 > [1] X1 + [1] X2 + [6]
                                 = __(X1,X2)            
          
                           nil() = [5]                  
                                 > [4]                  
                                 = n__nil()             
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [8]                            
                                    >= [1] V2 + [8]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [8]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [6]                            
                                    >= [1] V2 + [4]                            
                                    =  U42(isNeList(activate(V2)))             
          
                          U42(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [6]                            
                                    >= [1] V2 + [6]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                        U71(tt(),P) =  [1] P + [9]                             
                                    >= [1] P + [6]                             
                                    =  U72(isPal(activate(P)))                 
          
                          U72(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                          U81(tt()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [11]                            
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [6]                   
                                    >= [1] X1 + [1] X2 + [6]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [12]            
                                    >= [1] X + [1] Y + [1] Z + [12]            
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [11]                            
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [6]                                     
                                    >= [6]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [2]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                   activate(n__a()) =  [8]                                     
                                    >= [6]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [8]                                     
                                    >= [0]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [8]                                     
                                    >= [6]                                     
                                    =  i()                                     
          
                 activate(n__nil()) =  [6]                                     
                                    >= [5]                                     
                                    =  nil()                                   
          
                   activate(n__o()) =  [9]                                     
                                    >= [7]                                     
                                    =  o()                                     
          
                   activate(n__u()) =  [8]                                     
                                    >= [7]                                     
                                    =  u()                                     
          
                                e() =  [0]                                     
                                    >= [6]                                     
                                    =  n__e()                                  
          
                                i() =  [6]                                     
                                    >= [6]                                     
                                    =  n__i()                                  
          
                          isList(V) =  [1] V + [4]                             
                                    >= [1] V + [4]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [10]                  
                                    >= [1] V1 + [1] V2 + [10]                  
                                    =  U21(isList(activate(V1)),activate(V2))  
          
                   isList(n__nil()) =  [8]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [2]                             
                                    >= [1] V + [2]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [8]                   
                                    >= [1] V1 + [1] V2 + [8]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [8]                   
                                    >= [1] V1 + [1] V2 + [6]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [2]                             
                                    >= [1] V + [2]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [14]                    
                                    >= [1] I + [1] P + [7]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [4]                             
                                    >= [1] V + [4]                             
                                    =  U81(isNePal(activate(V)))               
          
                    isPal(n__nil()) =  [8]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__a()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [7]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [6]                                     
                                    >= [6]                                     
                                    =  tt()                                    
          
                                o() =  [7]                                     
                                    >= [7]                                     
                                    =  n__o()                                  
          
                                u() =  [7]                                     
                                    >= [6]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 11: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            e() -> n__e()
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + 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(U11) = {1},
            uargs(U21) = {1,2},
            uargs(U22) = {1},
            uargs(U31) = {1},
            uargs(U41) = {1,2},
            uargs(U42) = {1},
            uargs(U51) = {1,2},
            uargs(U52) = {1},
            uargs(U61) = {1},
            uargs(U71) = {1,2},
            uargs(U72) = {1},
            uargs(U81) = {1},
            uargs(__) = {2},
            uargs(activate) = {1},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                 p(U11) = [1] x1 + [1]         
                 p(U21) = [1] x1 + [1] x2 + [5]
                 p(U22) = [1] x1 + [0]         
                 p(U31) = [1] x1 + [1]         
                 p(U41) = [1] x1 + [1] x2 + [3]
                 p(U42) = [1] x1 + [0]         
                 p(U51) = [1] x1 + [1] x2 + [5]
                 p(U52) = [1] x1 + [0]         
                 p(U61) = [1] x1 + [0]         
                 p(U71) = [1] x1 + [1] x2 + [6]
                 p(U72) = [1] x1 + [0]         
                 p(U81) = [1] x1 + [0]         
                  p(__) = [1] x1 + [1] x2 + [7]
                   p(a) = [4]                  
            p(activate) = [1] x1 + [1]         
                   p(e) = [3]                  
                   p(i) = [2]                  
              p(isList) = [1] x1 + [4]         
            p(isNeList) = [1] x1 + [2]         
             p(isNePal) = [1] x1 + [1]         
               p(isPal) = [1] x1 + [5]         
               p(isQid) = [1] x1 + [0]         
               p(n____) = [1] x1 + [1] x2 + [7]
                p(n__a) = [4]                  
                p(n__e) = [2]                  
                p(n__i) = [1]                  
              p(n__nil) = [0]                  
                p(n__o) = [0]                  
                p(n__u) = [0]                  
                 p(nil) = [0]                  
                   p(o) = [0]                  
                  p(tt) = [0]                  
                   p(u) = [0]                  
          
          Following rules are strictly oriented:
          e() = [3]   
              > [2]   
              = n__e()
          
          
          Following rules are (at-least) weakly oriented:
                          U11(tt()) =  [1]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U21(tt(),V2) =  [1] V2 + [5]                            
                                    >= [1] V2 + [5]                            
                                    =  U22(isList(activate(V2)))               
          
                          U22(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U31(tt()) =  [1]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U41(tt(),V2) =  [1] V2 + [3]                            
                                    >= [1] V2 + [3]                            
                                    =  U42(isNeList(activate(V2)))             
          
                          U42(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                       U51(tt(),V2) =  [1] V2 + [5]                            
                                    >= [1] V2 + [5]                            
                                    =  U52(isList(activate(V2)))               
          
                          U52(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U61(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        U71(tt(),P) =  [1] P + [6]                             
                                    >= [1] P + [6]                             
                                    =  U72(isPal(activate(P)))                 
          
                          U72(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                          U81(tt()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        __(X,nil()) =  [1] X + [7]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [7]                   
                                    >= [1] X1 + [1] X2 + [7]                   
                                    =  n____(X1,X2)                            
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [14]            
                                    >= [1] X + [1] Y + [1] Z + [14]            
                                    =  __(X,__(Y,Z))                           
          
                        __(nil(),X) =  [1] X + [7]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
                                a() =  [4]                                     
                                    >= [4]                                     
                                    =  n__a()                                  
          
                        activate(X) =  [1] X + [1]                             
                                    >= [1] X + [0]                             
                                    =  X                                       
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [8]                   
                                    >= [1] X1 + [1] X2 + [7]                   
                                    =  __(X1,X2)                               
          
                   activate(n__a()) =  [5]                                     
                                    >= [4]                                     
                                    =  a()                                     
          
                   activate(n__e()) =  [3]                                     
                                    >= [3]                                     
                                    =  e()                                     
          
                   activate(n__i()) =  [2]                                     
                                    >= [2]                                     
                                    =  i()                                     
          
                 activate(n__nil()) =  [1]                                     
                                    >= [0]                                     
                                    =  nil()                                   
          
                   activate(n__o()) =  [1]                                     
                                    >= [0]                                     
                                    =  o()                                     
          
                   activate(n__u()) =  [1]                                     
                                    >= [0]                                     
                                    =  u()                                     
          
                                i() =  [2]                                     
                                    >= [1]                                     
                                    =  n__i()                                  
          
                          isList(V) =  [1] V + [4]                             
                                    >= [1] V + [4]                             
                                    =  U11(isNeList(activate(V)))              
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [11]                  
                                    >= [1] V1 + [1] V2 + [11]                  
                                    =  U21(isList(activate(V1)),activate(V2))  
          
                   isList(n__nil()) =  [4]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                        isNeList(V) =  [1] V + [2]                             
                                    >= [1] V + [2]                             
                                    =  U31(isQid(activate(V)))                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [9]                   
                                    >= [1] V1 + [1] V2 + [9]                   
                                    =  U41(isList(activate(V1)),activate(V2))  
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [9]                   
                                    >= [1] V1 + [1] V2 + [9]                   
                                    =  U51(isNeList(activate(V1)),activate(V2))
          
                         isNePal(V) =  [1] V + [1]                             
                                    >= [1] V + [1]                             
                                    =  U61(isQid(activate(V)))                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [15]                    
                                    >= [1] I + [1] P + [8]                     
                                    =  U71(isQid(activate(I)),activate(P))     
          
                           isPal(V) =  [1] V + [5]                             
                                    >= [1] V + [2]                             
                                    =  U81(isNePal(activate(V)))               
          
                    isPal(n__nil()) =  [5]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__a()) =  [4]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__e()) =  [2]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__i()) =  [1]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__o()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                      isQid(n__u()) =  [0]                                     
                                    >= [0]                                     
                                    =  tt()                                    
          
                              nil() =  [0]                                     
                                    >= [0]                                     
                                    =  n__nil()                                
          
                                o() =  [0]                                     
                                    >= [0]                                     
                                    =  n__o()                                  
          
                                u() =  [0]                                     
                                    >= [0]                                     
                                    =  n__u()                                  
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 12: MI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + Applied Processor:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
        
        The following argument positions are considered usable:
          uargs(U11) = {1},
          uargs(U21) = {1,2},
          uargs(U22) = {1},
          uargs(U31) = {1},
          uargs(U41) = {1,2},
          uargs(U42) = {1},
          uargs(U51) = {1,2},
          uargs(U52) = {1},
          uargs(U61) = {1},
          uargs(U71) = {1,2},
          uargs(U72) = {1},
          uargs(U81) = {1},
          uargs(__) = {2},
          uargs(activate) = {1},
          uargs(isList) = {1},
          uargs(isNeList) = {1},
          uargs(isNePal) = {1},
          uargs(isPal) = {1},
          uargs(isQid) = {1},
          uargs(n____) = {2}
        
        Following symbols are considered usable:
          all
        TcT has computed the following interpretation:
               p(U11) = [1 0] x_1 + [0]            
                        [0 0]       [1]            
               p(U21) = [1 0] x_1 + [1 0] x_2 + [4]
                        [0 0]       [0 0]       [0]
               p(U22) = [1 0] x_1 + [0]            
                        [0 0]       [0]            
               p(U31) = [1 0] x_1 + [0]            
                        [0 0]       [0]            
               p(U41) = [1 0] x_1 + [1 0] x_2 + [4]
                        [0 0]       [0 0]       [2]
               p(U42) = [1 0] x_1 + [1]            
                        [0 0]       [2]            
               p(U51) = [1 0] x_1 + [1 0] x_2 + [4]
                        [0 0]       [0 0]       [2]
               p(U52) = [1 0] x_1 + [0]            
                        [0 0]       [2]            
               p(U61) = [1 0] x_1 + [0]            
                        [1 0]       [0]            
               p(U71) = [1 0] x_1 + [1 0] x_2 + [7]
                        [0 1]       [0 0]       [7]
               p(U72) = [1 7] x_1 + [0]            
                        [0 1]       [1]            
               p(U81) = [1 0] x_1 + [0]            
                        [0 0]       [0]            
                p(__) = [1 4] x_1 + [1 0] x_2 + [4]
                        [2 2]       [0 1]       [1]
                 p(a) = [0]                        
                        [5]                        
          p(activate) = [1 0] x_1 + [0]            
                        [2 4]       [0]            
                 p(e) = [4]                        
                        [0]                        
                 p(i) = [0]                        
                        [0]                        
            p(isList) = [1 0] x_1 + [0]            
                        [0 0]       [2]            
          p(isNeList) = [1 0] x_1 + [0]            
                        [0 0]       [2]            
           p(isNePal) = [1 0] x_1 + [0]            
                        [1 0]       [0]            
             p(isPal) = [1 0] x_1 + [0]            
                        [0 0]       [1]            
             p(isQid) = [1 0] x_1 + [0]            
                        [2 0]       [1]            
             p(n____) = [1 4] x_1 + [1 0] x_2 + [4]
                        [0 0]       [0 1]       [0]
              p(n__a) = [0]                        
                        [2]                        
              p(n__e) = [4]                        
                        [0]                        
              p(n__i) = [0]                        
                        [0]                        
            p(n__nil) = [4]                        
                        [0]                        
              p(n__o) = [0]                        
                        [0]                        
              p(n__u) = [4]                        
                        [0]                        
               p(nil) = [4]                        
                        [0]                        
                 p(o) = [0]                        
                        [0]                        
                p(tt) = [0]                        
                        [0]                        
                 p(u) = [4]                        
                        [3]                        
        
        Following rules are strictly oriented:
        __(__(X,Y),Z) = [9 12] X + [1 4] Y + [1 0] Z + [12]
                        [6 12]     [2 2]     [0 1]     [11]
                      > [1 4] X + [1 4] Y + [1 0] Z + [8]  
                        [2 2]     [2 2]     [0 1]     [2]  
                      = __(X,__(Y,Z))                      
        
        
        Following rules are (at-least) weakly oriented:
                        U11(tt()) =  [0]                                     
                                     [1]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                     U21(tt(),V2) =  [1 0] V2 + [4]                          
                                     [0 0]      [0]                          
                                  >= [1 0] V2 + [0]                          
                                     [0 0]      [0]                          
                                  =  U22(isList(activate(V2)))               
        
                        U22(tt()) =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                        U31(tt()) =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                     U41(tt(),V2) =  [1 0] V2 + [4]                          
                                     [0 0]      [2]                          
                                  >= [1 0] V2 + [1]                          
                                     [0 0]      [2]                          
                                  =  U42(isNeList(activate(V2)))             
        
                        U42(tt()) =  [1]                                     
                                     [2]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                     U51(tt(),V2) =  [1 0] V2 + [4]                          
                                     [0 0]      [2]                          
                                  >= [1 0] V2 + [0]                          
                                     [0 0]      [2]                          
                                  =  U52(isList(activate(V2)))               
        
                        U52(tt()) =  [0]                                     
                                     [2]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                        U61(tt()) =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                      U71(tt(),P) =  [1 0] P + [7]                           
                                     [0 0]     [7]                           
                                  >= [1 0] P + [7]                           
                                     [0 0]     [2]                           
                                  =  U72(isPal(activate(P)))                 
        
                        U72(tt()) =  [0]                                     
                                     [1]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                        U81(tt()) =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                      __(X,nil()) =  [1 4] X + [8]                           
                                     [2 2]     [1]                           
                                  >= [1 0] X + [0]                           
                                     [0 1]     [0]                           
                                  =  X                                       
        
                        __(X1,X2) =  [1 4] X1 + [1 0] X2 + [4]               
                                     [2 2]      [0 1]      [1]               
                                  >= [1 4] X1 + [1 0] X2 + [4]               
                                     [0 0]      [0 1]      [0]               
                                  =  n____(X1,X2)                            
        
                      __(nil(),X) =  [1 0] X + [8]                           
                                     [0 1]     [9]                           
                                  >= [1 0] X + [0]                           
                                     [0 1]     [0]                           
                                  =  X                                       
        
                              a() =  [0]                                     
                                     [5]                                     
                                  >= [0]                                     
                                     [2]                                     
                                  =  n__a()                                  
        
                      activate(X) =  [1 0] X + [0]                           
                                     [2 4]     [0]                           
                                  >= [1 0] X + [0]                           
                                     [0 1]     [0]                           
                                  =  X                                       
        
           activate(n____(X1,X2)) =  [1 4] X1 + [1 0] X2 + [4]               
                                     [2 8]      [2 4]      [8]               
                                  >= [1 4] X1 + [1 0] X2 + [4]               
                                     [2 2]      [0 1]      [1]               
                                  =  __(X1,X2)                               
        
                 activate(n__a()) =  [0]                                     
                                     [8]                                     
                                  >= [0]                                     
                                     [5]                                     
                                  =  a()                                     
        
                 activate(n__e()) =  [4]                                     
                                     [8]                                     
                                  >= [4]                                     
                                     [0]                                     
                                  =  e()                                     
        
                 activate(n__i()) =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  i()                                     
        
               activate(n__nil()) =  [4]                                     
                                     [8]                                     
                                  >= [4]                                     
                                     [0]                                     
                                  =  nil()                                   
        
                 activate(n__o()) =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  o()                                     
        
                 activate(n__u()) =  [4]                                     
                                     [8]                                     
                                  >= [4]                                     
                                     [3]                                     
                                  =  u()                                     
        
                              e() =  [4]                                     
                                     [0]                                     
                                  >= [4]                                     
                                     [0]                                     
                                  =  n__e()                                  
        
                              i() =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  n__i()                                  
        
                        isList(V) =  [1 0] V + [0]                           
                                     [0 0]     [2]                           
                                  >= [1 0] V + [0]                           
                                     [0 0]     [1]                           
                                  =  U11(isNeList(activate(V)))              
        
             isList(n____(V1,V2)) =  [1 4] V1 + [1 0] V2 + [4]               
                                     [0 0]      [0 0]      [2]               
                                  >= [1 0] V1 + [1 0] V2 + [4]               
                                     [0 0]      [0 0]      [0]               
                                  =  U21(isList(activate(V1)),activate(V2))  
        
                 isList(n__nil()) =  [4]                                     
                                     [2]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                      isNeList(V) =  [1 0] V + [0]                           
                                     [0 0]     [2]                           
                                  >= [1 0] V + [0]                           
                                     [0 0]     [0]                           
                                  =  U31(isQid(activate(V)))                 
        
           isNeList(n____(V1,V2)) =  [1 4] V1 + [1 0] V2 + [4]               
                                     [0 0]      [0 0]      [2]               
                                  >= [1 0] V1 + [1 0] V2 + [4]               
                                     [0 0]      [0 0]      [2]               
                                  =  U41(isList(activate(V1)),activate(V2))  
        
           isNeList(n____(V1,V2)) =  [1 4] V1 + [1 0] V2 + [4]               
                                     [0 0]      [0 0]      [2]               
                                  >= [1 0] V1 + [1 0] V2 + [4]               
                                     [0 0]      [0 0]      [2]               
                                  =  U51(isNeList(activate(V1)),activate(V2))
        
                       isNePal(V) =  [1 0] V + [0]                           
                                     [1 0]     [0]                           
                                  >= [1 0] V + [0]                           
                                     [1 0]     [0]                           
                                  =  U61(isQid(activate(V)))                 
        
        isNePal(n____(I,__(P,I))) =  [2 4] I + [1 4] P + [8]                 
                                     [2 4]     [1 4]     [8]                 
                                  >= [1 0] I + [1 0] P + [7]                 
                                     [2 0]     [0 0]     [8]                 
                                  =  U71(isQid(activate(I)),activate(P))     
        
                         isPal(V) =  [1 0] V + [0]                           
                                     [0 0]     [1]                           
                                  >= [1 0] V + [0]                           
                                     [0 0]     [0]                           
                                  =  U81(isNePal(activate(V)))               
        
                  isPal(n__nil()) =  [4]                                     
                                     [1]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                    isQid(n__a()) =  [0]                                     
                                     [1]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                    isQid(n__e()) =  [4]                                     
                                     [9]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                    isQid(n__i()) =  [0]                                     
                                     [1]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                    isQid(n__o()) =  [0]                                     
                                     [1]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                    isQid(n__u()) =  [4]                                     
                                     [9]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  tt()                                    
        
                            nil() =  [4]                                     
                                     [0]                                     
                                  >= [4]                                     
                                     [0]                                     
                                  =  n__nil()                                
        
                              o() =  [0]                                     
                                     [0]                                     
                                  >= [0]                                     
                                     [0]                                     
                                  =  n__o()                                  
        
                              u() =  [4]                                     
                                     [3]                                     
                                  >= [4]                                     
                                     [0]                                     
                                  =  n__u()                                  
        
* Step 13: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            U11(tt()) -> tt()
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            __(nil(),X) -> X
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> U11(isNeList(activate(V)))
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isList(n__nil()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
            ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
            ,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
            ,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))