Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) ->
f(a(),
f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
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:
{ a_0() -> 1
, a_1() -> 2
, a_1() -> 6
, a_1() -> 8
, a_1() -> 12
, a_1() -> 14
, a_1() -> 16
, a_2() -> 22
, a_2() -> 26
, a_2() -> 28
, a_2() -> 32
, a_2() -> 34
, a_2() -> 36
, a_3() -> 66
, a_3() -> 70
, a_3() -> 72
, a_3() -> 76
, a_3() -> 78
, a_3() -> 80
, b_0() -> 1
, b_1() -> 4
, b_1() -> 10
, b_1() -> 18
, b_2() -> 24
, b_2() -> 30
, b_2() -> 38
, b_3() -> 68
, b_3() -> 74
, b_3() -> 82
, f_0(1, 1) -> 1
, f_1(2, 3) -> 1
, f_1(4, 5) -> 3
, f_1(6, 7) -> 5
, f_1(8, 9) -> 7
, f_1(10, 11) -> 9
, f_1(12, 13) -> 11
, f_1(14, 15) -> 13
, f_1(16, 3) -> 13
, f_1(16, 3) -> 52
, f_1(16, 17) -> 15
, f_1(18, 1) -> 17
, f_1(18, 3) -> 17
, f_1(18, 7) -> 17
, f_1(18, 13) -> 17
, f_1(18, 39) -> 17
, f_1(18, 47) -> 17
, f_2(22, 23) -> 13
, f_2(24, 25) -> 23
, f_2(26, 27) -> 25
, f_2(28, 29) -> 27
, f_2(30, 31) -> 29
, f_2(32, 33) -> 31
, f_2(34, 35) -> 33
, f_2(36, 23) -> 52
, f_2(36, 23) -> 88
, f_2(36, 37) -> 35
, f_2(36, 39) -> 5
, f_2(36, 39) -> 48
, f_2(36, 41) -> 40
, f_2(36, 42) -> 41
, f_2(36, 44) -> 43
, f_2(36, 45) -> 44
, f_2(36, 46) -> 45
, f_2(36, 47) -> 11
, f_2(36, 47) -> 51
, f_2(36, 49) -> 48
, f_2(36, 50) -> 49
, f_2(36, 52) -> 51
, f_2(36, 53) -> 52
, f_2(36, 54) -> 53
, f_2(38, 3) -> 37
, f_2(38, 7) -> 46
, f_2(38, 9) -> 37
, f_2(38, 13) -> 54
, f_2(38, 15) -> 37
, f_2(38, 17) -> 37
, f_2(38, 23) -> 37
, f_2(38, 27) -> 46
, f_2(38, 33) -> 54
, f_2(38, 39) -> 46
, f_2(38, 40) -> 39
, f_2(38, 43) -> 42
, f_2(38, 47) -> 54
, f_2(38, 48) -> 47
, f_2(38, 51) -> 50
, f_3(66, 67) -> 48
, f_3(68, 69) -> 67
, f_3(70, 71) -> 69
, f_3(72, 73) -> 71
, f_3(74, 75) -> 73
, f_3(76, 77) -> 75
, f_3(78, 79) -> 77
, f_3(80, 67) -> 84
, f_3(80, 81) -> 79
, f_3(80, 83) -> 51
, f_3(80, 83) -> 87
, f_3(80, 85) -> 84
, f_3(80, 86) -> 85
, f_3(80, 88) -> 87
, f_3(80, 89) -> 88
, f_3(80, 90) -> 89
, f_3(82, 27) -> 81
, f_3(82, 33) -> 90
, f_3(82, 84) -> 83
, f_3(82, 87) -> 86}
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:
{f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) ->
f(a(),
f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool IDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) ->
f(a(),
f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) ->
f(a(),
f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI2
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) ->
f(a(),
f(b(), f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x)))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..