Problem AProVE 04 Liveness6.1

Tool Bounds

Execution Time	60.056755ms
Answer	TIMEOUT
Input	AProVE 04 Liveness6.1

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  check(old(x)) -> old(x)
     , check(old(x)) -> old(check(x))
     , check(new(x)) -> new(check(x))
     , check(free(x)) -> free(check(x))
     , old(serve()) -> free(serve())
     , new(serve()) -> free(serve())
     , old(free(x)) -> free(old(x))
     , new(free(x)) -> free(new(x))
     , top(free(x)) -> top(check(new(x)))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time	0.7571399ms
Answer	MAYBE
Input	AProVE 04 Liveness6.1

stdout:

MAYBE

Statistics:
Number of monomials: 384
Last formula building started for bound 3
Last SAT solving started for bound 3

Tool EDA

Execution Time	60.032566ms
Answer	TIMEOUT
Input	AProVE 04 Liveness6.1

stdout:

Tool IDA

Execution Time	60.043736ms
Answer	TIMEOUT
Input	AProVE 04 Liveness6.1

stdout:

Tool TRI

Execution Time	60.03559ms
Answer	TIMEOUT
Input	AProVE 04 Liveness6.1

stdout:

Tool TRI2

Execution Time	0.22867179ms
Answer	MAYBE
Input	AProVE 04 Liveness6.1

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  check(old(x)) -> old(x)
     , check(old(x)) -> old(check(x))
     , check(new(x)) -> new(check(x))
     , check(free(x)) -> free(check(x))
     , old(serve()) -> free(serve())
     , new(serve()) -> free(serve())
     , old(free(x)) -> free(old(x))
     , new(free(x)) -> free(new(x))
     , top(free(x)) -> top(check(new(x)))}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..