Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(q0(0(x1))) -> 0(0(q0(x1)))
0(q0(h(x1))) -> 0(0(q0(h(x1))))
0(q0(1(x1))) -> 0(1(q0(x1)))
1(q0(0(x1))) -> 0(0(q1(x1)))
1(q0(h(x1))) -> 0(0(q1(h(x1))))
1(q0(1(x1))) -> 0(1(q1(x1)))
1(q1(0(x1))) -> 1(0(q1(x1)))
1(q1(h(x1))) -> 1(0(q1(h(x1))))
1(q1(1(x1))) -> 1(1(q1(x1)))
0(q1(0(x1))) -> 0(0(q2(x1)))
0(q1(h(x1))) -> 0(0(q2(h(x1))))
0(q1(1(x1))) -> 0(1(q2(x1)))
1(q2(0(x1))) -> 1(0(q2(x1)))
1(q2(h(x1))) -> 1(0(q2(h(x1))))
1(q2(1(x1))) -> 1(1(q2(x1)))
0(q2(x1)) -> q3(1(x1))
1(q3(x1)) -> q3(1(x1))
0(q3(x1)) -> q4(0(x1))
1(q4(x1)) -> q4(1(x1))
0(q4(0(x1))) -> 1(0(q5(x1)))
0(q4(h(x1))) -> 1(0(q5(h(x1))))
0(q4(1(x1))) -> 1(1(q5(x1)))
1(q5(0(x1))) -> 0(0(q1(x1)))
1(q5(h(x1))) -> 0(0(q1(h(x1))))
1(q5(1(x1))) -> 0(1(q1(x1)))
h(q0(x1)) -> h(0(q0(x1)))
h(q1(x1)) -> h(0(q1(x1)))
h(q2(x1)) -> h(0(q2(x1)))
h(q3(x1)) -> h(0(q3(x1)))
h(q4(x1)) -> h(0(q4(x1)))
h(q5(x1)) -> h(0(q5(x1)))
Proof:
Bounds Processor:
bound: 4
enrichment: match
automaton:
final states: {9,8,7}
transitions:
h3(348) -> 349*
h1(68) -> 69*
q52(324) -> 325*
q52(338) -> 339*
q52(340) -> 341*
q52(330) -> 331*
q52(320) -> 321*
q52(332) -> 333*
01(50) -> 51*
01(67) -> 68*
01(42) -> 43*
01(39) -> 40*
01(56) -> 57*
01(58) -> 59*
01(48) -> 49*
14(352) -> 353*
q51(212) -> 213*
q51(204) -> 205*
q51(206) -> 207*
q51(196) -> 197*
q51(198) -> 199*
q51(190) -> 191*
04(351) -> 352*
q41(40) -> 41*
q41(182) -> 183*
q41(172) -> 173*
q41(174) -> 175*
q41(64) -> 65*
q41(166) -> 167*
q41(188) -> 189*
q41(180) -> 181*
q54(350) -> 351*
q31(142) -> 143*
q31(164) -> 165*
q31(156) -> 157*
q31(11) -> 12*
q31(158) -> 159*
q31(148) -> 149*
q31(150) -> 151*
q13(367) -> 368*
q21(132) -> 133*
q21(134) -> 135*
q21(124) -> 125*
q21(126) -> 127*
q21(118) -> 119*
q21(140) -> 141*
q11(102) -> 103*
q11(94) -> 95*
q11(116) -> 117*
q11(108) -> 109*
q11(110) -> 111*
q11(100) -> 101*
q01(92) -> 93*
q01(84) -> 85*
q01(86) -> 87*
q01(76) -> 77*
q01(66) -> 67*
q01(78) -> 79*
11(20) -> 21*
11(10) -> 11*
11(34) -> 35*
11(26) -> 27*
11(28) -> 29*
11(18) -> 19*
q42(311) -> 312*
q42(241) -> 242*
00(5) -> 7*
00(2) -> 7*
00(4) -> 7*
00(6) -> 7*
00(1) -> 7*
00(3) -> 7*
02(252) -> 253*
02(274) -> 275*
02(269) -> 270*
02(258) -> 259*
02(243) -> 244*
02(310) -> 311*
02(260) -> 261*
02(250) -> 251*
02(240) -> 241*
q00(5) -> 1*
q00(2) -> 1*
q00(4) -> 1*
q00(6) -> 1*
q00(1) -> 1*
q00(3) -> 1*
q32(218) -> 219*
h0(5) -> 9*
h0(2) -> 9*
h0(4) -> 9*
h0(6) -> 9*
h0(1) -> 9*
h0(3) -> 9*
12(217) -> 218*
12(234) -> 235*
12(321) -> 322*
12(236) -> 237*
12(226) -> 227*
12(228) -> 229*
12(220) -> 221*
12(322) -> 323*
10(5) -> 8*
10(2) -> 8*
10(4) -> 8*
10(6) -> 8*
10(1) -> 8*
10(3) -> 8*
h2(270) -> 271*
q10(5) -> 2*
q10(2) -> 2*
q10(4) -> 2*
q10(6) -> 2*
q10(1) -> 2*
q10(3) -> 2*
13(359) -> 360*
13(368) -> 369*
13(288) -> 289*
q20(5) -> 3*
q20(2) -> 3*
q20(4) -> 3*
q20(6) -> 3*
q20(1) -> 3*
q20(3) -> 3*
03(287) -> 288*
03(276) -> 277*
03(347) -> 348*
q30(5) -> 4*
q30(2) -> 4*
q30(4) -> 4*
q30(6) -> 4*
q30(1) -> 4*
q30(3) -> 4*
q53(304) -> 305*
q53(306) -> 307*
q53(296) -> 297*
q53(286) -> 287*
q53(358) -> 359*
q53(298) -> 299*
q53(290) -> 291*
q40(5) -> 5*
q40(2) -> 5*
q40(4) -> 5*
q40(6) -> 5*
q40(1) -> 5*
q40(3) -> 5*
q43(277) -> 278*
q50(5) -> 6*
q50(2) -> 6*
q50(4) -> 6*
q50(6) -> 6*
q50(1) -> 6*
q50(3) -> 6*
1 -> 206,182,158,134,110,86,56,28
2 -> 196,172,148,124,100,76,42,18
3 -> 212,188,164,140,116,92,58,34
4 -> 198,174,150,126,102,78,48,20
5 -> 190,166,142,118,94,66,39,10
6 -> 204,180,156,132,108,84,50,26
10 -> 324*
11 -> 310,64
12 -> 229,218,244,241,21,11,64,59,8,7
18 -> 340*
19 -> 11*
20 -> 320*
21 -> 11*
26 -> 332*
27 -> 11*
28 -> 338*
29 -> 11*
34 -> 330*
35 -> 11*
41 -> 261,241,49,7
43 -> 40*
49 -> 40*
51 -> 40*
57 -> 40*
59 -> 40*
65 -> 235,218,11,64,8
69 -> 9*
77 -> 67*
79 -> 67*
85 -> 67*
87 -> 67*
93 -> 67*
95 -> 67*
101 -> 67*
103 -> 67*
109 -> 67*
111 -> 67*
117 -> 67*
118 -> 234*
119 -> 67*
124 -> 226*
125 -> 67*
126 -> 228*
127 -> 67*
132 -> 217*
133 -> 67*
134 -> 220*
135 -> 67*
140 -> 236*
141 -> 67*
142 -> 240*
143 -> 67*
148 -> 258*
149 -> 67*
150 -> 260*
151 -> 67*
156 -> 250*
157 -> 67*
158 -> 252*
159 -> 67*
164 -> 243*
165 -> 67*
167 -> 67*
173 -> 67*
175 -> 67*
181 -> 67*
183 -> 67*
189 -> 67*
191 -> 67*
197 -> 67*
199 -> 67*
205 -> 67*
207 -> 67*
213 -> 67*
218 -> 276*
219 -> 269,68
221 -> 218*
227 -> 218*
229 -> 218*
235 -> 218*
237 -> 218*
240 -> 306*
242 -> 274,68
243 -> 296*
244 -> 241*
250 -> 304*
251 -> 241*
252 -> 286*
253 -> 241*
258 -> 290*
259 -> 241*
260 -> 298*
261 -> 241*
271 -> 69,9
275 -> 270*
276 -> 350*
278 -> 347,270
289 -> 275,270
291 -> 287*
297 -> 287*
299 -> 287*
305 -> 287*
307 -> 287*
312 -> 311,277
321 -> 367*
322 -> 358*
323 -> 311,277
325 -> 321*
331 -> 321*
333 -> 321*
339 -> 321*
341 -> 321*
349 -> 271,69
352 -> 360*
353 -> 348*
360 -> 352*
369 -> 351*
problem:
QedTool IRC1
stdout:
MAYBE
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:
{ 0(q0(0(x1))) -> 0(0(q0(x1)))
, 0(q0(h(x1))) -> 0(0(q0(h(x1))))
, 0(q0(1(x1))) -> 0(1(q0(x1)))
, 1(q0(0(x1))) -> 0(0(q1(x1)))
, 1(q0(h(x1))) -> 0(0(q1(h(x1))))
, 1(q0(1(x1))) -> 0(1(q1(x1)))
, 1(q1(0(x1))) -> 1(0(q1(x1)))
, 1(q1(h(x1))) -> 1(0(q1(h(x1))))
, 1(q1(1(x1))) -> 1(1(q1(x1)))
, 0(q1(0(x1))) -> 0(0(q2(x1)))
, 0(q1(h(x1))) -> 0(0(q2(h(x1))))
, 0(q1(1(x1))) -> 0(1(q2(x1)))
, 1(q2(0(x1))) -> 1(0(q2(x1)))
, 1(q2(h(x1))) -> 1(0(q2(h(x1))))
, 1(q2(1(x1))) -> 1(1(q2(x1)))
, 0(q2(x1)) -> q3(1(x1))
, 1(q3(x1)) -> q3(1(x1))
, 0(q3(x1)) -> q4(0(x1))
, 1(q4(x1)) -> q4(1(x1))
, 0(q4(0(x1))) -> 1(0(q5(x1)))
, 0(q4(h(x1))) -> 1(0(q5(h(x1))))
, 0(q4(1(x1))) -> 1(1(q5(x1)))
, 1(q5(0(x1))) -> 0(0(q1(x1)))
, 1(q5(h(x1))) -> 0(0(q1(h(x1))))
, 1(q5(1(x1))) -> 0(1(q1(x1)))
, h(q0(x1)) -> h(0(q0(x1)))
, h(q1(x1)) -> h(0(q1(x1)))
, h(q2(x1)) -> h(0(q2(x1)))
, h(q3(x1)) -> h(0(q3(x1)))
, h(q4(x1)) -> h(0(q4(x1)))
, h(q5(x1)) -> h(0(q5(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:
{ 0(q0(0(x1))) -> 0(0(q0(x1)))
, 0(q0(h(x1))) -> 0(0(q0(h(x1))))
, 0(q0(1(x1))) -> 0(1(q0(x1)))
, 1(q0(0(x1))) -> 0(0(q1(x1)))
, 1(q0(h(x1))) -> 0(0(q1(h(x1))))
, 1(q0(1(x1))) -> 0(1(q1(x1)))
, 1(q1(0(x1))) -> 1(0(q1(x1)))
, 1(q1(h(x1))) -> 1(0(q1(h(x1))))
, 1(q1(1(x1))) -> 1(1(q1(x1)))
, 0(q1(0(x1))) -> 0(0(q2(x1)))
, 0(q1(h(x1))) -> 0(0(q2(h(x1))))
, 0(q1(1(x1))) -> 0(1(q2(x1)))
, 1(q2(0(x1))) -> 1(0(q2(x1)))
, 1(q2(h(x1))) -> 1(0(q2(h(x1))))
, 1(q2(1(x1))) -> 1(1(q2(x1)))
, 0(q2(x1)) -> q3(1(x1))
, 1(q3(x1)) -> q3(1(x1))
, 0(q3(x1)) -> q4(0(x1))
, 1(q4(x1)) -> q4(1(x1))
, 0(q4(0(x1))) -> 1(0(q5(x1)))
, 0(q4(h(x1))) -> 1(0(q5(h(x1))))
, 0(q4(1(x1))) -> 1(1(q5(x1)))
, 1(q5(0(x1))) -> 0(0(q1(x1)))
, 1(q5(h(x1))) -> 0(0(q1(h(x1))))
, 1(q5(1(x1))) -> 0(1(q1(x1)))
, h(q0(x1)) -> h(0(q0(x1)))
, h(q1(x1)) -> h(0(q1(x1)))
, h(q2(x1)) -> h(0(q2(x1)))
, h(q3(x1)) -> h(0(q3(x1)))
, h(q4(x1)) -> h(0(q4(x1)))
, h(q5(x1)) -> h(0(q5(x1)))}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(2) -> 4
, 0_1(6) -> 5
, 0_2(2) -> 8
, 0_2(3) -> 16
, 0_2(5) -> 9
, 0_3(7) -> 10
, 0_3(9) -> 15
, 0_3(12) -> 11
, 0_3(21) -> 19
, 0_4(18) -> 17
, q0_0(2) -> 2
, q0_1(2) -> 6
, h_0(2) -> 1
, h_1(5) -> 1
, h_2(9) -> 1
, h_3(15) -> 1
, 1_0(2) -> 1
, 1_1(2) -> 3
, 1_2(2) -> 7
, 1_2(13) -> 10
, 1_2(13) -> 16
, 1_2(14) -> 13
, 1_3(11) -> 9
, 1_3(19) -> 15
, 1_3(20) -> 19
, 1_3(22) -> 21
, 1_4(17) -> 15
, q1_0(2) -> 2
, q1_1(2) -> 6
, q1_3(14) -> 22
, q2_0(2) -> 2
, q2_1(2) -> 6
, q3_0(2) -> 2
, q3_1(2) -> 6
, q3_1(3) -> 1
, q3_1(3) -> 3
, q3_1(3) -> 4
, q3_1(3) -> 7
, q3_1(3) -> 8
, q3_2(7) -> 5
, q4_0(2) -> 2
, q4_1(2) -> 6
, q4_1(3) -> 1
, q4_1(3) -> 3
, q4_1(3) -> 7
, q4_1(4) -> 1
, q4_1(4) -> 4
, q4_1(4) -> 8
, q4_2(8) -> 5
, q4_2(16) -> 10
, q4_2(16) -> 16
, q4_3(10) -> 9
, q5_0(2) -> 2
, q5_1(2) -> 6
, q5_2(2) -> 14
, q5_3(2) -> 12
, q5_3(13) -> 20
, q5_4(7) -> 18}Tool RC1
stdout:
MAYBE
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:
{ 0(q0(0(x1))) -> 0(0(q0(x1)))
, 0(q0(h(x1))) -> 0(0(q0(h(x1))))
, 0(q0(1(x1))) -> 0(1(q0(x1)))
, 1(q0(0(x1))) -> 0(0(q1(x1)))
, 1(q0(h(x1))) -> 0(0(q1(h(x1))))
, 1(q0(1(x1))) -> 0(1(q1(x1)))
, 1(q1(0(x1))) -> 1(0(q1(x1)))
, 1(q1(h(x1))) -> 1(0(q1(h(x1))))
, 1(q1(1(x1))) -> 1(1(q1(x1)))
, 0(q1(0(x1))) -> 0(0(q2(x1)))
, 0(q1(h(x1))) -> 0(0(q2(h(x1))))
, 0(q1(1(x1))) -> 0(1(q2(x1)))
, 1(q2(0(x1))) -> 1(0(q2(x1)))
, 1(q2(h(x1))) -> 1(0(q2(h(x1))))
, 1(q2(1(x1))) -> 1(1(q2(x1)))
, 0(q2(x1)) -> q3(1(x1))
, 1(q3(x1)) -> q3(1(x1))
, 0(q3(x1)) -> q4(0(x1))
, 1(q4(x1)) -> q4(1(x1))
, 0(q4(0(x1))) -> 1(0(q5(x1)))
, 0(q4(h(x1))) -> 1(0(q5(h(x1))))
, 0(q4(1(x1))) -> 1(1(q5(x1)))
, 1(q5(0(x1))) -> 0(0(q1(x1)))
, 1(q5(h(x1))) -> 0(0(q1(h(x1))))
, 1(q5(1(x1))) -> 0(1(q1(x1)))
, h(q0(x1)) -> h(0(q0(x1)))
, h(q1(x1)) -> h(0(q1(x1)))
, h(q2(x1)) -> h(0(q2(x1)))
, h(q3(x1)) -> h(0(q3(x1)))
, h(q4(x1)) -> h(0(q4(x1)))
, h(q5(x1)) -> h(0(q5(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:
{ 0(q0(0(x1))) -> 0(0(q0(x1)))
, 0(q0(h(x1))) -> 0(0(q0(h(x1))))
, 0(q0(1(x1))) -> 0(1(q0(x1)))
, 1(q0(0(x1))) -> 0(0(q1(x1)))
, 1(q0(h(x1))) -> 0(0(q1(h(x1))))
, 1(q0(1(x1))) -> 0(1(q1(x1)))
, 1(q1(0(x1))) -> 1(0(q1(x1)))
, 1(q1(h(x1))) -> 1(0(q1(h(x1))))
, 1(q1(1(x1))) -> 1(1(q1(x1)))
, 0(q1(0(x1))) -> 0(0(q2(x1)))
, 0(q1(h(x1))) -> 0(0(q2(h(x1))))
, 0(q1(1(x1))) -> 0(1(q2(x1)))
, 1(q2(0(x1))) -> 1(0(q2(x1)))
, 1(q2(h(x1))) -> 1(0(q2(h(x1))))
, 1(q2(1(x1))) -> 1(1(q2(x1)))
, 0(q2(x1)) -> q3(1(x1))
, 1(q3(x1)) -> q3(1(x1))
, 0(q3(x1)) -> q4(0(x1))
, 1(q4(x1)) -> q4(1(x1))
, 0(q4(0(x1))) -> 1(0(q5(x1)))
, 0(q4(h(x1))) -> 1(0(q5(h(x1))))
, 0(q4(1(x1))) -> 1(1(q5(x1)))
, 1(q5(0(x1))) -> 0(0(q1(x1)))
, 1(q5(h(x1))) -> 0(0(q1(h(x1))))
, 1(q5(1(x1))) -> 0(1(q1(x1)))
, h(q0(x1)) -> h(0(q0(x1)))
, h(q1(x1)) -> h(0(q1(x1)))
, h(q2(x1)) -> h(0(q2(x1)))
, h(q3(x1)) -> h(0(q3(x1)))
, h(q4(x1)) -> h(0(q4(x1)))
, h(q5(x1)) -> h(0(q5(x1)))}
Proof Output:
The problem is match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(2) -> 4
, 0_1(6) -> 5
, 0_2(2) -> 8
, 0_2(3) -> 16
, 0_2(5) -> 9
, 0_3(7) -> 10
, 0_3(9) -> 15
, 0_3(12) -> 11
, 0_3(21) -> 19
, 0_4(18) -> 17
, q0_0(2) -> 2
, q0_1(2) -> 6
, h_0(2) -> 1
, h_1(5) -> 1
, h_2(9) -> 1
, h_3(15) -> 1
, 1_0(2) -> 1
, 1_1(2) -> 3
, 1_2(2) -> 7
, 1_2(13) -> 10
, 1_2(13) -> 16
, 1_2(14) -> 13
, 1_3(11) -> 9
, 1_3(19) -> 15
, 1_3(20) -> 19
, 1_3(22) -> 21
, 1_4(17) -> 15
, q1_0(2) -> 2
, q1_1(2) -> 6
, q1_3(14) -> 22
, q2_0(2) -> 2
, q2_1(2) -> 6
, q3_0(2) -> 2
, q3_1(2) -> 6
, q3_1(3) -> 1
, q3_1(3) -> 3
, q3_1(3) -> 4
, q3_1(3) -> 7
, q3_1(3) -> 8
, q3_2(7) -> 5
, q4_0(2) -> 2
, q4_1(2) -> 6
, q4_1(3) -> 1
, q4_1(3) -> 3
, q4_1(3) -> 7
, q4_1(4) -> 1
, q4_1(4) -> 4
, q4_1(4) -> 8
, q4_2(8) -> 5
, q4_2(16) -> 10
, q4_2(16) -> 16
, q4_3(10) -> 9
, q5_0(2) -> 2
, q5_1(2) -> 6
, q5_2(2) -> 14
, q5_3(2) -> 12
, q5_3(13) -> 20
, q5_4(7) -> 18}