Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(c(b(a(x1))))
, c(d(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(c(x1))
, b(c(a(x1))) -> a(b(a(b(c(x1)))))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ a_0(1) -> 1
, a_1(1) -> 4
, a_1(2) -> 1
, a_1(2) -> 4
, a_1(2) -> 6
, a_1(2) -> 9
, a_1(2) -> 12
, a_1(2) -> 13
, a_1(9) -> 5
, a_1(17) -> 4
, a_2(2) -> 16
, a_2(10) -> 2
, a_2(10) -> 9
, a_2(10) -> 12
, a_2(12) -> 11
, a_2(14) -> 4
, a_2(14) -> 5
, a_2(14) -> 11
, a_2(17) -> 1
, a_2(17) -> 4
, a_2(17) -> 5
, a_2(17) -> 6
, a_2(17) -> 9
, a_2(17) -> 12
, a_2(17) -> 13
, a_3(10) -> 30
, a_3(17) -> 12
, a_3(24) -> 12
, a_3(26) -> 25
, a_3(28) -> 11
, a_3(28) -> 16
, c_0(1) -> 1
, c_1(1) -> 6
, c_1(2) -> 6
, c_1(3) -> 2
, c_1(4) -> 5
, c_1(6) -> 1
, c_1(17) -> 6
, c_2(1) -> 13
, c_2(2) -> 13
, c_2(4) -> 7
, c_2(5) -> 8
, c_2(6) -> 19
, c_2(7) -> 3
, c_2(8) -> 2
, c_2(10) -> 13
, c_2(12) -> 14
, c_2(14) -> 13
, c_2(15) -> 14
, c_2(17) -> 13
, c_2(18) -> 17
, c_2(19) -> 9
, c_3(2) -> 20
, c_3(10) -> 27
, c_3(11) -> 21
, c_3(13) -> 22
, c_3(16) -> 23
, c_3(17) -> 27
, c_3(20) -> 18
, c_3(21) -> 10
, c_3(22) -> 12
, c_3(23) -> 15
, c_3(29) -> 28
, c_4(12) -> 31
, c_4(25) -> 32
, c_4(27) -> 33
, c_4(30) -> 31
, c_4(31) -> 29
, c_4(32) -> 24
, c_4(33) -> 26
, b_0(1) -> 1
, b_1(4) -> 3
, b_1(5) -> 2
, b_1(6) -> 9
, b_2(2) -> 18
, b_2(11) -> 10
, b_2(13) -> 12
, b_2(16) -> 15
, b_3(12) -> 29
, b_3(25) -> 24
, b_3(27) -> 26
, b_3(30) -> 29
, d_0(1) -> 1}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
TIMEOUT
Statistics:
Number of monomials: 3434
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(c(b(a(x1))))
, c(d(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(c(x1))
, b(c(a(x1))) -> a(b(a(b(c(x1)))))}
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:
{ a(a(x1)) -> a(c(b(a(x1))))
, c(d(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(c(x1))
, b(c(a(x1))) -> a(b(a(b(c(x1)))))}
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^3))
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(c(b(a(x1))))
, c(d(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(c(x1))
, b(c(a(x1))) -> a(b(a(b(c(x1)))))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^3))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
a(x1) = [1 0 1 0 1] x1 + [0]
[0 0 0 0 0] [0]
[0 0 1 0 1] [3]
[0 0 0 0 0] [0]
[0 0 0 0 0] [0]
c(x1) = [1 0 0 0 3] x1 + [0]
[0 0 1 0 0] [0]
[0 0 0 0 3] [0]
[0 0 0 0 0] [1]
[0 0 0 0 0] [0]
b(x1) = [1 2 0 0 3] x1 + [2]
[0 0 0 0 3] [0]
[0 0 0 3 0] [0]
[0 0 0 0 0] [1]
[0 0 0 0 0] [0]
d(x1) = [1 3 3 3 3] x1 + [3]
[0 1 3 3 3] [3]
[0 0 0 0 0] [0]
[0 0 0 0 0] [0]
[0 0 0 0 0] [3]
Hurray, we answered YES(?,O(n^3))Tool TRI2
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(c(b(a(x1))))
, c(d(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(c(x1))
, b(c(a(x1))) -> a(b(a(b(c(x1)))))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..