Tool Bounds
| Execution Time | 6.2216997e-2ms |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | Rubio 04 gmnp |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ e(g(X)) -> e(X)
, f(c(b())) -> f(d(a()))
, f(d(X)) -> X
, f(a()) -> f(d(a()))
, f(c(a())) -> f(d(b()))
, f(c(X)) -> X
, f(a()) -> f(c(a()))}
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:
{ a_0() -> 1
, a_0() -> 2
, a_1() -> 2
, a_1() -> 9
, a_2() -> 2
, a_2() -> 11
, f_0(1) -> 2
, f_0(2) -> 2
, f_0(3) -> 2
, f_0(4) -> 2
, f_0(5) -> 2
, f_0(6) -> 2
, f_0(7) -> 2
, f_1(8) -> 2
, f_2(10) -> 2
, c_0(1) -> 2
, c_0(1) -> 3
, c_0(2) -> 2
, c_0(2) -> 3
, c_0(3) -> 2
, c_0(3) -> 3
, c_0(4) -> 2
, c_0(4) -> 3
, c_0(5) -> 2
, c_0(5) -> 3
, c_0(6) -> 2
, c_0(6) -> 3
, c_0(7) -> 2
, c_0(7) -> 3
, c_1(9) -> 8
, b_0() -> 2
, b_0() -> 4
, b_1() -> 2
, b_1() -> 9
, b_2() -> 2
, b_2() -> 11
, d_0(1) -> 2
, d_0(1) -> 5
, d_0(2) -> 2
, d_0(2) -> 5
, d_0(3) -> 2
, d_0(3) -> 5
, d_0(4) -> 2
, d_0(4) -> 5
, d_0(5) -> 2
, d_0(5) -> 5
, d_0(6) -> 2
, d_0(6) -> 5
, d_0(7) -> 2
, d_0(7) -> 5
, d_1(9) -> 8
, d_2(11) -> 10
, g_0(1) -> 2
, g_0(1) -> 6
, g_0(2) -> 2
, g_0(2) -> 6
, g_0(3) -> 2
, g_0(3) -> 6
, g_0(4) -> 2
, g_0(4) -> 6
, g_0(5) -> 2
, g_0(5) -> 6
, g_0(6) -> 2
, g_0(6) -> 6
, g_0(7) -> 2
, g_0(7) -> 6
, e_0(1) -> 2
, e_0(1) -> 7
, e_0(2) -> 2
, e_0(2) -> 7
, e_0(3) -> 2
, e_0(3) -> 7
, e_0(4) -> 2
, e_0(4) -> 7
, e_0(5) -> 2
, e_0(5) -> 7
, e_0(6) -> 2
, e_0(6) -> 7
, e_0(7) -> 2
, e_0(7) -> 7
, e_1(1) -> 2
, e_1(1) -> 7
, e_1(2) -> 2
, e_1(2) -> 7
, e_1(3) -> 2
, e_1(3) -> 7
, e_1(4) -> 2
, e_1(4) -> 7
, e_1(5) -> 2
, e_1(5) -> 7
, e_1(6) -> 2
, e_1(6) -> 7
, e_1(7) -> 2
, e_1(7) -> 7}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
MAYBE
Statistics:
Number of monomials: 413
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ e(g(X)) -> e(X)
, f(c(b())) -> f(d(a()))
, f(d(X)) -> X
, f(a()) -> f(d(a()))
, f(c(a())) -> f(d(b()))
, f(c(X)) -> X
, f(a()) -> f(c(a()))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool IDA
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ e(g(X)) -> e(X)
, f(c(b())) -> f(d(a()))
, f(d(X)) -> X
, f(a()) -> f(d(a()))
, f(c(a())) -> f(d(b()))
, f(c(X)) -> X
, f(a()) -> f(c(a()))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 4' 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 4' failed due to the following reason:
The input cannot be shown compatible
5) 'matrix-interpretation of dimension 3' failed due to the following reason:
The input cannot be shown compatible
6) 'matrix-interpretation of dimension 3' failed due to the following reason:
The input cannot be shown compatible
7) 'matrix-interpretation of dimension 3' failed due to the following reason:
The input cannot be shown compatible
8) 'matrix-interpretation of dimension 2' failed due to the following reason:
The input cannot be shown compatible
9) 'matrix-interpretation of dimension 2' failed due to the following reason:
The input cannot be shown compatible
10) 'matrix-interpretation of dimension 1' failed due to the following reason:
The input cannot be shown compatible
Arrrr..Tool TRI
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ e(g(X)) -> e(X)
, f(c(b())) -> f(d(a()))
, f(d(X)) -> X
, f(a()) -> f(d(a()))
, f(c(a())) -> f(d(b()))
, f(c(X)) -> X
, f(a()) -> f(c(a()))}
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:
{ e(g(X)) -> e(X)
, f(c(b())) -> f(d(a()))
, f(d(X)) -> X
, f(a()) -> f(d(a()))
, f(c(a())) -> f(d(b()))
, f(c(X)) -> X
, f(a()) -> f(c(a()))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..