Problem Transformed CSR 04 PALINDROME nokinds-noand Z

Tool CaT

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

stdout:

YES(?,O(n^2))

Problem:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(V) -> U11(isNeList(activate(V)))
isList(n__nil()) -> tt()
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(V) -> U31(isQid(activate(V)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(V) -> U81(isNePal(activate(V)))
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
nil() -> n__nil()
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n__nil()) -> nil()
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__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
   U11(tt()) -> tt()
   U21(tt(),V2) -> U22(isList(activate(V2)))
   U22(tt()) -> tt()
   U31(tt()) -> tt()
   U41(tt(),V2) -> U42(isNeList(activate(V2)))
   U42(tt()) -> tt()
   U51(tt(),V2) -> U52(isList(activate(V2)))
   U52(tt()) -> tt()
   U61(tt()) -> tt()
   U71(tt(),P) -> U72(isPal(activate(P)))
   U72(tt()) -> tt()
   U81(tt()) -> tt()
   isList(V) -> U11(isNeList(activate(V)))
   isList(n__nil()) -> tt()
   isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
   isNeList(V) -> U31(isQid(activate(V)))
   isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
   isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
   isNePal(V) -> U61(isQid(activate(V)))
   isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
   isPal(V) -> U81(isNePal(activate(V)))
   isPal(n__nil()) -> tt()
   isQid(n__a()) -> tt()
   isQid(n__e()) -> tt()
   isQid(n__i()) -> tt()
   isQid(n__o()) -> tt()
   isQid(n__u()) -> tt()
   nil() -> n__nil()
   __(X1,X2) -> n____(X1,X2)
   a() -> n__a()
   e() -> n__e()
   i() -> n__i()
   o() -> n__o()
   u() -> n__u()
   activate(n__nil()) -> nil()
   activate(n____(X1,X2)) -> __(X1,X2)
   activate(n__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] = 0,

     [n__o] = 34,

     [n__i] = 16,

     [n__e] = 42,

     [n__a] = 0,

     [isNePal](x0) = x0 + 11,

     [isQid](x0) = x0 + 12,

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

     [n__nil] = 2,

     [U81](x0) = x0 + 40,

     [U72](x0) = x0 + 31,

     [isPal](x0) = x0 + 14,

     [U71](x0, x1) = x0 + x1 + 58,

     [U61](x0) = x0 + 11,

     [U52](x0) = x0 + 10,

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

     [U42](x0) = x0 + 46,

     [isNeList](x0) = x0 + 48,

     [U41](x0, x1) = x0 + x1 + 11,

     [U31](x0) = x0 + 8,

     [U22](x0) = x0 + 12,

     [isList](x0) = x0 + 1,

     [activate](x0) = x0 + 20,

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

     [U11](x0) = x0,

     [tt] = 53,

     [nil] = 6,

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

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

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

     U11(tt()) = 53 >= 53 = tt()

     U21(tt(),V2) = V2 + 67 >= V2 + 33 = U22(isList(activate(V2)))

     U22(tt()) = 65 >= 53 = tt()

     U31(tt()) = 61 >= 53 = tt()

     U41(tt(),V2) = V2 + 64 >= V2 + 114 = U42(isNeList(activate(V2)))

     U42(tt()) = 99 >= 53 = tt()

     U51(tt(),V2) = V2 + 61 >= V2 + 31 = U52(isList(activate(V2)))

     U52(tt()) = 63 >= 53 = tt()

     U61(tt()) = 64 >= 53 = tt()

     U71(tt(),P) = P + 111 >= P + 65 = U72(isPal(activate(P)))

     U72(tt()) = 84 >= 53 = tt()

     U81(tt()) = 93 >= 53 = tt()

     isList(V) = V + 1 >= V + 68 = U11(isNeList(activate(V)))

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

     isList(n____(V1,V2)) = V1 + V2 + 33 >= V1 + V2 + 55 = U21(isList(activate(V1)),activate(V2))

     isNeList(V) = V + 48 >= V + 40 = U31(isQid(activate(V)))

     isNeList(n____(V1,V2)) = V1 + V2 + 80 >= V1 + V2 + 52 = U41(isList(activate(V1)),activate(V2))

     isNeList(n____(V1,V2)) = V1 + V2 + 80 >= V1 + V2 + 96 = U51(isNeList(activate(V1)),activate(V2))

     isNePal(V) = V + 11 >= V + 43 = U61(isQid(activate(V)))

     isNePal(n____(I,__(P,I))) = 2I + P + 43 >= I + P + 110 = U71(isQid(activate(I)),activate(P))

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

     isPal(n__nil()) = 16 >= 53 = tt()

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

     isQid(n__e()) = 54 >= 53 = tt()

     isQid(n__i()) = 28 >= 53 = tt()

     isQid(n__o()) = 46 >= 53 = tt()

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

     nil() = 6 >= 2 = n__nil()

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

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

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

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

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

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

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

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

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

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

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

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

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

     activate(X) = X + 20 >= X = X
    problem:
     strict:
      __(__(X,Y),Z) -> __(X,__(Y,Z))
      U11(tt()) -> tt()
      U41(tt(),V2) -> U42(isNeList(activate(V2)))
      isList(V) -> U11(isNeList(activate(V)))
      isList(n__nil()) -> tt()
      isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
      isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
      isNePal(V) -> U61(isQid(activate(V)))
      isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
      isPal(V) -> U81(isNePal(activate(V)))
      isPal(n__nil()) -> tt()
      isQid(n__a()) -> tt()
      isQid(n__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
      U21(tt(),V2) -> U22(isList(activate(V2)))
      U22(tt()) -> tt()
      U31(tt()) -> tt()
      U42(tt()) -> tt()
      U51(tt(),V2) -> U52(isList(activate(V2)))
      U52(tt()) -> tt()
      U61(tt()) -> tt()
      U71(tt(),P) -> U72(isPal(activate(P)))
      U72(tt()) -> tt()
      U81(tt()) -> tt()
      isNeList(V) -> U31(isQid(activate(V)))
      isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
      isQid(n__e()) -> tt()
      nil() -> n__nil()
      activate(n__nil()) -> nil()
      activate(n____(X1,X2)) -> __(X1,X2)
      activate(n__a()) -> a()
      activate(n__e()) -> e()
      activate(n__i()) -> i()
      activate(n__o()) -> o()
      activate(n__u()) -> u()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [u] = 0,

       [o] = 8,

       [i] = 5,

       [e] = 9,

       [a] = 0,

       [n__u] = 3,

       [n__o] = 3,

       [n__i] = 0,

       [n__e] = 4,

       [n__a] = 12,

       [isNePal](x0) = x0 + 1,

       [isQid](x0) = x0,

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

       [n__nil] = 0,

       [U81](x0) = x0,

       [U72](x0) = x0,

       [isPal](x0) = x0 + 7,

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

       [U61](x0) = x0,

       [U52](x0) = x0 + 7,

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

       [U42](x0) = x0 + 6,

       [isNeList](x0) = x0 + 11,

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

       [U31](x0) = x0 + 6,

       [U22](x0) = x0,

       [isList](x0) = x0,

       [activate](x0) = x0 + 5,

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

       [U11](x0) = x0 + 13,

       [tt] = 4,

       [nil] = 0,

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

       U11(tt()) = 17 >= 4 = tt()

       U41(tt(),V2) = V2 + 5 >= V2 + 22 = U42(isNeList(activate(V2)))

       isList(V) = V >= V + 29 = U11(isNeList(activate(V)))

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

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

       isNeList(n____(V1,V2)) = V1 + V2 + 11 >= V1 + V2 + 31 = U51(isNeList(activate(V1)),activate(V2))

       isNePal(V) = V + 1 >= V + 5 = U61(isQid(activate(V)))

       isNePal(n____(I,__(P,I))) = 2I + P + 1 >= I + P + 18 = U71(isQid(activate(I)),activate(P))

       isPal(V) = V + 7 >= V + 6 = U81(isNePal(activate(V)))

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

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

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

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

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

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

       a() = 0 >= 12 = n__a()

       e() = 9 >= 4 = n__e()

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

       o() = 8 >= 3 = n__o()

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

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

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

       U21(tt(),V2) = V2 + 5 >= V2 + 5 = U22(isList(activate(V2)))

       U22(tt()) = 4 >= 4 = tt()

       U31(tt()) = 10 >= 4 = tt()

       U42(tt()) = 10 >= 4 = tt()

       U51(tt(),V2) = V2 + 14 >= V2 + 12 = U52(isList(activate(V2)))

       U52(tt()) = 11 >= 4 = tt()

       U61(tt()) = 4 >= 4 = tt()

       U71(tt(),P) = P + 12 >= P + 12 = U72(isPal(activate(P)))

       U72(tt()) = 4 >= 4 = tt()

       U81(tt()) = 4 >= 4 = tt()

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

       isNeList(n____(V1,V2)) = V1 + V2 + 11 >= V1 + V2 + 11 = U41(isList(activate(V1)),activate(V2))

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

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

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

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

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

       activate(n__e()) = 9 >= 9 = e()

       activate(n__i()) = 5 >= 5 = i()

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

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

       activate(X) = X + 5 >= X = X
      problem:
       strict:
        __(__(X,Y),Z) -> __(X,__(Y,Z))
        U41(tt(),V2) -> U42(isNeList(activate(V2)))
        isList(V) -> U11(isNeList(activate(V)))
        isList(n__nil()) -> tt()
        isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
        isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
        isNePal(V) -> U61(isQid(activate(V)))
        isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
        isQid(n__i()) -> tt()
        isQid(n__o()) -> tt()
        isQid(n__u()) -> tt()
        __(X1,X2) -> n____(X1,X2)
        a() -> n__a()
        u() -> n__u()
       weak:
        U11(tt()) -> tt()
        isPal(V) -> U81(isNePal(activate(V)))
        isPal(n__nil()) -> tt()
        isQid(n__a()) -> tt()
        e() -> n__e()
        i() -> n__i()
        o() -> n__o()
        __(X,nil()) -> X
        __(nil(),X) -> X
        U21(tt(),V2) -> U22(isList(activate(V2)))
        U22(tt()) -> tt()
        U31(tt()) -> tt()
        U42(tt()) -> tt()
        U51(tt(),V2) -> U52(isList(activate(V2)))
        U52(tt()) -> tt()
        U61(tt()) -> tt()
        U71(tt(),P) -> U72(isPal(activate(P)))
        U72(tt()) -> tt()
        U81(tt()) -> tt()
        isNeList(V) -> U31(isQid(activate(V)))
        isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
        isQid(n__e()) -> tt()
        nil() -> n__nil()
        activate(n__nil()) -> nil()
        activate(n____(X1,X2)) -> __(X1,X2)
        activate(n__a()) -> a()
        activate(n__e()) -> e()
        activate(n__i()) -> i()
        activate(n__o()) -> o()
        activate(n__u()) -> u()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [u] = 0,

         [o] = 2,

         [i] = 0,

         [e] = 17,

         [a] = 12,

         [n__u] = 11,

         [n__o] = 2,

         [n__i] = 0,

         [n__e] = 17,

         [n__a] = 12,

         [isNePal](x0) = x0,

         [isQid](x0) = x0,

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

         [n__nil] = 0,

         [U81](x0) = x0 + 21,

         [U72](x0) = x0 + 1,

         [isPal](x0) = x0 + 21,

         [U71](x0, x1) = x0 + x1 + 11,

         [U61](x0) = x0,

         [U52](x0) = x0 + 18,

         [U51](x0, x1) = x0 + x1 + 50,

         [U42](x0) = x0 + 24,

         [isNeList](x0) = x0 + 49,

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

         [U31](x0) = x0 + 49,

         [U22](x0) = x0,

         [isList](x0) = x0 + 12,

         [activate](x0) = x0,

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

         [U11](x0) = x0,

         [tt] = 12,

         [nil] = 0,

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

         U41(tt(),V2) = V2 + 28 >= V2 + 73 = U42(isNeList(activate(V2)))

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

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

         isList(n____(V1,V2)) = V1 + V2 + 62 >= V1 + V2 + 12 = U21(isList(activate(V1)),activate(V2))

         isNeList(n____(V1,V2)) = V1 + V2 + 99 >= V1 + V2 + 99 = U51(isNeList(activate(V1)),activate(V2))

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

         isNePal(n____(I,__(P,I))) = 2I + P + 98 >= I + P + 11 = U71(isQid(activate(I)),activate(P))

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

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

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

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

         a() = 12 >= 12 = n__a()

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

         U11(tt()) = 12 >= 12 = tt()

         isPal(V) = V + 21 >= V + 21 = U81(isNePal(activate(V)))

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

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

         e() = 17 >= 17 = n__e()

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

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

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

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

         U21(tt(),V2) = V2 + 12 >= V2 + 12 = U22(isList(activate(V2)))

         U22(tt()) = 12 >= 12 = tt()

         U31(tt()) = 61 >= 12 = tt()

         U42(tt()) = 36 >= 12 = tt()

         U51(tt(),V2) = V2 + 62 >= V2 + 30 = U52(isList(activate(V2)))

         U52(tt()) = 30 >= 12 = tt()

         U61(tt()) = 12 >= 12 = tt()

         U71(tt(),P) = P + 23 >= P + 22 = U72(isPal(activate(P)))

         U72(tt()) = 13 >= 12 = tt()

         U81(tt()) = 33 >= 12 = tt()

         isNeList(V) = V + 49 >= V + 49 = U31(isQid(activate(V)))

         isNeList(n____(V1,V2)) = V1 + V2 + 99 >= V1 + V2 + 28 = U41(isList(activate(V1)),activate(V2))

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

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

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

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

         activate(n__a()) = 12 >= 12 = a()

         activate(n__e()) = 17 >= 17 = e()

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

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

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

         activate(X) = X >= X = X
        problem:
         strict:
          __(__(X,Y),Z) -> __(X,__(Y,Z))
          U41(tt(),V2) -> U42(isNeList(activate(V2)))
          isList(V) -> U11(isNeList(activate(V)))
          isList(n__nil()) -> tt()
          isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
          isNePal(V) -> U61(isQid(activate(V)))
          isQid(n__i()) -> tt()
          isQid(n__o()) -> tt()
          isQid(n__u()) -> tt()
          __(X1,X2) -> n____(X1,X2)
          a() -> n__a()
          u() -> n__u()
         weak:
          isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
          isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
          U11(tt()) -> tt()
          isPal(V) -> U81(isNePal(activate(V)))
          isPal(n__nil()) -> tt()
          isQid(n__a()) -> tt()
          e() -> n__e()
          i() -> n__i()
          o() -> n__o()
          __(X,nil()) -> X
          __(nil(),X) -> X
          U21(tt(),V2) -> U22(isList(activate(V2)))
          U22(tt()) -> tt()
          U31(tt()) -> tt()
          U42(tt()) -> tt()
          U51(tt(),V2) -> U52(isList(activate(V2)))
          U52(tt()) -> tt()
          U61(tt()) -> tt()
          U71(tt(),P) -> U72(isPal(activate(P)))
          U72(tt()) -> tt()
          U81(tt()) -> tt()
          isNeList(V) -> U31(isQid(activate(V)))
          isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
          isQid(n__e()) -> tt()
          nil() -> n__nil()
          activate(n__nil()) -> nil()
          activate(n____(X1,X2)) -> __(X1,X2)
          activate(n__a()) -> a()
          activate(n__e()) -> e()
          activate(n__i()) -> i()
          activate(n__o()) -> o()
          activate(n__u()) -> u()
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [u] = 0,

           [o] = 20,

           [i] = 1,

           [e] = 18,

           [a] = 11,

           [n__u] = 0,

           [n__o] = 20,

           [n__i] = 1,

           [n__e] = 18,

           [n__a] = 11,

           [isNePal](x0) = x0 + 20,

           [isQid](x0) = x0 + 20,

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

           [n__nil] = 8,

           [U81](x0) = x0 + 3,

           [U72](x0) = x0,

           [isPal](x0) = x0 + 23,

           [U71](x0, x1) = x0 + x1 + 2,

           [U61](x0) = x0 + 3,

           [U52](x0) = x0 + 16,

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

           [U42](x0) = x0 + 8,

           [isNeList](x0) = x0 + 26,

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

           [U31](x0) = x0 + 6,

           [U22](x0) = x0 + 6,

           [isList](x0) = x0 + 10,

           [activate](x0) = x0,

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

           [U11](x0) = x0,

           [tt] = 31,

           [nil] = 8,

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

           U41(tt(),V2) = V2 + 48 >= V2 + 34 = U42(isNeList(activate(V2)))

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

           isList(n__nil()) = 18 >= 31 = tt()

           isNeList(n____(V1,V2)) = V1 + V2 + 27 >= V1 + V2 + 42 = U51(isNeList(activate(V1)),activate(V2))

           isNePal(V) = V + 20 >= V + 23 = U61(isQid(activate(V)))

           isQid(n__i()) = 21 >= 31 = tt()

           isQid(n__o()) = 40 >= 31 = tt()

           isQid(n__u()) = 20 >= 31 = tt()

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

           a() = 11 >= 11 = n__a()

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

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

           isNePal(n____(I,__(P,I))) = 2I + P + 22 >= I + P + 22 = U71(isQid(activate(I)),activate(P))

           U11(tt()) = 31 >= 31 = tt()

           isPal(V) = V + 23 >= V + 23 = U81(isNePal(activate(V)))

           isPal(n__nil()) = 31 >= 31 = tt()

           isQid(n__a()) = 31 >= 31 = tt()

           e() = 18 >= 18 = n__e()

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

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

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

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

           U21(tt(),V2) = V2 + 32 >= V2 + 16 = U22(isList(activate(V2)))

           U22(tt()) = 37 >= 31 = tt()

           U31(tt()) = 37 >= 31 = tt()

           U42(tt()) = 39 >= 31 = tt()

           U51(tt(),V2) = V2 + 47 >= V2 + 26 = U52(isList(activate(V2)))

           U52(tt()) = 47 >= 31 = tt()

           U61(tt()) = 34 >= 31 = tt()

           U71(tt(),P) = P + 33 >= P + 23 = U72(isPal(activate(P)))

           U72(tt()) = 31 >= 31 = tt()

           U81(tt()) = 34 >= 31 = tt()

           isNeList(V) = V + 26 >= V + 26 = U31(isQid(activate(V)))

           isNeList(n____(V1,V2)) = V1 + V2 + 27 >= V1 + V2 + 27 = U41(isList(activate(V1)),activate(V2))

           isQid(n__e()) = 38 >= 31 = tt()

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

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

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

           activate(n__a()) = 11 >= 11 = a()

           activate(n__e()) = 18 >= 18 = e()

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

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

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

           activate(X) = X >= X = X
          problem:
           strict:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            isList(V) -> U11(isNeList(activate(V)))
            isList(n__nil()) -> tt()
            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
            isNePal(V) -> U61(isQid(activate(V)))
            isQid(n__i()) -> tt()
            isQid(n__u()) -> tt()
            __(X1,X2) -> n____(X1,X2)
            a() -> n__a()
            u() -> n__u()
           weak:
            U41(tt(),V2) -> U42(isNeList(activate(V2)))
            isQid(n__o()) -> tt()
            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
            U11(tt()) -> tt()
            isPal(V) -> U81(isNePal(activate(V)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            e() -> n__e()
            i() -> n__i()
            o() -> n__o()
            __(X,nil()) -> X
            __(nil(),X) -> X
            U21(tt(),V2) -> U22(isList(activate(V2)))
            U22(tt()) -> tt()
            U31(tt()) -> tt()
            U42(tt()) -> tt()
            U51(tt(),V2) -> U52(isList(activate(V2)))
            U52(tt()) -> tt()
            U61(tt()) -> tt()
            U71(tt(),P) -> U72(isPal(activate(P)))
            U72(tt()) -> tt()
            U81(tt()) -> tt()
            isNeList(V) -> U31(isQid(activate(V)))
            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
            isQid(n__e()) -> tt()
            nil() -> n__nil()
            activate(n__nil()) -> nil()
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            activate(X) -> X
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [u] = 3,

             [o] = 4,

             [i] = 12,

             [e] = 4,

             [a] = 0,

             [n__u] = 2,

             [n__o] = 4,

             [n__i] = 12,

             [n__e] = 4,

             [n__a] = 4,

             [isNePal](x0) = x0 + 5,

             [isQid](x0) = x0 + 6,

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

             [n__nil] = 1,

             [U81](x0) = x0 + 3,

             [U72](x0) = x0,

             [isPal](x0) = x0 + 9,

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

             [U61](x0) = x0,

             [U52](x0) = x0,

             [U51](x0, x1) = x0 + x1 + 6,

             [U42](x0) = x0,

             [isNeList](x0) = x0 + 15,

             [U41](x0, x1) = x0 + x1 + 6,

             [U31](x0) = x0 + 8,

             [U22](x0) = x0,

             [isList](x0) = x0 + 9,

             [activate](x0) = x0 + 1,

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

             [U11](x0) = x0,

             [tt] = 10,

             [nil] = 2,

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

             isList(V) = V + 9 >= V + 16 = U11(isNeList(activate(V)))

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

             isNeList(n____(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 23 = U51(isNeList(activate(V1)),activate(V2))

             isNePal(V) = V + 5 >= V + 7 = U61(isQid(activate(V)))

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

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

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

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

             u() = 3 >= 2 = n__u()

             U41(tt(),V2) = V2 + 16 >= V2 + 16 = U42(isNeList(activate(V2)))

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

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

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

             U11(tt()) = 10 >= 10 = tt()

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

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

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

             e() = 4 >= 4 = n__e()

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

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

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

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

             U21(tt(),V2) = V2 + 10 >= V2 + 10 = U22(isList(activate(V2)))

             U22(tt()) = 10 >= 10 = tt()

             U31(tt()) = 18 >= 10 = tt()

             U42(tt()) = 10 >= 10 = tt()

             U51(tt(),V2) = V2 + 16 >= V2 + 10 = U52(isList(activate(V2)))

             U52(tt()) = 10 >= 10 = tt()

             U61(tt()) = 10 >= 10 = tt()

             U71(tt(),P) = P + 10 >= P + 10 = U72(isPal(activate(P)))

             U72(tt()) = 10 >= 10 = tt()

             U81(tt()) = 13 >= 10 = tt()

             isNeList(V) = V + 15 >= V + 15 = U31(isQid(activate(V)))

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

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

             nil() = 2 >= 1 = n__nil()

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

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

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

             activate(n__e()) = 5 >= 4 = e()

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

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

             activate(n__u()) = 3 >= 3 = u()

             activate(X) = X + 1 >= X = X
            problem:
             strict:
              __(__(X,Y),Z) -> __(X,__(Y,Z))
              isList(V) -> U11(isNeList(activate(V)))
              isList(n__nil()) -> tt()
              isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
              isNePal(V) -> U61(isQid(activate(V)))
              isQid(n__u()) -> tt()
              __(X1,X2) -> n____(X1,X2)
              a() -> n__a()
             weak:
              isQid(n__i()) -> tt()
              u() -> n__u()
              U41(tt(),V2) -> U42(isNeList(activate(V2)))
              isQid(n__o()) -> tt()
              isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
              isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
              U11(tt()) -> tt()
              isPal(V) -> U81(isNePal(activate(V)))
              isPal(n__nil()) -> tt()
              isQid(n__a()) -> tt()
              e() -> n__e()
              i() -> n__i()
              o() -> n__o()
              __(X,nil()) -> X
              __(nil(),X) -> X
              U21(tt(),V2) -> U22(isList(activate(V2)))
              U22(tt()) -> tt()
              U31(tt()) -> tt()
              U42(tt()) -> tt()
              U51(tt(),V2) -> U52(isList(activate(V2)))
              U52(tt()) -> tt()
              U61(tt()) -> tt()
              U71(tt(),P) -> U72(isPal(activate(P)))
              U72(tt()) -> tt()
              U81(tt()) -> tt()
              isNeList(V) -> U31(isQid(activate(V)))
              isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
              isQid(n__e()) -> tt()
              nil() -> n__nil()
              activate(n__nil()) -> nil()
              activate(n____(X1,X2)) -> __(X1,X2)
              activate(n__a()) -> a()
              activate(n__e()) -> e()
              activate(n__i()) -> i()
              activate(n__o()) -> o()
              activate(n__u()) -> u()
              activate(X) -> X
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [u] = 0,

               [o] = 7,

               [i] = 0,

               [e] = 0,

               [a] = 0,

               [n__u] = 0,

               [n__o] = 7,

               [n__i] = 0,

               [n__e] = 0,

               [n__a] = 0,

               [isNePal](x0) = x0 + 4,

               [isQid](x0) = x0 + 1,

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

               [n__nil] = 0,

               [U81](x0) = x0,

               [U72](x0) = x0,

               [isPal](x0) = x0 + 4,

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

               [U61](x0) = x0 + 7,

               [U52](x0) = x0 + 9,

               [U51](x0, x1) = x0 + x1 + 11,

               [U42](x0) = x0 + 7,

               [isNeList](x0) = x0 + 1,

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

               [U31](x0) = x0,

               [U22](x0) = x0,

               [isList](x0) = x0,

               [activate](x0) = x0,

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

               [U11](x0) = x0 + 5,

               [tt] = 1,

               [nil] = 0,

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

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

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

               isNeList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 12 = U51(isNeList(activate(V1)),activate(V2))

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

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

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

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

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

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

               U41(tt(),V2) = V2 + 8 >= V2 + 8 = U42(isNeList(activate(V2)))

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

               isList(n____(V1,V2)) = V1 + V2 + 13 >= V1 + V2 + 8 = U21(isList(activate(V1)),activate(V2))

               isNePal(n____(I,__(P,I))) = 2I + P + 24 >= I + P + 4 = U71(isQid(activate(I)),activate(P))

               U11(tt()) = 6 >= 1 = tt()

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

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

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

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

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

               o() = 7 >= 7 = n__o()

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

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

               U21(tt(),V2) = V2 + 9 >= V2 = U22(isList(activate(V2)))

               U22(tt()) = 1 >= 1 = tt()

               U31(tt()) = 1 >= 1 = tt()

               U42(tt()) = 8 >= 1 = tt()

               U51(tt(),V2) = V2 + 12 >= V2 + 9 = U52(isList(activate(V2)))

               U52(tt()) = 10 >= 1 = tt()

               U61(tt()) = 8 >= 1 = tt()

               U71(tt(),P) = P + 4 >= P + 4 = U72(isPal(activate(P)))

               U72(tt()) = 1 >= 1 = tt()

               U81(tt()) = 1 >= 1 = tt()

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

               isNeList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 7 = U41(isList(activate(V1)),activate(V2))

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

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

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

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

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

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

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

               activate(n__o()) = 7 >= 7 = o()

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

               activate(X) = X >= X = X
              problem:
               strict:
                __(__(X,Y),Z) -> __(X,__(Y,Z))
                isList(V) -> U11(isNeList(activate(V)))
                isList(n__nil()) -> tt()
                isNePal(V) -> U61(isQid(activate(V)))
                isQid(n__u()) -> tt()
                __(X1,X2) -> n____(X1,X2)
                a() -> n__a()
               weak:
                isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                isQid(n__i()) -> tt()
                u() -> n__u()
                U41(tt(),V2) -> U42(isNeList(activate(V2)))
                isQid(n__o()) -> tt()
                isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                U11(tt()) -> tt()
                isPal(V) -> U81(isNePal(activate(V)))
                isPal(n__nil()) -> tt()
                isQid(n__a()) -> tt()
                e() -> n__e()
                i() -> n__i()
                o() -> n__o()
                __(X,nil()) -> X
                __(nil(),X) -> X
                U21(tt(),V2) -> U22(isList(activate(V2)))
                U22(tt()) -> tt()
                U31(tt()) -> tt()
                U42(tt()) -> tt()
                U51(tt(),V2) -> U52(isList(activate(V2)))
                U52(tt()) -> tt()
                U61(tt()) -> tt()
                U71(tt(),P) -> U72(isPal(activate(P)))
                U72(tt()) -> tt()
                U81(tt()) -> tt()
                isNeList(V) -> U31(isQid(activate(V)))
                isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                isQid(n__e()) -> tt()
                nil() -> n__nil()
                activate(n__nil()) -> nil()
                activate(n____(X1,X2)) -> __(X1,X2)
                activate(n__a()) -> a()
                activate(n__e()) -> e()
                activate(n__i()) -> i()
                activate(n__o()) -> o()
                activate(n__u()) -> u()
                activate(X) -> X
              Matrix Interpretation Processor:
               dimension: 1
               max_matrix:
                1
                interpretation:
                 [u] = 1,

                 [o] = 0,

                 [i] = 7,

                 [e] = 16,

                 [a] = 0,

                 [n__u] = 1,

                 [n__o] = 0,

                 [n__i] = 7,

                 [n__e] = 16,

                 [n__a] = 0,

                 [isNePal](x0) = x0,

                 [isQid](x0) = x0 + 2,

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

                 [n__nil] = 0,

                 [U81](x0) = x0,

                 [U72](x0) = x0 + 12,

                 [isPal](x0) = x0,

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

                 [U61](x0) = x0,

                 [U52](x0) = x0 + 1,

                 [U51](x0, x1) = x0 + x1 + 21,

                 [U42](x0) = x0 + 1,

                 [isNeList](x0) = x0 + 2,

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

                 [U31](x0) = x0,

                 [U22](x0) = x0,

                 [isList](x0) = x0 + 20,

                 [activate](x0) = x0,

                 [U21](x0, x1) = x0 + x1 + 21,

                 [U11](x0) = x0 + 31,

                 [tt] = 0,

                 [nil] = 0,

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

                 isList(V) = V + 20 >= V + 33 = U11(isNeList(activate(V)))

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

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

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

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

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

                 isNeList(n____(V1,V2)) = V1 + V2 + 23 >= V1 + V2 + 23 = U51(isNeList(activate(V1)),activate(V2))

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

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

                 U41(tt(),V2) = V2 + 3 >= V2 + 3 = U42(isNeList(activate(V2)))

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

                 isList(n____(V1,V2)) = V1 + V2 + 41 >= V1 + V2 + 41 = U21(isList(activate(V1)),activate(V2))

                 isNePal(n____(I,__(P,I))) = 2I + P + 22 >= I + P + 14 = U71(isQid(activate(I)),activate(P))

                 U11(tt()) = 31 >= 0 = tt()

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

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

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

                 e() = 16 >= 16 = n__e()

                 i() = 7 >= 7 = n__i()

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

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

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

                 U21(tt(),V2) = V2 + 21 >= V2 + 20 = U22(isList(activate(V2)))

                 U22(tt()) = 0 >= 0 = tt()

                 U31(tt()) = 0 >= 0 = tt()

                 U42(tt()) = 1 >= 0 = tt()

                 U51(tt(),V2) = V2 + 21 >= V2 + 21 = U52(isList(activate(V2)))

                 U52(tt()) = 1 >= 0 = tt()

                 U61(tt()) = 0 >= 0 = tt()

                 U71(tt(),P) = P + 12 >= P + 12 = U72(isPal(activate(P)))

                 U72(tt()) = 12 >= 0 = tt()

                 U81(tt()) = 0 >= 0 = tt()

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

                 isNeList(n____(V1,V2)) = V1 + V2 + 23 >= V1 + V2 + 23 = U41(isList(activate(V1)),activate(V2))

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

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

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

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

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

                 activate(n__e()) = 16 >= 16 = e()

                 activate(n__i()) = 7 >= 7 = i()

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

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

                 activate(X) = X >= X = X
                problem:
                 strict:
                  __(__(X,Y),Z) -> __(X,__(Y,Z))
                  isList(V) -> U11(isNeList(activate(V)))
                  isNePal(V) -> U61(isQid(activate(V)))
                  __(X1,X2) -> n____(X1,X2)
                  a() -> n__a()
                 weak:
                  isList(n__nil()) -> tt()
                  isQid(n__u()) -> tt()
                  isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                  isQid(n__i()) -> tt()
                  u() -> n__u()
                  U41(tt(),V2) -> U42(isNeList(activate(V2)))
                  isQid(n__o()) -> tt()
                  isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                  isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                  U11(tt()) -> tt()
                  isPal(V) -> U81(isNePal(activate(V)))
                  isPal(n__nil()) -> tt()
                  isQid(n__a()) -> tt()
                  e() -> n__e()
                  i() -> n__i()
                  o() -> n__o()
                  __(X,nil()) -> X
                  __(nil(),X) -> X
                  U21(tt(),V2) -> U22(isList(activate(V2)))
                  U22(tt()) -> tt()
                  U31(tt()) -> tt()
                  U42(tt()) -> tt()
                  U51(tt(),V2) -> U52(isList(activate(V2)))
                  U52(tt()) -> tt()
                  U61(tt()) -> tt()
                  U71(tt(),P) -> U72(isPal(activate(P)))
                  U72(tt()) -> tt()
                  U81(tt()) -> tt()
                  isNeList(V) -> U31(isQid(activate(V)))
                  isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                  isQid(n__e()) -> tt()
                  nil() -> n__nil()
                  activate(n__nil()) -> nil()
                  activate(n____(X1,X2)) -> __(X1,X2)
                  activate(n__a()) -> a()
                  activate(n__e()) -> e()
                  activate(n__i()) -> i()
                  activate(n__o()) -> o()
                  activate(n__u()) -> u()
                  activate(X) -> X
                Matrix Interpretation Processor:
                 dimension: 1
                 max_matrix:
                  1
                  interpretation:
                   [u] = 3,

                   [o] = 4,

                   [i] = 4,

                   [e] = 12,

                   [a] = 0,

                   [n__u] = 3,

                   [n__o] = 3,

                   [n__i] = 3,

                   [n__e] = 10,

                   [n__a] = 8,

                   [isNePal](x0) = x0 + 7,

                   [isQid](x0) = x0 + 5,

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

                   [n__nil] = 7,

                   [U81](x0) = x0 + 1,

                   [U72](x0) = x0 + 4,

                   [isPal](x0) = x0 + 10,

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

                   [U61](x0) = x0 + 8,

                   [U52](x0) = x0 + 1,

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

                   [U42](x0) = x0 + 3,

                   [isNeList](x0) = x0 + 15,

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

                   [U31](x0) = x0 + 8,

                   [U22](x0) = x0 + 4,

                   [isList](x0) = x0 + 1,

                   [activate](x0) = x0 + 2,

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

                   [U11](x0) = x0,

                   [tt] = 8,

                   [nil] = 8,

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

                   isList(V) = V + 1 >= V + 17 = U11(isNeList(activate(V)))

                   isNePal(V) = V + 7 >= V + 15 = U61(isQid(activate(V)))

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

                   a() = 0 >= 8 = n__a()

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

                   isQid(n__u()) = 8 >= 8 = tt()

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

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

                   u() = 3 >= 3 = n__u()

                   U41(tt(),V2) = V2 + 20 >= V2 + 20 = U42(isNeList(activate(V2)))

                   isQid(n__o()) = 8 >= 8 = tt()

                   isList(n____(V1,V2)) = V1 + V2 + 5 >= V1 + V2 + 5 = U21(isList(activate(V1)),activate(V2))

                   isNePal(n____(I,__(P,I))) = 2I + P + 17 >= I + P + 17 = U71(isQid(activate(I)),activate(P))

                   U11(tt()) = 8 >= 8 = tt()

                   isPal(V) = V + 10 >= V + 10 = U81(isNePal(activate(V)))

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

                   isQid(n__a()) = 13 >= 8 = tt()

                   e() = 12 >= 10 = n__e()

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

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

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

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

                   U21(tt(),V2) = V2 + 8 >= V2 + 7 = U22(isList(activate(V2)))

                   U22(tt()) = 12 >= 8 = tt()

                   U31(tt()) = 16 >= 8 = tt()

                   U42(tt()) = 11 >= 8 = tt()

                   U51(tt(),V2) = V2 + 8 >= V2 + 4 = U52(isList(activate(V2)))

                   U52(tt()) = 9 >= 8 = tt()

                   U61(tt()) = 16 >= 8 = tt()

                   U71(tt(),P) = P + 16 >= P + 16 = U72(isPal(activate(P)))

                   U72(tt()) = 12 >= 8 = tt()

                   U81(tt()) = 9 >= 8 = tt()

                   isNeList(V) = V + 15 >= V + 15 = U31(isQid(activate(V)))

                   isNeList(n____(V1,V2)) = V1 + V2 + 19 >= V1 + V2 + 17 = U41(isList(activate(V1)),activate(V2))

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

                   nil() = 8 >= 7 = n__nil()

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

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

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

                   activate(n__e()) = 12 >= 12 = e()

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

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

                   activate(n__u()) = 5 >= 3 = u()

                   activate(X) = X + 2 >= X = X
                  problem:
                   strict:
                    __(__(X,Y),Z) -> __(X,__(Y,Z))
                    isList(V) -> U11(isNeList(activate(V)))
                    isNePal(V) -> U61(isQid(activate(V)))
                    a() -> n__a()
                   weak:
                    __(X1,X2) -> n____(X1,X2)
                    isList(n__nil()) -> tt()
                    isQid(n__u()) -> tt()
                    isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                    isQid(n__i()) -> tt()
                    u() -> n__u()
                    U41(tt(),V2) -> U42(isNeList(activate(V2)))
                    isQid(n__o()) -> tt()
                    isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                    isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                    U11(tt()) -> tt()
                    isPal(V) -> U81(isNePal(activate(V)))
                    isPal(n__nil()) -> tt()
                    isQid(n__a()) -> tt()
                    e() -> n__e()
                    i() -> n__i()
                    o() -> n__o()
                    __(X,nil()) -> X
                    __(nil(),X) -> X
                    U21(tt(),V2) -> U22(isList(activate(V2)))
                    U22(tt()) -> tt()
                    U31(tt()) -> tt()
                    U42(tt()) -> tt()
                    U51(tt(),V2) -> U52(isList(activate(V2)))
                    U52(tt()) -> tt()
                    U61(tt()) -> tt()
                    U71(tt(),P) -> U72(isPal(activate(P)))
                    U72(tt()) -> tt()
                    U81(tt()) -> tt()
                    isNeList(V) -> U31(isQid(activate(V)))
                    isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                    isQid(n__e()) -> tt()
                    nil() -> n__nil()
                    activate(n__nil()) -> nil()
                    activate(n____(X1,X2)) -> __(X1,X2)
                    activate(n__a()) -> a()
                    activate(n__e()) -> e()
                    activate(n__i()) -> i()
                    activate(n__o()) -> o()
                    activate(n__u()) -> u()
                    activate(X) -> X
                  Matrix Interpretation Processor:
                   dimension: 1
                   max_matrix:
                    1
                    interpretation:
                     [u] = 9,

                     [o] = 1,

                     [i] = 8,

                     [e] = 0,

                     [a] = 0,

                     [n__u] = 9,

                     [n__o] = 1,

                     [n__i] = 8,

                     [n__e] = 0,

                     [n__a] = 8,

                     [isNePal](x0) = x0,

                     [isQid](x0) = x0 + 1,

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

                     [n__nil] = 14,

                     [U81](x0) = x0 + 4,

                     [U72](x0) = x0,

                     [isPal](x0) = x0 + 4,

                     [U71](x0, x1) = x0 + x1 + 5,

                     [U61](x0) = x0 + 6,

                     [U52](x0) = x0 + 1,

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

                     [U42](x0) = x0 + 1,

                     [isNeList](x0) = x0 + 1,

                     [U41](x0, x1) = x0 + x1 + 2,

                     [U31](x0) = x0,

                     [U22](x0) = x0,

                     [isList](x0) = x0 + 2,

                     [activate](x0) = x0,

                     [U21](x0, x1) = x0 + x1 + 2,

                     [U11](x0) = x0,

                     [tt] = 0,

                     [nil] = 14,

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

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

                     isNePal(V) = V >= V + 7 = U61(isQid(activate(V)))

                     a() = 0 >= 8 = n__a()

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

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

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

                     isNeList(n____(V1,V2)) = V1 + V2 + 4 >= V1 + V2 + 4 = U51(isNeList(activate(V1)),activate(V2))

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

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

                     U41(tt(),V2) = V2 + 2 >= V2 + 2 = U42(isNeList(activate(V2)))

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

                     isList(n____(V1,V2)) = V1 + V2 + 5 >= V1 + V2 + 4 = U21(isList(activate(V1)),activate(V2))

                     isNePal(n____(I,__(P,I))) = 2I + P + 6 >= I + P + 6 = U71(isQid(activate(I)),activate(P))

                     U11(tt()) = 0 >= 0 = tt()

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

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

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

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

                     i() = 8 >= 8 = n__i()

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

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

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

                     U21(tt(),V2) = V2 + 2 >= V2 + 2 = U22(isList(activate(V2)))

                     U22(tt()) = 0 >= 0 = tt()

                     U31(tt()) = 0 >= 0 = tt()

                     U42(tt()) = 1 >= 0 = tt()

                     U51(tt(),V2) = V2 + 3 >= V2 + 3 = U52(isList(activate(V2)))

                     U52(tt()) = 1 >= 0 = tt()

                     U61(tt()) = 6 >= 0 = tt()

                     U71(tt(),P) = P + 5 >= P + 4 = U72(isPal(activate(P)))

                     U72(tt()) = 0 >= 0 = tt()

                     U81(tt()) = 4 >= 0 = tt()

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

                     isNeList(n____(V1,V2)) = V1 + V2 + 4 >= V1 + V2 + 4 = U41(isList(activate(V1)),activate(V2))

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

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

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

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

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

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

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

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

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

                     activate(X) = X >= X = X
                    problem:
                     strict:
                      __(__(X,Y),Z) -> __(X,__(Y,Z))
                      isNePal(V) -> U61(isQid(activate(V)))
                      a() -> n__a()
                     weak:
                      isList(V) -> U11(isNeList(activate(V)))
                      __(X1,X2) -> n____(X1,X2)
                      isList(n__nil()) -> tt()
                      isQid(n__u()) -> tt()
                      isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                      isQid(n__i()) -> tt()
                      u() -> n__u()
                      U41(tt(),V2) -> U42(isNeList(activate(V2)))
                      isQid(n__o()) -> tt()
                      isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                      isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                      U11(tt()) -> tt()
                      isPal(V) -> U81(isNePal(activate(V)))
                      isPal(n__nil()) -> tt()
                      isQid(n__a()) -> tt()
                      e() -> n__e()
                      i() -> n__i()
                      o() -> n__o()
                      __(X,nil()) -> X
                      __(nil(),X) -> X
                      U21(tt(),V2) -> U22(isList(activate(V2)))
                      U22(tt()) -> tt()
                      U31(tt()) -> tt()
                      U42(tt()) -> tt()
                      U51(tt(),V2) -> U52(isList(activate(V2)))
                      U52(tt()) -> tt()
                      U61(tt()) -> tt()
                      U71(tt(),P) -> U72(isPal(activate(P)))
                      U72(tt()) -> tt()
                      U81(tt()) -> tt()
                      isNeList(V) -> U31(isQid(activate(V)))
                      isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                      isQid(n__e()) -> tt()
                      nil() -> n__nil()
                      activate(n__nil()) -> nil()
                      activate(n____(X1,X2)) -> __(X1,X2)
                      activate(n__a()) -> a()
                      activate(n__e()) -> e()
                      activate(n__i()) -> i()
                      activate(n__o()) -> o()
                      activate(n__u()) -> u()
                      activate(X) -> X
                    Matrix Interpretation Processor:
                     dimension: 1
                     max_matrix:
                      1
                      interpretation:
                       [u] = 0,

                       [o] = 0,

                       [i] = 0,

                       [e] = 5,

                       [a] = 7,

                       [n__u] = 0,

                       [n__o] = 0,

                       [n__i] = 0,

                       [n__e] = 5,

                       [n__a] = 7,

                       [isNePal](x0) = x0 + 1,

                       [isQid](x0) = x0,

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

                       [n__nil] = 5,

                       [U81](x0) = x0,

                       [U72](x0) = x0,

                       [isPal](x0) = x0 + 4,

                       [U71](x0, x1) = x0 + x1 + 4,

                       [U61](x0) = x0,

                       [U52](x0) = x0,

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

                       [U42](x0) = x0 + 3,

                       [isNeList](x0) = x0 + 1,

                       [U41](x0, x1) = x0 + x1 + 4,

                       [U31](x0) = x0,

                       [U22](x0) = x0 + 1,

                       [isList](x0) = x0 + 1,

                       [activate](x0) = x0,

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

                       [U11](x0) = x0,

                       [tt] = 0,

                       [nil] = 5,

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

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

                       a() = 7 >= 7 = n__a()

                       isList(V) = V + 1 >= V + 1 = U11(isNeList(activate(V)))

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

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

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

                       isNeList(n____(V1,V2)) = V1 + V2 + 16 >= V1 + V2 + 2 = U51(isNeList(activate(V1)),activate(V2))

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

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

                       U41(tt(),V2) = V2 + 4 >= V2 + 4 = U42(isNeList(activate(V2)))

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

                       isList(n____(V1,V2)) = V1 + V2 + 16 >= V1 + V2 + 4 = U21(isList(activate(V1)),activate(V2))

                       isNePal(n____(I,__(P,I))) = 2I + P + 31 >= I + P + 4 = U71(isQid(activate(I)),activate(P))

                       U11(tt()) = 0 >= 0 = tt()

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

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

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

                       e() = 5 >= 5 = n__e()

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

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

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

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

                       U21(tt(),V2) = V2 + 3 >= V2 + 2 = U22(isList(activate(V2)))

                       U22(tt()) = 1 >= 0 = tt()

                       U31(tt()) = 0 >= 0 = tt()

                       U42(tt()) = 3 >= 0 = tt()

                       U51(tt(),V2) = V2 + 1 >= V2 + 1 = U52(isList(activate(V2)))

                       U52(tt()) = 0 >= 0 = tt()

                       U61(tt()) = 0 >= 0 = tt()

                       U71(tt(),P) = P + 4 >= P + 4 = U72(isPal(activate(P)))

                       U72(tt()) = 0 >= 0 = tt()

                       U81(tt()) = 0 >= 0 = tt()

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

                       isNeList(n____(V1,V2)) = V1 + V2 + 16 >= V1 + V2 + 5 = U41(isList(activate(V1)),activate(V2))

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

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

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

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

                       activate(n__a()) = 7 >= 7 = a()

                       activate(n__e()) = 5 >= 5 = e()

                       activate(n__i()) = 0 >= 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))
                        a() -> n__a()
                       weak:
                        isNePal(V) -> U61(isQid(activate(V)))
                        isList(V) -> U11(isNeList(activate(V)))
                        __(X1,X2) -> n____(X1,X2)
                        isList(n__nil()) -> tt()
                        isQid(n__u()) -> tt()
                        isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                        isQid(n__i()) -> tt()
                        u() -> n__u()
                        U41(tt(),V2) -> U42(isNeList(activate(V2)))
                        isQid(n__o()) -> tt()
                        isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                        isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                        U11(tt()) -> tt()
                        isPal(V) -> U81(isNePal(activate(V)))
                        isPal(n__nil()) -> tt()
                        isQid(n__a()) -> tt()
                        e() -> n__e()
                        i() -> n__i()
                        o() -> n__o()
                        __(X,nil()) -> X
                        __(nil(),X) -> X
                        U21(tt(),V2) -> U22(isList(activate(V2)))
                        U22(tt()) -> tt()
                        U31(tt()) -> tt()
                        U42(tt()) -> tt()
                        U51(tt(),V2) -> U52(isList(activate(V2)))
                        U52(tt()) -> tt()
                        U61(tt()) -> tt()
                        U71(tt(),P) -> U72(isPal(activate(P)))
                        U72(tt()) -> tt()
                        U81(tt()) -> tt()
                        isNeList(V) -> U31(isQid(activate(V)))
                        isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                        isQid(n__e()) -> tt()
                        nil() -> n__nil()
                        activate(n__nil()) -> nil()
                        activate(n____(X1,X2)) -> __(X1,X2)
                        activate(n__a()) -> a()
                        activate(n__e()) -> e()
                        activate(n__i()) -> i()
                        activate(n__o()) -> o()
                        activate(n__u()) -> u()
                        activate(X) -> X
                      Matrix Interpretation Processor:
                       dimension: 1
                       max_matrix:
                        1
                        interpretation:
                         [u] = 12,

                         [o] = 15,

                         [i] = 12,

                         [e] = 12,

                         [a] = 15,

                         [n__u] = 12,

                         [n__o] = 15,

                         [n__i] = 12,

                         [n__e] = 12,

                         [n__a] = 14,

                         [isNePal](x0) = x0 + 3,

                         [isQid](x0) = x0 + 2,

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

                         [n__nil] = 5,

                         [U81](x0) = x0 + 6,

                         [U72](x0) = x0 + 3,

                         [isPal](x0) = x0 + 10,

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

                         [U61](x0) = x0,

                         [U52](x0) = x0 + 1,

                         [U51](x0, x1) = x0 + x1 + 4,

                         [U42](x0) = x0 + 6,

                         [isNeList](x0) = x0 + 8,

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

                         [U31](x0) = x0 + 2,

                         [U22](x0) = x0 + 2,

                         [isList](x0) = x0 + 12,

                         [activate](x0) = x0 + 1,

                         [U21](x0, x1) = x0 + x1 + 5,

                         [U11](x0) = x0 + 3,

                         [tt] = 14,

                         [nil] = 6,

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

                         a() = 15 >= 14 = n__a()

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

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

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

                         isList(n__nil()) = 17 >= 14 = tt()

                         isQid(n__u()) = 14 >= 14 = tt()

                         isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 14 = U51(isNeList(activate(V1)),activate(V2))

                         isQid(n__i()) = 14 >= 14 = tt()

                         u() = 12 >= 12 = n__u()

                         U41(tt(),V2) = V2 + 15 >= V2 + 15 = U42(isNeList(activate(V2)))

                         isQid(n__o()) = 17 >= 14 = tt()

                         isList(n____(V1,V2)) = V1 + V2 + 19 >= V1 + V2 + 19 = U21(isList(activate(V1)),activate(V2))

                         isNePal(n____(I,__(P,I))) = 2I + P + 18 >= I + P + 4 = U71(isQid(activate(I)),activate(P))

                         U11(tt()) = 17 >= 14 = tt()

                         isPal(V) = V + 10 >= V + 10 = U81(isNePal(activate(V)))

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

                         isQid(n__a()) = 16 >= 14 = tt()

                         e() = 12 >= 12 = n__e()

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

                         o() = 15 >= 15 = n__o()

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

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

                         U21(tt(),V2) = V2 + 19 >= V2 + 15 = U22(isList(activate(V2)))

                         U22(tt()) = 16 >= 14 = tt()

                         U31(tt()) = 16 >= 14 = tt()

                         U42(tt()) = 20 >= 14 = tt()

                         U51(tt(),V2) = V2 + 18 >= V2 + 14 = U52(isList(activate(V2)))

                         U52(tt()) = 15 >= 14 = tt()

                         U61(tt()) = 14 >= 14 = tt()

                         U71(tt(),P) = P + 14 >= P + 14 = U72(isPal(activate(P)))

                         U72(tt()) = 17 >= 14 = tt()

                         U81(tt()) = 20 >= 14 = tt()

                         isNeList(V) = V + 8 >= V + 5 = U31(isQid(activate(V)))

                         isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 15 = U41(isList(activate(V1)),activate(V2))

                         isQid(n__e()) = 14 >= 14 = tt()

                         nil() = 6 >= 5 = n__nil()

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

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

                         activate(n__a()) = 15 >= 15 = a()

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

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

                         activate(n__o()) = 16 >= 15 = o()

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

                         activate(X) = X + 1 >= X = X
                        problem:
                         strict:
                          __(__(X,Y),Z) -> __(X,__(Y,Z))
                         weak:
                          a() -> n__a()
                          isNePal(V) -> U61(isQid(activate(V)))
                          isList(V) -> U11(isNeList(activate(V)))
                          __(X1,X2) -> n____(X1,X2)
                          isList(n__nil()) -> tt()
                          isQid(n__u()) -> tt()
                          isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                          isQid(n__i()) -> tt()
                          u() -> n__u()
                          U41(tt(),V2) -> U42(isNeList(activate(V2)))
                          isQid(n__o()) -> tt()
                          isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                          isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                          U11(tt()) -> tt()
                          isPal(V) -> U81(isNePal(activate(V)))
                          isPal(n__nil()) -> tt()
                          isQid(n__a()) -> tt()
                          e() -> n__e()
                          i() -> n__i()
                          o() -> n__o()
                          __(X,nil()) -> X
                          __(nil(),X) -> X
                          U21(tt(),V2) -> U22(isList(activate(V2)))
                          U22(tt()) -> tt()
                          U31(tt()) -> tt()
                          U42(tt()) -> tt()
                          U51(tt(),V2) -> U52(isList(activate(V2)))
                          U52(tt()) -> tt()
                          U61(tt()) -> tt()
                          U71(tt(),P) -> U72(isPal(activate(P)))
                          U72(tt()) -> tt()
                          U81(tt()) -> tt()
                          isNeList(V) -> U31(isQid(activate(V)))
                          isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                          isQid(n__e()) -> tt()
                          nil() -> n__nil()
                          activate(n__nil()) -> nil()
                          activate(n____(X1,X2)) -> __(X1,X2)
                          activate(n__a()) -> a()
                          activate(n__e()) -> e()
                          activate(n__i()) -> i()
                          activate(n__o()) -> o()
                          activate(n__u()) -> u()
                          activate(X) -> X
                        Matrix Interpretation Processor:
                         dimension: 2
                         max_matrix:
                          [1 2]
                          [0 1]
                          interpretation:
                                 [0]
                           [u] = [1],

                                 [0]
                           [o] = [0],

                                 [3]
                           [i] = [0],

                                 [0]
                           [e] = [0],

                                 [2]
                           [a] = [0],

                                    [0]
                           [n__u] = [1],

                                    [0]
                           [n__o] = [0],

                                    [3]
                           [n__i] = [0],

                                    [0]
                           [n__e] = [0],

                                    [2]
                           [n__a] = [0],

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

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

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

                                      [0]
                           [n__nil] = [0],

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

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

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

                                           [1 0]     [1 2]     [0]
                           [U71](x0, x1) = [0 0]x0 + [0 0]x1 + [1],

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

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

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

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

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

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

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

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

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


                           [activate](x0) = x0,

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

                                       [1 0]     [0]
                           [U11](x0) = [0 0]x0 + [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))

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

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

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

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

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

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

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

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

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

                                          [1 1]     [0]    [1 1]
                           U41(tt(),V2) = [0 0]V2 + [1] >= [0 0]V2 = U42(isNeList(activate(V2)))

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

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

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

                                       [0]    [0]
                           U11(tt()) = [1] >= [0] = tt()

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

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

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

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

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

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

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

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

                                          [1 1]     [1]    [1 1]     [1]
                           U21(tt(),V2) = [0 0]V2 + [1] >= [0 0]V2 + [1] = U22(isList(activate(V2)))

                                       [1]    [0]
                           U22(tt()) = [1] >= [0] = tt()

                                       [0]    [0]
                           U31(tt()) = [1] >= [0] = tt()

                                       [0]    [0]
                           U42(tt()) = [0] >= [0] = tt()

                                          [1 1]     [1]    [1 1]
                           U51(tt(),V2) = [0 0]V2 + [1] >= [0 0]V2 = U52(isList(activate(V2)))

                                       [0]    [0]
                           U52(tt()) = [0] >= [0] = tt()

                                       [0]    [0]
                           U61(tt()) = [0] >= [0] = tt()

                                         [1 2]    [0]    [1 2]
                           U71(tt(),P) = [0 0]P + [1] >= [0 0]P = U72(isPal(activate(P)))

                                       [0]    [0]
                           U72(tt()) = [0] >= [0] = tt()

                                       [0]    [0]
                           U81(tt()) = [0] >= [0] = tt()

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

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

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

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

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

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

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

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

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

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


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

                           weak:
                            __(__(X,Y),Z) -> __(X,__(Y,Z))
                            a() -> n__a()
                            isNePal(V) -> U61(isQid(activate(V)))
                            isList(V) -> U11(isNeList(activate(V)))
                            __(X1,X2) -> n____(X1,X2)
                            isList(n__nil()) -> tt()
                            isQid(n__u()) -> tt()
                            isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
                            isQid(n__i()) -> tt()
                            u() -> n__u()
                            U41(tt(),V2) -> U42(isNeList(activate(V2)))
                            isQid(n__o()) -> tt()
                            isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
                            isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
                            U11(tt()) -> tt()
                            isPal(V) -> U81(isNePal(activate(V)))
                            isPal(n__nil()) -> tt()
                            isQid(n__a()) -> tt()
                            e() -> n__e()
                            i() -> n__i()
                            o() -> n__o()
                            __(X,nil()) -> X
                            __(nil(),X) -> X
                            U21(tt(),V2) -> U22(isList(activate(V2)))
                            U22(tt()) -> tt()
                            U31(tt()) -> tt()
                            U42(tt()) -> tt()
                            U51(tt(),V2) -> U52(isList(activate(V2)))
                            U52(tt()) -> tt()
                            U61(tt()) -> tt()
                            U71(tt(),P) -> U72(isPal(activate(P)))
                            U72(tt()) -> tt()
                            U81(tt()) -> tt()
                            isNeList(V) -> U31(isQid(activate(V)))
                            isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
                            isQid(n__e()) -> tt()
                            nil() -> n__nil()
                            activate(n__nil()) -> nil()
                            activate(n____(X1,X2)) -> __(X1,X2)
                            activate(n__a()) -> a()
                            activate(n__e()) -> e()
                            activate(n__i()) -> i()
                            activate(n__o()) -> o()
                            activate(n__u()) -> u()
                            activate(X) -> X
                          Qed

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nokinds-noand 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
     , U11(tt()) -> tt()
     , U21(tt(), V2) -> U22(isList(activate(V2)))
     , U22(tt()) -> tt()
     , U31(tt()) -> tt()
     , U41(tt(), V2) -> U42(isNeList(activate(V2)))
     , U42(tt()) -> tt()
     , U51(tt(), V2) -> U52(isList(activate(V2)))
     , U52(tt()) -> tt()
     , U61(tt()) -> tt()
     , U71(tt(), P) -> U72(isPal(activate(P)))
     , U72(tt()) -> tt()
     , U81(tt()) -> tt()
     , isList(V) -> U11(isNeList(activate(V)))
     , isList(n__nil()) -> tt()
     , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
     , isNeList(V) -> U31(isQid(activate(V)))
     , isNeList(n____(V1, V2)) ->
       U41(isList(activate(V1)), activate(V2))
     , isNeList(n____(V1, V2)) ->
       U51(isNeList(activate(V1)), activate(V2))
     , isNePal(V) -> U61(isQid(activate(V)))
     , isNePal(n____(I, __(P, I))) ->
       U71(isQid(activate(I)), activate(P))
     , isPal(V) -> U81(isNePal(activate(V)))
     , isPal(n__nil()) -> tt()
     , isQid(n__a()) -> tt()
     , isQid(n__e()) -> tt()
     , isQid(n__i()) -> tt()
     , isQid(n__o()) -> tt()
     , isQid(n__u()) -> tt()
     , nil() -> n__nil()
     , __(X1, X2) -> n____(X1, X2)
     , a() -> n__a()
     , e() -> n__e()
     , i() -> n__i()
     , o() -> n__o()
     , u() -> n__u()
     , activate(n__nil()) -> nil()
     , activate(n____(X1, X2)) -> __(X1, X2)
     , activate(n__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-noand Z

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nokinds-noand 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
     , U11(tt()) -> tt()
     , U21(tt(), V2) -> U22(isList(activate(V2)))
     , U22(tt()) -> tt()
     , U31(tt()) -> tt()
     , U41(tt(), V2) -> U42(isNeList(activate(V2)))
     , U42(tt()) -> tt()
     , U51(tt(), V2) -> U52(isList(activate(V2)))
     , U52(tt()) -> tt()
     , U61(tt()) -> tt()
     , U71(tt(), P) -> U72(isPal(activate(P)))
     , U72(tt()) -> tt()
     , U81(tt()) -> tt()
     , isList(V) -> U11(isNeList(activate(V)))
     , isList(n__nil()) -> tt()
     , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
     , isNeList(V) -> U31(isQid(activate(V)))
     , isNeList(n____(V1, V2)) ->
       U41(isList(activate(V1)), activate(V2))
     , isNeList(n____(V1, V2)) ->
       U51(isNeList(activate(V1)), activate(V2))
     , isNePal(V) -> U61(isQid(activate(V)))
     , isNePal(n____(I, __(P, I))) ->
       U71(isQid(activate(I)), activate(P))
     , isPal(V) -> U81(isNePal(activate(V)))
     , isPal(n__nil()) -> tt()
     , isQid(n__a()) -> tt()
     , isQid(n__e()) -> tt()
     , isQid(n__i()) -> tt()
     , isQid(n__o()) -> tt()
     , isQid(n__u()) -> tt()
     , nil() -> n__nil()
     , __(X1, X2) -> n____(X1, X2)
     , a() -> n__a()
     , e() -> n__e()
     , i() -> n__i()
     , o() -> n__o()
     , u() -> n__u()
     , activate(n__nil()) -> nil()
     , activate(n____(X1, X2)) -> __(X1, X2)
     , activate(n__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