We consider the following Problem:

  Strict Trs:
    {  __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(X, nil()) -> X
     , __(nil(), X) -> X
     , and(tt(), X) -> activate(X)
     , isList(V) -> isNeList(activate(V))
     , isList(n__nil()) -> tt()
     , isList(n____(V1, V2)) ->
       and(isList(activate(V1)), n__isList(activate(V2)))
     , 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()
     , __(X1, X2) -> n____(X1, X2)
     , isList(X) -> n__isList(X)
     , isNeList(X) -> n__isNeList(X)
     , isPal(X) -> n__isPal(X)
     , a() -> n__a()
     , e() -> n__e()
     , i() -> n__i()
     , o() -> n__o()
     , u() -> n__u()
     , activate(n__nil()) -> nil()
     , activate(n____(X1, X2)) -> __(X1, X2)
     , activate(n__isList(X)) -> isList(X)
     , activate(n__isNeList(X)) -> isNeList(X)
     , activate(n__isPal(X)) -> isPal(X)
     , activate(n__a()) -> a()
     , activate(n__e()) -> e()
     , activate(n__i()) -> i()
     , activate(n__o()) -> o()
     , activate(n__u()) -> u()
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  Arguments of following rules are not normal-forms:
  {  __(__(X, Y), Z) -> __(X, __(Y, Z))
   , isNePal(n____(I, __(P, I))) ->
     and(isQid(activate(I)), n__isPal(activate(P)))
   , __(X, nil()) -> X
   , __(nil(), X) -> X}
  
  All above mentioned rules can be savely removed.
  
  We consider the following Problem:
  
    Strict Trs:
      {  and(tt(), X) -> activate(X)
       , isList(V) -> isNeList(activate(V))
       , isList(n__nil()) -> tt()
       , isList(n____(V1, V2)) ->
         and(isList(activate(V1)), n__isList(activate(V2)))
       , 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))
       , 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()
       , __(X1, X2) -> n____(X1, X2)
       , isList(X) -> n__isList(X)
       , isNeList(X) -> n__isNeList(X)
       , isPal(X) -> n__isPal(X)
       , a() -> n__a()
       , e() -> n__e()
       , i() -> n__i()
       , o() -> n__o()
       , u() -> n__u()
       , activate(n__nil()) -> nil()
       , activate(n____(X1, X2)) -> __(X1, X2)
       , activate(n__isList(X)) -> isList(X)
       , activate(n__isNeList(X)) -> isNeList(X)
       , activate(n__isPal(X)) -> isPal(X)
       , activate(n__a()) -> a()
       , activate(n__e()) -> e()
       , activate(n__i()) -> i()
       , activate(n__o()) -> o()
       , activate(n__u()) -> u()
       , activate(X) -> X}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^1))
  
  Proof:
    The weightgap principle applies, where following rules are oriented strictly:
    
    TRS Component:
      {  and(tt(), X) -> activate(X)
       , isList(n__nil()) -> tt()
       , isPal(n__nil()) -> tt()
       , isQid(n__a()) -> tt()
       , isQid(n__e()) -> tt()
       , isQid(n__i()) -> tt()
       , isQid(n__o()) -> tt()
       , isQid(n__u()) -> tt()
       , isList(X) -> n__isList(X)
       , isNeList(X) -> n__isNeList(X)
       , isPal(X) -> n__isPal(X)}
    
    Interpretation of nonconstant growth:
    -------------------------------------
      The following argument positions are usable:
        Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
        Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
        Uargs(n__isList) = {1}, Uargs(isQid) = {1},
        Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
        Uargs(n__isPal) = {}, Uargs(isPal) = {}
      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
      Interpretation Functions:
       __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                    [0 0]      [0 0]      [0]
       nil() = [0]
               [0]
       and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                     [0 0]      [0 0]      [1]
       tt() = [0]
              [0]
       activate(x1) = [1 0] x1 + [0]
                      [0 0]      [0]
       isList(x1) = [1 1] x1 + [1]
                    [0 0]      [1]
       isNeList(x1) = [1 1] x1 + [1]
                      [0 0]      [1]
       n__nil() = [0]
                  [0]
       n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                       [1 0]      [0 0]      [0]
       n__isList(x1) = [1 1] x1 + [0]
                       [0 0]      [0]
       isQid(x1) = [1 0] x1 + [1]
                   [0 0]      [1]
       n__isNeList(x1) = [1 1] x1 + [0]
                         [0 0]      [0]
       isNePal(x1) = [1 0] x1 + [1]
                     [0 0]      [1]
       n__isPal(x1) = [1 0] x1 + [0]
                      [0 0]      [0]
       isPal(x1) = [1 0] x1 + [1]
                   [0 0]      [1]
       n__a() = [0]
                [0]
       n__e() = [0]
                [0]
       n__i() = [0]
                [0]
       n__o() = [0]
                [0]
       n__u() = [0]
                [0]
       a() = [0]
             [0]
       e() = [0]
             [0]
       i() = [0]
             [0]
       o() = [0]
             [0]
       u() = [0]
             [0]
    
    The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Strict Trs:
        {  isList(V) -> isNeList(activate(V))
         , isList(n____(V1, V2)) ->
           and(isList(activate(V1)), n__isList(activate(V2)))
         , 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))
         , isPal(V) -> isNePal(activate(V))
         , nil() -> n__nil()
         , __(X1, X2) -> n____(X1, X2)
         , a() -> n__a()
         , e() -> n__e()
         , i() -> n__i()
         , o() -> n__o()
         , u() -> n__u()
         , activate(n__nil()) -> nil()
         , activate(n____(X1, X2)) -> __(X1, X2)
         , activate(n__isList(X)) -> isList(X)
         , activate(n__isNeList(X)) -> isNeList(X)
         , activate(n__isPal(X)) -> isPal(X)
         , activate(n__a()) -> a()
         , activate(n__e()) -> e()
         , activate(n__i()) -> i()
         , activate(n__o()) -> o()
         , activate(n__u()) -> u()
         , activate(X) -> X}
      Weak Trs:
        {  and(tt(), X) -> activate(X)
         , isList(n__nil()) -> tt()
         , isPal(n__nil()) -> tt()
         , isQid(n__a()) -> tt()
         , isQid(n__e()) -> tt()
         , isQid(n__i()) -> tt()
         , isQid(n__o()) -> tt()
         , isQid(n__u()) -> tt()
         , isList(X) -> n__isList(X)
         , isNeList(X) -> n__isNeList(X)
         , isPal(X) -> n__isPal(X)}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^1))
    
    Proof:
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component: {nil() -> n__nil()}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
          Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
          Uargs(n__isList) = {1}, Uargs(isQid) = {1},
          Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
          Uargs(n__isPal) = {}, Uargs(isPal) = {}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                      [0 0]      [0 0]      [0]
         nil() = [2]
                 [0]
         and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                       [0 0]      [0 0]      [1]
         tt() = [0]
                [0]
         activate(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
         isList(x1) = [1 1] x1 + [1]
                      [0 0]      [1]
         isNeList(x1) = [1 1] x1 + [1]
                        [0 0]      [1]
         n__nil() = [0]
                    [0]
         n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                         [1 0]      [0 0]      [0]
         n__isList(x1) = [1 1] x1 + [0]
                         [0 0]      [0]
         isQid(x1) = [1 0] x1 + [1]
                     [0 0]      [1]
         n__isNeList(x1) = [1 1] x1 + [0]
                           [0 0]      [0]
         isNePal(x1) = [1 0] x1 + [1]
                       [0 0]      [1]
         n__isPal(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
         isPal(x1) = [1 0] x1 + [1]
                     [0 0]      [1]
         n__a() = [0]
                  [0]
         n__e() = [0]
                  [0]
         n__i() = [0]
                  [0]
         n__o() = [0]
                  [0]
         n__u() = [0]
                  [0]
         a() = [0]
               [0]
         e() = [0]
               [0]
         i() = [0]
               [0]
         o() = [0]
               [0]
         u() = [0]
               [0]
      
      The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs:
          {  isList(V) -> isNeList(activate(V))
           , isList(n____(V1, V2)) ->
             and(isList(activate(V1)), n__isList(activate(V2)))
           , 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))
           , isPal(V) -> isNePal(activate(V))
           , __(X1, X2) -> n____(X1, X2)
           , a() -> n__a()
           , e() -> n__e()
           , i() -> n__i()
           , o() -> n__o()
           , u() -> n__u()
           , activate(n__nil()) -> nil()
           , activate(n____(X1, X2)) -> __(X1, X2)
           , activate(n__isList(X)) -> isList(X)
           , activate(n__isNeList(X)) -> isNeList(X)
           , activate(n__isPal(X)) -> isPal(X)
           , activate(n__a()) -> a()
           , activate(n__e()) -> e()
           , activate(n__i()) -> i()
           , activate(n__o()) -> o()
           , activate(n__u()) -> u()
           , activate(X) -> X}
        Weak Trs:
          {  nil() -> n__nil()
           , and(tt(), X) -> activate(X)
           , isList(n__nil()) -> tt()
           , isPal(n__nil()) -> tt()
           , isQid(n__a()) -> tt()
           , isQid(n__e()) -> tt()
           , isQid(n__i()) -> tt()
           , isQid(n__o()) -> tt()
           , isQid(n__u()) -> tt()
           , isList(X) -> n__isList(X)
           , isNeList(X) -> n__isNeList(X)
           , isPal(X) -> n__isPal(X)}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^1))
      
      Proof:
        The weightgap principle applies, where following rules are oriented strictly:
        
        TRS Component: {__(X1, X2) -> n____(X1, X2)}
        
        Interpretation of nonconstant growth:
        -------------------------------------
          The following argument positions are usable:
            Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
            Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
            Uargs(n__isList) = {1}, Uargs(isQid) = {1},
            Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
            Uargs(n__isPal) = {}, Uargs(isPal) = {}
          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           __(x1, x2) = [0 0] x1 + [1 0] x2 + [2]
                        [1 0]      [0 0]      [0]
           nil() = [0]
                   [0]
           and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                         [0 0]      [0 0]      [1]
           tt() = [0]
                  [0]
           activate(x1) = [1 0] x1 + [0]
                          [0 0]      [0]
           isList(x1) = [1 1] x1 + [1]
                        [0 0]      [1]
           isNeList(x1) = [1 1] x1 + [1]
                          [0 0]      [1]
           n__nil() = [0]
                      [0]
           n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                           [1 0]      [0 0]      [0]
           n__isList(x1) = [1 1] x1 + [0]
                           [0 0]      [0]
           isQid(x1) = [1 0] x1 + [1]
                       [0 0]      [1]
           n__isNeList(x1) = [1 1] x1 + [0]
                             [0 0]      [0]
           isNePal(x1) = [1 0] x1 + [1]
                         [0 0]      [1]
           n__isPal(x1) = [1 0] x1 + [0]
                          [0 0]      [0]
           isPal(x1) = [1 0] x1 + [1]
                       [0 0]      [1]
           n__a() = [0]
                    [0]
           n__e() = [0]
                    [0]
           n__i() = [0]
                    [0]
           n__o() = [0]
                    [0]
           n__u() = [0]
                    [0]
           a() = [0]
                 [0]
           e() = [0]
                 [0]
           i() = [0]
                 [0]
           o() = [0]
                 [0]
           u() = [0]
                 [0]
        
        The strictly oriented rules are moved into the weak component.
        
        We consider the following Problem:
        
          Strict Trs:
            {  isList(V) -> isNeList(activate(V))
             , isList(n____(V1, V2)) ->
               and(isList(activate(V1)), n__isList(activate(V2)))
             , 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))
             , isPal(V) -> isNePal(activate(V))
             , a() -> n__a()
             , e() -> n__e()
             , i() -> n__i()
             , o() -> n__o()
             , u() -> n__u()
             , activate(n__nil()) -> nil()
             , activate(n____(X1, X2)) -> __(X1, X2)
             , activate(n__isList(X)) -> isList(X)
             , activate(n__isNeList(X)) -> isNeList(X)
             , activate(n__isPal(X)) -> isPal(X)
             , activate(n__a()) -> a()
             , activate(n__e()) -> e()
             , activate(n__i()) -> i()
             , activate(n__o()) -> o()
             , activate(n__u()) -> u()
             , activate(X) -> X}
          Weak Trs:
            {  __(X1, X2) -> n____(X1, X2)
             , nil() -> n__nil()
             , and(tt(), X) -> activate(X)
             , isList(n__nil()) -> tt()
             , isPal(n__nil()) -> tt()
             , isQid(n__a()) -> tt()
             , isQid(n__e()) -> tt()
             , isQid(n__i()) -> tt()
             , isQid(n__o()) -> tt()
             , isQid(n__u()) -> tt()
             , isList(X) -> n__isList(X)
             , isNeList(X) -> n__isNeList(X)
             , isPal(X) -> n__isPal(X)}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^1))
        
        Proof:
          The weightgap principle applies, where following rules are oriented strictly:
          
          TRS Component: {a() -> n__a()}
          
          Interpretation of nonconstant growth:
          -------------------------------------
            The following argument positions are usable:
              Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
              Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
              Uargs(n__isList) = {1}, Uargs(isQid) = {1},
              Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
              Uargs(n__isPal) = {}, Uargs(isPal) = {}
            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                          [1 0]      [0 0]      [0]
             nil() = [0]
                     [0]
             and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                           [0 0]      [0 0]      [1]
             tt() = [0]
                    [0]
             activate(x1) = [1 0] x1 + [0]
                            [0 0]      [0]
             isList(x1) = [1 1] x1 + [1]
                          [0 0]      [1]
             isNeList(x1) = [1 1] x1 + [1]
                            [0 0]      [1]
             n__nil() = [0]
                        [0]
             n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                             [1 0]      [0 0]      [0]
             n__isList(x1) = [1 1] x1 + [0]
                             [0 0]      [0]
             isQid(x1) = [1 0] x1 + [1]
                         [0 0]      [1]
             n__isNeList(x1) = [1 1] x1 + [0]
                               [0 0]      [0]
             isNePal(x1) = [1 0] x1 + [1]
                           [0 0]      [1]
             n__isPal(x1) = [1 0] x1 + [0]
                            [0 0]      [0]
             isPal(x1) = [1 0] x1 + [1]
                         [0 0]      [1]
             n__a() = [0]
                      [0]
             n__e() = [0]
                      [0]
             n__i() = [0]
                      [0]
             n__o() = [0]
                      [0]
             n__u() = [0]
                      [0]
             a() = [2]
                   [0]
             e() = [0]
                   [0]
             i() = [0]
                   [0]
             o() = [0]
                   [0]
             u() = [0]
                   [0]
          
          The strictly oriented rules are moved into the weak component.
          
          We consider the following Problem:
          
            Strict Trs:
              {  isList(V) -> isNeList(activate(V))
               , isList(n____(V1, V2)) ->
                 and(isList(activate(V1)), n__isList(activate(V2)))
               , 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))
               , isPal(V) -> isNePal(activate(V))
               , e() -> n__e()
               , i() -> n__i()
               , o() -> n__o()
               , u() -> n__u()
               , activate(n__nil()) -> nil()
               , activate(n____(X1, X2)) -> __(X1, X2)
               , activate(n__isList(X)) -> isList(X)
               , activate(n__isNeList(X)) -> isNeList(X)
               , activate(n__isPal(X)) -> isPal(X)
               , activate(n__a()) -> a()
               , activate(n__e()) -> e()
               , activate(n__i()) -> i()
               , activate(n__o()) -> o()
               , activate(n__u()) -> u()
               , activate(X) -> X}
            Weak Trs:
              {  a() -> n__a()
               , __(X1, X2) -> n____(X1, X2)
               , nil() -> n__nil()
               , and(tt(), X) -> activate(X)
               , isList(n__nil()) -> tt()
               , isPal(n__nil()) -> tt()
               , isQid(n__a()) -> tt()
               , isQid(n__e()) -> tt()
               , isQid(n__i()) -> tt()
               , isQid(n__o()) -> tt()
               , isQid(n__u()) -> tt()
               , isList(X) -> n__isList(X)
               , isNeList(X) -> n__isNeList(X)
               , isPal(X) -> n__isPal(X)}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(?,O(n^1))
          
          Proof:
            The weightgap principle applies, where following rules are oriented strictly:
            
            TRS Component: {e() -> n__e()}
            
            Interpretation of nonconstant growth:
            -------------------------------------
              The following argument positions are usable:
                Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                Uargs(n__isPal) = {}, Uargs(isPal) = {}
              We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
              Interpretation Functions:
               __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                            [1 0]      [0 0]      [0]
               nil() = [0]
                       [0]
               and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 0]      [0 0]      [1]
               tt() = [0]
                      [0]
               activate(x1) = [1 0] x1 + [0]
                              [0 0]      [0]
               isList(x1) = [1 1] x1 + [1]
                            [0 0]      [1]
               isNeList(x1) = [1 1] x1 + [1]
                              [0 0]      [1]
               n__nil() = [0]
                          [0]
               n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                               [1 0]      [0 0]      [0]
               n__isList(x1) = [1 1] x1 + [0]
                               [0 0]      [0]
               isQid(x1) = [1 0] x1 + [1]
                           [0 0]      [1]
               n__isNeList(x1) = [1 1] x1 + [0]
                                 [0 0]      [0]
               isNePal(x1) = [1 0] x1 + [1]
                             [0 0]      [1]
               n__isPal(x1) = [1 0] x1 + [0]
                              [0 0]      [0]
               isPal(x1) = [1 0] x1 + [1]
                           [0 0]      [1]
               n__a() = [0]
                        [0]
               n__e() = [0]
                        [0]
               n__i() = [0]
                        [0]
               n__o() = [0]
                        [0]
               n__u() = [0]
                        [0]
               a() = [0]
                     [0]
               e() = [2]
                     [0]
               i() = [0]
                     [0]
               o() = [0]
                     [0]
               u() = [0]
                     [0]
            
            The strictly oriented rules are moved into the weak component.
            
            We consider the following Problem:
            
              Strict Trs:
                {  isList(V) -> isNeList(activate(V))
                 , isList(n____(V1, V2)) ->
                   and(isList(activate(V1)), n__isList(activate(V2)))
                 , 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))
                 , isPal(V) -> isNePal(activate(V))
                 , i() -> n__i()
                 , o() -> n__o()
                 , u() -> n__u()
                 , activate(n__nil()) -> nil()
                 , activate(n____(X1, X2)) -> __(X1, X2)
                 , activate(n__isList(X)) -> isList(X)
                 , activate(n__isNeList(X)) -> isNeList(X)
                 , activate(n__isPal(X)) -> isPal(X)
                 , activate(n__a()) -> a()
                 , activate(n__e()) -> e()
                 , activate(n__i()) -> i()
                 , activate(n__o()) -> o()
                 , activate(n__u()) -> u()
                 , activate(X) -> X}
              Weak Trs:
                {  e() -> n__e()
                 , a() -> n__a()
                 , __(X1, X2) -> n____(X1, X2)
                 , nil() -> n__nil()
                 , and(tt(), X) -> activate(X)
                 , isList(n__nil()) -> tt()
                 , isPal(n__nil()) -> tt()
                 , isQid(n__a()) -> tt()
                 , isQid(n__e()) -> tt()
                 , isQid(n__i()) -> tt()
                 , isQid(n__o()) -> tt()
                 , isQid(n__u()) -> tt()
                 , isList(X) -> n__isList(X)
                 , isNeList(X) -> n__isNeList(X)
                 , isPal(X) -> n__isPal(X)}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: YES(?,O(n^1))
            
            Proof:
              The weightgap principle applies, where following rules are oriented strictly:
              
              TRS Component: {i() -> n__i()}
              
              Interpretation of nonconstant growth:
              -------------------------------------
                The following argument positions are usable:
                  Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                  Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                  Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                  Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                  Uargs(n__isPal) = {}, Uargs(isPal) = {}
                We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                Interpretation Functions:
                 __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                              [1 0]      [0 0]      [0]
                 nil() = [0]
                         [0]
                 and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                               [0 0]      [0 0]      [1]
                 tt() = [0]
                        [0]
                 activate(x1) = [1 0] x1 + [0]
                                [0 0]      [0]
                 isList(x1) = [1 1] x1 + [1]
                              [0 0]      [1]
                 isNeList(x1) = [1 1] x1 + [1]
                                [0 0]      [1]
                 n__nil() = [0]
                            [0]
                 n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                 [1 0]      [0 0]      [0]
                 n__isList(x1) = [1 1] x1 + [0]
                                 [0 0]      [0]
                 isQid(x1) = [1 0] x1 + [1]
                             [0 0]      [1]
                 n__isNeList(x1) = [1 1] x1 + [0]
                                   [0 0]      [0]
                 isNePal(x1) = [1 0] x1 + [1]
                               [0 0]      [1]
                 n__isPal(x1) = [1 0] x1 + [0]
                                [0 0]      [0]
                 isPal(x1) = [1 0] x1 + [1]
                             [0 0]      [1]
                 n__a() = [0]
                          [0]
                 n__e() = [0]
                          [0]
                 n__i() = [0]
                          [0]
                 n__o() = [0]
                          [0]
                 n__u() = [0]
                          [0]
                 a() = [0]
                       [0]
                 e() = [0]
                       [0]
                 i() = [2]
                       [0]
                 o() = [0]
                       [0]
                 u() = [0]
                       [0]
              
              The strictly oriented rules are moved into the weak component.
              
              We consider the following Problem:
              
                Strict Trs:
                  {  isList(V) -> isNeList(activate(V))
                   , isList(n____(V1, V2)) ->
                     and(isList(activate(V1)), n__isList(activate(V2)))
                   , 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))
                   , isPal(V) -> isNePal(activate(V))
                   , o() -> n__o()
                   , u() -> n__u()
                   , activate(n__nil()) -> nil()
                   , activate(n____(X1, X2)) -> __(X1, X2)
                   , activate(n__isList(X)) -> isList(X)
                   , activate(n__isNeList(X)) -> isNeList(X)
                   , activate(n__isPal(X)) -> isPal(X)
                   , activate(n__a()) -> a()
                   , activate(n__e()) -> e()
                   , activate(n__i()) -> i()
                   , activate(n__o()) -> o()
                   , activate(n__u()) -> u()
                   , activate(X) -> X}
                Weak Trs:
                  {  i() -> n__i()
                   , e() -> n__e()
                   , a() -> n__a()
                   , __(X1, X2) -> n____(X1, X2)
                   , nil() -> n__nil()
                   , and(tt(), X) -> activate(X)
                   , isList(n__nil()) -> tt()
                   , isPal(n__nil()) -> tt()
                   , isQid(n__a()) -> tt()
                   , isQid(n__e()) -> tt()
                   , isQid(n__i()) -> tt()
                   , isQid(n__o()) -> tt()
                   , isQid(n__u()) -> tt()
                   , isList(X) -> n__isList(X)
                   , isNeList(X) -> n__isNeList(X)
                   , isPal(X) -> n__isPal(X)}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(?,O(n^1))
              
              Proof:
                The weightgap principle applies, where following rules are oriented strictly:
                
                TRS Component: {o() -> n__o()}
                
                Interpretation of nonconstant growth:
                -------------------------------------
                  The following argument positions are usable:
                    Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                    Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                    Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                    Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                    Uargs(n__isPal) = {}, Uargs(isPal) = {}
                  We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                  Interpretation Functions:
                   __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                [1 0]      [0 0]      [0]
                   nil() = [0]
                           [0]
                   and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                 [0 0]      [0 0]      [1]
                   tt() = [0]
                          [0]
                   activate(x1) = [1 0] x1 + [0]
                                  [0 0]      [0]
                   isList(x1) = [1 1] x1 + [1]
                                [0 0]      [1]
                   isNeList(x1) = [1 1] x1 + [1]
                                  [0 0]      [1]
                   n__nil() = [0]
                              [0]
                   n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                   [1 0]      [0 0]      [0]
                   n__isList(x1) = [1 1] x1 + [0]
                                   [0 0]      [0]
                   isQid(x1) = [1 0] x1 + [1]
                               [0 0]      [1]
                   n__isNeList(x1) = [1 1] x1 + [0]
                                     [0 0]      [0]
                   isNePal(x1) = [1 0] x1 + [1]
                                 [0 0]      [1]
                   n__isPal(x1) = [1 0] x1 + [0]
                                  [0 0]      [0]
                   isPal(x1) = [1 0] x1 + [1]
                               [0 0]      [1]
                   n__a() = [0]
                            [0]
                   n__e() = [0]
                            [0]
                   n__i() = [0]
                            [0]
                   n__o() = [0]
                            [0]
                   n__u() = [0]
                            [0]
                   a() = [0]
                         [0]
                   e() = [0]
                         [0]
                   i() = [0]
                         [0]
                   o() = [2]
                         [0]
                   u() = [0]
                         [0]
                
                The strictly oriented rules are moved into the weak component.
                
                We consider the following Problem:
                
                  Strict Trs:
                    {  isList(V) -> isNeList(activate(V))
                     , isList(n____(V1, V2)) ->
                       and(isList(activate(V1)), n__isList(activate(V2)))
                     , 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))
                     , isPal(V) -> isNePal(activate(V))
                     , u() -> n__u()
                     , activate(n__nil()) -> nil()
                     , activate(n____(X1, X2)) -> __(X1, X2)
                     , activate(n__isList(X)) -> isList(X)
                     , activate(n__isNeList(X)) -> isNeList(X)
                     , activate(n__isPal(X)) -> isPal(X)
                     , activate(n__a()) -> a()
                     , activate(n__e()) -> e()
                     , activate(n__i()) -> i()
                     , activate(n__o()) -> o()
                     , activate(n__u()) -> u()
                     , activate(X) -> X}
                  Weak Trs:
                    {  o() -> n__o()
                     , i() -> n__i()
                     , e() -> n__e()
                     , a() -> n__a()
                     , __(X1, X2) -> n____(X1, X2)
                     , nil() -> n__nil()
                     , and(tt(), X) -> activate(X)
                     , isList(n__nil()) -> tt()
                     , isPal(n__nil()) -> tt()
                     , isQid(n__a()) -> tt()
                     , isQid(n__e()) -> tt()
                     , isQid(n__i()) -> tt()
                     , isQid(n__o()) -> tt()
                     , isQid(n__u()) -> tt()
                     , isList(X) -> n__isList(X)
                     , isNeList(X) -> n__isNeList(X)
                     , isPal(X) -> n__isPal(X)}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(?,O(n^1))
                
                Proof:
                  The weightgap principle applies, where following rules are oriented strictly:
                  
                  TRS Component: {u() -> n__u()}
                  
                  Interpretation of nonconstant growth:
                  -------------------------------------
                    The following argument positions are usable:
                      Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                      Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                      Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                      Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                      Uargs(n__isPal) = {}, Uargs(isPal) = {}
                    We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                    Interpretation Functions:
                     __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                  [1 0]      [0 0]      [0]
                     nil() = [0]
                             [0]
                     and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                   [0 0]      [0 0]      [1]
                     tt() = [0]
                            [0]
                     activate(x1) = [1 0] x1 + [0]
                                    [0 0]      [0]
                     isList(x1) = [1 1] x1 + [1]
                                  [0 0]      [1]
                     isNeList(x1) = [1 1] x1 + [1]
                                    [0 0]      [1]
                     n__nil() = [0]
                                [0]
                     n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                     [1 0]      [0 0]      [0]
                     n__isList(x1) = [1 1] x1 + [0]
                                     [0 0]      [0]
                     isQid(x1) = [1 0] x1 + [1]
                                 [0 0]      [1]
                     n__isNeList(x1) = [1 1] x1 + [0]
                                       [0 0]      [0]
                     isNePal(x1) = [1 0] x1 + [1]
                                   [0 0]      [1]
                     n__isPal(x1) = [1 0] x1 + [0]
                                    [0 0]      [0]
                     isPal(x1) = [1 0] x1 + [1]
                                 [0 0]      [1]
                     n__a() = [0]
                              [0]
                     n__e() = [0]
                              [0]
                     n__i() = [0]
                              [0]
                     n__o() = [0]
                              [0]
                     n__u() = [0]
                              [0]
                     a() = [0]
                           [0]
                     e() = [0]
                           [0]
                     i() = [0]
                           [0]
                     o() = [0]
                           [0]
                     u() = [2]
                           [0]
                  
                  The strictly oriented rules are moved into the weak component.
                  
                  We consider the following Problem:
                  
                    Strict Trs:
                      {  isList(V) -> isNeList(activate(V))
                       , isList(n____(V1, V2)) ->
                         and(isList(activate(V1)), n__isList(activate(V2)))
                       , 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))
                       , isPal(V) -> isNePal(activate(V))
                       , activate(n__nil()) -> nil()
                       , activate(n____(X1, X2)) -> __(X1, X2)
                       , activate(n__isList(X)) -> isList(X)
                       , activate(n__isNeList(X)) -> isNeList(X)
                       , activate(n__isPal(X)) -> isPal(X)
                       , activate(n__a()) -> a()
                       , activate(n__e()) -> e()
                       , activate(n__i()) -> i()
                       , activate(n__o()) -> o()
                       , activate(n__u()) -> u()
                       , activate(X) -> X}
                    Weak Trs:
                      {  u() -> n__u()
                       , o() -> n__o()
                       , i() -> n__i()
                       , e() -> n__e()
                       , a() -> n__a()
                       , __(X1, X2) -> n____(X1, X2)
                       , nil() -> n__nil()
                       , and(tt(), X) -> activate(X)
                       , isList(n__nil()) -> tt()
                       , isPal(n__nil()) -> tt()
                       , isQid(n__a()) -> tt()
                       , isQid(n__e()) -> tt()
                       , isQid(n__i()) -> tt()
                       , isQid(n__o()) -> tt()
                       , isQid(n__u()) -> tt()
                       , isList(X) -> n__isList(X)
                       , isNeList(X) -> n__isNeList(X)
                       , isPal(X) -> n__isPal(X)}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(?,O(n^1))
                  
                  Proof:
                    The weightgap principle applies, where following rules are oriented strictly:
                    
                    TRS Component: {isPal(V) -> isNePal(activate(V))}
                    
                    Interpretation of nonconstant growth:
                    -------------------------------------
                      The following argument positions are usable:
                        Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                        Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                        Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                        Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                        Uargs(n__isPal) = {}, Uargs(isPal) = {}
                      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                      Interpretation Functions:
                       __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                    [1 0]      [0 0]      [0]
                       nil() = [0]
                               [0]
                       and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                     [0 0]      [0 0]      [1]
                       tt() = [0]
                              [0]
                       activate(x1) = [1 0] x1 + [0]
                                      [0 0]      [0]
                       isList(x1) = [1 1] x1 + [1]
                                    [0 0]      [1]
                       isNeList(x1) = [1 1] x1 + [1]
                                      [0 0]      [1]
                       n__nil() = [0]
                                  [0]
                       n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                       [1 0]      [0 0]      [0]
                       n__isList(x1) = [1 1] x1 + [0]
                                       [0 0]      [0]
                       isQid(x1) = [1 0] x1 + [1]
                                   [0 0]      [1]
                       n__isNeList(x1) = [1 1] x1 + [0]
                                         [0 0]      [0]
                       isNePal(x1) = [1 0] x1 + [1]
                                     [0 0]      [1]
                       n__isPal(x1) = [1 0] x1 + [0]
                                      [0 0]      [0]
                       isPal(x1) = [1 0] x1 + [3]
                                   [0 0]      [1]
                       n__a() = [0]
                                [0]
                       n__e() = [0]
                                [0]
                       n__i() = [0]
                                [0]
                       n__o() = [0]
                                [0]
                       n__u() = [0]
                                [0]
                       a() = [0]
                             [0]
                       e() = [0]
                             [0]
                       i() = [0]
                             [0]
                       o() = [0]
                             [0]
                       u() = [0]
                             [0]
                    
                    The strictly oriented rules are moved into the weak component.
                    
                    We consider the following Problem:
                    
                      Strict Trs:
                        {  isList(V) -> isNeList(activate(V))
                         , isList(n____(V1, V2)) ->
                           and(isList(activate(V1)), n__isList(activate(V2)))
                         , 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))
                         , activate(n__nil()) -> nil()
                         , activate(n____(X1, X2)) -> __(X1, X2)
                         , activate(n__isList(X)) -> isList(X)
                         , activate(n__isNeList(X)) -> isNeList(X)
                         , activate(n__isPal(X)) -> isPal(X)
                         , activate(n__a()) -> a()
                         , activate(n__e()) -> e()
                         , activate(n__i()) -> i()
                         , activate(n__o()) -> o()
                         , activate(n__u()) -> u()
                         , activate(X) -> X}
                      Weak Trs:
                        {  isPal(V) -> isNePal(activate(V))
                         , u() -> n__u()
                         , o() -> n__o()
                         , i() -> n__i()
                         , e() -> n__e()
                         , a() -> n__a()
                         , __(X1, X2) -> n____(X1, X2)
                         , nil() -> n__nil()
                         , and(tt(), X) -> activate(X)
                         , isList(n__nil()) -> tt()
                         , isPal(n__nil()) -> tt()
                         , isQid(n__a()) -> tt()
                         , isQid(n__e()) -> tt()
                         , isQid(n__i()) -> tt()
                         , isQid(n__o()) -> tt()
                         , isQid(n__u()) -> tt()
                         , isList(X) -> n__isList(X)
                         , isNeList(X) -> n__isNeList(X)
                         , isPal(X) -> n__isPal(X)}
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(?,O(n^1))
                    
                    Proof:
                      The weightgap principle applies, where following rules are oriented strictly:
                      
                      TRS Component: {isNePal(V) -> isQid(activate(V))}
                      
                      Interpretation of nonconstant growth:
                      -------------------------------------
                        The following argument positions are usable:
                          Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                          Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                          Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                          Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                          Uargs(n__isPal) = {}, Uargs(isPal) = {}
                        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                        Interpretation Functions:
                         __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                      [1 0]      [0 0]      [0]
                         nil() = [0]
                                 [0]
                         and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                       [0 0]      [0 0]      [1]
                         tt() = [0]
                                [0]
                         activate(x1) = [1 0] x1 + [0]
                                        [0 0]      [0]
                         isList(x1) = [1 1] x1 + [1]
                                      [0 0]      [1]
                         isNeList(x1) = [1 1] x1 + [1]
                                        [0 0]      [1]
                         n__nil() = [0]
                                    [0]
                         n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                         [1 0]      [0 0]      [0]
                         n__isList(x1) = [1 1] x1 + [0]
                                         [0 0]      [0]
                         isQid(x1) = [1 0] x1 + [1]
                                     [0 0]      [1]
                         n__isNeList(x1) = [1 1] x1 + [0]
                                           [0 0]      [0]
                         isNePal(x1) = [1 0] x1 + [3]
                                       [0 0]      [1]
                         n__isPal(x1) = [1 0] x1 + [0]
                                        [0 0]      [0]
                         isPal(x1) = [1 0] x1 + [3]
                                     [0 0]      [1]
                         n__a() = [0]
                                  [0]
                         n__e() = [0]
                                  [0]
                         n__i() = [0]
                                  [0]
                         n__o() = [0]
                                  [0]
                         n__u() = [0]
                                  [0]
                         a() = [0]
                               [0]
                         e() = [0]
                               [0]
                         i() = [0]
                               [0]
                         o() = [0]
                               [0]
                         u() = [0]
                               [0]
                      
                      The strictly oriented rules are moved into the weak component.
                      
                      We consider the following Problem:
                      
                        Strict Trs:
                          {  isList(V) -> isNeList(activate(V))
                           , isList(n____(V1, V2)) ->
                             and(isList(activate(V1)), n__isList(activate(V2)))
                           , 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)))
                           , activate(n__nil()) -> nil()
                           , activate(n____(X1, X2)) -> __(X1, X2)
                           , activate(n__isList(X)) -> isList(X)
                           , activate(n__isNeList(X)) -> isNeList(X)
                           , activate(n__isPal(X)) -> isPal(X)
                           , activate(n__a()) -> a()
                           , activate(n__e()) -> e()
                           , activate(n__i()) -> i()
                           , activate(n__o()) -> o()
                           , activate(n__u()) -> u()
                           , activate(X) -> X}
                        Weak Trs:
                          {  isNePal(V) -> isQid(activate(V))
                           , isPal(V) -> isNePal(activate(V))
                           , u() -> n__u()
                           , o() -> n__o()
                           , i() -> n__i()
                           , e() -> n__e()
                           , a() -> n__a()
                           , __(X1, X2) -> n____(X1, X2)
                           , nil() -> n__nil()
                           , and(tt(), X) -> activate(X)
                           , isList(n__nil()) -> tt()
                           , isPal(n__nil()) -> tt()
                           , isQid(n__a()) -> tt()
                           , isQid(n__e()) -> tt()
                           , isQid(n__i()) -> tt()
                           , isQid(n__o()) -> tt()
                           , isQid(n__u()) -> tt()
                           , isList(X) -> n__isList(X)
                           , isNeList(X) -> n__isNeList(X)
                           , isPal(X) -> n__isPal(X)}
                        StartTerms: basic terms
                        Strategy: innermost
                      
                      Certificate: YES(?,O(n^1))
                      
                      Proof:
                        The weightgap principle applies, where following rules are oriented strictly:
                        
                        TRS Component: {isNeList(V) -> isQid(activate(V))}
                        
                        Interpretation of nonconstant growth:
                        -------------------------------------
                          The following argument positions are usable:
                            Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                            Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                            Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                            Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                            Uargs(n__isPal) = {}, Uargs(isPal) = {}
                          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                          Interpretation Functions:
                           __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                        [1 0]      [0 0]      [0]
                           nil() = [0]
                                   [0]
                           and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                         [0 0]      [0 0]      [1]
                           tt() = [0]
                                  [0]
                           activate(x1) = [1 0] x1 + [0]
                                          [0 0]      [0]
                           isList(x1) = [1 1] x1 + [1]
                                        [0 0]      [1]
                           isNeList(x1) = [1 1] x1 + [1]
                                          [0 0]      [1]
                           n__nil() = [0]
                                      [0]
                           n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                           [1 0]      [0 0]      [0]
                           n__isList(x1) = [1 1] x1 + [0]
                                           [0 0]      [0]
                           isQid(x1) = [1 0] x1 + [0]
                                       [0 0]      [0]
                           n__isNeList(x1) = [1 1] x1 + [0]
                                             [0 0]      [0]
                           isNePal(x1) = [1 0] x1 + [1]
                                         [0 0]      [0]
                           n__isPal(x1) = [1 0] x1 + [0]
                                          [0 0]      [0]
                           isPal(x1) = [1 0] x1 + [1]
                                       [0 0]      [0]
                           n__a() = [1]
                                    [0]
                           n__e() = [1]
                                    [0]
                           n__i() = [0]
                                    [0]
                           n__o() = [1]
                                    [0]
                           n__u() = [0]
                                    [0]
                           a() = [1]
                                 [0]
                           e() = [1]
                                 [0]
                           i() = [0]
                                 [0]
                           o() = [1]
                                 [0]
                           u() = [0]
                                 [0]
                        
                        The strictly oriented rules are moved into the weak component.
                        
                        We consider the following Problem:
                        
                          Strict Trs:
                            {  isList(V) -> isNeList(activate(V))
                             , isList(n____(V1, V2)) ->
                               and(isList(activate(V1)), n__isList(activate(V2)))
                             , isNeList(n____(V1, V2)) ->
                               and(isList(activate(V1)), n__isNeList(activate(V2)))
                             , isNeList(n____(V1, V2)) ->
                               and(isNeList(activate(V1)), n__isList(activate(V2)))
                             , activate(n__nil()) -> nil()
                             , activate(n____(X1, X2)) -> __(X1, X2)
                             , activate(n__isList(X)) -> isList(X)
                             , activate(n__isNeList(X)) -> isNeList(X)
                             , activate(n__isPal(X)) -> isPal(X)
                             , activate(n__a()) -> a()
                             , activate(n__e()) -> e()
                             , activate(n__i()) -> i()
                             , activate(n__o()) -> o()
                             , activate(n__u()) -> u()
                             , activate(X) -> X}
                          Weak Trs:
                            {  isNeList(V) -> isQid(activate(V))
                             , isNePal(V) -> isQid(activate(V))
                             , isPal(V) -> isNePal(activate(V))
                             , u() -> n__u()
                             , o() -> n__o()
                             , i() -> n__i()
                             , e() -> n__e()
                             , a() -> n__a()
                             , __(X1, X2) -> n____(X1, X2)
                             , nil() -> n__nil()
                             , and(tt(), X) -> activate(X)
                             , isList(n__nil()) -> tt()
                             , isPal(n__nil()) -> tt()
                             , isQid(n__a()) -> tt()
                             , isQid(n__e()) -> tt()
                             , isQid(n__i()) -> tt()
                             , isQid(n__o()) -> tt()
                             , isQid(n__u()) -> tt()
                             , isList(X) -> n__isList(X)
                             , isNeList(X) -> n__isNeList(X)
                             , isPal(X) -> n__isPal(X)}
                          StartTerms: basic terms
                          Strategy: innermost
                        
                        Certificate: YES(?,O(n^1))
                        
                        Proof:
                          The weightgap principle applies, where following rules are oriented strictly:
                          
                          TRS Component: {isList(V) -> isNeList(activate(V))}
                          
                          Interpretation of nonconstant growth:
                          -------------------------------------
                            The following argument positions are usable:
                              Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                              Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                              Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                              Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                              Uargs(n__isPal) = {}, Uargs(isPal) = {}
                            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                            Interpretation Functions:
                             __(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                          [1 0]      [0 0]      [0]
                             nil() = [0]
                                     [0]
                             and(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
                                           [0 0]      [0 0]      [1]
                             tt() = [0]
                                    [0]
                             activate(x1) = [1 0] x1 + [0]
                                            [0 0]      [1]
                             isList(x1) = [1 1] x1 + [3]
                                          [0 0]      [3]
                             isNeList(x1) = [1 1] x1 + [0]
                                            [0 0]      [3]
                             n__nil() = [0]
                                        [0]
                             n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                                             [1 0]      [0 0]      [0]
                             n__isList(x1) = [1 1] x1 + [0]
                                             [0 0]      [0]
                             isQid(x1) = [1 0] x1 + [0]
                                         [0 0]      [1]
                             n__isNeList(x1) = [1 1] x1 + [0]
                                               [0 0]      [0]
                             isNePal(x1) = [1 0] x1 + [0]
                                           [0 0]      [1]
                             n__isPal(x1) = [1 0] x1 + [0]
                                            [0 0]      [0]
                             isPal(x1) = [1 0] x1 + [0]
                                         [0 0]      [1]
                             n__a() = [0]
                                      [0]
                             n__e() = [0]
                                      [0]
                             n__i() = [1]
                                      [0]
                             n__o() = [0]
                                      [0]
                             n__u() = [1]
                                      [0]
                             a() = [0]
                                   [0]
                             e() = [0]
                                   [0]
                             i() = [1]
                                   [0]
                             o() = [0]
                                   [0]
                             u() = [1]
                                   [0]
                          
                          The strictly oriented rules are moved into the weak component.
                          
                          We consider the following Problem:
                          
                            Strict Trs:
                              {  isList(n____(V1, V2)) ->
                                 and(isList(activate(V1)), n__isList(activate(V2)))
                               , isNeList(n____(V1, V2)) ->
                                 and(isList(activate(V1)), n__isNeList(activate(V2)))
                               , isNeList(n____(V1, V2)) ->
                                 and(isNeList(activate(V1)), n__isList(activate(V2)))
                               , activate(n__nil()) -> nil()
                               , activate(n____(X1, X2)) -> __(X1, X2)
                               , activate(n__isList(X)) -> isList(X)
                               , activate(n__isNeList(X)) -> isNeList(X)
                               , activate(n__isPal(X)) -> isPal(X)
                               , activate(n__a()) -> a()
                               , activate(n__e()) -> e()
                               , activate(n__i()) -> i()
                               , activate(n__o()) -> o()
                               , activate(n__u()) -> u()
                               , activate(X) -> X}
                            Weak Trs:
                              {  isList(V) -> isNeList(activate(V))
                               , isNeList(V) -> isQid(activate(V))
                               , isNePal(V) -> isQid(activate(V))
                               , isPal(V) -> isNePal(activate(V))
                               , u() -> n__u()
                               , o() -> n__o()
                               , i() -> n__i()
                               , e() -> n__e()
                               , a() -> n__a()
                               , __(X1, X2) -> n____(X1, X2)
                               , nil() -> n__nil()
                               , and(tt(), X) -> activate(X)
                               , isList(n__nil()) -> tt()
                               , isPal(n__nil()) -> tt()
                               , isQid(n__a()) -> tt()
                               , isQid(n__e()) -> tt()
                               , isQid(n__i()) -> tt()
                               , isQid(n__o()) -> tt()
                               , isQid(n__u()) -> tt()
                               , isList(X) -> n__isList(X)
                               , isNeList(X) -> n__isNeList(X)
                               , isPal(X) -> n__isPal(X)}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(?,O(n^1))
                          
                          Proof:
                            The weightgap principle applies, where following rules are oriented strictly:
                            
                            TRS Component:
                              {  isList(n____(V1, V2)) ->
                                 and(isList(activate(V1)), n__isList(activate(V2)))
                               , isNeList(n____(V1, V2)) ->
                                 and(isList(activate(V1)), n__isNeList(activate(V2)))
                               , isNeList(n____(V1, V2)) ->
                                 and(isNeList(activate(V1)), n__isList(activate(V2)))}
                            
                            Interpretation of nonconstant growth:
                            -------------------------------------
                              The following argument positions are usable:
                                Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                                Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                                Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                                Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                                Uargs(n__isPal) = {}, Uargs(isPal) = {}
                              We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                              Interpretation Functions:
                               __(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                            [1 0]      [0 0]      [2]
                               nil() = [0]
                                       [0]
                               and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                             [0 0]      [0 0]      [0]
                               tt() = [0]
                                      [0]
                               activate(x1) = [1 0] x1 + [0]
                                              [0 0]      [0]
                               isList(x1) = [1 1] x1 + [0]
                                            [0 0]      [0]
                               isNeList(x1) = [1 1] x1 + [0]
                                              [0 0]      [0]
                               n__nil() = [0]
                                          [0]
                               n____(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
                                               [1 0]      [0 0]      [1]
                               n__isList(x1) = [1 1] x1 + [0]
                                               [0 0]      [0]
                               isQid(x1) = [1 0] x1 + [0]
                                           [0 0]      [0]
                               n__isNeList(x1) = [1 1] x1 + [0]
                                                 [0 0]      [0]
                               isNePal(x1) = [1 0] x1 + [1]
                                             [0 0]      [1]
                               n__isPal(x1) = [1 0] x1 + [1]
                                              [0 0]      [0]
                               isPal(x1) = [1 0] x1 + [1]
                                           [0 0]      [1]
                               n__a() = [1]
                                        [0]
                               n__e() = [1]
                                        [0]
                               n__i() = [0]
                                        [0]
                               n__o() = [0]
                                        [0]
                               n__u() = [0]
                                        [0]
                               a() = [1]
                                     [0]
                               e() = [1]
                                     [0]
                               i() = [0]
                                     [0]
                               o() = [0]
                                     [0]
                               u() = [0]
                                     [0]
                            
                            The strictly oriented rules are moved into the weak component.
                            
                            We consider the following Problem:
                            
                              Strict Trs:
                                {  activate(n__nil()) -> nil()
                                 , activate(n____(X1, X2)) -> __(X1, X2)
                                 , activate(n__isList(X)) -> isList(X)
                                 , activate(n__isNeList(X)) -> isNeList(X)
                                 , activate(n__isPal(X)) -> isPal(X)
                                 , activate(n__a()) -> a()
                                 , activate(n__e()) -> e()
                                 , activate(n__i()) -> i()
                                 , activate(n__o()) -> o()
                                 , activate(n__u()) -> u()
                                 , activate(X) -> X}
                              Weak Trs:
                                {  isList(n____(V1, V2)) ->
                                   and(isList(activate(V1)), n__isList(activate(V2)))
                                 , isNeList(n____(V1, V2)) ->
                                   and(isList(activate(V1)), n__isNeList(activate(V2)))
                                 , isNeList(n____(V1, V2)) ->
                                   and(isNeList(activate(V1)), n__isList(activate(V2)))
                                 , isList(V) -> isNeList(activate(V))
                                 , isNeList(V) -> isQid(activate(V))
                                 , isNePal(V) -> isQid(activate(V))
                                 , isPal(V) -> isNePal(activate(V))
                                 , u() -> n__u()
                                 , o() -> n__o()
                                 , i() -> n__i()
                                 , e() -> n__e()
                                 , a() -> n__a()
                                 , __(X1, X2) -> n____(X1, X2)
                                 , nil() -> n__nil()
                                 , and(tt(), X) -> activate(X)
                                 , isList(n__nil()) -> tt()
                                 , isPal(n__nil()) -> tt()
                                 , isQid(n__a()) -> tt()
                                 , isQid(n__e()) -> tt()
                                 , isQid(n__i()) -> tt()
                                 , isQid(n__o()) -> tt()
                                 , isQid(n__u()) -> tt()
                                 , isList(X) -> n__isList(X)
                                 , isNeList(X) -> n__isNeList(X)
                                 , isPal(X) -> n__isPal(X)}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(?,O(n^1))
                            
                            Proof:
                              The weightgap principle applies, where following rules are oriented strictly:
                              
                              TRS Component:
                                {  activate(n__nil()) -> nil()
                                 , activate(n____(X1, X2)) -> __(X1, X2)
                                 , activate(n__a()) -> a()
                                 , activate(n__e()) -> e()
                                 , activate(n__i()) -> i()
                                 , activate(n__o()) -> o()
                                 , activate(n__u()) -> u()
                                 , activate(X) -> X}
                              
                              Interpretation of nonconstant growth:
                              -------------------------------------
                                The following argument positions are usable:
                                  Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                                  Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                                  Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                                  Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                                  Uargs(n__isPal) = {}, Uargs(isPal) = {}
                                We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                                Interpretation Functions:
                                 __(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
                                              [0 1]      [0 1]      [0]
                                 nil() = [0]
                                         [0]
                                 and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                               [0 0]      [0 1]      [1]
                                 tt() = [1]
                                        [0]
                                 activate(x1) = [1 0] x1 + [1]
                                                [0 1]      [1]
                                 isList(x1) = [1 0] x1 + [2]
                                              [0 0]      [1]
                                 isNeList(x1) = [1 0] x1 + [1]
                                                [0 0]      [1]
                                 n__nil() = [0]
                                            [0]
                                 n____(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
                                                 [0 1]      [0 1]      [0]
                                 n__isList(x1) = [1 0] x1 + [0]
                                                 [0 0]      [0]
                                 isQid(x1) = [1 0] x1 + [0]
                                             [0 0]      [1]
                                 n__isNeList(x1) = [1 0] x1 + [0]
                                                   [0 0]      [0]
                                 isNePal(x1) = [1 0] x1 + [1]
                                               [0 0]      [1]
                                 n__isPal(x1) = [1 0] x1 + [0]
                                                [0 0]      [0]
                                 isPal(x1) = [1 0] x1 + [2]
                                             [0 0]      [1]
                                 n__a() = [2]
                                          [0]
                                 n__e() = [2]
                                          [0]
                                 n__i() = [2]
                                          [0]
                                 n__o() = [2]
                                          [0]
                                 n__u() = [2]
                                          [0]
                                 a() = [2]
                                       [0]
                                 e() = [2]
                                       [0]
                                 i() = [2]
                                       [0]
                                 o() = [2]
                                       [0]
                                 u() = [2]
                                       [0]
                              
                              The strictly oriented rules are moved into the weak component.
                              
                              We consider the following Problem:
                              
                                Strict Trs:
                                  {  activate(n__isList(X)) -> isList(X)
                                   , activate(n__isNeList(X)) -> isNeList(X)
                                   , activate(n__isPal(X)) -> isPal(X)}
                                Weak Trs:
                                  {  activate(n__nil()) -> nil()
                                   , activate(n____(X1, X2)) -> __(X1, X2)
                                   , activate(n__a()) -> a()
                                   , activate(n__e()) -> e()
                                   , activate(n__i()) -> i()
                                   , activate(n__o()) -> o()
                                   , activate(n__u()) -> u()
                                   , activate(X) -> X
                                   , isList(n____(V1, V2)) ->
                                     and(isList(activate(V1)), n__isList(activate(V2)))
                                   , isNeList(n____(V1, V2)) ->
                                     and(isList(activate(V1)), n__isNeList(activate(V2)))
                                   , isNeList(n____(V1, V2)) ->
                                     and(isNeList(activate(V1)), n__isList(activate(V2)))
                                   , isList(V) -> isNeList(activate(V))
                                   , isNeList(V) -> isQid(activate(V))
                                   , isNePal(V) -> isQid(activate(V))
                                   , isPal(V) -> isNePal(activate(V))
                                   , u() -> n__u()
                                   , o() -> n__o()
                                   , i() -> n__i()
                                   , e() -> n__e()
                                   , a() -> n__a()
                                   , __(X1, X2) -> n____(X1, X2)
                                   , nil() -> n__nil()
                                   , and(tt(), X) -> activate(X)
                                   , isList(n__nil()) -> tt()
                                   , isPal(n__nil()) -> tt()
                                   , isQid(n__a()) -> tt()
                                   , isQid(n__e()) -> tt()
                                   , isQid(n__i()) -> tt()
                                   , isQid(n__o()) -> tt()
                                   , isQid(n__u()) -> tt()
                                   , isList(X) -> n__isList(X)
                                   , isNeList(X) -> n__isNeList(X)
                                   , isPal(X) -> n__isPal(X)}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(?,O(n^1))
                              
                              Proof:
                                The weightgap principle applies, where following rules are oriented strictly:
                                
                                TRS Component: {activate(n__isPal(X)) -> isPal(X)}
                                
                                Interpretation of nonconstant growth:
                                -------------------------------------
                                  The following argument positions are usable:
                                    Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                                    Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                                    Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                                    Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                                    Uargs(n__isPal) = {}, Uargs(isPal) = {}
                                  We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                                  Interpretation Functions:
                                   __(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
                                                [0 0]      [0 0]      [0]
                                   nil() = [3]
                                           [0]
                                   and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                                 [0 0]      [0 1]      [0]
                                   tt() = [2]
                                          [0]
                                   activate(x1) = [1 0] x1 + [1]
                                                  [0 1]      [0]
                                   isList(x1) = [1 0] x1 + [2]
                                                [0 0]      [2]
                                   isNeList(x1) = [1 0] x1 + [1]
                                                  [0 0]      [1]
                                   n__nil() = [3]
                                              [0]
                                   n____(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
                                                   [0 0]      [0 0]      [0]
                                   n__isList(x1) = [1 0] x1 + [0]
                                                   [0 0]      [1]
                                   isQid(x1) = [1 0] x1 + [0]
                                               [0 0]      [0]
                                   n__isNeList(x1) = [1 0] x1 + [0]
                                                     [0 0]      [0]
                                   isNePal(x1) = [1 0] x1 + [1]
                                                 [0 0]      [1]
                                   n__isPal(x1) = [1 0] x1 + [3]
                                                  [0 0]      [1]
                                   isPal(x1) = [1 0] x1 + [3]
                                               [0 0]      [1]
                                   n__a() = [2]
                                            [0]
                                   n__e() = [2]
                                            [0]
                                   n__i() = [2]
                                            [0]
                                   n__o() = [2]
                                            [0]
                                   n__u() = [2]
                                            [0]
                                   a() = [2]
                                         [0]
                                   e() = [2]
                                         [0]
                                   i() = [2]
                                         [0]
                                   o() = [2]
                                         [0]
                                   u() = [2]
                                         [0]
                                
                                The strictly oriented rules are moved into the weak component.
                                
                                We consider the following Problem:
                                
                                  Strict Trs:
                                    {  activate(n__isList(X)) -> isList(X)
                                     , activate(n__isNeList(X)) -> isNeList(X)}
                                  Weak Trs:
                                    {  activate(n__isPal(X)) -> isPal(X)
                                     , activate(n__nil()) -> nil()
                                     , activate(n____(X1, X2)) -> __(X1, X2)
                                     , activate(n__a()) -> a()
                                     , activate(n__e()) -> e()
                                     , activate(n__i()) -> i()
                                     , activate(n__o()) -> o()
                                     , activate(n__u()) -> u()
                                     , activate(X) -> X
                                     , isList(n____(V1, V2)) ->
                                       and(isList(activate(V1)), n__isList(activate(V2)))
                                     , isNeList(n____(V1, V2)) ->
                                       and(isList(activate(V1)), n__isNeList(activate(V2)))
                                     , isNeList(n____(V1, V2)) ->
                                       and(isNeList(activate(V1)), n__isList(activate(V2)))
                                     , isList(V) -> isNeList(activate(V))
                                     , isNeList(V) -> isQid(activate(V))
                                     , isNePal(V) -> isQid(activate(V))
                                     , isPal(V) -> isNePal(activate(V))
                                     , u() -> n__u()
                                     , o() -> n__o()
                                     , i() -> n__i()
                                     , e() -> n__e()
                                     , a() -> n__a()
                                     , __(X1, X2) -> n____(X1, X2)
                                     , nil() -> n__nil()
                                     , and(tt(), X) -> activate(X)
                                     , isList(n__nil()) -> tt()
                                     , isPal(n__nil()) -> tt()
                                     , isQid(n__a()) -> tt()
                                     , isQid(n__e()) -> tt()
                                     , isQid(n__i()) -> tt()
                                     , isQid(n__o()) -> tt()
                                     , isQid(n__u()) -> tt()
                                     , isList(X) -> n__isList(X)
                                     , isNeList(X) -> n__isNeList(X)
                                     , isPal(X) -> n__isPal(X)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(?,O(n^1))
                                
                                Proof:
                                  The weightgap principle applies, where following rules are oriented strictly:
                                  
                                  TRS Component: {activate(n__isNeList(X)) -> isNeList(X)}
                                  
                                  Interpretation of nonconstant growth:
                                  -------------------------------------
                                    The following argument positions are usable:
                                      Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                                      Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
                                      Uargs(n__isList) = {1}, Uargs(isQid) = {1},
                                      Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
                                      Uargs(n__isPal) = {}, Uargs(isPal) = {}
                                    We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                                    Interpretation Functions:
                                     __(x1, x2) = [1 2] x1 + [1 2] x2 + [2]
                                                  [0 0]      [0 0]      [2]
                                     nil() = [0]
                                             [0]
                                     and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                                   [0 1]      [0 1]      [0]
                                     tt() = [1]
                                            [0]
                                     activate(x1) = [1 0] x1 + [1]
                                                    [0 1]      [0]
                                     isList(x1) = [1 2] x1 + [2]
                                                  [0 0]      [0]
                                     isNeList(x1) = [1 1] x1 + [1]
                                                    [0 0]      [0]
                                     n__nil() = [0]
                                                [0]
                                     n____(x1, x2) = [1 2] x1 + [1 2] x2 + [2]
                                                     [0 0]      [0 0]      [2]
                                     n__isList(x1) = [1 2] x1 + [0]
                                                     [0 0]      [0]
                                     isQid(x1) = [1 0] x1 + [0]
                                                 [0 0]      [0]
                                     n__isNeList(x1) = [1 1] x1 + [1]
                                                       [0 0]      [0]
                                     isNePal(x1) = [1 1] x1 + [1]
                                                   [0 0]      [1]
                                     n__isPal(x1) = [1 1] x1 + [2]
                                                    [0 0]      [1]
                                     isPal(x1) = [1 1] x1 + [2]
                                                 [0 0]      [1]
                                     n__a() = [2]
                                              [0]
                                     n__e() = [1]
                                              [0]
                                     n__i() = [2]
                                              [0]
                                     n__o() = [2]
                                              [0]
                                     n__u() = [1]
                                              [0]
                                     a() = [2]
                                           [0]
                                     e() = [1]
                                           [0]
                                     i() = [2]
                                           [0]
                                     o() = [2]
                                           [0]
                                     u() = [2]
                                           [0]
                                  
                                  The strictly oriented rules are moved into the weak component.
                                  
                                  We consider the following Problem:
                                  
                                    Strict Trs: {activate(n__isList(X)) -> isList(X)}
                                    Weak Trs:
                                      {  activate(n__isNeList(X)) -> isNeList(X)
                                       , activate(n__isPal(X)) -> isPal(X)
                                       , activate(n__nil()) -> nil()
                                       , activate(n____(X1, X2)) -> __(X1, X2)
                                       , activate(n__a()) -> a()
                                       , activate(n__e()) -> e()
                                       , activate(n__i()) -> i()
                                       , activate(n__o()) -> o()
                                       , activate(n__u()) -> u()
                                       , activate(X) -> X
                                       , isList(n____(V1, V2)) ->
                                         and(isList(activate(V1)), n__isList(activate(V2)))
                                       , isNeList(n____(V1, V2)) ->
                                         and(isList(activate(V1)), n__isNeList(activate(V2)))
                                       , isNeList(n____(V1, V2)) ->
                                         and(isNeList(activate(V1)), n__isList(activate(V2)))
                                       , isList(V) -> isNeList(activate(V))
                                       , isNeList(V) -> isQid(activate(V))
                                       , isNePal(V) -> isQid(activate(V))
                                       , isPal(V) -> isNePal(activate(V))
                                       , u() -> n__u()
                                       , o() -> n__o()
                                       , i() -> n__i()
                                       , e() -> n__e()
                                       , a() -> n__a()
                                       , __(X1, X2) -> n____(X1, X2)
                                       , nil() -> n__nil()
                                       , and(tt(), X) -> activate(X)
                                       , isList(n__nil()) -> tt()
                                       , isPal(n__nil()) -> tt()
                                       , isQid(n__a()) -> tt()
                                       , isQid(n__e()) -> tt()
                                       , isQid(n__i()) -> tt()
                                       , isQid(n__o()) -> tt()
                                       , isQid(n__u()) -> tt()
                                       , isList(X) -> n__isList(X)
                                       , isNeList(X) -> n__isNeList(X)
                                       , isPal(X) -> n__isPal(X)}
                                    StartTerms: basic terms
                                    Strategy: innermost
                                  
                                  Certificate: YES(?,O(n^1))
                                  
                                  Proof:
                                    The weightgap principle applies, where following rules are oriented strictly:
                                    
                                    TRS Component: {activate(n__isList(X)) -> isList(X)}
                                    
                                    Interpretation of nonconstant growth:
                                    -------------------------------------
                                      The following argument positions are usable:
                                        Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
                                        Uargs(isList) = {1}, Uargs(isNeList) = {1},
                                        Uargs(n____) = {}, Uargs(n__isList) = {1},
                                        Uargs(isQid) = {1}, Uargs(n__isNeList) = {1},
                                        Uargs(isNePal) = {1}, Uargs(n__isPal) = {},
                                        Uargs(isPal) = {}
                                      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                                      Interpretation Functions:
                                       __(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
                                                    [0 1]      [0 1]      [3]
                                       nil() = [0]
                                               [0]
                                       and(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
                                                     [0 0]      [0 1]      [0]
                                       tt() = [0]
                                              [1]
                                       activate(x1) = [1 0] x1 + [1]
                                                      [0 1]      [0]
                                       isList(x1) = [1 1] x1 + [2]
                                                    [0 0]      [1]
                                       isNeList(x1) = [1 1] x1 + [1]
                                                      [0 0]      [1]
                                       n__nil() = [0]
                                                  [0]
                                       n____(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
                                                       [0 1]      [0 1]      [3]
                                       n__isList(x1) = [1 1] x1 + [2]
                                                       [0 0]      [1]
                                       isQid(x1) = [1 0] x1 + [0]
                                                   [0 0]      [1]
                                       n__isNeList(x1) = [1 1] x1 + [0]
                                                         [0 0]      [1]
                                       isNePal(x1) = [1 0] x1 + [2]
                                                     [0 0]      [1]
                                       n__isPal(x1) = [1 0] x1 + [3]
                                                      [0 1]      [2]
                                       isPal(x1) = [1 0] x1 + [3]
                                                   [0 1]      [2]
                                       n__a() = [0]
                                                [0]
                                       n__e() = [0]
                                                [0]
                                       n__i() = [0]
                                                [1]
                                       n__o() = [0]
                                                [1]
                                       n__u() = [0]
                                                [0]
                                       a() = [0]
                                             [0]
                                       e() = [0]
                                             [0]
                                       i() = [0]
                                             [1]
                                       o() = [0]
                                             [1]
                                       u() = [0]
                                             [0]
                                    
                                    The strictly oriented rules are moved into the weak component.
                                    
                                    We consider the following Problem:
                                    
                                      Weak Trs:
                                        {  activate(n__isList(X)) -> isList(X)
                                         , activate(n__isNeList(X)) -> isNeList(X)
                                         , activate(n__isPal(X)) -> isPal(X)
                                         , activate(n__nil()) -> nil()
                                         , activate(n____(X1, X2)) -> __(X1, X2)
                                         , activate(n__a()) -> a()
                                         , activate(n__e()) -> e()
                                         , activate(n__i()) -> i()
                                         , activate(n__o()) -> o()
                                         , activate(n__u()) -> u()
                                         , activate(X) -> X
                                         , isList(n____(V1, V2)) ->
                                           and(isList(activate(V1)), n__isList(activate(V2)))
                                         , isNeList(n____(V1, V2)) ->
                                           and(isList(activate(V1)), n__isNeList(activate(V2)))
                                         , isNeList(n____(V1, V2)) ->
                                           and(isNeList(activate(V1)), n__isList(activate(V2)))
                                         , isList(V) -> isNeList(activate(V))
                                         , isNeList(V) -> isQid(activate(V))
                                         , isNePal(V) -> isQid(activate(V))
                                         , isPal(V) -> isNePal(activate(V))
                                         , u() -> n__u()
                                         , o() -> n__o()
                                         , i() -> n__i()
                                         , e() -> n__e()
                                         , a() -> n__a()
                                         , __(X1, X2) -> n____(X1, X2)
                                         , nil() -> n__nil()
                                         , and(tt(), X) -> activate(X)
                                         , isList(n__nil()) -> tt()
                                         , isPal(n__nil()) -> tt()
                                         , isQid(n__a()) -> tt()
                                         , isQid(n__e()) -> tt()
                                         , isQid(n__i()) -> tt()
                                         , isQid(n__o()) -> tt()
                                         , isQid(n__u()) -> tt()
                                         , isList(X) -> n__isList(X)
                                         , isNeList(X) -> n__isNeList(X)
                                         , isPal(X) -> n__isPal(X)}
                                      StartTerms: basic terms
                                      Strategy: innermost
                                    
                                    Certificate: YES(O(1),O(1))
                                    
                                    Proof:
                                      We consider the following Problem:
                                      
                                        Weak Trs:
                                          {  activate(n__isList(X)) -> isList(X)
                                           , activate(n__isNeList(X)) -> isNeList(X)
                                           , activate(n__isPal(X)) -> isPal(X)
                                           , activate(n__nil()) -> nil()
                                           , activate(n____(X1, X2)) -> __(X1, X2)
                                           , activate(n__a()) -> a()
                                           , activate(n__e()) -> e()
                                           , activate(n__i()) -> i()
                                           , activate(n__o()) -> o()
                                           , activate(n__u()) -> u()
                                           , activate(X) -> X
                                           , isList(n____(V1, V2)) ->
                                             and(isList(activate(V1)), n__isList(activate(V2)))
                                           , isNeList(n____(V1, V2)) ->
                                             and(isList(activate(V1)), n__isNeList(activate(V2)))
                                           , isNeList(n____(V1, V2)) ->
                                             and(isNeList(activate(V1)), n__isList(activate(V2)))
                                           , isList(V) -> isNeList(activate(V))
                                           , isNeList(V) -> isQid(activate(V))
                                           , isNePal(V) -> isQid(activate(V))
                                           , isPal(V) -> isNePal(activate(V))
                                           , u() -> n__u()
                                           , o() -> n__o()
                                           , i() -> n__i()
                                           , e() -> n__e()
                                           , a() -> n__a()
                                           , __(X1, X2) -> n____(X1, X2)
                                           , nil() -> n__nil()
                                           , and(tt(), X) -> activate(X)
                                           , isList(n__nil()) -> tt()
                                           , isPal(n__nil()) -> tt()
                                           , isQid(n__a()) -> tt()
                                           , isQid(n__e()) -> tt()
                                           , isQid(n__i()) -> tt()
                                           , isQid(n__o()) -> tt()
                                           , isQid(n__u()) -> tt()
                                           , isList(X) -> n__isList(X)
                                           , isNeList(X) -> n__isNeList(X)
                                           , isPal(X) -> n__isPal(X)}
                                        StartTerms: basic terms
                                        Strategy: innermost
                                      
                                      Certificate: YES(O(1),O(1))
                                      
                                      Proof:
                                        Empty rules are trivially bounded

Hurray, we answered YES(?,O(n^1))