Tool Bounds
| Execution Time | 60.028805ms |
|---|
| Answer | TIMEOUT |
|---|
| Input | AG01 3.49 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ g(c(s(x), s(y))) -> f(c(x, y))
, g(c(x, s(y))) -> g(c(s(x), y))
, f(c(s(x), s(y))) -> g(c(x, y))
, f(c(s(x), y)) -> f(c(x, s(y)))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool CDI
| Execution Time | 40.133606ms |
|---|
| Answer | MAYBE |
|---|
| Input | AG01 3.49 |
|---|
stdout:
MAYBE
Statistics:
Number of monomials: 1491
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
| Execution Time | 60.033844ms |
|---|
| Answer | TIMEOUT |
|---|
| Input | AG01 3.49 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ g(c(s(x), s(y))) -> f(c(x, y))
, g(c(x, s(y))) -> g(c(s(x), y))
, f(c(s(x), s(y))) -> g(c(x, y))
, f(c(s(x), y)) -> f(c(x, s(y)))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool IDA
| Execution Time | 60.031525ms |
|---|
| Answer | TIMEOUT |
|---|
| Input | AG01 3.49 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ g(c(s(x), s(y))) -> f(c(x, y))
, g(c(x, s(y))) -> g(c(s(x), y))
, f(c(s(x), s(y))) -> g(c(x, y))
, f(c(s(x), y)) -> f(c(x, s(y)))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI
| Execution Time | 60.02741ms |
|---|
| Answer | TIMEOUT |
|---|
| Input | AG01 3.49 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ g(c(s(x), s(y))) -> f(c(x, y))
, g(c(x, s(y))) -> g(c(s(x), y))
, f(c(s(x), s(y))) -> g(c(x, y))
, f(c(s(x), y)) -> f(c(x, s(y)))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI2
| Execution Time | 1.6563351ms |
|---|
| Answer | MAYBE |
|---|
| Input | AG01 3.49 |
|---|
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ g(c(s(x), s(y))) -> f(c(x, y))
, g(c(x, s(y))) -> g(c(s(x), y))
, f(c(s(x), s(y))) -> g(c(x, y))
, f(c(s(x), y)) -> f(c(x, s(y)))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..