Tool Bounds
| Execution Time | 6.4961195e-2ms |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | CiME 04 dpqs |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ g(c(1())) -> g(d(0()))
, g(c(0())) -> g(d(1()))
, g(d(x)) -> x
, g(c(x)) -> x
, f(f(x)) -> f(d(f(x)))
, f(f(x)) -> f(c(f(x)))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(1) -> 1
, f_1(1) -> 5
, f_1(4) -> 1
, f_1(4) -> 5
, f_2(4) -> 7
, f_2(6) -> 5
, c_0(1) -> 1
, c_1(5) -> 4
, c_2(7) -> 6
, d_0(1) -> 1
, d_1(3) -> 2
, d_1(5) -> 4
, d_2(7) -> 6
, g_0(1) -> 1
, g_1(2) -> 1
, 0_0() -> 1
, 0_1() -> 1
, 0_1() -> 3
, 1_0() -> 1
, 1_1() -> 1
, 1_1() -> 3}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
MAYBE
Statistics:
Number of monomials: 432
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
| Execution Time | 2.753678ms |
|---|
| Answer | YES(?,O(n^3)) |
|---|
| Input | CiME 04 dpqs |
|---|
stdout:
YES(?,O(n^3))
We consider the following Problem:
Strict Trs:
{ g(c(1())) -> g(d(0()))
, g(c(0())) -> g(d(1()))
, g(d(x)) -> x
, g(c(x)) -> x
, f(f(x)) -> f(d(f(x)))
, f(f(x)) -> f(c(f(x)))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^3))
Proof:
We have the following EDA-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 3 0] x1 + [0]
[0 0 0] [3]
[0 0 0] [0]
c(x1) = [1 0 3] x1 + [0]
[0 0 1] [1]
[0 1 0] [2]
d(x1) = [1 0 0] x1 + [0]
[0 0 1] [0]
[0 1 0] [1]
g(x1) = [1 0 1] x1 + [0]
[0 0 1] [0]
[0 1 0] [0]
0() = [3]
[0]
[0]
1() = [3]
[0]
[1]
Hurray, we answered YES(?,O(n^3))Tool IDA
| Execution Time | 4.259421ms |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | CiME 04 dpqs |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ g(c(1())) -> g(d(0()))
, g(c(0())) -> g(d(1()))
, g(d(x)) -> x
, g(c(x)) -> x
, f(f(x)) -> f(d(f(x)))
, f(f(x)) -> f(c(f(x)))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 1 0] x1 + [0]
[0 0 0] [2]
[0 0 0] [0]
c(x1) = [1 0 0] x1 + [1]
[0 0 1] [0]
[0 1 0] [0]
d(x1) = [1 0 0] x1 + [0]
[0 0 1] [0]
[0 1 0] [0]
g(x1) = [1 0 0] x1 + [1]
[0 0 1] [0]
[0 1 0] [0]
0() = [0]
[0]
[0]
1() = [0]
[0]
[0]
Hurray, we answered YES(?,O(n^1))Tool TRI
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ g(c(1())) -> g(d(0()))
, g(c(0())) -> g(d(1()))
, g(d(x)) -> x
, g(c(x)) -> x
, f(f(x)) -> f(d(f(x)))
, f(f(x)) -> f(c(f(x)))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 6' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 5' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 4' failed due to the following reason:
The input cannot be shown compatible
4) 'matrix-interpretation of dimension 3' failed due to the following reason:
The input cannot be shown compatible
5) 'matrix-interpretation of dimension 2' failed due to the following reason:
The input cannot be shown compatible
6) 'matrix-interpretation of dimension 1' failed due to the following reason:
The input cannot be shown compatible
Arrrr..Tool TRI2
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ g(c(1())) -> g(d(0()))
, g(c(0())) -> g(d(1()))
, g(d(x)) -> x
, g(c(x)) -> x
, f(f(x)) -> f(d(f(x)))
, f(f(x)) -> f(c(f(x)))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..