Problem Transformed CSR 04 Ex1 Zan97 C

Tool Bounds

Execution Time60.03546ms
Answer
TIMEOUT
InputTransformed CSR 04 Ex1 Zan97 C

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  top(ok(X)) -> top(active(X))
     , top(mark(X)) -> top(proper(X))
     , h(ok(X)) -> ok(h(X))
     , g(ok(X)) -> ok(g(X))
     , proper(d()) -> ok(d())
     , proper(c()) -> ok(c())
     , proper(h(X)) -> h(proper(X))
     , proper(g(X)) -> g(proper(X))
     , active(h(d())) -> mark(g(c()))
     , active(c()) -> mark(d())
     , active(g(X)) -> mark(h(X))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time16.261719ms
Answer
MAYBE
InputTransformed CSR 04 Ex1 Zan97 C

stdout:

MAYBE

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

Tool EDA

Execution Time60.039036ms
Answer
TIMEOUT
InputTransformed CSR 04 Ex1 Zan97 C

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  top(ok(X)) -> top(active(X))
     , top(mark(X)) -> top(proper(X))
     , h(ok(X)) -> ok(h(X))
     , g(ok(X)) -> ok(g(X))
     , proper(d()) -> ok(d())
     , proper(c()) -> ok(c())
     , proper(h(X)) -> h(proper(X))
     , proper(g(X)) -> g(proper(X))
     , active(h(d())) -> mark(g(c()))
     , active(c()) -> mark(d())
     , active(g(X)) -> mark(h(X))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool IDA

Execution Time60.036934ms
Answer
TIMEOUT
InputTransformed CSR 04 Ex1 Zan97 C

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  top(ok(X)) -> top(active(X))
     , top(mark(X)) -> top(proper(X))
     , h(ok(X)) -> ok(h(X))
     , g(ok(X)) -> ok(g(X))
     , proper(d()) -> ok(d())
     , proper(c()) -> ok(c())
     , proper(h(X)) -> h(proper(X))
     , proper(g(X)) -> g(proper(X))
     , active(h(d())) -> mark(g(c()))
     , active(c()) -> mark(d())
     , active(g(X)) -> mark(h(X))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool TRI

Execution Time60.03572ms
Answer
TIMEOUT
InputTransformed CSR 04 Ex1 Zan97 C

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  top(ok(X)) -> top(active(X))
     , top(mark(X)) -> top(proper(X))
     , h(ok(X)) -> ok(h(X))
     , g(ok(X)) -> ok(g(X))
     , proper(d()) -> ok(d())
     , proper(c()) -> ok(c())
     , proper(h(X)) -> h(proper(X))
     , proper(g(X)) -> g(proper(X))
     , active(h(d())) -> mark(g(c()))
     , active(c()) -> mark(d())
     , active(g(X)) -> mark(h(X))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool TRI2

Execution Time0.86299515ms
Answer
MAYBE
InputTransformed CSR 04 Ex1 Zan97 C

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  top(ok(X)) -> top(active(X))
     , top(mark(X)) -> top(proper(X))
     , h(ok(X)) -> ok(h(X))
     , g(ok(X)) -> ok(g(X))
     , proper(d()) -> ok(d())
     , proper(c()) -> ok(c())
     , proper(h(X)) -> h(proper(X))
     , proper(g(X)) -> g(proper(X))
     , active(h(d())) -> mark(g(c()))
     , active(c()) -> mark(d())
     , active(g(X)) -> mark(h(X))}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..