-
Notifications
You must be signed in to change notification settings - Fork 2
/
bdd-solve.rs
1322 lines (1317 loc) · 95.9 KB
/
bdd-solve.rs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
// note: i temporarily replaced '//!' with '///'
// until i get benchmarks cleanly factored out.
/// example for bdd-based general solver with bex:
///
/// ```text
/// NB. k =: 614889782588491410
/// k =: */2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
/// ```
///
/// That is, k is the product of the first 15 primes. This is the value with the
/// largest number of unique prime factors that still fits into a u64.
///
/// Now, we want to find all pairs (x,y) of 32 bit numbers such that x>y and x*y=k.
/// (The first condition strips out duplicates, but also just makes our BDD
/// a little more interesting.)
///
/// There are 2^15=32,768 ways to group the factors into two products that multiply to k.
/// But since we only care about one ordering, this brings us down to 2^14 = 16,384.
/// However, many of these (for example, 307,444,891,294,245,705 * 2) involve an x
/// that's too big to fit in a u32. Once we eliminate these numbers, we wind up with
/// 3827 possible solutions.
///
/// The list was generated with the following J program:
///
/// ```text
/// xy0 =: */L:0 (0,"1#:i.2^n-1) </."1 |.p:i.n=:15
/// xys =: ({~[:I.([:*./(2^32)>])"1) \:~\:~@;"1 xy0
/// txt =: ,(' ',LF,~}:)"1 ] _4 ;\ ([: < ','10} 3|.'), (', ": )"1 xys
/// txt 1!:2 <'nums.txt'
/// ```
/// Product of the first 15 primes: 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
const K:u64 = 614_889_782_588_491_410;
/// All 3,827 ordered pairs of 32-bit ints that multiply to produce K.
#[allow(clippy::unreadable_literal)]
fn factors()->Vec<(u64,u64)> {
vec![
(429400657, 143197215), (429319798, 143224185), (429192489, 143266669),
(429092163, 143300166), (428929966, 143354354), (428759840, 143411235),
(428350132, 143548405), (427995090, 143667485), (427896131, 143700711),
(427891905, 143702130), (427713143, 143762190), (427662391, 143779251),
(427545970, 143818402), (427435437, 143855593), (426797553, 144070597),
(426655128, 144118690), (426531359, 144160510), (426328023, 144229267),
(426239813, 144259115), (426222854, 144264855), (426079933, 144313246),
(425565809, 144487590), (425100439, 144645765), (424961733, 144692977),
(424871196, 144723810), (424832565, 144736970), (424808137, 144745293),
(424765183, 144759930), (424752566, 144764230), (424604622, 144814670),
(424302378, 144917826), (423948201, 145038894), (423417603, 145220647),
(423238297, 145282170), (423045486, 145348385), (423013691, 145359310),
(422631649, 145490709), (422600194, 145501538), (422138067, 145660823),
(421954460, 145724205), (421628699, 145836795), (421510316, 145877754),
(421470549, 145891518), (421182463, 145991307), (421139876, 146006070),
(420837796, 146110874), (420612792, 146189035), (420288901, 146301694),
(420261695, 146311165), (419962543, 146415387), (419803797, 146470753),
(419699049, 146507309), (419647728, 146525226), (419138301, 146703315),
(419014011, 146746831), (418508413, 146924115), (418489480, 146930762),
(418368079, 146973398), (418351433, 146979246), (418100640, 147067410),
(418065479, 147079779), (417804731, 147171570), (417577360, 147251705),
(417181219, 147391530), (417073365, 147429645), (416959827, 147469790),
(416910351, 147487291), (416736177, 147548933), (416732061, 147550390),
(416726040, 147552522), (416701798, 147561106), (416635706, 147584514),
(415864807, 147858095), (415727626, 147906885), (415570481, 147962815),
(415473340, 147997410), (415154807, 148110963), (414936506, 148188885),
(414843596, 148222074), (414679383, 148280770), (414088941, 148492201),
(414013399, 148519295), (413947734, 148542855), (413778529, 148603598),
(413642036, 148652634), (413559251, 148682391), (413336231, 148762614),
(413320303, 148768347), (412721809, 148984078), (412636415, 149014910),
(412597485, 149028970), (412500364, 149064058), (412179453, 149180115),
(412167186, 149184555), (412117088, 149202690), (412044963, 149228807),
(411063081, 149585261), (411029170, 149597602), (410943533, 149628777),
(410857453, 149660126), (410796341, 149682390), (410738266, 149703554),
(410533207, 149778330), (410498683, 149790927), (409913254, 150004855),
(409882445, 150016130), (409706214, 150080658), (409585449, 150124909),
(409544034, 150140090), (409428533, 150182445), (409287909, 150234045),
(408985323, 150345195), (408794743, 150415286), (408377369, 150569015),
(408088342, 150675655), (408066798, 150683610), (407782428, 150788690),
(407771117, 150792873), (407758981, 150797361), (407635042, 150843210),
(407554719, 150872939), (406849088, 151134610), (406810704, 151148870),
(406633481, 151214745), (406532638, 151252255), (406414705, 151296145),
(406398535, 151302165), (406017137, 151444293), (405769435, 151536742),
(405515671, 151631571), (405196071, 151751171), (405072911, 151797310),
(405049619, 151806039), (404974731, 151834111), (404836632, 151885905),
(404806502, 151897210), (404634416, 151961810), (404229680, 152113962),
(404192926, 152127794), (403723761, 152304581), (403421119, 152418838),
(403183781, 152508561), (403046279, 152560590), (402944371, 152599174),
(402231221, 152869730), (402055994, 152936355), (402018062, 152950785),
(402015471, 152951771), (401933852, 152982830), (401905185, 152993742),
(401804903, 153031926), (401530259, 153136599), (401320681, 153216570),
(401201674, 153262018), (401097915, 153301665), (400989061, 153343281),
(400797242, 153416670), (400740580, 153438362), (400714639, 153448295),
(400489961, 153534381), (400178163, 153654007), (400129229, 153672798),
(399174581, 154040315), (399042905, 154091145), (398654098, 154241430),
(398584329, 154268429), (398524021, 154291774), (398312827, 154373583),
(398155157, 154434715), (397674604, 154621335), (397544847, 154671803),
(397424012, 154718830), (397376497, 154737330), (397349175, 154747970),
(397290201, 154770941), (396988061, 154888734), (396830916, 154950070),
(396522258, 155070685), (395932600, 155301630), (395530333, 155459577),
(395500605, 155471262), (395365091, 155524551), (395332475, 155537382),
(394903353, 155706397), (394695701, 155788315), (394607323, 155823206),
(394533016, 155852554), (394426848, 155894505), (394075456, 156033514),
(393673110, 156192985), (393444023, 156283930), (393385629, 156307129),
(393255863, 156358707), (393173488, 156391466), (393158337, 156397493),
(392880081, 156508261), (392781943, 156547365), (392573681, 156630414),
(392269641, 156751815), (392061469, 156835045), (391894801, 156901745),
(391689535, 156983970), (391512364, 157055010), (391479439, 157068219),
(391475573, 157069770), (391438639, 157084590), (390818145, 157333990),
(390474357, 157472513), (390324763, 157532865), (390230817, 157570790),
(390044787, 157645943), (389927293, 157693445), (389840489, 157728558),
(389817811, 157737734), (389720545, 157777102), (389034820, 158055205),
(388921678, 158101185), (388862833, 158125110), (388710844, 158186938),
(388614955, 158225970), (388079493, 158444286), (387925874, 158507030),
(387868299, 158530559), (387830910, 158545842), (387755781, 158576561),
(387708366, 158595954), (387083140, 158852122), (387041615, 158869165),
(386878009, 158936349), (386654477, 159028233), (386211423, 159210667),
(386150167, 159235923), (386138697, 159240653), (385978292, 159306830),
(385600715, 159462822), (385393255, 159548662), (385298184, 159588030),
(384557901, 159895241), (384511159, 159914678), (384458467, 159936595),
(384431047, 159948003), (384299941, 160002570), (384047194, 160107870),
(384019304, 160119498), (383627225, 160283145), (383466956, 160350135),
(383355715, 160396665), (383317077, 160412833), (383179781, 160470310),
(382907024, 160584618), (382854433, 160606677), (382762285, 160645342),
(382726672, 160660290), (382541131, 160738214), (382407425, 160794415),
(382155510, 160900410), (381744062, 161073830), (381633321, 161120570),
(381541760, 161159235), (381473885, 161187910), (381428619, 161207039),
(381259994, 161278338), (381177348, 161313306), (380680006, 161524055),
(380351471, 161663574), (380272774, 161697030), (380207698, 161724706),
(380091491, 161774151), (380053059, 161790510), (379988020, 161818202),
(379909398, 161851690), (379822483, 161888727), (379727711, 161929131),
(379577398, 161993255), (379054389, 162216769), (378939174, 162266090),
(378882933, 162290177), (378847329, 162305429), (378811587, 162320743),
(378718139, 162360795), (378633339, 162397158), (378523500, 162444282),
(378144107, 162607263), (378115963, 162619366), (377551681, 162862414),
(377482805, 162892130), (377393950, 162930482), (377246731, 162994065),
(377105228, 163055226), (377043294, 163082010), (376337761, 163387745),
(376280820, 163412470), (376253494, 163424338), (376081413, 163499115),
(376078989, 163500169), (376047964, 163513658), (375799493, 163621770),
(375088623, 163931867), (375027019, 163958795), (374939355, 163997130),
(374886349, 164020318), (374651899, 164122959), (374583552, 164152905),
(374454896, 164209305), (374371050, 164246082), (374314440, 164270922),
(374024541, 164398245), (373826052, 164485535), (373621848, 164575435),
(373421382, 164663785), (373337708, 164700690), (373302486, 164716230),
(373267407, 164731710), (373212007, 164756163), (372869211, 164907631),
(372582728, 165034430), (372344072, 165140210), (372312759, 165154099),
(372188516, 165209230), (372080547, 165257170), (371966823, 165307695),
(371955753, 165312615), (371903169, 165335989), (371826220, 165370205),
(371739304, 165408870), (371594008, 165473546), (370940177, 165765215),
(370851481, 165804861), (370776189, 165838530), (370711299, 165867559),
(370666240, 165887722), (370662111, 165889570), (370577311, 165927531),
(370539841, 165944310), (369827913, 166263757), (369827154, 166264098),
(369734876, 166305594), (369484286, 166418385), (369344621, 166481315),
(369148786, 166569634), (369079273, 166601006), (368912329, 166676398),
(368651233, 166794446), (368300168, 166953435), (368274845, 166964915),
(368248101, 166977041), (368005911, 167086931), (367998777, 167090170),
(367803759, 167178765), (367793283, 167183527), (367608741, 167267454),
(367322813, 167397657), (366961922, 167562285), (366764490, 167652485),
(366611266, 167722555), (366405709, 167816649), (366253501, 167886390),
(366184534, 167918010), (366120447, 167947403), (365664747, 168156703),
(365553602, 168207830), (365357465, 168298130), (364836983, 168538227),
(364770694, 168568855), (364726090, 168589470), (364655436, 168622135),
(363988524, 168931090), (363829957, 169004715), (363739175, 169046895),
(363687753, 169070797), (363676929, 169075829), (363632725, 169096382),
(363526971, 169145574), (362796788, 169486005), (362775683, 169495865),
(362694923, 169533606), (362585668, 169584690), (362467360, 169640042),
(362412817, 169665573), (362065957, 169828113), (361868177, 169920933),
(361294557, 170190713), (361260471, 170206771), (361226523, 170222767),
(361157954, 170255085), (361136391, 170265251), (360955738, 170350466),
(360529174, 170552018), (360058939, 170774758), (359700371, 170944995),
(359698053, 170946097), (359625026, 170980810), (359509650, 171035682),
(359506396, 171037230), (359453039, 171062619), (359243865, 171162222),
(358877082, 171337155), (358608058, 171465690), (358586943, 171475787),
(358557361, 171489934), (358354255, 171587130), (358124713, 171697110),
(357735978, 171883685), (357583902, 171956785), (357557027, 171969710),
(357500315, 171996990), (357467810, 172012630), (357193749, 172144609),
(357105634, 172187085), (357038389, 172219515), (356958443, 172258086),
(356662575, 172400982), (356385161, 172535181), (356244088, 172603505),
(356120005, 172663645), (355973164, 172734870), (355920331, 172760511),
(355853309, 172793049), (355629070, 172902002), (355199844, 173110938),
(355059240, 173179490), (354755289, 173327869), (354655485, 173376645),
(354550317, 173428073), (354106483, 173645446), (353747713, 173821557),
(353475922, 173955210), (353286323, 174048567), (353129076, 174126070),
(352908232, 174235035), (352689546, 174343070), (352593829, 174390398),
(352537905, 174418062), (352111150, 174629455), (351979075, 174694982),
(351885606, 174741385), (351860509, 174753849), (351786805, 174790462),
(351753616, 174806954), (351554364, 174906030), (351169928, 175097505),
(350978100, 175193205), (350889357, 175237513), (350882555, 175240910),
(350626321, 175368974), (350510660, 175426842), (350300536, 175532070),
(350271077, 175546833), (350218079, 175573398), (349893926, 175736055),
(349862112, 175752035), (349631636, 175867890), (349512163, 175928007),
(349363583, 176002827), (349218455, 176075970), (349153889, 176108530),
(349133813, 176118657), (348321873, 176529190), (347981133, 176702046),
(347933339, 176726319), (347793913, 176797166), (347708117, 176840790),
(347648614, 176871058), (347040057, 177181213), (346939383, 177232627),
(346925579, 177239679), (346823607, 177291790), (346821074, 177293085),
(346794441, 177306701), (346748426, 177330230), (346572303, 177420347),
(346554006, 177429714), (346308734, 177555378), (345955157, 177736845),
(345793948, 177819706), (345608413, 177915166), (345502781, 177969561),
(345419623, 178012406), (345387485, 178028970), (345287290, 178080630),
(345037099, 178209759), (345011166, 178223154), (344538867, 178467465),
(344490159, 178492699), (344404203, 178537247), (344318174, 178581855),
(344256920, 178613630), (344231920, 178626602), (344074484, 178708335),
(343989155, 178752665), (343624567, 178942323), (343540493, 178986115),
(343166187, 179181343), (343114264, 179208458), (342967911, 179284931),
(342845067, 179349170), (342766631, 179390211), (342734293, 179407137),
(342663379, 179444265), (342154012, 179711405), (342073473, 179753717),
(342011069, 179786515), (341969499, 179808370), (341928614, 179829870),
(341635903, 179983947), (341594378, 180005826), (341532062, 180038670),
(340873560, 180386470), (340841400, 180403490), (340655214, 180502090),
(340608426, 180526885), (340496070, 180586455), (340314474, 180682818),
(340185835, 180751142), (340073618, 180810786), (339968986, 180866434),
(339756373, 180979617), (339621882, 181051285), (339545836, 181091834),
(339390543, 181174695), (339370800, 181185235), (339365897, 181187853),
(339220769, 181265370), (339136128, 181310610), (339088183, 181336246),
(339000519, 181383139), (338777198, 181502706), (338678921, 181555374),
(338494611, 181654231), (338353197, 181730153), (338255043, 181782887),
(338038815, 181899165), (337857441, 181996815), (337700005, 182081662),
(337668271, 182098774), (337355218, 182267755), (336882731, 182523390),
(336854401, 182538741), (336755390, 182592410), (336493896, 182734305),
(336491727, 182735483), (336241651, 182871390), (336055010, 182972955),
(335780006, 183122810), (335733887, 183147965), (335550491, 183248065),
(335518834, 183265355), (335472055, 183290910), (335424628, 183316826),
(335340934, 183362578), (335019892, 183538290), (334653537, 183739215),
(334544343, 183799187), (334405371, 183875570), (334263213, 183953770),
(334148991, 184016651), (334007488, 184094610), (333928866, 184137954),
(333898504, 184154698), (333589456, 184325305), (333310999, 184479295),
(333010778, 184645610), (332957729, 184675029), (332914173, 184699190),
(332895031, 184709811), (332864763, 184726607), (332685259, 184826278),
(332645484, 184848378), (332321457, 185028613), (331920465, 185252145),
(331795964, 185321658), (331727314, 185360010), (331569173, 185448417),
(331535647, 185467170), (331486441, 185494701), (331251833, 185626077),
(330898659, 185824199), (330692277, 185940170), (330514899, 186039959),
(330435215, 186084822), (330401379, 186103879), (329845840, 186417322),
(329513338, 186605430), (329415625, 186660782), (329353594, 186695938),
(329322951, 186713310), (329183309, 186792515), (329087574, 186846855),
(328913084, 186945978), (328513803, 187173195), (328334351, 187275495),
(328303375, 187293165), (328244970, 187326490), (328206021, 187348721),
(328196253, 187354297), (328060925, 187431582), (328005268, 187463386),
(327700501, 187637730), (327561865, 187717145), (327290363, 187872865),
(327211457, 187918170), (327155461, 187950334), (327074757, 187996710),
(326898785, 188097910), (326823997, 188140953), (326794281, 188158061),
(326742449, 188187909), (326717891, 188202054), (326579001, 188282094),
(326015547, 188607503), (325948092, 188646535), (325803995, 188729970),
(325567921, 188866821), (325395147, 188967103), (325355596, 188990074),
(325018976, 189185810), (324970737, 189213893), (324939411, 189232134),
(324810786, 189307070), (324607652, 189425535), (324472040, 189504705),
(324312901, 189597694), (324195683, 189666246), (323953751, 189807891),
(323484661, 190083134), (323392864, 190137090), (323362354, 190155030),
(323233053, 190231097), (323141327, 190285095), (322673414, 190561030),
(322534679, 190642998), (322316079, 190772295), (322157998, 190865906),
(322113851, 190892065), (322023409, 190945678), (321817138, 191068066),
(321769270, 191096490), (321615877, 191187633), (321376590, 191329985),
(321283125, 191385645), (321244075, 191408910), (321026433, 191538677),
(320840949, 191649409), (320382056, 191923914), (320079559, 192105295),
(319943491, 192186995), (319868703, 192231930), (319839620, 192249410),
(319766447, 192293403), (319594877, 192396633), (319497735, 192455130),
(318984141, 192765001), (318851633, 192845110), (318677459, 192950510),
(318672854, 192953298), (318633689, 192977015), (318455033, 193085277),
(318368341, 193137854), (318194431, 193243414), (317808162, 193478285),
(317639653, 193580926), (317471323, 193683567), (317412627, 193719383),
(317382681, 193737661), (317304387, 193785465), (317256377, 193814790),
(317233338, 193828866), (317211526, 193842194), (316909447, 194026965),
(316656249, 194182109), (316482304, 194288835), (316418875, 194327782),
(316314498, 194391906), (316194931, 194465414), (316098289, 194524869),
(316068467, 194543223), (315901138, 194646270), (315294189, 195020969),
(315262308, 195040690), (315186671, 195087495), (315148362, 195111210),
(315093207, 195145363), (315033873, 195182117), (315029235, 195184990),
(314548642, 195483210), (314138379, 195738510), (314093968, 195766186),
(313988623, 195831867), (313897537, 195888693), (313872457, 195904345),
(313637171, 196051310), (313614801, 196065294), (313565417, 196096173),
(313062986, 196410885), (313034521, 196428745), (312984872, 196459905),
(312960837, 196474993), (312931311, 196493531), (312866563, 196534195),
(312828306, 196558230), (312522516, 196750554), (312458617, 196790790),
(312356665, 196855022), (312067555, 197037395), (311890519, 197149238),
(311833622, 197185210), (311638604, 197308605), (311594547, 197336503),
(311521710, 197382642), (311389617, 197466373), (311351540, 197490522),
(311184485, 197596542), (310881363, 197789207), (310787716, 197848805),
(310650321, 197936310), (310648318, 197937586), (310506242, 198028155),
(310483693, 198042537), (310100219, 198287439), (309855819, 198443839),
(309855183, 198444246), (309686559, 198552299), (309567915, 198628395),
(309232805, 198843645), (309228580, 198846362), (309116814, 198918258),
(309088708, 198936346), (308644135, 199222895), (308554600, 199280705),
(308351336, 199412070), (308305571, 199441671), (308211861, 199502310),
(308151129, 199541629), (307856117, 199732845), (307787184, 199777578),
(307665348, 199856690), (307588581, 199906570), (307454583, 199993695),
(307378336, 200043305), (307276941, 200109315), (307160790, 200184985),
(306996973, 200291806), (306964039, 200313295), (306895704, 200357898),
(306892285, 200360130), (306803258, 200418270), (306801280, 200419562),
(306656999, 200513859), (306428842, 200663155), (306257029, 200775729),
(305710779, 201134479), (305674229, 201158529), (305637075, 201182982),
(305581318, 201219690), (305509388, 201267066), (305254551, 201435091),
(304963358, 201627430), (304893589, 201673569), (304784382, 201745830),
(304753663, 201766166), (304665256, 201824714), (304563539, 201892119),
(304004883, 202263127), (303975578, 202282626), (303901205, 202332130),
(303879530, 202346562), (303855251, 202362730), (303665223, 202489365),
(303643171, 202504071), (303437588, 202641270), (303394690, 202669922),
(302979361, 202947745), (302737071, 203110171), (302649249, 203169109),
(302548253, 203236930), (302500267, 203269170), (302313069, 203395038),
(302293500, 203408205), (302152636, 203503034), (301701718, 203807186),
(301421391, 203996730), (301396043, 204013887), (301332312, 204057035),
(301307454, 204073870), (301295465, 204081990), (301208062, 204141210),
(301163357, 204171513), (301044143, 204252365), (300680798, 204499185),
(300629343, 204534187), (300555182, 204584655), (300437709, 204664649),
(300434742, 204666670), (300362662, 204715785), (299684260, 205179205),
(299527291, 205286730), (299384501, 205384641), (299363673, 205398930),
(299312443, 205434086), (299204805, 205507990), (299077611, 205595390),
(298934581, 205693761), (298474776, 206010635), (298429616, 206041810),
(298404519, 206059139), (298269543, 206152387), (298113315, 206260422),
(297986585, 206348142), (297909547, 206401503), (297828448, 206457706),
(297665758, 206570546), (297365695, 206778990), (297143785, 206933415),
(297081543, 206976770), (296981469, 207046515), (296906379, 207098879),
(296870073, 207124206), (296766671, 207196374), (296683810, 207254242),
(296463676, 207408135), (296383219, 207464439), (296199559, 207593078),
(296161786, 207619555), (296064091, 207688065), (296004754, 207729698),
(295842154, 207843870), (295723857, 207927013), (295676953, 207959997),
(295496646, 208086890), (295282533, 208237777), (294849884, 208543335),
(294827724, 208559010), (294740296, 208620874), (294712489, 208640558),
(294405133, 208858377), (294288594, 208941085), (293965777, 209170533),
(293876425, 209234130), (293649279, 209395979), (293425958, 209555346),
(293402514, 209572090), (293309807, 209638330), (293238005, 209689662),
(293154370, 209749485), (293081669, 209801515), (292838746, 209975555),
(292773175, 210022582), (292718044, 210062138), (292645835, 210113970),
(292531453, 210196126), (292517519, 210206139), (292348507, 210327663),
(291837245, 210696130), (291715323, 210784190), (291698121, 210796621),
(291551760, 210902442), (291532887, 210916095), (291491673, 210945917),
(291273163, 211104166), (290763291, 211474351), (290760659, 211476265),
(290688109, 211529045), (290667377, 211544133), (290608364, 211587090),
(290606491, 211588454), (290579074, 211608418), (290518952, 211652210),
(290452487, 211700643), (290371389, 211759769), (289938430, 212075985),
(289865121, 212129621), (289766265, 212201990), (289706781, 212245561),
(289595792, 212326905), (289378703, 212486190), (289324212, 212526210),
(289169023, 212640267), (289147501, 212656094), (288482794, 213146085),
(288431474, 213184010), (288414889, 213196269), (288327224, 213261090),
(288207130, 213349955), (287744156, 213693230), (287547475, 213839395),
(287474113, 213893966), (287308015, 214017622), (287182853, 214110897),
(287159908, 214128005), (287155759, 214131099), (286657629, 214503198),
(286602099, 214544759), (286514985, 214609990), (286498511, 214622331),
(286418517, 214682273), (286347861, 214735245), (286298859, 214771999),
(286283744, 214783338), (285953311, 215031531), (285866395, 215096910),
(285439781, 215418390), (285346645, 215488702), (285288303, 215532770),
(285128343, 215653686), (285124701, 215656441), (285030647, 215727603),
(285009224, 215743818), (284436752, 216178035), (284396541, 216208601),
(284354239, 216240765), (284337697, 216253345), (284294676, 216286070),
(284211995, 216348990), (284053289, 216469869), (283860969, 216616530),
(283840355, 216632262), (283820839, 216647158), (283534733, 216865770),
(283485111, 216903731), (283450654, 216930098), (283221710, 217105455),
(283168377, 217146345), (283069748, 217222005), (283018235, 217261542),
(282911254, 217343698), (282809000, 217422282), (282648966, 217545385),
(282440004, 217706335), (282342996, 217781135), (282237091, 217862854),
(282009127, 218038965), (281974850, 218065470), (281925501, 218103641),
(281868263, 218147930), (281733463, 218252307), (281621940, 218338735),
(281410829, 218502530), (281195079, 218670179), (281129348, 218721306),
(281071181, 218766570), (281031445, 218797502), (281023081, 218804014),
(280692342, 219061830), (280558531, 219166311), (280466963, 219237865),
(280349791, 219329495), (280342972, 219334830), (280192601, 219452541),
(280043907, 219569063), (279991173, 219610417), (279778239, 219777558),
(279625983, 219897227), (279625409, 219897678), (279599028, 219918426),
(279260567, 220184965), (279218339, 220218265), (279155818, 220267586),
(279059938, 220343266), (279009030, 220383470), (278992987, 220396143),
(278912053, 220460097), (278818978, 220533690), (278736298, 220599106),
(277991213, 221190366), (277973218, 221204685), (277821374, 221325585),
(277801199, 221341659), (277759166, 221375154), (277542919, 221547638),
(277239417, 221790173), (277193884, 221826605), (277167732, 221847535),
(277089910, 221909842), (276871233, 222085110), (276755563, 222177930),
(276452922, 222421155), (276432347, 222437710), (276232047, 222599003),
(276024976, 222765994), (275919229, 222851370), (275852353, 222905397),
(275802232, 222945905), (275768507, 222973170), (275698780, 223029562),
(275620544, 223092870), (275210835, 223424990), (275147873, 223476117),
(275090943, 223522365), (275064990, 223543455), (275043867, 223560623),
(275016056, 223583230), (275007372, 223590290), (275000243, 223596087),
(274975239, 223616419), (274916656, 223664070), (274319424, 224151018),
(274173174, 224270585), (274103224, 224327818), (274035607, 224383170),
(274019447, 224396403), (273904969, 224490189), (273825511, 224555331),
(273254963, 225024195), (273148161, 225112181), (273122493, 225133337),
(273031350, 225208490), (273029356, 225210135), (272968221, 225260574),
(272741969, 225447438), (272674330, 225503362), (272595229, 225568798),
(272529829, 225622929), (272481346, 225663074), (272074708, 226000346),
(272004369, 226058789), (271934038, 226117255), (271911605, 226135910),
(271854952, 226183035), (271821909, 226210530), (271637751, 226363891),
(271623410, 226375842), (271299651, 226645991), (271232725, 226701915),
(271207136, 226723305), (271126713, 226790557), (271071668, 226836610),
(270709110, 227140410), (270658133, 227183190), (270512957, 227305113),
(270347996, 227443810), (270305116, 227479890), (270048607, 227695965),
(269871001, 227845815), (269756277, 227942715), (269630575, 228048982),
(269613121, 228063745), (269461951, 228191691), (269355286, 228282055),
(269261467, 228361595), (269210764, 228404605), (268947413, 228628257),
(268927396, 228645274), (268812687, 228742843), (268772014, 228777458),
(268629581, 228898761), (268428209, 229070478), (268321953, 229161190),
(268154147, 229304595), (268138548, 229317935), (267998103, 229438110),
(267955901, 229474245), (267939903, 229487947), (267813825, 229595982),
(267805870, 229602802), (267739048, 229660106), (267467783, 229893027),
(267160387, 230157543), (267018609, 230279749), (267000033, 230295770),
(266872749, 230405609), (266732966, 230526354), (266729559, 230529299),
(266619576, 230624394), (266271703, 230925695), (266130520, 231048202),
(266064043, 231105930), (265960051, 231196294), (265875738, 231269610),
(265848940, 231292922), (265809397, 231327330), (265771819, 231360038),
(265682681, 231437661), (265528074, 231572418), (265306587, 231765743),
(265218053, 231843110), (265195749, 231862609), (265105307, 231941710),
(264949341, 232078245), (264899450, 232121955), (264840135, 232173942),
(264700874, 232296090), (264553944, 232425105), (264413549, 232548515),
(264301145, 232647415), (264043222, 232874670), (263255292, 233571670),
(263071549, 233734809), (263053461, 233750881), (263050530, 233753485),
(263022011, 233778831), (262974221, 233821315), (262942065, 233849910),
(262856269, 233926238), (262716971, 234050271), (262296015, 234425895),
(262256329, 234461370), (262210431, 234502411), (262185693, 234524537),
(262175639, 234533530), (262115659, 234587199), (262042473, 234652717),
(261585597, 235062553), (261560381, 235085214), (261243756, 235370135),
(261008447, 235582330), (260862101, 235714494), (260722136, 235841034),
(260545430, 236000985), (260468169, 236070989), (260332218, 236194270),
(260153878, 236356185), (260142109, 236366878), (260089361, 236414815),
(260056296, 236444874), (259991803, 236503526), (259878541, 236606601),
(259813697, 236665653), (259404117, 237039330), (259353003, 237086047),
(259285943, 237147365), (259264553, 237166930), (259140563, 237280407),
(258989763, 237418566), (258617249, 237760545), (258593735, 237782165),
(258216913, 238129166), (258117988, 238220430), (258055427, 238278183),
(257976990, 238350630), (257773670, 238538630), (257455298, 238833610),
(257318861, 238960245), (257234901, 239038241), (257213680, 239057962),
(257203446, 239067474), (257128833, 239136846), (257125969, 239139510),
(256928837, 239322993), (256737678, 239501185), (256597434, 239632085),
(256483996, 239738070), (256419145, 239798702), (256340773, 239872017),
(256162137, 240039293), (256148613, 240051966), (255967325, 240221982),
(255828027, 240352783), (255803366, 240375954), (255525699, 240637159),
(255453187, 240705465), (255397876, 240757594), (255357368, 240795786),
(255334150, 240817682), (255310156, 240840314), (255286069, 240863038),
(255174857, 240968013), (255027421, 241107321), (254884882, 241242155),
(254581427, 241529710), (254496041, 241610745), (254460063, 241644907),
(254422214, 241680855), (254368920, 241731490), (254315923, 241781865),
(253688971, 242379390), (253644573, 242421817), (253613743, 242451286),
(253606195, 242458502), (253578989, 242484515), (253471799, 242587059),
(253446169, 242611590), (253325347, 242727303), (253307723, 242744190),
(253272932, 242777535), (252906189, 243129590), (252882329, 243152530),
(252709477, 243318845), (252626116, 243399135), (252482801, 243537294),
(252436741, 243581730), (252235054, 243776498), (252077309, 243929049),
(251977525, 244025645), (251921104, 244080298), (251788637, 244208710),
(251701121, 244293621), (251655203, 244338195), (251617127, 244375170),
(251595967, 244395723), (251110260, 244868442), (251010860, 244965410),
(250870119, 245102838), (250853880, 245118705), (250839287, 245132965),
(250835663, 245136507), (250775290, 245195522), (250698643, 245270487),
(250630396, 245337274), (250465561, 245498734), (250191669, 245767489),
(250035624, 245920870), (250014597, 245941553), (249981423, 245974190),
(249924233, 246030477), (249901509, 246052849), (249854451, 246099191),
(249736883, 246215046), (249469612, 246478830), (249395635, 246551942),
(249144231, 246800730), (249092884, 246851605), (249000280, 246943410),
(248906157, 247036790), (248831583, 247110827), (248801338, 247140866),
(248728980, 247212762), (248388485, 247551645), (248229381, 247710315),
(248210319, 247729339), (248185221, 247754390), (248135550, 247803985),
(248125677, 247813845), (248053698, 247885755), (248003983, 247935446),
(248001738, 247937690), (247992181, 247947245), (247731148, 248208506),
(247729339, 248210319), (247623399, 248316510), (247361446, 248579474),
(247300426, 248640810), (247110827, 248831583), (247108074, 248834355),
(246801488, 249143466), (246566119, 249381295), (246299209, 249651545),
(246099191, 249854451), (246052849, 249901509), (246030477, 249924233),
(245978060, 249977490), (245941553, 250014597), (245897800, 250059082),
(245823728, 250134430), (245767489, 250191669), (245332518, 250635255),
(245270487, 250698643), (245250253, 250719326), (245240495, 250729302),
(245189753, 250781190), (245136507, 250835663), (244662670, 251321455),
(244655388, 251328935), (244554508, 251432610), (244395723, 251595967),
(244293621, 251701121), (244234724, 251761818), (244032288, 251970666),
(243929049, 252077309), (243702401, 252311745), (243610282, 252407155),
(243571643, 252447195), (243553337, 252466170), (243481114, 252541058),
(243458143, 252564886), (243435265, 252588622), (243325153, 252702926),
(243309402, 252719285), (243029771, 253010065), (242727303, 253325347),
(242659016, 253396635), (242587059, 253471799), (242537808, 253523270),
(242421817, 253644573), (242300549, 253771518), (242240091, 253834854),
(241910268, 254180935), (241851946, 254242230), (241810558, 254285746),
(241644907, 254460063), (241571458, 254537430), (241525969, 254585370),
(241143111, 254989570), (241107321, 255027421), (241082942, 255053210),
(240968013, 255174857), (240918155, 255227665), (240637159, 255525699),
(240619249, 255544718), (240593436, 255572135), (240537196, 255631890),
(240352783, 255828027), (240293976, 255890635), (240172608, 256019946),
(240077537, 256121330), (240039293, 256162137), (239936641, 256271730),
(239914005, 256295910), (239872017, 256340773), (239842861, 256371934),
(239750017, 256471215), (239622896, 256607274), (239322993, 256928837),
(239299923, 256953606), (239038241, 257234901), (238987696, 257289305),
(238860979, 257425798), (238816000, 257474282), (238371351, 257954565),
(238311873, 258018945), (238278183, 258055427), (238192836, 258147890),
(237864841, 258503854), (237829461, 258542310), (237795838, 258578866),
(237556127, 258839790), (237318199, 259099295), (237300363, 259118770),
(237280407, 259140563), (237219054, 259207585), (237199485, 259228970),
(237086047, 259353003), (236948081, 259504014), (236706160, 259769235),
(236665653, 259813697), (236606601, 259878541), (236468914, 260029858),
(236249198, 260271690), (236208769, 260316238), (236150500, 260380470),
(236070989, 260468169), (235953517, 260597845), (235798080, 260769630),
(235544208, 261050690), (235540805, 261054462), (235419384, 261189105),
(235366670, 261247602), (235285830, 261337362), (235126364, 261514605),
(235062553, 261585597), (234887663, 261780365), (234762391, 261920054),
(234684950, 262006482), (234652717, 262042473), (234596239, 262105558),
(234587199, 262115659), (234524537, 262185693), (234502411, 262210431),
(234460693, 262257086), (234050271, 262716971), (233921703, 262861365),
(233904293, 262880930), (233778831, 263022011), (233750881, 263053461),
(233734809, 263071549), (233722469, 263085438), (233624826, 263195394),
(233559595, 263268902), (233070410, 263821470), (232935745, 263973990),
(232847696, 264073810), (232769259, 264162795), (232717139, 264221958),
(232698546, 264243070), (232681949, 264261918), (232625019, 264326590),
(232214582, 264793785), (232156411, 264860134), (232126805, 264893915),
(232098421, 264926310), (232040508, 264992430), (232007704, 265029898),
(231992686, 265047055), (231876283, 265180110), (231862609, 265195749),
(231765743, 265306587), (231690100, 265393205), (231437661, 265682681),
(231402643, 265722886), (231360429, 265771370), (231215738, 265937685),
(231165617, 265995345), (230994903, 266191926), (230973110, 266217042),
(230658628, 266580005), (230529299, 266729559), (230481010, 266785442),
(230411582, 266865830), (230405609, 266872749), (230335576, 266953890),
(230279749, 267018609), (230157543, 267160387), (229893027, 267467783),
(229835193, 267535086), (229744214, 267641030), (229712659, 267677795),
(229504613, 267920445), (229487947, 267939903), (229427656, 268010314),
(228898761, 268629581), (228776797, 268772790), (228755996, 268797230),
(228742843, 268812687), (228719714, 268839870), (228706409, 268855510),
(228628257, 268947413), (228563378, 269023755), (228477645, 269124702),
(228456871, 269149174), (228210882, 269439290), (228191691, 269461951),
(228054894, 269623585), (227979666, 269712555), (227893489, 269814545),
(227836626, 269881885), (227808766, 269914890), (227751166, 269983154),
(227626756, 270130714), (227305113, 270512957), (227249040, 270579705),
(227227600, 270605235), (227180003, 270661930), (227114100, 270740470),
(227103476, 270753135), (226886464, 271012105), (226790557, 271126713),
(226767625, 271154130), (226645991, 271299651), (226611698, 271340706),
(226363891, 271637751), (226309408, 271703146), (226263137, 271758710),
(226058789, 272004369), (225622929, 272529829), (225187363, 273056966),
(225133337, 273122493), (225131113, 273125190), (225112181, 273148161),
(224791139, 273538265), (224677601, 273676494), (224622630, 273743470),
(224588664, 273784870), (224555331, 273825511), (224503593, 273888615),
(224490189, 273904969), (224462738, 273938466), (224396403, 274019447),
(224384556, 274033914), (224377891, 274042054), (224342303, 274085526),
(223927204, 274593605), (223853337, 274684215), (223843210, 274696642),
(223616419, 274975239), (223596087, 275000243), (223560623, 275043867),
(223476117, 275147873), (223448790, 275181522), (222936914, 275813355),
(222918523, 275836110), (222905397, 275852353), (222842142, 275930655),
(222738301, 276059294), (222599003, 276232047), (222510888, 276341435),
(222346386, 276545885), (222229926, 276690810), (222007185, 276968415),
(221942782, 277048785), (221896292, 277106830), (221893086, 277110834),
(221840925, 277175990), (221790173, 277239417), (221341659, 277801199),
(221323399, 277824118), (221268802, 277892670), (221247926, 277918890),
(221230936, 277940234), (220565244, 278779090), (220461518, 278910255),
(220460097, 278912053), (220396143, 278992987), (220393687, 278996095),
(220344624, 279058218), (220250954, 279176898), (220120246, 279342674),
(219897227, 279625983), (219843425, 279694415), (219792036, 279759810),
(219760963, 279799366), (219728275, 279840990), (219706129, 279869198),
(219610417, 279991173), (219569063, 280043907), (219495791, 280137390),
(219452541, 280192601), (219208775, 280504182), (219166311, 280558531),
(219145184, 280585578), (218902189, 280897045), (218829980, 280989735),
(218670179, 281195079), (218595604, 281291010), (218491234, 281425378),
(218252307, 281733463), (218116182, 281909290), (218103641, 281925501),
(217932523, 282146865), (217830970, 282278402), (217703130, 282444162),
(217616954, 282556010), (217447690, 282775955), (217338585, 282917910),
(217239574, 283046855), (217213010, 283081470), (217120906, 283201555),
(217070153, 283267770), (217039465, 283307822), (216903731, 283485111),
(216741134, 283697778), (216679317, 283778715), (216540524, 283960605),
(216469869, 284053289), (216343900, 284218682), (216208601, 284396541),
(216142884, 284483010), (216105895, 284531702), (216071619, 284576838),
(215783389, 284956958), (215727603, 285030647), (215705790, 285059470),
(215671823, 285104365), (215656441, 285124701), (215546319, 285270370),
(215494779, 285338598), (215115609, 285841545), (215031531, 285953311),
(214900003, 286128326), (214771999, 286298859), (214700328, 286394430),
(214682273, 286418517), (214659899, 286448370), (214622331, 286498511),
(214596244, 286533338), (214544759, 286602099), (214379920, 286822470),
(214175066, 287096810), (214131099, 287155759), (214110897, 287182853),
(213997545, 287334970), (213948065, 287401422), (213831195, 287558502),
(213831096, 287558635), (213717718, 287711186), (213552198, 287934185),
(213511985, 287988415), (213398776, 288141194), (213226413, 288374115),
(213196269, 288414889), (213164011, 288458534), (213119906, 288518230),
(213111427, 288529710), (212640267, 289169023), (212567755, 289267665),
(212550219, 289291530), (212480866, 289385954), (212451639, 289425765),
(212404068, 289490586), (212248627, 289702595), (212245561, 289706781),
(212129621, 289865121), (211971793, 290080945), (211759769, 290371389),
(211708801, 290441294), (211700643, 290452487), (211544133, 290667377),
(211522743, 290696770), (211474351, 290763291), (211315824, 290981418),
(211116305, 291256415), (211069033, 291321646), (210977230, 291448410),
(210945917, 291491673), (210814349, 291673590), (210796621, 291698121),
(210591231, 291982614), (210327663, 292348507), (210306396, 292378070),
(210206139, 292517519), (210174872, 292561035), (210162646, 292578055),
(210130847, 292622330), (210019490, 292777485), (209981271, 292830774),
(209901898, 292941506), (209849524, 293014618), (209707297, 293213345),
(209618149, 293338045), (209569150, 293406630), (209507005, 293493662),
(209480287, 293531095), (209395979, 293649279), (209254206, 293848230),
(209170533, 293965777), (209091447, 294076965), (209032739, 294159558),
(208858377, 294405133), (208788680, 294503410), (208760003, 294543865),
(208536682, 294859290), (208455175, 294974582), (208368088, 295097866),
(208237777, 295282533), (208155347, 295399465), (207959997, 295676953),
(207932403, 295716190), (207927013, 295723857), (207889081, 295777815),
(207863813, 295813770), (207785240, 295925630), (207577403, 296221926),
(207468253, 296377770), (207464439, 296383219), (207301668, 296615935),
(207098879, 296906379), (207044470, 296984402), (207022259, 297016265),
(207006699, 297038590), (206973867, 297085710), (206779625, 297364782),
(206660151, 297536694), (206401503, 297909547), (206174740, 298237205),
(206152387, 298269543), (206089726, 298360230), (206083593, 298369110),
(206059139, 298404519), (206022481, 298457614), (205693761, 298934581),
(205659978, 298983685), (205640575, 299011895), (205531540, 299170522),
(205471766, 299257554), (205384641, 299384501), (205249341, 299581854),
(205110232, 299785035), (205059054, 299859855), (204981541, 299973245),
(204956627, 300009710), (204792724, 300249818), (204714266, 300364890),
(204664649, 300437709), (204643954, 300468090), (204534187, 300629343),
(204492661, 300690390), (204188684, 301138030), (204171513, 301163357),
(204044171, 301351310), (204013887, 301396043), (203885558, 301585746),
(203879490, 301594722), (203853823, 301632695), (203777359, 301745878),
(203619538, 301979755), (203316740, 302429490), (203308905, 302441145),
(203266319, 302504510), (203207352, 302592290), (203199267, 302604330),
(203169109, 302649249), (203110171, 302737071), (203008568, 302888586),
(202757835, 303263142), (202600803, 303498195), (202598035, 303502342),
(202570167, 303544095), (202524809, 303612078), (202504071, 303643171),
(202487365, 303668222), (202418316, 303771810), (202263127, 304004883),
(202112640, 304231235), (201892119, 304563539), (201861880, 304609162),
(201698835, 304855395), (201673569, 304893589), (201591890, 305017122),
(201435091, 305254551), (201158529, 305674229), (201134479, 305710779),
(201027997, 305872710), (201009031, 305901570), (201007735, 305903542),
(200871636, 306110805), (200775729, 306257029), (200765129, 306273198),
(200548957, 306603330), (200513859, 306656999), (200494530, 306686562),
(200357319, 306896590), (200289828, 307000005), (200244980, 307068762),
(200089081, 307308014), (199774637, 307791715), (199737018, 307849685),
(199587290, 308080630), (199541629, 308151129), (199521452, 308182290),
(199469870, 308261985), (199441671, 308305571), (199385074, 308393085),
(199292164, 308536858), (199156413, 308747166), (199077578, 308869430),
(198953077, 309062715), (198941503, 309080695), (198891864, 309157835),
(198837302, 309242670), (198772423, 309343606), (198751099, 309376795),
(198645100, 309541882), (198552299, 309686559), (198443839, 309855819),
(198287439, 310100219), (198261129, 310141370), (198054362, 310465155),
(198042537, 310483693), (197789207, 310881363), (197765166, 310919154),
(197682545, 311049102), (197466373, 311389617), (197451676, 311412794),
(197347850, 311576630), (197336503, 311594547), (197213424, 311789010),
(196997764, 312130335), (196836555, 312385970), (196692814, 312614258),
(196627931, 312717414), (196579168, 312794986), (196493531, 312931311),
(196474993, 312960837), (196440040, 313016522), (196390971, 313094730),
(196134820, 313503630), (196096173, 313565417), (196094398, 313568255),
(196045469, 313646515), (196030734, 313670090), (195947400, 313803490),
(195888693, 313897537), (195831867, 313988623), (195739719, 314136438),
(195601676, 314358135), (195539871, 314457495), (195340752, 314778035),
(195237178, 314945026), (195182117, 315033873), (195162381, 315065730),
(195145363, 315093207), (195022393, 315291886), (195020969, 315294189),
(194963646, 315386890), (194558163, 316044195), (194543223, 316068467),
(194524869, 316098289), (194517410, 316110410), (194476882, 316176285),
(194460839, 316202370), (194372250, 316346485), (194182109, 316656249),
(193934149, 317061118), (193877890, 317153122), (193737661, 317382681),
(193719383, 317412627), (193683567, 317471323), (193679301, 317478315),
(193520807, 317738330), (193439004, 317872698), (193327238, 318056466),
(193177510, 318302985), (193105711, 318421334), (193085277, 318455033),
(193075083, 318471846), (193069348, 318481306), (192969526, 318646055),
(192765001, 318984141), (192396633, 319594877), (192293403, 319766447),
(192287649, 319776015), (192278950, 319790482), (192229233, 319873190),
(192215523, 319896006), (191859868, 320489005), (191829437, 320539845),
(191813612, 320566290), (191756926, 320661055), (191733478, 320700270),
(191677857, 320793330), (191658538, 320825666), (191649409, 320840949),
(191538677, 321026433), (191427216, 321213354), (191203712, 321588830),
(191187633, 321615877), (191073019, 321808795), (191009990, 321914985),
(190770880, 322318470), (190714309, 322414078), (190482793, 322805945),
(190340003, 323048110), (190231097, 323233053), (190192202, 323299155),
(190045745, 323548302), (189911241, 323777454), (189863855, 323858262),
(189807891, 323953751), (189788699, 323986510), (189658973, 324208115),
(189641080, 324238705), (189529784, 324429105), (189527194, 324433538),
(189441466, 324580354), (189423664, 324610858), (189405793, 324641486),
(189359069, 324721590), (189213893, 324970737), (189072053, 325214526),
(188967103, 325395147), (188866821, 325567921), (188623365, 325988130),
(188607503, 326015547), (188393173, 326386445), (188338522, 326481155),
(188187909, 326742449), (188168880, 326775490), (188158061, 326794281),
(188140953, 326823997), (188139250, 326826955), (188040706, 326998230),
(188039494, 327000338), (187912175, 327221895), (187607219, 327753795),
(187544311, 327863734), (187513509, 327917590), (187354297, 328196253),
(187348721, 328206021), (187325949, 328245918), (187291776, 328305810),
(187227448, 328418610), (187012270, 328796490), (186913026, 328971070),
(186810924, 329150870), (186710691, 329327570), (186606003, 329512326),
(186434605, 329815262), (186290215, 330070895), (186156379, 330308198),
(186103879, 330401379), (186060131, 330479065), (186039959, 330514899),
(186006020, 330575205), (185983411, 330615390), (185977876, 330625230),
(185951584, 330671978), (185913110, 330740410), (185824199, 330898659),
(185626077, 331251833), (185494701, 331486441), (185470088, 331530430),
(185448417, 331569173), (185425740, 331609722), (185355649, 331735118),
(185288655, 331855062), (185028613, 332321457), (184983342, 332402785),
(184913956, 332527514), (184742143, 332836770), (184726607, 332864763),
(184709811, 332895031), (184675029, 332957729), (184672310, 332962630),
(184288231, 333656565), (184150084, 333906870), (184137422, 333929830),
(184124050, 333954082), (184016651, 334148991), (184002955, 334173862),
(183994199, 334189765), (183901879, 334357530), (183896641, 334367054),
(183799187, 334544343), (183754217, 334626215), (183661406, 334795314),
(183480961, 335124570), (183473890, 335137485), (183404537, 335264215),
(183382245, 335304970), (183344037, 335374845), (183338248, 335385435),
(183305633, 335445110), (183202854, 335633298), (183060223, 335894806),
(182936153, 336122615), (182832373, 336313406), (182738123, 336486865),
(182735483, 336491727), (182538741, 336854401), (182418491, 337076454),
(182385347, 337137710), (182327718, 337244270), (182185902, 337506785),
(182020900, 337812735), (181914978, 338009430), (181869587, 338093790),
(181843876, 338141594), (181838464, 338151658), (181782887, 338255043),
(181730153, 338353197), (181654231, 338494611), (181398394, 338972010),
(181387841, 338991730), (181383139, 339000519), (181274403, 339203865),
(181206408, 339331146), (181187853, 339365897), (181032978, 339656226),
(180979617, 339756373), (180934088, 339841866), (180837625, 340023145),
(180714445, 340254915), (180698014, 340285855), (180647278, 340381426),
(180630235, 340413542), (180613261, 340445534), (180578977, 340510170),
(180568195, 340530502), (180231997, 341165715), (179983947, 341635903),
(179850185, 341889990), (179849026, 341892194), (179753717, 342073473),
(179726519, 342125238), (179630700, 342307735), (179438541, 342674310),
(179407137, 342734293), (179390211, 342766631), (179360748, 342822935),
(179293471, 342951574), (179284931, 342967911), (179181343, 343166187),
(178942323, 343624567), (178881302, 343741785), (178867989, 343767370),
(178791951, 343913570), (178745728, 344002505), (178596874, 344289218),
(178552817, 344374170), (178537247, 344404203), (178519194, 344439030),
(178492699, 344490159), (178209759, 345037099), (178192580, 345070362),
(178122044, 345207010), (178060002, 345327290), (178000022, 345443655),
(177969561, 345502781), (177960165, 345521022), (177926654, 345586098),
(177829931, 345774065), (177420347, 346572303), (177406171, 346599995),
(177377644, 346655738), (177327742, 346753290), (177306701, 346794441),
(177275158, 346856146), (177239679, 346925579), (177232627, 346939383),
(177181213, 347040057), (176873856, 347643114), (176812035, 347764665),
(176736871, 347912565), (176726319, 347933339), (176643161, 348097134),
(176643079, 348097295), (176454116, 348470070), (176379466, 348617555),
(176118657, 349133813), (176055575, 349258910), (176002827, 349363583),
(175942803, 349482770), (175930254, 349507698), (175928007, 349512163),
(175584964, 350195010), (175546833, 350271077), (175510511, 350343565),
(175503528, 350357505), (175489050, 350386410), (175444678, 350475026),
(175409104, 350546105), (175237513, 350889357), (175135538, 351093666),
(174946963, 351472110), (174931056, 351504070), (174783759, 351800295),
(174756081, 351856014), (174753849, 351860509), (174681791, 352005654),
(174566906, 352237314), (174400426, 352573555), (174271492, 352834405),
(174048567, 353286323), (174005631, 353373495), (173966669, 353452638),
(173821557, 353747713), (173554812, 354291405), (173520028, 354362426),
(173501413, 354400445), (173469691, 354465254), (173462789, 354479358),
(173428073, 354550317), (173410537, 354586170), (173397220, 354613402),
(173327869, 354755289), (173286151, 354840694), (173048933, 355327115),
(172977578, 355473690), (172843035, 355750395), (172793049, 355853309),
(172760511, 355920331), (172751390, 355939122), (172535181, 356385161),
(172518549, 356419518), (172309711, 356851495), (172293455, 356885165),
(172269433, 356934930), (172245079, 356985398), (172202101, 357074494),
(172159087, 357163710), (172144609, 357193749), (172037242, 357416670),
(171994577, 357505330), (171899106, 357703885), (171849113, 357807945),
(171812283, 357884646), (171770246, 357972230), (171636865, 358250415),
(171583093, 358362686), (171571986, 358385885), (171483955, 358569862),
(171475787, 358586943), (171383315, 358780422), (171367146, 358814274),
(171331689, 358888530), (171077006, 359422810), (171062619, 359453039),
(171036736, 359507434), (171018388, 359546005), (171005534, 359573030),
(170946097, 359698053), (170817951, 359967894), (170431973, 360783115),
(170304213, 361053770), (170265251, 361136391), (170248035, 361172910),
(170222767, 361226523), (170206771, 361260471), (170190713, 361294557),
(169920933, 361868177), (169878186, 361959234), (169828113, 362065957),
(169810941, 362102570), (169720951, 362294565), (169695271, 362349390),
(169685400, 362370470), (169682948, 362375706), (169665573, 362412817),
(169579280, 362597235), (169500259, 362766278), (169247305, 363308462),
(169176598, 363460306), (169127521, 363565774), (169075829, 363676929),
(169070797, 363687753), (169040077, 363753845), (169019407, 363798330),
(168928720, 363993630), (168677609, 364535510), (168604126, 364694385),
(168588219, 364728795), (168538227, 364836983), (168427200, 365077482),
(168335118, 365277185), (168246948, 365468610), (168245863, 365470966),
(168156703, 365664747), (168115560, 365754235), (168027505, 365945910),
(167947403, 366120447), (167866943, 366295930), (167859091, 366313065),
(167816649, 366405709), (167775245, 366496130), (167759417, 366530710),
(167397657, 367322813), (167395792, 367326905), (167347231, 367433495),
(167340573, 367448115), (167326768, 367478430), (167272171, 367598374),
(167183527, 367793283), (167086931, 368005911), (167074495, 368033302),
(166977041, 368248101), (166794728, 368650610), (166690416, 368881305),
(166680719, 368902765), (166655499, 368958590), (166654282, 368961285),
(166478864, 369350058), (166447515, 369419622), (166432381, 369453214),
(166263757, 369827913), (166160728, 370057226), (165960232, 370504290),
(165937438, 370555185), (165927531, 370577311), (165867559, 370711299),
(165804861, 370851481), (165784586, 370896834), (165743220, 370989402),
(165625916, 371252154), (165511411, 371508995), (165456814, 371631585),
(165449329, 371648398), (165335989, 371903169), (165334492, 371906535),
(165257449, 372079918), (165200689, 372207758), (165154099, 372312759),
(165088723, 372460195), (165000145, 372660145), (164907631, 372869211),
(164756163, 373212007), (164591654, 373585030), (164543787, 373693710),
(164411668, 373994005), (164342981, 374150315), (164295306, 374258885),
(164256901, 374346390), (164167175, 374550990), (164151687, 374586330),
(164122959, 374651899), (164103010, 374697442), (164098126, 374708594),
(163931867, 375088623), (163882485, 375201645), (163780932, 375434290),
(163645181, 375745730), (163517897, 376038215), (163500169, 376078989),
(163411998, 376281906), (163397140, 376316122), (163371224, 376375818),
(163007773, 377215006), (162974046, 377293070), (162783960, 377733642),
(162697573, 377934206), (162607263, 378144107), (162485368, 378427786),
(162320743, 378811587), (162307774, 378841855), (162305429, 378847329),
(162303826, 378851070), (162290177, 378882933), (162236020, 379009410),
(162216769, 379054389), (161976875, 379615782), (161929131, 379727711),
(161888727, 379822483), (161774151, 380091491), (161691872, 380284905),
(161677170, 380319485), (161616526, 380462194), (161570663, 380570190),
(161368447, 381047095), (161207039, 381428619), (161177748, 381497935),
(161158039, 381544590), (161056925, 381784130), (160807938, 382375266),
(160762074, 382484355), (160721961, 382579815), (160688295, 382659970),
(160641562, 382771290), (160606677, 382854433), (160513216, 383077354),
(160480669, 383155045), (160420474, 383298818), (160412833, 383317077),
(160296232, 383595905), (160051691, 384181995), (160039779, 384210590),
(159971745, 384373990), (159948003, 384431047), (159895241, 384557901),
(159883223, 384586806), (159797438, 384793266), (159492070, 385530002),
(159409608, 385729435), (159316844, 385954030), (159240653, 386138697),
(159235923, 386150167), (159227516, 386170554), (159210667, 386211423),
(159028233, 386654477), (158936349, 386878009), (158904081, 386956570),
(158795224, 387221835), (158735661, 387367134), (158706313, 387438766),
(158691340, 387475322), (158652193, 387570930), (158576561, 387755781),
(158530559, 387868299), (158454723, 388053930), (158328124, 388364218),
(158241152, 388577670), (158200242, 388678155), (158132990, 388843455),
(158049144, 389049738), (158034233, 389086446), (157842929, 389558015),
(157813206, 389631385), (157647094, 390041938), (157645943, 390044787),
(157630182, 390083785), (157593335, 390174990), (157546603, 390290726),
(157516936, 390364234), (157472513, 390474357), (157269395, 390978665),
(157068219, 391479439), (157029472, 391576035), (156994311, 391663734),
(156948768, 391777386), (156936228, 391808690), (156782708, 392192346),
(156531493, 392821770), (156517260, 392857490), (156508261, 392880081),
(156492436, 392919810), (156480418, 392949986), (156465655, 392987062),
(156433281, 393068390), (156397493, 393158337), (156358707, 393255863),
(156307129, 393385629), (156033777, 394074790), (155936195, 394321395),
(155927124, 394344335), (155888218, 394442755), (155819302, 394617210),
(155797273, 394673006), (155706397, 394903353), (155694808, 394932746),
(155524551, 395365091), (155484337, 395467345), (155459577, 395530333),
(155440681, 395578414), (155393858, 395697610), (155253121, 396056310),
(155241846, 396085074), (155231797, 396110715), (155132364, 396364605),
(155083346, 396489885), (155050109, 396574878), (154927909, 396887678),
(154843279, 397104598), (154833256, 397130305), (154783957, 397256790),
(154770941, 397290201), (154671803, 397544847), (154616402, 397687290),
(154373583, 398312827), (154322067, 398445790), (154277300, 398561410),
(154268429, 398584329), (154240286, 398657055), (154157302, 398871655),
(154152785, 398883342), (154075564, 399083258), (153928058, 399465690),
(153804463, 399786695), (153727291, 399987390), (153689168, 400086610),
(153654007, 400178163), (153638470, 400218630), (153607721, 400298745),
(153580395, 400369970), (153534381, 400489961), (153482019, 400626590),
(153343281, 400989061), (153328499, 401027718), (153214421, 401326310),
(153162809, 401461545), (153136599, 401530259), (153128514, 401551458),
(153104914, 401613355), (153016452, 401845535), (152951771, 402015471),
(152855389, 402268958), (152837114, 402317058), (152627275, 402870182),
(152508561, 403183781), (152503997, 403195845), (152470939, 403283265),
(152446794, 403347138), (152304581, 403723761), (152281769, 403784238),
(152140588, 404158935), (152083079, 404311765), (152002441, 404526254),
(151995208, 404545505), (151834111, 404974731), (151832611, 404978730),
(151821585, 405008142), (151806039, 405049619), (151751171, 405196071),
(151631571, 405515671), (151489680, 405895490), (151453335, 405992895),
(151444293, 406017137), (151409400, 406110705), (151368535, 406220342),
(151324624, 406338218), (151246385, 406548415), (151146750, 406816410),
(151020672, 407156035), (150957580, 407326205), (150872939, 407554719),
(150842091, 407638065), (150797361, 407758981), (150792873, 407771117),
(150698021, 408027774), (150666156, 408114070), (150581678, 408343026),
(150522071, 408504730), (150501397, 408560845), (150419185, 408784145),
(150340399, 408998370), (150314671, 409068374), (150277591, 409169310),
(150218854, 409329298), (150181331, 409431570), (150124909, 409585449),
(149954539, 410050795), (149842130, 410358410), (149790927, 410498683),
(149748420, 410615205), (149725776, 410677305), (149692250, 410769282),
(149628777, 410943533), (149585261, 411063081), (149467290, 411387522),
(149237388, 412021270), (149228807, 412044963), (149202259, 412118278),
(149134771, 412304774), (148954773, 412803006), (148768347, 413320303),
(148682391, 413559251), (148637603, 413683865), (148571892, 413866830),
(148492201, 414088941), (148490734, 414093030), (148453189, 414197758),
(148266496, 414719305), (148231838, 414816270), (148191609, 414928878),
(148110963, 415154807), (148080893, 415239110), (148032045, 415376130),
(147930861, 415660245), (147893950, 415763985), (147861928, 415854026),
(147838476, 415919994), (147659514, 416424085), (147641266, 416475554),
(147631709, 416502515), (147564931, 416690995), (147548933, 416736177),
(147487291, 416910351), (147460493, 416986115), (147424942, 417086670),
(147202566, 417716754), (147144297, 417882170), (147079779, 418065479),
(147043496, 418168635), (146982888, 418341066), (146824639, 418791958),
(146746831, 419014011), (146577185, 419498970), (146540834, 419603030),
(146507309, 419699049), (146470753, 419803797), (146419373, 419951110),
(146415387, 419962543), (146258759, 420412278), (146174253, 420655326),
(145991307, 421182463), (145849060, 421593242), (145766443, 421832190),
(145745836, 421891834), (145660823, 422138067), (145490709, 422631649),
(145453090, 422740955), (145410788, 422863935), (145381645, 422948702),
(145380329, 422952530), (145344054, 423058090), (145333688, 423088266),
(145226243, 423401286), (145220647, 423417603), (145185694, 423519538),
(145077969, 423834015), (144986944, 424100105), (144969215, 424151970),
(144932560, 424259242), (144853390, 424491122), (144797896, 424653810),
(144745293, 424808137), (144692977, 424961733), (144584511, 425280534),
(144382295, 425876165), (144241397, 426292170), (144229267, 426328023),
(144211669, 426380045), (144207444, 426392538), (144103565, 426699910),
(144070597, 426797553), (144023575, 426936895), (143855593, 427435437),
(143803860, 427589205), (143779251, 427662391), (143773737, 427678790),
(143700711, 427896131), (143697546, 427905555), (143591426, 428221794),
(143579954, 428256010), (143577879, 428262198), (143422944, 428724835),
(143301049, 429089518), (143266669, 429192489), (143249255, 429244662),
(143209258, 429364546), (143173930, 429470490), (143149429, 429543998),
(143064163, 429800007), (142976655, 430063062), (142783377, 430645215),
(142669299, 430989559), (142665030, 431002455), (142562350, 431312882),
(142515323, 431455206), (142478479, 431566779), (142288419, 432143239),
(142265851, 432211791), (142251628, 432255005), (142218376, 432356070),
(142198270, 432417202), (142177119, 432481530), (142168848, 432506690),
(142109341, 432687801), (142079937, 432777345), (142026644, 432939738),
(141848889, 433482269), (141742555, 433807462), (141653911, 434078931),
(141642593, 434113615), (141610855, 434210910), (141584188, 434292690),
(141534874, 434444010), (141324483, 435090770), (141222081, 435406261),
(141220002, 435412670), (141171498, 435562270), (141139201, 435661941),
(141037531, 435975995), (141015162, 436045155), (141004563, 436077930),
(140962750, 436207282), (140866731, 436504614), (140810970, 436677470),
(140791630, 436737455), (140714722, 436976155), (140712689, 436982469),
(140701446, 437017385), (140597539, 437340358), (140292789, 438290369),
(140279265, 438332622), (140252091, 438417551), (140250528, 438422435),
(140233481, 438475730), (140204264, 438567105), (140174895, 438658990),
(140096300, 438905082), (140087231, 438933495), (140021953, 439138126),
(139995586, 439220834), (139934599, 439412259), (139899683, 439521927),
(139812991, 439794454), (139671337, 440240493), (139630283, 440369930),
(139609169, 440436530), (139588449, 440501909), (139529109, 440689249),
(139496493, 440792286), (139456026, 440920194), (139192453, 441755115),
(139117565, 441992915), (139059445, 442177645), (138986609, 442409370),
(138970117, 442461873), (138912059, 442646799), (138910687, 442651170),
(138900599, 442683318), (138621602, 443574285), (138619708, 443580346),
(138596942, 443653210), (138583866, 443695070), (138555417, 443786173),
(138523493, 443888445), (138317579, 444549265), (138243365, 444787915),
(138226461, 444842310), (138167849, 445031015), (138116023, 445198006),
(138029647, 445476603), (138004466, 445557885), (137926176, 445810794),
(137901116, 445891810), (137692768, 446566505), (137590761, 446897581),
(137573936, 446952234), (137545471, 447044730), (137532495, 447086910),
(137521933, 447121246), (137500121, 447192174), (137487619, 447232838),
(137348321, 447686421), (137245705, 448021145), (137086587, 448541170),
(137042763, 448684607), (137021027, 448755783), (137016957, 448769113),
(137009723, 448792806), (136969233, 448925477), (136952484, 448980378),
(136912755, 449110662), (136838247, 449355203), (136637751, 450014565),
(136627481, 450048390), (136574080, 450224362), (136561246, 450266674),
(136528483, 450374727), (136514678, 450420270), (136264914, 451245858),
(136125789, 451707045), (136074334, 451877855), (136029447, 452026965),
(136002184, 452117578), (135987594, 452166085), (135967019, 452234510),
(135927476, 452366070), (135851573, 452618817), (135818875, 452727782),
(135818334, 452729585), (135670353, 453223397), (135649825, 453291982),
(135635273, 453340615), (135616362, 453403830), (135603568, 453446610),
(135563356, 453581114), (135510879, 453756765), (135471568, 453888435),
(135256478, 454610226), (135080002, 455204155), (135067308, 455246935),
(135065357, 455253513), (135024303, 455391930), (134991577, 455502333),
(134935500, 455691630), (134878138, 455885430), (134806560, 456127490),
(134730975, 456383382), (134677643, 456564110), (134630733, 456723190),
(134605382, 456809210), (134574587, 456913743), (134562351, 456955291),
(134473706, 457256514), (134406343, 457485686), (134314790, 457797522),
(134169851, 458292065), (134136373, 458406445), (134077073, 458609190),
(134069274, 458635870), (134005157, 458855313), (133977950, 458948490),
(133969951, 458975894), (133767543, 459670387), (133733891, 459786054),
(133580193, 460315086), (133571546, 460344885), (133559401, 460386745),
(133509304, 460559498), (133436374, 460811218), (133392721, 460962021),
(133364779, 461058598), (133135851, 461851390), (133108521, 461946221),
(133095963, 461989807), (133074103, 462065695), (133058193, 462120945),
(132861443, 462805287), (132841340, 462875322), (132718385, 463304145),
(132653293, 463531486), (132597874, 463725218), (132514949, 464015409),
(132474670, 464156490), (132449725, 464243910), (132430067, 464312823),
(132276972, 464850210), (132206774, 465097030), (132174086, 465212055),
(132150572, 465294830), (132130959, 465363899), (132110979, 465434279),
(131938336, 466043305), (131766250, 466651955), (131741437, 466739845),
(131634451, 467119191), (131597697, 467249653), (131565233, 467364945),
(131542719, 467444939), (131535774, 467469618), (131526730, 467501762),
(131525265, 467506970), (131511005, 467557662), (131487110, 467642630),
(131358485, 468100542), (131224370, 468578955), (131202107, 468658465),
(131148007, 468851790), (131128543, 468921387), (131105215, 469004822),
(131092846, 469049074), (131057829, 469174398), (131052779, 469192479),
(131021236, 469305434), (131003241, 469369901), (130960027, 469524783),
(130862184, 469875835), (130792798, 470125106), (130687156, 470505135),
(130668681, 470571661), (130631600, 470705235), (130623801, 470733341),
(130621878, 470740270), (130527231, 471081611), (130272715, 472001970),
(130234084, 472141978), (130158119, 472417539), (130142238, 472475185),
(130076939, 472712370), (130044680, 472829630), (130014929, 472937829),
(129975764, 473080335), (129939270, 473213202), (129906848, 473331306),
(129752007, 473896163), (129725160, 473994235), (129678273, 474165615),
(129676501, 474172094), (129642971, 474294730), (129570281, 474560814),
(129393864, 475207835), (129308624, 475521090), (129296867, 475564330),
(129289433, 475591677), (129251927, 475729683), (129027713, 476556366),
(129013871, 476607495), (128863199, 477164765), (128809363, 477364195),
(128737141, 477632001), (128726855, 477670165), (128712899, 477721959),
(128659430, 477920490), (128617450, 478076482), (128476803, 478599847),
(128464418, 478645986), (128368839, 479002370), (128303637, 479245793),
(128298717, 479264170), (128185967, 479685723), (128170386, 479744034),
(128152822, 479809785), (128081068, 480078586), (128009973, 480345217),
(127914013, 480705566), (127772359, 481238499), (127762849, 481274318),
(127726593, 481410930), (127587428, 481936026), (127513710, 482214642),
(127469141, 482383245), (127442441, 482484310), (127347336, 482844635),
(127277772, 483108535), (127248020, 483221490), (127230031, 483289814),
(127211107, 483361710), (127157961, 483563730), (127142873, 483621117),
(127055861, 483952315), (126917427, 484480183), (126893335, 484572165),
(126885759, 484601099), (126884610, 484605485), (126822286, 484843634),
(126789494, 484969030), (126735899, 485174118), (126662673, 485454606),
(126636466, 485555070), (126567550, 485819455), (126525799, 485979765),
(126477972, 486163535), (126354738, 486637690), (126351463, 486650307),
(126313058, 486798270), (126294311, 486870531), (126282443, 486916287),
(126270529, 486962229), (126038654, 487858098), (125988762, 488051290),
(125985333, 488064577), (125880909, 488469449), (125850560, 488587242),
(125827601, 488676390), (125797983, 488791446), (125637587, 489415465),
(125445920, 490163235), (125426940, 490237410), (125419643, 490265930),
(125417831, 490273014), (125364651, 490480991), (125359663, 490500507),
(125349321, 490540974), (125095834, 491534978), (125029541, 491795601),
(125009006, 491876385), (125007298, 491883106), (124962116, 492060954),
(124950754, 492105698), (124942666, 492137555), (124927225, 492198382),
(124756207, 492873095), (124608684, 493456605), (124571733, 493602977),
(124546442, 493703210), (124540616, 493726305), (124473794, 493991355),
(124415791, 494221654), (124289737, 494722893), (124259327, 494843965),
(124194242, 495103290), (124114690, 495420630), (124105159, 495458678),
(124104253, 495462297), (124067775, 495607970), (124062838, 495627690),
(124026849, 495771510), (123996090, 495894490), (123967723, 496007967),
(123942073, 496110615), (123864669, 496420638), (123691432, 497115905),
(123646725, 497295645), (123635483, 497340865), (123606381, 497457961),
(123570433, 497602677), (123555413, 497663166), (123554037, 497668710),
(123283059, 498762590), (123275971, 498791271), (123149604, 499303090),
(123114873, 499443945), (123107523, 499473767), (123049595, 499708902),
(123026424, 499803018), (123015238, 499848466), (122970776, 500029194),
(122883744, 500383338), (122798789, 500729515), (122758281, 500894745),
(122749367, 500931123), (122720512, 501048905), (122668637, 501260793),
(122666259, 501270510), (122635243, 501397286), (122597761, 501550581),
(122568253, 501671326), (122551419, 501740239), (122434221, 502220521),
(122331335, 502642910), (122327694, 502657870), (122254830, 502957455),
(122203755, 503167665), (122197861, 503191934), (122146810, 503402242),
(122040149, 503842209), (121964524, 504154618), (121901465, 504415415),
(121888249, 504470109), (121866102, 504561785), (121851200, 504623490),
(121805141, 504814310), (121785821, 504894390), (121768647, 504965603),
(121654701, 505438570), (121590231, 505706565), (121551812, 505866405),
(121514885, 506020130), (121363651, 506650694), (121357876, 506674805),
(121329508, 506793270), (121293529, 506943598), (121229251, 507212391),
(121225643, 507227487), (121210908, 507289146), (120955134, 508361870),
(120925227, 508487595), (120861054, 508757585), (120822453, 508920126),
(120680687, 509517965), (120553660, 510054842), (120484006, 510349714),
(120459077, 510455330), (120431519, 510572139), (120420157, 510620313),
(120408841, 510668301), (120397893, 510714737), (120378797, 510795753),
(120318579, 511051398), (120296718, 511144270), (120187977, 511606733),
(120176391, 511656054), (120146988, 511781270), (120110991, 511934651),
(120025983, 512297227), (120019646, 512324274), (119936008, 512681546),
(119899351, 512838291), (119875008, 512942430), (119724977, 513585215),
(119661496, 513857674), (119568423, 514257667), (119533737, 514406893),
(119528981, 514427361), (119519120, 514469802), (119493848, 514578610),
(119245326, 515651055), (119194634, 515870355), (119185675, 515909130),
(119155936, 516037890), (119139091, 516110854), (119131379, 516144265),
(119066303, 516426365), (119064583, 516433827), (118748029, 517810515),