Problem AProVE 04 Liveness6.1

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 Liveness6.1

stdout:

MAYBE

Problem:
 top(free(x)) -> top(check(new(x)))
 new(free(x)) -> free(new(x))
 old(free(x)) -> free(old(x))
 new(serve()) -> free(serve())
 old(serve()) -> free(serve())
 check(free(x)) -> free(check(x))
 check(new(x)) -> new(check(x))
 check(old(x)) -> old(check(x))
 check(old(x)) -> old(x)

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 Liveness6.1

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 04 Liveness6.1

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  top(free(x)) -> top(check(new(x)))
     , new(free(x)) -> free(new(x))
     , old(free(x)) -> free(old(x))
     , new(serve()) -> free(serve())
     , old(serve()) -> free(serve())
     , check(free(x)) -> free(check(x))
     , check(new(x)) -> new(check(x))
     , check(old(x)) -> old(check(x))
     , check(old(x)) -> old(x)}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 Liveness6.1

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 04 Liveness6.1

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  top(free(x)) -> top(check(new(x)))
     , new(free(x)) -> free(new(x))
     , old(free(x)) -> free(old(x))
     , new(serve()) -> free(serve())
     , old(serve()) -> free(serve())
     , check(free(x)) -> free(check(x))
     , check(new(x)) -> new(check(x))
     , check(old(x)) -> old(check(x))
     , check(old(x)) -> old(x)}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds