Problem Transformed CSR 04 PALINDROME nokinds FR

Tool CaT

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

stdout:

MAYBE

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,n____(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)) -> __(activate(X1),activate(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,n____(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)) -> __(activate(X1),activate(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] = 1,

     [n__o] = 8,

     [n__i] = 0,

     [n__e] = 8,

     [n__a] = 3,

     [isPal](x0) = x0 + 1,

     [n__isPal](x0) = x0,

     [isNePal](x0) = x0 + 5,

     [n__isNeList](x0) = x0,

     [isQid](x0) = x0 + 1,

     [n__isList](x0) = x0 + 1,

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

     [n__nil] = 0,

     [isNeList](x0) = x0 + 4,

     [isList](x0) = x0 + 2,

     [activate](x0) = x0 + 11,

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

     [tt] = 10,

     [nil] = 2,

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

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

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

     and(tt(),X) = X + 10 >= X + 11 = activate(X)

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

     isList(n__nil()) = 2 >= 10 = tt()

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

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

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

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

     isNePal(V) = V + 5 >= V + 12 = isQid(activate(V))

     isNePal(n____(I,n____(P,I))) = 2I + P + 31 >= I + P + 23 = and(isQid(activate(I)),n__isPal(activate(P)))

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

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

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

     isQid(n__e()) = 9 >= 10 = tt()

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

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

     isQid(n__u()) = 2 >= 10 = tt()

     nil() = 2 >= 0 = n__nil()

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

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

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

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

     a() = 0 >= 3 = n__a()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

       [o] = 9,

       [i] = 0,

       [e] = 0,

       [a] = 0,

       [n__u] = 24,

       [n__o] = 9,

       [n__i] = 3,

       [n__e] = 0,

       [n__a] = 16,

       [isPal](x0) = x0 + 4,

       [n__isPal](x0) = x0 + 4,

       [isNePal](x0) = x0 + 54,

       [n__isNeList](x0) = x0 + 6,

       [isQid](x0) = x0 + 36,

       [n__isList](x0) = x0 + 9,

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

       [n__nil] = 0,

       [isNeList](x0) = x0 + 6,

       [isList](x0) = x0 + 9,

       [activate](x0) = x0,

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

       [tt] = 4,

       [nil] = 0,

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

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

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

       isList(n__nil()) = 9 >= 4 = tt()

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

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

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

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

       isNePal(V) = V + 54 >= V + 36 = isQid(activate(V))

       isPal(V) = V + 4 >= V + 54 = isNePal(activate(V))

       isPal(n__nil()) = 4 >= 4 = tt()

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

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

       isQid(n__i()) = 39 >= 4 = tt()

       isQid(n__o()) = 45 >= 4 = tt()

       isQid(n__u()) = 60 >= 4 = tt()

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

       a() = 0 >= 16 = n__a()

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

       i() = 0 >= 3 = n__i()

       o() = 9 >= 9 = n__o()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

       activate(n__o()) = 9 >= 9 = o()

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

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

         [o] = 12,

         [i] = 10,

         [e] = 34,

         [a] = 0,

         [n__u] = 57,

         [n__o] = 10,

         [n__i] = 2,

         [n__e] = 26,

         [n__a] = 1,

         [isPal](x0) = x0,

         [n__isPal](x0) = x0,

         [isNePal](x0) = x0 + 17,

         [n__isNeList](x0) = x0,

         [isQid](x0) = x0 + 9,

         [n__isList](x0) = x0 + 32,

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

         [n__nil] = 2,

         [isNeList](x0) = x0,

         [isList](x0) = x0 + 32,

         [activate](x0) = x0 + 8,

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

         [tt] = 0,

         [nil] = 4,

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

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

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

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

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

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

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

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

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

         e() = 34 >= 26 = n__e()

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

         o() = 12 >= 10 = n__o()

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

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

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

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

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

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

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

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

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

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

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

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

         isNePal(n____(I,n____(P,I))) = 2I + P + 113 >= I + P + 58 = and(isQid(activate(I)),n__isPal(activate(P)))

         nil() = 4 >= 2 = n__nil()

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

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

         isPal(X) = X >= X = n__isPal(X)

         activate(n__nil()) = 10 >= 4 = nil()

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

         activate(n__isList(X)) = X + 40 >= X + 32 = isList(X)

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

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

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

         activate(n__e()) = 34 >= 34 = e()

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

         activate(n__o()) = 18 >= 12 = o()

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

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

           [o] = 2,

           [i] = 0,

           [e] = 0,

           [a] = 0,

           [n__u] = 2,

           [n__o] = 2,

           [n__i] = 0,

           [n__e] = 0,

           [n__a] = 1,

           [isPal](x0) = x0,

           [n__isPal](x0) = x0,

           [isNePal](x0) = x0 + 2,

           [n__isNeList](x0) = x0,

           [isQid](x0) = x0 + 2,

           [n__isList](x0) = x0,

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

           [n__nil] = 0,

           [isNeList](x0) = x0,

           [isList](x0) = x0,

           [activate](x0) = x0,

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

           [tt] = 0,

           [nil] = 0,

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

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

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

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

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

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

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

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

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

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

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

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

           o() = 2 >= 2 = n__o()

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

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

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

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

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

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

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

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

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

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

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

           isNePal(n____(I,n____(P,I))) = 2I + P + 22 >= I + P + 11 = and(isQid(activate(I)),n__isPal(activate(P)))

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

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

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

           isPal(X) = X >= X = n__isPal(X)

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

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

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

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

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

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

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

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

           activate(n__o()) = 2 >= 2 = o()

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

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

             [o] = 20,

             [i] = 4,

             [e] = 0,

             [a] = 2,

             [n__u] = 16,

             [n__o] = 20,

             [n__i] = 4,

             [n__e] = 0,

             [n__a] = 1,

             [isPal](x0) = x0,

             [n__isPal](x0) = x0,

             [isNePal](x0) = x0 + 16,

             [n__isNeList](x0) = x0 + 1,

             [isQid](x0) = x0 + 9,

             [n__isList](x0) = x0 + 3,

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

             [n__nil] = 2,

             [isNeList](x0) = x0 + 2,

             [isList](x0) = x0 + 4,

             [activate](x0) = x0 + 2,

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

             [tt] = 2,

             [nil] = 4,

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

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

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

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

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

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

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

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

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

             isPal(n__nil()) = 2 >= 2 = tt()

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

             i() = 4 >= 4 = n__i()

             o() = 20 >= 20 = n__o()

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

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

             isList(n__nil()) = 6 >= 2 = tt()

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

             isQid(n__a()) = 10 >= 2 = tt()

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

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

             isQid(n__o()) = 29 >= 2 = tt()

             isQid(n__u()) = 25 >= 2 = tt()

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

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

             isNePal(n____(I,n____(P,I))) = 2I + P + 30 >= I + P + 13 = and(isQid(activate(I)),n__isPal(activate(P)))

             nil() = 4 >= 2 = n__nil()

             isList(X) = X + 4 >= X + 3 = n__isList(X)

             isNeList(X) = X + 2 >= X + 1 = n__isNeList(X)

             isPal(X) = X >= X = n__isPal(X)

             activate(n__nil()) = 4 >= 4 = nil()

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

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

             activate(n__isNeList(X)) = X + 3 >= X + 2 = isNeList(X)

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

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

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

             activate(n__i()) = 6 >= 4 = i()

             activate(n__o()) = 22 >= 20 = o()

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

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

               [o] = 18,

               [i] = 2,

               [e] = 0,

               [a] = 1,

               [n__u] = 16,

               [n__o] = 18,

               [n__i] = 2,

               [n__e] = 0,

               [n__a] = 0,

               [isPal](x0) = x0 + 1,

               [n__isPal](x0) = x0 + 1,

               [isNePal](x0) = x0 + 3,

               [n__isNeList](x0) = x0 + 4,

               [isQid](x0) = x0 + 1,

               [n__isList](x0) = x0 + 18,

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

               [n__nil] = 0,

               [isNeList](x0) = x0 + 4,

               [isList](x0) = x0 + 19,

               [activate](x0) = x0 + 1,

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

               [tt] = 0,

               [nil] = 1,

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

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

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

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

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

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

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

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

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

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

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

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

               o() = 18 >= 18 = n__o()

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

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

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

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

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

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

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

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

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

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

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

               isNePal(n____(I,n____(P,I))) = 2I + P + 59 >= I + P + 11 = and(isQid(activate(I)),n__isPal(activate(P)))

               nil() = 1 >= 0 = n__nil()

               isList(X) = X + 19 >= X + 18 = n__isList(X)

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

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

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

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

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

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

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

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

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

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

               activate(n__o()) = 19 >= 18 = o()

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

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

                 [o] = 32,

                 [i] = 48,

                 [e] = 32,

                 [a] = 33,

                 [n__u] = 28,

                 [n__o] = 28,

                 [n__i] = 44,

                 [n__e] = 31,

                 [n__a] = 29,

                 [isPal](x0) = x0 + 51,

                 [n__isPal](x0) = x0 + 48,

                 [isNePal](x0) = x0 + 13,

                 [n__isNeList](x0) = x0 + 10,

                 [isQid](x0) = x0 + 4,

                 [n__isList](x0) = x0 + 34,

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

                 [n__nil] = 4,

                 [isNeList](x0) = x0 + 11,

                 [isList](x0) = x0 + 37,

                 [activate](x0) = x0 + 4,

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

                 [tt] = 32,

                 [nil] = 8,

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

                 isPal(V) = V + 51 >= V + 17 = isNePal(activate(V))

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

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

                 isNeList(V) = V + 11 >= V + 8 = isQid(activate(V))

                 a() = 33 >= 29 = n__a()

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

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

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

                 isPal(n__nil()) = 55 >= 32 = tt()

                 e() = 32 >= 31 = n__e()

                 i() = 48 >= 44 = n__i()

                 o() = 32 >= 28 = n__o()

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

                 isList(V) = V + 37 >= V + 15 = isNeList(activate(V))

                 isList(n__nil()) = 41 >= 32 = tt()

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

                 isQid(n__a()) = 33 >= 32 = tt()

                 isQid(n__e()) = 35 >= 32 = tt()

                 isQid(n__i()) = 48 >= 32 = tt()

                 isQid(n__o()) = 32 >= 32 = tt()

                 isQid(n__u()) = 32 >= 32 = tt()

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

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

                 isNePal(n____(I,n____(P,I))) = 2I + P + 127 >= I + P + 73 = and(isQid(activate(I)),n__isPal(activate(P)))

                 nil() = 8 >= 4 = n__nil()

                 isList(X) = X + 37 >= X + 34 = n__isList(X)

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

                 isPal(X) = X + 51 >= X + 48 = n__isPal(X)

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

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

                 activate(n__isList(X)) = X + 38 >= X + 37 = isList(X)

                 activate(n__isNeList(X)) = X + 14 >= X + 11 = isNeList(X)

                 activate(n__isPal(X)) = X + 52 >= X + 51 = isPal(X)

                 activate(n__a()) = 33 >= 33 = a()

                 activate(n__e()) = 35 >= 32 = e()

                 activate(n__i()) = 48 >= 48 = i()

                 activate(n__o()) = 32 >= 32 = o()

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

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

                   [o] = 5,

                   [i] = 12,

                   [e] = 13,

                   [a] = 4,

                   [n__u] = 4,

                   [n__o] = 4,

                   [n__i] = 11,

                   [n__e] = 9,

                   [n__a] = 4,

                   [isPal](x0) = x0 + 8,

                   [n__isPal](x0) = x0 + 4,

                   [isNePal](x0) = x0 + 4,

                   [n__isNeList](x0) = x0,

                   [isQid](x0) = x0,

                   [n__isList](x0) = x0 + 4,

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

                   [n__nil] = 3,

                   [isNeList](x0) = x0 + 4,

                   [isList](x0) = x0 + 8,

                   [activate](x0) = x0 + 4,

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

                   [tt] = 3,

                   [nil] = 4,

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

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

                   u() = 6 >= 4 = n__u()

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

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

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

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

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

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

                   isPal(n__nil()) = 11 >= 3 = tt()

                   e() = 13 >= 9 = n__e()

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

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

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

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

                   isList(n__nil()) = 11 >= 3 = tt()

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

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

                   isQid(n__e()) = 9 >= 3 = tt()

                   isQid(n__i()) = 11 >= 3 = tt()

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

                   isQid(n__u()) = 4 >= 3 = tt()

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

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

                   isNePal(n____(I,n____(P,I))) = 2I + P + 30 >= I + P + 13 = and(isQid(activate(I)),n__isPal(activate(P)))

                   nil() = 4 >= 3 = n__nil()

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

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

                   isPal(X) = X + 8 >= X + 4 = n__isPal(X)

                   activate(n__nil()) = 7 >= 4 = nil()

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

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

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

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

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

                   activate(n__e()) = 13 >= 13 = e()

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

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

                   activate(n__u()) = 8 >= 6 = u()

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

                           [0]
                     [o] = [1],

                           [2]
                     [i] = [0],

                           [0]
                     [e] = [2],

                           [2]
                     [a] = [0],

                              [1]
                     [n__u] = [0],

                              [0]
                     [n__o] = [1],

                              [2]
                     [n__i] = [0],

                              [0]
                     [n__e] = [2],

                              [2]
                     [n__a] = [0],

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

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

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

                                         [1 2]
                     [n__isNeList](x0) = [0 0]x0,

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

                                       [1 2]
                     [n__isList](x0) = [0 0]x0,

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

                                [0]
                     [n__nil] = [0],

                                      [1 2]
                     [isNeList](x0) = [0 0]x0,

                                    [1 2]
                     [isList](x0) = [0 0]x0,


                     [activate](x0) = x0,

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

                            [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))

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

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

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

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

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

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

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

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

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

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

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

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


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

                                 [1 2]     [1 2]
                     isList(V) = [0 0]V >= [0 0]V = isNeList(activate(V))

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

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

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

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

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

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

                                     [1]    [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

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

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

                                 [1 2]     [1 2]
                     isList(X) = [0 0]X >= [0 0]X = n__isList(X)

                                   [1 2]     [1 2]
                     isNeList(X) = [0 0]X >= [0 0]X = n__isNeList(X)

                                [1 0]    [0]    [1 0]    [0]
                     isPal(X) = [0 0]X + [1] >= [0 0]X + [1] = n__isPal(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] = __(activate(X1),activate(X2))

                                              [1 2]     [1 2]
                     activate(n__isList(X)) = [0 0]X >= [0 0]X = isList(X)

                                                [1 2]     [1 2]
                     activate(n__isNeList(X)) = [0 0]X >= [0 0]X = isNeList(X)

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

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

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

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

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

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


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

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

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

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, n____(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)) -> __(activate(X1), activate(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 FR

stdout:

MAYBE

Tool RC2

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

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, n____(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)) -> __(activate(X1), activate(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