Problem AProVE 04 Liveness6.4

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	AProVE 04 Liveness6.4

stdout:

MAYBE

Problem:
top1(free(x),y) -> top2(check(new(x)),y)
top1(free(x),y) -> top2(new(x),check(y))
top1(free(x),y) -> top2(check(x),new(y))
top1(free(x),y) -> top2(x,check(new(y)))
top2(x,free(y)) -> top1(check(new(x)),y)
top2(x,free(y)) -> top1(new(x),check(y))
top2(x,free(y)) -> top1(check(x),new(y))
top2(x,free(y)) -> top1(x,check(new(y)))
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 Time	Unknown
Answer	MAYBE
Input	AProVE 04 Liveness6.4

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AProVE 04 Liveness6.4

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  top1(free(x), y) -> top2(check(new(x)), y)
     , top1(free(x), y) -> top2(new(x), check(y))
     , top1(free(x), y) -> top2(check(x), new(y))
     , top1(free(x), y) -> top2(x, check(new(y)))
     , top2(x, free(y)) -> top1(check(new(x)), y)
     , top2(x, free(y)) -> top1(new(x), check(y))
     , top2(x, free(y)) -> top1(check(x), new(y))
     , top2(x, free(y)) -> top1(x, check(new(y)))
     , 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 Time	Unknown
Answer	MAYBE
Input	AProVE 04 Liveness6.4

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AProVE 04 Liveness6.4

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  top1(free(x), y) -> top2(check(new(x)), y)
     , top1(free(x), y) -> top2(new(x), check(y))
     , top1(free(x), y) -> top2(check(x), new(y))
     , top1(free(x), y) -> top2(x, check(new(y)))
     , top2(x, free(y)) -> top1(check(new(x)), y)
     , top2(x, free(y)) -> top1(new(x), check(y))
     , top2(x, free(y)) -> top1(check(x), new(y))
     , top2(x, free(y)) -> top1(x, check(new(y)))
     , 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