Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))
, a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), 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:
{ f_0() -> 1
, f_1() -> 4
, f_1() -> 6
, f_2() -> 14
, f_2() -> 16
, f_3() -> 29
, f_3() -> 31
, g_0() -> 1
, g_1() -> 2
, g_1() -> 8
, g_2() -> 12
, g_2() -> 18
, g_3() -> 27
, g_3() -> 33
, a_0(1, 1) -> 1
, a_1(2, 3) -> 1
, a_1(4, 5) -> 3
, a_1(6, 1) -> 11
, a_1(6, 7) -> 1
, a_1(6, 7) -> 5
, a_1(6, 7) -> 11
, a_1(6, 7) -> 24
, a_1(6, 9) -> 1
, a_1(6, 9) -> 5
, a_1(6, 9) -> 11
, a_1(6, 9) -> 15
, a_1(6, 9) -> 24
, a_1(6, 11) -> 3
, a_1(6, 15) -> 1
, a_1(6, 20) -> 1
, a_1(6, 22) -> 1
, a_1(8, 1) -> 7
, a_1(8, 3) -> 7
, a_1(8, 3) -> 17
, a_1(8, 7) -> 7
, a_1(8, 10) -> 9
, a_1(8, 11) -> 7
, a_1(8, 11) -> 10
, a_1(8, 11) -> 17
, a_1(8, 11) -> 23
, a_1(8, 13) -> 1
, a_1(8, 19) -> 1
, a_1(8, 23) -> 1
, a_2(12, 13) -> 7
, a_2(14, 15) -> 13
, a_2(16, 1) -> 24
, a_2(16, 5) -> 24
, a_2(16, 7) -> 24
, a_2(16, 9) -> 24
, a_2(16, 11) -> 24
, a_2(16, 17) -> 15
, a_2(16, 20) -> 19
, a_2(16, 21) -> 20
, a_2(16, 22) -> 1
, a_2(16, 22) -> 5
, a_2(16, 22) -> 11
, a_2(16, 22) -> 15
, a_2(16, 22) -> 20
, a_2(16, 22) -> 24
, a_2(18, 1) -> 17
, a_2(18, 3) -> 21
, a_2(18, 7) -> 22
, a_2(18, 10) -> 17
, a_2(18, 11) -> 17
, a_2(18, 13) -> 10
, a_2(18, 13) -> 17
, a_2(18, 13) -> 23
, a_2(18, 19) -> 7
, a_2(18, 19) -> 10
, a_2(18, 19) -> 17
, a_2(18, 19) -> 23
, a_2(18, 23) -> 22
, a_2(18, 24) -> 23
, a_3(27, 28) -> 17
, a_3(29, 30) -> 28
, a_3(31, 15) -> 45
, a_3(31, 20) -> 45
, a_3(31, 22) -> 45
, a_3(31, 32) -> 30
, a_3(31, 35) -> 34
, a_3(31, 36) -> 35
, a_3(31, 43) -> 15
, a_3(31, 43) -> 24
, a_3(31, 43) -> 30
, a_3(31, 43) -> 35
, a_3(33, 7) -> 32
, a_3(33, 13) -> 36
, a_3(33, 17) -> 43
, a_3(33, 19) -> 32
, a_3(33, 23) -> 32
, a_3(33, 28) -> 23
, a_3(33, 28) -> 44
, a_3(33, 34) -> 23
, a_3(33, 44) -> 43
, a_3(33, 45) -> 44}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
TIMEOUT
Statistics:
Number of monomials: 1168
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(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))
, a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), 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:
{ a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))
, a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), 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:
{ a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))
, a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x))))}
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(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))
, a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x))))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..