Problem Transformed CSR 04 PALINDROME nokinds GM

Tool CaT

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

stdout:

MAYBE

Problem:
a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
a____(X,nil()) -> mark(X)
a____(nil(),X) -> mark(X)
a__and(tt(),X) -> mark(X)
a__isList(V) -> a__isNeList(V)
a__isList(nil()) -> tt()
a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
a__isNeList(V) -> a__isQid(V)
a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
a__isNePal(V) -> a__isQid(V)
a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
a__isPal(V) -> a__isNePal(V)
a__isPal(nil()) -> tt()
a__isQid(a()) -> tt()
a__isQid(e()) -> tt()
a__isQid(i()) -> tt()
a__isQid(o()) -> tt()
a__isQid(u()) -> tt()
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isList(X)) -> a__isList(X)
mark(isNeList(X)) -> a__isNeList(X)
mark(isQid(X)) -> a__isQid(X)
mark(isNePal(X)) -> a__isNePal(X)
mark(isPal(X)) -> a__isPal(X)
mark(nil()) -> nil()
mark(tt()) -> tt()
mark(a()) -> a()
mark(e()) -> e()
mark(i()) -> i()
mark(o()) -> o()
mark(u()) -> u()
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isList(X) -> isList(X)
a__isNeList(X) -> isNeList(X)
a__isQid(X) -> isQid(X)
a__isNePal(X) -> isNePal(X)
a__isPal(X) -> isPal(X)

Proof:
Complexity Transformation Processor:
  strict:
   a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
   a____(X,nil()) -> mark(X)
   a____(nil(),X) -> mark(X)
   a__and(tt(),X) -> mark(X)
   a__isList(V) -> a__isNeList(V)
   a__isList(nil()) -> tt()
   a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
   a__isNeList(V) -> a__isQid(V)
   a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
   a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
   a__isNePal(V) -> a__isQid(V)
   a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
   a__isPal(V) -> a__isNePal(V)
   a__isPal(nil()) -> tt()
   a__isQid(a()) -> tt()
   a__isQid(e()) -> tt()
   a__isQid(i()) -> tt()
   a__isQid(o()) -> tt()
   a__isQid(u()) -> tt()
   mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
   mark(and(X1,X2)) -> a__and(mark(X1),X2)
   mark(isList(X)) -> a__isList(X)
   mark(isNeList(X)) -> a__isNeList(X)
   mark(isQid(X)) -> a__isQid(X)
   mark(isNePal(X)) -> a__isNePal(X)
   mark(isPal(X)) -> a__isPal(X)
   mark(nil()) -> nil()
   mark(tt()) -> tt()
   mark(a()) -> a()
   mark(e()) -> e()
   mark(i()) -> i()
   mark(o()) -> o()
   mark(u()) -> u()
   a____(X1,X2) -> __(X1,X2)
   a__and(X1,X2) -> and(X1,X2)
   a__isList(X) -> isList(X)
   a__isNeList(X) -> isNeList(X)
   a__isQid(X) -> isQid(X)
   a__isNePal(X) -> isNePal(X)
   a__isPal(X) -> isPal(X)
  weak:

  Matrix Interpretation Processor:
   dimension: 2
   max_matrix:
    [1 2]
    [0 0]
    interpretation:
                     [1 0]
     [isNePal](x0) = [0 0]x0,

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

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

           [2]
     [u] = [0],

           [2]
     [o] = [0],

           [2]
     [i] = [0],

           [1]
     [e] = [0],

           [0]
     [a] = [0],

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

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

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

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

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

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

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

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

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

            [0]
     [tt] = [0],

             [0]
     [nil] = [0],

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

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

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

                      [1 0]     [1 0]
     a____(X,nil()) = [0 0]X >= [0 0]X = mark(X)

                      [1 0]     [1 0]
     a____(nil(),X) = [0 0]X >= [0 0]X = mark(X)

                      [1 2]     [1 0]
     a__and(tt(),X) = [0 0]X >= [0 0]X = mark(X)

                    [1 0]     [1 0]
     a__isList(V) = [0 0]V >= [0 0]V = a__isNeList(V)

                        [0]    [0]
     a__isList(nil()) = [0] >= [0] = tt()

                            [1 0]     [1 0]      [1 0]     [1 0]
     a__isList(__(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = a__and(a__isList(V1),isList(V2))

                      [1 0]     [1 0]
     a__isNeList(V) = [0 0]V >= [0 0]V = a__isQid(V)

                              [1 0]     [1 0]      [1 0]     [1 0]
     a__isNeList(__(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = a__and(a__isList(V1),isNeList(V2))

                              [1 0]     [1 0]      [1 0]     [1 0]
     a__isNeList(__(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = a__and(a__isNeList(V1),isList(V2))

                     [1 0]     [1 0]
     a__isNePal(V) = [0 0]V >= [0 0]V = a__isQid(V)

                                 [2 0]    [1 0]     [1 0]    [1 0]
     a__isNePal(__(I,__(P,I))) = [0 0]I + [0 0]P >= [0 0]I + [0 0]P = a__and(a__isQid(I),isPal(P))

                   [1 0]     [1 0]
     a__isPal(V) = [0 0]V >= [0 0]V = a__isNePal(V)

                       [0]    [0]
     a__isPal(nil()) = [0] >= [0] = tt()

                     [0]    [0]
     a__isQid(a()) = [0] >= [0] = tt()

                     [1]    [0]
     a__isQid(e()) = [0] >= [0] = tt()

                     [2]    [0]
     a__isQid(i()) = [0] >= [0] = tt()

                     [2]    [0]
     a__isQid(o()) = [0] >= [0] = tt()

                     [2]    [0]
     a__isQid(u()) = [0] >= [0] = tt()

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

                        [1 2]     [1 2]      [1 0]     [1 2]
     mark(and(X1,X2)) = [0 0]X1 + [0 0]X2 >= [0 0]X1 + [0 0]X2 = a__and(mark(X1),X2)

                       [1 0]     [1 0]
     mark(isList(X)) = [0 0]X >= [0 0]X = a__isList(X)

                         [1 0]     [1 0]
     mark(isNeList(X)) = [0 0]X >= [0 0]X = a__isNeList(X)

                      [1 0]     [1 0]
     mark(isQid(X)) = [0 0]X >= [0 0]X = a__isQid(X)

                        [1 0]     [1 0]
     mark(isNePal(X)) = [0 0]X >= [0 0]X = a__isNePal(X)

                      [1 0]     [1 0]
     mark(isPal(X)) = [0 0]X >= [0 0]X = a__isPal(X)

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

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

                 [0]    [0]
     mark(a()) = [0] >= [0] = a()

                 [1]    [1]
     mark(e()) = [0] >= [0] = e()

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

                 [2]    [2]
     mark(o()) = [0] >= [0] = o()

                 [2]    [2]
     mark(u()) = [0] >= [0] = u()

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

                     [1 2]     [1 2]      [1 2]     [1 2]
     a__and(X1,X2) = [0 0]X1 + [0 0]X2 >= [0 0]X1 + [0 0]X2 = and(X1,X2)

                    [1 0]     [1 0]
     a__isList(X) = [0 0]X >= [0 0]X = isList(X)

                      [1 0]     [1 0]
     a__isNeList(X) = [0 0]X >= [0 0]X = isNeList(X)

                   [1 0]     [1 0]
     a__isQid(X) = [0 0]X >= [0 0]X = isQid(X)

                     [1 0]     [1 0]
     a__isNePal(X) = [0 0]X >= [0 0]X = isNePal(X)

                   [1 0]     [1 0]
     a__isPal(X) = [0 0]X >= [0 0]X = isPal(X)
    problem:
     strict:
      a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
      a____(X,nil()) -> mark(X)
      a____(nil(),X) -> mark(X)
      a__and(tt(),X) -> mark(X)
      a__isList(V) -> a__isNeList(V)
      a__isList(nil()) -> tt()
      a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
      a__isNeList(V) -> a__isQid(V)
      a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
      a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
      a__isNePal(V) -> a__isQid(V)
      a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
      a__isPal(V) -> a__isNePal(V)
      a__isPal(nil()) -> tt()
      a__isQid(a()) -> tt()
      mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
      mark(and(X1,X2)) -> a__and(mark(X1),X2)
      mark(isList(X)) -> a__isList(X)
      mark(isNeList(X)) -> a__isNeList(X)
      mark(isQid(X)) -> a__isQid(X)
      mark(isNePal(X)) -> a__isNePal(X)
      mark(isPal(X)) -> a__isPal(X)
      mark(nil()) -> nil()
      mark(tt()) -> tt()
      mark(a()) -> a()
      mark(e()) -> e()
      mark(i()) -> i()
      mark(o()) -> o()
      mark(u()) -> u()
      a____(X1,X2) -> __(X1,X2)
      a__and(X1,X2) -> and(X1,X2)
      a__isList(X) -> isList(X)
      a__isNeList(X) -> isNeList(X)
      a__isQid(X) -> isQid(X)
      a__isNePal(X) -> isNePal(X)
      a__isPal(X) -> isPal(X)
     weak:
      a__isQid(e()) -> tt()
      a__isQid(i()) -> tt()
      a__isQid(o()) -> tt()
      a__isQid(u()) -> tt()
    Matrix Interpretation Processor:
     dimension: 3
     max_matrix:
      [1 1 1]
      [0 0 0]
      [0 0 0]
      interpretation:
                       [1 0 0]     [1]
       [isNePal](x0) = [0 0 0]x0 + [0]
                       [0 0 0]     [0],

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

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

             [1]
       [u] = [0]
             [0],

             [0]
       [o] = [0]
             [0],

             [0]
       [i] = [0]
             [0],

             [1]
       [e] = [0]
             [0],

             [0]
       [a] = [0]
             [0],

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

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

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

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

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

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

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

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

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

              [0]
       [tt] = [0]
              [0],

               [1]
       [nil] = [0]
               [0],

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

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

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

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

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

                        [1 0 0]     [1 0 0]
       a__and(tt(),X) = [0 0 0]X >= [0 0 0]X = mark(X)
                        [0 0 0]     [0 0 0]

                      [1 0 0]     [1 0 0]
       a__isList(V) = [0 0 0]V >= [0 0 0]V = a__isNeList(V)
                      [0 0 0]     [0 0 0]

                          [1]    [0]
       a__isList(nil()) = [0] >= [0] = tt()
                          [0]    [0]

                              [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]
       a__isList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isList(V1),isList(V2))
                              [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                        [1 0 0]     [1 0 0]
       a__isNeList(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                        [0 0 0]     [0 0 0]

                                [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]
       a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isList(V1),isNeList(V2))
                                [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                                [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]
       a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isNeList(V1),isList(V2))
                                [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                       [1 0 0]    [1]    [1 0 0]
       a__isNePal(V) = [0 0 0]V + [0] >= [0 0 0]V = a__isQid(V)
                       [0 0 0]    [0]    [0 0 0]

                                   [2 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1]
       a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P + [0] >= [0 0 0]I + [0 0 0]P + [0] = a__and(a__isQid(I),isPal(P))
                                   [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]

                     [1 0 0]    [1]    [1 0 0]    [1]
       a__isPal(V) = [0 0 0]V + [0] >= [0 0 0]V + [0] = a__isNePal(V)
                     [0 0 0]    [0]    [0 0 0]    [0]

                         [2]    [0]
       a__isPal(nil()) = [0] >= [0] = tt()
                         [0]    [0]

                       [0]    [0]
       a__isQid(a()) = [0] >= [0] = tt()
                       [0]    [0]

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

                          [1 0 1]     [1 0 0]      [1 0 0]     [1 0 0]
       mark(and(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = a__and(mark(X1),X2)
                          [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                         [1 0 0]     [1 0 0]
       mark(isList(X)) = [0 0 0]X >= [0 0 0]X = a__isList(X)
                         [0 0 0]     [0 0 0]

                           [1 0 0]     [1 0 0]
       mark(isNeList(X)) = [0 0 0]X >= [0 0 0]X = a__isNeList(X)
                           [0 0 0]     [0 0 0]

                        [1 0 0]     [1 0 0]
       mark(isQid(X)) = [0 0 0]X >= [0 0 0]X = a__isQid(X)
                        [0 0 0]     [0 0 0]

                          [1 0 0]    [1]    [1 0 0]    [1]
       mark(isNePal(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__isNePal(X)
                          [0 0 0]    [0]    [0 0 0]    [0]

                        [1 0 0]    [1]    [1 0 0]    [1]
       mark(isPal(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__isPal(X)
                        [0 0 0]    [0]    [0 0 0]    [0]

                     [1]    [1]
       mark(nil()) = [0] >= [0] = nil()
                     [0]    [0]

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

                   [0]    [0]
       mark(a()) = [0] >= [0] = a()
                   [0]    [0]

                   [1]    [1]
       mark(e()) = [0] >= [0] = e()
                   [0]    [0]

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

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

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

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

                       [1 0 1]     [1 0 0]      [1 0 1]     [1 0 0]
       a__and(X1,X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = and(X1,X2)
                       [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                      [1 0 0]     [1 0 0]
       a__isList(X) = [0 0 0]X >= [0 0 0]X = isList(X)
                      [0 0 0]     [0 0 0]

                        [1 0 0]     [1 0 0]
       a__isNeList(X) = [0 0 0]X >= [0 0 0]X = isNeList(X)
                        [0 0 0]     [0 0 0]

                     [1 0 0]     [1 0 0]
       a__isQid(X) = [0 0 0]X >= [0 0 0]X = isQid(X)
                     [0 0 0]     [0 0 0]

                       [1 0 0]    [1]    [1 0 0]    [1]
       a__isNePal(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = isNePal(X)
                       [0 0 0]    [0]    [0 0 0]    [0]

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

                       [1]    [0]
       a__isQid(e()) = [0] >= [0] = tt()
                       [0]    [0]

                       [0]    [0]
       a__isQid(i()) = [0] >= [0] = tt()
                       [0]    [0]

                       [0]    [0]
       a__isQid(o()) = [0] >= [0] = tt()
                       [0]    [0]

                       [1]    [0]
       a__isQid(u()) = [0] >= [0] = tt()
                       [0]    [0]
      problem:
       strict:
        a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
        a__and(tt(),X) -> mark(X)
        a__isList(V) -> a__isNeList(V)
        a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
        a__isNeList(V) -> a__isQid(V)
        a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
        a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
        a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
        a__isPal(V) -> a__isNePal(V)
        a__isQid(a()) -> tt()
        mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
        mark(and(X1,X2)) -> a__and(mark(X1),X2)
        mark(isList(X)) -> a__isList(X)
        mark(isNeList(X)) -> a__isNeList(X)
        mark(isQid(X)) -> a__isQid(X)
        mark(isNePal(X)) -> a__isNePal(X)
        mark(isPal(X)) -> a__isPal(X)
        mark(nil()) -> nil()
        mark(tt()) -> tt()
        mark(a()) -> a()
        mark(e()) -> e()
        mark(i()) -> i()
        mark(o()) -> o()
        mark(u()) -> u()
        a____(X1,X2) -> __(X1,X2)
        a__and(X1,X2) -> and(X1,X2)
        a__isList(X) -> isList(X)
        a__isNeList(X) -> isNeList(X)
        a__isQid(X) -> isQid(X)
        a__isNePal(X) -> isNePal(X)
        a__isPal(X) -> isPal(X)
       weak:
        a____(X,nil()) -> mark(X)
        a____(nil(),X) -> mark(X)
        a__isList(nil()) -> tt()
        a__isNePal(V) -> a__isQid(V)
        a__isPal(nil()) -> tt()
        a__isQid(e()) -> tt()
        a__isQid(i()) -> tt()
        a__isQid(o()) -> tt()
        a__isQid(u()) -> tt()
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 0]
        interpretation:
                         [1 0]
         [isNePal](x0) = [0 0]x0,

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

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

               [0]
         [u] = [0],

               [1]
         [o] = [0],

               [2]
         [i] = [0],

               [0]
         [e] = [0],

               [1]
         [a] = [0],

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

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

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

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

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

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

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

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

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

                [0]
         [tt] = [0],

                 [1]
         [nil] = [0],

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

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

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

                          [1 0]     [1 0]
         a__and(tt(),X) = [0 0]X >= [0 0]X = mark(X)

                        [1 0]     [1 0]
         a__isList(V) = [0 0]V >= [0 0]V = a__isNeList(V)

                                [1 0]     [1 0]      [1 0]     [1 0]
         a__isList(__(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = a__and(a__isList(V1),isList(V2))

                          [1 0]     [1 0]
         a__isNeList(V) = [0 0]V >= [0 0]V = a__isQid(V)

                                  [1 0]     [1 0]      [1 0]     [1 0]
         a__isNeList(__(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = a__and(a__isList(V1),isNeList(V2))

                                  [1 0]     [1 0]      [1 0]     [1 0]
         a__isNeList(__(V1,V2)) = [0 0]V1 + [0 0]V2 >= [0 0]V1 + [0 0]V2 = a__and(a__isNeList(V1),isList(V2))

                                     [2 0]    [1 0]     [1 0]    [1 0]
         a__isNePal(__(I,__(P,I))) = [0 0]I + [0 0]P >= [0 0]I + [0 0]P = a__and(a__isQid(I),isPal(P))

                       [1 0]     [1 0]
         a__isPal(V) = [0 0]V >= [0 0]V = a__isNePal(V)

                         [1]    [0]
         a__isQid(a()) = [0] >= [0] = tt()

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

                            [1 1]     [1 0]      [1 0]     [1 0]
         mark(and(X1,X2)) = [0 0]X1 + [0 0]X2 >= [0 0]X1 + [0 0]X2 = a__and(mark(X1),X2)

                           [1 0]     [1 0]
         mark(isList(X)) = [0 0]X >= [0 0]X = a__isList(X)

                             [1 0]     [1 0]
         mark(isNeList(X)) = [0 0]X >= [0 0]X = a__isNeList(X)

                          [1 0]     [1 0]
         mark(isQid(X)) = [0 0]X >= [0 0]X = a__isQid(X)

                            [1 0]     [1 0]
         mark(isNePal(X)) = [0 0]X >= [0 0]X = a__isNePal(X)

                          [1 0]     [1 0]
         mark(isPal(X)) = [0 0]X >= [0 0]X = a__isPal(X)

                       [1]    [1]
         mark(nil()) = [0] >= [0] = nil()

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

                     [1]    [1]
         mark(a()) = [0] >= [0] = a()

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

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

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

                     [0]    [0]
         mark(u()) = [0] >= [0] = u()

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

                         [1 1]     [1 0]      [1 1]     [1 0]
         a__and(X1,X2) = [0 0]X1 + [0 0]X2 >= [0 0]X1 + [0 0]X2 = and(X1,X2)

                        [1 0]     [1 0]
         a__isList(X) = [0 0]X >= [0 0]X = isList(X)

                          [1 0]     [1 0]
         a__isNeList(X) = [0 0]X >= [0 0]X = isNeList(X)

                       [1 0]     [1 0]
         a__isQid(X) = [0 0]X >= [0 0]X = isQid(X)

                         [1 0]     [1 0]
         a__isNePal(X) = [0 0]X >= [0 0]X = isNePal(X)

                       [1 0]     [1 0]
         a__isPal(X) = [0 0]X >= [0 0]X = isPal(X)

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

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

                            [1]    [0]
         a__isList(nil()) = [0] >= [0] = tt()

                         [1 0]     [1 0]
         a__isNePal(V) = [0 0]V >= [0 0]V = a__isQid(V)

                           [1]    [0]
         a__isPal(nil()) = [0] >= [0] = tt()

                         [0]    [0]
         a__isQid(e()) = [0] >= [0] = tt()

                         [2]    [0]
         a__isQid(i()) = [0] >= [0] = tt()

                         [1]    [0]
         a__isQid(o()) = [0] >= [0] = tt()

                         [0]    [0]
         a__isQid(u()) = [0] >= [0] = tt()
        problem:
         strict:
          a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
          a__and(tt(),X) -> mark(X)
          a__isList(V) -> a__isNeList(V)
          a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
          a__isNeList(V) -> a__isQid(V)
          a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
          a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
          a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
          a__isPal(V) -> a__isNePal(V)
          mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
          mark(and(X1,X2)) -> a__and(mark(X1),X2)
          mark(isList(X)) -> a__isList(X)
          mark(isNeList(X)) -> a__isNeList(X)
          mark(isQid(X)) -> a__isQid(X)
          mark(isNePal(X)) -> a__isNePal(X)
          mark(isPal(X)) -> a__isPal(X)
          mark(nil()) -> nil()
          mark(tt()) -> tt()
          mark(a()) -> a()
          mark(e()) -> e()
          mark(i()) -> i()
          mark(o()) -> o()
          mark(u()) -> u()
          a____(X1,X2) -> __(X1,X2)
          a__and(X1,X2) -> and(X1,X2)
          a__isList(X) -> isList(X)
          a__isNeList(X) -> isNeList(X)
          a__isQid(X) -> isQid(X)
          a__isNePal(X) -> isNePal(X)
          a__isPal(X) -> isPal(X)
         weak:
          a__isQid(a()) -> tt()
          a____(X,nil()) -> mark(X)
          a____(nil(),X) -> mark(X)
          a__isList(nil()) -> tt()
          a__isNePal(V) -> a__isQid(V)
          a__isPal(nil()) -> tt()
          a__isQid(e()) -> tt()
          a__isQid(i()) -> tt()
          a__isQid(o()) -> tt()
          a__isQid(u()) -> tt()
        Matrix Interpretation Processor:
         dimension: 3
         max_matrix:
          [1 1 1]
          [0 0 1]
          [0 0 0]
          interpretation:
                           [1 0 0]
           [isNePal](x0) = [0 0 0]x0
                           [0 0 0]  ,

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

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

                 [1]
           [u] = [0]
                 [0],

                 [1]
           [o] = [0]
                 [0],

                 [1]
           [i] = [0]
                 [0],

                 [1]
           [e] = [0]
                 [0],

                 [1]
           [a] = [0]
                 [0],

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

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

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

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

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

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

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

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

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

                  [1]
           [tt] = [0]
                  [0],

                   [1]
           [nil] = [0]
                   [0],

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

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

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

                            [1 1 0]    [1]    [1 0 0]
           a__and(tt(),X) = [0 0 0]X + [0] >= [0 0 0]X = mark(X)
                            [0 0 0]    [0]    [0 0 0]

                          [1 0 0]     [1 0 0]
           a__isList(V) = [0 0 0]V >= [0 0 0]V = a__isNeList(V)
                          [0 0 0]     [0 0 0]

                                  [1 0 0]     [1 0 1]      [1 0 0]     [1 0 0]
           a__isList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isList(V1),isList(V2))
                                  [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                            [1 0 0]     [1 0 0]
           a__isNeList(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                            [0 0 0]     [0 0 0]

                                    [1 0 0]     [1 0 1]      [1 0 0]     [1 0 0]
           a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isList(V1),isNeList(V2))
                                    [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                                    [1 0 0]     [1 0 1]      [1 0 0]     [1 0 0]
           a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isNeList(V1),isList(V2))
                                    [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                                       [2 0 1]    [1 0 0]     [1 0 0]    [1 0 0]
           a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P >= [0 0 0]I + [0 0 0]P = a__and(a__isQid(I),isPal(P))
                                       [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]

                         [1 0 0]     [1 0 0]
           a__isPal(V) = [0 0 0]V >= [0 0 0]V = a__isNePal(V)
                         [0 0 0]     [0 0 0]

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

                              [1 0 0]     [1 1 0]      [1 0 0]     [1 1 0]
           mark(and(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = a__and(mark(X1),X2)
                              [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                             [1 0 0]     [1 0 0]
           mark(isList(X)) = [0 0 0]X >= [0 0 0]X = a__isList(X)
                             [0 0 0]     [0 0 0]

                               [1 0 0]     [1 0 0]
           mark(isNeList(X)) = [0 0 0]X >= [0 0 0]X = a__isNeList(X)
                               [0 0 0]     [0 0 0]

                            [1 0 0]     [1 0 0]
           mark(isQid(X)) = [0 0 0]X >= [0 0 0]X = a__isQid(X)
                            [0 0 0]     [0 0 0]

                              [1 0 0]     [1 0 0]
           mark(isNePal(X)) = [0 0 0]X >= [0 0 0]X = a__isNePal(X)
                              [0 0 0]     [0 0 0]

                            [1 0 0]     [1 0 0]
           mark(isPal(X)) = [0 0 0]X >= [0 0 0]X = a__isPal(X)
                            [0 0 0]     [0 0 0]

                         [1]    [1]
           mark(nil()) = [0] >= [0] = nil()
                         [0]    [0]

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

                       [1]    [1]
           mark(a()) = [0] >= [0] = a()
                       [0]    [0]

                       [1]    [1]
           mark(e()) = [0] >= [0] = e()
                       [0]    [0]

                       [1]    [1]
           mark(i()) = [0] >= [0] = i()
                       [0]    [0]

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

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

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

                           [1 0 0]     [1 1 0]      [1 0 0]     [1 1 0]
           a__and(X1,X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = and(X1,X2)
                           [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                          [1 0 0]     [1 0 0]
           a__isList(X) = [0 0 0]X >= [0 0 0]X = isList(X)
                          [0 0 0]     [0 0 0]

                            [1 0 0]     [1 0 0]
           a__isNeList(X) = [0 0 0]X >= [0 0 0]X = isNeList(X)
                            [0 0 0]     [0 0 0]

                         [1 0 0]     [1 0 0]
           a__isQid(X) = [0 0 0]X >= [0 0 0]X = isQid(X)
                         [0 0 0]     [0 0 0]

                           [1 0 0]     [1 0 0]
           a__isNePal(X) = [0 0 0]X >= [0 0 0]X = isNePal(X)
                           [0 0 0]     [0 0 0]

                         [1 0 0]     [1 0 0]
           a__isPal(X) = [0 0 0]X >= [0 0 0]X = isPal(X)
                         [0 0 0]     [0 0 0]

                           [1]    [1]
           a__isQid(a()) = [0] >= [0] = tt()
                           [0]    [0]

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

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

                              [1]    [1]
           a__isList(nil()) = [0] >= [0] = tt()
                              [0]    [0]

                           [1 0 0]     [1 0 0]
           a__isNePal(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                           [0 0 0]     [0 0 0]

                             [1]    [1]
           a__isPal(nil()) = [0] >= [0] = tt()
                             [0]    [0]

                           [1]    [1]
           a__isQid(e()) = [0] >= [0] = tt()
                           [0]    [0]

                           [1]    [1]
           a__isQid(i()) = [0] >= [0] = tt()
                           [0]    [0]

                           [1]    [1]
           a__isQid(o()) = [0] >= [0] = tt()
                           [0]    [0]

                           [1]    [1]
           a__isQid(u()) = [0] >= [0] = tt()
                           [0]    [0]
          problem:
           strict:
            a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
            a__isList(V) -> a__isNeList(V)
            a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
            a__isNeList(V) -> a__isQid(V)
            a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
            a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
            a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
            a__isPal(V) -> a__isNePal(V)
            mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
            mark(and(X1,X2)) -> a__and(mark(X1),X2)
            mark(isList(X)) -> a__isList(X)
            mark(isNeList(X)) -> a__isNeList(X)
            mark(isQid(X)) -> a__isQid(X)
            mark(isNePal(X)) -> a__isNePal(X)
            mark(isPal(X)) -> a__isPal(X)
            mark(nil()) -> nil()
            mark(tt()) -> tt()
            mark(a()) -> a()
            mark(e()) -> e()
            mark(i()) -> i()
            mark(o()) -> o()
            mark(u()) -> u()
            a____(X1,X2) -> __(X1,X2)
            a__and(X1,X2) -> and(X1,X2)
            a__isList(X) -> isList(X)
            a__isNeList(X) -> isNeList(X)
            a__isQid(X) -> isQid(X)
            a__isNePal(X) -> isNePal(X)
            a__isPal(X) -> isPal(X)
           weak:
            a__and(tt(),X) -> mark(X)
            a__isQid(a()) -> tt()
            a____(X,nil()) -> mark(X)
            a____(nil(),X) -> mark(X)
            a__isList(nil()) -> tt()
            a__isNePal(V) -> a__isQid(V)
            a__isPal(nil()) -> tt()
            a__isQid(e()) -> tt()
            a__isQid(i()) -> tt()
            a__isQid(o()) -> tt()
            a__isQid(u()) -> tt()
          Matrix Interpretation Processor:
           dimension: 3
           max_matrix:
            [1 1 1]
            [0 0 1]
            [0 0 0]
            interpretation:
                             [1 0 0]
             [isNePal](x0) = [0 0 0]x0
                             [0 0 0]  ,

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

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

                   [0]
             [u] = [0]
                   [0],

                   [1]
             [o] = [0]
                   [0],

                   [0]
             [i] = [0]
                   [0],

                   [0]
             [e] = [0]
                   [0],

                   [0]
             [a] = [0]
                   [0],

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

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

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

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

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

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

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

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

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

                    [0]
             [tt] = [0]
                    [0],

                     [0]
             [nil] = [0]
                     [0],

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

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

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

                            [1 0 0]     [1 0 0]
             a__isList(V) = [0 0 0]V >= [0 0 0]V = a__isNeList(V)
                            [0 0 0]     [0 0 0]

                                    [1 0 0]     [1 1 1]     [1]    [1 0 0]     [1 0 0]
             a__isList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isList(V1),isList(V2))
                                    [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]

                              [1 0 0]     [1 0 0]
             a__isNeList(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                              [0 0 0]     [0 0 0]

                                      [1 0 0]     [1 1 1]     [1]    [1 0 0]     [1 0 0]
             a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isList(V1),isNeList(V2))
                                      [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]

                                      [1 0 0]     [1 1 1]     [1]    [1 0 0]     [1 0 0]
             a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 = a__and(a__isNeList(V1),isList(V2))
                                      [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]

                                         [2 1 2]    [1 0 0]    [2]    [1 0 0]    [1 0 0]
             a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P + [0] >= [0 0 0]I + [0 0 0]P = a__and(a__isQid(I),isPal(P))
                                         [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]

                           [1 0 0]     [1 0 0]
             a__isPal(V) = [0 0 0]V >= [0 0 0]V = a__isNePal(V)
                           [0 0 0]     [0 0 0]

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

                                [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]
             mark(and(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = a__and(mark(X1),X2)
                                [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                               [1 0 0]     [1 0 0]
             mark(isList(X)) = [0 0 0]X >= [0 0 0]X = a__isList(X)
                               [0 0 0]     [0 0 0]

                                 [1 0 0]     [1 0 0]
             mark(isNeList(X)) = [0 0 0]X >= [0 0 0]X = a__isNeList(X)
                                 [0 0 0]     [0 0 0]

                              [1 0 0]     [1 0 0]
             mark(isQid(X)) = [0 0 0]X >= [0 0 0]X = a__isQid(X)
                              [0 0 0]     [0 0 0]

                                [1 0 0]     [1 0 0]
             mark(isNePal(X)) = [0 0 0]X >= [0 0 0]X = a__isNePal(X)
                                [0 0 0]     [0 0 0]

                              [1 0 0]     [1 0 0]
             mark(isPal(X)) = [0 0 0]X >= [0 0 0]X = a__isPal(X)
                              [0 0 0]     [0 0 0]

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

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

                         [0]    [0]
             mark(a()) = [0] >= [0] = a()
                         [0]    [0]

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

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

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

                         [0]    [0]
             mark(u()) = [0] >= [0] = u()
                         [0]    [0]

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

                             [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]
             a__and(X1,X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = and(X1,X2)
                             [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                            [1 0 0]     [1 0 0]
             a__isList(X) = [0 0 0]X >= [0 0 0]X = isList(X)
                            [0 0 0]     [0 0 0]

                              [1 0 0]     [1 0 0]
             a__isNeList(X) = [0 0 0]X >= [0 0 0]X = isNeList(X)
                              [0 0 0]     [0 0 0]

                           [1 0 0]     [1 0 0]
             a__isQid(X) = [0 0 0]X >= [0 0 0]X = isQid(X)
                           [0 0 0]     [0 0 0]

                             [1 0 0]     [1 0 0]
             a__isNePal(X) = [0 0 0]X >= [0 0 0]X = isNePal(X)
                             [0 0 0]     [0 0 0]

                           [1 0 0]     [1 0 0]
             a__isPal(X) = [0 0 0]X >= [0 0 0]X = isPal(X)
                           [0 0 0]     [0 0 0]

                              [1 0 0]     [1 0 0]
             a__and(tt(),X) = [0 0 0]X >= [0 0 0]X = mark(X)
                              [0 0 0]     [0 0 0]

                             [0]    [0]
             a__isQid(a()) = [0] >= [0] = tt()
                             [0]    [0]

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

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

                                [0]    [0]
             a__isList(nil()) = [0] >= [0] = tt()
                                [0]    [0]

                             [1 0 0]     [1 0 0]
             a__isNePal(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                             [0 0 0]     [0 0 0]

                               [0]    [0]
             a__isPal(nil()) = [0] >= [0] = tt()
                               [0]    [0]

                             [0]    [0]
             a__isQid(e()) = [0] >= [0] = tt()
                             [0]    [0]

                             [0]    [0]
             a__isQid(i()) = [0] >= [0] = tt()
                             [0]    [0]

                             [1]    [0]
             a__isQid(o()) = [0] >= [0] = tt()
                             [0]    [0]

                             [0]    [0]
             a__isQid(u()) = [0] >= [0] = tt()
                             [0]    [0]
            problem:
             strict:
              a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
              a__isList(V) -> a__isNeList(V)
              a__isNeList(V) -> a__isQid(V)
              a__isPal(V) -> a__isNePal(V)
              mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
              mark(and(X1,X2)) -> a__and(mark(X1),X2)
              mark(isList(X)) -> a__isList(X)
              mark(isNeList(X)) -> a__isNeList(X)
              mark(isQid(X)) -> a__isQid(X)
              mark(isNePal(X)) -> a__isNePal(X)
              mark(isPal(X)) -> a__isPal(X)
              mark(nil()) -> nil()
              mark(tt()) -> tt()
              mark(a()) -> a()
              mark(e()) -> e()
              mark(i()) -> i()
              mark(o()) -> o()
              mark(u()) -> u()
              a____(X1,X2) -> __(X1,X2)
              a__and(X1,X2) -> and(X1,X2)
              a__isList(X) -> isList(X)
              a__isNeList(X) -> isNeList(X)
              a__isQid(X) -> isQid(X)
              a__isNePal(X) -> isNePal(X)
              a__isPal(X) -> isPal(X)
             weak:
              a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
              a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
              a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
              a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
              a__and(tt(),X) -> mark(X)
              a__isQid(a()) -> tt()
              a____(X,nil()) -> mark(X)
              a____(nil(),X) -> mark(X)
              a__isList(nil()) -> tt()
              a__isNePal(V) -> a__isQid(V)
              a__isPal(nil()) -> tt()
              a__isQid(e()) -> tt()
              a__isQid(i()) -> tt()
              a__isQid(o()) -> tt()
              a__isQid(u()) -> tt()
            Matrix Interpretation Processor:
             dimension: 3
             max_matrix:
              [1 0 1]
              [0 0 1]
              [0 0 0]
              interpretation:
                               [1 0 0]
               [isNePal](x0) = [0 0 0]x0
                               [0 0 0]  ,

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

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

                     [0]
               [u] = [0]
                     [0],

                     [1]
               [o] = [0]
                     [0],

                     [0]
               [i] = [0]
                     [0],

                     [1]
               [e] = [0]
                     [0],

                     [0]
               [a] = [0]
                     [0],

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

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

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

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

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

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

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

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

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

                      [0]
               [tt] = [0]
                      [0],

                       [1]
               [nil] = [0]
                       [0],

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

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

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

                              [1 0 0]     [1 0 0]
               a__isList(V) = [0 0 0]V >= [0 0 0]V = a__isNeList(V)
                              [0 0 0]     [0 0 0]

                                [1 0 0]     [1 0 0]
               a__isNeList(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                                [0 0 0]     [0 0 0]

                             [1 0 0]    [1]    [1 0 0]
               a__isPal(V) = [0 0 0]V + [0] >= [0 0 0]V = a__isNePal(V)
                             [0 0 0]    [0]    [0 0 0]

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

                                  [1 0 0]     [1 0 1]     [1]    [1 0 0]     [1 0 1]     [1]
               mark(and(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = a__and(mark(X1),X2)
                                  [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                 [1 0 0]     [1 0 0]
               mark(isList(X)) = [0 0 0]X >= [0 0 0]X = a__isList(X)
                                 [0 0 0]     [0 0 0]

                                   [1 0 0]     [1 0 0]
               mark(isNeList(X)) = [0 0 0]X >= [0 0 0]X = a__isNeList(X)
                                   [0 0 0]     [0 0 0]

                                [1 0 0]     [1 0 0]
               mark(isQid(X)) = [0 0 0]X >= [0 0 0]X = a__isQid(X)
                                [0 0 0]     [0 0 0]

                                  [1 0 0]     [1 0 0]
               mark(isNePal(X)) = [0 0 0]X >= [0 0 0]X = a__isNePal(X)
                                  [0 0 0]     [0 0 0]

                                [1 0 0]    [1]    [1 0 0]    [1]
               mark(isPal(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__isPal(X)
                                [0 0 0]    [0]    [0 0 0]    [0]

                             [1]    [1]
               mark(nil()) = [0] >= [0] = nil()
                             [0]    [0]

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

                           [0]    [0]
               mark(a()) = [0] >= [0] = a()
                           [0]    [0]

                           [1]    [1]
               mark(e()) = [0] >= [0] = e()
                           [0]    [0]

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

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

                           [0]    [0]
               mark(u()) = [0] >= [0] = u()
                           [0]    [0]

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

                               [1 0 1]     [1 0 1]     [1]    [1 0 0]     [1 0 1]     [1]
               a__and(X1,X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = and(X1,X2)
                               [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                              [1 0 0]     [1 0 0]
               a__isList(X) = [0 0 0]X >= [0 0 0]X = isList(X)
                              [0 0 0]     [0 0 0]

                                [1 0 0]     [1 0 0]
               a__isNeList(X) = [0 0 0]X >= [0 0 0]X = isNeList(X)
                                [0 0 0]     [0 0 0]

                             [1 0 0]     [1 0 0]
               a__isQid(X) = [0 0 0]X >= [0 0 0]X = isQid(X)
                             [0 0 0]     [0 0 0]

                               [1 0 0]     [1 0 0]
               a__isNePal(X) = [0 0 0]X >= [0 0 0]X = isNePal(X)
                               [0 0 0]     [0 0 0]

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

                                      [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]
               a__isList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isList(V1),isList(V2))
                                      [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                        [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]
               a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isList(V1),isNeList(V2))
                                        [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                        [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]
               a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isNeList(V1),isList(V2))
                                        [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                           [2 0 0]    [1 0 0]    [2]    [1 0 0]    [1 0 0]    [2]
               a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P + [0] >= [0 0 0]I + [0 0 0]P + [0] = a__and(a__isQid(I),isPal(P))
                                           [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]

                                [1 0 1]    [1]    [1 0 0]
               a__and(tt(),X) = [0 0 0]X + [0] >= [0 0 0]X = mark(X)
                                [0 0 0]    [0]    [0 0 0]

                               [0]    [0]
               a__isQid(a()) = [0] >= [0] = tt()
                               [0]    [0]

                                [1 0 0]    [2]    [1 0 0]
               a____(X,nil()) = [0 0 0]X + [0] >= [0 0 0]X = mark(X)
                                [0 0 0]    [0]    [0 0 0]

                                [1 0 0]    [2]    [1 0 0]
               a____(nil(),X) = [0 0 1]X + [0] >= [0 0 0]X = mark(X)
                                [0 0 0]    [0]    [0 0 0]

                                  [1]    [0]
               a__isList(nil()) = [0] >= [0] = tt()
                                  [0]    [0]

                               [1 0 0]     [1 0 0]
               a__isNePal(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                               [0 0 0]     [0 0 0]

                                 [2]    [0]
               a__isPal(nil()) = [0] >= [0] = tt()
                                 [0]    [0]

                               [1]    [0]
               a__isQid(e()) = [0] >= [0] = tt()
                               [0]    [0]

                               [0]    [0]
               a__isQid(i()) = [0] >= [0] = tt()
                               [0]    [0]

                               [1]    [0]
               a__isQid(o()) = [0] >= [0] = tt()
                               [0]    [0]

                               [0]    [0]
               a__isQid(u()) = [0] >= [0] = tt()
                               [0]    [0]
              problem:
               strict:
                a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
                a__isList(V) -> a__isNeList(V)
                a__isNeList(V) -> a__isQid(V)
                mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
                mark(and(X1,X2)) -> a__and(mark(X1),X2)
                mark(isList(X)) -> a__isList(X)
                mark(isNeList(X)) -> a__isNeList(X)
                mark(isQid(X)) -> a__isQid(X)
                mark(isNePal(X)) -> a__isNePal(X)
                mark(isPal(X)) -> a__isPal(X)
                mark(nil()) -> nil()
                mark(tt()) -> tt()
                mark(a()) -> a()
                mark(e()) -> e()
                mark(i()) -> i()
                mark(o()) -> o()
                mark(u()) -> u()
                a____(X1,X2) -> __(X1,X2)
                a__and(X1,X2) -> and(X1,X2)
                a__isList(X) -> isList(X)
                a__isNeList(X) -> isNeList(X)
                a__isQid(X) -> isQid(X)
                a__isNePal(X) -> isNePal(X)
                a__isPal(X) -> isPal(X)
               weak:
                a__isPal(V) -> a__isNePal(V)
                a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
                a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
                a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
                a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
                a__and(tt(),X) -> mark(X)
                a__isQid(a()) -> tt()
                a____(X,nil()) -> mark(X)
                a____(nil(),X) -> mark(X)
                a__isList(nil()) -> tt()
                a__isNePal(V) -> a__isQid(V)
                a__isPal(nil()) -> tt()
                a__isQid(e()) -> tt()
                a__isQid(i()) -> tt()
                a__isQid(o()) -> tt()
                a__isQid(u()) -> tt()
              Matrix Interpretation Processor:
               dimension: 3
               max_matrix:
                [1 1 1]
                [0 0 1]
                [0 0 0]
                interpretation:
                                 [1 0 0]
                 [isNePal](x0) = [0 0 0]x0
                                 [0 0 0]  ,

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

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

                       [1]
                 [u] = [0]
                       [0],

                       [1]
                 [o] = [0]
                       [0],

                       [1]
                 [i] = [0]
                       [0],

                       [1]
                 [e] = [0]
                       [0],

                       [1]
                 [a] = [0]
                       [0],

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

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

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

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

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

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

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

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

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

                        [1]
                 [tt] = [0]
                        [0],

                         [1]
                 [nil] = [0]
                         [0],

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

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

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

                                [1 0 0]    [1]    [1 0 0]    [1]
                 a__isList(V) = [0 0 0]V + [0] >= [0 0 0]V + [0] = a__isNeList(V)
                                [0 0 0]    [0]    [0 0 0]    [0]

                                  [1 0 0]    [1]    [1 0 0]
                 a__isNeList(V) = [0 0 0]V + [0] >= [0 0 0]V = a__isQid(V)
                                  [0 0 0]    [0]    [0 0 0]

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

                                    [1 1 0]     [1 0 1]      [1 0 0]     [1 0 1]
                 mark(and(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = a__and(mark(X1),X2)
                                    [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                                   [1 0 0]    [1]    [1 0 0]    [1]
                 mark(isList(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__isList(X)
                                   [0 0 0]    [0]    [0 0 0]    [0]

                                     [1 0 0]    [1]    [1 0 0]    [1]
                 mark(isNeList(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__isNeList(X)
                                     [0 0 0]    [0]    [0 0 0]    [0]

                                  [1 0 0]     [1 0 0]
                 mark(isQid(X)) = [0 0 0]X >= [0 0 0]X = a__isQid(X)
                                  [0 0 0]     [0 0 0]

                                    [1 0 0]     [1 0 0]
                 mark(isNePal(X)) = [0 0 0]X >= [0 0 0]X = a__isNePal(X)
                                    [0 0 0]     [0 0 0]

                                  [1 0 0]     [1 0 0]
                 mark(isPal(X)) = [0 0 0]X >= [0 0 0]X = a__isPal(X)
                                  [0 0 0]     [0 0 0]

                               [1]    [1]
                 mark(nil()) = [0] >= [0] = nil()
                               [0]    [0]

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

                             [1]    [1]
                 mark(a()) = [0] >= [0] = a()
                             [0]    [0]

                             [1]    [1]
                 mark(e()) = [0] >= [0] = e()
                             [0]    [0]

                             [1]    [1]
                 mark(i()) = [0] >= [0] = i()
                             [0]    [0]

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

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

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

                                 [1 1 0]     [1 0 1]      [1 1 0]     [1 0 1]
                 a__and(X1,X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = and(X1,X2)
                                 [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                                [1 0 0]    [1]    [1 0 0]    [1]
                 a__isList(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = isList(X)
                                [0 0 0]    [0]    [0 0 0]    [0]

                                  [1 0 0]    [1]    [1 0 0]    [1]
                 a__isNeList(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = isNeList(X)
                                  [0 0 0]    [0]    [0 0 0]    [0]

                               [1 0 0]     [1 0 0]
                 a__isQid(X) = [0 0 0]X >= [0 0 0]X = isQid(X)
                               [0 0 0]     [0 0 0]

                                 [1 0 0]     [1 0 0]
                 a__isNePal(X) = [0 0 0]X >= [0 0 0]X = isNePal(X)
                                 [0 0 0]     [0 0 0]

                               [1 0 0]     [1 0 0]
                 a__isPal(X) = [0 0 0]X >= [0 0 0]X = isPal(X)
                               [0 0 0]     [0 0 0]

                               [1 0 0]     [1 0 0]
                 a__isPal(V) = [0 0 0]V >= [0 0 0]V = a__isNePal(V)
                               [0 0 0]     [0 0 0]

                                        [1 0 0]     [1 0 0]     [2]    [1 0 0]     [1 0 0]     [2]
                 a__isList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isList(V1),isList(V2))
                                        [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                          [1 0 0]     [1 0 0]     [2]    [1 0 0]     [1 0 0]     [2]
                 a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isList(V1),isNeList(V2))
                                          [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                          [1 0 0]     [1 0 0]     [2]    [1 0 0]     [1 0 0]     [2]
                 a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isNeList(V1),isList(V2))
                                          [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                             [2 0 0]    [1 0 0]    [2]    [1 0 0]    [1 0 0]
                 a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P + [0] >= [0 0 0]I + [0 0 0]P = a__and(a__isQid(I),isPal(P))
                                             [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]

                                  [1 0 1]    [1]    [1 0 0]
                 a__and(tt(),X) = [0 0 0]X + [0] >= [0 0 0]X = mark(X)
                                  [0 0 0]    [0]    [0 0 0]

                                 [1]    [1]
                 a__isQid(a()) = [0] >= [0] = tt()
                                 [0]    [0]

                                  [1 0 0]    [2]    [1 0 0]
                 a____(X,nil()) = [0 0 1]X + [0] >= [0 0 0]X = mark(X)
                                  [0 0 0]    [0]    [0 0 0]

                                  [1 0 0]    [2]    [1 0 0]
                 a____(nil(),X) = [0 0 0]X + [0] >= [0 0 0]X = mark(X)
                                  [0 0 0]    [0]    [0 0 0]

                                    [2]    [1]
                 a__isList(nil()) = [0] >= [0] = tt()
                                    [0]    [0]

                                 [1 0 0]     [1 0 0]
                 a__isNePal(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                                 [0 0 0]     [0 0 0]

                                   [1]    [1]
                 a__isPal(nil()) = [0] >= [0] = tt()
                                   [0]    [0]

                                 [1]    [1]
                 a__isQid(e()) = [0] >= [0] = tt()
                                 [0]    [0]

                                 [1]    [1]
                 a__isQid(i()) = [0] >= [0] = tt()
                                 [0]    [0]

                                 [1]    [1]
                 a__isQid(o()) = [0] >= [0] = tt()
                                 [0]    [0]

                                 [1]    [1]
                 a__isQid(u()) = [0] >= [0] = tt()
                                 [0]    [0]
                problem:
                 strict:
                  a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
                  a__isList(V) -> a__isNeList(V)
                  mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
                  mark(and(X1,X2)) -> a__and(mark(X1),X2)
                  mark(isList(X)) -> a__isList(X)
                  mark(isNeList(X)) -> a__isNeList(X)
                  mark(isQid(X)) -> a__isQid(X)
                  mark(isNePal(X)) -> a__isNePal(X)
                  mark(isPal(X)) -> a__isPal(X)
                  mark(nil()) -> nil()
                  mark(tt()) -> tt()
                  mark(a()) -> a()
                  mark(e()) -> e()
                  mark(i()) -> i()
                  mark(o()) -> o()
                  mark(u()) -> u()
                  a____(X1,X2) -> __(X1,X2)
                  a__and(X1,X2) -> and(X1,X2)
                  a__isList(X) -> isList(X)
                  a__isNeList(X) -> isNeList(X)
                  a__isQid(X) -> isQid(X)
                  a__isNePal(X) -> isNePal(X)
                  a__isPal(X) -> isPal(X)
                 weak:
                  a__isNeList(V) -> a__isQid(V)
                  a__isPal(V) -> a__isNePal(V)
                  a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
                  a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
                  a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
                  a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
                  a__and(tt(),X) -> mark(X)
                  a__isQid(a()) -> tt()
                  a____(X,nil()) -> mark(X)
                  a____(nil(),X) -> mark(X)
                  a__isList(nil()) -> tt()
                  a__isNePal(V) -> a__isQid(V)
                  a__isPal(nil()) -> tt()
                  a__isQid(e()) -> tt()
                  a__isQid(i()) -> tt()
                  a__isQid(o()) -> tt()
                  a__isQid(u()) -> tt()
                Matrix Interpretation Processor:
                 dimension: 3
                 max_matrix:
                  [1 1 0]
                  [0 0 0]
                  [0 0 0]
                  interpretation:
                                   [1 0 0]
                   [isNePal](x0) = [0 0 0]x0
                                   [0 0 0]  ,

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

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

                         [0]
                   [u] = [0]
                         [0],

                         [0]
                   [o] = [0]
                         [0],

                         [0]
                   [i] = [0]
                         [0],

                         [0]
                   [e] = [0]
                         [0],

                         [0]
                   [a] = [0]
                         [0],

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

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

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

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

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

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

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

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

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

                          [0]
                   [tt] = [0]
                          [0],

                           [0]
                   [nil] = [0]
                           [0],

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

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

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

                                  [1 0 0]    [1]    [1 0 0]
                   a__isList(V) = [0 0 0]V + [0] >= [0 0 0]V = a__isNeList(V)
                                  [0 0 0]    [0]    [0 0 0]

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

                                      [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]
                   mark(and(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = a__and(mark(X1),X2)
                                      [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                                     [1 0 0]    [1]    [1 0 0]    [1]
                   mark(isList(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__isList(X)
                                     [0 0 0]    [0]    [0 0 0]    [0]

                                       [1 0 0]     [1 0 0]
                   mark(isNeList(X)) = [0 0 0]X >= [0 0 0]X = a__isNeList(X)
                                       [0 0 0]     [0 0 0]

                                    [1 0 0]     [1 0 0]
                   mark(isQid(X)) = [0 0 0]X >= [0 0 0]X = a__isQid(X)
                                    [0 0 0]     [0 0 0]

                                      [1 0 0]     [1 0 0]
                   mark(isNePal(X)) = [0 0 0]X >= [0 0 0]X = a__isNePal(X)
                                      [0 0 0]     [0 0 0]

                                    [1 0 0]     [1 0 0]
                   mark(isPal(X)) = [0 0 0]X >= [0 0 0]X = a__isPal(X)
                                    [0 0 0]     [0 0 0]

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

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

                               [0]    [0]
                   mark(a()) = [0] >= [0] = a()
                               [0]    [0]

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

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

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

                               [0]    [0]
                   mark(u()) = [0] >= [0] = u()
                               [0]    [0]

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

                                   [1 1 0]     [1 0 0]      [1 0 0]     [1 0 0]
                   a__and(X1,X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = and(X1,X2)
                                   [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]

                                  [1 0 0]    [1]    [1 0 0]    [1]
                   a__isList(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = isList(X)
                                  [0 0 0]    [0]    [0 0 0]    [0]

                                    [1 0 0]     [1 0 0]
                   a__isNeList(X) = [0 0 0]X >= [0 0 0]X = isNeList(X)
                                    [0 0 0]     [0 0 0]

                                 [1 0 0]     [1 0 0]
                   a__isQid(X) = [0 0 0]X >= [0 0 0]X = isQid(X)
                                 [0 0 0]     [0 0 0]

                                   [1 0 0]     [1 0 0]
                   a__isNePal(X) = [0 0 0]X >= [0 0 0]X = isNePal(X)
                                   [0 0 0]     [0 0 0]

                                 [1 0 0]     [1 0 0]
                   a__isPal(X) = [0 0 0]X >= [0 0 0]X = isPal(X)
                                 [0 0 0]     [0 0 0]

                                    [1 0 0]     [1 0 0]
                   a__isNeList(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                                    [0 0 0]     [0 0 0]

                                 [1 0 0]     [1 0 0]
                   a__isPal(V) = [0 0 0]V >= [0 0 0]V = a__isNePal(V)
                                 [0 0 0]     [0 0 0]

                                          [1 0 0]     [1 0 0]     [2]    [1 0 0]     [1 0 0]     [2]
                   a__isList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isList(V1),isList(V2))
                                          [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                            [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]
                   a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isList(V1),isNeList(V2))
                                            [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                            [1 0 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]
                   a__isNeList(__(V1,V2)) = [0 0 0]V1 + [0 0 0]V2 + [0] >= [0 0 0]V1 + [0 0 0]V2 + [0] = a__and(a__isNeList(V1),isList(V2))
                                            [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

                                               [2 0 0]    [1 0 0]    [2]    [1 0 0]    [1 0 0]
                   a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P + [0] >= [0 0 0]I + [0 0 0]P = a__and(a__isQid(I),isPal(P))
                                               [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]

                                    [1 0 0]     [1 0 0]
                   a__and(tt(),X) = [0 0 0]X >= [0 0 0]X = mark(X)
                                    [0 0 0]     [0 0 0]

                                   [0]    [0]
                   a__isQid(a()) = [0] >= [0] = tt()
                                   [0]    [0]

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

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

                                      [1]    [0]
                   a__isList(nil()) = [0] >= [0] = tt()
                                      [0]    [0]

                                   [1 0 0]     [1 0 0]
                   a__isNePal(V) = [0 0 0]V >= [0 0 0]V = a__isQid(V)
                                   [0 0 0]     [0 0 0]

                                     [0]    [0]
                   a__isPal(nil()) = [0] >= [0] = tt()
                                     [0]    [0]

                                   [0]    [0]
                   a__isQid(e()) = [0] >= [0] = tt()
                                   [0]    [0]

                                   [0]    [0]
                   a__isQid(i()) = [0] >= [0] = tt()
                                   [0]    [0]

                                   [0]    [0]
                   a__isQid(o()) = [0] >= [0] = tt()
                                   [0]    [0]

                                   [0]    [0]
                   a__isQid(u()) = [0] >= [0] = tt()
                                   [0]    [0]
                  problem:
                   strict:
                    a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
                    mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
                    mark(and(X1,X2)) -> a__and(mark(X1),X2)
                    mark(isList(X)) -> a__isList(X)
                    mark(isNeList(X)) -> a__isNeList(X)
                    mark(isQid(X)) -> a__isQid(X)
                    mark(isNePal(X)) -> a__isNePal(X)
                    mark(isPal(X)) -> a__isPal(X)
                    mark(nil()) -> nil()
                    mark(tt()) -> tt()
                    mark(a()) -> a()
                    mark(e()) -> e()
                    mark(i()) -> i()
                    mark(o()) -> o()
                    mark(u()) -> u()
                    a____(X1,X2) -> __(X1,X2)
                    a__and(X1,X2) -> and(X1,X2)
                    a__isList(X) -> isList(X)
                    a__isNeList(X) -> isNeList(X)
                    a__isQid(X) -> isQid(X)
                    a__isNePal(X) -> isNePal(X)
                    a__isPal(X) -> isPal(X)
                   weak:
                    a__isList(V) -> a__isNeList(V)
                    a__isNeList(V) -> a__isQid(V)
                    a__isPal(V) -> a__isNePal(V)
                    a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
                    a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
                    a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
                    a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
                    a__and(tt(),X) -> mark(X)
                    a__isQid(a()) -> tt()
                    a____(X,nil()) -> mark(X)
                    a____(nil(),X) -> mark(X)
                    a__isList(nil()) -> tt()
                    a__isNePal(V) -> a__isQid(V)
                    a__isPal(nil()) -> tt()
                    a__isQid(e()) -> tt()
                    a__isQid(i()) -> tt()
                    a__isQid(o()) -> tt()
                    a__isQid(u()) -> tt()
                  Matrix Interpretation Processor:
                   dimension: 1
                   max_matrix:
                    1
                    interpretation:
                     [isNePal](x0) = x0 + 8,

                     [isQid](x0) = x0 + 96,

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

                     [u] = 28,

                     [o] = 28,

                     [i] = 28,

                     [e] = 28,

                     [a] = 28,

                     [a__isPal](x0) = x0 + 11,

                     [isPal](x0) = x0 + 1,

                     [a__isNePal](x0) = x0 + 11,

                     [isNeList](x0) = x0,

                     [a__isQid](x0) = x0 + 11,

                     [isList](x0) = x0,

                     [a__isNeList](x0) = x0 + 11,

                     [a__isList](x0) = x0 + 11,

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

                     [tt] = 39,

                     [nil] = 28,

                     [mark](x0) = x0 + 40,

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

                     [__](x0, x1) = x0 + x1 + 1
                    orientation:
                     a____(__(X,Y),Z) = X + Y + Z + 13 >= X + Y + Z + 144 = a____(mark(X),a____(mark(Y),mark(Z)))

                     mark(__(X1,X2)) = X1 + X2 + 41 >= X1 + X2 + 92 = a____(mark(X1),mark(X2))

                     mark(and(X1,X2)) = X1 + X2 + 65 >= X1 + X2 + 41 = a__and(mark(X1),X2)

                     mark(isList(X)) = X + 40 >= X + 11 = a__isList(X)

                     mark(isNeList(X)) = X + 40 >= X + 11 = a__isNeList(X)

                     mark(isQid(X)) = X + 136 >= X + 11 = a__isQid(X)

                     mark(isNePal(X)) = X + 48 >= X + 11 = a__isNePal(X)

                     mark(isPal(X)) = X + 41 >= X + 11 = a__isPal(X)

                     mark(nil()) = 68 >= 28 = nil()

                     mark(tt()) = 79 >= 39 = tt()

                     mark(a()) = 68 >= 28 = a()

                     mark(e()) = 68 >= 28 = e()

                     mark(i()) = 68 >= 28 = i()

                     mark(o()) = 68 >= 28 = o()

                     mark(u()) = 68 >= 28 = u()

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

                     a__and(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 25 = and(X1,X2)

                     a__isList(X) = X + 11 >= X = isList(X)

                     a__isNeList(X) = X + 11 >= X = isNeList(X)

                     a__isQid(X) = X + 11 >= X + 96 = isQid(X)

                     a__isNePal(X) = X + 11 >= X + 8 = isNePal(X)

                     a__isPal(X) = X + 11 >= X + 1 = isPal(X)

                     a__isList(V) = V + 11 >= V + 11 = a__isNeList(V)

                     a__isNeList(V) = V + 11 >= V + 11 = a__isQid(V)

                     a__isPal(V) = V + 11 >= V + 11 = a__isNePal(V)

                     a__isList(__(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = a__and(a__isList(V1),isList(V2))

                     a__isNeList(__(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = a__and(a__isList(V1),isNeList(V2))

                     a__isNeList(__(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = a__and(a__isNeList(V1),isList(V2))

                     a__isNePal(__(I,__(P,I))) = 2I + P + 13 >= I + P + 13 = a__and(a__isQid(I),isPal(P))

                     a__and(tt(),X) = X + 40 >= X + 40 = mark(X)

                     a__isQid(a()) = 39 >= 39 = tt()

                     a____(X,nil()) = X + 40 >= X + 40 = mark(X)

                     a____(nil(),X) = X + 40 >= X + 40 = mark(X)

                     a__isList(nil()) = 39 >= 39 = tt()

                     a__isNePal(V) = V + 11 >= V + 11 = a__isQid(V)

                     a__isPal(nil()) = 39 >= 39 = tt()

                     a__isQid(e()) = 39 >= 39 = tt()

                     a__isQid(i()) = 39 >= 39 = tt()

                     a__isQid(o()) = 39 >= 39 = tt()

                     a__isQid(u()) = 39 >= 39 = tt()
                    problem:
                     strict:
                      a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
                      mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
                      a__and(X1,X2) -> and(X1,X2)
                      a__isQid(X) -> isQid(X)
                     weak:
                      mark(and(X1,X2)) -> a__and(mark(X1),X2)
                      mark(isList(X)) -> a__isList(X)
                      mark(isNeList(X)) -> a__isNeList(X)
                      mark(isQid(X)) -> a__isQid(X)
                      mark(isNePal(X)) -> a__isNePal(X)
                      mark(isPal(X)) -> a__isPal(X)
                      mark(nil()) -> nil()
                      mark(tt()) -> tt()
                      mark(a()) -> a()
                      mark(e()) -> e()
                      mark(i()) -> i()
                      mark(o()) -> o()
                      mark(u()) -> u()
                      a____(X1,X2) -> __(X1,X2)
                      a__isList(X) -> isList(X)
                      a__isNeList(X) -> isNeList(X)
                      a__isNePal(X) -> isNePal(X)
                      a__isPal(X) -> isPal(X)
                      a__isList(V) -> a__isNeList(V)
                      a__isNeList(V) -> a__isQid(V)
                      a__isPal(V) -> a__isNePal(V)
                      a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
                      a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
                      a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
                      a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
                      a__and(tt(),X) -> mark(X)
                      a__isQid(a()) -> tt()
                      a____(X,nil()) -> mark(X)
                      a____(nil(),X) -> mark(X)
                      a__isList(nil()) -> tt()
                      a__isNePal(V) -> a__isQid(V)
                      a__isPal(nil()) -> tt()
                      a__isQid(e()) -> tt()
                      a__isQid(i()) -> tt()
                      a__isQid(o()) -> tt()
                      a__isQid(u()) -> tt()
                    Matrix Interpretation Processor:
                     dimension: 1
                     max_matrix:
                      1
                      interpretation:
                       [isNePal](x0) = x0 + 2,

                       [isQid](x0) = x0 + 1,

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

                       [u] = 5,

                       [o] = 2,

                       [i] = 8,

                       [e] = 3,

                       [a] = 4,

                       [a__isPal](x0) = x0 + 6,

                       [isPal](x0) = x0 + 5,

                       [a__isNePal](x0) = x0 + 4,

                       [isNeList](x0) = x0 + 2,

                       [a__isQid](x0) = x0 + 2,

                       [isList](x0) = x0,

                       [a__isNeList](x0) = x0 + 2,

                       [a__isList](x0) = x0 + 2,

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

                       [tt] = 4,

                       [nil] = 14,

                       [mark](x0) = x0 + 2,

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

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

                       mark(__(X1,X2)) = X1 + X2 + 10 >= X1 + X2 + 12 = a____(mark(X1),mark(X2))

                       a__and(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 4 = and(X1,X2)

                       a__isQid(X) = X + 2 >= X + 1 = isQid(X)

                       mark(and(X1,X2)) = X1 + X2 + 6 >= X1 + X2 + 3 = a__and(mark(X1),X2)

                       mark(isList(X)) = X + 2 >= X + 2 = a__isList(X)

                       mark(isNeList(X)) = X + 4 >= X + 2 = a__isNeList(X)

                       mark(isQid(X)) = X + 3 >= X + 2 = a__isQid(X)

                       mark(isNePal(X)) = X + 4 >= X + 4 = a__isNePal(X)

                       mark(isPal(X)) = X + 7 >= X + 6 = a__isPal(X)

                       mark(nil()) = 16 >= 14 = nil()

                       mark(tt()) = 6 >= 4 = tt()

                       mark(a()) = 6 >= 4 = a()

                       mark(e()) = 5 >= 3 = e()

                       mark(i()) = 10 >= 8 = i()

                       mark(o()) = 4 >= 2 = o()

                       mark(u()) = 7 >= 5 = u()

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

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

                       a__isNeList(X) = X + 2 >= X + 2 = isNeList(X)

                       a__isNePal(X) = X + 4 >= X + 2 = isNePal(X)

                       a__isPal(X) = X + 6 >= X + 5 = isPal(X)

                       a__isList(V) = V + 2 >= V + 2 = a__isNeList(V)

                       a__isNeList(V) = V + 2 >= V + 2 = a__isQid(V)

                       a__isPal(V) = V + 6 >= V + 4 = a__isNePal(V)

                       a__isList(__(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 3 = a__and(a__isList(V1),isList(V2))

                       a__isNeList(__(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 5 = a__and(a__isList(V1),isNeList(V2))

                       a__isNeList(__(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 3 = a__and(a__isNeList(V1),isList(V2))

                       a__isNePal(__(I,__(P,I))) = 2I + P + 20 >= I + P + 8 = a__and(a__isQid(I),isPal(P))

                       a__and(tt(),X) = X + 5 >= X + 2 = mark(X)

                       a__isQid(a()) = 6 >= 4 = tt()

                       a____(X,nil()) = X + 22 >= X + 2 = mark(X)

                       a____(nil(),X) = X + 22 >= X + 2 = mark(X)

                       a__isList(nil()) = 16 >= 4 = tt()

                       a__isNePal(V) = V + 4 >= V + 2 = a__isQid(V)

                       a__isPal(nil()) = 20 >= 4 = tt()

                       a__isQid(e()) = 5 >= 4 = tt()

                       a__isQid(i()) = 10 >= 4 = tt()

                       a__isQid(o()) = 4 >= 4 = tt()

                       a__isQid(u()) = 7 >= 4 = tt()
                      problem:
                       strict:
                        a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
                        mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
                        a__and(X1,X2) -> and(X1,X2)
                       weak:
                        a__isQid(X) -> isQid(X)
                        mark(and(X1,X2)) -> a__and(mark(X1),X2)
                        mark(isList(X)) -> a__isList(X)
                        mark(isNeList(X)) -> a__isNeList(X)
                        mark(isQid(X)) -> a__isQid(X)
                        mark(isNePal(X)) -> a__isNePal(X)
                        mark(isPal(X)) -> a__isPal(X)
                        mark(nil()) -> nil()
                        mark(tt()) -> tt()
                        mark(a()) -> a()
                        mark(e()) -> e()
                        mark(i()) -> i()
                        mark(o()) -> o()
                        mark(u()) -> u()
                        a____(X1,X2) -> __(X1,X2)
                        a__isList(X) -> isList(X)
                        a__isNeList(X) -> isNeList(X)
                        a__isNePal(X) -> isNePal(X)
                        a__isPal(X) -> isPal(X)
                        a__isList(V) -> a__isNeList(V)
                        a__isNeList(V) -> a__isQid(V)
                        a__isPal(V) -> a__isNePal(V)
                        a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
                        a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
                        a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
                        a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
                        a__and(tt(),X) -> mark(X)
                        a__isQid(a()) -> tt()
                        a____(X,nil()) -> mark(X)
                        a____(nil(),X) -> mark(X)
                        a__isList(nil()) -> tt()
                        a__isNePal(V) -> a__isQid(V)
                        a__isPal(nil()) -> tt()
                        a__isQid(e()) -> tt()
                        a__isQid(i()) -> tt()
                        a__isQid(o()) -> tt()
                        a__isQid(u()) -> tt()
                      Matrix Interpretation Processor:
                       dimension: 2
                       max_matrix:
                        [1 1]
                        [0 1]
                        interpretation:
                                         [1 0]
                         [isNePal](x0) = [0 0]x0,

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

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

                               [2]
                         [u] = [0],

                               [2]
                         [o] = [2],

                               [3]
                         [i] = [0],

                               [2]
                         [e] = [0],

                               [2]
                         [a] = [0],

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

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

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


                         [isNeList](x0) = x0,

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


                         [isList](x0) = x0,


                         [a__isNeList](x0) = x0,


                         [a__isList](x0) = x0,

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

                                [0]
                         [tt] = [0],

                                 [1]
                         [nil] = [2],


                         [mark](x0) = x0,

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

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

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

                                         [1 0]           [1 0]
                         a__and(X1,X2) = [0 0]X1 + X2 >= [0 0]X1 + X2 = and(X1,X2)

                                       [1 0]     [1 0]
                         a__isQid(X) = [0 0]X >= [0 0]X = isQid(X)

                                            [1 0]           [1 0]
                         mark(and(X1,X2)) = [0 0]X1 + X2 >= [0 0]X1 + X2 = a__and(mark(X1),X2)


                         mark(isList(X)) = X >= X = a__isList(X)


                         mark(isNeList(X)) = X >= X = a__isNeList(X)

                                          [1 0]     [1 0]
                         mark(isQid(X)) = [0 0]X >= [0 0]X = a__isQid(X)

                                            [1 0]     [1 0]
                         mark(isNePal(X)) = [0 0]X >= [0 0]X = a__isNePal(X)

                                          [1 0]     [1 0]
                         mark(isPal(X)) = [0 0]X >= [0 0]X = a__isPal(X)

                                       [1]    [1]
                         mark(nil()) = [2] >= [2] = nil()

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

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

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

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

                                     [2]    [2]
                         mark(o()) = [2] >= [2] = o()

                                     [2]    [2]
                         mark(u()) = [0] >= [0] = u()

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


                         a__isList(X) = X >= X = isList(X)


                         a__isNeList(X) = X >= X = isNeList(X)

                                         [1 0]     [1 0]
                         a__isNePal(X) = [0 0]X >= [0 0]X = isNePal(X)

                                       [1 0]     [1 0]
                         a__isPal(X) = [0 0]X >= [0 0]X = isPal(X)


                         a__isList(V) = V >= V = a__isNeList(V)

                                               [1 0]
                         a__isNeList(V) = V >= [0 0]V = a__isQid(V)

                                       [1 0]     [1 0]
                         a__isPal(V) = [0 0]V >= [0 0]V = a__isNePal(V)

                                                [1 1]          [0]    [1 0]
                         a__isList(__(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + V2 = a__and(a__isList(V1),isList(V2))

                                                  [1 1]          [0]    [1 0]
                         a__isNeList(__(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + V2 = a__and(a__isList(V1),isNeList(V2))

                                                  [1 1]          [0]    [1 0]
                         a__isNeList(__(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + V2 = a__and(a__isNeList(V1),isList(V2))

                                                     [2 1]    [1 1]     [1 0]    [1 0]
                         a__isNePal(__(I,__(P,I))) = [0 0]I + [0 0]P >= [0 0]I + [0 0]P = a__and(a__isQid(I),isPal(P))


                         a__and(tt(),X) = X >= X = mark(X)

                                         [2]    [0]
                         a__isQid(a()) = [0] >= [0] = tt()

                                          [1 1]    [1]
                         a____(X,nil()) = [0 1]X + [3] >= X = mark(X)

                                              [3]
                         a____(nil(),X) = X + [3] >= X = mark(X)

                                            [1]    [0]
                         a__isList(nil()) = [2] >= [0] = tt()

                                         [1 0]     [1 0]
                         a__isNePal(V) = [0 0]V >= [0 0]V = a__isQid(V)

                                           [1]    [0]
                         a__isPal(nil()) = [0] >= [0] = tt()

                                         [2]    [0]
                         a__isQid(e()) = [0] >= [0] = tt()

                                         [3]    [0]
                         a__isQid(i()) = [0] >= [0] = tt()

                                         [2]    [0]
                         a__isQid(o()) = [0] >= [0] = tt()

                                         [2]    [0]
                         a__isQid(u()) = [0] >= [0] = tt()
                        problem:
                         strict:
                          mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
                          a__and(X1,X2) -> and(X1,X2)
                         weak:
                          a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
                          a__isQid(X) -> isQid(X)
                          mark(and(X1,X2)) -> a__and(mark(X1),X2)
                          mark(isList(X)) -> a__isList(X)
                          mark(isNeList(X)) -> a__isNeList(X)
                          mark(isQid(X)) -> a__isQid(X)
                          mark(isNePal(X)) -> a__isNePal(X)
                          mark(isPal(X)) -> a__isPal(X)
                          mark(nil()) -> nil()
                          mark(tt()) -> tt()
                          mark(a()) -> a()
                          mark(e()) -> e()
                          mark(i()) -> i()
                          mark(o()) -> o()
                          mark(u()) -> u()
                          a____(X1,X2) -> __(X1,X2)
                          a__isList(X) -> isList(X)
                          a__isNeList(X) -> isNeList(X)
                          a__isNePal(X) -> isNePal(X)
                          a__isPal(X) -> isPal(X)
                          a__isList(V) -> a__isNeList(V)
                          a__isNeList(V) -> a__isQid(V)
                          a__isPal(V) -> a__isNePal(V)
                          a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
                          a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
                          a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
                          a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
                          a__and(tt(),X) -> mark(X)
                          a__isQid(a()) -> tt()
                          a____(X,nil()) -> mark(X)
                          a____(nil(),X) -> mark(X)
                          a__isList(nil()) -> tt()
                          a__isNePal(V) -> a__isQid(V)
                          a__isPal(nil()) -> tt()
                          a__isQid(e()) -> tt()
                          a__isQid(i()) -> tt()
                          a__isQid(o()) -> tt()
                          a__isQid(u()) -> tt()
                        Open

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

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

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z)))
     , a____(X, nil()) -> mark(X)
     , a____(nil(), X) -> mark(X)
     , a__and(tt(), X) -> mark(X)
     , a__isList(V) -> a__isNeList(V)
     , a__isList(nil()) -> tt()
     , a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2))
     , a__isNeList(V) -> a__isQid(V)
     , a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2))
     , a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2))
     , a__isNePal(V) -> a__isQid(V)
     , a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P))
     , a__isPal(V) -> a__isNePal(V)
     , a__isPal(nil()) -> tt()
     , a__isQid(a()) -> tt()
     , a__isQid(e()) -> tt()
     , a__isQid(i()) -> tt()
     , a__isQid(o()) -> tt()
     , a__isQid(u()) -> tt()
     , mark(__(X1, X2)) -> a____(mark(X1), mark(X2))
     , mark(and(X1, X2)) -> a__and(mark(X1), X2)
     , mark(isList(X)) -> a__isList(X)
     , mark(isNeList(X)) -> a__isNeList(X)
     , mark(isQid(X)) -> a__isQid(X)
     , mark(isNePal(X)) -> a__isNePal(X)
     , mark(isPal(X)) -> a__isPal(X)
     , mark(nil()) -> nil()
     , mark(tt()) -> tt()
     , mark(a()) -> a()
     , mark(e()) -> e()
     , mark(i()) -> i()
     , mark(o()) -> o()
     , mark(u()) -> u()
     , a____(X1, X2) -> __(X1, X2)
     , a__and(X1, X2) -> and(X1, X2)
     , a__isList(X) -> isList(X)
     , a__isNeList(X) -> isNeList(X)
     , a__isQid(X) -> isQid(X)
     , a__isNePal(X) -> isNePal(X)
     , a__isPal(X) -> isPal(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 GM

stdout:

MAYBE

Tool RC2

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

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z)))
     , a____(X, nil()) -> mark(X)
     , a____(nil(), X) -> mark(X)
     , a__and(tt(), X) -> mark(X)
     , a__isList(V) -> a__isNeList(V)
     , a__isList(nil()) -> tt()
     , a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2))
     , a__isNeList(V) -> a__isQid(V)
     , a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2))
     , a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2))
     , a__isNePal(V) -> a__isQid(V)
     , a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P))
     , a__isPal(V) -> a__isNePal(V)
     , a__isPal(nil()) -> tt()
     , a__isQid(a()) -> tt()
     , a__isQid(e()) -> tt()
     , a__isQid(i()) -> tt()
     , a__isQid(o()) -> tt()
     , a__isQid(u()) -> tt()
     , mark(__(X1, X2)) -> a____(mark(X1), mark(X2))
     , mark(and(X1, X2)) -> a__and(mark(X1), X2)
     , mark(isList(X)) -> a__isList(X)
     , mark(isNeList(X)) -> a__isNeList(X)
     , mark(isQid(X)) -> a__isQid(X)
     , mark(isNePal(X)) -> a__isNePal(X)
     , mark(isPal(X)) -> a__isPal(X)
     , mark(nil()) -> nil()
     , mark(tt()) -> tt()
     , mark(a()) -> a()
     , mark(e()) -> e()
     , mark(i()) -> i()
     , mark(o()) -> o()
     , mark(u()) -> u()
     , a____(X1, X2) -> __(X1, X2)
     , a__and(X1, X2) -> and(X1, X2)
     , a__isList(X) -> isList(X)
     , a__isNeList(X) -> isNeList(X)
     , a__isQid(X) -> isQid(X)
     , a__isNePal(X) -> isNePal(X)
     , a__isPal(X) -> isPal(X)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds