Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ c(y) -> y
, c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)
, c(c(c(y))) -> c(c(a(y, 0())))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ c_0(1) -> 1
, c_1(3) -> 2
, c_1(4) -> 2
, c_1(4) -> 3
, c_1(5) -> 2
, c_1(5) -> 3
, c_1(5) -> 4
, c_1(6) -> 1
, c_1(7) -> 1
, c_1(7) -> 6
, c_2(8) -> 2
, c_2(9) -> 2
, c_2(9) -> 8
, c_2(10) -> 13
, c_2(10) -> 14
, c_2(10) -> 15
, c_2(14) -> 13
, c_2(15) -> 13
, c_2(15) -> 14
, c_3(16) -> 13
, c_3(17) -> 13
, c_3(17) -> 16
, 0_0() -> 1
, 0_1() -> 2
, 0_1() -> 3
, 0_1() -> 4
, 0_1() -> 5
, 0_2() -> 10
, 0_2() -> 13
, 0_2() -> 14
, 0_2() -> 15
, 0_3() -> 18
, a_0(1, 1) -> 1
, a_1(1, 5) -> 1
, a_1(1, 5) -> 6
, a_1(1, 5) -> 7
, a_1(2, 1) -> 1
, a_1(2, 5) -> 1
, a_1(2, 5) -> 6
, a_1(6, 5) -> 1
, a_1(6, 5) -> 6
, a_1(6, 5) -> 7
, a_1(7, 5) -> 1
, a_1(7, 5) -> 6
, a_1(7, 5) -> 7
, a_2(5, 10) -> 2
, a_2(5, 10) -> 8
, a_2(5, 10) -> 9
, a_2(13, 5) -> 1
, a_2(13, 5) -> 6
, a_3(10, 18) -> 13
, a_3(10, 18) -> 16
, a_3(10, 18) -> 17}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
TIMEOUT
Statistics:
Number of monomials: 0
Last formula building started for bound 0
Last SAT solving started for bound 0Tool EDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ c(y) -> y
, c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)
, c(c(c(y))) -> c(c(a(y, 0())))}
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:
{ c(y) -> y
, c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)
, c(c(c(y))) -> c(c(a(y, 0())))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 3' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 3' failed due to the following reason:
The input cannot be shown compatible
4) 'matrix-interpretation of dimension 2' 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 TRI
stdout:
YES(?,O(n^5))
We consider the following Problem:
Strict Trs:
{ c(y) -> y
, c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)
, c(c(c(y))) -> c(c(a(y, 0())))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^5))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
c(x1) = [1 0 2 0 0] x1 + [2]
[0 1 0 0 0] [0]
[0 0 1 2 0] [0]
[0 0 0 1 2] [0]
[0 0 0 0 1] [2]
0() = [0]
[0]
[0]
[0]
[0]
a(x1, x2) = [1 0 0 0 0] x1 + [1 3 0 0 0] x2 + [1]
[0 0 0 0 0] [0 0 0 0 0] [0]
[0 0 0 0 1] [0 0 0 0 0] [0]
[0 0 0 0 1] [0 0 0 0 0] [0]
[0 0 0 0 0] [0 0 0 0 0] [2]
Hurray, we answered YES(?,O(n^5))Tool TRI2
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ c(y) -> y
, c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)
, c(c(c(y))) -> c(c(a(y, 0())))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..