Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs: {b(a(b(c(c(b(x1)))))) -> a(b(b(c(c(b(a(x1)))))))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ b_0(1) -> 1
, b_1(3) -> 2
, b_1(4) -> 3
, b_1(7) -> 6
, c_0(1) -> 1
, c_1(5) -> 4
, c_1(6) -> 5
, a_0(1) -> 1
, a_1(1) -> 7
, a_1(2) -> 1
, a_1(2) -> 6}
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: {b(a(b(c(c(b(x1)))))) -> a(b(b(c(c(b(a(x1)))))))}
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: {b(a(b(c(c(b(x1)))))) -> a(b(b(c(c(b(a(x1)))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs: {b(a(b(c(c(b(x1)))))) -> a(b(b(c(c(b(a(x1)))))))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
b(x1) = [1 2 0] x1 + [0]
[0 0 2] [0]
[0 0 0] [2]
c(x1) = [1 1 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
a(x1) = [1 0 0] x1 + [0]
[0 0 1] [0]
[0 0 0] [1]
Hurray, we answered YES(?,O(n^1))Tool TRI2
stdout:
MAYBE
We consider the following Problem:
Strict Trs: {b(a(b(c(c(b(x1)))))) -> a(b(b(c(c(b(a(x1)))))))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..