Problem HirokawaMiddeldorp 04 t012

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t012

stdout:

MAYBE

Problem:
minus(minus(x)) -> x
minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))

Proof:
Complexity Transformation Processor:
  strict:
   minus(minus(x)) -> x
   minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
   minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
   f(minus(x)) -> minus(minus(minus(f(x))))
  weak:

  Bounds Processor:
   bound: 0
   enrichment: match
   automaton:
    final states: {4,3}
    transitions:
     minus0(25) -> 26*
     minus0(20) -> 27*
     minus0(27) -> 28*
     minus0(22) -> 23*
     minus0(17) -> 18*
     minus0(2) -> 3*
     minus0(29) -> 3*
     minus0(24) -> 25*
     minus0(19) -> 20*
     minus0(26) -> 3*
     minus0(21) -> 22*
     minus0(1) -> 3*
     minus0(28) -> 29*
     minus0(23) -> 3*
     minus0(18) -> 24,21
     minus0(3) -> 19,17
     +0(1,2) -> 1*
     +0(2,1) -> 1*
     +0(18,18) -> 3*
     +0(29,23) -> 27,21,24,19,17
     +0(1,1) -> 1*
     +0(2,2) -> 1*
     *0(23,23) -> 27,21,24,19
     *0(1,2) -> 2*
     *0(2,1) -> 2*
     *0(20,18) -> 3*
     *0(1,1) -> 2*
     *0(26,23) -> 17*
     *0(2,2) -> 2*
     f0(2) -> 4*
     f0(1) -> 4*
     1 -> 17,19
     2 -> 27,17,19
     3 -> 18,20
     17 -> 24,21
     18 -> 22,25
     19 -> 27*
     20 -> 28*
     21 -> 23*
     22 -> 3*
     23 -> 27*
     24 -> 26*
     25 -> 3*
     26 -> 27*
     27 -> 29*
     28 -> 3*
     29 -> 17,19,24,23,27
   problem:
    strict:
     minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
     minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
     minus(minus(x)) -> x
    weak:
     f(minus(x)) -> minus(minus(minus(f(x))))
   Matrix Interpretation Processor:
    dimension: 1
    max_matrix:
     1
     interpretation:
      [f](x0) = x0 + 12,

      [*](x0, x1) = x0 + x1 + 9,

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

      [minus](x0) = x0
     orientation:
      minus(+(x,y)) = x + y >= x + y + 9 = *(minus(minus(minus(x))),minus(minus(minus(y))))

      minus(*(x,y)) = x + y + 9 >= x + y = +(minus(minus(minus(x))),minus(minus(minus(y))))

      minus(minus(x)) = x >= x = x

      f(minus(x)) = x + 12 >= x + 12 = minus(minus(minus(f(x))))
     problem:
      strict:
       minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
       minus(minus(x)) -> x
      weak:
       minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
       f(minus(x)) -> minus(minus(minus(f(x))))
     Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t012

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t012

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  minus(minus(x)) -> x
     , minus(+(x, y)) ->
       *(minus(minus(minus(x))), minus(minus(minus(y))))
     , minus(*(x, y)) ->
       +(minus(minus(minus(x))), minus(minus(minus(y))))
     , f(minus(x)) -> minus(minus(minus(f(x))))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	HirokawaMiddeldorp 04 t012

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	HirokawaMiddeldorp 04 t012

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  minus(minus(x)) -> x
     , minus(+(x, y)) ->
       *(minus(minus(minus(x))), minus(minus(minus(y))))
     , minus(*(x, y)) ->
       +(minus(minus(minus(x))), minus(minus(minus(y))))
     , f(minus(x)) -> minus(minus(minus(f(x))))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds