Tool CaT
stdout:
YES(?,O(n^1))
Problem:
0(1(2(3(4(5(1(x1))))))) -> 0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))
0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6}
transitions:
11(75) -> 76*
11(70) -> 71*
11(40) -> 41*
11(67) -> 68*
11(37) -> 38*
11(69) -> 70*
11(39) -> 40*
11(31) -> 32*
21(30) -> 31*
21(74) -> 75*
21(44) -> 45*
21(66) -> 67*
21(36) -> 37*
31(65) -> 66*
31(35) -> 36*
31(29) -> 30*
31(73) -> 74*
31(43) -> 44*
41(72) -> 73*
41(42) -> 43*
41(64) -> 65*
41(34) -> 35*
41(28) -> 29*
51(55) -> 56*
51(47) -> 48*
51(27) -> 28*
51(71) -> 72*
51(61) -> 62*
51(41) -> 42*
51(93) -> 94*
51(63) -> 64*
51(53) -> 54*
51(33) -> 34*
01(45) -> 46*
01(32) -> 33*
01(68) -> 69*
01(38) -> 39*
12(197) -> 198*
12(107) -> 108*
12(219) -> 220*
12(214) -> 215*
12(199) -> 200*
12(99) -> 100*
12(211) -> 212*
12(191) -> 192*
12(161) -> 162*
12(156) -> 157*
12(213) -> 214*
12(153) -> 154*
12(108) -> 109*
12(200) -> 201*
12(155) -> 156*
12(105) -> 106*
00(5) -> 6*
00(2) -> 6*
00(4) -> 6*
00(1) -> 6*
00(3) -> 6*
22(152) -> 153*
22(112) -> 113*
22(204) -> 205*
22(104) -> 105*
22(196) -> 197*
22(218) -> 219*
22(98) -> 99*
22(210) -> 211*
22(190) -> 191*
22(160) -> 161*
10(5) -> 1*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
32(217) -> 218*
32(97) -> 98*
32(209) -> 210*
32(189) -> 190*
32(159) -> 160*
32(151) -> 152*
32(111) -> 112*
32(203) -> 204*
32(103) -> 104*
32(195) -> 196*
20(5) -> 2*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
42(202) -> 203*
42(102) -> 103*
42(194) -> 195*
42(216) -> 217*
42(96) -> 97*
42(208) -> 209*
42(188) -> 189*
42(158) -> 159*
42(150) -> 151*
42(110) -> 111*
30(5) -> 3*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
52(237) -> 238*
52(207) -> 208*
52(187) -> 188*
52(157) -> 158*
52(149) -> 150*
52(109) -> 110*
52(201) -> 202*
52(101) -> 102*
52(193) -> 194*
52(163) -> 164*
52(235) -> 236*
52(215) -> 216*
52(95) -> 96*
40(5) -> 4*
40(2) -> 4*
40(4) -> 4*
40(1) -> 4*
40(3) -> 4*
02(212) -> 213*
02(192) -> 193*
02(154) -> 155*
02(106) -> 107*
02(198) -> 199*
02(113) -> 114*
02(205) -> 206*
02(100) -> 101*
50(5) -> 5*
50(2) -> 5*
50(4) -> 5*
50(1) -> 5*
50(3) -> 5*
1 -> 55*
2 -> 47*
3 -> 61*
4 -> 53*
5 -> 27*
39 -> 63*
46 -> 33,6
48 -> 28*
54 -> 28*
56 -> 28*
62 -> 28*
69 -> 93*
75 -> 95*
76 -> 33,6
94 -> 64*
107 -> 149*
114 -> 39*
155 -> 163*
161 -> 187*
162 -> 39*
164 -> 150*
199 -> 207*
206 -> 69*
213 -> 235*
219 -> 237*
220 -> 69*
236 -> 208*
238 -> 188*
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(1(2(3(4(5(1(x1))))))) ->
0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(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(1(2(3(4(5(1(x1))))))) ->
0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(3) -> 1
, 0_1(3) -> 15
, 0_1(10) -> 9
, 0_1(16) -> 15
, 0_1(28) -> 27
, 0_2(40) -> 39
, 0_2(46) -> 45
, 0_2(52) -> 51
, 0_2(58) -> 57
, 0_2(63) -> 9
, 0_2(69) -> 27
, 0_2(76) -> 75
, 0_2(82) -> 81
, 0_2(87) -> 27
, 0_2(94) -> 93
, 1_0(2) -> 2
, 1_1(8) -> 7
, 1_1(9) -> 8
, 1_1(11) -> 10
, 1_1(17) -> 16
, 1_1(21) -> 1
, 1_1(21) -> 15
, 1_1(26) -> 25
, 1_1(27) -> 26
, 1_1(29) -> 28
, 1_2(33) -> 9
, 1_2(38) -> 37
, 1_2(39) -> 38
, 1_2(41) -> 40
, 1_2(45) -> 38
, 1_2(47) -> 46
, 1_2(51) -> 68
, 1_2(53) -> 52
, 1_2(59) -> 58
, 1_2(68) -> 67
, 1_2(74) -> 73
, 1_2(75) -> 74
, 1_2(77) -> 76
, 1_2(83) -> 82
, 1_2(87) -> 27
, 1_2(92) -> 91
, 1_2(93) -> 92
, 1_2(95) -> 94
, 2_0(2) -> 2
, 2_1(4) -> 3
, 2_1(12) -> 11
, 2_1(18) -> 17
, 2_1(22) -> 21
, 2_1(30) -> 29
, 2_2(34) -> 33
, 2_2(42) -> 41
, 2_2(48) -> 47
, 2_2(54) -> 53
, 2_2(60) -> 59
, 2_2(64) -> 63
, 2_2(70) -> 69
, 2_2(78) -> 77
, 2_2(84) -> 83
, 2_2(88) -> 87
, 2_2(96) -> 95
, 3_0(2) -> 2
, 3_1(5) -> 4
, 3_1(13) -> 12
, 3_1(19) -> 18
, 3_1(23) -> 22
, 3_1(31) -> 30
, 3_2(35) -> 34
, 3_2(43) -> 42
, 3_2(49) -> 48
, 3_2(55) -> 54
, 3_2(61) -> 60
, 3_2(65) -> 64
, 3_2(71) -> 70
, 3_2(79) -> 78
, 3_2(85) -> 84
, 3_2(89) -> 88
, 3_2(97) -> 96
, 4_0(2) -> 2
, 4_1(6) -> 5
, 4_1(14) -> 13
, 4_1(20) -> 19
, 4_1(24) -> 23
, 4_1(32) -> 31
, 4_2(36) -> 35
, 4_2(44) -> 43
, 4_2(50) -> 49
, 4_2(56) -> 55
, 4_2(62) -> 61
, 4_2(66) -> 65
, 4_2(72) -> 71
, 4_2(80) -> 79
, 4_2(86) -> 85
, 4_2(90) -> 89
, 4_2(98) -> 97
, 5_0(2) -> 2
, 5_1(2) -> 20
, 5_1(7) -> 6
, 5_1(9) -> 32
, 5_1(15) -> 14
, 5_1(25) -> 24
, 5_1(27) -> 32
, 5_2(21) -> 62
, 5_2(33) -> 86
, 5_2(37) -> 36
, 5_2(45) -> 44
, 5_2(51) -> 50
, 5_2(57) -> 56
, 5_2(67) -> 66
, 5_2(73) -> 72
, 5_2(75) -> 98
, 5_2(81) -> 80
, 5_2(87) -> 80
, 5_2(91) -> 90
, 5_2(93) -> 98}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(1(2(3(4(5(1(x1))))))) ->
0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(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(1(2(3(4(5(1(x1))))))) ->
0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))
, 0(1(2(3(4(5(1(x1))))))) ->
1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))))))))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ 0_0(2) -> 1
, 0_1(3) -> 1
, 0_1(3) -> 15
, 0_1(10) -> 9
, 0_1(16) -> 15
, 0_1(28) -> 27
, 0_2(40) -> 39
, 0_2(46) -> 45
, 0_2(52) -> 51
, 0_2(58) -> 57
, 0_2(63) -> 9
, 0_2(69) -> 27
, 0_2(76) -> 75
, 0_2(82) -> 81
, 0_2(87) -> 27
, 0_2(94) -> 93
, 1_0(2) -> 2
, 1_1(8) -> 7
, 1_1(9) -> 8
, 1_1(11) -> 10
, 1_1(17) -> 16
, 1_1(21) -> 1
, 1_1(21) -> 15
, 1_1(26) -> 25
, 1_1(27) -> 26
, 1_1(29) -> 28
, 1_2(33) -> 9
, 1_2(38) -> 37
, 1_2(39) -> 38
, 1_2(41) -> 40
, 1_2(45) -> 38
, 1_2(47) -> 46
, 1_2(51) -> 68
, 1_2(53) -> 52
, 1_2(59) -> 58
, 1_2(68) -> 67
, 1_2(74) -> 73
, 1_2(75) -> 74
, 1_2(77) -> 76
, 1_2(83) -> 82
, 1_2(87) -> 27
, 1_2(92) -> 91
, 1_2(93) -> 92
, 1_2(95) -> 94
, 2_0(2) -> 2
, 2_1(4) -> 3
, 2_1(12) -> 11
, 2_1(18) -> 17
, 2_1(22) -> 21
, 2_1(30) -> 29
, 2_2(34) -> 33
, 2_2(42) -> 41
, 2_2(48) -> 47
, 2_2(54) -> 53
, 2_2(60) -> 59
, 2_2(64) -> 63
, 2_2(70) -> 69
, 2_2(78) -> 77
, 2_2(84) -> 83
, 2_2(88) -> 87
, 2_2(96) -> 95
, 3_0(2) -> 2
, 3_1(5) -> 4
, 3_1(13) -> 12
, 3_1(19) -> 18
, 3_1(23) -> 22
, 3_1(31) -> 30
, 3_2(35) -> 34
, 3_2(43) -> 42
, 3_2(49) -> 48
, 3_2(55) -> 54
, 3_2(61) -> 60
, 3_2(65) -> 64
, 3_2(71) -> 70
, 3_2(79) -> 78
, 3_2(85) -> 84
, 3_2(89) -> 88
, 3_2(97) -> 96
, 4_0(2) -> 2
, 4_1(6) -> 5
, 4_1(14) -> 13
, 4_1(20) -> 19
, 4_1(24) -> 23
, 4_1(32) -> 31
, 4_2(36) -> 35
, 4_2(44) -> 43
, 4_2(50) -> 49
, 4_2(56) -> 55
, 4_2(62) -> 61
, 4_2(66) -> 65
, 4_2(72) -> 71
, 4_2(80) -> 79
, 4_2(86) -> 85
, 4_2(90) -> 89
, 4_2(98) -> 97
, 5_0(2) -> 2
, 5_1(2) -> 20
, 5_1(7) -> 6
, 5_1(9) -> 32
, 5_1(15) -> 14
, 5_1(25) -> 24
, 5_1(27) -> 32
, 5_2(21) -> 62
, 5_2(33) -> 86
, 5_2(37) -> 36
, 5_2(45) -> 44
, 5_2(51) -> 50
, 5_2(57) -> 56
, 5_2(67) -> 66
, 5_2(73) -> 72
, 5_2(75) -> 98
, 5_2(81) -> 80
, 5_2(87) -> 80
, 5_2(91) -> 90
, 5_2(93) -> 98}