Problem Secret 05 SRS aprove1

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 SRS aprove1

stdout:

MAYBE

Problem:
p(0(x1)) -> 0(s(s(p(x1))))
p(s(x1)) -> x1
p(p(s(x1))) -> p(x1)
f(s(x1)) -> g(s(x1))
g(x1) -> i(s(half(x1)))
i(x1) -> f(p(x1))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
0(x1) -> x1
rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))

Proof:
Complexity Transformation Processor:
  strict:
   p(0(x1)) -> 0(s(s(p(x1))))
   p(s(x1)) -> x1
   p(p(s(x1))) -> p(x1)
   f(s(x1)) -> g(s(x1))
   g(x1) -> i(s(half(x1)))
   i(x1) -> f(p(x1))
   half(0(x1)) -> 0(s(s(half(x1))))
   half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
   0(x1) -> x1
   rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [rd](x0) = x0 + 8,

     [i](x0) = x0 + 16,

     [half](x0) = x0 + 16,

     [g](x0) = x0 + 8,

     [f](x0) = x0,

     [s](x0) = x0,

     [p](x0) = x0 + 15,

     [0](x0) = x0
    orientation:
     p(0(x1)) = x1 + 15 >= x1 + 15 = 0(s(s(p(x1))))

     p(s(x1)) = x1 + 15 >= x1 = x1

     p(p(s(x1))) = x1 + 30 >= x1 + 15 = p(x1)

     f(s(x1)) = x1 >= x1 + 8 = g(s(x1))

     g(x1) = x1 + 8 >= x1 + 32 = i(s(half(x1)))

     i(x1) = x1 + 16 >= x1 + 15 = f(p(x1))

     half(0(x1)) = x1 + 16 >= x1 + 16 = 0(s(s(half(x1))))

     half(s(s(x1))) = x1 + 16 >= x1 + 46 = s(half(p(p(s(s(x1))))))

     0(x1) = x1 >= x1 = x1

     rd(0(x1)) = x1 + 8 >= x1 + 8 = 0(0(0(0(0(0(rd(x1)))))))
    problem:
     strict:
      p(0(x1)) -> 0(s(s(p(x1))))
      f(s(x1)) -> g(s(x1))
      g(x1) -> i(s(half(x1)))
      half(0(x1)) -> 0(s(s(half(x1))))
      half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
      0(x1) -> x1
      rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
     weak:
      p(s(x1)) -> x1
      p(p(s(x1))) -> p(x1)
      i(x1) -> f(p(x1))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [rd](x0) = x0 + 7,

       [i](x0) = x0 + 1,

       [half](x0) = x0 + 28,

       [g](x0) = x0,

       [f](x0) = x0 + 1,

       [s](x0) = x0,

       [p](x0) = x0,

       [0](x0) = x0
      orientation:
       p(0(x1)) = x1 >= x1 = 0(s(s(p(x1))))

       f(s(x1)) = x1 + 1 >= x1 = g(s(x1))

       g(x1) = x1 >= x1 + 29 = i(s(half(x1)))

       half(0(x1)) = x1 + 28 >= x1 + 28 = 0(s(s(half(x1))))

       half(s(s(x1))) = x1 + 28 >= x1 + 28 = s(half(p(p(s(s(x1))))))

       0(x1) = x1 >= x1 = x1

       rd(0(x1)) = x1 + 7 >= x1 + 7 = 0(0(0(0(0(0(rd(x1)))))))

       p(s(x1)) = x1 >= x1 = x1

       p(p(s(x1))) = x1 >= x1 = p(x1)

       i(x1) = x1 + 1 >= x1 + 1 = f(p(x1))
      problem:
       strict:
        p(0(x1)) -> 0(s(s(p(x1))))
        g(x1) -> i(s(half(x1)))
        half(0(x1)) -> 0(s(s(half(x1))))
        half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
        0(x1) -> x1
        rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
       weak:
        f(s(x1)) -> g(s(x1))
        p(s(x1)) -> x1
        p(p(s(x1))) -> p(x1)
        i(x1) -> f(p(x1))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [rd](x0) = x0 + 7,

         [i](x0) = x0 + 10,

         [half](x0) = x0 + 32,

         [g](x0) = x0,

         [f](x0) = x0,

         [s](x0) = x0,

         [p](x0) = x0,

         [0](x0) = x0 + 40
        orientation:
         p(0(x1)) = x1 + 40 >= x1 + 40 = 0(s(s(p(x1))))

         g(x1) = x1 >= x1 + 42 = i(s(half(x1)))

         half(0(x1)) = x1 + 72 >= x1 + 72 = 0(s(s(half(x1))))

         half(s(s(x1))) = x1 + 32 >= x1 + 32 = s(half(p(p(s(s(x1))))))

         0(x1) = x1 + 40 >= x1 = x1

         rd(0(x1)) = x1 + 47 >= x1 + 247 = 0(0(0(0(0(0(rd(x1)))))))

         f(s(x1)) = x1 >= x1 = g(s(x1))

         p(s(x1)) = x1 >= x1 = x1

         p(p(s(x1))) = x1 >= x1 = p(x1)

         i(x1) = x1 + 10 >= x1 = f(p(x1))
        problem:
         strict:
          p(0(x1)) -> 0(s(s(p(x1))))
          g(x1) -> i(s(half(x1)))
          half(0(x1)) -> 0(s(s(half(x1))))
          half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
          rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))
         weak:
          0(x1) -> x1
          f(s(x1)) -> g(s(x1))
          p(s(x1)) -> x1
          p(p(s(x1))) -> p(x1)
          i(x1) -> f(p(x1))
        Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 SRS aprove1

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 05 SRS aprove1

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  p(0(x1)) -> 0(s(s(p(x1))))
     , p(s(x1)) -> x1
     , p(p(s(x1))) -> p(x1)
     , f(s(x1)) -> g(s(x1))
     , g(x1) -> i(s(half(x1)))
     , i(x1) -> f(p(x1))
     , half(0(x1)) -> 0(s(s(half(x1))))
     , half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
     , 0(x1) -> x1
     , rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Secret 05 SRS aprove1

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Secret 05 SRS aprove1

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  p(0(x1)) -> 0(s(s(p(x1))))
     , p(s(x1)) -> x1
     , p(p(s(x1))) -> p(x1)
     , f(s(x1)) -> g(s(x1))
     , g(x1) -> i(s(half(x1)))
     , i(x1) -> f(p(x1))
     , half(0(x1)) -> 0(s(s(half(x1))))
     , half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
     , 0(x1) -> x1
     , rd(0(x1)) -> 0(0(0(0(0(0(rd(x1)))))))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds