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