Problem Transformed CSR 04 PALINDROME nosorts GM

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 PALINDROME nosorts 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__isNePal(__(I,__(P,I))) -> tt()
mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
mark(and(X1,X2)) -> a__and(mark(X1),X2)
mark(isNePal(X)) -> a__isNePal(mark(X))
mark(nil()) -> nil()
mark(tt()) -> tt()
a____(X1,X2) -> __(X1,X2)
a__and(X1,X2) -> and(X1,X2)
a__isNePal(X) -> isNePal(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__isNePal(__(I,__(P,I))) -> tt()
   mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
   mark(and(X1,X2)) -> a__and(mark(X1),X2)
   mark(isNePal(X)) -> a__isNePal(mark(X))
   mark(nil()) -> nil()
   mark(tt()) -> tt()
   a____(X1,X2) -> __(X1,X2)
   a__and(X1,X2) -> and(X1,X2)
   a__isNePal(X) -> isNePal(X)
  weak:

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

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

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

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

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

                    [1 0 0]     [1 0 0]
     [__](x0, x1) = [0 0 0]x0 + [0 0 1]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 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 0 0]     [1 0 0]
     a____(X,nil()) = [0 0 0]X >= [0 0 0]X = mark(X)
                      [0 0 0]     [0 0 0]

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

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

                                 [2 0 0]    [1 0 0]    [1]    [1]
     a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P + [0] >= [0] = tt()
                                 [0 0 0]    [0 0 0]    [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 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [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 1]    [1]    [1 0 0]    [1]
     mark(isNePal(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__isNePal(mark(X))
                        [0 0 0]    [0]    [0 0 0]    [0]

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

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

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

                     [1 0 1]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [1]
     a__and(X1,X2) = [0 0 1]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 1]    [1]    [1 0 1]    [1]
     a__isNePal(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = isNePal(X)
                     [0 0 0]    [0]    [0 0 0]    [0]
    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__isNePal(__(I,__(P,I))) -> tt()
      mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
      mark(and(X1,X2)) -> a__and(mark(X1),X2)
      mark(isNePal(X)) -> a__isNePal(mark(X))
      mark(nil()) -> nil()
      mark(tt()) -> tt()
      a____(X1,X2) -> __(X1,X2)
      a__and(X1,X2) -> and(X1,X2)
      a__isNePal(X) -> isNePal(X)
     weak:
      a__and(tt(),X) -> mark(X)
    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 1 0]     [1 0 0]     [1]
       [and](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                       [0 0 0]     [0 0 0]     [0],

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

                          [1 1 0]     [1 0 0]     [1]
       [a__and](x0, x1) = [0 0 1]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 1]
       [a____](x0, x1) = [0 0 1]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 1]     [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 0 0]    [1]    [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 1]    [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]

                                   [2 0 0]    [1 0 0]     [0]
       a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P >= [0] = tt()
                                   [0 0 0]    [0 0 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 1 0]     [1 0 0]     [1]    [1 0 0]     [1 0 0]     [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(isNePal(X)) = [0 0 0]X >= [0 0 0]X = a__isNePal(mark(X))
                          [0 0 0]     [0 0 0]

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

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

                      [1 0 0]     [1 0 1]      [1 0 0]     [1 0 0]
       a____(X1,X2) = [0 0 1]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 1 0]     [1 0 0]     [1]    [1 1 0]     [1 0 0]     [1]
       a__and(X1,X2) = [0 0 1]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__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]
       a__and(tt(),X) = [0 0 0]X + [0] >= [0 0 0]X = mark(X)
                        [0 0 0]    [0]    [0 0 0]
      problem:
       strict:
        a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
        a__isNePal(__(I,__(P,I))) -> tt()
        mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
        mark(and(X1,X2)) -> a__and(mark(X1),X2)
        mark(isNePal(X)) -> a__isNePal(mark(X))
        mark(nil()) -> nil()
        mark(tt()) -> tt()
        a____(X1,X2) -> __(X1,X2)
        a__and(X1,X2) -> and(X1,X2)
        a__isNePal(X) -> isNePal(X)
       weak:
        a____(X,nil()) -> mark(X)
        a____(nil(),X) -> mark(X)
        a__and(tt(),X) -> mark(X)
      Matrix Interpretation Processor:
       dimension: 3
       max_matrix:
        [1 1 1]
        [0 0 0]
        [0 0 0]
        interpretation:
                         [1 0 0]
         [isNePal](x0) = [0 0 0]x0
                         [0 0 0]  ,

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

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

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

                                     [2 0 0]    [1 0 0]    [2]    [0]
         a__isNePal(__(I,__(P,I))) = [0 0 0]I + [0 0 0]P + [0] >= [0] = tt()
                                     [0 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 1]     [1 1 1]      [1 0 0]     [1 1 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 0 0]
         mark(isNePal(X)) = [0 0 0]X >= [0 0 0]X = a__isNePal(mark(X))
                            [0 0 0]     [0 0 0]

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

                      [0]    [0]
         mark(tt()) = [0] >= [0] = tt()
                      [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 1]     [1 1 1]      [1 1 1]     [1 1 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 1 1]     [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]    [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 0]X + [0] >= [0 0 0]X = mark(X)
                          [0 0 0]    [0]    [0 0 0]

                          [1 1 1]     [1 0 0]
         a__and(tt(),X) = [0 0 0]X >= [0 0 0]X = mark(X)
                          [0 0 0]     [0 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(isNePal(X)) -> a__isNePal(mark(X))
          mark(nil()) -> nil()
          mark(tt()) -> tt()
          a____(X1,X2) -> __(X1,X2)
          a__and(X1,X2) -> and(X1,X2)
          a__isNePal(X) -> isNePal(X)
         weak:
          a__isNePal(__(I,__(P,I))) -> tt()
          a____(X,nil()) -> mark(X)
          a____(nil(),X) -> mark(X)
          a__and(tt(),X) -> mark(X)
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [isNePal](x0) = x0 + 8,

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

           [a__isNePal](x0) = x0 + 9,

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

           [tt] = 15,

           [nil] = 12,

           [mark](x0) = x0 + 17,

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

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

           mark(__(X1,X2)) = X1 + X2 + 25 >= X1 + X2 + 39 = a____(mark(X1),mark(X2))

           mark(and(X1,X2)) = X1 + X2 + 37 >= X1 + X2 + 19 = a__and(mark(X1),X2)

           mark(isNePal(X)) = X + 25 >= X + 26 = a__isNePal(mark(X))

           mark(nil()) = 29 >= 12 = nil()

           mark(tt()) = 32 >= 15 = tt()

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

           a__and(X1,X2) = X1 + X2 + 2 >= X1 + X2 + 20 = and(X1,X2)

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

           a__isNePal(__(I,__(P,I))) = 2I + P + 25 >= 15 = tt()

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

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

           a__and(tt(),X) = X + 17 >= X + 17 = mark(X)
          problem:
           strict:
            a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
            mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
            mark(isNePal(X)) -> a__isNePal(mark(X))
            a____(X1,X2) -> __(X1,X2)
            a__and(X1,X2) -> and(X1,X2)
           weak:
            mark(and(X1,X2)) -> a__and(mark(X1),X2)
            mark(nil()) -> nil()
            mark(tt()) -> tt()
            a__isNePal(X) -> isNePal(X)
            a__isNePal(__(I,__(P,I))) -> tt()
            a____(X,nil()) -> mark(X)
            a____(nil(),X) -> mark(X)
            a__and(tt(),X) -> mark(X)
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [isNePal](x0) = x0,

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

             [a__isNePal](x0) = x0 + 129,

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

             [tt] = 224,

             [nil] = 9,

             [mark](x0) = x0 + 4,

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

             [__](x0, x1) = x0 + x1 + 76
            orientation:
             a____(__(X,Y),Z) = X + Y + Z + 91 >= X + Y + Z + 42 = a____(mark(X),a____(mark(Y),mark(Z)))

             mark(__(X1,X2)) = X1 + X2 + 80 >= X1 + X2 + 23 = a____(mark(X1),mark(X2))

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

             a____(X1,X2) = X1 + X2 + 15 >= X1 + X2 + 76 = __(X1,X2)

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

             mark(and(X1,X2)) = X1 + X2 + 5 >= X1 + X2 + 5 = a__and(mark(X1),X2)

             mark(nil()) = 13 >= 9 = nil()

             mark(tt()) = 228 >= 224 = tt()

             a__isNePal(X) = X + 129 >= X = isNePal(X)

             a__isNePal(__(I,__(P,I))) = 2I + P + 281 >= 224 = tt()

             a____(X,nil()) = X + 24 >= X + 4 = mark(X)

             a____(nil(),X) = X + 24 >= X + 4 = mark(X)

             a__and(tt(),X) = X + 225 >= X + 4 = mark(X)
            problem:
             strict:
              mark(isNePal(X)) -> a__isNePal(mark(X))
              a____(X1,X2) -> __(X1,X2)
              a__and(X1,X2) -> and(X1,X2)
             weak:
              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(nil()) -> nil()
              mark(tt()) -> tt()
              a__isNePal(X) -> isNePal(X)
              a__isNePal(__(I,__(P,I))) -> tt()
              a____(X,nil()) -> mark(X)
              a____(nil(),X) -> mark(X)
              a__and(tt(),X) -> mark(X)
            Open

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nosorts 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__isNePal(__(I, __(P, I))) -> tt()
     , mark(__(X1, X2)) -> a____(mark(X1), mark(X2))
     , mark(and(X1, X2)) -> a__and(mark(X1), X2)
     , mark(isNePal(X)) -> a__isNePal(mark(X))
     , mark(nil()) -> nil()
     , mark(tt()) -> tt()
     , a____(X1, X2) -> __(X1, X2)
     , a__and(X1, X2) -> and(X1, X2)
     , a__isNePal(X) -> isNePal(X)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

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

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nosorts 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__isNePal(__(I, __(P, I))) -> tt()
     , mark(__(X1, X2)) -> a____(mark(X1), mark(X2))
     , mark(and(X1, X2)) -> a__and(mark(X1), X2)
     , mark(isNePal(X)) -> a__isNePal(mark(X))
     , mark(nil()) -> nil()
     , mark(tt()) -> tt()
     , a____(X1, X2) -> __(X1, X2)
     , a__and(X1, X2) -> and(X1, X2)
     , a__isNePal(X) -> isNePal(X)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds