Problem Transformed CSR 04 Ex9 Luc06 GM

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex9 Luc06 GM

stdout:

YES(?,O(n^2))

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

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

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

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

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

              [0]
              [2]
     [a__b] = [0]
              [0],

                          [1 3 0 0]     [1 0 2 2]     [1 3 1 1]     [0]
                          [0 0 0 0]     [0 0 2 0]     [0 0 0 0]     [1]
     [a__f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 1]x1 + [0 0 0 0]x2 + [0]
                          [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0],

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

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

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

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

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

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

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

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

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

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

                            [1 1 0 0]     [1 1 0 0]     [1 0 0 2]     [0]
                            [0 0 0 0]     [0 0 1 0]     [0 0 0 0]     [0]
       [a__f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 3]x1 + [0 0 0 0]x2 + [2]
                            [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0],

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

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

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

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

                       [2 1 0 2]    [3]    [1 1 0 0]    [3]
                       [0 0 1 0]    [0]    [0 0 0 0]    [0]
       a__f(a(),X,X) = [0 0 0 3]X + [2] >= [0 0 0 0]X + [2] = a__f(X,a__b(),b())
                       [0 0 0 0]    [0]    [0 0 0 0]    [0]

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

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

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

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

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

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

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

                             [1 1 0]     [1 0 0]     [1 4 0]     [1]    [1 1 0]     [1 0 0]     [1 4 0]     [1]
         mark(f(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [0] = a__f(X1,mark(X2),X3)
                             [0 0 0]     [0 0 0]     [0 0 0]     [5]    [0 0 0]     [0 0 0]     [0 0 0]     [4]

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

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

                         [2 4 0]    [1]    [1 1 0]    [1]
         a__f(a(),X,X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__f(X,a__b(),b())
                         [0 0 0]    [4]    [0 0 0]    [4]

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

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

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

           [b] = 0,

           [a__b] = 0,

           [a__f](x0, x1, x2) = x0 + x1 + x2 + 173,

           [a] = 0
          orientation:
           mark(f(X1,X2,X3)) = X1 + X2 + X3 + 265 >= X1 + X2 + X3 + 197 = a__f(X1,mark(X2),X3)

           a__f(X1,X2,X3) = X1 + X2 + X3 + 173 >= X1 + X2 + X3 + 241 = f(X1,X2,X3)

           a__b() = 0 >= 0 = a()

           a__b() = 0 >= 0 = b()

           a__f(a(),X,X) = 2X + 173 >= X + 173 = a__f(X,a__b(),b())

           mark(b()) = 24 >= 0 = a__b()

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

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

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

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

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

                   [0]
                   [0]
             [a] = [1]
                   [1]
            orientation:
                              [1 0 0 1]     [1 1 0 0]     [1 0 0 1]     [1]    [1 0 0 1]     [1 1 0 0]     [1 0 0 0]     [0]
                              [0 0 1 1]     [0 0 1 0]     [0 0 0 1]     [1]    [0 0 0 0]     [0 0 1 0]     [0 0 0 0]     [1]
             a__f(X1,X2,X3) = [0 0 1 1]X1 + [0 0 1 0]X2 + [0 0 0 1]X3 + [1] >= [0 0 1 1]X1 + [0 0 1 0]X2 + [0 0 0 1]X3 + [1] = f(X1,X2,X3)
                              [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]    [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]

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

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

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

                             [2 1 0 1]    [2]    [1 0 0 1]    [1]
                             [0 0 1 1]    [3]    [0 0 1 1]    [2]
             a__f(a(),X,X) = [0 0 1 1]X + [3] >= [0 0 1 1]X + [2] = a__f(X,a__b(),b())
                             [0 0 0 0]    [0]    [0 0 0 0]    [0]

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

                         [2]    [0]
                         [1]    [0]
             mark(a()) = [1] >= [1] = a()
                         [1]    [1]
            problem:
             strict:

             weak:
              a__f(X1,X2,X3) -> f(X1,X2,X3)
              mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
              a__b() -> a()
              a__b() -> b()
              a__f(a(),X,X) -> a__f(X,a__b(),b())
              mark(b()) -> a__b()
              mark(a()) -> a()
            Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex9 Luc06 GM

stdout:

YES(?,O(n^2))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex9 Luc06 GM

stdout:

YES(?,O(n^1))

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

Proof Output:
  'matrix-interpretation of dimension 1' proved the best result:

  Details:
  --------
    'matrix-interpretation of dimension 1' succeeded with the following output:
     'matrix-interpretation of dimension 1'
     --------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  a__f(a(), X, X) -> a__f(X, a__b(), b())
          , a__b() -> a()
          , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3)
          , mark(b()) -> a__b()
          , mark(a()) -> a()
          , a__f(X1, X2, X3) -> f(X1, X2, X3)
          , a__b() -> b()}

     Proof Output:
       The following argument positions are usable:
         Uargs(a__f) = {2}, Uargs(mark) = {}, Uargs(f) = {}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        a__f(x1, x2, x3) = [2] x1 + [1] x2 + [4] x3 + [4]
        a() = [2]
        a__b() = [3]
        b() = [0]
        mark(x1) = [5] x1 + [4]
        f(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex9 Luc06 GM

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex9 Luc06 GM

stdout:

YES(?,O(n^1))

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

Proof Output:
  'matrix-interpretation of dimension 1' proved the best result:

  Details:
  --------
    'matrix-interpretation of dimension 1' succeeded with the following output:
     'matrix-interpretation of dimension 1'
     --------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  a__f(a(), X, X) -> a__f(X, a__b(), b())
          , a__b() -> a()
          , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3)
          , mark(b()) -> a__b()
          , mark(a()) -> a()
          , a__f(X1, X2, X3) -> f(X1, X2, X3)
          , a__b() -> b()}

     Proof Output:
       The following argument positions are usable:
         Uargs(a__f) = {2}, Uargs(mark) = {}, Uargs(f) = {2}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        a__f(x1, x2, x3) = [3] x1 + [1] x2 + [2] x3 + [4]
        a() = [2]
        a__b() = [3]
        b() = [1]
        mark(x1) = [5] x1 + [4]
        f(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]