* Step 1: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            __(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__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            and(tt(),X) -> activate(X)
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [4]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [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) = [0]                  
                   p(n__i) = [0]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [0]         
                 p(n__nil) = [0]                  
                   p(n__o) = [0]                  
                   p(n__u) = [0]                  
                    p(nil) = [7]                  
                      p(o) = [0]                  
                     p(tt) = [1]                  
                      p(u) = [0]                  
          
          Following rules are strictly oriented:
                        __(X,nil()) = [1] X + [11]                                 
                                    > [1] X + [0]                                  
                                    = X                                            
          
                          __(X1,X2) = [1] X1 + [1] X2 + [4]                        
                                    > [1] X1 + [1] X2 + [0]                        
                                    = n____(X1,X2)                                 
          
                        __(nil(),X) = [1] X + [11]                                 
                                    > [1] X + [0]                                  
                                    = X                                            
          
                        and(tt(),X) = [1] X + [1]                                  
                                    > [1] X + [0]                                  
                                    = activate(X)                                  
          
          isNePal(n____(I,__(P,I))) = [2] I + [1] P + [4]                          
                                    > [1] I + [1] P + [0]                          
                                    = and(isQid(activate(I)),n__isPal(activate(P)))
          
                              nil() = [7]                                          
                                    > [0]                                          
                                    = n__nil()                                     
          
          
          Following rules are (at-least) weakly oriented:
                     __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [8]                        
                                   >= [1] X + [1] Y + [1] Z + [8]                        
                                   =  __(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 + [4]                              
                                   =  __(X1,X2)                                          
          
                  activate(n__a()) =  [0]                                                
                                   >= [0]                                                
                                   =  a()                                                
          
                  activate(n__e()) =  [0]                                                
                                   >= [0]                                                
                                   =  e()                                                
          
                  activate(n__i()) =  [0]                                                
                                   >= [0]                                                
                                   =  i()                                                
          
            activate(n__isList(X)) =  [1] X + [0]                                        
                                   >= [1] X + [0]                                        
                                   =  isList(X)                                          
          
          activate(n__isNeList(X)) =  [1] X + [0]                                        
                                   >= [1] X + [0]                                        
                                   =  isNeList(X)                                        
          
             activate(n__isPal(X)) =  [1] X + [0]                                        
                                   >= [1] X + [0]                                        
                                   =  isPal(X)                                           
          
                activate(n__nil()) =  [0]                                                
                                   >= [7]                                                
                                   =  nil()                                              
          
                  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 + [0]                                        
                                   >= [1] V + [0]                                        
                                   =  isNeList(activate(V))                              
          
                         isList(X) =  [1] X + [0]                                        
                                   >= [1] X + [0]                                        
                                   =  n__isList(X)                                       
          
              isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                   >= [1] V1 + [1] V2 + [0]                              
                                   =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                  isList(n__nil()) =  [0]                                                
                                   >= [1]                                                
                                   =  tt()                                               
          
                       isNeList(V) =  [1] V + [0]                                        
                                   >= [1] V + [0]                                        
                                   =  isQid(activate(V))                                 
          
                       isNeList(X) =  [1] X + [0]                                        
                                   >= [1] X + [0]                                        
                                   =  n__isNeList(X)                                     
          
            isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                   >= [1] V1 + [1] V2 + [0]                              
                                   =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
            isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                   >= [1] V1 + [1] V2 + [0]                              
                                   =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                        isNePal(V) =  [1] V + [0]                                        
                                   >= [1] V + [0]                                        
                                   =  isQid(activate(V))                                 
          
                          isPal(V) =  [1] V + [0]                                        
                                   >= [1] V + [0]                                        
                                   =  isNePal(activate(V))                               
          
                          isPal(X) =  [1] X + [0]                                        
                                   >= [1] X + [0]                                        
                                   =  n__isPal(X)                                        
          
                   isPal(n__nil()) =  [0]                                                
                                   >= [1]                                                
                                   =  tt()                                               
          
                     isQid(n__a()) =  [0]                                                
                                   >= [1]                                                
                                   =  tt()                                               
          
                     isQid(n__e()) =  [0]                                                
                                   >= [1]                                                
                                   =  tt()                                               
          
                     isQid(n__i()) =  [0]                                                
                                   >= [1]                                                
                                   =  tt()                                               
          
                     isQid(n__o()) =  [0]                                                
                                   >= [1]                                                
                                   =  tt()                                               
          
                     isQid(n__u()) =  [0]                                                
                                   >= [1]                                                
                                   =  tt()                                               
          
                               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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            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__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            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()
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            and(tt(),X) -> activate(X)
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            nil() -> n__nil()
        - Signature:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [0]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [0]                  
                      p(i) = [0]                  
                 p(isList) = [1] x1 + [0]         
               p(isNeList) = [1] x1 + [0]         
                p(isNePal) = [1] x1 + [4]         
                  p(isPal) = [1] x1 + [0]         
                  p(isQid) = [1] x1 + [0]         
                  p(n____) = [1] x1 + [1] x2 + [0]
                   p(n__a) = [6]                  
                   p(n__e) = [1]                  
                   p(n__i) = [0]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [4]         
                 p(n__nil) = [0]                  
                   p(n__o) = [0]                  
                   p(n__u) = [0]                  
                    p(nil) = [0]                  
                      p(o) = [2]                  
                     p(tt) = [0]                  
                      p(u) = [1]                  
          
          Following rules are strictly oriented:
               activate(n__a()) = [6]               
                                > [0]               
                                = a()               
          
               activate(n__e()) = [1]               
                                > [0]               
                                = e()               
          
          activate(n__isPal(X)) = [1] X + [4]       
                                > [1] X + [0]       
                                = isPal(X)          
          
                     isNePal(V) = [1] V + [4]       
                                > [1] V + [0]       
                                = isQid(activate(V))
          
                  isQid(n__a()) = [6]               
                                > [0]               
                                = tt()              
          
                  isQid(n__e()) = [1]               
                                > [0]               
                                = tt()              
          
                            o() = [2]               
                                > [0]               
                                = n__o()            
          
                            u() = [1]               
                                > [0]               
                                = n__u()            
          
          
          Following rules are (at-least) weakly oriented:
                        __(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]                                                
                                    >= [6]                                                
                                    =  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__i()) =  [0]                                                
                                    >= [0]                                                
                                    =  i()                                                
          
             activate(n__isList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isNeList(X)                                        
          
                 activate(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [0]                                                
                                    >= [2]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [0]                                                
                                    >= [1]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  activate(X)                                        
          
                                e() =  [0]                                                
                                    >= [1]                                                
                                    =  n__e()                                             
          
                                i() =  [0]                                                
                                    >= [0]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [4]                                
                                    >= [1] I + [1] P + [4]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [0]                                        
                                    >= [1] V + [4]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [0]                                        
                                    >= [1] X + [4]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [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()                                           
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__i()) -> i()
            activate(n__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            isPal(n__nil()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__isPal(X)) -> isPal(X)
            and(tt(),X) -> activate(X)
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [0]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [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) = [0]                  
                   p(n__i) = [0]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [0]         
                 p(n__nil) = [0]                  
                   p(n__o) = [0]                  
                   p(n__u) = [1]                  
                    p(nil) = [0]                  
                      p(o) = [0]                  
                     p(tt) = [0]                  
                      p(u) = [1]                  
          
          Following rules are strictly oriented:
          isQid(n__u()) = [1] 
                        > [0] 
                        = tt()
          
          
          Following rules are (at-least) weakly oriented:
                        __(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__isList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [0]                                                
                                    >= [0]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [1]                                                
                                    >= [1]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  activate(X)                                        
          
                                e() =  [0]                                                
                                    >= [0]                                                
                                    =  n__e()                                             
          
                                i() =  [0]                                                
                                    >= [0]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [0]                                
                                    >= [1] I + [1] P + [0]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__i()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                              nil() =  [0]                                                
                                    >= [0]                                                
                                    =  n__nil()                                           
          
                                o() =  [0]                                                
                                    >= [0]                                                
                                    =  n__o()                                             
          
                                u() =  [1]                                                
                                    >= [1]                                                
                                    =  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^2))
    + 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__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            isPal(n__nil()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__isPal(X)) -> isPal(X)
            and(tt(),X) -> activate(X)
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [0]
                      p(a) = [1]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [0]                  
                      p(i) = [0]                  
                 p(isList) = [1] x1 + [7]         
               p(isNeList) = [1] x1 + [0]         
                p(isNePal) = [1] x1 + [1]         
                  p(isPal) = [1] x1 + [0]         
                  p(isQid) = [1] x1 + [1]         
                  p(n____) = [1] x1 + [1] x2 + [0]
                   p(n__a) = [1]                  
                   p(n__e) = [2]                  
                   p(n__i) = [1]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [0]         
                 p(n__nil) = [0]                  
                   p(n__o) = [0]                  
                   p(n__u) = [1]                  
                    p(nil) = [0]                  
                      p(o) = [0]                  
                     p(tt) = [1]                  
                      p(u) = [1]                  
          
          Following rules are strictly oriented:
          activate(n__i()) = [1]                  
                           > [0]                  
                           = i()                  
          
                 isList(V) = [1] V + [7]          
                           > [1] V + [0]          
                           = isNeList(activate(V))
          
                 isList(X) = [1] X + [7]          
                           > [1] X + [0]          
                           = n__isList(X)         
          
          isList(n__nil()) = [7]                  
                           > [1]                  
                           = tt()                 
          
             isQid(n__i()) = [2]                  
                           > [1]                  
                           = tt()                 
          
          
          Following rules are (at-least) weakly oriented:
                        __(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() =  [1]                                                
                                    >= [1]                                                
                                    =  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()) =  [1]                                                
                                    >= [1]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [2]                                                
                                    >= [0]                                                
                                    =  e()                                                
          
             activate(n__isList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [7]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [0]                                                
                                    >= [0]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [1]                                                
                                    >= [1]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [1]                                        
                                    >= [1] X + [0]                                        
                                    =  activate(X)                                        
          
                                e() =  [0]                                                
                                    >= [2]                                                
                                    =  n__e()                                             
          
                                i() =  [0]                                                
                                    >= [1]                                                
                                    =  n__i()                                             
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [7]                              
                                    >= [1] V1 + [1] V2 + [7]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                        isNeList(V) =  [1] V + [0]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [7]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [1]                                
                                    >= [1] I + [1] P + [1]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [0]                                        
                                    >= [1] V + [1]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [0]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [3]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__u()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                              nil() =  [0]                                                
                                    >= [0]                                                
                                    =  n__nil()                                           
          
                                o() =  [0]                                                
                                    >= [0]                                                
                                    =  n__o()                                             
          
                                u() =  [1]                                                
                                    >= [1]                                                
                                    =  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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            isPal(n__nil()) -> tt()
            isQid(n__o()) -> tt()
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__isPal(X)) -> isPal(X)
            and(tt(),X) -> activate(X)
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n__nil()) -> tt()
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__u()) -> tt()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [1]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [0]                  
                      p(i) = [0]                  
                 p(isList) = [1] x1 + [0]         
               p(isNeList) = [1] x1 + [0]         
                p(isNePal) = [1] x1 + [2]         
                  p(isPal) = [1] x1 + [2]         
                  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__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [2]         
                 p(n__nil) = [0]                  
                   p(n__o) = [1]                  
                   p(n__u) = [2]                  
                    p(nil) = [4]                  
                      p(o) = [1]                  
                     p(tt) = [0]                  
                      p(u) = [2]                  
          
          Following rules are strictly oriented:
            isList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]                              
                                 > [1] V1 + [1] V2 + [0]                              
                                 = and(isList(activate(V1)),n__isList(activate(V2)))  
          
          isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]                              
                                 > [1] V1 + [1] V2 + [0]                              
                                 = and(isList(activate(V1)),n__isNeList(activate(V2)))
          
          isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]                              
                                 > [1] V1 + [1] V2 + [0]                              
                                 = and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                 isPal(n__nil()) = [2]                                                
                                 > [0]                                                
                                 = tt()                                               
          
                   isQid(n__o()) = [1]                                                
                                 > [0]                                                
                                 = tt()                                               
          
          
          Following rules are (at-least) weakly oriented:
                        __(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__isList(X)) =  [1] X + [0]                                  
                                    >= [1] X + [0]                                  
                                    =  isList(X)                                    
          
           activate(n__isNeList(X)) =  [1] X + [0]                                  
                                    >= [1] X + [0]                                  
                                    =  isNeList(X)                                  
          
              activate(n__isPal(X)) =  [1] X + [2]                                  
                                    >= [1] X + [2]                                  
                                    =  isPal(X)                                     
          
                 activate(n__nil()) =  [0]                                          
                                    >= [4]                                          
                                    =  nil()                                        
          
                   activate(n__o()) =  [1]                                          
                                    >= [1]                                          
                                    =  o()                                          
          
                   activate(n__u()) =  [2]                                          
                                    >= [2]                                          
                                    =  u()                                          
          
                        and(tt(),X) =  [1] X + [0]                                  
                                    >= [1] X + [0]                                  
                                    =  activate(X)                                  
          
                                e() =  [0]                                          
                                    >= [0]                                          
                                    =  n__e()                                       
          
                                i() =  [0]                                          
                                    >= [0]                                          
                                    =  n__i()                                       
          
                          isList(V) =  [1] V + [0]                                  
                                    >= [1] V + [0]                                  
                                    =  isNeList(activate(V))                        
          
                          isList(X) =  [1] X + [0]                                  
                                    >= [1] X + [0]                                  
                                    =  n__isList(X)                                 
          
                   isList(n__nil()) =  [0]                                          
                                    >= [0]                                          
                                    =  tt()                                         
          
                        isNeList(V) =  [1] V + [0]                                  
                                    >= [1] V + [0]                                  
                                    =  isQid(activate(V))                           
          
                        isNeList(X) =  [1] X + [0]                                  
                                    >= [1] X + [0]                                  
                                    =  n__isNeList(X)                               
          
                         isNePal(V) =  [1] V + [2]                                  
                                    >= [1] V + [0]                                  
                                    =  isQid(activate(V))                           
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [4]                          
                                    >= [1] I + [1] P + [2]                          
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))
          
                           isPal(V) =  [1] V + [2]                                  
                                    >= [1] V + [2]                                  
                                    =  isNePal(activate(V))                         
          
                           isPal(X) =  [1] X + [2]                                  
                                    >= [1] X + [2]                                  
                                    =  n__isPal(X)                                  
          
                      isQid(n__a()) =  [0]                                          
                                    >= [0]                                          
                                    =  tt()                                         
          
                      isQid(n__e()) =  [0]                                          
                                    >= [0]                                          
                                    =  tt()                                         
          
                      isQid(n__i()) =  [0]                                          
                                    >= [0]                                          
                                    =  tt()                                         
          
                      isQid(n__u()) =  [2]                                          
                                    >= [0]                                          
                                    =  tt()                                         
          
                              nil() =  [4]                                          
                                    >= [0]                                          
                                    =  n__nil()                                     
          
                                o() =  [1]                                          
                                    >= [1]                                          
                                    =  n__o()                                       
          
                                u() =  [2]                                          
                                    >= [2]                                          
                                    =  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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__isPal(X)) -> isPal(X)
            and(tt(),X) -> activate(X)
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(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()
            nil() -> n__nil()
            o() -> n__o()
            u() -> n__u()
        - Signature:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [4]
                      p(a) = [2]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [0]                  
                      p(i) = [0]                  
                 p(isList) = [1] x1 + [0]         
               p(isNeList) = [1] x1 + [0]         
                p(isNePal) = [1] x1 + [4]         
                  p(isPal) = [1] x1 + [6]         
                  p(isQid) = [1] x1 + [0]         
                  p(n____) = [1] x1 + [1] x2 + [0]
                   p(n__a) = [3]                  
                   p(n__e) = [0]                  
                   p(n__i) = [7]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [6]         
                 p(n__nil) = [3]                  
                   p(n__o) = [0]                  
                   p(n__u) = [0]                  
                    p(nil) = [3]                  
                      p(o) = [0]                  
                     p(tt) = [0]                  
                      p(u) = [1]                  
          
          Following rules are strictly oriented:
          isPal(V) = [1] V + [6]         
                   > [1] V + [4]         
                   = isNePal(activate(V))
          
          
          Following rules are (at-least) weakly oriented:
                        __(X,nil()) =  [1] X + [7]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [4]                              
                                    >= [1] X1 + [1] X2 + [0]                              
                                    =  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 + [7]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                                a() =  [2]                                                
                                    >= [3]                                                
                                    =  n__a()                                             
          
                        activate(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [0]                              
                                    >= [1] X1 + [1] X2 + [4]                              
                                    =  __(X1,X2)                                          
          
                   activate(n__a()) =  [3]                                                
                                    >= [2]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [0]                                                
                                    >= [0]                                                
                                    =  e()                                                
          
                   activate(n__i()) =  [7]                                                
                                    >= [0]                                                
                                    =  i()                                                
          
             activate(n__isList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [6]                                        
                                    >= [1] X + [6]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [3]                                                
                                    >= [3]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [0]                                                
                                    >= [0]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [0]                                                
                                    >= [1]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  activate(X)                                        
          
                                e() =  [0]                                                
                                    >= [0]                                                
                                    =  n__e()                                             
          
                                i() =  [0]                                                
                                    >= [7]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [3]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [0]                              
                                    >= [1] V1 + [1] V2 + [0]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [4]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [8]                                
                                    >= [1] I + [1] P + [6]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(X) =  [1] X + [6]                                        
                                    >= [1] X + [6]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [9]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [3]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__i()) =  [7]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__u()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                              nil() =  [3]                                                
                                    >= [3]                                                
                                    =  n__nil()                                           
          
                                o() =  [0]                                                
                                    >= [0]                                                
                                    =  n__o()                                             
          
                                u() =  [1]                                                
                                    >= [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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isPal(X) -> n__isPal(X)
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__isPal(X)) -> isPal(X)
            and(tt(),X) -> activate(X)
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> 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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [7]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [4]
                      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 + [6]
                   p(n__a) = [1]                  
                   p(n__e) = [1]                  
                   p(n__i) = [1]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [2]         
               p(n__isPal) = [1] x1 + [2]         
                 p(n__nil) = [1]                  
                   p(n__o) = [2]                  
                   p(n__u) = [1]                  
                    p(nil) = [5]                  
                      p(o) = [4]                  
                     p(tt) = [1]                  
                      p(u) = [3]                  
          
          Following rules are strictly oriented:
          activate(n__isNeList(X)) = [1] X + [2]
                                   > [1] X + [0]
                                   = isNeList(X)
          
          
          Following rules are (at-least) weakly oriented:
                        __(X,nil()) =  [1] X + [12]                                       
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [7]                              
                                    >= [1] X1 + [1] X2 + [6]                              
                                    =  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 + [12]                                       
                                    >= [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 + [6]                              
                                    >= [1] X1 + [1] X2 + [7]                              
                                    =  __(X1,X2)                                          
          
                   activate(n__a()) =  [1]                                                
                                    >= [0]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [1]                                                
                                    >= [0]                                                
                                    =  e()                                                
          
                   activate(n__i()) =  [1]                                                
                                    >= [0]                                                
                                    =  i()                                                
          
             activate(n__isList(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isList(X)                                          
          
              activate(n__isPal(X)) =  [1] X + [2]                                        
                                    >= [1] X + [0]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [1]                                                
                                    >= [5]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [2]                                                
                                    >= [4]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [1]                                                
                                    >= [3]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [5]                                        
                                    >= [1] X + [0]                                        
                                    =  activate(X)                                        
          
                                e() =  [0]                                                
                                    >= [1]                                                
                                    =  n__e()                                             
          
                                i() =  [0]                                                
                                    >= [1]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                              
                                    >= [1] V1 + [1] V2 + [4]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [0]                                        
                                    >= [1] X + [2]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                              
                                    >= [1] V1 + [1] V2 + [6]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                              
                                    >= [1] V1 + [1] V2 + [4]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [13]                               
                                    >= [1] I + [1] P + [6]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [0]                                        
                                    >= [1] X + [2]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__i()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__u()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                              nil() =  [5]                                                
                                    >= [1]                                                
                                    =  n__nil()                                           
          
                                o() =  [4]                                                
                                    >= [2]                                                
                                    =  n__o()                                             
          
                                u() =  [3]                                                
                                    >= [1]                                                
                                    =  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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__isList(X)) -> isList(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isPal(X) -> n__isPal(X)
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            and(tt(),X) -> activate(X)
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> 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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [2]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [0]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [0]                  
                      p(i) = [0]                  
                 p(isList) = [1] x1 + [1]         
               p(isNeList) = [1] x1 + [1]         
                p(isNePal) = [1] x1 + [0]         
                  p(isPal) = [1] x1 + [0]         
                  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__isList) = [1] x1 + [1]         
            p(n__isNeList) = [1] x1 + [1]         
               p(n__isPal) = [1] x1 + [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:
          isNeList(V) = [1] V + [1]       
                      > [1] V + [0]       
                      = isQid(activate(V))
          
          
          Following rules are (at-least) weakly oriented:
                        __(X,nil()) =  [1] X + [2]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [2]                              
                                    >= [1] X1 + [1] X2 + [1]                              
                                    =  n____(X1,X2)                                       
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [4]                        
                                    >= [1] X + [1] Y + [1] Z + [4]                        
                                    =  __(X,__(Y,Z))                                      
          
                        __(nil(),X) =  [1] X + [2]                                        
                                    >= [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 + [2]                              
                                    =  __(X1,X2)                                          
          
                   activate(n__a()) =  [0]                                                
                                    >= [0]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [0]                                                
                                    >= [0]                                                
                                    =  e()                                                
          
                   activate(n__i()) =  [0]                                                
                                    >= [0]                                                
                                    =  i()                                                
          
             activate(n__isList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [0]                                                
                                    >= [0]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [0]                                                
                                    >= [0]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  activate(X)                                        
          
                                e() =  [0]                                                
                                    >= [0]                                                
                                    =  n__e()                                             
          
                                i() =  [0]                                                
                                    >= [0]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [2]                              
                                    >= [1] V1 + [1] V2 + [2]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [1]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                        isNeList(X) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [2]                              
                                    >= [1] V1 + [1] V2 + [2]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [2]                              
                                    >= [1] V1 + [1] V2 + [2]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [3]                                
                                    >= [1] I + [1] P + [0]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [0]                                        
                                    >= [1] V + [0]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [0]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [0]                                                
                                    >= [0]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [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()                                             
          
                                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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__isList(X)) -> isList(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            e() -> n__e()
            i() -> n__i()
            isNeList(X) -> n__isNeList(X)
            isPal(X) -> n__isPal(X)
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            and(tt(),X) -> activate(X)
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> 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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [3]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [1]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [3]                  
                      p(i) = [0]                  
                 p(isList) = [1] x1 + [2]         
               p(isNeList) = [1] x1 + [1]         
                p(isNePal) = [1] x1 + [1]         
                  p(isPal) = [1] x1 + [2]         
                  p(isQid) = [1] x1 + [0]         
                  p(n____) = [1] x1 + [1] x2 + [3]
                   p(n__a) = [1]                  
                   p(n__e) = [2]                  
                   p(n__i) = [2]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [2]         
                 p(n__nil) = [0]                  
                   p(n__o) = [2]                  
                   p(n__u) = [3]                  
                    p(nil) = [0]                  
                      p(o) = [2]                  
                     p(tt) = [1]                  
                      p(u) = [3]                  
          
          Following rules are strictly oriented:
                     activate(X) = [1] X + [1]          
                                 > [1] X + [0]          
                                 = X                    
          
          activate(n____(X1,X2)) = [1] X1 + [1] X2 + [4]
                                 > [1] X1 + [1] X2 + [3]
                                 = __(X1,X2)            
          
              activate(n__nil()) = [1]                  
                                 > [0]                  
                                 = nil()                
          
                activate(n__o()) = [3]                  
                                 > [2]                  
                                 = o()                  
          
                activate(n__u()) = [4]                  
                                 > [3]                  
                                 = u()                  
          
                             e() = [3]                  
                                 > [2]                  
                                 = n__e()               
          
                     isNeList(X) = [1] X + [1]          
                                 > [1] X + [0]          
                                 = n__isNeList(X)       
          
          
          Following rules are (at-least) weakly oriented:
                        __(X,nil()) =  [1] X + [3]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [3]                              
                                    >= [1] X1 + [1] X2 + [3]                              
                                    =  n____(X1,X2)                                       
          
                      __(__(X,Y),Z) =  [1] X + [1] Y + [1] Z + [6]                        
                                    >= [1] X + [1] Y + [1] Z + [6]                        
                                    =  __(X,__(Y,Z))                                      
          
                        __(nil(),X) =  [1] X + [3]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                                a() =  [0]                                                
                                    >= [1]                                                
                                    =  n__a()                                             
          
                   activate(n__a()) =  [2]                                                
                                    >= [0]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [3]                                                
                                    >= [3]                                                
                                    =  e()                                                
          
                   activate(n__i()) =  [3]                                                
                                    >= [0]                                                
                                    =  i()                                                
          
             activate(n__isList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [2]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [3]                                        
                                    >= [1] X + [2]                                        
                                    =  isPal(X)                                           
          
                        and(tt(),X) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  activate(X)                                        
          
                                i() =  [0]                                                
                                    >= [2]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [2]                                        
                                    >= [1] V + [2]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [2]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                              
                                    >= [1] V1 + [1] V2 + [4]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [4]                              
                                    >= [1] V1 + [1] V2 + [4]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [4]                              
                                    >= [1] V1 + [1] V2 + [3]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [7]                                
                                    >= [1] I + [1] P + [4]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [2]                                        
                                    >= [1] V + [2]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [2]                                        
                                    >= [1] X + [2]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [1]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__i()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__u()) =  [3]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                              nil() =  [0]                                                
                                    >= [0]                                                
                                    =  n__nil()                                           
          
                                o() =  [2]                                                
                                    >= [2]                                                
                                    =  n__o()                                             
          
                                u() =  [3]                                                
                                    >= [3]                                                
                                    =  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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(n__isList(X)) -> isList(X)
            i() -> n__i()
            isPal(X) -> n__isPal(X)
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            and(tt(),X) -> activate(X)
            e() -> n__e()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> 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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [5]
                      p(a) = [0]                  
               p(activate) = [1] x1 + [1]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [4]                  
                      p(i) = [7]                  
                 p(isList) = [1] x1 + [4]         
               p(isNeList) = [1] x1 + [1]         
                p(isNePal) = [1] x1 + [2]         
                  p(isPal) = [1] x1 + [3]         
                  p(isQid) = [1] x1 + [0]         
                  p(n____) = [1] x1 + [1] x2 + [5]
                   p(n__a) = [4]                  
                   p(n__e) = [4]                  
                   p(n__i) = [6]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [2]         
                 p(n__nil) = [1]                  
                   p(n__o) = [6]                  
                   p(n__u) = [7]                  
                    p(nil) = [1]                  
                      p(o) = [6]                  
                     p(tt) = [4]                  
                      p(u) = [7]                  
          
          Following rules are strictly oriented:
               i() = [7]        
                   > [6]        
                   = n__i()     
          
          isPal(X) = [1] X + [3]
                   > [1] X + [2]
                   = n__isPal(X)
          
          
          Following rules are (at-least) weakly oriented:
                        __(X,nil()) =  [1] X + [6]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [5]                              
                                    >= [1] X1 + [1] X2 + [5]                              
                                    =  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 + [6]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                                a() =  [0]                                                
                                    >= [4]                                                
                                    =  n__a()                                             
          
                        activate(X) =  [1] X + [1]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [6]                              
                                    >= [1] X1 + [1] X2 + [5]                              
                                    =  __(X1,X2)                                          
          
                   activate(n__a()) =  [5]                                                
                                    >= [0]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [5]                                                
                                    >= [4]                                                
                                    =  e()                                                
          
                   activate(n__i()) =  [7]                                                
                                    >= [7]                                                
                                    =  i()                                                
          
             activate(n__isList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [4]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [3]                                        
                                    >= [1] X + [3]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [2]                                                
                                    >= [1]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [7]                                                
                                    >= [6]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [8]                                                
                                    >= [7]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [4]                                        
                                    >= [1] X + [1]                                        
                                    =  activate(X)                                        
          
                                e() =  [4]                                                
                                    >= [4]                                                
                                    =  n__e()                                             
          
                          isList(V) =  [1] V + [4]                                        
                                    >= [1] V + [2]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [4]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [9]                              
                                    >= [1] V1 + [1] V2 + [6]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [5]                                                
                                    >= [4]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [1]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                              
                                    >= [1] V1 + [1] V2 + [6]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                              
                                    >= [1] V1 + [1] V2 + [3]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [2]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [12]                               
                                    >= [1] I + [1] P + [4]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [3]                                        
                                    >= [1] V + [3]                                        
                                    =  isNePal(activate(V))                               
          
                    isPal(n__nil()) =  [4]                                                
                                    >= [4]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [4]                                                
                                    >= [4]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [4]                                                
                                    >= [4]                                                
                                    =  tt()                                               
          
                      isQid(n__i()) =  [6]                                                
                                    >= [4]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [6]                                                
                                    >= [4]                                                
                                    =  tt()                                               
          
                      isQid(n__u()) =  [7]                                                
                                    >= [4]                                                
                                    =  tt()                                               
          
                              nil() =  [1]                                                
                                    >= [1]                                                
                                    =  n__nil()                                           
          
                                o() =  [6]                                                
                                    >= [6]                                                
                                    =  n__o()                                             
          
                                u() =  [7]                                                
                                    >= [7]                                                
                                    =  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^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            a() -> n__a()
            activate(n__isList(X)) -> isList(X)
        - Weak TRS:
            __(X,nil()) -> X
            __(X1,X2) -> n____(X1,X2)
            __(nil(),X) -> X
            activate(X) -> X
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            and(tt(),X) -> activate(X)
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [5]
                      p(a) = [5]                  
               p(activate) = [1] x1 + [1]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [6]                  
                      p(i) = [4]                  
                 p(isList) = [1] x1 + [2]         
               p(isNeList) = [1] x1 + [1]         
                p(isNePal) = [1] x1 + [3]         
                  p(isPal) = [1] x1 + [4]         
                  p(isQid) = [1] x1 + [0]         
                  p(n____) = [1] x1 + [1] x2 + [4]
                   p(n__a) = [4]                  
                   p(n__e) = [5]                  
                   p(n__i) = [4]                  
              p(n__isList) = [1] x1 + [0]         
            p(n__isNeList) = [1] x1 + [1]         
               p(n__isPal) = [1] x1 + [4]         
                 p(n__nil) = [2]                  
                   p(n__o) = [2]                  
                   p(n__u) = [2]                  
                    p(nil) = [2]                  
                      p(o) = [2]                  
                     p(tt) = [1]                  
                      p(u) = [3]                  
          
          Following rules are strictly oriented:
          a() = [5]   
              > [4]   
              = n__a()
          
          
          Following rules are (at-least) weakly oriented:
                        __(X,nil()) =  [1] X + [7]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [5]                              
                                    >= [1] X1 + [1] X2 + [4]                              
                                    =  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 + [7]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                        activate(X) =  [1] X + [1]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [5]                              
                                    >= [1] X1 + [1] X2 + [5]                              
                                    =  __(X1,X2)                                          
          
                   activate(n__a()) =  [5]                                                
                                    >= [5]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [6]                                                
                                    >= [6]                                                
                                    =  e()                                                
          
                   activate(n__i()) =  [5]                                                
                                    >= [4]                                                
                                    =  i()                                                
          
             activate(n__isList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [2]                                        
                                    =  isList(X)                                          
          
           activate(n__isNeList(X)) =  [1] X + [2]                                        
                                    >= [1] X + [1]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [5]                                        
                                    >= [1] X + [4]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [3]                                                
                                    >= [2]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [3]                                                
                                    >= [2]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [3]                                                
                                    >= [3]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  activate(X)                                        
          
                                e() =  [6]                                                
                                    >= [5]                                                
                                    =  n__e()                                             
          
                                i() =  [4]                                                
                                    >= [4]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [2]                                        
                                    >= [1] V + [2]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [2]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                              
                                    >= [1] V1 + [1] V2 + [4]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [4]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                              
                                    >= [1] V1 + [1] V2 + [5]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                              
                                    >= [1] V1 + [1] V2 + [3]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [3]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [12]                               
                                    >= [1] I + [1] P + [6]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [4]                                        
                                    >= [1] V + [4]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [4]                                        
                                    >= [1] X + [4]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [6]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [4]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [5]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__i()) =  [4]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__u()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                              nil() =  [2]                                                
                                    >= [2]                                                
                                    =  n__nil()                                           
          
                                o() =  [2]                                                
                                    >= [2]                                                
                                    =  n__o()                                             
          
                                u() =  [3]                                                
                                    >= [2]                                                
                                    =  n__u()                                             
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 12: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            activate(n__isList(X)) -> isList(X)
        - Weak TRS:
            __(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__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            and(tt(),X) -> activate(X)
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
            uargs(activate) = {1},
            uargs(and) = {1,2},
            uargs(isList) = {1},
            uargs(isNeList) = {1},
            uargs(isNePal) = {1},
            uargs(isPal) = {1},
            uargs(isQid) = {1},
            uargs(n____) = {2},
            uargs(n__isList) = {1},
            uargs(n__isNeList) = {1},
            uargs(n__isPal) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                     p(__) = [1] x1 + [1] x2 + [5]
                      p(a) = [2]                  
               p(activate) = [1] x1 + [1]         
                    p(and) = [1] x1 + [1] x2 + [0]
                      p(e) = [2]                  
                      p(i) = [4]                  
                 p(isList) = [1] x1 + [2]         
               p(isNeList) = [1] x1 + [1]         
                p(isNePal) = [1] x1 + [1]         
                  p(isPal) = [1] x1 + [5]         
                  p(isQid) = [1] x1 + [0]         
                  p(n____) = [1] x1 + [1] x2 + [4]
                   p(n__a) = [2]                  
                   p(n__e) = [2]                  
                   p(n__i) = [4]                  
              p(n__isList) = [1] x1 + [2]         
            p(n__isNeList) = [1] x1 + [0]         
               p(n__isPal) = [1] x1 + [5]         
                 p(n__nil) = [4]                  
                   p(n__o) = [2]                  
                   p(n__u) = [3]                  
                    p(nil) = [4]                  
                      p(o) = [2]                  
                     p(tt) = [1]                  
                      p(u) = [4]                  
          
          Following rules are strictly oriented:
          activate(n__isList(X)) = [1] X + [3]
                                 > [1] X + [2]
                                 = isList(X)  
          
          
          Following rules are (at-least) weakly oriented:
                        __(X,nil()) =  [1] X + [9]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                          __(X1,X2) =  [1] X1 + [1] X2 + [5]                              
                                    >= [1] X1 + [1] X2 + [4]                              
                                    =  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 + [9]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
                                a() =  [2]                                                
                                    >= [2]                                                
                                    =  n__a()                                             
          
                        activate(X) =  [1] X + [1]                                        
                                    >= [1] X + [0]                                        
                                    =  X                                                  
          
             activate(n____(X1,X2)) =  [1] X1 + [1] X2 + [5]                              
                                    >= [1] X1 + [1] X2 + [5]                              
                                    =  __(X1,X2)                                          
          
                   activate(n__a()) =  [3]                                                
                                    >= [2]                                                
                                    =  a()                                                
          
                   activate(n__e()) =  [3]                                                
                                    >= [2]                                                
                                    =  e()                                                
          
                   activate(n__i()) =  [5]                                                
                                    >= [4]                                                
                                    =  i()                                                
          
           activate(n__isNeList(X)) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  isNeList(X)                                        
          
              activate(n__isPal(X)) =  [1] X + [6]                                        
                                    >= [1] X + [5]                                        
                                    =  isPal(X)                                           
          
                 activate(n__nil()) =  [5]                                                
                                    >= [4]                                                
                                    =  nil()                                              
          
                   activate(n__o()) =  [3]                                                
                                    >= [2]                                                
                                    =  o()                                                
          
                   activate(n__u()) =  [4]                                                
                                    >= [4]                                                
                                    =  u()                                                
          
                        and(tt(),X) =  [1] X + [1]                                        
                                    >= [1] X + [1]                                        
                                    =  activate(X)                                        
          
                                e() =  [2]                                                
                                    >= [2]                                                
                                    =  n__e()                                             
          
                                i() =  [4]                                                
                                    >= [4]                                                
                                    =  n__i()                                             
          
                          isList(V) =  [1] V + [2]                                        
                                    >= [1] V + [2]                                        
                                    =  isNeList(activate(V))                              
          
                          isList(X) =  [1] X + [2]                                        
                                    >= [1] X + [2]                                        
                                    =  n__isList(X)                                       
          
               isList(n____(V1,V2)) =  [1] V1 + [1] V2 + [6]                              
                                    >= [1] V1 + [1] V2 + [6]                              
                                    =  and(isList(activate(V1)),n__isList(activate(V2)))  
          
                   isList(n__nil()) =  [6]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                        isNeList(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
                        isNeList(X) =  [1] X + [1]                                        
                                    >= [1] X + [0]                                        
                                    =  n__isNeList(X)                                     
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                              
                                    >= [1] V1 + [1] V2 + [4]                              
                                    =  and(isList(activate(V1)),n__isNeList(activate(V2)))
          
             isNeList(n____(V1,V2)) =  [1] V1 + [1] V2 + [5]                              
                                    >= [1] V1 + [1] V2 + [5]                              
                                    =  and(isNeList(activate(V1)),n__isList(activate(V2)))
          
                         isNePal(V) =  [1] V + [1]                                        
                                    >= [1] V + [1]                                        
                                    =  isQid(activate(V))                                 
          
          isNePal(n____(I,__(P,I))) =  [2] I + [1] P + [10]                               
                                    >= [1] I + [1] P + [7]                                
                                    =  and(isQid(activate(I)),n__isPal(activate(P)))      
          
                           isPal(V) =  [1] V + [5]                                        
                                    >= [1] V + [2]                                        
                                    =  isNePal(activate(V))                               
          
                           isPal(X) =  [1] X + [5]                                        
                                    >= [1] X + [5]                                        
                                    =  n__isPal(X)                                        
          
                    isPal(n__nil()) =  [9]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__a()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__e()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__i()) =  [4]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__o()) =  [2]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                      isQid(n__u()) =  [3]                                                
                                    >= [1]                                                
                                    =  tt()                                               
          
                              nil() =  [4]                                                
                                    >= [4]                                                
                                    =  n__nil()                                           
          
                                o() =  [2]                                                
                                    >= [2]                                                
                                    =  n__o()                                             
          
                                u() =  [4]                                                
                                    >= [3]                                                
                                    =  n__u()                                             
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 13: MI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
        - Weak TRS:
            __(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__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            and(tt(),X) -> activate(X)
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {2},
          uargs(activate) = {1},
          uargs(and) = {1,2},
          uargs(isList) = {1},
          uargs(isNeList) = {1},
          uargs(isNePal) = {1},
          uargs(isPal) = {1},
          uargs(isQid) = {1},
          uargs(n____) = {2},
          uargs(n__isList) = {1},
          uargs(n__isNeList) = {1},
          uargs(n__isPal) = {1}
        
        Following symbols are considered usable:
          all
        TcT has computed the following interpretation:
                   p(__) = [1 1] x_1 + [1 0] x_2 + [6]
                           [0 1]       [0 1]       [2]
                    p(a) = [5]                        
                           [0]                        
             p(activate) = [1 0] x_1 + [2]            
                           [0 4]       [0]            
                  p(and) = [1 0] x_1 + [1 0] x_2 + [0]
                           [0 0]       [0 5]       [0]
                    p(e) = [5]                        
                           [3]                        
                    p(i) = [2]                        
                           [2]                        
               p(isList) = [1 0] x_1 + [4]            
                           [0 0]       [0]            
             p(isNeList) = [1 0] x_1 + [2]            
                           [0 0]       [0]            
              p(isNePal) = [1 0] x_1 + [3]            
                           [0 0]       [0]            
                p(isPal) = [1 0] x_1 + [5]            
                           [0 0]       [0]            
                p(isQid) = [1 0] x_1 + [0]            
                           [0 0]       [0]            
                p(n____) = [1 1] x_1 + [1 0] x_2 + [6]
                           [0 1]       [0 1]       [1]
                 p(n__a) = [3]                        
                           [0]                        
                 p(n__e) = [5]                        
                           [2]                        
                 p(n__i) = [2]                        
                           [2]                        
            p(n__isList) = [1 0] x_1 + [2]            
                           [0 0]       [0]            
          p(n__isNeList) = [1 0] x_1 + [0]            
                           [0 0]       [0]            
             p(n__isPal) = [1 0] x_1 + [5]            
                           [0 0]       [0]            
               p(n__nil) = [1]                        
                           [0]                        
                 p(n__o) = [4]                        
                           [1]                        
                 p(n__u) = [2]                        
                           [1]                        
                  p(nil) = [1]                        
                           [0]                        
                    p(o) = [4]                        
                           [1]                        
                   p(tt) = [2]                        
                           [0]                        
                    p(u) = [2]                        
                           [2]                        
        
        Following rules are strictly oriented:
        __(__(X,Y),Z) = [1 2] X + [1 1] Y + [1 0] Z + [14]
                        [0 1]     [0 1]     [0 1]     [4] 
                      > [1 1] X + [1 1] Y + [1 0] Z + [12]
                        [0 1]     [0 1]     [0 1]     [4] 
                      = __(X,__(Y,Z))                     
        
        
        Following rules are (at-least) weakly oriented:
                      __(X,nil()) =  [1 1] X + [7]                                      
                                     [0 1]     [2]                                      
                                  >= [1 0] X + [0]                                      
                                     [0 1]     [0]                                      
                                  =  X                                                  
        
                        __(X1,X2) =  [1 1] X1 + [1 0] X2 + [6]                          
                                     [0 1]      [0 1]      [2]                          
                                  >= [1 1] X1 + [1 0] X2 + [6]                          
                                     [0 1]      [0 1]      [1]                          
                                  =  n____(X1,X2)                                       
        
                      __(nil(),X) =  [1 0] X + [7]                                      
                                     [0 1]     [2]                                      
                                  >= [1 0] X + [0]                                      
                                     [0 1]     [0]                                      
                                  =  X                                                  
        
                              a() =  [5]                                                
                                     [0]                                                
                                  >= [3]                                                
                                     [0]                                                
                                  =  n__a()                                             
        
                      activate(X) =  [1 0] X + [2]                                      
                                     [0 4]     [0]                                      
                                  >= [1 0] X + [0]                                      
                                     [0 1]     [0]                                      
                                  =  X                                                  
        
           activate(n____(X1,X2)) =  [1 1] X1 + [1 0] X2 + [8]                          
                                     [0 4]      [0 4]      [4]                          
                                  >= [1 1] X1 + [1 0] X2 + [6]                          
                                     [0 1]      [0 1]      [2]                          
                                  =  __(X1,X2)                                          
        
                 activate(n__a()) =  [5]                                                
                                     [0]                                                
                                  >= [5]                                                
                                     [0]                                                
                                  =  a()                                                
        
                 activate(n__e()) =  [7]                                                
                                     [8]                                                
                                  >= [5]                                                
                                     [3]                                                
                                  =  e()                                                
        
                 activate(n__i()) =  [4]                                                
                                     [8]                                                
                                  >= [2]                                                
                                     [2]                                                
                                  =  i()                                                
        
           activate(n__isList(X)) =  [1 0] X + [4]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] X + [4]                                      
                                     [0 0]     [0]                                      
                                  =  isList(X)                                          
        
         activate(n__isNeList(X)) =  [1 0] X + [2]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] X + [2]                                      
                                     [0 0]     [0]                                      
                                  =  isNeList(X)                                        
        
            activate(n__isPal(X)) =  [1 0] X + [7]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] X + [5]                                      
                                     [0 0]     [0]                                      
                                  =  isPal(X)                                           
        
               activate(n__nil()) =  [3]                                                
                                     [0]                                                
                                  >= [1]                                                
                                     [0]                                                
                                  =  nil()                                              
        
                 activate(n__o()) =  [6]                                                
                                     [4]                                                
                                  >= [4]                                                
                                     [1]                                                
                                  =  o()                                                
        
                 activate(n__u()) =  [4]                                                
                                     [4]                                                
                                  >= [2]                                                
                                     [2]                                                
                                  =  u()                                                
        
                      and(tt(),X) =  [1 0] X + [2]                                      
                                     [0 5]     [0]                                      
                                  >= [1 0] X + [2]                                      
                                     [0 4]     [0]                                      
                                  =  activate(X)                                        
        
                              e() =  [5]                                                
                                     [3]                                                
                                  >= [5]                                                
                                     [2]                                                
                                  =  n__e()                                             
        
                              i() =  [2]                                                
                                     [2]                                                
                                  >= [2]                                                
                                     [2]                                                
                                  =  n__i()                                             
        
                        isList(V) =  [1 0] V + [4]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] V + [4]                                      
                                     [0 0]     [0]                                      
                                  =  isNeList(activate(V))                              
        
                        isList(X) =  [1 0] X + [4]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] X + [2]                                      
                                     [0 0]     [0]                                      
                                  =  n__isList(X)                                       
        
             isList(n____(V1,V2)) =  [1 1] V1 + [1 0] V2 + [10]                         
                                     [0 0]      [0 0]      [0]                          
                                  >= [1 0] V1 + [1 0] V2 + [10]                         
                                     [0 0]      [0 0]      [0]                          
                                  =  and(isList(activate(V1)),n__isList(activate(V2)))  
        
                 isList(n__nil()) =  [5]                                                
                                     [0]                                                
                                  >= [2]                                                
                                     [0]                                                
                                  =  tt()                                               
        
                      isNeList(V) =  [1 0] V + [2]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] V + [2]                                      
                                     [0 0]     [0]                                      
                                  =  isQid(activate(V))                                 
        
                      isNeList(X) =  [1 0] X + [2]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] X + [0]                                      
                                     [0 0]     [0]                                      
                                  =  n__isNeList(X)                                     
        
           isNeList(n____(V1,V2)) =  [1 1] V1 + [1 0] V2 + [8]                          
                                     [0 0]      [0 0]      [0]                          
                                  >= [1 0] V1 + [1 0] V2 + [8]                          
                                     [0 0]      [0 0]      [0]                          
                                  =  and(isList(activate(V1)),n__isNeList(activate(V2)))
        
           isNeList(n____(V1,V2)) =  [1 1] V1 + [1 0] V2 + [8]                          
                                     [0 0]      [0 0]      [0]                          
                                  >= [1 0] V1 + [1 0] V2 + [8]                          
                                     [0 0]      [0 0]      [0]                          
                                  =  and(isNeList(activate(V1)),n__isList(activate(V2)))
        
                       isNePal(V) =  [1 0] V + [3]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] V + [2]                                      
                                     [0 0]     [0]                                      
                                  =  isQid(activate(V))                                 
        
        isNePal(n____(I,__(P,I))) =  [2 1] I + [1 1] P + [15]                           
                                     [0 0]     [0 0]     [0]                            
                                  >= [1 0] I + [1 0] P + [9]                            
                                     [0 0]     [0 0]     [0]                            
                                  =  and(isQid(activate(I)),n__isPal(activate(P)))      
        
                         isPal(V) =  [1 0] V + [5]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] V + [5]                                      
                                     [0 0]     [0]                                      
                                  =  isNePal(activate(V))                               
        
                         isPal(X) =  [1 0] X + [5]                                      
                                     [0 0]     [0]                                      
                                  >= [1 0] X + [5]                                      
                                     [0 0]     [0]                                      
                                  =  n__isPal(X)                                        
        
                  isPal(n__nil()) =  [6]                                                
                                     [0]                                                
                                  >= [2]                                                
                                     [0]                                                
                                  =  tt()                                               
        
                    isQid(n__a()) =  [3]                                                
                                     [0]                                                
                                  >= [2]                                                
                                     [0]                                                
                                  =  tt()                                               
        
                    isQid(n__e()) =  [5]                                                
                                     [0]                                                
                                  >= [2]                                                
                                     [0]                                                
                                  =  tt()                                               
        
                    isQid(n__i()) =  [2]                                                
                                     [0]                                                
                                  >= [2]                                                
                                     [0]                                                
                                  =  tt()                                               
        
                    isQid(n__o()) =  [4]                                                
                                     [0]                                                
                                  >= [2]                                                
                                     [0]                                                
                                  =  tt()                                               
        
                    isQid(n__u()) =  [2]                                                
                                     [0]                                                
                                  >= [2]                                                
                                     [0]                                                
                                  =  tt()                                               
        
                            nil() =  [1]                                                
                                     [0]                                                
                                  >= [1]                                                
                                     [0]                                                
                                  =  n__nil()                                           
        
                              o() =  [4]                                                
                                     [1]                                                
                                  >= [4]                                                
                                     [1]                                                
                                  =  n__o()                                             
        
                              u() =  [2]                                                
                                     [2]                                                
                                  >= [2]                                                
                                     [1]                                                
                                  =  n__u()                                             
        
* Step 14: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            __(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__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__nil()) -> nil()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            and(tt(),X) -> activate(X)
            e() -> n__e()
            i() -> n__i()
            isList(V) -> isNeList(activate(V))
            isList(X) -> n__isList(X)
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isList(n__nil()) -> tt()
            isNeList(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            isNePal(V) -> isQid(activate(V))
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            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:
            {__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
        - Obligation:
             runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o
            ,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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^2))