Problem AProVE 06 tower sizeChange

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	AProVE 06 tower sizeChange

stdout:

MAYBE

Problem:
tower(x) -> f(a(),x,s(0()))
f(a(),0(),y) -> y
f(a(),s(x),y) -> f(b(),y,s(x))
f(b(),y,x) -> f(a(),half(x),exp(y))
exp(0()) -> s(0())
exp(s(x)) -> double(exp(x))
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
half(0()) -> double(0())
half(s(0())) -> half(0())
half(s(s(x))) -> s(half(x))

Proof:
Complexity Transformation Processor:
  strict:
   tower(x) -> f(a(),x,s(0()))
   f(a(),0(),y) -> y
   f(a(),s(x),y) -> f(b(),y,s(x))
   f(b(),y,x) -> f(a(),half(x),exp(y))
   exp(0()) -> s(0())
   exp(s(x)) -> double(exp(x))
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   half(0()) -> double(0())
   half(s(0())) -> half(0())
   half(s(s(x))) -> s(half(x))
  weak:

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

     [exp](x0) = x0 + 14,

     [half](x0) = x0 + 89,

     [b] = 44,

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

     [s](x0) = x0 + 49,

     [0] = 83,

     [a] = 11,

     [tower](x0) = x0
    orientation:
     tower(x) = x >= x + 168 = f(a(),x,s(0()))

     f(a(),0(),y) = y + 119 >= y = y

     f(a(),s(x),y) = x + y + 85 >= x + y + 118 = f(b(),y,s(x))

     f(b(),y,x) = x + y + 69 >= x + y + 139 = f(a(),half(x),exp(y))

     exp(0()) = 97 >= 132 = s(0())

     exp(s(x)) = x + 63 >= x + 38 = double(exp(x))

     double(0()) = 107 >= 83 = 0()

     double(s(x)) = x + 73 >= x + 122 = s(s(double(x)))

     half(0()) = 172 >= 107 = double(0())

     half(s(0())) = 221 >= 172 = half(0())

     half(s(s(x))) = x + 187 >= x + 138 = s(half(x))
    problem:
     strict:
      tower(x) -> f(a(),x,s(0()))
      f(a(),s(x),y) -> f(b(),y,s(x))
      f(b(),y,x) -> f(a(),half(x),exp(y))
      exp(0()) -> s(0())
      double(s(x)) -> s(s(double(x)))
     weak:
      f(a(),0(),y) -> y
      exp(s(x)) -> double(exp(x))
      double(0()) -> 0()
      half(0()) -> double(0())
      half(s(0())) -> half(0())
      half(s(s(x))) -> s(half(x))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [double](x0) = x0 + 2,

       [exp](x0) = x0 + 5,

       [half](x0) = x0 + 8,

       [b] = 6,

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

       [s](x0) = x0 + 2,

       [0] = 0,

       [a] = 0,

       [tower](x0) = x0
      orientation:
       tower(x) = x >= x + 2 = f(a(),x,s(0()))

       f(a(),s(x),y) = x + y + 2 >= x + y + 8 = f(b(),y,s(x))

       f(b(),y,x) = x + y + 6 >= x + y + 13 = f(a(),half(x),exp(y))

       exp(0()) = 5 >= 2 = s(0())

       double(s(x)) = x + 4 >= x + 6 = s(s(double(x)))

       f(a(),0(),y) = y >= y = y

       exp(s(x)) = x + 7 >= x + 7 = double(exp(x))

       double(0()) = 2 >= 0 = 0()

       half(0()) = 8 >= 2 = double(0())

       half(s(0())) = 10 >= 8 = half(0())

       half(s(s(x))) = x + 12 >= x + 10 = s(half(x))
      problem:
       strict:
        tower(x) -> f(a(),x,s(0()))
        f(a(),s(x),y) -> f(b(),y,s(x))
        f(b(),y,x) -> f(a(),half(x),exp(y))
        double(s(x)) -> s(s(double(x)))
       weak:
        exp(0()) -> s(0())
        f(a(),0(),y) -> y
        exp(s(x)) -> double(exp(x))
        double(0()) -> 0()
        half(0()) -> double(0())
        half(s(0())) -> half(0())
        half(s(s(x))) -> s(half(x))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [double](x0) = x0 + 60,

         [exp](x0) = x0 + 211,

         [half](x0) = x0 + 73,

         [b] = 0,

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

         [s](x0) = x0 + 129,

         [0] = 68,

         [a] = 4,

         [tower](x0) = x0
        orientation:
         tower(x) = x >= x + 219 = f(a(),x,s(0()))

         f(a(),s(x),y) = x + y + 151 >= x + y + 147 = f(b(),y,s(x))

         f(b(),y,x) = x + y + 18 >= x + y + 306 = f(a(),half(x),exp(y))

         double(s(x)) = x + 189 >= x + 318 = s(s(double(x)))

         exp(0()) = 279 >= 197 = s(0())

         f(a(),0(),y) = y + 90 >= y = y

         exp(s(x)) = x + 340 >= x + 271 = double(exp(x))

         double(0()) = 128 >= 68 = 0()

         half(0()) = 141 >= 128 = double(0())

         half(s(0())) = 270 >= 141 = half(0())

         half(s(s(x))) = x + 331 >= x + 202 = s(half(x))
        problem:
         strict:
          tower(x) -> f(a(),x,s(0()))
          f(b(),y,x) -> f(a(),half(x),exp(y))
          double(s(x)) -> s(s(double(x)))
         weak:
          f(a(),s(x),y) -> f(b(),y,s(x))
          exp(0()) -> s(0())
          f(a(),0(),y) -> y
          exp(s(x)) -> double(exp(x))
          double(0()) -> 0()
          half(0()) -> double(0())
          half(s(0())) -> half(0())
          half(s(s(x))) -> s(half(x))
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [double](x0) = x0 + 6,

           [exp](x0) = x0 + 8,

           [half](x0) = x0 + 17,

           [b] = 1,

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

           [s](x0) = x0 + 8,

           [0] = 20,

           [a] = 1,

           [tower](x0) = x0 + 103
          orientation:
           tower(x) = x + 103 >= x + 102 = f(a(),x,s(0()))

           f(b(),y,x) = x + y + 74 >= x + y + 99 = f(a(),half(x),exp(y))

           double(s(x)) = x + 14 >= x + 22 = s(s(double(x)))

           f(a(),s(x),y) = x + y + 82 >= x + y + 82 = f(b(),y,s(x))

           exp(0()) = 28 >= 28 = s(0())

           f(a(),0(),y) = y + 94 >= y = y

           exp(s(x)) = x + 16 >= x + 14 = double(exp(x))

           double(0()) = 26 >= 20 = 0()

           half(0()) = 37 >= 26 = double(0())

           half(s(0())) = 45 >= 37 = half(0())

           half(s(s(x))) = x + 33 >= x + 25 = s(half(x))
          problem:
           strict:
            f(b(),y,x) -> f(a(),half(x),exp(y))
            double(s(x)) -> s(s(double(x)))
           weak:
            tower(x) -> f(a(),x,s(0()))
            f(a(),s(x),y) -> f(b(),y,s(x))
            exp(0()) -> s(0())
            f(a(),0(),y) -> y
            exp(s(x)) -> double(exp(x))
            double(0()) -> 0()
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
          Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	AProVE 06 tower sizeChange

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AProVE 06 tower sizeChange

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  tower(x) -> f(a(), x, s(0()))
     , f(a(), 0(), y) -> y
     , f(a(), s(x), y) -> f(b(), y, s(x))
     , f(b(), y, x) -> f(a(), half(x), exp(y))
     , exp(0()) -> s(0())
     , exp(s(x)) -> double(exp(x))
     , double(0()) -> 0()
     , double(s(x)) -> s(s(double(x)))
     , half(0()) -> double(0())
     , half(s(0())) -> half(0())
     , half(s(s(x))) -> s(half(x))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	AProVE 06 tower sizeChange

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AProVE 06 tower sizeChange

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  tower(x) -> f(a(), x, s(0()))
     , f(a(), 0(), y) -> y
     , f(a(), s(x), y) -> f(b(), y, s(x))
     , f(b(), y, x) -> f(a(), half(x), exp(y))
     , exp(0()) -> s(0())
     , exp(s(x)) -> double(exp(x))
     , double(0()) -> 0()
     , double(s(x)) -> s(s(double(x)))
     , half(0()) -> double(0())
     , half(s(0())) -> half(0())
     , half(s(s(x))) -> s(half(x))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds