Problem Transformed CSR 04 Ex5 Zan97 GM

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex5 Zan97 GM

stdout:

MAYBE

Problem:
a__f(X) -> a__if(mark(X),c(),f(true()))
a__if(true(),X,Y) -> mark(X)
a__if(false(),X,Y) -> mark(Y)
mark(f(X)) -> a__f(mark(X))
mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
mark(c()) -> c()
mark(true()) -> true()
mark(false()) -> false()
a__f(X) -> f(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)

Proof:
Complexity Transformation Processor:
  strict:
   a__f(X) -> a__if(mark(X),c(),f(true()))
   a__if(true(),X,Y) -> mark(X)
   a__if(false(),X,Y) -> mark(Y)
   mark(f(X)) -> a__f(mark(X))
   mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
   mark(c()) -> c()
   mark(true()) -> true()
   mark(false()) -> false()
   a__f(X) -> f(X)
   a__if(X1,X2,X3) -> if(X1,X2,X3)
  weak:

  Matrix Interpretation Processor:
   dimension: 3
   max_matrix:
    [1 3 2]
    [0 0 1]
    [0 0 0]
    interpretation:
                        [1 0 2]     [1 0 0]     [1 3 0]
     [if](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]
     [false] = [0]
               [0],

                           [1 0 2]     [1 0 1]     [1 3 0]
     [a__if](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 1 0]     [2]
     [f](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [0],

              [0]
     [true] = [0]
              [0],

           [0]
     [c] = [0]
           [0],

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

                  [1 2 1]     [2]
     [a__f](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [0]
    orientation:
               [1 2 1]    [2]    [1 0 0]    [2]
     a__f(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__if(mark(X),c(),f(true()))
               [0 0 0]    [0]    [0 0 0]    [0]

                         [1 0 1]    [1 3 0]     [1 0 0]
     a__if(true(),X,Y) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X = mark(X)
                         [0 0 0]    [0 0 0]     [0 0 0]

                          [1 0 1]    [1 3 0]    [1]    [1 0 0]
     a__if(false(),X,Y) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]Y = mark(Y)
                          [0 0 0]    [0 0 0]    [0]    [0 0 0]

                  [1 1 0]    [2]    [1 0 0]    [2]
     mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__f(mark(X))
                  [0 0 0]    [0]    [0 0 0]    [0]

                          [1 0 2]     [1 0 0]     [1 3 0]      [1 0 0]     [1 0 0]     [1 3 0]
     mark(if(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__if(mark(X1),mark(X2),X3)
                          [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]

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

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

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

               [1 2 1]    [2]    [1 1 0]    [2]
     a__f(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X)
               [0 0 0]    [0]    [0 0 0]    [0]

                       [1 0 2]     [1 0 1]     [1 3 0]      [1 0 2]     [1 0 0]     [1 3 0]
     a__if(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 = if(X1,X2,X3)
                       [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]
    problem:
     strict:
      a__f(X) -> a__if(mark(X),c(),f(true()))
      a__if(true(),X,Y) -> mark(X)
      mark(f(X)) -> a__f(mark(X))
      mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
      mark(c()) -> c()
      mark(true()) -> true()
      mark(false()) -> false()
      a__f(X) -> f(X)
      a__if(X1,X2,X3) -> if(X1,X2,X3)
     weak:
      a__if(false(),X,Y) -> mark(Y)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [if](x0, x1, x2) = x0 + x1 + x2 + 2,

       [false] = 0,

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

       [f](x0) = x0 + 13,

       [true] = 46,

       [c] = 1,

       [mark](x0) = x0 + 7,

       [a__f](x0) = x0 + 25
      orientation:
       a__f(X) = X + 25 >= X + 74 = a__if(mark(X),c(),f(true()))

       a__if(true(),X,Y) = X + Y + 53 >= X + 7 = mark(X)

       mark(f(X)) = X + 20 >= X + 32 = a__f(mark(X))

       mark(if(X1,X2,X3)) = X1 + X2 + X3 + 9 >= X1 + X2 + X3 + 21 = a__if(mark(X1),mark(X2),X3)

       mark(c()) = 8 >= 1 = c()

       mark(true()) = 53 >= 46 = true()

       mark(false()) = 7 >= 0 = false()

       a__f(X) = X + 25 >= X + 13 = f(X)

       a__if(X1,X2,X3) = X1 + X2 + X3 + 7 >= X1 + X2 + X3 + 2 = if(X1,X2,X3)

       a__if(false(),X,Y) = X + Y + 7 >= Y + 7 = mark(Y)
      problem:
       strict:
        a__f(X) -> a__if(mark(X),c(),f(true()))
        mark(f(X)) -> a__f(mark(X))
        mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
       weak:
        a__if(true(),X,Y) -> mark(X)
        mark(c()) -> c()
        mark(true()) -> true()
        mark(false()) -> false()
        a__f(X) -> f(X)
        a__if(X1,X2,X3) -> if(X1,X2,X3)
        a__if(false(),X,Y) -> mark(Y)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [if](x0, x1, x2) = x0 + x1 + x2,

         [false] = 16,

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

         [f](x0) = x0,

         [true] = 0,

         [c] = 96,

         [mark](x0) = x0,

         [a__f](x0) = x0 + 128
        orientation:
         a__f(X) = X + 128 >= X + 96 = a__if(mark(X),c(),f(true()))

         mark(f(X)) = X >= X + 128 = a__f(mark(X))

         mark(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__if(mark(X1),mark(X2),X3)

         a__if(true(),X,Y) = X + Y >= X = mark(X)

         mark(c()) = 96 >= 96 = c()

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

         mark(false()) = 16 >= 16 = false()

         a__f(X) = X + 128 >= X = f(X)

         a__if(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3)

         a__if(false(),X,Y) = X + Y + 16 >= Y = mark(Y)
        problem:
         strict:
          mark(f(X)) -> a__f(mark(X))
          mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
         weak:
          a__f(X) -> a__if(mark(X),c(),f(true()))
          a__if(true(),X,Y) -> mark(X)
          mark(c()) -> c()
          mark(true()) -> true()
          mark(false()) -> false()
          a__f(X) -> f(X)
          a__if(X1,X2,X3) -> if(X1,X2,X3)
          a__if(false(),X,Y) -> mark(Y)
        Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex5 Zan97 GM

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex5 Zan97 GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a__f(X) -> a__if(mark(X), c(), f(true()))
     , a__if(true(), X, Y) -> mark(X)
     , a__if(false(), X, Y) -> mark(Y)
     , mark(f(X)) -> a__f(mark(X))
     , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3)
     , mark(c()) -> c()
     , mark(true()) -> true()
     , mark(false()) -> false()
     , a__f(X) -> f(X)
     , a__if(X1, X2, X3) -> if(X1, X2, X3)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex5 Zan97 GM

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex5 Zan97 GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__f(X) -> a__if(mark(X), c(), f(true()))
     , a__if(true(), X, Y) -> mark(X)
     , a__if(false(), X, Y) -> mark(Y)
     , mark(f(X)) -> a__f(mark(X))
     , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3)
     , mark(c()) -> c()
     , mark(true()) -> true()
     , mark(false()) -> false()
     , a__f(X) -> f(X)
     , a__if(X1, X2, X3) -> if(X1, X2, X3)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds