Problem Transformed CSR 04 Ex16 Luc06 GM

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex16 Luc06 GM

stdout:

MAYBE

Problem:
a__f(X,X) -> a__f(a(),b())
a__b() -> a()
mark(f(X1,X2)) -> a__f(mark(X1),X2)
mark(b()) -> a__b()
mark(a()) -> a()
a__f(X1,X2) -> f(X1,X2)
a__b() -> b()

Proof:
Complexity Transformation Processor:
  strict:
   a__f(X,X) -> a__f(a(),b())
   a__b() -> a()
   mark(f(X1,X2)) -> a__f(mark(X1),X2)
   mark(b()) -> a__b()
   mark(a()) -> a()
   a__f(X1,X2) -> f(X1,X2)
   a__b() -> b()
  weak:

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

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

              [0]
              [3]
     [a__b] = [0]
              [1],

           [0]
           [2]
     [b] = [0]
           [1],

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

                      [1 1 0 0]     [1 0 0 0]     [0]
                      [0 0 0 2]     [0 0 0 0]     [1]
     [a__f](x0, x1) = [0 0 0 2]x0 + [0 0 0 0]x1 + [0]
                      [0 0 0 0]     [0 0 0 0]     [1]
    orientation:
                 [2 1 0 0]    [0]    [0]
                 [0 0 0 2]    [1]    [1]
     a__f(X,X) = [0 0 0 2]X + [0] >= [0] = a__f(a(),b())
                 [0 0 0 0]    [1]    [1]

              [0]    [0]
              [3]    [0]
     a__b() = [0] >= [0] = a()
              [1]    [0]

                      [1 1 0 2]     [1 0 0 0]     [1]    [1 1 0 2]     [1 0 0 0]     [1]
                      [0 0 0 0]     [0 0 0 0]     [3]    [0 0 0 0]     [0 0 0 0]     [3]
     mark(f(X1,X2)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [2] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [2] = a__f(mark(X1),X2)
                      [0 0 0 0]     [0 0 0 0]     [1]    [0 0 0 0]     [0 0 0 0]     [1]

                 [2]    [0]
                 [3]    [3]
     mark(b()) = [2] >= [0] = a__b()
                 [1]    [1]

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

                   [1 1 0 0]     [1 0 0 0]     [0]    [1 1 0 0]     [1 0 0 0]     [0]
                   [0 0 0 2]     [0 0 0 0]     [1]    [0 0 0 2]     [0 0 0 0]     [1]
     a__f(X1,X2) = [0 0 0 2]X1 + [0 0 0 0]X2 + [0] >= [0 0 0 2]X1 + [0 0 0 0]X2 + [0] = f(X1,X2)
                   [0 0 0 0]     [0 0 0 0]     [1]    [0 0 0 0]     [0 0 0 0]     [1]

              [0]    [0]
              [3]    [2]
     a__b() = [0] >= [0] = b()
              [1]    [1]
    problem:
     strict:
      a__f(X,X) -> a__f(a(),b())
      a__b() -> a()
      mark(f(X1,X2)) -> a__f(mark(X1),X2)
      mark(a()) -> a()
      a__f(X1,X2) -> f(X1,X2)
      a__b() -> b()
     weak:
      mark(b()) -> a__b()
    Matrix Interpretation Processor:
     dimension: 4
     max_matrix:
      [1 2 2 2]
      [0 0 1 1]
      [0 0 0 0]
      [0 0 0 0]
      interpretation:
                    [1 0 0 0]     [3]
                    [0 0 0 1]     [1]
       [mark](x0) = [0 0 0 0]x0 + [3]
                    [0 0 0 0]     [2],

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

                [1]
                [1]
       [a__b] = [2]
                [2],

             [0]
             [0]
       [b] = [0]
             [0],

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

                        [1 0 0 0]     [1 2 2 2]     [0]
                        [0 0 1 0]     [0 0 0 0]     [0]
       [a__f](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0]
                        [0 0 0 0]     [0 0 0 0]     [2]
      orientation:
                   [2 2 2 2]    [0]    [0]
                   [0 0 1 0]    [0]    [0]
       a__f(X,X) = [0 0 0 0]X + [0] >= [0] = a__f(a(),b())
                   [0 0 0 0]    [2]    [2]

                [1]    [0]
                [1]    [0]
       a__b() = [2] >= [0] = a()
                [2]    [0]

                        [1 0 0 0]     [1 2 2 2]     [3]    [1 0 0 0]     [1 2 2 2]     [3]
                        [0 0 0 0]     [0 0 0 0]     [3]    [0 0 0 0]     [0 0 0 0]     [3]
       mark(f(X1,X2)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [3] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0] = a__f(mark(X1),X2)
                        [0 0 0 0]     [0 0 0 0]     [2]    [0 0 0 0]     [0 0 0 0]     [2]

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

                     [1 0 0 0]     [1 2 2 2]     [0]    [1 0 0 0]     [1 2 2 2]     [0]
                     [0 0 1 0]     [0 0 0 0]     [0]    [0 0 1 0]     [0 0 0 0]     [0]
       a__f(X1,X2) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0] = f(X1,X2)
                     [0 0 0 0]     [0 0 0 0]     [2]    [0 0 0 0]     [0 0 0 0]     [2]

                [1]    [0]
                [1]    [0]
       a__b() = [2] >= [0] = b()
                [2]    [0]

                   [3]    [1]
                   [1]    [1]
       mark(b()) = [3] >= [2] = a__b()
                   [2]    [2]
      problem:
       strict:
        a__f(X,X) -> a__f(a(),b())
        mark(f(X1,X2)) -> a__f(mark(X1),X2)
        a__f(X1,X2) -> f(X1,X2)
       weak:
        a__b() -> a()
        mark(a()) -> a()
        a__b() -> b()
        mark(b()) -> a__b()
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [mark](x0) = x0,

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

         [a__b] = 1,

         [b] = 1,

         [a] = 1,

         [a__f](x0, x1) = x0 + x1 + 23
        orientation:
         a__f(X,X) = 2X + 23 >= 25 = a__f(a(),b())

         mark(f(X1,X2)) = X1 + X2 >= X1 + X2 + 23 = a__f(mark(X1),X2)

         a__f(X1,X2) = X1 + X2 + 23 >= X1 + X2 = f(X1,X2)

         a__b() = 1 >= 1 = a()

         mark(a()) = 1 >= 1 = a()

         a__b() = 1 >= 1 = b()

         mark(b()) = 1 >= 1 = a__b()
        problem:
         strict:
          a__f(X,X) -> a__f(a(),b())
          mark(f(X1,X2)) -> a__f(mark(X1),X2)
         weak:
          a__f(X1,X2) -> f(X1,X2)
          a__b() -> a()
          mark(a()) -> a()
          a__b() -> b()
          mark(b()) -> a__b()
        Matrix Interpretation Processor:
         dimension: 4
         max_matrix:
          [1 0 1 1]
          [0 0 0 1]
          [0 0 1 1]
          [0 0 0 0]
          interpretation:
                        [1 0 1 0]
                        [0 0 0 0]
           [mark](x0) = [0 0 1 0]x0
                        [0 0 0 0]  ,

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

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

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

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

                            [1 0 0 1]     [1 0 0 1]     [1]
                            [0 0 0 1]     [0 0 0 0]     [0]
           [a__f](x0, x1) = [0 0 1 1]x0 + [0 0 0 1]x1 + [1]
                            [0 0 0 0]     [0 0 0 0]     [0]
          orientation:
                       [2 0 0 2]    [1]    [1]
                       [0 0 0 1]    [0]    [0]
           a__f(X,X) = [0 0 1 2]X + [1] >= [1] = a__f(a(),b())
                       [0 0 0 0]    [0]    [0]

                            [1 0 1 0]     [1 0 0 1]     [2]    [1 0 1 0]     [1 0 0 1]     [1]
                            [0 0 0 0]     [0 0 0 0]     [0]    [0 0 0 0]     [0 0 0 0]     [0]
           mark(f(X1,X2)) = [0 0 1 0]X1 + [0 0 0 1]X2 + [1] >= [0 0 1 0]X1 + [0 0 0 1]X2 + [1] = a__f(mark(X1),X2)
                            [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]     [1]    [1 0 0 0]     [1 0 0 0]     [1]
                         [0 0 0 1]     [0 0 0 0]     [0]    [0 0 0 0]     [0 0 0 0]     [0]
           a__f(X1,X2) = [0 0 1 1]X1 + [0 0 0 1]X2 + [1] >= [0 0 1 0]X1 + [0 0 0 1]X2 + [1] = f(X1,X2)
                         [0 0 0 0]     [0 0 0 0]     [0]    [0 0 0 0]     [0 0 0 0]     [0]

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

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

                    [0]    [0]
                    [0]    [0]
           a__b() = [1] >= [1] = b()
                    [0]    [0]

                       [1]    [0]
                       [0]    [0]
           mark(b()) = [1] >= [1] = a__b()
                       [0]    [0]
          problem:
           strict:
            a__f(X,X) -> a__f(a(),b())
           weak:
            mark(f(X1,X2)) -> a__f(mark(X1),X2)
            a__f(X1,X2) -> f(X1,X2)
            a__b() -> a()
            mark(a()) -> a()
            a__b() -> b()
            mark(b()) -> a__b()
          Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex16 Luc06 GM

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex16 Luc06 GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a__f(X, X) -> a__f(a(), b())
     , a__b() -> a()
     , mark(f(X1, X2)) -> a__f(mark(X1), X2)
     , mark(b()) -> a__b()
     , mark(a()) -> a()
     , a__f(X1, X2) -> f(X1, X2)
     , a__b() -> b()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex16 Luc06 GM

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex16 Luc06 GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__f(X, X) -> a__f(a(), b())
     , a__b() -> a()
     , mark(f(X1, X2)) -> a__f(mark(X1), X2)
     , mark(b()) -> a__b()
     , mark(a()) -> a()
     , a__f(X1, X2) -> f(X1, X2)
     , a__b() -> b()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds