Problem Transformed CSR 04 PEANO nosorts noand GM

Tool CaT

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

stdout:

MAYBE

Problem:
a__U11(tt(),M,N) -> a__U12(tt(),M,N)
a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
a__plus(N,0()) -> mark(N)
a__plus(N,s(M)) -> a__U11(tt(),M,N)
mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
mark(tt()) -> tt()
mark(s(X)) -> s(mark(X))
mark(0()) -> 0()
a__U11(X1,X2,X3) -> U11(X1,X2,X3)
a__U12(X1,X2,X3) -> U12(X1,X2,X3)
a__plus(X1,X2) -> plus(X1,X2)

Proof:
Complexity Transformation Processor:
  strict:
   a__U11(tt(),M,N) -> a__U12(tt(),M,N)
   a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
   a__plus(N,0()) -> mark(N)
   a__plus(N,s(M)) -> a__U11(tt(),M,N)
   mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
   mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
   mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
   mark(tt()) -> tt()
   mark(s(X)) -> s(mark(X))
   mark(0()) -> 0()
   a__U11(X1,X2,X3) -> U11(X1,X2,X3)
   a__U12(X1,X2,X3) -> U12(X1,X2,X3)
   a__plus(X1,X2) -> plus(X1,X2)
  weak:

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

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

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

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

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

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

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

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

                            [1 0 1]     [1 0 0]     [1 0 0]
     [a__U11](x0, x1, x2) = [0 0 1]x0 + [0 0 0]x1 + [0 0 0]x2
                            [0 0 0]     [0 0 0]     [0 0 0]  ,

            [1]
     [tt] = [0]
            [0]
    orientation:
                        [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1]
     a__U11(tt(),M,N) = [0 0 0]M + [0 0 0]N + [0] >= [0 0 0]M + [0 0 0]N + [0] = a__U12(tt(),M,N)
                        [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__U12(tt(),M,N) = [0 0 0]M + [0 0 0]N + [0] >= [0 0 0]M + [0 0 0]N + [0] = s(a__plus(mark(N),mark(M)))
                        [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]

                      [1 1 0]    [2]    [1 0 0]
     a__plus(N,0()) = [0 0 0]N + [0] >= [0 0 0]N = mark(N)
                      [0 0 0]    [0]    [0 0 0]

                       [1 1 0]    [1 1 0]    [1]    [1 0 0]    [1 0 0]    [1]
     a__plus(N,s(M)) = [0 0 0]M + [0 0 0]N + [0] >= [0 0 0]M + [0 0 0]N + [0] = a__U11(tt(),M,N)
                       [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]

                           [1 0 1]     [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]     [1 0 0]
     mark(U11(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = a__U11(mark(X1),X2,X3)
                           [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                           [1 0 1]     [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]     [1 0 0]
     mark(U12(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = a__U12(mark(X1),X2,X3)
                           [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                         [1 1 0]     [1 0 1]     [1]    [1 0 0]     [1 0 0]     [1]
     mark(plus(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = a__plus(mark(X1),mark(X2))
                         [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]

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

                  [1 1 0]     [1 0 0]
     mark(s(X)) = [0 0 0]X >= [0 0 0]X = s(mark(X))
                  [0 0 0]     [0 0 0]

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

                        [1 0 1]     [1 0 0]     [1 0 0]      [1 0 1]     [1 0 0]     [1 0 0]
     a__U11(X1,X2,X3) = [0 0 1]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = U11(X1,X2,X3)
                        [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                        [1 0 1]     [1 0 0]     [1 0 0]      [1 0 1]     [1 0 0]     [1 0 0]
     a__U12(X1,X2,X3) = [0 0 1]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = U12(X1,X2,X3)
                        [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

                      [1 1 0]     [1 0 1]     [1]    [1 1 0]     [1 0 1]     [1]
     a__plus(X1,X2) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = plus(X1,X2)
                      [0 0 0]     [0 0 0]     [0]    [0 0 0]     [0 0 0]     [0]
    problem:
     strict:
      a__U11(tt(),M,N) -> a__U12(tt(),M,N)
      a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
      a__plus(N,s(M)) -> a__U11(tt(),M,N)
      mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
      mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
      mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
      mark(tt()) -> tt()
      mark(s(X)) -> s(mark(X))
      mark(0()) -> 0()
      a__U11(X1,X2,X3) -> U11(X1,X2,X3)
      a__U12(X1,X2,X3) -> U12(X1,X2,X3)
      a__plus(X1,X2) -> plus(X1,X2)
     weak:
      a__plus(N,0()) -> mark(N)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [plus](x0, x1) = x0 + x1,

       [U12](x0, x1, x2) = x0 + x1 + x2 + 1,

       [U11](x0, x1, x2) = x0 + x1 + x2,

       [0] = 6,

       [s](x0) = x0 + 3,

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

       [mark](x0) = x0 + 9,

       [a__U12](x0, x1, x2) = x0 + x1 + x2 + 7,

       [a__U11](x0, x1, x2) = x0 + x1 + x2,

       [tt] = 2
      orientation:
       a__U11(tt(),M,N) = M + N + 2 >= M + N + 9 = a__U12(tt(),M,N)

       a__U12(tt(),M,N) = M + N + 9 >= M + N + 24 = s(a__plus(mark(N),mark(M)))

       a__plus(N,s(M)) = M + N + 6 >= M + N + 2 = a__U11(tt(),M,N)

       mark(U11(X1,X2,X3)) = X1 + X2 + X3 + 9 >= X1 + X2 + X3 + 9 = a__U11(mark(X1),X2,X3)

       mark(U12(X1,X2,X3)) = X1 + X2 + X3 + 10 >= X1 + X2 + X3 + 16 = a__U12(mark(X1),X2,X3)

       mark(plus(X1,X2)) = X1 + X2 + 9 >= X1 + X2 + 21 = a__plus(mark(X1),mark(X2))

       mark(tt()) = 11 >= 2 = tt()

       mark(s(X)) = X + 12 >= X + 12 = s(mark(X))

       mark(0()) = 15 >= 6 = 0()

       a__U11(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = U11(X1,X2,X3)

       a__U12(X1,X2,X3) = X1 + X2 + X3 + 7 >= X1 + X2 + X3 + 1 = U12(X1,X2,X3)

       a__plus(X1,X2) = X1 + X2 + 3 >= X1 + X2 = plus(X1,X2)

       a__plus(N,0()) = N + 9 >= N + 9 = mark(N)
      problem:
       strict:
        a__U11(tt(),M,N) -> a__U12(tt(),M,N)
        a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
        mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
        mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
        mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
        mark(s(X)) -> s(mark(X))
        a__U11(X1,X2,X3) -> U11(X1,X2,X3)
       weak:
        a__plus(N,s(M)) -> a__U11(tt(),M,N)
        mark(tt()) -> tt()
        mark(0()) -> 0()
        a__U12(X1,X2,X3) -> U12(X1,X2,X3)
        a__plus(X1,X2) -> plus(X1,X2)
        a__plus(N,0()) -> mark(N)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [plus](x0, x1) = x0 + x1,

         [U12](x0, x1, x2) = x0 + x1 + x2,

         [U11](x0, x1, x2) = x0 + x1 + x2,

         [0] = 0,

         [s](x0) = x0 + 12,

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

         [mark](x0) = x0,

         [a__U12](x0, x1, x2) = x0 + x1 + x2,

         [a__U11](x0, x1, x2) = x0 + x1 + x2 + 11,

         [tt] = 1
        orientation:
         a__U11(tt(),M,N) = M + N + 12 >= M + N + 1 = a__U12(tt(),M,N)

         a__U12(tt(),M,N) = M + N + 1 >= M + N + 12 = s(a__plus(mark(N),mark(M)))

         mark(U11(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 + 11 = a__U11(mark(X1),X2,X3)

         mark(U12(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__U12(mark(X1),X2,X3)

         mark(plus(X1,X2)) = X1 + X2 >= X1 + X2 = a__plus(mark(X1),mark(X2))

         mark(s(X)) = X + 12 >= X + 12 = s(mark(X))

         a__U11(X1,X2,X3) = X1 + X2 + X3 + 11 >= X1 + X2 + X3 = U11(X1,X2,X3)

         a__plus(N,s(M)) = M + N + 12 >= M + N + 12 = a__U11(tt(),M,N)

         mark(tt()) = 1 >= 1 = tt()

         mark(0()) = 0 >= 0 = 0()

         a__U12(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = U12(X1,X2,X3)

         a__plus(X1,X2) = X1 + X2 >= X1 + X2 = plus(X1,X2)

         a__plus(N,0()) = N >= N = mark(N)
        problem:
         strict:
          a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
          mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
          mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
          mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
          mark(s(X)) -> s(mark(X))
         weak:
          a__U11(tt(),M,N) -> a__U12(tt(),M,N)
          a__U11(X1,X2,X3) -> U11(X1,X2,X3)
          a__plus(N,s(M)) -> a__U11(tt(),M,N)
          mark(tt()) -> tt()
          mark(0()) -> 0()
          a__U12(X1,X2,X3) -> U12(X1,X2,X3)
          a__plus(X1,X2) -> plus(X1,X2)
          a__plus(N,0()) -> mark(N)
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                                 [1 1]
           [plus](x0, x1) = x0 + [0 1]x1,

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

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

                 [0]
           [0] = [0],

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

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


           [mark](x0) = x0,

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

                                       [1 1]
           [a__U11](x0, x1, x2) = x0 + [0 1]x1 + x2,

                  [1]
           [tt] = [1]
          orientation:
                              [1 1]        [1]    [1 1]        [0]
           a__U12(tt(),M,N) = [0 1]M + N + [1] >= [0 1]M + N + [1] = s(a__plus(mark(N),mark(M)))

                                      [1 1]                [1 1]
           mark(U11(X1,X2,X3)) = X1 + [0 1]X2 + X3 >= X1 + [0 1]X2 + X3 = a__U11(mark(X1),X2,X3)

                                      [1 1]                [1 1]
           mark(U12(X1,X2,X3)) = X1 + [0 1]X2 + X3 >= X1 + [0 1]X2 + X3 = a__U12(mark(X1),X2,X3)

                                    [1 1]           [1 1]
           mark(plus(X1,X2)) = X1 + [0 1]X2 >= X1 + [0 1]X2 = a__plus(mark(X1),mark(X2))

                            [0]        [0]
           mark(s(X)) = X + [1] >= X + [1] = s(mark(X))

                              [1 1]        [1]    [1 1]        [1]
           a__U11(tt(),M,N) = [0 1]M + N + [1] >= [0 1]M + N + [1] = a__U12(tt(),M,N)

                                   [1 1]                [1 1]
           a__U11(X1,X2,X3) = X1 + [0 1]X2 + X3 >= X1 + [0 1]X2 + X3 = U11(X1,X2,X3)

                             [1 1]        [1]    [1 1]        [1]
           a__plus(N,s(M)) = [0 1]M + N + [1] >= [0 1]M + N + [1] = a__U11(tt(),M,N)

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

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

                                   [1 1]                [1 1]
           a__U12(X1,X2,X3) = X1 + [0 1]X2 + X3 >= X1 + [0 1]X2 + X3 = U12(X1,X2,X3)

                                 [1 1]           [1 1]
           a__plus(X1,X2) = X1 + [0 1]X2 >= X1 + [0 1]X2 = plus(X1,X2)


           a__plus(N,0()) = N >= N = mark(N)
          problem:
           strict:
            mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
            mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
            mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
            mark(s(X)) -> s(mark(X))
           weak:
            a__U12(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
            a__U11(tt(),M,N) -> a__U12(tt(),M,N)
            a__U11(X1,X2,X3) -> U11(X1,X2,X3)
            a__plus(N,s(M)) -> a__U11(tt(),M,N)
            mark(tt()) -> tt()
            mark(0()) -> 0()
            a__U12(X1,X2,X3) -> U12(X1,X2,X3)
            a__plus(X1,X2) -> plus(X1,X2)
            a__plus(N,0()) -> mark(N)
          Open

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PEANO nosorts noand GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a__U11(tt(), M, N) -> a__U12(tt(), M, N)
     , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M)))
     , a__plus(N, 0()) -> mark(N)
     , a__plus(N, s(M)) -> a__U11(tt(), M, N)
     , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3)
     , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3)
     , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
     , mark(tt()) -> tt()
     , mark(s(X)) -> s(mark(X))
     , mark(0()) -> 0()
     , a__U11(X1, X2, X3) -> U11(X1, X2, X3)
     , a__U12(X1, X2, X3) -> U12(X1, X2, X3)
     , a__plus(X1, X2) -> plus(X1, X2)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

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

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 PEANO nosorts noand GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__U11(tt(), M, N) -> a__U12(tt(), M, N)
     , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M)))
     , a__plus(N, 0()) -> mark(N)
     , a__plus(N, s(M)) -> a__U11(tt(), M, N)
     , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3)
     , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3)
     , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
     , mark(tt()) -> tt()
     , mark(s(X)) -> s(mark(X))
     , mark(0()) -> 0()
     , a__U11(X1, X2, X3) -> U11(X1, X2, X3)
     , a__U12(X1, X2, X3) -> U12(X1, X2, X3)
     , a__plus(X1, X2) -> plus(X1, X2)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds