Tool CaT
stdout:
YES(?,O(n^1))
Problem:
R(2(x1)) -> 2(R(x1))
R(3(x1)) -> 3(R(x1))
R(1(x1)) -> L(3(x1))
3(L(x1)) -> L(3(x1))
2(L(x1)) -> L(2(x1))
0(L(x1)) -> 2(R(x1))
R(b(x1)) -> c(1(b(x1)))
3(c(x1)) -> c(1(x1))
2(c(1(x1))) -> c(0(R(1(x1))))
2(c(0(x1))) -> c(0(0(x1)))
Proof:
Bounds Processor:
bound: 6
enrichment: match
automaton:
final states: {8,7,6,5}
transitions:
R3(152) -> 153*
R3(324) -> 325*
R3(299) -> 300*
R3(234) -> 235*
R3(216) -> 217*
R3(161) -> 162*
R3(163) -> 164*
R3(155) -> 156*
23(217) -> 218*
23(264) -> 265*
23(235) -> 236*
34(247) -> 248*
34(306) -> 307*
34(383) -> 384*
34(328) -> 329*
34(223) -> 224*
34(407) -> 408*
R4(222) -> 223*
R4(334) -> 335*
R4(259) -> 260*
R4(246) -> 247*
R4(343) -> 344*
R4(253) -> 254*
R4(255) -> 256*
R4(362) -> 363*
c3(326) -> 327*
c3(301) -> 302*
c3(313) -> 314*
03(325) -> 326*
03(300) -> 301*
13(323) -> 324*
13(298) -> 299*
13(312) -> 313*
b2(277) -> 278*
b2(283) -> 284*
b2(273) -> 274*
b2(285) -> 286*
L4(307) -> 308*
L4(414) -> 415*
L4(384) -> 385*
L4(329) -> 330*
L4(408) -> 409*
R0(2) -> 5*
R0(4) -> 5*
R0(1) -> 5*
R0(3) -> 5*
c4(345) -> 346*
20(2) -> 7*
20(4) -> 7*
20(1) -> 7*
20(3) -> 7*
04(344) -> 345*
30(2) -> 6*
30(4) -> 6*
30(1) -> 6*
30(3) -> 6*
14(342) -> 343*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
24(413) -> 414*
24(363) -> 364*
24(335) -> 336*
L0(2) -> 2*
L0(4) -> 2*
L0(1) -> 2*
L0(3) -> 2*
L5(420) -> 421*
L5(402) -> 403*
L5(357) -> 358*
00(2) -> 8*
00(4) -> 8*
00(1) -> 8*
00(3) -> 8*
35(366) -> 367*
35(356) -> 357*
35(351) -> 352*
b0(2) -> 3*
b0(4) -> 3*
b0(1) -> 3*
b0(3) -> 3*
R5(371) -> 372*
R5(365) -> 366*
R5(350) -> 351*
c0(2) -> 4*
c0(4) -> 4*
c0(1) -> 4*
c0(3) -> 4*
25(419) -> 420*
25(401) -> 402*
25(372) -> 373*
c1(65) -> 66*
c1(84) -> 85*
c1(103) -> 104*
36(375) -> 376*
01(102) -> 103*
R6(374) -> 375*
R1(55) -> 56*
R1(45) -> 46*
R1(101) -> 102*
R1(61) -> 62*
R1(53) -> 54*
11(99) -> 100*
11(64) -> 65*
11(91) -> 92*
11(93) -> 94*
11(83) -> 84*
b1(75) -> 76*
b1(81) -> 82*
b1(73) -> 74*
b1(63) -> 64*
21(35) -> 36*
21(37) -> 38*
21(27) -> 28*
21(46) -> 47*
21(43) -> 44*
L1(28) -> 29*
L1(13) -> 14*
31(15) -> 16*
31(12) -> 13*
31(21) -> 22*
31(23) -> 24*
L2(229) -> 230*
L2(131) -> 132*
L2(110) -> 111*
32(117) -> 118*
32(119) -> 120*
32(109) -> 110*
32(228) -> 229*
32(125) -> 126*
c2(147) -> 148*
c2(296) -> 297*
c2(181) -> 182*
c2(238) -> 239*
c2(275) -> 276*
02(146) -> 147*
02(180) -> 181*
R2(179) -> 180*
R2(133) -> 134*
R2(145) -> 146*
12(237) -> 238*
12(274) -> 275*
12(189) -> 190*
12(144) -> 145*
12(191) -> 192*
12(183) -> 184*
12(178) -> 179*
12(295) -> 296*
22(134) -> 135*
22(130) -> 131*
L3(396) -> 397*
L3(196) -> 197*
L3(171) -> 172*
L3(390) -> 391*
L3(265) -> 266*
33(389) -> 390*
33(211) -> 212*
33(203) -> 204*
33(395) -> 396*
33(153) -> 154*
33(205) -> 206*
33(195) -> 196*
33(170) -> 171*
1 -> 93,75,55,37,21
2 -> 83,63,45,27,12
3 -> 99,81,61,43,23
4 -> 91,73,53,35,15
13 -> 228,130
14 -> 260,247,204,196,156,153,126,110,13,56,46,6,5
16 -> 13*
22 -> 13*
24 -> 13*
29 -> 28,7
36 -> 28*
38 -> 28*
44 -> 28*
47 -> 8*
54 -> 46*
56 -> 46*
62 -> 46*
63 -> 285*
64 -> 144*
65 -> 237*
66 -> 247,162,153,62,46,5
73 -> 283*
74 -> 64*
75 -> 273*
76 -> 64*
81 -> 277*
82 -> 64*
83 -> 191,125
84 -> 295,101
85 -> 206,196,118,110,16,13,6
91 -> 183,117
92 -> 84*
93 -> 189,119
94 -> 84*
99 -> 178,109
100 -> 84*
104 -> 36,28,7
109 -> 161*
110 -> 395,133
111 -> 366,102
117 -> 152*
118 -> 110*
119 -> 155*
120 -> 110*
125 -> 163*
126 -> 110*
132 -> 131,47
135 -> 103*
144 -> 170*
148 -> 47,8
154 -> 134*
156 -> 153*
162 -> 153*
164 -> 153*
170 -> 222*
171 -> 383,216
172 -> 351,146
178 -> 211*
182 -> 131*
183 -> 205*
184 -> 179*
189 -> 195*
190 -> 179*
191 -> 203*
192 -> 179*
195 -> 259*
196 -> 234*
197 -> 180*
203 -> 253*
204 -> 196*
205 -> 255*
206 -> 196*
211 -> 246*
212 -> 196*
218 -> 147*
224 -> 217*
229 -> 264*
230 -> 396,248,235,229,154,134
236 -> 181*
237 -> 298*
239 -> 248,235,154,134
248 -> 235*
254 -> 247*
256 -> 247*
260 -> 247*
266 -> 414,236,265,135,103
274 -> 389*
275 -> 312*
276 -> 223*
278 -> 274*
284 -> 274*
286 -> 274*
295 -> 323*
297 -> 396,229
298 -> 306*
302 -> 236,135,103
306 -> 350*
307 -> 334*
308 -> 300*
312 -> 342*
314 -> 224,217
323 -> 328*
327 -> 414,265
328 -> 365*
329 -> 362*
330 -> 325*
336 -> 301*
342 -> 356*
346 -> 218,147
352 -> 335*
356 -> 374*
357 -> 371*
358 -> 344*
364 -> 326*
367 -> 363*
373 -> 345*
376 -> 372*
384 -> 401*
385 -> 352,335
390 -> 407*
391 -> 375*
396 -> 413*
397 -> 367,363
403 -> 336,301
408 -> 419*
409 -> 376,372
415 -> 364,326
421 -> 373,345
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:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Proof Output:
The problem is match-bounded by 6.
The enriched problem is compatible with the following automaton:
{ R_0(4) -> 1
, R_0(5) -> 1
, R_0(7) -> 1
, R_0(8) -> 1
, R_1(4) -> 11
, R_1(5) -> 11
, R_1(7) -> 11
, R_1(8) -> 11
, R_1(14) -> 16
, R_2(19) -> 18
, R_2(20) -> 23
, R_2(27) -> 26
, R_3(4) -> 28
, R_3(5) -> 28
, R_3(7) -> 28
, R_3(8) -> 28
, R_3(21) -> 24
, R_3(30) -> 33
, R_3(41) -> 40
, R_3(44) -> 43
, R_4(4) -> 48
, R_4(5) -> 48
, R_4(7) -> 48
, R_4(8) -> 48
, R_4(13) -> 29
, R_4(47) -> 46
, R_4(49) -> 52
, R_4(50) -> 53
, R_5(12) -> 55
, R_5(14) -> 56
, R_5(51) -> 54
, R_6(34) -> 57
, 2_0(4) -> 2
, 2_0(5) -> 2
, 2_0(7) -> 2
, 2_0(8) -> 2
, 2_1(4) -> 10
, 2_1(5) -> 10
, 2_1(7) -> 10
, 2_1(8) -> 10
, 2_1(11) -> 6
, 2_2(9) -> 22
, 2_2(23) -> 15
, 2_3(24) -> 17
, 2_3(31) -> 32
, 2_3(33) -> 25
, 2_4(52) -> 39
, 2_4(53) -> 42
, 2_4(60) -> 63
, 2_4(61) -> 64
, 2_5(54) -> 45
, 2_5(62) -> 65
, 3_0(4) -> 3
, 3_0(5) -> 3
, 3_0(7) -> 3
, 3_0(8) -> 3
, 3_1(4) -> 9
, 3_1(5) -> 9
, 3_1(7) -> 9
, 3_1(8) -> 9
, 3_2(4) -> 20
, 3_2(5) -> 20
, 3_2(7) -> 20
, 3_2(8) -> 20
, 3_2(9) -> 31
, 3_2(13) -> 58
, 3_3(4) -> 30
, 3_3(5) -> 30
, 3_3(7) -> 30
, 3_3(8) -> 30
, 3_3(13) -> 21
, 3_3(20) -> 60
, 3_3(28) -> 23
, 3_3(35) -> 59
, 3_3(58) -> 61
, 3_4(12) -> 49
, 3_4(14) -> 50
, 3_4(29) -> 24
, 3_4(48) -> 33
, 3_4(59) -> 62
, 3_5(34) -> 51
, 3_5(55) -> 52
, 3_5(56) -> 53
, 3_6(57) -> 54
, 1_0(4) -> 4
, 1_0(5) -> 4
, 1_0(7) -> 4
, 1_0(8) -> 4
, 1_1(4) -> 14
, 1_1(5) -> 14
, 1_1(7) -> 14
, 1_1(8) -> 14
, 1_1(13) -> 12
, 1_2(4) -> 27
, 1_2(5) -> 27
, 1_2(7) -> 27
, 1_2(8) -> 27
, 1_2(12) -> 36
, 1_2(13) -> 19
, 1_2(14) -> 37
, 1_2(35) -> 34
, 1_3(12) -> 41
, 1_3(14) -> 44
, 1_3(34) -> 38
, 1_4(34) -> 47
, L_0(4) -> 5
, L_0(5) -> 5
, L_0(7) -> 5
, L_0(8) -> 5
, L_1(9) -> 1
, L_1(9) -> 3
, L_1(9) -> 9
, L_1(9) -> 11
, L_1(9) -> 20
, L_1(9) -> 28
, L_1(9) -> 30
, L_1(9) -> 48
, L_1(10) -> 2
, L_1(10) -> 10
, L_2(20) -> 16
, L_2(20) -> 56
, L_2(22) -> 6
, L_2(22) -> 22
, L_2(31) -> 23
, L_2(31) -> 31
, L_2(31) -> 33
, L_2(31) -> 60
, L_2(58) -> 55
, L_3(21) -> 18
, L_3(30) -> 26
, L_3(32) -> 15
, L_3(32) -> 25
, L_3(32) -> 32
, L_3(32) -> 63
, L_3(59) -> 57
, L_3(60) -> 53
, L_3(61) -> 52
, L_4(49) -> 40
, L_4(50) -> 43
, L_4(62) -> 54
, L_4(63) -> 42
, L_4(64) -> 39
, L_5(51) -> 46
, L_5(65) -> 45
, 0_0(4) -> 6
, 0_0(5) -> 6
, 0_0(7) -> 6
, 0_0(8) -> 6
, 0_1(16) -> 15
, 0_2(18) -> 17
, 0_2(26) -> 25
, 0_3(40) -> 39
, 0_3(43) -> 42
, 0_4(46) -> 45
, b_0(4) -> 7
, b_0(5) -> 7
, b_0(7) -> 7
, b_0(8) -> 7
, b_1(4) -> 13
, b_1(5) -> 13
, b_1(7) -> 13
, b_1(8) -> 13
, b_2(4) -> 35
, b_2(5) -> 35
, b_2(7) -> 35
, b_2(8) -> 35
, c_0(4) -> 8
, c_0(5) -> 8
, c_0(7) -> 8
, c_0(8) -> 8
, c_1(12) -> 1
, c_1(12) -> 11
, c_1(12) -> 28
, c_1(12) -> 48
, c_1(14) -> 3
, c_1(14) -> 9
, c_1(14) -> 20
, c_1(14) -> 30
, c_1(15) -> 2
, c_1(15) -> 10
, c_2(17) -> 6
, c_2(25) -> 22
, c_2(34) -> 29
, c_2(36) -> 23
, c_2(36) -> 33
, c_2(37) -> 31
, c_2(37) -> 60
, c_3(38) -> 24
, c_3(39) -> 15
, c_3(39) -> 25
, c_3(42) -> 32
, c_3(42) -> 63
, c_4(45) -> 17}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:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ R(2(x1)) -> 2(R(x1))
, R(3(x1)) -> 3(R(x1))
, R(1(x1)) -> L(3(x1))
, 3(L(x1)) -> L(3(x1))
, 2(L(x1)) -> L(2(x1))
, 0(L(x1)) -> 2(R(x1))
, R(b(x1)) -> c(1(b(x1)))
, 3(c(x1)) -> c(1(x1))
, 2(c(1(x1))) -> c(0(R(1(x1))))
, 2(c(0(x1))) -> c(0(0(x1)))}
Proof Output:
The problem is match-bounded by 6.
The enriched problem is compatible with the following automaton:
{ R_0(4) -> 1
, R_0(5) -> 1
, R_0(7) -> 1
, R_0(8) -> 1
, R_1(4) -> 11
, R_1(5) -> 11
, R_1(7) -> 11
, R_1(8) -> 11
, R_1(14) -> 16
, R_2(19) -> 18
, R_2(20) -> 23
, R_2(27) -> 26
, R_3(4) -> 28
, R_3(5) -> 28
, R_3(7) -> 28
, R_3(8) -> 28
, R_3(21) -> 24
, R_3(30) -> 33
, R_3(41) -> 40
, R_3(44) -> 43
, R_4(4) -> 48
, R_4(5) -> 48
, R_4(7) -> 48
, R_4(8) -> 48
, R_4(13) -> 29
, R_4(47) -> 46
, R_4(49) -> 52
, R_4(50) -> 53
, R_5(12) -> 55
, R_5(14) -> 56
, R_5(51) -> 54
, R_6(34) -> 57
, 2_0(4) -> 2
, 2_0(5) -> 2
, 2_0(7) -> 2
, 2_0(8) -> 2
, 2_1(4) -> 10
, 2_1(5) -> 10
, 2_1(7) -> 10
, 2_1(8) -> 10
, 2_1(11) -> 6
, 2_2(9) -> 22
, 2_2(23) -> 15
, 2_3(24) -> 17
, 2_3(31) -> 32
, 2_3(33) -> 25
, 2_4(52) -> 39
, 2_4(53) -> 42
, 2_4(60) -> 63
, 2_4(61) -> 64
, 2_5(54) -> 45
, 2_5(62) -> 65
, 3_0(4) -> 3
, 3_0(5) -> 3
, 3_0(7) -> 3
, 3_0(8) -> 3
, 3_1(4) -> 9
, 3_1(5) -> 9
, 3_1(7) -> 9
, 3_1(8) -> 9
, 3_2(4) -> 20
, 3_2(5) -> 20
, 3_2(7) -> 20
, 3_2(8) -> 20
, 3_2(9) -> 31
, 3_2(13) -> 58
, 3_3(4) -> 30
, 3_3(5) -> 30
, 3_3(7) -> 30
, 3_3(8) -> 30
, 3_3(13) -> 21
, 3_3(20) -> 60
, 3_3(28) -> 23
, 3_3(35) -> 59
, 3_3(58) -> 61
, 3_4(12) -> 49
, 3_4(14) -> 50
, 3_4(29) -> 24
, 3_4(48) -> 33
, 3_4(59) -> 62
, 3_5(34) -> 51
, 3_5(55) -> 52
, 3_5(56) -> 53
, 3_6(57) -> 54
, 1_0(4) -> 4
, 1_0(5) -> 4
, 1_0(7) -> 4
, 1_0(8) -> 4
, 1_1(4) -> 14
, 1_1(5) -> 14
, 1_1(7) -> 14
, 1_1(8) -> 14
, 1_1(13) -> 12
, 1_2(4) -> 27
, 1_2(5) -> 27
, 1_2(7) -> 27
, 1_2(8) -> 27
, 1_2(12) -> 36
, 1_2(13) -> 19
, 1_2(14) -> 37
, 1_2(35) -> 34
, 1_3(12) -> 41
, 1_3(14) -> 44
, 1_3(34) -> 38
, 1_4(34) -> 47
, L_0(4) -> 5
, L_0(5) -> 5
, L_0(7) -> 5
, L_0(8) -> 5
, L_1(9) -> 1
, L_1(9) -> 3
, L_1(9) -> 9
, L_1(9) -> 11
, L_1(9) -> 20
, L_1(9) -> 28
, L_1(9) -> 30
, L_1(9) -> 48
, L_1(10) -> 2
, L_1(10) -> 10
, L_2(20) -> 16
, L_2(20) -> 56
, L_2(22) -> 6
, L_2(22) -> 22
, L_2(31) -> 23
, L_2(31) -> 31
, L_2(31) -> 33
, L_2(31) -> 60
, L_2(58) -> 55
, L_3(21) -> 18
, L_3(30) -> 26
, L_3(32) -> 15
, L_3(32) -> 25
, L_3(32) -> 32
, L_3(32) -> 63
, L_3(59) -> 57
, L_3(60) -> 53
, L_3(61) -> 52
, L_4(49) -> 40
, L_4(50) -> 43
, L_4(62) -> 54
, L_4(63) -> 42
, L_4(64) -> 39
, L_5(51) -> 46
, L_5(65) -> 45
, 0_0(4) -> 6
, 0_0(5) -> 6
, 0_0(7) -> 6
, 0_0(8) -> 6
, 0_1(16) -> 15
, 0_2(18) -> 17
, 0_2(26) -> 25
, 0_3(40) -> 39
, 0_3(43) -> 42
, 0_4(46) -> 45
, b_0(4) -> 7
, b_0(5) -> 7
, b_0(7) -> 7
, b_0(8) -> 7
, b_1(4) -> 13
, b_1(5) -> 13
, b_1(7) -> 13
, b_1(8) -> 13
, b_2(4) -> 35
, b_2(5) -> 35
, b_2(7) -> 35
, b_2(8) -> 35
, c_0(4) -> 8
, c_0(5) -> 8
, c_0(7) -> 8
, c_0(8) -> 8
, c_1(12) -> 1
, c_1(12) -> 11
, c_1(12) -> 28
, c_1(12) -> 48
, c_1(14) -> 3
, c_1(14) -> 9
, c_1(14) -> 20
, c_1(14) -> 30
, c_1(15) -> 2
, c_1(15) -> 10
, c_2(17) -> 6
, c_2(25) -> 22
, c_2(34) -> 29
, c_2(36) -> 23
, c_2(36) -> 33
, c_2(37) -> 31
, c_2(37) -> 60
, c_3(38) -> 24
, c_3(39) -> 15
, c_3(39) -> 25
, c_3(42) -> 32
, c_3(42) -> 63
, c_4(45) -> 17}