Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs: {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ a_0() -> 1
, a_1() -> 8
, a_1() -> 9
, a_1() -> 10
, a_2() -> 15
, a_2() -> 16
, a_2() -> 17
, f_0(1, 1) -> 2
, f_0(1, 2) -> 2
, f_0(1, 3) -> 2
, f_0(2, 1) -> 2
, f_0(2, 2) -> 2
, f_0(2, 3) -> 2
, f_0(3, 1) -> 2
, f_0(3, 2) -> 2
, f_0(3, 3) -> 2
, f_1(4, 1) -> 2
, f_1(4, 2) -> 2
, f_1(4, 3) -> 2
, f_1(4, 4) -> 2
, f_1(4, 7) -> 5
, f_1(5, 6) -> 4
, f_1(7, 1) -> 5
, f_1(7, 2) -> 5
, f_1(7, 3) -> 5
, f_1(7, 4) -> 5
, f_1(8, 9) -> 7
, f_2(11, 4) -> 5
, f_2(12, 13) -> 11
, f_2(14, 8) -> 12
, f_2(15, 16) -> 14
, h_0(1) -> 3
, h_0(2) -> 3
, h_0(3) -> 3
, h_1(10) -> 6
, h_2(17) -> 13}
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(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), 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(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), 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(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), 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: {f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x)}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..