def blocks26 : List (ℕ × ℕ × ℕ × ℕ × List ℕ) :=
  [ (4, 9, 4, 20174002,
     [3, 3, 3, 3, 2, 2, 2, 2, 2])
  , (4, 9, 4, 20174002,
     [3, 3, 3, 3, 2, 2, 2, 2, 2])
  , (4, 10, 5, 141234823,
     [3, 3, 3, 3, 3, 2, 2, 2, 2, 2])
  , (4, 10, 5, 141234823,
     [3, 3, 3, 3, 3, 2, 2, 2, 2, 2])
  , (6, 9, 12, 1178941635,
     [5, 5, 5, 5, 3, 3, 3, 3, 3])
  , (6, 9, 12, 1178941635,
     [5, 5, 5, 5, 3, 3, 3, 3, 3])
  , (6, 10, 13, 12968519039,
     [5, 5, 5, 5, 4, 3, 3, 3, 3, 3])
  , (12, 8, 44, 39148165341,
     [11, 11, 10, 8, 7, 6, 6, 6])
  , (6, 11, 15, 142655480993,
     [5, 5, 5, 5, 5, 3, 3, 3, 3, 3, 3])
  , (8, 10, 26, 288323564464,
     [7, 7, 7, 7, 5, 5, 4, 4, 4, 4])
  , (9, 10, 32, 1007996772435,
     [8, 8, 8, 8, 8, 6, 6, 5, 5, 5])
  , (10, 10, 39, 3065480580577,
     [9, 9, 9, 8, 7, 5, 5, 5, 5, 5])
  , (11, 10, 48, 8339935791921,
     [10, 10, 10, 10, 9, 7, 7, 6, 6, 6])
  , (12, 10, 57, 20713080642599,
     [11, 11, 11, 10, 7, 7, 6, 6, 6, 6])
  , (10, 11, 43, 58245024902707,
     [9, 9, 9, 9, 7, 5, 5, 5, 5, 5, 5])
  , (15, 10, 89, 210353530941928,
     [14, 14, 14, 14, 10, 9, 9, 8, 8, 8])
  , (12, 11, 63, 476404401204776,
     [11, 11, 11, 11, 8, 6, 6, 6, 6, 6, 6])
  , (18, 10, 128, 1379267836015099,
     [17, 17, 17, 14, 11, 10, 10, 9, 9, 9])
  , (20, 10, 161, 4070191835798995,
     [19, 19, 19, 16, 12, 11, 11, 10, 10, 10])
  , (16, 11, 111, 12704207178489388,
     [15, 15, 15, 14, 11, 8, 8, 8, 8, 8, 8])
  , (18, 11, 141, 48274502939122224,
     [17, 17, 17, 16, 11, 10, 10, 9, 9, 9, 9])
  , (20, 11, 176, 158737756058174173,
     [19, 19, 19, 18, 12, 11, 11, 10, 10, 10, 10])
  , (22, 11, 213, 464646545841009414,
     [21, 21, 21, 20, 13, 11, 11, 11, 11, 11, 11])
  , (24, 11, 255, 1236078990778438957,
     [23, 23, 23, 22, 13, 13, 12, 12, 12, 12, 12])
  , (19, 12, 174, 3291475889527238177,
     [18, 18, 18, 18, 17, 11, 11, 10, 10, 10, 10, 10])
  , (21, 12, 213, 11281744726473724099,
     [20, 20, 20, 20, 18, 13, 12, 12, 11, 11, 11, 11])
  , (23, 12, 255, 34476260596628410227,
     [22, 22, 22, 22, 19, 15, 13, 12, 12, 12, 12, 12])
  , (25, 12, 306, 95790613541711729395,
     [24, 24, 24, 24, 21, 16, 13, 13, 13, 13, 13, 13])
  , (20, 13, 210, 241440362452890378697,
     [19, 19, 19, 19, 17, 11, 11, 10, 10, 10, 10, 10, 10])
  , (22, 13, 256, 859132035981840009419,
     [21, 21, 21, 21, 19, 11, 11, 11, 11, 11, 11, 11, 11])
  , (24, 13, 303, 2730499776945674512146,
     [23, 23, 23, 23, 20, 14, 12, 12, 12, 12, 12, 12, 12])
  , (26, 13, 357, 7895548133290205689726,
     [25, 25, 25, 25, 22, 13, 13, 13, 13, 13, 13, 13, 13])
  , (21, 14, 252, 18964613572290658358808,
     [20, 20, 20, 20, 20, 17, 14, 11, 11, 11, 11, 11, 11, 11])
  , (23, 14, 301, 69814430029041992363352,
     [22, 22, 22, 22, 22, 18, 14, 13, 13, 12, 12, 12, 12, 12])
  , (25, 14, 357, 229993268100624116936742,
     [24, 24, 24, 24, 24, 19, 16, 13, 13, 13, 13, 13, 13, 13])
  , (21, 15, 268, 777549157118875615772942,
     [20, 20, 20, 20, 20, 19, 14, 12, 11, 11, 11, 11, 11, 11, 11])
  , (22, 15, 295, 1588535180290004404198286,
     [21, 21, 21, 21, 21, 16, 13, 12, 12, 11, 11, 11, 11, 11, 11])
  , (24, 15, 352, 6031674169570724883894066,
     [23, 23, 23, 23, 23, 18, 13, 12, 12, 12, 12, 12, 12, 12, 12])
  , (26, 15, 411, 20536321065820087520359711,
     [25, 25, 25, 25, 25, 19, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (22, 16, 314, 68307012817292676301490348,
     [21, 21, 21, 21, 21, 19, 13, 11, 11, 11, 11, 11, 11, 11, 11, 11])
  , (24, 16, 373, 283488686077284406247548507,
     [23, 23, 23, 23, 23, 20, 15, 13, 12, 12, 12, 12, 12, 12, 12, 12])
  , (26, 16, 439, 1047352374718665833311935580,
     [25, 25, 25, 25, 25, 22, 15, 14, 13, 13, 13, 13, 13, 13, 13, 13])
  , (22, 17, 335, 2937201553002686840718744833,
     [21, 21, 21, 21, 21, 21, 13, 12, 12, 11, 11, 11, 11, 11, 11, 11, 11])
  , (23, 17, 367, 6361839942729851717363991477,
     [22, 22, 22, 22, 22, 22, 20, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 17, 433, 27058478018720021721491702120,
     [24, 24, 24, 24, 24, 24, 21, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 17, 469, 53414971128744071755532800294,
     [25, 25, 25, 25, 25, 25, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (23, 18, 389, 286282797425942691193379616477,
     [22, 22, 22, 22, 22, 22, 22, 14, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (24, 18, 422, 626226507900765922446928018748,
     [23, 23, 23, 23, 23, 23, 18, 14, 13, 13, 12, 12, 12, 12, 12, 12, 12, 12])
  , (26, 18, 496, 2724163527602374641223422393313,
     [25, 25, 25, 25, 25, 25, 20, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (22, 19, 374, 5430885671743584843344089037364,
     [21, 21, 21, 21, 21, 21, 19, 14, 12, 12, 11, 11, 11, 11, 11, 11, 11, 11, 11])
  , (24, 19, 446, 29432645871684572804332462615891,
     [23, 23, 23, 23, 23, 23, 21, 14, 13, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 19, 485, 64967405723541146373366086496668,
     [24, 24, 24, 24, 24, 24, 24, 19, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 19, 523, 138932339908649994735521406305779,
     [25, 25, 25, 25, 25, 25, 23, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (23, 20, 434, 579722664788018183660408381569602,
     [22, 22, 22, 22, 22, 22, 22, 21, 14, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (24, 20, 470, 1383334355980213112698975857879784,
     [23, 23, 23, 23, 23, 23, 23, 15, 13, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (26, 20, 551, 7085549335373357373532695384693298,
     [25, 25, 25, 25, 25, 25, 25, 15, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (23, 21, 455, 26087519915464126453570712668678977,
     [22, 22, 22, 22, 22, 22, 22, 22, 17, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (24, 21, 494, 65016714731091976487159456601637409,
     [23, 23, 23, 23, 23, 23, 23, 19, 14, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 21, 539, 155986741142269804587834354149271966,
     [24, 24, 24, 24, 24, 24, 24, 24, 17, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 21, 581, 361363016104120800791671999323167668,
     [25, 25, 25, 25, 25, 25, 25, 20, 16, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (23, 22, 477, 1173938396195895067953885540793678977,
     [22, 22, 22, 22, 22, 22, 22, 22, 20, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (24, 22, 518, 3055785592362087318663868232973205774,
     [23, 23, 23, 23, 23, 23, 23, 22, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (26, 22, 608, 18429513821312576878149434939387485684,
     [25, 25, 25, 25, 25, 25, 25, 23, 16, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (23, 23, 499, 52827227828815560487461330335715553977,
     [22, 22, 22, 22, 22, 22, 22, 22, 22, 14, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (24, 23, 541, 143621922841030948248510602561373744494,
     [23, 23, 23, 23, 23, 23, 23, 23, 16, 14, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 23, 590, 374524165482592579701151459428242877521,
     [24, 24, 24, 24, 24, 24, 24, 24, 23, 16, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 23, 636, 939905204887024371725496788388486940201,
     [25, 25, 25, 25, 25, 25, 25, 25, 17, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 23, 636, 939905204887024371725496788388486940201,
     [25, 25, 25, 25, 25, 25, 25, 25, 17, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 24, 565, 6750230373528502564406415414190111518233,
     [23, 23, 23, 23, 23, 23, 23, 23, 20, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 24, 616, 18351684108647060324656321838461871792194,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 19, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 24, 664, 47935165449238408053914904011029739481469,
     [25, 25, 25, 25, 25, 25, 25, 25, 21, 15, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 24, 664, 47935165449238408053914904011029739481469,
     [25, 25, 25, 25, 25, 25, 25, 25, 21, 15, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (25, 25, 642, 899232521323706023986167178706145942384067,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 22, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 25, 692, 2444693437911165053791268541687089648569084,
     [25, 25, 25, 25, 25, 25, 25, 25, 24, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (23, 26, 565, 4813881135900820236540643782147133567116477,
     [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 17, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (24, 26, 613, 14911258895124544400876146178583907075604873,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 17, 14, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 26, 668, 44062393544861597407186254552017089590563397,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 16, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 26, 720, 124679365333469532993188598748222832969455603,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 18, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 26, 720, 124679365333469532993188598748222832969455603,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 18, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (25, 27, 694, 2159057283698218277414455864069359751373552967,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 20, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 27, 748, 6358647632006946607877682826616934899838298369,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 22, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 28, 661, 32938970899330126069038587992379649872327688959,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 28, 720, 105793806901212695754577777105838279175926618792,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 23, 15, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 28, 776, 324291029232354288114211596606902337490474854388,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 24, 16, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 29, 684, 1548131632268515931560374587791883389118761047904,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 18, 14, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 29, 746, 5183896538159422094789497679820365951792572960971,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 18, 15, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 29, 804, 16538842490850068988139187648954238296084761317505,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 19, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 30, 708, 72762186716620248959933480857856975210969940188249,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 21, 14, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 30, 772, 254010930369811682655237065771584058800378815790697,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 22, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 30, 832, 843480967033353519234247766550256079196192554577373,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 22, 16, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 31, 732, 3419822775681151706709076315987828939124545935178100,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 15, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 31, 798, 12446535588120772450371789307393584228396464311904266,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 16, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 31, 860, 43017529318701029522904202746684816508016505363017137,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 32, 756, 160731670457014130226453379444037010085055761865442188,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 19, 13, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 32, 824, 609880243817917850068742772886721876530950666872526894,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 20, 15, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 32, 888, 2193893995253752505753146380432499171737675660286613407,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 20, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 33, 780, 7554388511479664120908967895509867591190200079488298927,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 21, 15, 14, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 33, 850, 29884131947077974653387493637001253174320335203148108221,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 23, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 33, 916, 111888593757941377795592536732673607782138948144351534473,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 23, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 34, 804, 355056260039544213695071959084455387718812850321306173228,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 16, 13, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 34, 876, 1464322465406820758016318521982251569242995213925788347792,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 18, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 34, 944, 5706318281655010267649674603647170306522554952186408220841,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 16, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 35, 827, 16687644221858578043686976857382502081759522442485622418849,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 19, 15, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 35, 902, 71751800804934217142800549996969483722031328803715403274019,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 21, 16, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 35, 972, 291022232364405523650316963027087949806085387764126818653857,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 21, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 36, 851, 784319278427353168054143532262839069815128293126812004619175,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 22, 14, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 36, 928, 3515838239441776639997272497849983434118622085491868623231649,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 15, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (26, 36, 1000, 14842133850584681706170036757736025866886520862819244264401927,
     [25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 23, 16, 15, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  , (24, 37, 875, 36863006086085598898559108338670969023078043071684400855145234,
     [23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 23, 17, 13, 13, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12])
  , (25, 37, 954, 172276073732647055359866428834519153745602479000771844061706820,
     [24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 20, 14, 14, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
  ]