Tool Bounds
| Execution Time | 3.1569958e-2ms |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))
, f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ a_0() -> 1
, a_1() -> 13
, b_0() -> 1
, b_1() -> 9
, b_1() -> 14
, b'_0() -> 1
, b'_1() -> 16
, i_0(1, 1, 1) -> 1
, c_0() -> 1
, c_1() -> 5
, c_1() -> 12
, g_0(1, 1) -> 1
, g_1(11, 12) -> 10
, d_0() -> 1
, d_1() -> 8
, f_0(1, 1) -> 1
, f_1(5, 6) -> 4
, f_1(7, 8) -> 3
, f_1(15, 6) -> 3
, e_0() -> 1
, e_1() -> 2
, ._0(1, 1) -> 1
, ._1(9, 10) -> 7
, ._1(14, 12) -> 15
, ._1(16, 12) -> 5
, d'_0() -> 1
, d'_1() -> 6
, if_0(1, 1, 1) -> 1
, if_1(2, 3, 4) -> 1
, h_0(1, 1) -> 1
, h_1(13, 14) -> 11}
Hurray, we answered YES(?,O(n^1))Tool CDI
| Execution Time | 60.041473ms |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 4.47 |
|---|
stdout:
TIMEOUT
Statistics:
Number of monomials: 0
Last formula building started for bound 0
Last SAT solving started for bound 0Tool EDA
| Execution Time | 4.3309712ms |
|---|
| Answer | YES(?,O(n^2)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))
, f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following EDA-non-satisfying matrix interpretation:
Interpretation Functions:
a() = [0]
[0]
b() = [0]
[0]
b'() = [0]
[0]
i(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
c() = [0]
[0]
g(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [3]
d() = [0]
[0]
f(x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
e() = [0]
[3]
.(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
d'() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
h(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
Hurray, we answered YES(?,O(n^2))Tool IDA
| Execution Time | 6.7027316ms |
|---|
| Answer | YES(?,O(n^2)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))
, f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
a() = [0]
[0]
b() = [0]
[0]
b'() = [0]
[0]
i(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
c() = [0]
[0]
g(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [3]
d() = [0]
[0]
f(x1, x2) = [1 3] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
e() = [0]
[3]
.(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
d'() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
h(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
Hurray, we answered YES(?,O(n^2))Tool TRI
| Execution Time | 0.882319ms |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))
, f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
a() = [0]
[0]
b() = [0]
[0]
b'() = [0]
[0]
i(x1, x2, x3) = [1 3] x1 + [1 3] x2 + [1 3] x3 + [0]
[0 0] [0 0] [0 0] [0]
c() = [0]
[0]
g(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [2]
d() = [0]
[0]
f(x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
e() = [0]
[3]
.(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
d'() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
h(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [2]
Hurray, we answered YES(?,O(n^1))Tool TRI2
| Execution Time | 1.1000199ms |
|---|
| Answer | YES(?,O(n^2)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))
, f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
a() = [2]
[1]
b() = [0]
[2]
b'() = [0]
[0]
i(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [1 3] x3 + [0]
[0 0] [0 1] [0 0] [0]
c() = [0]
[0]
g(x1, x2) = [1 2] x1 + [1 0] x2 + [3]
[0 0] [0 0] [1]
d() = [0]
[0]
f(x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
e() = [0]
[3]
.(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
d'() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
h(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [0]
Hurray, we answered YES(?,O(n^2))