Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(a(c(x1)))
, a(c(b(x1))) -> b(a(b(a(x1))))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 5.
The enriched problem is compatible with the following automaton:
{ b_0(1) -> 1
, b_0(2) -> 1
, b_0(3) -> 1
, b_1(5) -> 4
, b_1(6) -> 12
, b_1(11) -> 3
, b_1(11) -> 6
, b_1(11) -> 7
, b_2(14) -> 13
, b_2(22) -> 6
, b_2(22) -> 7
, b_2(22) -> 11
, b_2(22) -> 16
, b_2(24) -> 23
, b_3(29) -> 15
, b_3(29) -> 16
, b_3(29) -> 18
, b_3(31) -> 30
, b_3(33) -> 32
, b_4(42) -> 41
, c_0(1) -> 2
, c_0(2) -> 2
, c_0(3) -> 2
, c_1(1) -> 8
, c_1(2) -> 8
, c_1(3) -> 8
, c_1(6) -> 5
, c_1(7) -> 1
, c_2(5) -> 10
, c_2(6) -> 17
, c_2(9) -> 4
, c_2(11) -> 19
, c_2(15) -> 14
, c_2(16) -> 12
, c_2(18) -> 3
, c_2(18) -> 6
, c_2(18) -> 7
, c_2(22) -> 14
, c_3(14) -> 21
, c_3(20) -> 13
, c_3(22) -> 26
, c_3(24) -> 28
, c_3(25) -> 6
, c_3(25) -> 7
, c_3(25) -> 11
, c_3(25) -> 16
, c_3(27) -> 23
, c_3(29) -> 33
, c_3(34) -> 33
, c_4(29) -> 36
, c_4(31) -> 38
, c_4(33) -> 40
, c_4(35) -> 15
, c_4(35) -> 16
, c_4(35) -> 18
, c_4(37) -> 30
, c_4(39) -> 32
, c_4(43) -> 42
, c_5(42) -> 45
, c_5(44) -> 41
, a_0(1) -> 3
, a_0(2) -> 3
, a_0(3) -> 3
, a_1(1) -> 6
, a_1(2) -> 6
, a_1(3) -> 6
, a_1(4) -> 3
, a_1(4) -> 6
, a_1(8) -> 7
, a_1(11) -> 6
, a_1(12) -> 11
, a_1(22) -> 6
, a_1(29) -> 6
, a_2(4) -> 15
, a_2(10) -> 9
, a_2(11) -> 24
, a_2(12) -> 15
, a_2(13) -> 6
, a_2(13) -> 24
, a_2(17) -> 16
, a_2(19) -> 18
, a_2(22) -> 24
, a_2(23) -> 22
, a_2(29) -> 24
, a_2(30) -> 15
, a_3(21) -> 20
, a_3(22) -> 31
, a_3(23) -> 34
, a_3(26) -> 25
, a_3(28) -> 27
, a_3(29) -> 31
, a_3(30) -> 29
, a_3(32) -> 24
, a_3(32) -> 31
, a_4(30) -> 43
, a_4(36) -> 35
, a_4(38) -> 37
, a_4(40) -> 39
, a_4(41) -> 31
, a_5(45) -> 44}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
MAYBE
Statistics:
Number of monomials: 1494
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(a(c(x1)))
, a(c(b(x1))) -> b(a(b(a(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 2' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 1' failed due to the following reason:
The input cannot be shown compatible
Arrrr..Tool IDA
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(a(c(x1)))
, a(c(b(x1))) -> b(a(b(a(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:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(a(c(x1)))
, a(c(b(x1))) -> b(a(b(a(x1))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI2
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ a(a(x1)) -> a(b(c(a(x1))))
, b(x1) -> c(a(c(x1)))
, a(c(b(x1))) -> b(a(b(a(x1))))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..