Problem Transformed CSR 04 PALINDROME nokinds Z

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 PALINDROME nokinds Z

stdout:

YES(?,O(n^2))

Problem:
__(__(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

Proof:
Complexity Transformation Processor:
  strict:
   __(__(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
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [u] = 0,

     [o] = 0,

     [i] = 0,

     [e] = 0,

     [a] = 0,

     [n__u] = 6,

     [n__o] = 5,

     [n__i] = 64,

     [n__e] = 53,

     [n__a] = 33,

     [isPal](x0) = x0 + 12,

     [n__isPal](x0) = x0 + 70,

     [isNePal](x0) = x0 + 32,

     [n__isNeList](x0) = x0 + 82,

     [isQid](x0) = x0 + 16,

     [n__isList](x0) = x0,

     [n____](x0, x1) = x0 + x1 + 92,

     [n__nil] = 88,

     [isNeList](x0) = x0 + 114,

     [isList](x0) = x0 + 6,

     [activate](x0) = x0 + 1,

     [and](x0, x1) = x0 + x1 + 17,

     [tt] = 36,

     [nil] = 36,

     [__](x0, x1) = x0 + x1 + 8
    orientation:
     __(__(X,Y),Z) = X + Y + Z + 16 >= X + Y + Z + 16 = __(X,__(Y,Z))

     __(X,nil()) = X + 44 >= X = X

     __(nil(),X) = X + 44 >= X = X

     and(tt(),X) = X + 53 >= X + 1 = activate(X)

     isList(V) = V + 6 >= V + 115 = isNeList(activate(V))

     isList(n__nil()) = 94 >= 36 = tt()

     isList(n____(V1,V2)) = V1 + V2 + 98 >= V1 + V2 + 25 = and(isList(activate(V1)),n__isList(activate(V2)))

     isNeList(V) = V + 114 >= V + 17 = isQid(activate(V))

     isNeList(n____(V1,V2)) = V1 + V2 + 206 >= V1 + V2 + 107 = and(isList(activate(V1)),n__isNeList(activate(V2)))

     isNeList(n____(V1,V2)) = V1 + V2 + 206 >= V1 + V2 + 133 = and(isNeList(activate(V1)),n__isList(activate(V2)))

     isNePal(V) = V + 32 >= V + 17 = isQid(activate(V))

     isNePal(n____(I,__(P,I))) = 2I + P + 132 >= I + P + 105 = and(isQid(activate(I)),n__isPal(activate(P)))

     isPal(V) = V + 12 >= V + 33 = isNePal(activate(V))

     isPal(n__nil()) = 100 >= 36 = tt()

     isQid(n__a()) = 49 >= 36 = tt()

     isQid(n__e()) = 69 >= 36 = tt()

     isQid(n__i()) = 80 >= 36 = tt()

     isQid(n__o()) = 21 >= 36 = tt()

     isQid(n__u()) = 22 >= 36 = tt()

     nil() = 36 >= 88 = n__nil()

     __(X1,X2) = X1 + X2 + 8 >= X1 + X2 + 92 = n____(X1,X2)

     isList(X) = X + 6 >= X = n__isList(X)

     isNeList(X) = X + 114 >= X + 82 = n__isNeList(X)

     isPal(X) = X + 12 >= X + 70 = n__isPal(X)

     a() = 0 >= 33 = n__a()

     e() = 0 >= 53 = n__e()

     i() = 0 >= 64 = n__i()

     o() = 0 >= 5 = n__o()

     u() = 0 >= 6 = n__u()

     activate(n__nil()) = 89 >= 36 = nil()

     activate(n____(X1,X2)) = X1 + X2 + 93 >= X1 + X2 + 8 = __(X1,X2)

     activate(n__isList(X)) = X + 1 >= X + 6 = isList(X)

     activate(n__isNeList(X)) = X + 83 >= X + 114 = isNeList(X)

     activate(n__isPal(X)) = X + 71 >= X + 12 = isPal(X)

     activate(n__a()) = 34 >= 0 = a()

     activate(n__e()) = 54 >= 0 = e()

     activate(n__i()) = 65 >= 0 = i()

     activate(n__o()) = 6 >= 0 = o()

     activate(n__u()) = 7 >= 0 = u()

     activate(X) = X + 1 >= X = X
    problem:
     strict:
      __(__(X,Y),Z) -> __(X,__(Y,Z))
      isList(V) -> isNeList(activate(V))
      isPal(V) -> isNePal(activate(V))
      isQid(n__o()) -> tt()
      isQid(n__u()) -> tt()
      nil() -> n__nil()
      __(X1,X2) -> n____(X1,X2)
      isPal(X) -> n__isPal(X)
      a() -> n__a()
      e() -> n__e()
      i() -> n__i()
      o() -> n__o()
      u() -> n__u()
      activate(n__isList(X)) -> isList(X)
      activate(n__isNeList(X)) -> isNeList(X)
     weak:
      __(X,nil()) -> X
      __(nil(),X) -> X
      and(tt(),X) -> activate(X)
      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(n__nil()) -> tt()
      isQid(n__a()) -> tt()
      isQid(n__e()) -> tt()
      isQid(n__i()) -> tt()
      isList(X) -> n__isList(X)
      isNeList(X) -> n__isNeList(X)
      activate(n__nil()) -> nil()
      activate(n____(X1,X2)) -> __(X1,X2)
      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
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [u] = 14,

       [o] = 0,

       [i] = 10,

       [e] = 0,

       [a] = 0,

       [n__u] = 14,

       [n__o] = 1,

       [n__i] = 10,

       [n__e] = 24,

       [n__a] = 26,

       [isPal](x0) = x0 + 6,

       [n__isPal](x0) = x0 + 24,

       [isNePal](x0) = x0 + 24,

       [n__isNeList](x0) = x0 + 8,

       [isQid](x0) = x0 + 2,

       [n__isList](x0) = x0,

       [n____](x0, x1) = x0 + x1 + 14,

       [n__nil] = 12,

       [isNeList](x0) = x0 + 10,

       [isList](x0) = x0,

       [activate](x0) = x0,

       [and](x0, x1) = x0 + x1 + 12,

       [tt] = 12,

       [nil] = 0,

       [__](x0, x1) = x0 + x1
      orientation:
       __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))

       isList(V) = V >= V + 10 = isNeList(activate(V))

       isPal(V) = V + 6 >= V + 24 = isNePal(activate(V))

       isQid(n__o()) = 3 >= 12 = tt()

       isQid(n__u()) = 16 >= 12 = tt()

       nil() = 0 >= 12 = n__nil()

       __(X1,X2) = X1 + X2 >= X1 + X2 + 14 = n____(X1,X2)

       isPal(X) = X + 6 >= X + 24 = n__isPal(X)

       a() = 0 >= 26 = n__a()

       e() = 0 >= 24 = n__e()

       i() = 10 >= 10 = n__i()

       o() = 0 >= 1 = n__o()

       u() = 14 >= 14 = n__u()

       activate(n__isList(X)) = X >= X = isList(X)

       activate(n__isNeList(X)) = X + 8 >= X + 10 = isNeList(X)

       __(X,nil()) = X >= X = X

       __(nil(),X) = X >= X = X

       and(tt(),X) = X + 24 >= X = activate(X)

       isList(n__nil()) = 12 >= 12 = tt()

       isList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 12 = and(isList(activate(V1)),n__isList(activate(V2)))

       isNeList(V) = V + 10 >= V + 2 = isQid(activate(V))

       isNeList(n____(V1,V2)) = V1 + V2 + 24 >= V1 + V2 + 20 = and(isList(activate(V1)),n__isNeList(activate(V2)))

       isNeList(n____(V1,V2)) = V1 + V2 + 24 >= V1 + V2 + 22 = and(isNeList(activate(V1)),n__isList(activate(V2)))

       isNePal(V) = V + 24 >= V + 2 = isQid(activate(V))

       isNePal(n____(I,__(P,I))) = 2I + P + 38 >= I + P + 38 = and(isQid(activate(I)),n__isPal(activate(P)))

       isPal(n__nil()) = 18 >= 12 = tt()

       isQid(n__a()) = 28 >= 12 = tt()

       isQid(n__e()) = 26 >= 12 = tt()

       isQid(n__i()) = 12 >= 12 = tt()

       isList(X) = X >= X = n__isList(X)

       isNeList(X) = X + 10 >= X + 8 = n__isNeList(X)

       activate(n__nil()) = 12 >= 0 = nil()

       activate(n____(X1,X2)) = X1 + X2 + 14 >= X1 + X2 = __(X1,X2)

       activate(n__isPal(X)) = X + 24 >= X + 6 = isPal(X)

       activate(n__a()) = 26 >= 0 = a()

       activate(n__e()) = 24 >= 0 = e()

       activate(n__i()) = 10 >= 10 = i()

       activate(n__o()) = 1 >= 0 = o()

       activate(n__u()) = 14 >= 14 = u()

       activate(X) = X >= X = X
      problem:
       strict:
        __(__(X,Y),Z) -> __(X,__(Y,Z))
        isList(V) -> isNeList(activate(V))
        isPal(V) -> isNePal(activate(V))
        isQid(n__o()) -> tt()
        nil() -> n__nil()
        __(X1,X2) -> n____(X1,X2)
        isPal(X) -> n__isPal(X)
        a() -> n__a()
        e() -> n__e()
        i() -> n__i()
        o() -> n__o()
        u() -> n__u()
        activate(n__isList(X)) -> isList(X)
        activate(n__isNeList(X)) -> isNeList(X)
       weak:
        isQid(n__u()) -> tt()
        __(X,nil()) -> X
        __(nil(),X) -> X
        and(tt(),X) -> activate(X)
        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(n__nil()) -> tt()
        isQid(n__a()) -> tt()
        isQid(n__e()) -> tt()
        isQid(n__i()) -> tt()
        isList(X) -> n__isList(X)
        isNeList(X) -> n__isNeList(X)
        activate(n__nil()) -> nil()
        activate(n____(X1,X2)) -> __(X1,X2)
        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
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [u] = 0,

         [o] = 0,

         [i] = 0,

         [e] = 1,

         [a] = 4,

         [n__u] = 9,

         [n__o] = 5,

         [n__i] = 1,

         [n__e] = 1,

         [n__a] = 4,

         [isPal](x0) = x0,

         [n__isPal](x0) = x0 + 1,

         [isNePal](x0) = x0 + 14,

         [n__isNeList](x0) = x0,

         [isQid](x0) = x0,

         [n__isList](x0) = x0,

         [n____](x0, x1) = x0 + x1,

         [n__nil] = 8,

         [isNeList](x0) = x0 + 12,

         [isList](x0) = x0,

         [activate](x0) = x0,

         [and](x0, x1) = x0 + x1,

         [tt] = 1,

         [nil] = 2,

         [__](x0, x1) = x0 + x1
        orientation:
         __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))

         isList(V) = V >= V + 12 = isNeList(activate(V))

         isPal(V) = V >= V + 14 = isNePal(activate(V))

         isQid(n__o()) = 5 >= 1 = tt()

         nil() = 2 >= 8 = n__nil()

         __(X1,X2) = X1 + X2 >= X1 + X2 = n____(X1,X2)

         isPal(X) = X >= X + 1 = n__isPal(X)

         a() = 4 >= 4 = n__a()

         e() = 1 >= 1 = n__e()

         i() = 0 >= 1 = n__i()

         o() = 0 >= 5 = n__o()

         u() = 0 >= 9 = n__u()

         activate(n__isList(X)) = X >= X = isList(X)

         activate(n__isNeList(X)) = X >= X + 12 = isNeList(X)

         isQid(n__u()) = 9 >= 1 = tt()

         __(X,nil()) = X + 2 >= X = X

         __(nil(),X) = X + 2 >= X = X

         and(tt(),X) = X + 1 >= X = activate(X)

         isList(n__nil()) = 8 >= 1 = tt()

         isList(n____(V1,V2)) = V1 + V2 >= V1 + V2 = and(isList(activate(V1)),n__isList(activate(V2)))

         isNeList(V) = V + 12 >= V = isQid(activate(V))

         isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 = and(isList(activate(V1)),n__isNeList(activate(V2)))

         isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = and(isNeList(activate(V1)),n__isList(activate(V2)))

         isNePal(V) = V + 14 >= V = isQid(activate(V))

         isNePal(n____(I,__(P,I))) = 2I + P + 14 >= I + P + 1 = and(isQid(activate(I)),n__isPal(activate(P)))

         isPal(n__nil()) = 8 >= 1 = tt()

         isQid(n__a()) = 4 >= 1 = tt()

         isQid(n__e()) = 1 >= 1 = tt()

         isQid(n__i()) = 1 >= 1 = tt()

         isList(X) = X >= X = n__isList(X)

         isNeList(X) = X + 12 >= X = n__isNeList(X)

         activate(n__nil()) = 8 >= 2 = nil()

         activate(n____(X1,X2)) = X1 + X2 >= X1 + X2 = __(X1,X2)

         activate(n__isPal(X)) = X + 1 >= X = isPal(X)

         activate(n__a()) = 4 >= 4 = a()

         activate(n__e()) = 1 >= 1 = e()

         activate(n__i()) = 1 >= 0 = i()

         activate(n__o()) = 5 >= 0 = o()

         activate(n__u()) = 9 >= 0 = u()

         activate(X) = X >= X = X
        problem:
         strict:
          __(__(X,Y),Z) -> __(X,__(Y,Z))
          isList(V) -> isNeList(activate(V))
          isPal(V) -> isNePal(activate(V))
          nil() -> n__nil()
          __(X1,X2) -> n____(X1,X2)
          isPal(X) -> n__isPal(X)
          a() -> n__a()
          e() -> n__e()
          i() -> n__i()
          o() -> n__o()
          u() -> n__u()
          activate(n__isList(X)) -> isList(X)
          activate(n__isNeList(X)) -> isNeList(X)
         weak:
          isQid(n__o()) -> tt()
          isQid(n__u()) -> tt()
          __(X,nil()) -> X
          __(nil(),X) -> X
          and(tt(),X) -> activate(X)
          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(n__nil()) -> tt()
          isQid(n__a()) -> tt()
          isQid(n__e()) -> tt()
          isQid(n__i()) -> tt()
          isList(X) -> n__isList(X)
          isNeList(X) -> n__isNeList(X)
          activate(n__nil()) -> nil()
          activate(n____(X1,X2)) -> __(X1,X2)
          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
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [u] = 0,

           [o] = 0,

           [i] = 0,

           [e] = 8,

           [a] = 1,

           [n__u] = 0,

           [n__o] = 0,

           [n__i] = 12,

           [n__e] = 8,

           [n__a] = 1,

           [isPal](x0) = x0 + 1,

           [n__isPal](x0) = x0 + 2,

           [isNePal](x0) = x0,

           [n__isNeList](x0) = x0,

           [isQid](x0) = x0,

           [n__isList](x0) = x0,

           [n____](x0, x1) = x0 + x1 + 8,

           [n__nil] = 5,

           [isNeList](x0) = x0,

           [isList](x0) = x0,

           [activate](x0) = x0,

           [and](x0, x1) = x0 + x1,

           [tt] = 0,

           [nil] = 0,

           [__](x0, x1) = x0 + x1
          orientation:
           __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))

           isList(V) = V >= V = isNeList(activate(V))

           isPal(V) = V + 1 >= V = isNePal(activate(V))

           nil() = 0 >= 5 = n__nil()

           __(X1,X2) = X1 + X2 >= X1 + X2 + 8 = n____(X1,X2)

           isPal(X) = X + 1 >= X + 2 = n__isPal(X)

           a() = 1 >= 1 = n__a()

           e() = 8 >= 8 = n__e()

           i() = 0 >= 12 = n__i()

           o() = 0 >= 0 = n__o()

           u() = 0 >= 0 = n__u()

           activate(n__isList(X)) = X >= X = isList(X)

           activate(n__isNeList(X)) = X >= X = isNeList(X)

           isQid(n__o()) = 0 >= 0 = tt()

           isQid(n__u()) = 0 >= 0 = tt()

           __(X,nil()) = X >= X = X

           __(nil(),X) = X >= X = X

           and(tt(),X) = X >= X = activate(X)

           isList(n__nil()) = 5 >= 0 = tt()

           isList(n____(V1,V2)) = V1 + V2 + 8 >= V1 + V2 = and(isList(activate(V1)),n__isList(activate(V2)))

           isNeList(V) = V >= V = isQid(activate(V))

           isNeList(n____(V1,V2)) = V1 + V2 + 8 >= V1 + V2 = and(isList(activate(V1)),n__isNeList(activate(V2)))

           isNeList(n____(V1,V2)) = V1 + V2 + 8 >= V1 + V2 = and(isNeList(activate(V1)),n__isList(activate(V2)))

           isNePal(V) = V >= V = isQid(activate(V))

           isNePal(n____(I,__(P,I))) = 2I + P + 8 >= I + P + 2 = and(isQid(activate(I)),n__isPal(activate(P)))

           isPal(n__nil()) = 6 >= 0 = tt()

           isQid(n__a()) = 1 >= 0 = tt()

           isQid(n__e()) = 8 >= 0 = tt()

           isQid(n__i()) = 12 >= 0 = tt()

           isList(X) = X >= X = n__isList(X)

           isNeList(X) = X >= X = n__isNeList(X)

           activate(n__nil()) = 5 >= 0 = nil()

           activate(n____(X1,X2)) = X1 + X2 + 8 >= X1 + X2 = __(X1,X2)

           activate(n__isPal(X)) = X + 2 >= X + 1 = isPal(X)

           activate(n__a()) = 1 >= 1 = a()

           activate(n__e()) = 8 >= 8 = e()

           activate(n__i()) = 12 >= 0 = i()

           activate(n__o()) = 0 >= 0 = o()

           activate(n__u()) = 0 >= 0 = u()

           activate(X) = X >= X = X
          problem:
           strict:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            isList(V) -> isNeList(activate(V))
            nil() -> n__nil()
            __(X1,X2) -> n____(X1,X2)
            isPal(X) -> n__isPal(X)
            a() -> n__a()
            e() -> n__e()
            i() -> n__i()
            o() -> n__o()
            u() -> n__u()
            activate(n__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
           weak:
            isPal(V) -> isNePal(activate(V))
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            __(X,nil()) -> X
            __(nil(),X) -> X
            and(tt(),X) -> activate(X)
            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(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isList(X) -> n__isList(X)
            isNeList(X) -> n__isNeList(X)
            activate(n__nil()) -> nil()
            activate(n____(X1,X2)) -> __(X1,X2)
            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
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [u] = 0,

             [o] = 0,

             [i] = 2,

             [e] = 2,

             [a] = 1,

             [n__u] = 0,

             [n__o] = 0,

             [n__i] = 2,

             [n__e] = 2,

             [n__a] = 1,

             [isPal](x0) = x0,

             [n__isPal](x0) = x0 + 1,

             [isNePal](x0) = x0,

             [n__isNeList](x0) = x0,

             [isQid](x0) = x0,

             [n__isList](x0) = x0,

             [n____](x0, x1) = x0 + x1 + 15,

             [n__nil] = 14,

             [isNeList](x0) = x0,

             [isList](x0) = x0 + 2,

             [activate](x0) = x0,

             [and](x0, x1) = x0 + x1,

             [tt] = 0,

             [nil] = 0,

             [__](x0, x1) = x0 + x1
            orientation:
             __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))

             isList(V) = V + 2 >= V = isNeList(activate(V))

             nil() = 0 >= 14 = n__nil()

             __(X1,X2) = X1 + X2 >= X1 + X2 + 15 = n____(X1,X2)

             isPal(X) = X >= X + 1 = n__isPal(X)

             a() = 1 >= 1 = n__a()

             e() = 2 >= 2 = n__e()

             i() = 2 >= 2 = n__i()

             o() = 0 >= 0 = n__o()

             u() = 0 >= 0 = n__u()

             activate(n__isList(X)) = X >= X + 2 = isList(X)

             activate(n__isNeList(X)) = X >= X = isNeList(X)

             isPal(V) = V >= V = isNePal(activate(V))

             isQid(n__o()) = 0 >= 0 = tt()

             isQid(n__u()) = 0 >= 0 = tt()

             __(X,nil()) = X >= X = X

             __(nil(),X) = X >= X = X

             and(tt(),X) = X >= X = activate(X)

             isList(n__nil()) = 16 >= 0 = tt()

             isList(n____(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 2 = and(isList(activate(V1)),n__isList(activate(V2)))

             isNeList(V) = V >= V = isQid(activate(V))

             isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 2 = and(isList(activate(V1)),n__isNeList(activate(V2)))

             isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 = and(isNeList(activate(V1)),n__isList(activate(V2)))

             isNePal(V) = V >= V = isQid(activate(V))

             isNePal(n____(I,__(P,I))) = 2I + P + 15 >= I + P + 1 = and(isQid(activate(I)),n__isPal(activate(P)))

             isPal(n__nil()) = 14 >= 0 = tt()

             isQid(n__a()) = 1 >= 0 = tt()

             isQid(n__e()) = 2 >= 0 = tt()

             isQid(n__i()) = 2 >= 0 = tt()

             isList(X) = X + 2 >= X = n__isList(X)

             isNeList(X) = X >= X = n__isNeList(X)

             activate(n__nil()) = 14 >= 0 = nil()

             activate(n____(X1,X2)) = X1 + X2 + 15 >= X1 + X2 = __(X1,X2)

             activate(n__isPal(X)) = X + 1 >= X = isPal(X)

             activate(n__a()) = 1 >= 1 = a()

             activate(n__e()) = 2 >= 2 = e()

             activate(n__i()) = 2 >= 2 = i()

             activate(n__o()) = 0 >= 0 = o()

             activate(n__u()) = 0 >= 0 = u()

             activate(X) = X >= X = X
            problem:
             strict:
              __(__(X,Y),Z) -> __(X,__(Y,Z))
              nil() -> n__nil()
              __(X1,X2) -> n____(X1,X2)
              isPal(X) -> n__isPal(X)
              a() -> n__a()
              e() -> n__e()
              i() -> n__i()
              o() -> n__o()
              u() -> n__u()
              activate(n__isList(X)) -> isList(X)
              activate(n__isNeList(X)) -> isNeList(X)
             weak:
              isList(V) -> isNeList(activate(V))
              isPal(V) -> isNePal(activate(V))
              isQid(n__o()) -> tt()
              isQid(n__u()) -> tt()
              __(X,nil()) -> X
              __(nil(),X) -> X
              and(tt(),X) -> activate(X)
              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(n__nil()) -> tt()
              isQid(n__a()) -> tt()
              isQid(n__e()) -> tt()
              isQid(n__i()) -> tt()
              isList(X) -> n__isList(X)
              isNeList(X) -> n__isNeList(X)
              activate(n__nil()) -> nil()
              activate(n____(X1,X2)) -> __(X1,X2)
              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
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [u] = 69,

               [o] = 69,

               [i] = 97,

               [e] = 69,

               [a] = 0,

               [n__u] = 68,

               [n__o] = 68,

               [n__i] = 96,

               [n__e] = 68,

               [n__a] = 68,

               [isPal](x0) = x0 + 36,

               [n__isPal](x0) = x0 + 35,

               [isNePal](x0) = x0 + 35,

               [n__isNeList](x0) = x0 + 4,

               [isQid](x0) = x0,

               [n__isList](x0) = x0 + 5,

               [n____](x0, x1) = x0 + x1 + 16,

               [n__nil] = 70,

               [isNeList](x0) = x0 + 4,

               [isList](x0) = x0 + 5,

               [activate](x0) = x0 + 1,

               [and](x0, x1) = x0 + x1 + 9,

               [tt] = 68,

               [nil] = 0,

               [__](x0, x1) = x0 + x1
              orientation:
               __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))

               nil() = 0 >= 70 = n__nil()

               __(X1,X2) = X1 + X2 >= X1 + X2 + 16 = n____(X1,X2)

               isPal(X) = X + 36 >= X + 35 = n__isPal(X)

               a() = 0 >= 68 = n__a()

               e() = 69 >= 68 = n__e()

               i() = 97 >= 96 = n__i()

               o() = 69 >= 68 = n__o()

               u() = 69 >= 68 = n__u()

               activate(n__isList(X)) = X + 6 >= X + 5 = isList(X)

               activate(n__isNeList(X)) = X + 5 >= X + 4 = isNeList(X)

               isList(V) = V + 5 >= V + 5 = isNeList(activate(V))

               isPal(V) = V + 36 >= V + 36 = isNePal(activate(V))

               isQid(n__o()) = 68 >= 68 = tt()

               isQid(n__u()) = 68 >= 68 = tt()

               __(X,nil()) = X >= X = X

               __(nil(),X) = X >= X = X

               and(tt(),X) = X + 77 >= X + 1 = activate(X)

               isList(n__nil()) = 75 >= 68 = tt()

               isList(n____(V1,V2)) = V1 + V2 + 21 >= V1 + V2 + 21 = and(isList(activate(V1)),n__isList(activate(V2)))

               isNeList(V) = V + 4 >= V + 1 = isQid(activate(V))

               isNeList(n____(V1,V2)) = V1 + V2 + 20 >= V1 + V2 + 20 = and(isList(activate(V1)),n__isNeList(activate(V2)))

               isNeList(n____(V1,V2)) = V1 + V2 + 20 >= V1 + V2 + 20 = and(isNeList(activate(V1)),n__isList(activate(V2)))

               isNePal(V) = V + 35 >= V + 1 = isQid(activate(V))

               isNePal(n____(I,__(P,I))) = 2I + P + 51 >= I + P + 46 = and(isQid(activate(I)),n__isPal(activate(P)))

               isPal(n__nil()) = 106 >= 68 = tt()

               isQid(n__a()) = 68 >= 68 = tt()

               isQid(n__e()) = 68 >= 68 = tt()

               isQid(n__i()) = 96 >= 68 = tt()

               isList(X) = X + 5 >= X + 5 = n__isList(X)

               isNeList(X) = X + 4 >= X + 4 = n__isNeList(X)

               activate(n__nil()) = 71 >= 0 = nil()

               activate(n____(X1,X2)) = X1 + X2 + 17 >= X1 + X2 = __(X1,X2)

               activate(n__isPal(X)) = X + 36 >= X + 36 = isPal(X)

               activate(n__a()) = 69 >= 0 = a()

               activate(n__e()) = 69 >= 69 = e()

               activate(n__i()) = 97 >= 97 = i()

               activate(n__o()) = 69 >= 69 = o()

               activate(n__u()) = 69 >= 69 = u()

               activate(X) = X + 1 >= X = X
              problem:
               strict:
                __(__(X,Y),Z) -> __(X,__(Y,Z))
                nil() -> n__nil()
                __(X1,X2) -> n____(X1,X2)
                a() -> n__a()
               weak:
                isPal(X) -> n__isPal(X)
                e() -> n__e()
                i() -> n__i()
                o() -> n__o()
                u() -> n__u()
                activate(n__isList(X)) -> isList(X)
                activate(n__isNeList(X)) -> isNeList(X)
                isList(V) -> isNeList(activate(V))
                isPal(V) -> isNePal(activate(V))
                isQid(n__o()) -> tt()
                isQid(n__u()) -> tt()
                __(X,nil()) -> X
                __(nil(),X) -> X
                and(tt(),X) -> activate(X)
                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(n__nil()) -> tt()
                isQid(n__a()) -> tt()
                isQid(n__e()) -> tt()
                isQid(n__i()) -> tt()
                isList(X) -> n__isList(X)
                isNeList(X) -> n__isNeList(X)
                activate(n__nil()) -> nil()
                activate(n____(X1,X2)) -> __(X1,X2)
                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
              Matrix Interpretation Processor:
               dimension: 1
               max_matrix:
                1
                interpretation:
                 [u] = 0,

                 [o] = 4,

                 [i] = 11,

                 [e] = 2,

                 [a] = 1,

                 [n__u] = 0,

                 [n__o] = 4,

                 [n__i] = 11,

                 [n__e] = 2,

                 [n__a] = 0,

                 [isPal](x0) = x0 + 9,

                 [n__isPal](x0) = x0 + 9,

                 [isNePal](x0) = x0 + 8,

                 [n__isNeList](x0) = x0 + 6,

                 [isQid](x0) = x0 + 5,

                 [n__isList](x0) = x0 + 7,

                 [n____](x0, x1) = x0 + x1 + 12,

                 [n__nil] = 5,

                 [isNeList](x0) = x0 + 7,

                 [isList](x0) = x0 + 8,

                 [activate](x0) = x0 + 1,

                 [and](x0, x1) = x0 + x1 + 3,

                 [tt] = 1,

                 [nil] = 1,

                 [__](x0, x1) = x0 + x1 + 1
                orientation:
                 __(__(X,Y),Z) = X + Y + Z + 2 >= X + Y + Z + 2 = __(X,__(Y,Z))

                 nil() = 1 >= 5 = n__nil()

                 __(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 12 = n____(X1,X2)

                 a() = 1 >= 0 = n__a()

                 isPal(X) = X + 9 >= X + 9 = n__isPal(X)

                 e() = 2 >= 2 = n__e()

                 i() = 11 >= 11 = n__i()

                 o() = 4 >= 4 = n__o()

                 u() = 0 >= 0 = n__u()

                 activate(n__isList(X)) = X + 8 >= X + 8 = isList(X)

                 activate(n__isNeList(X)) = X + 7 >= X + 7 = isNeList(X)

                 isList(V) = V + 8 >= V + 8 = isNeList(activate(V))

                 isPal(V) = V + 9 >= V + 9 = isNePal(activate(V))

                 isQid(n__o()) = 9 >= 1 = tt()

                 isQid(n__u()) = 5 >= 1 = tt()

                 __(X,nil()) = X + 2 >= X = X

                 __(nil(),X) = X + 2 >= X = X

                 and(tt(),X) = X + 4 >= X + 1 = activate(X)

                 isList(n__nil()) = 13 >= 1 = tt()

                 isList(n____(V1,V2)) = V1 + V2 + 20 >= V1 + V2 + 20 = and(isList(activate(V1)),n__isList(activate(V2)))

                 isNeList(V) = V + 7 >= V + 6 = isQid(activate(V))

                 isNeList(n____(V1,V2)) = V1 + V2 + 19 >= V1 + V2 + 19 = and(isList(activate(V1)),n__isNeList(activate(V2)))

                 isNeList(n____(V1,V2)) = V1 + V2 + 19 >= V1 + V2 + 19 = and(isNeList(activate(V1)),n__isList(activate(V2)))

                 isNePal(V) = V + 8 >= V + 6 = isQid(activate(V))

                 isNePal(n____(I,__(P,I))) = 2I + P + 21 >= I + P + 19 = and(isQid(activate(I)),n__isPal(activate(P)))

                 isPal(n__nil()) = 14 >= 1 = tt()

                 isQid(n__a()) = 5 >= 1 = tt()

                 isQid(n__e()) = 7 >= 1 = tt()

                 isQid(n__i()) = 16 >= 1 = tt()

                 isList(X) = X + 8 >= X + 7 = n__isList(X)

                 isNeList(X) = X + 7 >= X + 6 = n__isNeList(X)

                 activate(n__nil()) = 6 >= 1 = nil()

                 activate(n____(X1,X2)) = X1 + X2 + 13 >= X1 + X2 + 1 = __(X1,X2)

                 activate(n__isPal(X)) = X + 10 >= X + 9 = isPal(X)

                 activate(n__a()) = 1 >= 1 = a()

                 activate(n__e()) = 3 >= 2 = e()

                 activate(n__i()) = 12 >= 11 = i()

                 activate(n__o()) = 5 >= 4 = o()

                 activate(n__u()) = 1 >= 0 = u()

                 activate(X) = X + 1 >= X = X
                problem:
                 strict:
                  __(__(X,Y),Z) -> __(X,__(Y,Z))
                  nil() -> n__nil()
                  __(X1,X2) -> n____(X1,X2)
                 weak:
                  a() -> n__a()
                  isPal(X) -> n__isPal(X)
                  e() -> n__e()
                  i() -> n__i()
                  o() -> n__o()
                  u() -> n__u()
                  activate(n__isList(X)) -> isList(X)
                  activate(n__isNeList(X)) -> isNeList(X)
                  isList(V) -> isNeList(activate(V))
                  isPal(V) -> isNePal(activate(V))
                  isQid(n__o()) -> tt()
                  isQid(n__u()) -> tt()
                  __(X,nil()) -> X
                  __(nil(),X) -> X
                  and(tt(),X) -> activate(X)
                  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(n__nil()) -> tt()
                  isQid(n__a()) -> tt()
                  isQid(n__e()) -> tt()
                  isQid(n__i()) -> tt()
                  isList(X) -> n__isList(X)
                  isNeList(X) -> n__isNeList(X)
                  activate(n__nil()) -> nil()
                  activate(n____(X1,X2)) -> __(X1,X2)
                  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
                Matrix Interpretation Processor:
                 dimension: 1
                 max_matrix:
                  1
                  interpretation:
                   [u] = 7,

                   [o] = 54,

                   [i] = 2,

                   [e] = 41,

                   [a] = 25,

                   [n__u] = 7,

                   [n__o] = 52,

                   [n__i] = 0,

                   [n__e] = 33,

                   [n__a] = 17,

                   [isPal](x0) = x0 + 72,

                   [n__isPal](x0) = x0 + 65,

                   [isNePal](x0) = x0 + 18,

                   [n__isNeList](x0) = x0 + 9,

                   [isQid](x0) = x0 + 8,

                   [n__isList](x0) = x0 + 26,

                   [n____](x0, x1) = x0 + x1 + 65,

                   [n__nil] = 16,

                   [isNeList](x0) = x0 + 16,

                   [isList](x0) = x0 + 33,

                   [activate](x0) = x0 + 8,

                   [and](x0, x1) = x0 + x1 + 23,

                   [tt] = 0,

                   [nil] = 22,

                   [__](x0, x1) = x0 + x1 + 73
                  orientation:
                   __(__(X,Y),Z) = X + Y + Z + 146 >= X + Y + Z + 146 = __(X,__(Y,Z))

                   nil() = 22 >= 16 = n__nil()

                   __(X1,X2) = X1 + X2 + 73 >= X1 + X2 + 65 = n____(X1,X2)

                   a() = 25 >= 17 = n__a()

                   isPal(X) = X + 72 >= X + 65 = n__isPal(X)

                   e() = 41 >= 33 = n__e()

                   i() = 2 >= 0 = n__i()

                   o() = 54 >= 52 = n__o()

                   u() = 7 >= 7 = n__u()

                   activate(n__isList(X)) = X + 34 >= X + 33 = isList(X)

                   activate(n__isNeList(X)) = X + 17 >= X + 16 = isNeList(X)

                   isList(V) = V + 33 >= V + 24 = isNeList(activate(V))

                   isPal(V) = V + 72 >= V + 26 = isNePal(activate(V))

                   isQid(n__o()) = 60 >= 0 = tt()

                   isQid(n__u()) = 15 >= 0 = tt()

                   __(X,nil()) = X + 95 >= X = X

                   __(nil(),X) = X + 95 >= X = X

                   and(tt(),X) = X + 23 >= X + 8 = activate(X)

                   isList(n__nil()) = 49 >= 0 = tt()

                   isList(n____(V1,V2)) = V1 + V2 + 98 >= V1 + V2 + 98 = and(isList(activate(V1)),n__isList(activate(V2)))

                   isNeList(V) = V + 16 >= V + 16 = isQid(activate(V))

                   isNeList(n____(V1,V2)) = V1 + V2 + 81 >= V1 + V2 + 81 = and(isList(activate(V1)),n__isNeList(activate(V2)))

                   isNeList(n____(V1,V2)) = V1 + V2 + 81 >= V1 + V2 + 81 = and(isNeList(activate(V1)),n__isList(activate(V2)))

                   isNePal(V) = V + 18 >= V + 16 = isQid(activate(V))

                   isNePal(n____(I,__(P,I))) = 2I + P + 156 >= I + P + 112 = and(isQid(activate(I)),n__isPal(activate(P)))

                   isPal(n__nil()) = 88 >= 0 = tt()

                   isQid(n__a()) = 25 >= 0 = tt()

                   isQid(n__e()) = 41 >= 0 = tt()

                   isQid(n__i()) = 8 >= 0 = tt()

                   isList(X) = X + 33 >= X + 26 = n__isList(X)

                   isNeList(X) = X + 16 >= X + 9 = n__isNeList(X)

                   activate(n__nil()) = 24 >= 22 = nil()

                   activate(n____(X1,X2)) = X1 + X2 + 73 >= X1 + X2 + 73 = __(X1,X2)

                   activate(n__isPal(X)) = X + 73 >= X + 72 = isPal(X)

                   activate(n__a()) = 25 >= 25 = a()

                   activate(n__e()) = 41 >= 41 = e()

                   activate(n__i()) = 8 >= 2 = i()

                   activate(n__o()) = 60 >= 54 = o()

                   activate(n__u()) = 15 >= 7 = u()

                   activate(X) = X + 8 >= X = X
                  problem:
                   strict:
                    __(__(X,Y),Z) -> __(X,__(Y,Z))
                   weak:
                    nil() -> n__nil()
                    __(X1,X2) -> n____(X1,X2)
                    a() -> n__a()
                    isPal(X) -> n__isPal(X)
                    e() -> n__e()
                    i() -> n__i()
                    o() -> n__o()
                    u() -> n__u()
                    activate(n__isList(X)) -> isList(X)
                    activate(n__isNeList(X)) -> isNeList(X)
                    isList(V) -> isNeList(activate(V))
                    isPal(V) -> isNePal(activate(V))
                    isQid(n__o()) -> tt()
                    isQid(n__u()) -> tt()
                    __(X,nil()) -> X
                    __(nil(),X) -> X
                    and(tt(),X) -> activate(X)
                    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(n__nil()) -> tt()
                    isQid(n__a()) -> tt()
                    isQid(n__e()) -> tt()
                    isQid(n__i()) -> tt()
                    isList(X) -> n__isList(X)
                    isNeList(X) -> n__isNeList(X)
                    activate(n__nil()) -> nil()
                    activate(n____(X1,X2)) -> __(X1,X2)
                    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
                  Matrix Interpretation Processor:
                   dimension: 2
                   max_matrix:
                    [1 1]
                    [0 1]
                    interpretation:
                           [3]
                     [u] = [0],

                           [0]
                     [o] = [1],

                           [0]
                     [i] = [0],

                           [0]
                     [e] = [0],

                           [3]
                     [a] = [2],

                              [3]
                     [n__u] = [0],

                              [0]
                     [n__o] = [1],

                              [0]
                     [n__i] = [0],

                              [0]
                     [n__e] = [0],

                              [3]
                     [n__a] = [2],

                                        [0]
                     [isPal](x0) = x0 + [1],

                                           [0]
                     [n__isPal](x0) = x0 + [1],


                     [isNePal](x0) = x0,


                     [n__isNeList](x0) = x0,

                                   [1 0]
                     [isQid](x0) = [0 0]x0,


                     [n__isList](x0) = x0,

                                       [1 1]          [0]
                     [n____](x0, x1) = [0 1]x0 + x1 + [1],

                                [0]
                     [n__nil] = [0],


                     [isNeList](x0) = x0,


                     [isList](x0) = x0,


                     [activate](x0) = x0,

                                     [1 1]          [0]
                     [and](x0, x1) = [0 0]x0 + x1 + [1],

                            [0]
                     [tt] = [0],

                             [0]
                     [nil] = [0],

                                    [1 1]          [0]
                     [__](x0, x1) = [0 1]x0 + x1 + [1]
                    orientation:
                                     [1 2]    [1 1]        [1]    [1 1]    [1 1]        [0]
                     __(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [2] >= [0 1]X + [0 1]Y + Z + [2] = __(X,__(Y,Z))

                             [0]    [0]
                     nil() = [0] >= [0] = n__nil()

                                 [1 1]          [0]    [1 1]          [0]
                     __(X1,X2) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = n____(X1,X2)

                           [3]    [3]
                     a() = [2] >= [2] = n__a()

                                    [0]        [0]
                     isPal(X) = X + [1] >= X + [1] = n__isPal(X)

                           [0]    [0]
                     e() = [0] >= [0] = n__e()

                           [0]    [0]
                     i() = [0] >= [0] = n__i()

                           [0]    [0]
                     o() = [1] >= [1] = n__o()

                           [3]    [3]
                     u() = [0] >= [0] = n__u()


                     activate(n__isList(X)) = X >= X = isList(X)


                     activate(n__isNeList(X)) = X >= X = isNeList(X)


                     isList(V) = V >= V = isNeList(activate(V))

                                    [0]
                     isPal(V) = V + [1] >= V = isNePal(activate(V))

                                     [0]    [0]
                     isQid(n__o()) = [0] >= [0] = tt()

                                     [3]    [0]
                     isQid(n__u()) = [0] >= [0] = tt()

                                   [1 1]    [0]
                     __(X,nil()) = [0 1]X + [1] >= X = X

                                       [0]
                     __(nil(),X) = X + [1] >= X = X

                                       [0]
                     and(tt(),X) = X + [1] >= X = activate(X)

                                        [0]    [0]
                     isList(n__nil()) = [0] >= [0] = tt()

                                            [1 1]          [0]    [1 1]          [0]
                     isList(n____(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + V2 + [1] = and(isList(activate(V1)),n__isList(activate(V2)))

                                        [1 0]
                     isNeList(V) = V >= [0 0]V = isQid(activate(V))

                                              [1 1]          [0]    [1 1]          [0]
                     isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + V2 + [1] = and(isList(activate(V1)),n__isNeList(activate(V2)))

                                              [1 1]          [0]    [1 1]          [0]
                     isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + V2 + [1] = and(isNeList(activate(V1)),n__isList(activate(V2)))

                                       [1 0]
                     isNePal(V) = V >= [0 0]V = isQid(activate(V))

                                                 [2 1]    [1 1]    [0]    [1 0]        [0]
                     isNePal(n____(I,__(P,I))) = [0 2]I + [0 1]P + [2] >= [0 0]I + P + [2] = and(isQid(activate(I)),n__isPal(activate(P)))

                                       [0]    [0]
                     isPal(n__nil()) = [1] >= [0] = tt()

                                     [3]    [0]
                     isQid(n__a()) = [0] >= [0] = tt()

                                     [0]    [0]
                     isQid(n__e()) = [0] >= [0] = tt()

                                     [0]    [0]
                     isQid(n__i()) = [0] >= [0] = tt()


                     isList(X) = X >= X = n__isList(X)


                     isNeList(X) = X >= X = n__isNeList(X)

                                          [0]    [0]
                     activate(n__nil()) = [0] >= [0] = nil()

                                              [1 1]          [0]    [1 1]          [0]
                     activate(n____(X1,X2)) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = __(X1,X2)

                                                 [0]        [0]
                     activate(n__isPal(X)) = X + [1] >= X + [1] = isPal(X)

                                        [3]    [3]
                     activate(n__a()) = [2] >= [2] = a()

                                        [0]    [0]
                     activate(n__e()) = [0] >= [0] = e()

                                        [0]    [0]
                     activate(n__i()) = [0] >= [0] = i()

                                        [0]    [0]
                     activate(n__o()) = [1] >= [1] = o()

                                        [3]    [3]
                     activate(n__u()) = [0] >= [0] = u()


                     activate(X) = X >= X = X
                    problem:
                     strict:

                     weak:
                      __(__(X,Y),Z) -> __(X,__(Y,Z))
                      nil() -> n__nil()
                      __(X1,X2) -> n____(X1,X2)
                      a() -> n__a()
                      isPal(X) -> n__isPal(X)
                      e() -> n__e()
                      i() -> n__i()
                      o() -> n__o()
                      u() -> n__u()
                      activate(n__isList(X)) -> isList(X)
                      activate(n__isNeList(X)) -> isNeList(X)
                      isList(V) -> isNeList(activate(V))
                      isPal(V) -> isNePal(activate(V))
                      isQid(n__o()) -> tt()
                      isQid(n__u()) -> tt()
                      __(X,nil()) -> X
                      __(nil(),X) -> X
                      and(tt(),X) -> activate(X)
                      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(n__nil()) -> tt()
                      isQid(n__a()) -> tt()
                      isQid(n__e()) -> tt()
                      isQid(n__i()) -> tt()
                      isList(X) -> n__isList(X)
                      isNeList(X) -> n__isNeList(X)
                      activate(n__nil()) -> nil()
                      activate(n____(X1,X2)) -> __(X1,X2)
                      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
                    Qed

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 PALINDROME nokinds Z

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nokinds Z

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  __(__(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}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 PALINDROME nokinds Z

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nokinds Z

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  __(__(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}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds