Problem Transformed CSR 04 PALINDROME nosorts noand GM

Tool CaT

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

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

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

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

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

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

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

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

                    [0]    [0]
     a__U11(tt()) = [0] >= [0] = a__U12(tt())
                    [0]    [0]

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

                    [1 0 0]     [1 0 0]
     mark(U12(X)) = [0 0 0]X >= [0 0 0]X = a__U12(mark(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(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 0 1]     [1 0 1]
     a__U11(X) = [0 0 0]X >= [0 0 0]X = U11(X)
                 [0 0 0]     [0 0 0]

                 [1 0 0]     [1 0 0]
     a__U12(X) = [0 0 0]X >= [0 0 0]X = U12(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]
    problem:
     strict:
      a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
      a__U11(tt()) -> a__U12(tt())
      a__U12(tt()) -> tt()
      mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
      mark(U11(X)) -> a__U11(mark(X))
      mark(U12(X)) -> a__U12(mark(X))
      mark(isNePal(X)) -> a__isNePal(mark(X))
      mark(nil()) -> nil()
      mark(tt()) -> tt()
      a____(X1,X2) -> __(X1,X2)
      a__U11(X) -> U11(X)
      a__U12(X) -> U12(X)
      a__isNePal(X) -> isNePal(X)
     weak:
      a____(X,nil()) -> mark(X)
      a____(nil(),X) -> mark(X)
      a__isNePal(__(I,__(P,I))) -> a__U11(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]
       [U12](x0) = [0 0 0]x0
                   [0 0 0]  ,

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

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

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

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

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

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

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

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

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

                   [1 0 0]     [1 0 0]
       a__U12(X) = [0 0 0]X >= [0 0 0]X = U12(X)
                   [0 0 0]     [0 0 0]

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

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

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

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

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

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

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

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

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

                     [1 0 0]    [1]    [1 0 0]    [1]
         a__U12(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = U12(X)
                     [0 0 0]    [0]    [0 0 0]    [0]

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

                        [1]    [1]
         a__U11(tt()) = [0] >= [0] = a__U12(tt())
                        [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]

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

           [U12](x0) = x0,

           [U11](x0) = x0 + 2,

           [a__isNePal](x0) = x0 + 45,

           [a__U12](x0) = x0 + 45,

           [a__U11](x0) = x0 + 45,

           [tt] = 4,

           [nil] = 1,

           [mark](x0) = x0,

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

           [__](x0, x1) = x0 + x1 + 32
          orientation:
           a____(__(X,Y),Z) = X + Y + Z + 38 >= X + Y + Z + 12 = a____(mark(X),a____(mark(Y),mark(Z)))

           mark(__(X1,X2)) = X1 + X2 + 32 >= X1 + X2 + 6 = a____(mark(X1),mark(X2))

           mark(U11(X)) = X + 2 >= X + 45 = a__U11(mark(X))

           mark(U12(X)) = X >= X + 45 = a__U12(mark(X))

           mark(isNePal(X)) = X + 53 >= X + 45 = a__isNePal(mark(X))

           mark(nil()) = 1 >= 1 = nil()

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

           a____(X1,X2) = X1 + X2 + 6 >= X1 + X2 + 32 = __(X1,X2)

           a__U11(X) = X + 45 >= X + 2 = U11(X)

           a__U12(X) = X + 45 >= X = U12(X)

           a__isNePal(X) = X + 45 >= X + 53 = isNePal(X)

           a__U12(tt()) = 49 >= 4 = tt()

           a__U11(tt()) = 49 >= 49 = a__U12(tt())

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

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

           a__isNePal(__(I,__(P,I))) = 2I + P + 109 >= 49 = a__U11(tt())
          problem:
           strict:
            mark(U11(X)) -> a__U11(mark(X))
            mark(U12(X)) -> a__U12(mark(X))
            mark(nil()) -> nil()
            mark(tt()) -> tt()
            a____(X1,X2) -> __(X1,X2)
            a__isNePal(X) -> isNePal(X)
           weak:
            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__U11(X) -> U11(X)
            a__U12(X) -> U12(X)
            a__U12(tt()) -> tt()
            a__U11(tt()) -> a__U12(tt())
            a____(X,nil()) -> mark(X)
            a____(nil(),X) -> mark(X)
            a__isNePal(__(I,__(P,I))) -> a__U11(tt())
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [isNePal](x0) = x0 + 164,

             [U12](x0) = x0,

             [U11](x0) = x0 + 48,

             [a__isNePal](x0) = x0 + 164,

             [a__U12](x0) = x0 + 112,

             [a__U11](x0) = x0 + 123,

             [tt] = 64,

             [nil] = 200,

             [mark](x0) = x0 + 14,

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

             [__](x0, x1) = x0 + x1 + 101
            orientation:
             mark(U11(X)) = X + 62 >= X + 137 = a__U11(mark(X))

             mark(U12(X)) = X + 14 >= X + 126 = a__U12(mark(X))

             mark(nil()) = 214 >= 200 = nil()

             mark(tt()) = 78 >= 64 = tt()

             a____(X1,X2) = X1 + X2 + 2 >= X1 + X2 + 101 = __(X1,X2)

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

             a____(__(X,Y),Z) = X + Y + Z + 103 >= X + Y + Z + 46 = a____(mark(X),a____(mark(Y),mark(Z)))

             mark(__(X1,X2)) = X1 + X2 + 115 >= X1 + X2 + 30 = a____(mark(X1),mark(X2))

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

             a__U11(X) = X + 123 >= X + 48 = U11(X)

             a__U12(X) = X + 112 >= X = U12(X)

             a__U12(tt()) = 176 >= 64 = tt()

             a__U11(tt()) = 187 >= 176 = a__U12(tt())

             a____(X,nil()) = X + 202 >= X + 14 = mark(X)

             a____(nil(),X) = X + 202 >= X + 14 = mark(X)

             a__isNePal(__(I,__(P,I))) = 2I + P + 366 >= 187 = a__U11(tt())
            problem:
             strict:
              mark(U11(X)) -> a__U11(mark(X))
              mark(U12(X)) -> a__U12(mark(X))
              a____(X1,X2) -> __(X1,X2)
              a__isNePal(X) -> isNePal(X)
             weak:
              mark(nil()) -> nil()
              mark(tt()) -> tt()
              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__U11(X) -> U11(X)
              a__U12(X) -> U12(X)
              a__U12(tt()) -> tt()
              a__U11(tt()) -> a__U12(tt())
              a____(X,nil()) -> mark(X)
              a____(nil(),X) -> mark(X)
              a__isNePal(__(I,__(P,I))) -> a__U11(tt())
            Open

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nosorts noand 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__U11(tt()) -> a__U12(tt())
     , a__U12(tt()) -> tt()
     , a__isNePal(__(I, __(P, I))) -> a__U11(tt())
     , mark(__(X1, X2)) -> a____(mark(X1), mark(X2))
     , mark(U11(X)) -> a__U11(mark(X))
     , mark(U12(X)) -> a__U12(mark(X))
     , mark(isNePal(X)) -> a__isNePal(mark(X))
     , mark(nil()) -> nil()
     , mark(tt()) -> tt()
     , a____(X1, X2) -> __(X1, X2)
     , a__U11(X) -> U11(X)
     , a__U12(X) -> U12(X)
     , 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 noand GM

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PALINDROME nosorts noand 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__U11(tt()) -> a__U12(tt())
     , a__U12(tt()) -> tt()
     , a__isNePal(__(I, __(P, I))) -> a__U11(tt())
     , mark(__(X1, X2)) -> a____(mark(X1), mark(X2))
     , mark(U11(X)) -> a__U11(mark(X))
     , mark(U12(X)) -> a__U12(mark(X))
     , mark(isNePal(X)) -> a__isNePal(mark(X))
     , mark(nil()) -> nil()
     , mark(tt()) -> tt()
     , a____(X1, X2) -> __(X1, X2)
     , a__U11(X) -> U11(X)
     , a__U12(X) -> U12(X)
     , a__isNePal(X) -> isNePal(X)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds