Tool CaT
stdout:
YES(?,O(n^1))
Problem:
t(o(x1)) -> m(a(x1))
t(e(x1)) -> n(s(x1))
a(l(x1)) -> a(t(x1))
o(m(a(x1))) -> t(e(n(x1)))
s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) -> a(l(a(t(x1))))
Proof:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {8,7,6,5,4}
transitions:
a1(27) -> 28*
t1(35) -> 36*
t1(29) -> 30*
t1(26) -> 27*
n1(10) -> 11*
s1(17) -> 18*
s1(19) -> 20*
s1(9) -> 10*
a2(45) -> 46*
a2(43) -> 44*
l2(44) -> 45*
t2(47) -> 48*
t2(42) -> 43*
t2(53) -> 54*
a3(59) -> 60*
t3(58) -> 59*
t0(2) -> 4*
t0(1) -> 4*
t0(3) -> 4*
o0(2) -> 6*
o0(1) -> 6*
o0(3) -> 6*
m0(2) -> 1*
m0(1) -> 1*
m0(3) -> 1*
a0(2) -> 5*
a0(1) -> 5*
a0(3) -> 5*
e0(2) -> 2*
e0(1) -> 2*
e0(3) -> 2*
n0(2) -> 8*
n0(1) -> 8*
n0(3) -> 8*
s0(2) -> 7*
s0(1) -> 7*
s0(3) -> 7*
l0(2) -> 3*
l0(1) -> 3*
l0(3) -> 3*
1 -> 29,17
2 -> 26,9
3 -> 35,19
9 -> 53*
11 -> 54,43,27,4
17 -> 42*
18 -> 10*
19 -> 47*
20 -> 10*
28 -> 5*
30 -> 27*
36 -> 27*
44 -> 58*
46 -> 11,4
48 -> 43*
54 -> 43*
60 -> 46,11,4,27
problem:
QedTool IRC1
stdout:
YES(?,O(n^1))
Tool IRC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ t(o(x1)) -> m(a(x1))
, t(e(x1)) -> n(s(x1))
, a(l(x1)) -> a(t(x1))
, o(m(a(x1))) -> t(e(n(x1)))
, s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
, n(s(x1)) -> a(l(a(t(x1))))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ t(o(x1)) -> m(a(x1))
, t(e(x1)) -> n(s(x1))
, a(l(x1)) -> a(t(x1))
, o(m(a(x1))) -> t(e(n(x1)))
, s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
, n(s(x1)) -> a(l(a(t(x1))))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ t_0(2) -> 1
, t_1(2) -> 4
, t_2(2) -> 7
, t_3(6) -> 8
, o_0(2) -> 1
, m_0(2) -> 2
, a_0(2) -> 1
, a_1(4) -> 1
, a_2(5) -> 1
, a_2(5) -> 4
, a_2(5) -> 7
, a_2(7) -> 6
, a_3(8) -> 1
, a_3(8) -> 4
, a_3(8) -> 7
, e_0(2) -> 2
, n_0(2) -> 1
, n_1(3) -> 1
, n_1(3) -> 4
, n_1(3) -> 7
, s_0(2) -> 1
, s_1(2) -> 3
, l_0(2) -> 2
, l_2(6) -> 5}Tool RC1
stdout:
YES(?,O(n^1))
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ t(o(x1)) -> m(a(x1))
, t(e(x1)) -> n(s(x1))
, a(l(x1)) -> a(t(x1))
, o(m(a(x1))) -> t(e(n(x1)))
, s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
, n(s(x1)) -> a(l(a(t(x1))))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ t(o(x1)) -> m(a(x1))
, t(e(x1)) -> n(s(x1))
, a(l(x1)) -> a(t(x1))
, o(m(a(x1))) -> t(e(n(x1)))
, s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
, n(s(x1)) -> a(l(a(t(x1))))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ t_0(2) -> 1
, t_1(2) -> 4
, t_2(2) -> 7
, t_3(6) -> 8
, o_0(2) -> 1
, m_0(2) -> 2
, a_0(2) -> 1
, a_1(4) -> 1
, a_2(5) -> 1
, a_2(5) -> 4
, a_2(5) -> 7
, a_2(7) -> 6
, a_3(8) -> 1
, a_3(8) -> 4
, a_3(8) -> 7
, e_0(2) -> 2
, n_0(2) -> 1
, n_1(3) -> 1
, n_1(3) -> 4
, n_1(3) -> 7
, s_0(2) -> 1
, s_1(2) -> 3
, l_0(2) -> 2
, l_2(6) -> 5}