MaxLeafFormal.DSTData

Source file MaxLeafFormal/DSTData.lean of the Lean project (how it is built).

import Mathlib

/-!
# Directed Steiner Tree certificate data (generated)

Generated by `formal/scripts/export_dst_cert.py` from
`ancillary/dst_certificates.json`, SHA-256 `f0ca3bd5d6f3ca881374e596ce53bd93bdc674fb71b0a1a6788e9690445972a7`.
Do not edit by hand. This file is data, not proof: every condition is re-checked in
`MaxLeafFormal.DSTCert`.
-/

set_option maxRecDepth 100000

namespace MaxLeafFormal.DSTCert

/-- The rational `a / b`. -/
def q (a b : ℕ) : ℚ := (a : ℚ) / b

/-! Certificate 0: |Z| = 27. -/

def Z0 : List (ℚ × ℚ) := [
  (q 122011476004000000000000000 233266568833673109847731143, q 246832256427000000000000000 316965519189303131112380779),
  (q 35644889599500000000000000 67465305976253401936394017, q 331684198469000000000000000 434921571459507407928128497),
  (q 24969920698600000000000000 47248557146275097036342849, q 11002078212000000000000000 14434101665556575399198333),
  (q 388959812954000000000000000 735067751773492489747548153, q 169725013463750000000000000 223208497108678927078402869),
  (q 32187178257250000000000000 60810916094918847578983899, q 109211505331500000000000000 143697082892630148012217093),
  (q 160835171975500000000000000 300838765496915822608534473, q 398058974669000000000000000 532909162455708550839937491),
  (q 225431097557500000000000000 420924165626907162508934331, q 723974180070000000000000000 972180236723781004137663179),
  (q 202972431103500000000000000 349351222644064528380877321, q 445335344340000000000000000 697420760521257226520139409),
  (q 17700562023500000000000000 28347049084450981029936627, q 21198207168720000000000000 37196437723280319030862273),
  (q 445337386930000000000000000 711946271859804660860628069, q 391603038166000000000000000 689233238550075986904861381),
  (q 514684986374000000000000000 816049360367394247905739551, q 438520516757000000000000000 782921723572707044713176349),
  (q 12262910804400000000000000 19409116301059068960583697, q 312071396520000000000000000 558856535205113787617364739),
  (q 440149380067000000000000000 656366666805362676946233129, q 1900362940125000000000000 3806898150619306378001849),
  (q 240296104199500000000000000 354751755271524469717544693, q 39352368604200000000000000 80497360904950183411339087),
  (q 545486999844000000000000000 805101054052489089485645867, q 327057182135000000000000000 669365494520062781175805413),
  (q 330959979937500000000000000 487857203280213791809896671, q 767657765500000000000000 1574914992842506925785007),
  (q 453340716956000000000000000 668063847756192947153852177, q 16909129091000000000000000 34707664974672055937377879),
  (q 658437190836000000000000000 960642344506934804897355397, q 308081329896000000000000000 643421762432657180328537503),
  (q 46085924487000000000000000 67120153462287917532946531, q 8025993257750000000000000 16813073027318675884026971),
  (q 558355180330000000000000000 749601361174039114273738751, q 9877815926050000000000000 24131995390586776328704607),
  (q 424665056141000000000000000 530471344153952335107955793, q 169021743321000000000000000 462667925210732744806374743),
  (q 310897441566500000000000000 387676802220231932097297741, q 254107281467000000000000000 697688989261230403377910669),
  (q 114258126344500000000000000 141304707234869387970392751, q 354861657397000000000000000 988353037368163707900262533),
  (q 652856475354000000000000000 805980457570401148254442349, q 135759707471000000000000000 379264209763073199755690199),
  (q 685459791110000000000000000 797302287319268973957812601, q 312028374193000000000000000 975109510029488073877789873),
  (q 713089316438000000000000000 821138387746885340078712171, q 2722207554540000000000000 8686735500131317763164499),
  (q 50000000000000000 38999999996099961, q 0 1)
]

/-- (C1) witnesses, row-major: entry `a * 27 + b` is for `z_a ∘ z_b`. -/
def pairs0 : List (List (ℕ × ℚ)) := [
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1101728714969670772022667882912141109369822107277839747074733795111131 2309531325495525245402539308031025249782796125986185924362958374933874), (8, q 1207802610525854473379871425118884140412974018708346177288224579822743 2309531325495525245402539308031025249782796125986185924362958374933874)],
  [(7, q 115982279407699226713913439304846367912014361730089815009614032842354687 344686491464753647773105698396286078704954490141683115551610744311858698), (8, q 228704212057054421059192259091439710792940128411593300541996711469504011 344686491464753647773105698396286078704954490141683115551610744311858698)],
  [(7, q 1139137038850448976090224237710727596245989440044104264292152627755807 3422170529628037259424023097946058683048167324184335618394414502975178), (8, q 2283033490777588283333798860235331086802177884140231354102261875219371 3422170529628037259424023097946058683048167324184335618394414502975178)],
  [(7, q 236801114067418470997743524157685119029497297157716868265348361355239 751486469778673539330454442368540391094037571839061653322801822906106), (8, q 514685355711255068332710918210855272064540274681344785057453461550867 751486469778673539330454442368540391094037571839061653322801822906106)],
  [(7, q 908518767947485478882305100117564035711167331876993576186709452980529 2920397583735771553346152552846484955453522879794653224682122691423766), (8, q 2011878815788286074463847452728920919742355547917659648495413238443237 2920397583735771553346152552846484955453522879794653224682122691423766)],
  [(7, q 61730803560244247425957843431771248414381806865667225412741076628135483 363955334732459029756455426583568075052336841896382821505358337056706482), (8, q 302224531172214782330497583151796826637955035030715596092617260428570999 363955334732459029756455426583568075052336841896382821505358337056706482)],
  [(7, q 68994464053852940773733696373670397156804833611144332112196732503637 477030998197467654268528693161770087700603962673599515807216331661998), (8, q 408036534143614713494794996788099690543799129062455183695019599158361 477030998197467654268528693161770087700603962673599515807216331661998)],
  [(12, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 49707678213346216659150267681152035796463542373255308316727307421029 338312041601430058489349255796869585762969811637181719264908897610766), (8, q 288604363388083841830198988115717549966506269263926410948181590189737 338312041601430058489349255796869585762969811637181719264908897610766)],
  [(7, q 2204464913363692303288083923666333779083239657194555288771494354504277 11599175794302264682299784491886529702131179955393735772846869096528558), (8, q 9394710880938572379011700568220195923047940298199180484075374742024281 11599175794302264682299784491886529702131179955393735772846869096528558)],
  [(7, q 4647000331229401318715316959483214574675613968180865881603185028066993 24321600016716637791794589637073933501701592110134664109888061376096022), (8, q 19674599685487236473079272677590718927025978141953798228284876348029029 24321600016716637791794589637073933501701592110134664109888061376096022)],
  [(7, q 60854846006655682346128437561259133119673085752012020913901560004959 312083475949463872681169915457197801326856988694333387134150105126986), (8, q 251228629942808190335041477895938668207183902942321366220248545122027 312083475949463872681169915457197801326856988694333387134150105126986)],
  [(7, q 12893273498556796486395607718444634513940640242160712406236500209709407 65926852570986135461185775866964101971233033640525853776943766208149578), (8, q 53033579072429338974790168148519467457292393398365141370707265998440171 65926852570986135461185775866964101971233033640525853776943766208149578)],
  [(7, q 2340032144367687566684455218746023046693512856264564115328768547171699 10915674363915494512761227746480401669799275422498946436954273888642946), (8, q 8575642219547806946076772527734378623105762566234382321625505341471247 10915674363915494512761227746480401669799275422498946436954273888642946)],
  [(7, q 24522662615227033612338761963693285644994263635697086786355349569 112816897688314390245591382295741921804411744879386541119510103926), (8, q 88294235073087356633252620332048636159417481243689454333154754357 112816897688314390245591382295741921804411744879386541119510103926)],
  [(7, q 2472361156676287303054459365940762825166896301221406032014057614226479 7347583588462586041261523705683167033611411672218865748946302264065066), (8, q 4875222431786298738207064339742404208444515370997459716932244649838587 7347583588462586041261523705683167033611411672218865748946302264065066)],
  [(7, q 19391332541355513865578664153027660145436586612516725029011031618099753 99690151609903493658982835614737824619611411080954511736701798326953062), (8, q 80298819068547979793404171461710164474174824468437786707690766708853309 99690151609903493658982835614737824619611411080954511736701798326953062)],
  [(7, q 2329869946349816635022057801181335354487478128647646872141965367287407 12207032741454352993529156727761039299486409951666893924142856643761578), (8, q 9877162795104536358507098926579703944998931823019247052000891276474171 12207032741454352993529156727761039299486409951666893924142856643761578)],
  [(7, q 12528035023514836807304212556531975542458565763319414230659628799147 72448250763247307556000146833955847497976719626795515638762577907538), (8, q 59920215739732470748695934277423871955518153863476101408102949108391 72448250763247307556000146833955847497976719626795515638762577907538)],
  [(7, q 998420305125833660414479957315256825514955649564882275484646662128657 5912457249271391440277096468181506073292918745786288118814567843189078), (8, q 4914036944145557779862616510866249247777963096221405843329921181060421 5912457249271391440277096468181506073292918745786288118814567843189078)],
  [(7, q 2731954652142418998019607908746238436785107409919108952229370351950477 105263082241858483566568557339995497610013588942337057534026970281183358), (8, q 102531127589716064568548949431249259173228481532417948581797599929232881 105263082241858483566568557339995497610013588942337057534026970281183358)],
  [(7, q 99779939300738575144941418515597003249523262488321131179894024803 137966800877057223216545561877492843962134445087422397580837646345762), (8, q 137867020937756484641400620458977246958884921824934076449657752320959 137966800877057223216545561877492843962134445087422397580837646345762)],
  [(13, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 33943759795347029470270305395703399821855372433147196521848765438213 236932977618222294898848751247020793784211526128091396834960468477902), (8, q 202989217822875265428578445851317393962356153694944200313111703039689 236932977618222294898848751247020793784211526128091396834960468477902)],
  [(7, q 1514187037219348378099906545118727275828627499218603048277318188334069 8123350401162981901099520959685205470688186838182957794927347264866926), (8, q 6609163363943633522999614414566478194859559338964354746650029076532857 8123350401162981901099520959685205470688186838182957794927347264866926)],
  [(7, q 13100822850934547309953235197549906854434991860243614196027081760073 69904329770619023586675928915655543898303912556278180583730161026342), (8, q 56803506919684476276722693718105637043868920696034566387703079266269 69904329770619023586675928915655543898303912556278180583730161026342)],
  [(7, q 41820585766798915562706712967140083545379770838562322539625824207423 218564100976531070544422826026705291350157605665950010041849502863242), (8, q 176743515209732154981716113059565207804777834827387687502223678655819 218564100976531070544422826026705291350157605665950010041849502863242)],
  [(7, q 8861001424268879779875960611707171730361584155827281186135899480879679 46171118860273141374191755339252293402782235001658324752891334467497866), (8, q 37310117436004261594315794727545121672420650845831043566755434986618187 46171118860273141374191755339252293402782235001658324752891334467497866)],
  [(7, q 1610927109833139148029491940005421124784675522850413466795998003285203 7644667974308545642465047796839637990276376147067791206103390069927362), (8, q 6033740864475406494435555856834216865491700624217377739307392066642159 7644667974308545642465047796839637990276376147067791206103390069927362)],
  [(7, q 68607817046799695311494131485798664661168501326130669133708230879359 321017739143616063000429207050054602687913695664548038381133179064586), (8, q 252409922096816367688935075564255938026745194338417369247424948185227 321017739143616063000429207050054602687913695664548038381133179064586)],
  [(7, q 1712879919088387841867434502258661329081762471070123942389085763886863 5145796317720736317375518378893830756914717694872261575932290699825002), (8, q 3432916398632348475508083876635169427832955223802137633543204935938139 5145796317720736317375518378893830756914717694872261575932290699825002)],
  [(7, q 13325449960971628596371835188962778723617271448813200860827209173344841 69816860045358224544510424814906428294782119166279775878428704858002214), (8, q 56491410084386595948138589625943649571164847717466575017601495684657373 69816860045358224544510424814906428294782119166279775878428704858002214)],
  [(7, q 4801377495197077920746486627600745067519031856609746047357040664237037 25647168232249691015493439424594758542367433001307242523894850271185598), (8, q 20845790737052613094746952796994013474848401144697496476537809606948561 25647168232249691015493439424594758542367433001307242523894850271185598)],
  [(7, q 25764695196255306745007637638418075262627624109616979468718971865377 152214916991845600360591507849615613352436963814466094910941149707958), (8, q 126450221795590293615583870211197538089809339704849115442222177842581 152214916991845600360591507849615613352436963814466094910941149707958)],
  [(7, q 9370937162115685280979017210201572072686785369829296415167214799273 56722218675440049172453150749449397226703144499558765792146826103142), (8, q 47351281513324363891474133539247825154016359129729469376979611303869 56722218675440049172453150749449397226703144499558765792146826103142)],
  [(7, q 1640786652782078825436783028081589797139843986881436822133800040135469 73719798416805525766605175295146305079041635909460514666048904926462526), (8, q 72079011764023446941168392267064715281901791922579077843915104886327057 73719798416805525766605175295146305079041635909460514666048904926462526)],
  [(8, q 1463447206295169748663501899340167523583209010941088395498712528820 1659031231334771969963595230645231251463094718289275420719424522487), (9, q 195584025039602221300093331305063727879885707348187025220711993667 1659031231334771969963595230645231251463094718289275420719424522487)],
  [(14, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 461732442304596396036074891176736385467465316012023058225453141263261 3686076394664173455661293868567785858300097790312755525786538591292894), (8, q 3224343952359577059625218977391049472832632474300732467561085450029633 3686076394664173455661293868567785858300097790312755525786538591292894)],
  [(7, q 7096362851741136985536491559018693668607148684488421060957307891366831 42126245236548420502546003550197453987329068404662418067596958428901674), (8, q 35029882384807283517009511991178760318721919720173997006639650537534843 42126245236548420502546003550197453987329068404662418067596958428901674)],
  [(7, q 134724436602809799097320129444798743005340815032045152650743828176982811 794987449554358447919723895109300861158489544597428541615092787441188594), (8, q 660263012951548648822403765664502118153148729565383388964348959264205783 794987449554358447919723895109300861158489544597428541615092787441188594)],
  [(7, q 11561299386077248407361131760523263932990392427455750147576773119581 66672612703981875729286925819331409656163140042681208726405312750174), (8, q 55111313317904627321925794058808145723172747615225458578828539630593 66672612703981875729286925819331409656163140042681208726405312750174)],
  [(7, q 2192455828433295382287029456446932918688463352789021542513548409696959 12601851646641511088301706767131664460170145580075627173726838638094986), (8, q 10409395818208215706014677310684731541481682227286605631213290228398027 12601851646641511088301706767131664460170145580075627173726838638094986)],
  [(7, q 7643804035019405243414260706008587442251596089210454823003401904013097 39643883611324277577387694589570128318165857301491230482791168663220838), (8, q 32000079576304872333973433883561540875914261212280775659787766759207741 39643883611324277577387694589570128318165857301491230482791168663220838)],
  [(7, q 325972203137561129558958675486090036666233253335528393443704585890541 1664740696463153467269092782025501782970481094588580002443437543630014), (8, q 1338768493325592337710134106539411746304247841253051608999732957739473 1664740696463153467269092782025501782970481094588580002443437543630014)],
  [(7, q 8408775004661699590544328766466278418450996120646924106978588316737437 26685181226036634844334065013995289195414919446488527520546057741727198), (8, q 18276406221374935253789736247529010776963923325841603413567469424989761 26685181226036634844334065013995289195414919446488527520546057741727198)],
  [(7, q 62608447160223601620052478658774570410080429569089308048016687161505259 362057774523117088385243543102158402530940403744222438577660992462783186), (8, q 299449327362893486765191064443383832120859974175133130529644305301277927 362057774523117088385243543102158402530940403744222438577660992462783186)],
  [(7, q 67537663792444826242108359574983466765959222287667228634794775516785989 399004910001205669153813542305402079319419505236254416901743027091766606), (8, q 331467246208760842911705182730418612553460282948587188266948251574980617 399004910001205669153813542305402079319419505236254416901743027091766606)],
  [(7, q 358287689910699436183192574619600640377907950151948802751665482922969 2368078171640117211849248924594675233283629670299857026057164616987526), (8, q 2009790481729417775666056349975074592905721720147908223305499134064557 2368078171640117211849248924594675233283629670299857026057164616987526)],
  [(7, q 9484820586792361765098976609947442905104966701350143468772801414999913 64419135061931604976798622275521881073538369025112284901560218973769702), (8, q 54934314475139243211699645665574438168433402323762141432787417558769789 64419135061931604976798622275521881073538369025112284901560218973769702)],
  [(7, q 4707863450187015939218548617844121965611552229625796582843843068316293 1146893148835728511549470012163727398673299075474581908554927345837398222), (8, q 1142185285385541495610251463545883276707687523244956111972083502769081929 1146893148835728511549470012163727398673299075474581908554927345837398222)],
  [(8, q 17000114635356216799014171701293188516106263368570478862546311820 104495220774580593411707333143698526757619252318379092397209156537), (9, q 87495106139224376612693161442405338241512988949808613534662844717 104495220774580593411707333143698526757619252318379092397209156537)],
  [(15, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 36957141266432182798280032835378385017822894473903602910034206717063 304942886985002544080366042447305389823248899442621104732466034415802), (8, q 267985745718570361282086009611927004805426004968717501822431827698739 304942886985002544080366042447305389823248899442621104732466034415802)],
  [(7, q 572928029808500050717387507149200998050419048268307172431002308681373 3485033261618456888899157125295134096125375137585410791340215176216542), (8, q 2912105231809956838181769618145933098074956089317103618909212867535169 3485033261618456888899157125295134096125375137585410791340215176216542)],
  [(7, q 10878661114228204433072535509743969046025276915023002660134046060359713 65767971693391007424327508662764364771206702549501247001476246673438902), (8, q 54889310579162802991254973153020395725181425634478244341342200613079189 65767971693391007424327508662764364771206702549501247001476246673438902)],
  [(7, q 15879225574945080425988652003622361996912608752435701429682082913591 93767118748182569243824772606471154008052650903400622611427304714714), (8, q 77887893173237488817836120602848792011140042150964921181745221801123 93767118748182569243824772606471154008052650903400622611427304714714)],
  [(7, q 3365836325348747808312884794377590522433284150489950735976076937874743 19808068962672683682586404860361122453220019829391763221480095558914522), (8, q 16442232637323935874273520065983531930786735678901812485504018621039779 19808068962672683682586404860361122453220019829391763221480095558914522)],
  [(7, q 619073075119999831084832444688862983309738605294034443363831197599851 3279671668561837960418266095259414149059933930239795596968259067660754), (8, q 2660598593441838129333433650570551165750195324945761153604427870060903 3279671668561837960418266095259414149059933930239795596968259067660754)],
  [(7, q 26409340325733733236911336731769369556391658604467546417240915453303 137721191778812349909952709086277851373956543345746086781417404284762), (8, q 111311851453078616673041372354508481817564884741278540364176488831459 137721191778812349909952709086277851373956543345746086781417404284762)],
  [(7, q 686777810989078412239024845960722729126627485387794871005439789736071 2207620063047276746698317089316672181718916304938216634983740949352634), (8, q 1520842252058198334459292243355949452592288819550421763978301159616563 2207620063047276746698317089316672181718916304938216634983740949352634)],
  [(7, q 5057983923094120910447021284502886597287251059494967623547992580318097 29952429412007140053168240598006906851514633846980020903455048567690838), (8, q 24894445488913019142721219313504020254227382787485053279907055987372741 29952429412007140053168240598006906851514633846980020903455048567690838)],
  [(7, q 147387450841976159070494381988349778482450958741094153510378054042451 892135233866712580503021584739028620154076801184555014902285718441154), (8, q 744747783024736421432527202750678841671625842443460861391907664398703 892135233866712580503021584739028620154076801184555014902285718441154)],
  [(7, q 134544513973810218389977296884019122641973163178653960674037721 913801282608331744040598407539559356831171304008301706263161734), (8, q 779256768634521525650621110655540234189198140829647745589124013 913801282608331744040598407539559356831171304008301706263161734)],
  [(7, q 763004925738643313772074490161835161579571364291718192747431068103979 5329286460611172475592269567465351220814867561725323866740874345450066), (8, q 4566281534872529161820195077303516059235296197433605673993443277346087 5329286460611172475592269567465351220814867561725323866740874345450066)],
  [(8, q 1 1)],
  [(9, q 1 1)],
  [(16, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(8, q 1 1)],
  [(7, q 369611691446031117487797272374292924165480536848773028822401593445471 17240870084977886568133998773888890784929252519944252401618239444380234), (8, q 16871258393531855450646201501514597860763771983095479372795837850934763 17240870084977886568133998773888890784929252519944252401618239444380234)],
  [(7, q 7308048360899027541272133962655220437269843210217086755347070622432651 325361903487736941272125361600683149179781375468547782361112573561271954), (8, q 318053855126837913730853227638027928742511532258330695605765502938839303 325361903487736941272125361600683149179781375468547782361112573561271954)],
  [(7, q 12264288796506750194371379391218316232418993279423604455730444189757 463876982290075789926167000613662867396006797661167249461710150168478), (8, q 451612693493569039731795621222444551163587804381743645005979705978721 463876982290075789926167000613662867396006797661167249461710150168478)],
  [(7, q 882571045508351947226858157116422030497360891477893434579896487287487 32664283521656186939483177121470922679107497738438426548643061570869898), (8, q 31781712476147834992256318964354500648610136846960533114063165083582411 32664283521656186939483177121470922679107497738438426548643061570869898)],
  [(7, q 249036910653150540312909659329767991173497592849401574645059396242259 5408307364121393907554669442849021263688766274637409185250041284181186), (8, q 5159270453468243367241759783519253272515268681788007610604981887938927 5408307364121393907554669442849021263688766274637409185250041284181186)],
  [(7, q 33436627443997787072952466890517420352274546484737203900853463331581 681322959398136835858225227042862452710529136152378897609803409798174), (8, q 647886331954139048785272760152345032358254589667641693708949946466593 681322959398136835858225227042862452710529136152378897609803409798174)],
  [(7, q 168398314317149125935735094695909040556477260298323627464158494398247 992850591939362930215331391502745513603796116993845316272496570338938), (8, q 824452277622213804279596296806836473047318856695521688808338075940691 992850591939362930215331391502745513603796116993845316272496570338938)],
  [(7, q 3845755845813607503512462639229818430740841471746860289921607649616219 148178196721733917246203050203690634149575821018609924947495769354023026), (8, q 144332440875920309742690587564460815718834979546863064657574161704406807 148178196721733917246203050203690634149575821018609924947495769354023026)],
  [(7, q 3634566699609109325932498685474970573564675657173414860529244900008149 163299429559194241883194418464464071865440919613260835807758961793571246), (8, q 159664862859585132557261919778989101291876243956087420947229716893563097 163299429559194241883194418464464071865440919613260835807758961793571246)],
  [(7, q 3978353422646668268785255094328262767525301707510373799342981756329 969175578764788400720544476568790778531599739919176543948385436356966), (8, q 965197225342141732451759221474462515764074438211666170149042454600637 969175578764788400720544476568790778531599739919176543948385436356966)],
  [(8, q 1 1)],
  [(10, q 1 1)],
  [(11, q 1 1)],
  [(17, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(7, q 784788166539752980035682840613868843064689465310998317789307395479 649042125277500194471963602688441547231792580110560669673246602391066), (8, q 648257337110960441491927919847827678388727890645249671355457294995587 649042125277500194471963602688441547231792580110560669673246602391066)],
  [(7, q 81851727497595623471426228855816530262307807544458113690645401229789 45702841069844833117718801534365721738474090421620542930106410361171806), (8, q 45620989342347237494247375305509905208211782614076084816415764959942017 45702841069844833117718801534365721738474090421620542930106410361171806)],
  [(7, q 157790312166999063335155513076148749515662452967653870686796739656473 7567134045828258448073527855034121597156709201814836021683283087751942), (8, q 7409343733661259384738372341957972847641046748847182150996486348095469 7567134045828258448073527855034121597156709201814836021683283087751942)],
  [(7, q 22770474439530022990438878396471426195486863306009100094509192642007 953285716797212411354594260750385006377929871654958927795775001389978), (8, q 930515242357682388364155382353913580182443008348949827701265808747971 953285716797212411354594260750385006377929871654958927795775001389978)],
  [(7, q 2210112039577574154300763640789916157051075878301159593768596798202599 15280819509591951744942415355622020896771110788021628091955125938231546), (8, q 13070707470014377590641651714832104739720034909720468498186529140028947 15280819509591951744942415355622020896771110788021628091955125938231546)],
  [(7, q 149941899518220524448494614993328247445002062185694729273977933164593 207326285614062561243615460227560943298231877445534178306079847718246422), (8, q 207176343714544340719166965612567615050786875383348483576805869785081829 207326285614062561243615460227560943298231877445534178306079847718246422)],
  [(8, q 3460581954961621821046451633061795843244652781779952528490683684181060 3923075268570852664222360813341372844995502694801926816275514300097571), (9, q 462493313609230843175909180279577001750849913021974287784830615916511 3923075268570852664222360813341372844995502694801926816275514300097571)],
  [(8, q 3787911793268897106691664376833036081008024157992298910118988690260 23283294707265017399326698527803405074094986791097711842755339519791), (9, q 19495382913996120292635034150970368993086962633105412932636350829531 23283294707265017399326698527803405074094986791097711842755339519791)],
  [(9, q 1 1)],
  [(11, q 1 1)],
  [(11, q 342992183330201884199184154925444941039306244352122867799057034776095 353106555486224876803535097325658130839882392309044497987444042155017), (12, q 10114372156022992604350942400213189800576147956921630188387007378922 353106555486224876803535097325658130839882392309044497987444042155017)],
  [(18, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(8, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(11, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(14, q 1 1)],
  [(15, q 1 1)],
  [(16, q 1 1)],
  [(17, q 1 1)],
  [(18, q 1 1)],
  [(19, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(18, q 51443708740880482603611018760305946805498139319614733360279162791590 207593541961636491818176901748101920360122837699280813794761939327169), (19, q 156149833220756009214565882987795973554624698379666080434482776535579 207593541961636491818176901748101920360122837699280813794761939327169)],
  [(18, q 678066339435615198959620120371455464218346453929273195863417752109890 2372478354181355788213455862139377588275423880723508058203997378792699), (19, q 1694412014745740589253835741767922124057077426794234862340579626682809 2372478354181355788213455862139377588275423880723508058203997378792699)],
  [(18, q 12836048285912453421865470169264053743965577813048026017641672826106090 44772338605606361550120812451273681857555022044770574100155021787724119), (19, q 31936290319693908128255342282009628113589444231722548082513348961618029 44772338605606361550120812451273681857555022044770574100155021787724119)],
  [(18, q 18521750888630165976897936480582739113887221097614972238875378250630 63833095085211559679561338759648791623954436241135689515628149631633), (19, q 45311344196581393702663402279066052510067215143520717276752771381003 63833095085211559679561338759648791623954436241135689515628149631633)],
  [(18, q 1306497504452653866580169755252979971788285018547995493783503395571330 4494860481403102424665233494354150129649501657208904453297856319351003), (19, q 3188362976950448558085063739101170157861216638660908959514352923779673 4494860481403102424665233494354150129649501657208904453297856319351003)],
  [(18, q 228649955637971596788132294889090209428221244269301722126740533310810 744225325688027101384794079263092470412941649830358265469900113636671), (19, q 515575370050055504596661784374002260984720405561056543343159580325861 744225325688027101384794079263092470412941649830358265469900113636671)],
  [(18, q 432834555835755901938425868678772927858922459423192262910 1396828741914341247064129462164857695207844965482892103781), (19, q 963994186078585345125703593486084767348922506059699840871 1396828741914341247064129462164857695207844965482892103781)],
  [(18, q 831664835871671493164673762344199632938557283389261050470 2004884217569579735082553596188148318739828920093094081377), (19, q 1173219381697908241917879833843948685801271636703833030907 2004884217569579735082553596188148318739828920093094081377)],
  [(18, q 5907869540036765519647664858921040088859967311242951287073574950267210 20390476962659124236408375644228087908956779425087091806735746017591911), (19, q 14482607422622358716760710785307047820096812113844140519662171067324701 20390476962659124236408375644228087908956779425087091806735746017591911)],
  [(18, q 6438428326802910867282163795297702173753726855550626486567403527565910 22471276679760928339344556613661044456203179373031627242735853541651081), (19, q 16032848352958017472062392818363342282449452517481000756168450014085171 22471276679760928339344556613661044456203179373031627242735853541651081)],
  [(18, q 1047014391237978781292937387562557452753015831971334688353075584011190 3867617704323321123998894228334396759836368011493854389509267334453529), (19, q 2820603313085342342705956840771839307083352179522519701156191750442339 3867617704323321123998894228334396759836368011493854389509267334453529)],
  [(18, q 6784213708369657081040307123078877198357239201319960165058799507416290 25395831475112057435245734346854360074374974078568344993750529652232939), (19, q 18611617766742400354205427223775482876017734877248384828691730144816649 25395831475112057435245734346854360074374974078568344993750529652232939)],
  [(18, q 9121874825637489530578325965119017524714046994055221176793712338931670 64591067988441571168687299135306744935882841704853492905079713318916297), (19, q 55469193162804081638108973170187727411168794710798271728286000979984627 64591067988441571168687299135306744935882841704853492905079713318916297)],
  [(18, q 70518131263922649221131811443800754939154581900728318377589671259910 592610056447489476613078996064240040657890091343418163928224201686481), (19, q 522091925183566827391947184620439285718735509442689845550634530426571 592610056447489476613078996064240040657890091343418163928224201686481)],
  [(20, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(18, q 1177105781352240602697651492966628765841711109925579834654915591326730 5213786021305063393768847332783614331978566687899604900272926487947143), (19, q 4036680239952822791071195839816985566136855577974025065618010896620413 5213786021305063393768847332783614331978566687899604900272926487947143)],
  [(18, q 15720481908775161986056237398539458746360589180099196870681029728426830 59585642029102765977600173936905718988086146668582449646616697809201053), (19, q 43865160120327603991543936538366260241725557488483252775935668080774223 59585642029102765977600173936905718988086146668582449646616697809201053)],
  [(18, q 297673361742675929299563624832974450242406874710767503363589434286208230 1124473290244193732728018616150639723024211553996695217308313577499413793), (19, q 826799928501517803428454991317665272781804679285927713944724143213205563 1124473290244193732728018616150639723024211553996695217308313577499413793)],
  [(18, q 429962485437397965526332818881487097158706962771020280063351618733610 1603191003472627320387045740483625723265377259192216507548955619588151), (19, q 1173228518035229354860712921602138626106670296421196227485604000854541 1603191003472627320387045740483625723265377259192216507548955619588151)],
  [(18, q 30333353846238193092761596017472224510762148497252599012500512189866510 112890027908415863871313757984466933005183638700885068235268867681444541), (19, q 82556674062177670778552161966994708494421490203632469222768355491578031 112890027908415863871313757984466933005183638700885068235268867681444541)],
  [(18, q 5332583333471291671680815595144733969853324340003319625696759423406070 18691485116095349218686451090789234653445648512715324257978548238025337), (19, q 13358901782624057547005635495644500683592324172712004632281788814619267 18691485116095349218686451090789234653445648512715324257978548238025337)],
  [(18, q 10101353610546869574032728959920895644691976521579107334770 35081853221117993415088032668861308015802264455746463317507), (19, q 24980499610571123841055303708940412371110287934167355982737 35081853221117993415088032668861308015802264455746463317507)],
  [(18, q 19792461519001598813480871689648592897331948445746955798090 50353383872756247182914008209557428408008981654500687481319), (19, q 30560922353754648369433136519908835510677033208753731683229 50353383872756247182914008209557428408008981654500687481319)],
  [(18, q 137128068737124456149992097472279108594133476143368369841567845611476870 512114118536989764408006052345340654139670640880741725629966694804713617), (19, q 374986049799865308258013954873061545545537164737373355788398849193236747 512114118536989764408006052345340654139670640880741725629966694804713617)],
  [(18, q 149301994498696232317841309496618149252404519723280045125619288753975770 564374147320379349480143393469036683004897859364990301690071411349380607), (19, q 415072152821683117162302083972418533752493339641710256564452122595404837 564374147320379349480143393469036683004897859364990301690071411349380607)],
  [(18, q 24158983522927812545049931196746989477725994354693584316328753178327930 97136601322017099755697045735179261976695795681083430155590466387374063), (19, q 72977617799089287210647114538432272498969801326389845839261713209046133 97136601322017099755697045735179261976695795681083430155590466387374063)],
  [(18, q 22335826985314475521529794438727030115243209689309897399845061678421090 91117912362492341911385198212630300368664936591294458132678608729240619), (19, q 68782085377177866389855403773903270253421726901984560732833547050819529 91117912362492341911385198212630300368664936591294458132678608729240619)],
  [(18, q 193038354903053407166305307686976579434105862664816227917348608579174490 1622227763913464956612001043149674801816444131198263370524119035450458559), (19, q 1429189409010411549445695735462698222382338268533447142606770426871284069 1622227763913464956612001043149674801816444131198263370524119035450458559)],
  [(18, q 205665141224394461534796610607849218665559402148072397078120810399110 2126230489497124292027177963163090164736536090119837095765961272909201), (19, q 1920565348272729830492381352555240946070976687971764698687840462510091 2126230489497124292027177963163090164736536090119837095765961272909201)],
  [(21, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(18, q 727308154109654297157799310883188465791641979936870158378725255068670 5976162690850200134876376074295193297457350899592498994164816016672997), (19, q 5248854536740545837718576763412004831665708919655628835786090761604327 5976162690850200134876376074295193297457350899592498994164816016672997)],
  [(18, q 10933143367183698933587539400331912216615645879469967627250540970066570 68298447490859197445431419893407122765133752832134710498160452939650887), (19, q 57365304123675498511843880493075210548518106952664742870909911969584317 68298447490859197445431419893407122765133752832134710498160452939650887)],
  [(18, q 207485143659960840161209670669842209549034448322923606149681057154057170 1288897414768246680625027070491946386763391380562146643564157167993523347), (19, q 1081412271108285840463817399822104177214356932239223037414476110839466177 1288897414768246680625027070491946386763391380562146643564157167993523347)],
  [(18, q 302244858647878526660297953268548335882838641502423670855694873604190 1837614781678670666338430621971884013662559313480376479833876552739829), (19, q 1535369923030792139678132668703335677779720671977952808978181679135639 1837614781678670666338430621971884013662559313480376479833876552739829)],
  [(18, q 21348916176181907434930993615328630249238886608394809997944819538713290 129397173224696556609563228173907582030387064269581079537201339576745639), (19, q 108048257048514649174632234558578951781148177661186269539256520038032349 129397173224696556609563228173907582030387064269581079537201339576745639)],
  [(18, q 3893313714014563814043434421335414959626417426380452519709622200342530 21424614575845283240342207727837762604113074480242787961760409561584923), (19, q 17531300861830719426298773306502347644486657053862335442050787361242393 21424614575845283240342207727837762604113074480242787961760409561584923)],
  [(18, q 7414436117852624221943281888702342027097942154587544539830 40211635362329184226909606119989138486079867625597142419353), (19, q 32797199244476560004966324231286796458981925471009597879523 40211635362329184226909606119989138486079867625597142419353)],
  [(18, q 16760256171769818262557605845000712963049615657913190930110 57716218661214009975334347993988154534894476379125950071301), (19, q 40955962489444191712776742148987441571844860721212759141191 57716218661214009975334347993988154534894476379125950071301)],
  [(18, q 96296943562408640467264114568756770955159873910068028372795178073655730 586997102710465029138932845093011209148006191458003261363640061252611043), (19, q 490700159148056388671668730524254438192846317547935232990844883178955313 586997102710465029138932845093011209148006191458003261363640061252611043)],
  [(18, q 104020792749978191624186806267211227155485046599874308559831148146078830 646898762073131959359966677458854155492969815562689537096271103312194253), (19, q 542877969323153767735779871191642928337484768962815228536439955166115423 646898762073131959359966677458854155492969815562689537096271103312194253)],
  [(18, q 16125972704686654906404275665997138096284604762245950013389120857243470 111340229607528611374199150945496461805603335573561286518621575740427677), (19, q 95214256902841956467794875279499323709318730811315336505232454883184207 111340229607528611374199150945496461805603335573561286518621575740427677)],
  [(18, q 14749748403549891514746212312938355057338737120674524012037014258847110 104441468465286615893047201362018384757982213261168327847120182774426001), (19, q 89691720061736724378300989049080029700643476140493803835083168515578891 104441468465286615893047201362018384757982213261168327847120182774426001)],
  [(18, q 26115501291889976155827936031774028207505698973333473056731885892425710 1859435158854930369217225398402537778994669928556511209045378258870389261), (19, q 1833319657563040393061397462370763750787164229583177735988646372977963551 1859435158854930369217225398402537778994669928556511209045378258870389261)],
  [(19, q 1 1)],
  [(22, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(15, q 1 1)],
  [(18, q 4711324506397517246835516174565413365546043379474855969879128147830 47379501916624577418106409629834418223929018396975439697842752692153), (19, q 42668177410227060171270893455269004858382975017500583727963624544323 47379501916624577418106409629834418223929018396975439697842752692153)],
  [(18, q 223980698032204803998797122178209395704047849949848898971140821264790 1624426872824282377621760694928302078019241788314273868027936854109289), (19, q 1400446174792077573622963572750092682315193938364424969056796032844499 1624426872824282377621760694928302078019241788314273868027936854109289)],
  [(18, q 1418165349073912303226990819604462396039979210489334801899501337234330 10218483112389440455438574144675843085706205488841254623294128081574303), (19, q 8800317763315528152211583325071380689666226278351919821394626744339973 10218483112389440455438574144675843085706205488841254623294128081574303)],
  [(18, q 6218896858793169452341495961121450191614196565836574681024355708930 43706276539557796321457388989330935031912119730904416181571861371163), (19, q 37487379680764626869115893028209484840297923165067841500547505662233 43706276539557796321457388989330935031912119730904416181571861371163)],
  [(18, q 69392136567798723617555476188618677051346749244066286285741866976310 485939023219403841884165463888417635627992648695629950842491319157721), (19, q 416546886651605118266609987699798958576645899451563664556749452181411 485939023219403841884165463888417635627992648695629950842491319157721)],
  [(18, q 243925527641705728179706048045532120724084272157540709261987508928730 1528704718869213906454211041756377037716188070186382105816053518985343), (19, q 1284779191227508178274504993710844916992103798028841396554066010056613 1528704718869213906454211041756377037716188070186382105816053518985343)],
  [(18, q 155159249466356376250892665338730150390270025482147956010 956403307579151335316484701236317532456604003977215543991), (19, q 801244058112794959065592035897587382066333978495067587981 956403307579151335316484701236317532456604003977215543991)],
  [(18, q 368475135845956094634239219637396243641719997771356043170 1372736570675728432102274371628781919896096336429201575947), (19, q 1004261434829772337468035151991385676254376338657845532777 1372736570675728432102274371628781919896096336429201575947)],
  [(18, q 1980562223621533577063526160026355806094374869587763363296003254723310 13961281741294223653249020519307958525532127532835201510013059560865421), (19, q 11980719517672690076185494359281602719437752663247438146717056306142111 13961281741294223653249020519307958525532127532835201510013059560865421)],
  [(18, q 710855703086565762683883105899345058494275046005968522414311675829670 5128665788237707734545073093197522326566469326985999323019961138828097), (19, q 4417810085151141971861189987298177268072194280980030800605649462998427 5128665788237707734545073093197522326566469326985999323019961138828097)],
  [(18, q 54856362570370314766491304400202036630776005331904308960275592110 447397039801178606179817185415065191431978498617867174823197155501), (19, q 392540677230808291413325881014863154801202493285962865862921563391 447397039801178606179817185415065191431978498617867174823197155501)],
  [(18, q 98530985421858868810186665299807854881948579558644249848544403247390 828020422352683558744688591988675498413124335366546336162006718268949), (19, q 729489436930824689934501926688867643531175755807902086313462315021559 828020422352683558744688591988675498413124335366546336162006718268949)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(23, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 23896400978814818791049961059531983057235622132549842943139 50093535620240579212161697685950251096818970243364128627129), (20, q 26197134641425760421111736626418268039583348110814285683990 50093535620240579212161697685950251096818970243364128627129)],
  [(19, q 2262159697944865605260678041251828769119761382259394919707677 6722888129113871991656057500082344078971619550280406948826247), (20, q 4460728431169006386395379458830515309851858168021012029118570 6722888129113871991656057500082344078971619550280406948826247)],
  [(19, q 186893613721525854679229374699210053420631567165784676177667373962903067 561461698847863349308985015532119830905307377607912544672200933864101537), (20, q 374568085126337494629755640832909777484675810442127868494533559901198470 561461698847863349308985015532119830905307377607912544672200933864101537)],
  [(19, q 30450785741262810803316346175587988217268527173542166204982977569184203 96635328633519717243247726523272273874253788249581929015819003154976433), (20, q 66184542892256906439931380347684285656985261076039762810836025585792230 96635328633519717243247726523272273874253788249581929015819003154976433)],
  [(19, q 197399817874112093994952392095665939681268927452696035752245224724395073 634533893506497215738274117401719149616788019576923907808705449440654003), (20, q 437134075632385121743321725306053209935519092124227872056460224716258930 634533893506497215738274117401719149616788019576923907808705449440654003)],
  [(19, q 273727666191141378962212055861588499282747729643899964420474754536847579 1613856269939980795999758127627430428035015823228348842696789169653471969), (20, q 1340128603748839417037546071765841928752268093584448878276314415116624390 1613856269939980795999758127627430428035015823228348842696789169653471969)],
  [(19, q 2141554098675737815638686310372225515996790171905283769465930137850867 14806806653180130953095699304847166505437895501044420383814926927047337), (20, q 12665252554504393137457012994474940989441105329139136614348996789196470 14806806653180130953095699304847166505437895501044420383814926927047337)],
  [(24, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 411898570666952756543462037868591174449016215069137544007530918335111 2803394795004424093721899293931540369350203355255713908206307056483621), (20, q 2391496224337471337178437256062949194901187140186576364198776138148510 2803394795004424093721899293931540369350203355255713908206307056483621)],
  [(19, q 6089038820137843051301454663808714260864220955808418004575907577473181 32038537454126516435987342073392586917534791358373331166104838421840391), (20, q 25949498633988673384685887409583872656670570402564913161528930844367210 32038537454126516435987342073392586917534791358373331166104838421840391)],
  [(19, q 115520953489736531884809447326850175092856072050300196764762050930672161 604616790200187104030187641170875499458359052489040026015650779339161171), (20, q 489095836710450572145378193844025324365502980438739829250888728408489010 604616790200187104030187641170875499458359052489040026015650779339161171)],
  [(19, q 168089552018605466048922158308520532238513888361436871302798909078327 862017983892652139692642376036631728438454460270371538879733885113397), (20, q 693928431874046673643720217728111196199940571908934667576934976035070 862017983892652139692642376036631728438454460270371538879733885113397)],
  [(19, q 35613015374137025684927420647115753790556382418115193279218003781430071 182099139868693862340094073997474329017728197405507288079446899724592181), (20, q 146486124494556836655166653350358575227171814987392094800228895943162110 182099139868693862340094073997474329017728197405507288079446899724592181)],
  [(19, q 6463494375006433042789163098352191852190492625139537400534386069245547 30150611400953627471050254974471080735452358937112505611069156823900817), (20, q 23687117025947194428261091876118888883261866311972968210534770754655270 30150611400953627471050254974471080735452358937112505611069156823900817)],
  [(19, q 275207330306508306188934841398050342696211867121448783783136480150391 1266095681102136475301912845611764673421978501499689427954927450003701), (20, q 990888350795628169112978004213714330725766634378240644171790969853310 1266095681102136475301912845611764673421978501499689427954927450003701)],
  [(19, q 9110182921618133266035070410635685614768963075525201349863 27074454855439328867528263497139286629869185104585377242693), (20, q 17964271933821195601493193086503601015100222029060175892830 27074454855439328867528263497139286629869185104585377242693)],
  [(19, q 706788244511413510716159629953332515168287733731343405090009 3633573252440118640406316917044095935714250154945346393000699), (20, q 2926785007928705129690157287090763420545962421214002987910690 3633573252440118640406316917044095935714250154945346393000699)],
  [(19, q 57918824731008063796607417170239657595798500409174439060981803106576639 303457706274830965514718489380538353545627670815541294953988209252495629), (20, q 245538881543822901718111072210298695949829170406366855893006406145918990 303457706274830965514718489380538353545627670815541294953988209252495629)],
  [(19, q 9031689906444350493071931751381128086812006330957265643248850611251951 52229270905598095151987052919880023963863618728938115230799621340624861), (20, q 43197580999153744658915121168498895877051612397980849587550770729372910 52229270905598095151987052919880023963863618728938115230799621340624861)],
  [(19, q 57913291863840023450659916948076268216898890775603931616179536946781741 342951621227675255530048293897231518459687064245055069340265882376538551), (20, q 285038329363835232079388376949155250242788173469451137724086345429756810 342951621227675255530048293897231518459687064245055069340265882376538551)],
  [(19, q 22638116620827935963756848627727460096322249435224152354798946950065343 872253838397519586521088991230706655516687541830074482326031333531344973), (20, q 849615721776691650557332142602979195420365292394850329971232386581279630 872253838397519586521088991230706655516687541830074482326031333531344973)],
  [(19, q 5787727590470973936757144948534164171078329168085448094554863989239 8002753515420935647172532167043224729628091518842424989975045158874229), (20, q 7996965787830464673235775022094690565457013189674339541880490294884990 8002753515420935647172532167043224729628091518842424989975045158874229)],
  [(25, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 303824843776432824834073364607876624424746449719222360531567999446003 2120746945664224027397537920245120080993479784156194775377044173976233), (20, q 1816922101887791202563464555637243456568733334436972414845476174530230 2120746945664224027397537920245120080993479784156194775377044173976233)],
  [(19, q 13553231663350749884973245519895698133658718836861778606202723810494339 72710733326392325760750966013917780371748483922797797952223755909770329), (20, q 59157501663041575875777720494022082238089765085936019346021032099275990 72710733326392325760750966013917780371748483922797797952223755909770329)],
  [(19, q 85719432847131474455556900796420259747969229199427226132247229042045653 457388025903190781669938830551565983612432937120849918732727539054382383), (20, q 371668593056059307214381929755145723864463707921422692600480310012336730 457388025903190781669938830551565983612432937120849918732727539054382383)],
  [(19, q 374328978694292209042541051139258792132734831079728388851298997129513 1956330242574795064535092328885038604589303944015936956609960954628843), (20, q 1582001263880502855492551277745779812456569112936208567758661957499330 1956330242574795064535092328885038604589303944015936956609960954628843)],
  [(19, q 79313322674416646611505308641654470624635577891180122808900365351166249 413269863423576826856963239774995257911708704576126088474195412671855339), (20, q 333956540749160180245457931133340787287073126684945965665295047320689090 413269863423576826856963239774995257911708704576126088474195412671855339)],
  [(19, q 14419135665323902049336761523141330607369597211973544968688280523224693 68426128013532708522437628826323190577465144823847206229515518984887823), (20, q 54006992348208806473100867303181859970095547611873661260827238461663130 68426128013532708522437628826323190577465144823847206229515518984887823)],
  [(19, q 614096948062408317958248045732017521390751564064115172184614406660329 2873375401924205942584464246159669874691237900592355474990602139762219), (20, q 2259278453861797624626216200427652353300486336528240302805987733101890 2873375401924205942584464246159669874691237900592355474990602139762219)],
  [(19, q 20453135202928555911020978174543792805668952863448119967097 61444860576734712991104174149748302814351362314161126107867), (20, q 40991725373806157080083195975204510008682409450713006140770 61444860576734712991104174149748302814351362314161126107867)],
  [(19, q 1573915209157214596502370015132707694983193897357200033667271 8246311997180662428903967371974676683675033715133901489681381), (20, q 6672396788023447832401597356841968988691839817776701456014110 8246311997180662428903967371974676683675033715133901489681381)],
  [(19, q 42976316595013860808784069601463030909344431914780360969342542187436747 229563458157024719045829912324471747258664110683536219505487645238084017), (20, q 186587141562010858237045842723008716349319678768755858536145103050647270 229563458157024719045829912324471747258664110683536219505487645238084017)],
  [(19, q 6687847240972387804323717168097817501509086652253838436493859140051323 39511048156576776329590816875883926721759562098455318866908916869122753), (20, q 32823200915604388525267099707786109220250475446201480430415057729071430 39511048156576776329590816875883926721759562098455318866908916869122753)],
  [(19, q 42861489921668115433512405349892366069011756132117810946391741854406993 259440305919537232515686194821044461407540563055286432230677916053713123), (20, q 216578815997869117082173789471152095338528806923168621284286174199306130 259440305919537232515686194821044461407540563055286432230677916053713123)],
  [(19, q 14686403375982901023516468796303664637811845216960404089853501107257739 659853427323822958992269678687530991245571142899265314015025098517727729), (20, q 645167023947840057968753209891227326607759297682304909925171597410469990 659853427323822958992269678687530991245571142899265314015025098517727729)],
  [(20, q 139618890813559803467042802288077051196193586317170789951006344476573 158278412331953618349866435814083737891852205173325548043036898293419), (21, q 18659521518393814882823633526006686695658618856154758092030553816846 158278412331953618349866435814083737891852205173325548043036898293419)],
  [(25, q 1776492216087577863218161350543307939525 1777453271098361209180941892515503838176), (26, q 961055010783345962780541972195898651 1777453271098361209180941892515503838176)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 160974555676583659215389830768317731233031863034783085053938637141639 1285082994947055451211879234305202381104652110783873121710993309710629), (20, q 1124108439270471791996489403536884649871620247749090036657054672568990 1285082994947055451211879234305202381104652110783873121710993309710629)],
  [(19, q 7422050644376862372020600814497483510712809365402647735226704542453207 44059630565027861118089137547793099683175899892076725772719309080429077), (20, q 36637579920650998746068536733295616172463090526674078037492604537975870 44059630565027861118089137547793099683175899892076725772719309080429077)],
  [(19, q 2472063487525408883051122496274443178246419409952229460753101293553531 14587253037681591891510645432823314825757072358551338928103914998914241), (20, q 12115189550156183008459522936548871647510652948599109467350813705360710 14587253037681591891510645432823314825757072358551338928103914998914241)],
  [(19, q 205562394844656464505836513051167420091336100489826709950637321039269 1185453423555968146771869027546941750397205707734095488500846593126559), (20, q 979891028711311682266032514495774330305869607244268778550209272087290 1185453423555968146771869027546941750397205707734095488500846593126559)],
  [(19, q 43568494473725099486967983571129221065871553989848576586345725863280037 250424066339227000005011733925418362620802912511958468433214246553346207), (20, q 206855571865501900518043750354289141554931358522109891846868520690066170 250424066339227000005011733925418362620802912511958468433214246553346207)],
  [(19, q 7994616657699024183653956768184346276794042528241150290850554322892609 41463340876212025315131119028607985876781087858476674770772254189669299), (20, q 33468724218513001131477162260423639599987045330235524479921699866776690 41463340876212025315131119028607985876781087858476674770772254189669299)],
  [(19, q 340932707485845491617558816492195316080430246151872371456124007999077 1741144022232906282372501449910791050360025972424217445097414618791647), (20, q 1400211314747060790754942633418595734279595726272345073641290610792570 1741144022232906282372501449910791050360025972424217445097414618791647)],
  [(19, q 11732497362340267486414148997703094267466904922806788948661 37232987941106503242046931819321828298468321642579250302671), (20, q 25500490578766235755632782821618734031001416719772461354010 37232987941106503242046931819321828298468321642579250302671)],
  [(19, q 864086347855522941201608119879737898174647130092334197379723 4996916459208049448473387839034267413237206831633910064295153), (20, q 4132830111352526507271779719154529515062559701541575866915430 4996916459208049448473387839034267413237206831633910064295153)],
  [(19, q 23545768987251160819945505378378474955593124161080275314433122496634111 139105750896854405434598905001096175263161690125737167182123225414372621), (20, q 115559981909603244614653399622717700307568565964656891867690102917738510 139105750896854405434598905001096175263161690125737167182123225414372621)],
  [(19, q 3622402707067739412799711675598795931052705707459772256843450532994799 23942024861739527286487919985863558485889819511642040923507127720039389), (20, q 20319622154671787873688208310264762554837113804182268666663677187044590 23942024861739527286487919985863558485889819511642040923507127720039389)],
  [(19, q 23146962349174975959817640128773348751095429425794510286004213121022509 157209857603560815728006091564430847706949477250657950278573735088758199), (20, q 134062895254385839768188451435657498955854047824863439992569521967735690 157209857603560815728006091564430847706949477250657950278573735088758199)],
  [(19, q 1641310329630067625690355856170318208053071800756229265607234008457407 399843281795128124564519694452645922496677805044934948989855358744755277), (20, q 398201971465498056938829338596475604288624733244178719724248124736297870 399843281795128124564519694452645922496677805044934948989855358744755277)],
  [(20, q 15603406895292876330387246537361816244836710280213790247810095823049 95910026686991722509579718104765858685118332818055619281229773137247), (21, q 80306619791698846179192471567404042440281622537841829033419677314198 95910026686991722509579718104765858685118332818055619281229773137247)],
  [(25, q 1073619441920687911337850803933450143825 1077061540827122279057488114149238587488), (26, q 3442098906434367719637310215788443663 1077061540827122279057488114149238587488)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 639819603997093544392794527469647637068573504465769911690264866536379 5279316270322258908545915818400998682699818841293154079945748557968769), (20, q 4639496666325165364153121290931351045631245336827384168255483691432390 5279316270322258908545915818400998682699818841293154079945748557968769)],
  [(19, q 9918802499041275123254965172377627462521364299497131791359329558579609 60334553078398033928295462836220453350801842617106181435304381258026299), (20, q 50415750579356758805040497663842825888280478317609049643945051699446690 60334553078398033928295462836220453350801842617106181435304381258026299)],
  [(19, q 188336554387287168610930793359771079362822181205761208690740443564858829 1138606400890043095346229128698807301740605791599160735073835892924845719), (20, q 950269846502755926735298335339036222377783610393399526383095449359986890 1138606400890043095346229128698807301740605791599160735073835892924845719)],
  [(19, q 274908704271722185538897780452750727283072541682865217045650867026603 1623340949260657929081926007861881321735543031195347802039341823402833), (20, q 1348432244988935743543028227409130594452470489512482584993690956376230 1623340949260657929081926007861881321735543031195347802039341823402833)],
  [(19, q 58270959035451526685846713495945171868863469767913434507919237585627819 342926709300309984081548949657817094893015414140891825001320276135670609), (20, q 284655750264858457395702236161871923024151944372978390493401038550042790 342926709300309984081548949657817094893015414140891825001320276135670609)],
  [(19, q 369575429897626342983104916131662787175541474933354837051616816849627 1957904673203326775150456641694743971749006721183059612167072279017697), (20, q 1588329243305700432167351725563081184573465246249704775115455462168070 1957904673203326775150456641694743971749006721183059612167072279017697)],
  [(19, q 457211058269351940268727169873852625679323436747419269835300362616299 2384294763241401714393673330672399733743505285915245077513604788975889), (20, q 1927083704972049774124946160798547108064181849167825807678304426359590 2384294763241401714393673330672399733743505285915245077513604788975889)],
  [(19, q 15861529427478187420021307552428079535530898904101266417307 50986257905283998066319546029431779831212249805288723974177), (20, q 35124728477805810646298238477003700295681350901187457556870 50986257905283998066319546029431779831212249805288723974177)],
  [(19, q 1155507393845374517799905310228627022051630478528327722379301 6842697441401439911958234881135061089885669069434375763015711), (20, q 5687190047556065394158329570906434067834038590906048040636410 6842697441401439911958234881135061089885669069434375763015711)],
  [(19, q 94410740560925516113138603669990013642789033305524322410638737459484371 571467568159218163517733908198030215084139332113807141043107015813809481), (20, q 477056827598292647404595304528040201441350298808282818632468278354325110 571467568159218163517733908198030215084139332113807141043107015813809481)],
  [(19, q 14481768869960943061354552649320266056970328264998900073257496471195139 98357477216675028804005546738178288341917979553579899772403740536199129), (20, q 83875708346714085742650994088858022284947651288580999699146244065003990 98357477216675028804005546738178288341917979553579899772403740536199129)],
  [(19, q 92466528766428433999115718955694413920176002813878840349483589343081449 645841990256604332620458191964463126662083502202125706320853881638602539), (20, q 553375461490175898621342473008768712741907499388246865971370292295521090 645841990256604332620458191964463126662083502202125706320853881638602539)],
  [(20, q 1 1)],
  [(21, q 1 1)],
  [(25, q 1469311712123882761233753088739682947775 1474910839477532226984801896389399741856), (26, q 5599127353649465751048807649716794081 1474910839477532226984801896389399741856)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(17, q 1 1)],
  [(17, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(20, q 1 1)],
  [(19, q 1859929045369757580923753701259142828417931392089858709778799115570349 86758064694981992252864891487244426211100908398675014840169274056240439), (20, q 84898135649612234671941137785985283382682977006585156130390474940670090 86758064694981992252864891487244426211100908398675014840169274056240439)],
  [(19, q 12258316611707834865932164476371859835449916845724580868466247395212923 545752987580107852962855479531627212865381533913355421190410120377340353), (20, q 533494670968400018096923315055255353029931617067630840321943872982127430 545752987580107852962855479531627212865381533913355421190410120377340353)],
  [(19, q 61715328495653019714704715542302032785209091350797168266270289614183 2334282959135645633898503031499822335062251708481784266012837517238213), (20, q 2272567630639992614183798315957520302277042617130987097746567227624030 2334282959135645633898503031499822335062251708481784266012837517238213)],
  [(19, q 13323600633853488549269483117855181267276414648689218378859314341709159 493111428080930838684019837873743079581538724386801002234636203563921349), (20, q 479787827447077350134750354755887898314262309738111783855776889222212190 493111428080930838684019837873743079581538724386801002234636203563921349)],
  [(19, q 3759548149146500798840863695978105421203884001543692570707962649785563 81645696163957825893017763636885769517899434863006532323050699545415393), (20, q 77886148014811325094176899940907664096695550861462839752342736895629830 81645696163957825893017763636885769517899434863006532323050699545415393)],
  [(19, q 168257000526670890950286298736645809678111654878460236945383878230439 3428496421485329033398354703124595625741519361247630078232962999607429), (20, q 3260239420958658142448068404387949816063407706369169841287579121376990 3428496421485329033398354703124595625741519361247630078232962999607429)],
  [(19, q 12435141595410570971016087130827454618726533189274540322327 73315684565589814063874212325325018638753749105349738397397), (20, q 60880542970179243092858125194497564020027215916075198075070 73315684565589814063874212325325018638753749105349738397397)],
  [(19, q 255369188692513628437352853749723496687122424404869769781161 9839456116263923581960530106748084246267755796389372519960171), (20, q 9584086927571409953523177252998360749580633371984502750179010 9839456116263923581960530106748084246267755796389372519960171)],
  [(19, q 6096520869861557689800425637838687289408672695053797172881476454485477 273913911237664782940656763634323990608798828428452027185941794991902047), (20, q 267817390367803225250856337996485303319390155733398230013060318537416570 273913911237664782940656763634323990608798828428452027185941794991902047)],
  [(19, q 193522194948947384890549431391193139530022100039137659360914691043893 47144374912948199424684301168216012494129239694394318059840620840179023), (20, q 46950852717999252039793751736824819354599217594355180400479706149135130 47144374912948199424684301168216012494129239694394318059840620840179023)],
  [(20, q 1 1)],
  [(22, q 1 1)],
  [(23, q 1 1)],
  [(25, q 2067935438991388390573158870985268859275 2120847897297782842895099514780848106016), (26, q 52912458306394452321940643795579246741 2120847897297782842895099514780848106016)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(13, q 1 1)],
  [(17, q 1 1)],
  [(17, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(19, q 197207884827734953824462970330125326553490799519263620414704289809 163096527378256797439878897725731358191094130400705143488975719518499), (20, q 162899319493429062486054434755401232864540639601185879868561015228690 163096527378256797439878897725731358191094130400705143488975719518499)],
  [(19, q 61705081973163800258354213160642512759396918308538139048306897213457 34453732875774871236317317863750956490366546570132815846562043672641827), (20, q 34392027793801707436058963650590313977607149651824277707513736775428370 34453732875774871236317317863750956490366546570132815846562043672641827)],
  [(19, q 118952457626834070275920673646739855846444128701688684296743309727549 5704590982685565959003299981092599589452132934579168707476248110449639), (20, q 5585638525058731888727379307445859733605688805877480023179504800722090 5704590982685565959003299981092599589452132934579168707476248110449639)],
  [(19, q 5721948026493203388360053302428884597882621479337769198126981778897 239549304973760726452509235044668948609662255779711332325333162157667), (20, q 233827356947267523064149181742240064011779634300373563127206180378770 239549304973760726452509235044668948609662255779711332325333162157667)],
  [(19, q 740893446025572341077197938573916264479572643049539741921 5122572440590097218111575432975112140439277253184783312531), (20, q 4381678994564524877034377494401195875959704610135243570610 5122572440590097218111575432975112140439277253184783312531)],
  [(19, q 497199804279989388167330564224033690680112284980165207903 687483545031586365378072905708337592277845074229133105817133), (20, q 686986345227306375989905575144113558587164961944152940609230 687483545031586365378072905708337592277845074229133105817133)],
  [(20, q 3415520522636770049250512735160548829174680986887174832013 3871991551144075175399235473176740089961360021888314695739), (21, q 456471028507305126148722738016191260786679035001139863726 3871991551144075175399235473176740089961360021888314695739)],
  [(20, q 4670172483498209135474649730863363205044475177136292916358626494767 28706318468206171094809060701325193398879715801373858240704422666601), (21, q 24036145984707961959334410970461830193835240624237565324345796171834 28706318468206171094809060701325193398879715801373858240704422666601)],
  [(21, q 1 1)],
  [(23, q 1 1)],
  [(23, q 353699090375165224371564249962883603870039121389172799830284638521295 364129194631673525788603053074119021016319383235426784904553212347058), (24, q 10430104256508301417038803111235417146280261846253985074268573825763 364129194631673525788603053074119021016319383235426784904553212347058)],
  [(25, q 143933440583282994034220145478318093325 148183803421513867126995324102161145568), (26, q 4250362838230873092775178623843052243 148183803421513867126995324102161145568)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(19, q 1 1)],
  [(20, q 1 1)],
  [(22, q 1 1)],
  [(22, q 1 1)],
  [(23, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(25, q 1 1)],
  [(25, q 11471239755525405806418603163552999993550225546278395704280575 11477445520091725027705825011550782930213185668512010877320608), (26, q 6205764566319221287221847997782936662960122233615173040033 11477445520091725027705825011550782930213185668512010877320608)],
  [(25, q 1969114097021781953369067560907750095745943074604029713160175 1975427214328857290002475524886679377549416222612979509843872), (26, q 6313117307075336633407963978929281803473148008949796683697 1975427214328857290002475524886679377549416222612979509843872)],
  [(25, q 1845993053527761332519333891757910200289060674649718158687275 1853027605907196808204943510452926842548634173870832205653536), (26, q 7034552379435475685609618695016642259573499221114046966261 1853027605907196808204943510452926842548634173870832205653536)],
  [(25, q 32167507538101515743721945385086293355011937732371255359203775 32990580574782271479583786847140272296003032765286191455380896), (26, q 823073036680755735861841462053978940991095032914936096177121 32990580574782271479583786847140272296003032765286191455380896)],
  [(25, q 153445564184659816986348442562589662122797565575 157976820583859526860551792872177004025657295008), (26, q 4531256399199709874203350309587341902859729433 157976820583859526860551792872177004025657295008)],
  [(25, q 1308663171806063839827957834903867179825 1654924415676785891389628158930184901728), (26, q 346261243870722051561670324026317721903 1654924415676785891389628158930184901728)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 815001187190148382541069414197641611360001563255169572902325 975452769432905916791829610552492215835363362646934340636128), (26, q 160451582242757534250760196354850604475361799391764767733803 975452769432905916791829610552492215835363362646934340636128)],
  [(25, q 28172094435206716389233379136963134944507455511530885387362725 33443823335797704325947930261268370679165305528375251823978464), (26, q 5271728900590987936714551124305235734657850016844366436615739 33443823335797704325947930261268370679165305528375251823978464)],
  [(25, q 177250847536202752482188841942242725818714027930616952325131075 210378903284464443342323475861811413728915159030540492548554528), (26, q 33128055748261690860134633919568687910201131099923540223423453 210378903284464443342323475861811413728915159030540492548554528)],
  [(25, q 758696142165505377905761461788713108110542325243490410122575 899828127512518948693222306394631841577813772478805908265888), (26, q 141131985347013570787460844605918733467271447235315498143313 899828127512518948693222306394631841577813772478805908265888)],
  [(25, q 160290014770189685683738755249866842581295105451604018340592975 190086437999526070446834239608711605918276524657310302924446624), (26, q 29796423229336384763095484358844763336981419205706284583853649 190086437999526070446834239608711605918276524657310302924446624)],
  [(25, q 26633762451399215407862198838289001325124209087769374518887075 31473088389367381196850368925488491235498912924491674511393568), (26, q 4839325937968165788988170087199489910374703836722299992506493 31473088389367381196850368925488491235498912924491674511393568)],
  [(25, q 1119044155769707059262293810622398222319625503242936908504975 1321629626371805370829274999260810580460531000941149437260704), (26, q 202585470602098311566981188638412358140905497698212528755729 1321629626371805370829274999260810580460531000941149437260704)],
  [(25, q 1410714951796135633567990053568995805848773558298746461805275 1629633610547352217543028519506743699902102791017164827674656), (26, q 218918658751216583975038465937747894053329232718418365869381 1629633610547352217543028519506743699902102791017164827674656)],
  [(25, q 242331615749697671324306154075116765881803232724425845516900025 287435924576488905578896039185424149775205858018412261746374496), (26, q 45104308826791234254589885110307383893402625293986416229474471 287435924576488905578896039185424149775205858018412261746374496)],
  [(25, q 88958968598251128890889575052425229084748462515316262323728925 105589359200859199583263553266018979161106725310962277728027872), (26, q 16630390602608070692373978213593750076358262795646015404298947 105589359200859199583263553266018979161106725310962277728027872)],
  [(25, q 15259210356734502326906807174872312216227051590742377532025325 18173390005971941294574949417982911819668772469333590673396448), (26, q 2914179649237438967668142243110599603441720878591213141371123 18173390005971941294574949417982911819668772469333590673396448)],
  [(25, q 2043247498447232845661021239576782510834178892112772304289175 2435335298592263981766241453026598778644373178016205920323232), (26, q 392087800145031136105220213449816267810194285903433616034057 2435335298592263981766241453026598778644373178016205920323232)],
  [(25, q 247740563258243578849900811417770299212566530472802762928997725 303504316919444133963782041208079581598931604632474012351216864), (26, q 55763753661200555113881229790309282386365074159671249422219139 303504316919444133963782041208079581598931604632474012351216864)],
  [(25, q 1180483499908559183813615720445301698103192543925 1453343535792755646758681595621471636065068117472), (26, q 272860035884196462945065875176169937961875573547 1453343535792755646758681595621471636065068117472)],
  [(25, q 724013373009387736009731471131843694975 1171142456148014069400726786253544230304), (26, q 447129083138626333390995315121700535329 1171142456148014069400726786253544230304)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 592778722593903828112436081893951793496687800352191299221025 712876227034931424449623862690512015520120015432207829143136), (26, q 120097504441027596337187780796560222023432215080016529922111 712876227034931424449623862690512015520120015432207829143136)],
  [(25, q 6830545968223134565339346578019018535352608493414448519925275 8147090713271801189607002349142358126135007766581897395175456), (26, q 1316544745048666624267655771123339590782399273167448875250181 8147090713271801189607002349142358126135007766581897395175456)],
  [(25, q 128927748003700649448781269944274231377468213984505819750934775 153748211621117705130490672150768343698740554008947729308043936), (26, q 24820463617417055681709402206494112321272340024441909557109161 153748211621117705130490672150768343698740554008947729308043936)],
  [(25, q 183952963979561645398911350232195910110349267108879707773425 219202849733721636768181879457399840573620016590738986310752), (26, q 35249885754159991369270529225203930463270749481859278537327 219202849733721636768181879457399840573620016590738986310752)],
  [(25, q 12954612701733428509577273924053252485038158205845412990471675 15435350978419229512725078342807669347123810868002987923584032), (26, q 2480738276685801003147804418754416862085652662157574933112357 15435350978419229512725078342807669347123810868002987923584032)],
  [(25, q 2152585704448521049539323005555806194131225899711317092522975 2555669782532870162497368695398726642654306429577559784337824), (26, q 403084078084349112958045689842920448523080529866242691814849 2555669782532870162497368695398726642654306429577559784337824)],
  [(25, q 271330108070928989052036622408657763077831486387297090863025 321955906395227652792481245604999655456442211367626498360416), (26, q 50625798324298663740444623196341892378610724980329407497391 321955906395227652792481245604999655456442211367626498360416)],
  [(25, q 342098748677613672980673181630592775751573732610755205946725 396987291830198575357227026689918879632891107447158686765024), (26, q 54888543152584902376553845059326103881317374836403480818299 396987291830198575357227026689918879632891107447158686765024)],
  [(25, q 58755528503017890310136200655438837148309375985896774402131975 70020898276639897026384662199221527488535498944024577467060384), (26, q 11265369773622006716248461543782690340226122958127803064928409 70020898276639897026384662199221527488535498944024577467060384)],
  [(25, q 64706469988491721810526542701267529483738980574537726324885225 77166364544646499734394803238179118565315633918488567794624864), (26, q 12459894556154777923868260536911589081576653343950841469739639 77166364544646499734394803238179118565315633918488567794624864)],
  [(25, q 11098912787702842351897920082535754386209868149112036574172025 13281399270026585009017539009804944089732283719545308451290976), (26, q 2182486482323742657119618927269189703522415570433271877118951 13281399270026585009017539009804944089732283719545308451290976)],
  [(25, q 10403158538051648034728122332420026999337845116095177211951325 12458469395338549613057240685792147483977842315143287212248288), (26, q 2055310857286901578329118353372120484639997199048110000296963 12458469395338549613057240685792147483977842315143287212248288)],
  [(25, q 180162498724099591285844864462187752314137379921081582213270825 221805728697794514069795204328233138513736951382666293695267168), (26, q 41643229973694922783950339866045386199599571461584711481996343 221805728697794514069795204328233138513736951382666293695267168)],
  [(25, q 858445647524493879715973629920108991928568040225 1062126315950563151006710151300649443469542420064), (26, q 203680668426069271290736521380540451540974379839 1062126315950563151006710151300649443469542420064)],
  [(25, q 525387336881223285289269715101196619075 855889328136910894651973709162961436448), (26, q 330501991255687609362703994061764817373 855889328136910894651973709162961436448)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(22, q 1 1)],
  [(22, q 1 1)],
  [(24, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 211180444952963246531173018082543218159944061236599068371275 259836972392908019239390764172278654739747186813615347864096), (26, q 48656527439944772708217746089735436579803125577016279492821 259836972392908019239390764172278654739747186813615347864096)],
  [(25, q 2434047023838669019476487446791488030655174427993684343918025 2969541281453325840652018212782160445412578318125257730571616), (26, q 535494257614656821175530765990672414757403890131573386653591 2969541281453325840652018212782160445412578318125257730571616)],
  [(25, q 45943339198638391906689043312972429511471642950162095394222525 56039840162179779917886669869034130395780834112770039258652896), (26, q 10096500963541388011197626556061700884309191162607943864430371 56039840162179779917886669869034130395780834112770039258652896)],
  [(25, q 65553080096780847017985890629768657127224014649045651087675 79897466986112389405703842188208094824948416998289352125472), (26, q 14344386889331542387717951558439437697724402349243701037797 79897466986112389405703842188208094824948416998289352125472)],
  [(25, q 13849480465368648233802103441491520091792409782886853860905275 16878139769378944239728142898432943466985756879597632817818656), (26, q 3028659304010296005926039456941423375193347096710778956913381 16878139769378944239728142898432943466985756879597632817818656)],
  [(25, q 2301536393122839212838101321014137468654142099200054557638175 2794555942024042354512680531474302935080148950558119755647392), (26, q 493019548901203141674579210460165466426006851358065198009217 2794555942024042354512680531474302935080148950558119755647392)],
  [(25, q 96703410688421753757238577831917144176276109855089187633275 117350031869769788583534086507972214957173600690403651462176), (26, q 20646621181348034826295508676055070780897490835314463828901 117350031869769788583534086507972214957173600690403651462176)],
  [(25, q 122009395940296415903828826703990841408296519391293779873975 144698296949330179933008511559586411085156614705722316501664), (26, q 22688901009033764029179684855595569676860095314428536627689 144698296949330179933008511559586411085156614705722316501664)],
  [(25, q 20937933311803345916376371240763439666094170735408455767311725 25521987579959490280507633619700766490442769286476069083046624), (26, q 4584054268156144364131262378937326824348598551067613315734899 25521987579959490280507633619700766490442769286476069083046624)],
  [(25, q 23058090860129398283100832257192281124280360518488599391797475 28126445760781263829964390275271308308516014028172968078383904), (26, q 5068354900651865546863558018079027184235653509684368686586429 28126445760781263829964390275271308308516014028172968078383904)],
  [(25, q 3954663565154383948408849917762313941313099689546647666432275 4840950566999318928279881375162694643321204514977315203714336), (26, q 886287001844934979871031457400380702008104825430667537282061 4840950566999318928279881375162694643321204514977315203714336)],
  [(25, q 3706668546267941550764069654924960775708096209865054412484575 4541000029975538207606374206562765843251989508884107324567968), (26, q 834331483707596656842304551637805067543893299019052912083393 4541000029975538207606374206562765843251989508884107324567968)],
  [(25, q 64135682420555186408298615139313837211645834943466617552199075 80846192955475854929081819227225595415566386320659218465743648), (26, q 16710510534920668520783204087911758203920551377192600913544573 80846192955475854929081819227225595415566386320659218465743648)],
  [(25, q 305547119575271792742617540747317084503174502475 387135488278674754816805871367516195897766851104), (26, q 81588368703402962074188330620199111394592348629 387135488278674754816805871367516195897766851104)],
  [(25, q 185074881905037988585847749500735229825 311963961333778301685813134046363013728), (26, q 126889079428740313099965384545627783903 311963961333778301685813134046363013728)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(20, q 1 1)],
  [(22, q 1 1)],
  [(22, q 1 1)],
  [(24, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 14836214922469307168481972363394791506175911668015444579972025 19300937519250803819978933473295511490217311592269317382362976), (26, q 4464722596781496651496961109900719984041399924253872802390951 19300937519250803819978933473295511490217311592269317382362976)],
  [(25, q 1198583619679727049566651550292612318182163590893064307756225 1482070385347111840951492384730497056667378326030570852305504), (26, q 283486765667384791384840834437884738485214735137506544549279 1482070385347111840951492384730497056667378326030570852305504)],
  [(25, q 41446664774805026430180946068854533348679730953360237050653425 50813429098758343787821492846358660950644149825476316054649952), (26, q 9366764323953317357640546777504127601964418872116079003996527 50813429098758343787821492846358660950644149825476316054649952)],
  [(25, q 86924308924832962412126991682565334880545826695150973672343325 106547561648722526344813670885525109691363618194394345249465568), (26, q 19623252723889563932686679202959774810817791499243371577122243 106547561648722526344813670885525109691363618194394345249465568)],
  [(25, q 1116237308482303701659893829385652473530115007736395542039475 1367168828137073619334277298318364421835087549895354294225184), (26, q 250931519654769917674383468932711948304972542158958752185709 1367168828137073619334277298318364421835087549895354294225184)],
  [(25, q 235829016265825425553087758340166009465682755346553063425866675 288810990386546844592287589569329196910656364668706546394220832), (26, q 52981974120721419039199831229163187444973609322153482968354157 288810990386546844592287589569329196910656364668706546394220832)],
  [(25, q 39191531432935231075087901856157186623611314521750288127537975 47819160187951887219194995407631367238078789111580152165835424), (26, q 8627628755016656144107093551474180614467474589829864038297449 47819160187951887219194995407631367238078789111580152165835424)],
  [(25, q 1646712811117490957491667465557029102086947534951438504082675 2008039949265579107259192410005295157805367968783832299946272), (26, q 361327138148088149767524944448266055718420433832393795863597 2008039949265579107259192410005295157805367968783832299946272)],
  [(25, q 2077948771271652821488985858130878444694400600289856275570575 2476010924201538357917221249273976747419073827832461836514208), (26, q 398062152929885536428235391143098302724673227542605560943633 2476010924201538357917221249273976747419073827832461836514208)],
  [(25, q 356530732776542729523500627432418108900053997335139045714582325 436720551572519423966643589307482295401274590000006112633167328), (26, q 80189818795976694443142961875064186501220592664867066918585003 436720551572519423966643589307482295401274590000006112633167328)],
  [(25, q 43625651044329214549176178532361612341674294806383644666316675 53476316224020533794951203279844962014471485516470882408748832), (26, q 9850665179691319245775024747483349672797190710087237742432157 53476316224020533794951203279844962014471485516470882408748832)],
  [(25, q 7482003106384072756087122499858671820255727059285578225265075 9204014099309941306333127508953101385406370765071600505293088), (26, q 1722010992925868550246005009094429565150643705786022280028013 9204014099309941306333127508953101385406370765071600505293088)],
  [(25, q 21038318455733413674671045038067925677529929637377430322972925 25901170269603953149064152534941713164587665551044487354308832), (26, q 4862851813870539474393107496873787487057735913667057031335907 25901170269603953149064152534941713164587665551044487354308832)],
  [(25, q 363950789165702649374923948653634487685279092235420348774708425 461134330668638189708223517088042090467210572467071110311501152), (26, q 97183541502935540333299568434407602781931480231650761536792727 461134330668638189708223517088042090467210572467071110311501152)],
  [(25, q 1733826915798956508622911530815306945198286745025 2208161667721071526997912409586853683492016499296), (26, q 474334751922115018375000878771546738293729754271 2208161667721071526997912409586853683492016499296)],
  [(25, q 1047799832459434208999976732877364752675 1779394764842109665264157887832986039072), (26, q 731594932382675456264181154955621286397 1779394764842109665264157887832986039072)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(25, q 80727983956185372535321123154993337779442901140564704818472725 142957416415907094092153449036010073887484112469367211600400864), (26, q 62229432459721721556832325881016736108041211328802506781928139 142957416415907094092153449036010073887484112469367211600400864)],
  [(25, q 2672564212319281497725684612463845591369601958642802330261425 4330687014313753270404592124347191883095653557923783739032672), (26, q 1658122801994471772678907511883346291726051599280981408771247 4330687014313753270404592124347191883095653557923783739032672)],
  [(25, q 8478800685938226502343250967496205686518186531539086118808225 13710196866191207599064930965897037100958828680846217105817184), (26, q 5231396180252981096721679998400831414440642149307130987008959 13710196866191207599064930965897037100958828680846217105817184)],
  [(25, q 234078492100729693497592457847073860223897326845047908729517975 374873140402231837751143353909614658053832695315181492686718624), (26, q 140794648301502144253550896062540797829935368470133583957200649 374873140402231837751143353909614658053832695315181492686718624)],
  [(25, q 3981830409568976543120408742166757639970802315031959468605575 6364373348825183459000845797936556895307720894928459655528608), (26, q 2382542939256206915880437055769799255336918579896500186923033 6364373348825183459000845797936556895307720894928459655528608)],
  [(25, q 979576037580067382430839820870237558979017946220640864742525 1466112604972418503134820195035556174120721383565879816169696), (26, q 486536567392351120703980374165318615141703437345238951427171 1466112604972418503134820195035556174120721383565879816169696)],
  [(25, q 11318502725656818232948046565658828226545513215798877883901775 16755436547887896242436159881570120748472372565465066363149216), (26, q 5436933822231078009488113315911292521926859349666188479247441 16755436547887896242436159881570120748472372565465066363149216)],
  [(25, q 213652284850178095349364999622692151019924118181983384322281275 316201021301054262505458752458773043994368880168994440184638496), (26, q 102548736450876167156093752836080892974444761987011055862357221 316201021301054262505458752458773043994368880168994440184638496)],
  [(25, q 304912368549388589464999398348514440639591432784891892998925 450816072766495262757268002173922620480240158350424904744672), (26, q 145903704217106673292268603825408179840648725565533011745747 450816072766495262757268002173922620480240158350424904744672)],
  [(25, q 64421311857982168633686887139643998365306440199979594582176525 95233766143775060587068293886734561369192688102934277644140256), (26, q 30812454285792891953381406747090563003886247902954683061963731 95233766143775060587068293886734561369192688102934277644140256)],
  [(25, q 10717050655458496631733331564926104130020796101462161795724425 15768093563323272039606742327651674790587090172597242538378592), (26, q 5051042907864775407873410762725570660566294071135080742654167 15768093563323272039606742327651674790587090172597242538378592)],
  [(25, q 450372964612040435177675112133339991074429563569090959704525 662139646000895281308452366801111246074869483164162221655776), (26, q 211766681388854846130777254667771255000439919595071261951251 662139646000895281308452366801111246074869483164162221655776)],
  [(25, q 571945936851497890550716099447969528119765380485064511090225 816450388571589121282182366727041648581169544368514968532064), (26, q 244504451720091230731466267279072120461404163883450457441839 816450388571589121282182366727041648581169544368514968532064)],
  [(25, q 97387661158464526680835146536087824556402655535109959340990475 144006094861461709070334641218673129758472802427930905312533024), (26, q 46618433702997182389499494682585305202070146892820945971542549 144006094861461709070334641218673129758472802427930905312533024)],
  [(25, q 107226800668160202815119130691487776304119047457247701710738725 158701574618870384387365001582971188536099831624118660132878304), (26, q 51474773950710181572245870891483412231980784166870958422139579 158701574618870384387365001582971188536099831624118660132878304)],
  [(25, q 18371509323679742727345991221858734229161696708243202911153525 27314737317651232899817765142352763835720791685848247339283936), (26, q 8943227993971490172471773920494029606559094977605044428130411 27314737317651232899817765142352763835720791685848247339283936)],
  [(25, q 17215434322177956308126885976556070528860203479695007251610825 25622286627709258182327057286957961420466382131875622876732768), (26, q 8406852305531301874200171310401890891606178652180615625121943 25622286627709258182327057286957961420466382131875622876732768)],
  [(25, q 295359932127079536725539752346443150316273064976562359942900325 456169195109089251466398778786313819281608692507869068635156448), (26, q 160809262982009714740859026439870668965335627531306708692256123 456169195109089251466398778786313819281608692507869068635156448)],
  [(25, q 1404928817546797351556374188116424446426875193725 2184385901553895481209092628649588853687095265504), (26, q 779457084007098129652718440533164407260220071779 2184385901553895481209092628649588853687095265504)],
  [(25, q 765318058567084742352893538703676943575 1760235626964471606335795166574523514528), (26, q 994917568397386863982901627870846570953 1760235626964471606335795166574523514528)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(24, q 1 1)],
  [(25, q 1 1)],
  [(25, q 1 1)],
  [(25, q 289969852801108736500669349342979800856771848086825 537904200233527621103240139442667127361228995936608), (26, q 247934347432418884602570790099687326504457147849783 537904200233527621103240139442667127361228995936608)],
  [(25, q 9647084268889287510139668662866149706880459580725 16295025422947952320946425928142297808256736943584), (26, q 6647941154058664810806757265276148101376277362859 16295025422947952320946425928142297808256736943584)],
  [(25, q 30609127994751832703984906434473885298007738980325 51587197539282025136121633711529262742446278983648), (26, q 20978069544530192432136727277055377444438540003323 51587197539282025136121633711529262742446278983648)],
  [(25, q 845469633962968571321786215782233385170090730401075 1410530784848850847581650764214809431795583351511328), (26, q 565061150885882276259864548432576046625492621110253 1410530784848850847581650764214809431795583351511328)],
  [(25, q 14383469216262294272985319648147593075310256418275 23947153229375643617690583133058450659922465356576), (26, q 9563684013113349344705263484910857584612208938301 23947153229375643617690583133058450659922465356576)],
  [(25, q 3550241554605600470429444550630502870369143717425 5516524766617359680951390614043307851892420719712), (26, q 1966283212011759210521946063412804981523277002287 5516524766617359680951390614043307851892420719712)],
  [(25, q 41043017535670483977626184409347270812664890889675 63045485304758118787021603324071165644496292037152), (26, q 22002467769087634809395418914723894831831401147477 63045485304758118787021603324071165644496292037152)],
  [(25, q 774752861745849658253279761152580899103195510851175 1189765887914035543508576535058148020206175051953312), (26, q 415013026168185885255296773905567121102979541102137 1189765887914035543508576535058148020206175051953312)],
  [(25, q 1105735966672403288355551534872867505727998868225 1696280369032316498331967939892931290968993407584), (26, q 590544402359913209976416405020063785240994539359 1696280369032316498331967939892931290968993407584)],
  [(25, q 233619443553662613934248820980033392125938876615425 358334979024523386486184819450061280392393523176032), (26, q 124715535470860772551935998470027888266454646560607 358334979024523386486184819450061280392393523176032)],
  [(25, q 38873473512586409294169360978236937580788224591725 59330421394234603496779660168891425698837349081824), (26, q 20456947881648194202610299190654488118049124490099 59330421394234603496779660168891425698837349081824)],
  [(25, q 1633676237503658269256237878140876989165262431425 2491425108640892717742374801471159197161083685472), (26, q 857748871137234448486136923330282207995821254047 2491425108640892717742374801471159197161083685472)],
  [(25, q 2077548194338012440407347924594186479340061734325 3072048336528878008312454238406637989010634903008), (26, q 994500142190865567905106313812451509670573168683 3072048336528878008312454238406637989010634903008)],
  [(25, q 353165118632327120985039884946854438859300006483575 541850050366388773590479871523832616997634666388128), (26, q 188684931734061652605439986576978178138334659904553 541850050366388773590479871523832616997634666388128)],
  [(25, q 388828356037844619723870323476879858551150946088825 597144560327029983286138550130289898574333106536288), (26, q 208316204289185363562268226653410040023182160447463 597144560327029983286138550130289898574333106536288)],
  [(25, q 66604593549396275912373479284339512715758360284425 102776842921492508366250032578828572340731006448992), (26, q 36172249372096232453876553294489059624972646164567 102776842921492508366250032578828572340731006448992)],
  [(25, q 62410213590954255230140996982599532137504810852525 96408678487411276960885065608096948910129570192096), (26, q 33998464896457021730744068625497416772624759339571 96408678487411276960885065608096948910129570192096)],
  [(25, q 1068798593393198965946279300889046170063082870084025 1716422499917418620087498014343497988889840447625056), (26, q 647623906524219654141218713454451818826757577541031 1716422499917418620087498014343497988889840447625056)],
  [(25, q 1391064393644118767892906822914204446158316441975 2249690168894167569352563044352058297788174170784), (26, q 858625775250048801459656221437853851629857728809 2249690168894167569352563044352058297788174170784)],
  [(25, q 2701226782722133501967804275 6623218024521671574263574816), (26, q 3921991241799538072295770541 6623218024521671574263574816)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)]
]

/-- (C2) witness for `(1, 0) / e2`. -/
def c2w0 : List (ℕ × ℚ) := [(26, q 1 1)]

/-- (C3) witnesses: entry `a` is for `((y, 1) ∘ z_a) / e1`. -/
def c3w0 : List (List (ℕ × ℚ)) := [
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(1, q 1 1)],
  [(2, q 1 1)],
  [(3, q 1 1)],
  [(4, q 1 1)],
  [(5, q 1 1)],
  [(6, q 1 1)],
  [(7, q 1 1)]
]

/-! Certificate 1: |Z| = 10. -/

def Z1 : List (ℚ × ℚ) := [
  (q 465155055805000000000000000 868722838610126847407461303, q 128270723961750000000000000 172240157713775811986742269),
  (q 256327562635000000000000000 474935497063505975353402889, q 713255868557000000000000000 970360737791962955850362111),
  (q 702216890400000000000000 1182521262881746691178737, q 91196600301250000000000000 148116927188188159162772797),
  (q 75655174382000000000000000 121260224524873856286075463, q 2464176221860000000000000 4323794520567616224105479),
  (q 608768326083000000000000000 968027307094196301253592809, q 118721987234000000000000000 211059757861893813151942117),
  (q 101386304516750000000000000 147692142184230638087957801, q 100267138789500000000000000 210034234887996366474865091),
  (q 131007840572400000000000000 189335134812066297181765169, q 12387654064950000000000000 26290662470370907462037527),
  (q 1174304205300000000000000 1542456432560038528557853, q 274082893150000000000000000 694436553981555650158345949),
  (q 155957135089200000000000000 194975293473502275675406507, q 229553862299000000000000000 628351255078164246134644859),
  (q 50000000000000000 38999999996099961, q 0 1)
]

/-- (C1) witnesses, row-major: entry `a * 10 + b` is for `z_a ∘ z_b`. -/
def pairs1 : List (List (ℕ × ℚ)) := [
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(2, q 1 1)],
  [(2, q 1 1)],
  [(2, q 1 1)],
  [(2, q 142884929208423156946927441935872978183246321790653776419611941705 5929792186683155821238343708351816780005320302667996515148247201231), (3, q 5786907257474732664291416266415943801822073980877342738728635259526 5929792186683155821238343708351816780005320302667996515148247201231)],
  [(2, q 35434653496102496010256524834035807218717615696115963582028939565 951534934442088441937126486532977023255610155846917167858453124683), (3, q 916100280945985945926869961698941216036892540150801204276424185118 951534934442088441937126486532977023255610155846917167858453124683)],
  [(2, q 5461692983446210347615700880158686570109795900225693768935714015 33332436350215960431542016006642215174709360874196195880387657673), (3, q 27870743366769750083926315126483528604599564973970502111451943658 33332436350215960431542016006642215174709360874196195880387657673)],
  [(3, q 1 1)],
  [(5, q 1 1)],
  [(1, q 1 1)],
  [(1, q 1 1)],
  [(2, q 1 1)],
  [(2, q 1 1)],
  [(2, q 1 1)],
  [(3, q 1 1)],
  [(3, q 1 1)],
  [(3, q 1 1)],
  [(4, q 1 1)],
  [(6, q 1 1)],
  [(2, q 1 1)],
  [(2, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(6, q 1 1)],
  [(7, q 1 1)],
  [(3, q 1 1)],
  [(3, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(6, q 2705434156054304333561632708681497633036599656749292078669760051697433 5335449712258659285278373899747846537003960412768970157383395875477565), (7, q 2630015556204354951716741191066348903967360756019678078713635823780132 5335449712258659285278373899747846537003960412768970157383395875477565)],
  [(6, q 110616725672882204417770534305565312729424631394323517319 215330618059142403594994271743821074122711812859293933795), (7, q 104713892386260199177223737438255761393287181464970416476 215330618059142403594994271743821074122711812859293933795)],
  [(6, q 68996772394294183548634545686458927635445550617193053502513 119441741087538113549187141563594447834402359222153810006965), (7, q 50444968693243930000552595877135520198956808604960756504452 119441741087538113549187141563594447834402359222153810006965)],
  [(6, q 242522307024185362957631048835983993268272940453068084118101764652633 490046358315175951802823357175886274240377207959267809465423598013565), (7, q 247524051290990588845192308339902280972104267506199725347321833360932 490046358315175951802823357175886274240377207959267809465423598013565)],
  [(8, q 1 1)],
  [(4, q 1 1)],
  [(4, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(6, q 2005391123718820905579874095007736684526616392071821595608144346515391 4732577797809442382530737202212795936945412694546098627172064738677755), (7, q 2727186674090621476950863107205059252418796302474277031563920392162364 4732577797809442382530737202212795936945412694546098627172064738677755)],
  [(6, q 739913618706387986310801507282507231892474698677193557417 1718996638439857581729868000691653825449867424211004476685), (7, q 979083019733469595419066493409146593557392725533810919268 1718996638439857581729868000691653825449867424211004476685)],
  [(6, q 157296346650374880428069598433436960820449832750538508073653 317836749939092805113959191697080016367497201502231065294665), (7, q 160540403288717924685889593263643055547047368751692557221012 317836749939092805113959191697080016367497201502231065294665)],
  [(6, q 178857096000873773924045524166215388872211256403992495944212183985791 434674233726024818140209448479970656703894293954297739900909569549755), (7, q 255817137725151044216163924313755267831683037550305243956697385563964 434674233726024818140209448479970656703894293954297739900909569549755)],
  [(8, q 8755828157831764094494412719436161479625 8873026402245074163003106299980048857252), (9, q 117198244413310068508693580543887377627 8873026402245074163003106299980048857252)],
  [(5, q 1 1)],
  [(5, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 89616356447592560088701087877672700981209346129059453863153715096788 3719120893724873723197996259289512010637023228223533798763717244143815), (8, q 3629504537277281163109295171411839309655813882094474344900563529047027 3719120893724873723197996259289512010637023228223533798763717244143815)],
  [(7, q 1058302302756612326383795708000158920278751411456448346148247334804 28418834641056281866560196036309953207408414708029587875808906999895), (8, q 27360532338299669540176400328309794287129663296573139529660659665091 28418834641056281866560196036309953207408414708029587875808906999895)],
  [(7, q 13642237940166222002499826447730304078087460591668826271668 83257888054105286970438113041741571054549655166317560023215), (8, q 69615650113939064967938286594011266976462194574648733751547 83257888054105286970438113041741571054549655166317560023215)],
  [(8, q 1 1)],
  [(8, q 1128561786207031494136810824871736111625 1353759617524191163320597492546903953828), (9, q 225197831317159669183786667675167842203 1353759617524191163320597492546903953828)],
  [(6, q 1 1)],
  [(6, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 25025044911841838349981009646376633011081589897375 25360009380897646186210412549119715113711917151484), (9, q 334964469055807836229402902743082102630327254109 25360009380897646186210412549119715113711917151484)],
  [(8, q 1421547664128938071924402824197468164625 1735463078105730037881661912604652027332), (9, q 313915413976791965957259088407183862707 1735463078105730037881661912604652027332)],
  [(7, q 1 1)],
  [(7, q 1 1)],
  [(8, q 265012960463409360678616813760338473158486695875574085375 353763224318642473824966981111297167172801215615551020668), (9, q 88750263855233113146350167350958694014314519739976935293 353763224318642473824966981111297167172801215615551020668)],
  [(8, q 5737072354957443683303443435007611232327903960109691254125 7412769334523906354326735765340220060463599151794719401268), (9, q 1675696979566462671023292330332608828135695191685028147143 7412769334523906354326735765340220060463599151794719401268)],
  [(8, q 172827212418480234236300813301308271285614921580709335956125 222201385788513855510346329242302755013154829802466381103604), (9, q 49374173370033621274045515940994483727539908221757045147479 222201385788513855510346329242302755013154829802466381103604)],
  [(8, q 360182196572020423664961036123210902973482104039194977167375 438575684818688367949700840883096510911308669699972039686844), (9, q 78393488246667944284739804759885607937826565660777062519469 438575684818688367949700840883096510911308669699972039686844)],
  [(8, q 57879334293306321413591077189153360755683588618656299540875 70376848355502609801260030111366317388929940222900605381292), (9, q 12497514062196288387668952922212956633246351604244305840417 70376848355502609801260030111366317388929940222900605381292)],
  [(8, q 88373972301349433184102765507510931756517759996955081423875 106008475923905820309804633770865067239672313405545114372236), (9, q 17634503622556387125701868263354135483154553408590032948361 106008475923905820309804633770865067239672313405545114372236)],
  [(8, q 169229920412179638267025118764384032440296277875 206600373661104516376392970815380199338265042508), (9, q 37370453248924878109367852050996166897968764633 206600373661104516376392970815380199338265042508)],
  [(8, q 8972573570015955917006906338118816125 14138296048177693957803653781213556084), (9, q 5165722478161738040796747443094739959 14138296048177693957803653781213556084)],
  [(8, q 1 1)],
  [(8, q 1 1)],
  [(8, q 149627055122221691783785830360827233266749111125 229350545542553551736420048672168906712966674644), (9, q 79723490420331859952634218311341673446217563519 229350545542553551736420048672168906712966674644)],
  [(8, q 3260610007996382025797296875308951749338735367375 4805820882395709153239483487464709055154475904444), (9, q 1545210874399327127442186612155757305815740537069 4805820882395709153239483487464709055154475904444)],
  [(8, q 98321217442046865734784735069588678781887964433375 144056831088254763113293422450053929195547534516732), (9, q 45735613646207897378508687380465250413659570083357 144056831088254763113293422450053929195547534516732)],
  [(8, q 207046848404237354245289674539653884763703495717125 284335865517393959787100358227832801738971041781652), (9, q 77289017113156605541810683688178916975267546064527 284335865517393959787100358227832801738971041781652)],
  [(8, q 4754290386652493484993567598073016938188381945375 6518067717261626376172039608655504391457254673148), (9, q 1763777330609132891178472010582487453268872727773 6518067717261626376172039608655504391457254673148)],
  [(8, q 50940526446031729550900764185503160949540850106625 68727047114945722091265971925980987175304101273988), (9, q 17786520668913992540365207740477826225763251167363 68727047114945722091265971925980987175304101273988)],
  [(8, q 18958042734243321535632949669123069062545682317125 26115465977507373595228341817332617637068478050452), (9, q 7157423243264052059595392148209548574522795733327 26115465977507373595228341817332617637068478050452)],
  [(8, q 4877269798037784459425813375 9166091014511381732366184572), (9, q 4288821216473597272940371197 9166091014511381732366184572)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)],
  [(9, q 1 1)]
]

/-- (C2) witness for `(1, 0) / e2`. -/
def c2w1 : List (ℕ × ℚ) := [(9, q 1 1)]

/-- (C3) witnesses: entry `a` is for `((y, 1) ∘ z_a) / e1`. -/
def c3w1 : List (List (ℕ × ℚ)) := [
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(1, q 1 1)],
  [(2, q 1 1)]
]

/-! Certificate 2: |Z| = 28. -/

def Z2 : List (ℚ × ℚ) := [
  (q 14117395550000000000 655592414904440758503, q 215945307276800000000 208278058009172194197),
  (q 9198828385000000000 426626299750973733657, q 71697059267500000000 69159712023084028797),
  (q 214463198410000000000 9946430597615356940139, q 8419793127080000000000 8121818989677818100951),
  (q 190196319640000000000 8820971914827902808429, q 3727548541615000000000 3595631690470436830917),
  (q 82817097905000000000 3840755345645924465397, q 7828754609950000000000 7551711015014828898423),
  (q 143938722560000000000 6675291995502470800383, q 3452771178910000000000 3330586010290274732271),
  (q 83409730435000000000 3863928447423607155219, q 8436296670880000000000 8138146671976185332721),
  (q 214984929950000000000 9956614161334338583767, q 185433689044375000000 178882154118778451253),
  (q 200517666530000000000 9016356696868364330223, q 407550892640800000000 393662930070633706989),
  (q 3379266788200000000 150955251854904474813, q 2177877092350000000000 2104281961446238470501),
  (q 19615892836000000000 491150548020884945193, q 482619242950000000000 483360523310552836553),
  (q 294461934700000000000 7101446755979855324331, q 7987241344700000000000 8012758221368724177783),
  (q 3259254910000000000 78599232987343328733, q 32088779988000000000 32191352722336420283),
  (q 413843259770000000000 9980030155231996984377, q 544046426492000000000 545785705468754762781),
  (q 2175803782000000000 52412566788395106957, q 109001088965000000000 109354798600527934773),
  (q 13328585870000000000 320989685948810122311, q 1731810736085000000000 1737449317096255068273),
  (q 204089870095000000000 4772030771132796922839, q 7543555631390000000000 7577956513632204348561),
  (q 1328566113500000000 30861161108732065707, q 817637765410000000000 821608355707839164421),
  (q 766838879450000000000 9984217200711578279829, q 844328456215000000000 879450317035388301621),
  (q 474826632380000000000 5954647913434535208597, q 8474275990360000000000 8841402750805859724831),
  (q 466980435440000000 5856012687192176509, q 1502226655672000000000 1567309710313269028953),
  (q 273137129005000000000 3425153591867484640779, q 9388936781750000000 9795710669020428933),
  (q 178783602980000000000 2239477638966052236081, q 1809139208482000000000 1887610278841238972097),
  (q 413959211680000000000 5184034682851596531663, q 8507410751980000000000 8876514321702348567741),
  (q 170533486925000000000 2073455896182654410361, q 768986296255000000000 803392829222994050403),
  (q 191481085825000000000 2312907774038709222573, q 8378844335780000000000 8756314790034368520909),
  (q 421750137170000000000 2855409976104459002361, q 463910288000000000 502536055404291849),
  (q 250000000000 129999999987, q 0 1)
]

/-- (C1) witnesses, row-major: entry `a * 28 + b` is for `z_a ∘ z_b`. -/
def pairs2 : List (List (ℕ × ℚ)) := [
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(8, q 18522458996010895333312736249084399367196705106415028665031793 46679183414132876536237830873336773621648469337482554492844843), (9, q 28156724418121981202925094624252374254451764231067525827813050 46679183414132876536237830873336773621648469337482554492844843)],
  [(8, q 1685669818373830055385917745704549141974442321687195934932083 8481276893058827062091833688491454662600937301551480746161633), (9, q 6795607074684997006705915942786905520626494979864284811229550 8481276893058827062091833688491454662600937301551480746161633)],
  [(8, q 34886606269185454310737650357965231604075352125839405639 175723970073474382403424009247186037224498700296153545789), (9, q 140837363804288928092686358889220805620423348170314140150 175723970073474382403424009247186037224498700296153545789)],
  [(8, q 437062086126593910379276129845224633801125356182565275119 2202058748475013314787254678739468791409814205931804513269), (9, q 1764996662348419404407978548894244157608688849749239238150 2202058748475013314787254678739468791409814205931804513269)],
  [(8, q 1440233818319859848676607031142209664098681730014102625828163 7490929836590978769630375019395575490448578453594594456565713), (9, q 6050696018271118920953767988253365826349896723580491830737550 7490929836590978769630375019395575490448578453594594456565713)],
  [(8, q 15562848469663527886667198156544558610854661955530598477937097 81543063195164161787364026656721318333372520184262856729650547), (9, q 65980214725500633900696828500176759722517858228732258251713450 81543063195164161787364026656721318333372520184262856729650547)],
  [(8, q 2676530314998222701633316973355024326500928388243044444667 121310338067567835976910684979588698508642451427775231202617), (9, q 118633807752569613275277368006233674182141523039532186757950 121310338067567835976910684979588698508642451427775231202617)],
  [(9, q 1 1)],
  [(9, q 7194646788651078962403697584322906661201438254704459672386380 7481666903039102830215169363479195076820060442819384775300989), (10, q 287020114388023867811471779156288415618622188114925102914609 7481666903039102830215169363479195076820060442819384775300989)],
  [(10, q 21551048265979884944968027034473452725 610196313996068087542193531901573405984), (11, q 588645265730088202597225504867099953259 610196313996068087542193531901573405984)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(8, q 6037375987295644336308807757017728964626437476306614055329167 30376445551572289254953518154688809916659905955108308412412117), (9, q 24339069564276644918644710397671080952033468478801694357082950 30376445551572289254953518154688809916659905955108308412412117)],
  [(8, q 26889034380575758395620497032555489542803754454394000114447 60711034254936958461677402501679248881684856306289381654125397), (9, q 60684145220556382703281782004646693392142052551834987654010950 60711034254936958461677402501679248881684856306289381654125397)],
  [(8, q 430483538494578121115576317655851104799231168757895497 1943988234512625922719643092944361372374800625673057448947), (9, q 1943557750974131344598527516626705521270001394504299553450 1943988234512625922719643092944361372374800625673057448947)],
  [(8, q 242899185828040647383105651679128837122169511449820561 1432988171214717862855691288064967591628057801007400550411), (9, q 1432745272028889822208308182413288462790935631495950729850 1432988171214717862855691288064967591628057801007400550411)],
  [(9, q 558784067335958880364102363469634240276271316574903449428430540 558812313748774883088843186635807815066983629025441213482036637), (10, q 28246412816002724740823166173574790712312450537764053606097 558812313748774883088843186635807815066983629025441213482036637)],
  [(9, q 42578291366813266551853658447737633895902596110792036089909381820 42580945444407622424824962858058533926087435136637846947974858721), (10, q 2654077594355872971304410320900030184839025845810858065476901 42580945444407622424824962858058533926087435136637846947974858721)],
  [(9, q 63253662228353612088825299029729595780816062080962428288196020 63347005676432414110824967194087661188953603558326745293009731), (10, q 93343448078802021999668164358065408137541477364317004813711 63347005676432414110824967194087661188953603558326745293009731)],
  [(9, q 2078560489238502090284763745425534957113899836733688514287710420 2082294327311826820279922069079482624172284501332288225324605051), (10, q 3733838073324729995158323653947667058384664598599711036894631 2082294327311826820279922069079482624172284501332288225324605051)],
  [(9, q 4673596246059196217806745597492456508128380213457986146007220 4868689439120719373751803754236954475112123912852138935721091), (10, q 195093193061523155945058156744497966983743699394152789713871 4868689439120719373751803754236954475112123912852138935721091)],
  [(10, q 212374754366002748786702349292852025 4367933011545718581374252664455476887456), (11, q 4367720636791352578625465962106184035431 4367933011545718581374252664455476887456)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(8, q 140599670770664221670945824637168823991961659707683123821120909 708201082908663125987620166823375510447905819411964992268950559), (9, q 567601412137998904316674342186206686455944159704281868447829650 708201082908663125987620166823375510447905819411964992268950559)],
  [(8, q 1676133375347967413974964594180421197954551348122100873687 7569124646398633819998543584091477189374470950862749156758637), (9, q 7567448513023285852584568619497296768176516399514627055884950 7569124646398633819998543584091477189374470950862749156758637)],
  [(9, q 1 1)],
  [(9, q 3829821944674202076311032096562095759347647760916936093463540 3829823606048295731022070015781696087093371322868866264572787), (10, q 1661374093654711037919219600327745723561951930171109247 3829823606048295731022070015781696087093371322868866264572787)],
  [(9, q 13027552848551173916779995768059364414145420881351350409721732580 13028235481589907005119327496369341180839735593155091771657716599), (10, q 682633038733088339331728309976766694314711803741361935984019 13028235481589907005119327496369341180839735593155091771657716599)],
  [(9, q 992674940796240458085683786273294578181857014744650240362673673140 992738654159071344225161398306021864786853353570592153405801129667), (10, q 63713362830886139477612032727286604996338825941913043127456527 992738654159071344225161398306021864786853353570592153405801129667)],
  [(9, q 1474702791005868764467655586613036819064780838743256320304496540 1476881748488462649280423532787788931370131846743542184063408937), (10, q 2178957482593884812767946174752112305351008000285863758912397 1476881748488462649280423532787788931370131846743542184063408937)],
  [(9, q 48459786256263809452577879771567616510870468296538643509674265340 48546927422206979244593326028749307917113291430885079181179546577), (10, q 87141165943169792015446257181691406242823134346435671505281237 48546927422206979244593326028749307917113291430885079181179546577)],
  [(9, q 108960718948124570974412613168630737489055743586346897067638940 113509367884314417256190867804318067033075513444615829470887657), (10, q 4548648936189846281778254635687329544019769858268932403248717 113509367884314417256190867804318067033075513444615829470887657)],
  [(10, q 85490834651896096710481927043855425 9257696016765627024012452471501840786592), (11, q 9257610525930975127915741989574796931167 9257696016765627024012452471501840786592)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(8, q 124657956198876645680809526590277010700861695597406886048663899 628066702027332240091842269770170740102977267519380927003305049), (9, q 503408745828455594411032743179893729402115571921974040954641150 628066702027332240091842269770170740102977267519380927003305049)],
  [(8, q 19343150680866383721399569167897555753547265924741051680369 114115269754082704944425378196988358324794304323749676393631019), (9, q 114095926603401838560703978627820460769040757057824935341950650 114115269754082704944425378196988358324794304323749676393631019)],
  [(9, q 2481038367444418140046262719534559938955767413608231099326820 2481039443717134223980479628262881446299431823767674333048471), (10, q 1076272716083934216908728321507343664410159443233721651 2481039443717134223980479628262881446299431823767674333048471)],
  [(9, q 3396468394423961586134792319745609325765150650201645472032940 3396471340763822420971406263926465477311912643013114549928357), (10, q 2946339860834836613944180856151546761992811469077895417 3396471340763822420971406263926465477311912643013114549928357)],
  [(9, q 11553453957969048014474984180013283160613158425749634660205976380 11554064360577880661304914464693472716894682108185297262171415489), (10, q 610402608832646829930284680189556281523682435662601965439109 11554064360577880661304914464693472716894682108185297262171415489)],
  [(9, q 880351387320598853596335074196856745985170341483134787781714498540 880408273215185175485313714361411027230250593104070173732647502037), (10, q 56885894586321888978640164554281245080251620935385950933003497 880408273215185175485313714361411027230250593104070173732647502037)],
  [(9, q 1307836627251332776624873829977784875347721458783651792187695940 1309769599967046320738427894810997153152650728204633322091791007), (10, q 1932972715713544113554064833212277804929269420981529904095067 1309769599967046320738427894810997153152650728204633322091791007)],
  [(9, q 42976445006766441591753411492531529145011741557826023331029632740 43053744671494931538223426059779470176572585119292319526311349047), (10, q 77299664728489946470014567247941031560843561466296195281716307 43053744671494931538223426059779470176572585119292319526311349047)],
  [(9, q 96631548811926375199472844000237718898450289987270691661302340 100665553974453631121580920525626588164957715113594215223368927), (10, q 4034005162527255922108076525388869266507425126323523562066587 100665553974453631121580920525626588164957715113594215223368927)],
  [(11, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(8, q 52577901526908530685543642212426594927445727892017383928569107 273467659405958476190601064589829382040109668765014530397221057), (9, q 220889757879049945505057422377402787112663940872997146468651950 273467659405958476190601064589829382040109668765014530397221057)],
  [(9, q 39869114190687505416610000242759461617627944463193378019700392580 39871129565720303978347345113001753790090700291686743810669339599), (10, q 2015375032798561737344870242292172462755828493365790968947019 39871129565720303978347345113001753790090700291686743810669339599)],
  [(9, q 1080217271883195139233969028052459040415407580511026633664260 1080273874378488610691305624117650532612891700736364367376303), (10, q 56602495293471457336596065191492197484120225337733712043 1080273874378488610691305624117650532612891700736364367376303)],
  [(9, q 1478785604873088473911008097494049822722478204902524695153420 1478863733421867444664002187590136984083002479297434071326701), (10, q 78128548778970752994090096087161360524274394909376173281 1478863733421867444664002187590136984083002479297434071326701)],
  [(9, q 5030248874196874444751742749038353653877246042859296775544733340 5030776073805506240257912957610886217491768285838705767898831977), (10, q 527199608631795506170208572532563614522242979408992354098637 5030776073805506240257912957610886217491768285838705767898831977)],
  [(9, q 383295470448852084563213500076445642728069585064751167052716054220 383340159605087214020679763861438749182000695360088931675311158941), (10, q 44689156235129457466263784993106453931110295337764622595104721 383340159605087214020679763861438749182000695360088931675311158941)],
  [(9, q 569417844789843434371744294514690295844023642012779407982312420 570289151945010174122496542448864974905371277427370012056828151), (10, q 871307155166739750752247934174679061347635414590604074515731 570289151945010174122496542448864974905371277427370012056828151)],
  [(9, q 147334458512585636958839085377892035417355675958185194036513660 147607156583933218543785947898659225630785059044072516497965873), (10, q 272698071347581584946862520767190213429383085887322461452213 147607156583933218543785947898659225630785059044072516497965873)],
  [(9, q 42072168415580367807321847915704796321653294588006289098107620 43830971040716017101121122124358660244274887599842850270694711), (10, q 1758802625135649293799274208653863922621593011836561172587091 43830971040716017101121122124358660244274887599842850270694711)],
  [(12, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(8, q 90711357154804801819881688235793355788148607780992197586402073 475291007517790356724522043309611425746604395937416528013393123), (9, q 384579650362985554904640355073818069958455788156424330426991050 475291007517790356724522043309611425746604395937416528013393123)],
  [(9, q 9898902646072730748163108858456083245100238124511162886003456660 9899519684823657899509305593991444333067290747207049676276912523), (10, q 617038750927151346196735535361087967052622695886790273455863 9899519684823657899509305593991444333067290747207049676276912523)],
  [(9, q 268201735293631023141109187693284530351958430706286309664020 268218949422617598259070076593115114612570101494964491345131), (10, q 17214128986575117960888899830584260611670788678181681111 268218949422617598259070076593115114612570101494964491345131)],
  [(9, q 2570121890954469147840350213483630401376204605014049130297380 2570287965189222349510368293907596701543702345457886582808039), (10, q 166074234753201670018080423966300167497740443837452510659 2570287965189222349510368293907596701543702345457886582808039)],
  [(9, q 8742547054687630429590098486128557704543422824927533652445778260 8743566365066546471954488039991351902080676329092306906385783003), (10, q 1019310378916042364389553862794197537253504164773253940004743 8743566365066546471954488039991351902080676329092306906385783003)],
  [(9, q 95166512183824564906637003839046032213090567114244261797823826940 95178729504987528809577628606872492051420931728723763167830439057), (10, q 12217321162963902940624767826459838330364614479501370006612117 95178729504987528809577628606872492051420931728723763167830439057)],
  [(9, q 141377899900982833605654328234439945952172656477860532367828340 141595905288193361356380540950519844693043044826094944567654227), (10, q 218005387210527750726212716079898740870388348234412199825887 141595905288193361356380540950519844693043044826094944567654227)],
  [(9, q 4645778526210097586876546200209628147410294848264764263300693140 4654432316157312400300491308786452885046957083869703659223910667), (10, q 8653789947214813423945108576824737636662235604939395923217527 4654432316157312400300491308786452885046957083869703659223910667)],
  [(9, q 10445878775213359453075591158033929939902115373397420100378740 10882700473968000305408875237366045530952094751202523345075347), (10, q 436821698754640852333284079332115591049979377805103244696607 10882700473968000305408875237366045530952094751202523345075347)],
  [(13, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(8, q 6070056856715297441868636071375942905778241651016551991940389 275117619722098631423944662334343505614414144051794391422368039), (9, q 269047562865383333982076026262967562708635902400777839430427650 275117619722098631423944662334343505614414144051794391422368039)],
  [(9, q 40052585421357246435665543536536145215282335477765789367462629660 40111691033522472848665365332555419324534159369347408955746665673), (10, q 59105612165226412999821796019274109251823891581619588284036013 40111691033522472848665365332555419324534159369347408955746665673)],
  [(9, q 1085188252374432801668412925676311875959621824451876599845020 1086791679910445583368565476900902231796548112093155688520681), (10, q 1603427536012781700152551224590355836926287641279088675661 1086791679910445583368565476900902231796548112093155688520681)],
  [(9, q 1485590729003551052054164729004015457803488523056599228112340 1487786420947059277423638652498250869270068554884207413374427), (10, q 2195691943508225369473923494235411466580031827608185262087 1487786420947059277423638652498250869270068554884207413374427)],
  [(9, q 5053396570862242593689142958067799321083259398931674548768490180 5061129136025724314039724523226720042327499165546461184776082879), (10, q 7732565163481720350581565158920721244239766614786636007592699 5061129136025724314039724523226720042327499165546461184776082879)],
  [(9, q 385059269709709882367902287015301952172009097779988742993225233940 385653032916341532175039035473350659752227637521716350861285684907), (10, q 593763206631649807136748458048707580218539741727607868060450967 385653032916341532175039035473350659752227637521716350861285684907)],
  [(9, q 572036062072584356777612911182515997081086070552228009937905340 573729977348198555433671181148835529954612416419990404721988577), (10, q 1693915275614198656058269966319532873526345867762394784083237 573729977348198555433671181148835529954612416419990404721988577)],
  [(9, q 18797497391174284847688293424025985661048632304387945207689210140 18859213067514616147923024066800766521071023182803756768696627017), (10, q 61715676340331300234730642774780860022390878415811561007416877 18859213067514616147923024066800766521071023182803756768696627017)],
  [(9, q 42261291279947256560151974250084046382925239780265489667575740 44095424113493126814002372390724659476310856405778905125345697), (10, q 1834132833545870253850398140640613093385616625513415457769957 44095424113493126814002372390724659476310856405778905125345697)],
  [(14, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(9, q 1 1)],
  [(9, q 103174916297856770271614807066267995843457447046738902549061734380 103360255349897611889687099497792058275927231838619141880138450389), (10, q 185339052040841618072292431524062432469784791880239331076716009 103360255349897611889687099497792058275927231838619141880138450389)],
  [(9, q 2795430202815428142897059877321667040475947449348987476458860 2800456990302642754741238898543979722727922398471971788514933), (10, q 5026787487214611844179021222312682251974949122984312056073 2800456990302642754741238898543979722727922398471971788514933)],
  [(9, q 3826861544770846925865873351650561393320242181461996578471620 3833744736582701045066797841787357453278388419901969733638911), (10, q 6883191811854119200924490136796059958146238439973155167291 3833744736582701045066797841787357453278388419901969733638911)],
  [(9, q 13017480558435341497957630885774833918014142243135375371673434740 13041574323586600441583953400907262076992895454962576667878832147), (10, q 24093765151258943626322515132428158978753211827201296205397407 13041574323586600441583953400907262076992895454962576667878832147)],
  [(9, q 991907413797831631424444487191682190391849004902558958130402540420 993755060722381477930105166875301935170199661056740318167347441551), (10, q 1847646924549846505660679683619744778350656154181360036944901131 993755060722381477930105166875301935170199661056740318167347441551)],
  [(9, q 1473555882877879267430639448704483395014918437954477946514020620 1478393840614731451792281489217527104706188150751055431971694861), (10, q 4837957736852184361642040513043709691269712796577485457674241 1478393840614731451792281489217527104706188150751055431971694861)],
  [(9, q 48422048222735470329713992448689113410140252185790877396794647020 48596631758241189259918178898320634199506893736246004876905053781), (10, q 174583535505718930204186449631520789366641550455127480110406761 48596631758241189259918178898320634199506893736246004876905053781)],
  [(9, q 108861912274443674247425521547959839410461163876246191962807820 113625583432113883837507420278408358023067849018225955342339021), (10, q 4763671157670209590081898730448518612606685141979763379531201 113625583432113883837507420278408358023067849018225955342339021)],
  [(15, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(9, q 495388701629576673871516785867625270460805228644722919880684135620 515151523347599357147776908112461155608189223564775796618379298111), (10, q 19762821718022683276260122244835885147383994920052876737695162491 515151523347599357147776908112461155608189223564775796618379298111)],
  [(9, q 89848762171836772276230442821318876118146463453615407431413014220 93599381819289083328942085046112379412061982676565310631934646941), (10, q 3750619647452311052711642224793503293915519222949903200521632721 93599381819289083328942085046112379412061982676565310631934646941)],
  [(9, q 2434369896991365250453810036224272416086291429464059671435340 2535994538872758896330397173657761149931553351819254020310077), (10, q 101624641881393645876587137433488733845261922355194348874737 2535994538872758896330397173657761149931553351819254020310077)],
  [(9, q 3332580526325720830988252364948093718031854465574500826599780 3471703278812086886128109125518983342778896645071953133884759), (10, q 139122752486366055139856760570889624747042179497452307284979 3471703278812086886128109125518983342778896645071953133884759)],
  [(9, q 11336088602813342265261945827821168965564534243915952728303463060 11809987219030493390110365417139817236886062098253759673177410443), (10, q 473898616217151124848419589318648271321527854337806944873947383 11809987219030493390110365417139817236886062098253759673177410443)],
  [(9, q 863787799354970545179597622329346123730261381654449795072773266980 899909341830947130587009544518583605215708412941505790112695842919), (10, q 36121542475976585407411922189237481485447031287055995039922575939 899909341830947130587009544518583605215708412941505790112695842919)],
  [(9, q 1283094933086248414907563362283349225176545224767399546393580780 1338781034340009814087743077639879054637710036931291983891100309), (10, q 55686101253761399180179715356529829461164812163892437497519529 1338781034340009814087743077639879054637710036931291983891100309)],
  [(9, q 42162408220431096810682099122832087603037482639590014834192562380 44007386356321658242155282836412787232168521584965854556657493789), (10, q 1844978135890561431473183713580699629131038945375839722464931409 44007386356321658242155282836412787232168521584965854556657493789)],
  [(9, q 94519114724837870941767395281297989109163130206043693724377580 102895298895103304296580985534370433079165619448305790122091349), (10, q 8376184170265433354813590253072443970002489242262096397713769 102895298895103304296580985534370433079165619448305790122091349)],
  [(16, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(9, q 1633460402213630024798167184467251784173056247545911180 1714056599407865810268225967620821675792852011274280429), (10, q 80596197194235785470058783153569891619795763728369249 1714056599407865810268225967620821675792852011274280429)],
  [(9, q 296252793171575948876529394699784780525591393921836580 311431939607398820544972662982450596792906863494557799), (10, q 15179146435822871668443268282665816267315469572721219 311431939607398820544972662982450596792906863494557799)],
  [(9, q 8026697770528145060686129893265123176244084932260 8437979853325840798071857581836028836951508901703), (10, q 411282082797695737385727688570905660707423969443 8437979853325840798071857581836028836951508901703)],
  [(9, q 86522143455417227930582890791022099233332413460 90955517420755920140845713893636064928464751563), (10, q 4433373965338692210262823102613965695132338103 90955517420755920140845713893636064928464751563)],
  [(9, q 37377752851755936890219638224442460142296189145145340 39295208524585447768846202706102072153067045789010577), (10, q 1917455672829510878626564481659612010770856643865237 39295208524585447768846202706102072153067045789010577)],
  [(9, q 2848111157877999394995097386207293847136443556506850220 2994256012698078462881465338187338557782326576775712741), (10, q 146144854820079067886367951980044710645883020268862521 2994256012698078462881465338187338557782326576775712741)],
  [(9, q 4230563925847829579329319707861178536938994929868420 4454507776975354886446244271366448530621961898559951), (10, q 223943851127525307116924563505269993682966968691531 4454507776975354886446244271366448530621961898559951)],
  [(9, q 139015274421558709787693012696952576972960852589110820 146425173154049892835117065201590202433384406694493671), (10, q 7409898732491183047424052504637625460423554105382851 146425173154049892835117065201590202433384406694493671)],
  [(9, q 311431004682501044297811605279416030722486589023620 342362117019678985177162933557873362996943785834511), (10, q 30931112337177940879351328278457332274457196810891 342362117019678985177162933557873362996943785834511)],
  [(17, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 86592656695745987599623962174280904107504508282975 2451784214054933218163898866366589158592507438382944), (11, q 2365191557359187230564274904192308254485002930099969 2451784214054933218163898866366589158592507438382944)],
  [(10, q 238253803276260426276116641794691551061872106975 4900190022314780759195204735833557706133756473175904), (11, q 4899951768511504498768928619191763014582694601068929 4900190022314780759195204735833557706133756473175904)],
  [(10, q 111458247739229796594593253349761995623325 12069674834567729200790580629518684162931723808), (11, q 12069563376319989970993986036265334400936100483 12069674834567729200790580629518684162931723808)],
  [(11, q 1 1)],
  [(12, q 1 1)],
  [(13, q 1 1)],
  [(14, q 1 1)],
  [(15, q 1 1)],
  [(16, q 1 1)],
  [(18, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(16, q 1255736501918870148281736564956503220078115655390436148880775027 6326802615931057938051839148145984330392316582664079159905996557), (17, q 5071066114012187789770102583189481110314200927273643011025221530 6326802615931057938051839148145984330392316582664079159905996557)],
  [(16, q 194852387338461544001698982240491556044078235819963145489337 1149535208389999029141952778428064649426764221547943924428621767), (17, q 1149340356002660567597951079445824157870720143312123961283132430 1149535208389999029141952778428064649426764221547943924428621767)],
  [(17, q 913103449402164781399911015487409181920561929645834363268918300 913103845505805596176659228065959884623934337244452359936509157), (18, q 396103640814776748212578550702703372407598617996667590857 913103845505805596176659228065959884623934337244452359936509157)],
  [(17, q 673083227261173292510323889729032265100293529696037840638427900 673083811141755309443338476579750451244387374315126992099296141), (18, q 583880582016933014586850718186144093844619089151460868241 673083811141755309443338476579750451244387374315126992099296141)],
  [(17, q 2289565269857916743568263704442726318232747693981161069287139348300 2289686234256866823395982424367797971214604228209491176261185918857), (18, q 120964398950079827718719925071652981856534228330106974046570557 2289686234256866823395982424367797971214604228209491176261185918857)],
  [(17, q 24922936082431915507112888257217887204535811604837378762096695817700 24924546534275570323627138786790222940441143435057276122975340336283), (18, q 1610451843654816514250529572335735905331830219897360878644518583 24924546534275570323627138786790222940441143435057276122975340336283)],
  [(17, q 37025134664072591859425721587224530633483511606396099502730054700 37079857535117811040439398694026573642370900200393723801830126513), (18, q 54722871045219181013677106802043008887388593997624299100071813 37079857535117811040439398694026573642370900200393723801830126513)],
  [(17, q 1216672350814080687750935262798381092037393477223649056529298738700 1218860720856962620468602261431130243973630002035945248162648062873), (18, q 2188370042881932717666998632749151936236524812296191633349324173 1218860720856962620468602261431130243973630002035945248162648062873)],
  [(17, q 2735659816378515349482358401867010324899946949170479371530086700 2849863365404393771534048800075229744032278040542807870583399793), (18, q 114203549025878422051690398208219419132331091372328499053313093 2849863365404393771534048800075229744032278040542807870583399793)],
  [(19, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(16, q 40390040453296663293914346107658915014250101556813297864985983 210076277396189681473280366368808685152103963065227918993988353), (17, q 169686236942893018179366020261149770137853861508414621129002370 210076277396189681473280366368808685152103963065227918993988353)],
  [(17, q 28691351480335566716513782185494619229415393490515172006040922900 28692801821899575962572968279523154305935869307586392763027072191), (18, q 1450341564009246059186094028535076520475817071220756986149291 28692801821899575962572968279523154305935869307586392763027072191)],
  [(17, q 10105757869824940131995125831643571707583712473008548520736900 10106287403213412135219851174984212626296483553728834227871251), (18, q 529533388472003224725343340640918712771080720285707134351 10106287403213412135219851174984212626296483553728834227871251)],
  [(17, q 22348013661940812273256915155170974000178726538549039114949100 22349194372565634492182177482906437818238587466583803775074689), (18, q 1180710624822218925262327735463818059860928034764660125589 22349194372565634492182177482906437818238587466583803775074689)],
  [(17, q 25339727001458932614049191377973339749442146111290776551774226900 25342382753588128910524925777332551090243747434379768233055238351), (18, q 2655752129196296475734399359211340801601323088991681281011451 25342382753588128910524925777332551090243747434379768233055238351)],
  [(17, q 275834196136649912840368906498800886334831459368462352330282911100 275866356176192597279883496452797250398428082556305074220073282669), (18, q 32160039542684439514589953996364063596623187842721889790371569 275866356176192597279883496452797250398428082556305074220073282669)],
  [(17, q 409775031516917678128360628067518202402638280299199077832602100 410402057733669271675269413022609643574501803157705419987987559), (18, q 627026216751593546908784955091441171863522858506342155385459 410402057733669271675269413022609643574501803157705419987987559)],
  [(17, q 13465499601889463340950085976604515647445973679888450377016014100 13490422595520676097311786295302089539346464062924549837445951039), (18, q 24922993631212756361700318697573891900490383036099460429936939 13490422595520676097311786295302089539346464062924549837445951039)],
  [(17, q 90830262677361501816374162038590455317582619667835499821934300 94627369183988449545155393158902570616456855138056097401015797), (18, q 3797106506626947728781231120312115298874235470220597579081497 94627369183988449545155393158902570616456855138056097401015797)],
  [(20, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(16, q 1696959083457484187618172426750580910765180504780337679845728209 8891382708745011503311005036876404714995464221196470142938316719), (17, q 7194423625287527315692832610125823804230283716416132463092588510 8891382708745011503311005036876404714995464221196470142938316719)],
  [(17, q 3643002202184937322196331527756271388570071146529543298996438020100 3643229285287866694556610445489619871773629935577166007799472569779), (18, q 227083102929372360278917733348483203558789047622708803034549679 3643229285287866694556610445489619871773629935577166007799472569779)],
  [(17, q 1283149669625049502126331222111481150026039131275649652429586100 1283232026675789204350778650765477281719710587680200455189980919), (18, q 82357050739702224447428653996131693671456404550802760394819 1283232026675789204350778650765477281719710587680200455189980919)],
  [(17, q 945858348485272441400596302641718032787213442408325686749449300 945919467260207903355670788815467709422936579670528488609337647), (18, q 61118774935461955074486173749676635723137262202801859888347 945919467260207903355670788815467709422936579670528488609337647)],
  [(17, q 3217439277026148515643368868936667542621523131822167389444674396100 3217814404460761550539601739702934941676402617353999491285697970819), (18, q 375127434613034896232870766267399054879485531832101841023574719 3217814404460761550539601739702934941676402617353999491285697970819)],
  [(17, q 35023257208967331322990668364905295994621476957150121887902282925900 35027753437437583355859631407627887542140168416298661900061108871561), (18, q 4496228470252032868963042722591547518691459148540012158825945661 35027753437437583355859631407627887542140168416298661900061108871561)],
  [(17, q 52030009698488948389715055333561437598271704898844915159300204900 52110240218385140093935850996525805188792666587483483445288902971), (18, q 80230519896191704220795662964367590520961688638568285988698071 52110240218385140093935850996525805188792666587483483445288902971)],
  [(17, q 1709743191439659215703029527869454415797619863933991078679970832900 1712927966253810885282008204937060068938866968764919606284323191091), (18, q 3184774814151669578978677067605653141247104830928527604352358191 1712927966253810885282008204937060068938866968764919606284323191091)],
  [(17, q 3844300802064839838905511878716013122802734501789254610444748900 4005060278889947641032109725313989726915435569527712525130308731), (18, q 160759476825107802126597846597976604112701067738457914685559831 4005060278889947641032109725313989726915435569527712525130308731)],
  [(21, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(16, q 1030260935070076293412600071984836743369526184452955595064069 46695268733128006536963382421743306240143472233793848194617979), (17, q 45665007798057930243550782349758469496773946049340892599553910 46695268733128006536963382421743306240143472233793848194617979)],
  [(17, q 210156268523043558002707610032972149661662090565795773398661315100 210466396190726996521047493826332623341127412706936474802999977829), (18, q 310127667683438518339883793360473679465322141140701404338662729 210466396190726996521047493826332623341127412706936474802999977829)],
  [(17, q 6729263650280644277284839056302687197461440028998556044780100 6739206521123877065763718374561057495401832944888412026350179), (18, q 9942870843232788478879318258370297940392915889855981570079 6739206521123877065763718374561057495401832944888412026350179)],
  [(17, q 4960395771816690073092244136761244549245197271231983525171300 4967727199524305219113192971055022920434178902197151630316027), (18, q 7331427707615146020948834293778371188981630965168105144727 4967727199524305219113192971055022920434178902197151630316027)],
  [(17, q 16873319477586825169068152166701674517505296622657034464076990100 16899138556013605709087391582149662058790403836579411128882186079), (18, q 25819078426780540019239415447987541285107213922376664805195979 16899138556013605709087391582149662058790403836579411128882186079)],
  [(17, q 183673580008714474732476121274108829638208807571753738302208211900 183956805533766065274184775521967232768366634127776975572161001501), (18, q 283225525051590541708654247858403130157826556023237269952789601 183956805533766065274184775521967232768366634127776975572161001501)],
  [(17, q 272861659697655962650640937027489971513434575094564515349150900 273669658640618951476631881415014073270632936123769722151464311), (18, q 807998942962988825990944387524101757198361029205206802313411 273669658640618951476631881415014073270632936123769722151464311)],
  [(17, q 8966421308709994467893795765549364183412026141150096991434898900 8995859735746524967298531500608928240245998693464272365353377231), (18, q 29438427036530499404735735059564056833972552314175373918478331 8995859735746524967298531500608928240245998693464272365353377231)],
  [(17, q 20158669783565637167508264041885808834451189424266150595454900 21033552613948789580550239723429409988328838545136461641900471), (18, q 874882830383152413041975681543601153877649120870311046445571 21033552613948789580550239723429409988328838545136461641900471)],
  [(22, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(17, q 1 1)],
  [(17, q 1286645677734750301029585483336820880895305698279080285218118137300 1288956953563997427225935913617244558375557745720845859311919433167), (18, q 2311275829247126196350430280423677480252047441765574093801295867 1288956953563997427225935913617244558375557745720845859311919433167)],
  [(17, q 41198761481923819051726246658993833339821227401708552061332300 41272845756500776250654504861307181161960412995923817759662217), (18, q 74084274576957198928258202313347822139185594215265698329917 41272845756500776250654504861307181161960412995923817759662217)],
  [(17, q 30369171551153948626877361514555454991959471749560876124009900 30423795119450887534832777657827025642409324117912687045603921), (18, q 54623568296938907955416143271570650449852368351810921594021 30423795119450887534832777657827025642409324117912687045603921)],
  [(17, q 103303998751438136555354872457995535868709213356646307185561162300 103495201824408390168594575557088730966806089225247454231214897917), (18, q 191203072970253613239703099093195098096875868601147045653735617 103495201824408390168594575557088730966806089225247454231214897917)],
  [(17, q 1124509920954097960539461540781595769907350595310111836483866283700 1126604569374076730846630958707458119626839070360982604678328178423), (18, q 2094648419978770307169417925862349719488475050870768194461894723 1126604569374076730846630958707458119626839070360982604678328178423)],
  [(17, q 1670547257058995891818773647605613484947951198366040664079980700 1676031974076501811831424940736727847050247438282440703168682053), (18, q 5484717017505920012651293131114362102296239916400039088701353 1676031974076501811831424940736727847050247438282440703168682053)],
  [(17, q 54895318718206375241812261001364292395672481877627315687389384700 55093241341810686486507854850739751415681755207213605888299867213), (18, q 197922623604311244695593849375459020009273329586290200910482513 55093241341810686486507854850739751415681755207213605888299867213)],
  [(17, q 123415047275367195080711375166794924472882062981068107490572700 128815546759943969092015988426960843701662847642235660076137733), (18, q 5400499484576774011304613260165919228780784661167552585565033 128815546759943969092015988426960843701662847642235660076137733)],
  [(23, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(17, q 27703729463285096324734903586376067693057982346384322100 28808930014904924064646761344864670468240015932660926359), (18, q 1105200551619827739911857758488602775182033586276604259 28808930014904924064646761344864670468240015932660926359)],
  [(17, q 1672233825705763803315804735982298642734374499144720146943246000700 1742039050510433982878879200347966798755379648274597936574934617853), (18, q 69805224804670179563074464365668156021005149129877789631688617153 1742039050510433982878879200347966798755379648274597936574934617853)],
  [(17, q 588999365591290721946074418512890975453816211560799451474562700 613587596685735436660140996019337362887061427633767303192099833), (18, q 24588231094444714714066577506446387433245216072967851717537133 613587596685735436660140996019337362887061427633767303192099833)],
  [(17, q 434173785349032349005118095456084106087732315189818077861125100 452298914388833566505502877993903735992075639058727199510417729), (18, q 18125129039801217500384782537819629904343323868909121649292629 452298914388833566505502877993903735992075639058727199510417729)],
  [(17, q 1476883292348219297033506812730892201827490343848543808528054232700 1538623542718559412052787291898895733634587617801670560084954169133), (18, q 61740250370340115019280479168003531807097273953126751556899936433 1538623542718559412052787291898895733634587617801670560084954169133)],
  [(17, q 16076517265210490643626345741494457968384096352201847182922156221300 16748798815950980282309259649100960983927936064254676982799744795527), (18, q 672281550740489638682913907606503015543839712052829799877588574227 16748798815950980282309259649100960983927936064254676982799744795527)],
  [(17, q 23880515399810934673899398728593443653650386607093485021406574300 24916925695148370659967224417773649455520029100502115394653841397), (18, q 1036410295337435986067825689180205801869642493408630373247267097 24916925695148370659967224417773649455520029100502115394653841397)],
  [(17, q 784712037151688902459766301708780336700637941873418063571461770300 819050126758568851647150070072123463045242599803422405562700090237), (18, q 34338089606879949187383768363343126344604657930004341991238319937 819050126758568851647150070072123463045242599803422405562700090237)],
  [(17, q 1759156798580594775353708886387286293836048657882194212576782300 1915051417062601590177255122067141664454950230437753724516417717), (18, q 155894618482006814823546235679855370618901572555559511939635417 1915051417062601590177255122067141664454950230437753724516417717)],
  [(24, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(17, q 5230156211027893521449243740344454172295100 5488216155896720379535735618125317381872029), (18, q 258059944868826858086491877780863209576929 5488216155896720379535735618125317381872029)],
  [(17, q 3472593546622757357196311871983213269563752529742708700 3650519315328514474584975004131806600002620657188629173), (18, q 177925768705757117388663132148593330438868127445920473 3650519315328514474584975004131806600002620657188629173)],
  [(17, q 111193417419848828898008332478920750022430058413700 116890886244169582167543443030881212192902100831123), (18, q 5697468824320753269535110551960462170472042417423 116890886244169582167543443030881212192902100831123)],
  [(17, q 81964887252462824128317259175483662558215906488100 86164748498436594210806868945071932340291725411499), (18, q 4199861245973770082489609769588269782075818923399 86164748498436594210806868945071932340291725411499)],
  [(17, q 278811089203704662248175092140576851080505007585183700 293113926154918098628275369197553689169016751233209423), (18, q 14302836951213436380100277056976838088511743648025723 293113926154918098628275369197553689169016751233209423)],
  [(17, q 3034979417724813184573695642836014799123677155398290300 3190713025648946196373364948190263328667243448334221037), (18, q 155733607924133011799669305354248529543566292935930737 3190713025648946196373364948190263328667243448334221037)],
  [(17, q 4508136701337006231865524943257869993637798267533300 4746773798424346375467868727780847508244025113900007), (18, q 238637097087340143602343784522977514606226846366707 4746773798424346375467868727780847508244025113900007)],
  [(17, q 148136246526677903226489489000644407442648464734209300 156032318306857784750107539508838157229669753622938047), (18, q 7896071780179881523618050508193749787021288888728747 156032318306857784750107539508838157229669753622938047)],
  [(17, q 331864396036061683798046273278230067411341692781300 364824938692904954087887570610167327320509044517927), (18, q 32960542656843270289841297331937259909167351736627 364824938692904954087887570610167327320509044517927)],
  [(25, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 54120417011653413362833300661253713527068894725282318 1532365320000234263241671258402964477197615038900951833), (19, q 1478244902988580849878837957741710763670546144175669515 1532365320000234263241671258402964477197615038900951833)],
  [(18, q 68201259353280958905503222183342390458 1402702185680707028616949937239047051985923), (19, q 1402633984421353747658044434016863709595465 1402702185680707028616949937239047051985923)],
  [(18, q 905598372787121282237730682079475866478991138 98066119948041194188530752537139150929412929575503), (19, q 98065214349668407067248514806457071453546450584365 98066119948041194188530752537139150929412929575503)],
  [(19, q 1 1)],
  [(20, q 1 1)],
  [(21, q 1 1)],
  [(22, q 1 1)],
  [(23, q 1 1)],
  [(24, q 1 1)],
  [(26, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(24, q 1079001051666086273659839292101040306203180115462662563454714451 5436352822300603141817228781554714425128006598634982703261256784), (25, q 4357351770634516868157389489453674118924826483172320139806542333 5436352822300603141817228781554714425128006598634982703261256784)],
  [(24, q 167428382123657141463042602268843409766819931067455889723481 987746789939207500369687147514915947291799245249683481545752304), (25, q 987579361557083843228224104912647103882032425318616025656028823 987746789939207500369687147514915947291799245249683481545752304)],
  [(25, q 286902090899771300143177765380032017000711816149553663128951274 286902215357698581666456568416084154856023458677316027134971569), (26, q 124457927281523278803036052137855311642527762364006020295 286902215357698581666456568416084154856023458677316027134971569)],
  [(25, q 211486426184492674734420403997969378184910414728495131696008762 211486609642960479682927173695371700965382871760081021059911097), (26, q 183458467804948506769697402322780472457031585889363902335 211486609642960479682927173695371700965382871760081021059911097)],
  [(25, q 16730090993238357615436010891594317779318726180991491723848311318 16730974892652806078376901493067276154683212913241492625279170383), (26, q 883899414448462940890601472958375364486732250000901430859065 16730974892652806078376901493067276154683212913241492625279170383)],
  [(25, q 7830922638713798301449392757498983792818078999099549972417617942806 7831428651478878672612111740361588240315143506922484163900454728911), (26, q 506012765080371162718982862604447497064507822934191482836786105 7831428651478878672612111740361588240315143506922484163900454728911)],
  [(25, q 11633499531649939348029217743545536670723787801532416320575697666 11650693756612279538396288088650389800026142925000069576519663821), (26, q 17194224962340190367070345104853129302355123467653255943966155 11650693756612279538396288088650389800026142925000069576519663821)],
  [(25, q 4958499884585597278780328648933326509078689876327597554 4967418499854366114784502150608467013301079679198987749), (26, q 8918615268768836004173501675140504222389802871390195 4967418499854366114784502150608467013301079679198987749)],
  [(25, q 3010283156422824578691354421173919589070645950801134 3135951201103691744573719331911338199855255033163979), (26, q 125668044680867165882364910737418610784609082362845 3135951201103691744573719331911338199855255033163979)],
  [(26, q 39117840886893374835705958737562075 39242616998200081996423185630336438), (27, q 124776111306707160717226892774363 39242616998200081996423185630336438)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(24, q 1027899918018559414379411767245016582356427612005390862757547 5346302848170121693299759701613434463747186563367385653015248), (25, q 4318402930151562278920347934368417881390758951361994790257701 5346302848170121693299759701613434463747186563367385653015248)],
  [(25, q 801012298744467202770252426412909941267187432669749565079984098 801052789741586803170771655919271156033252645043283175293426813), (26, q 40490997119600400519229506361214766065212373533610213442715 801052789741586803170771655919271156033252645043283175293426813)],
  [(25, q 846405197825361237571327078013220314642767709228457160748334 846449548760560426330608012956375106849876330954665709507179), (26, q 44350935199188759280934943154792207108621726208548758845 846449548760560426330608012956375106849876330954665709507179)],
  [(25, q 1871752239485088467466939513192148649790144867681728484145626 1871851129605240454688285629217167823517694059855359165371081), (26, q 98890120151987221346116025019173727549192173630681225455 1871851129605240454688285629217167823517694059855359165371081)],
  [(25, q 49356335687786469632308180506406376942854408041948916432086738 49361508521478971628736849987691418878954277942578638543605653), (26, q 5172833692501996428669481285041936099869900629722111518915 49361508521478971628736849987691418878954277942578638543605653)],
  [(25, q 1100115401232031304509205995149564162277264590043770945690652426 1100243665802924314304305526813832870594903965783562419876346881), (26, q 128264570893009795099531664268708317639375739791474185694455 1100243665802924314304305526813832870594903965783562419876346881)],
  [(25, q 34320604261714663849208837513175475040444625999042235216129206 34373120684121334235573721547334984440264419698867213043977311), (26, q 52516422406670386364884034159509399819793699824977827848105 34373120684121334235573721547334984440264419698867213043977311)],
  [(25, q 14628333181123361113603098756966335006254485382007814 14655408437555525264388119976546570376675739585347559), (26, q 27075256432164150785021219580235370421254203339745 14655408437555525264388119976546570376675739585347559)],
  [(25, q 20928742142142669949613055749135226254155065534 21803656081847194366188641661953417555169855379), (26, q 874913939704524416575585912818191301014789845 21803656081847194366188641661953417555169855379)],
  [(26, q 38469741136851577154237006556275 38592586221867053984122924294886), (27, q 122845085015476829885917738611 38592586221867053984122924294886)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(24, q 596806666110001794592514451152060544823804276003349815001810957 3127026764076461539842202563215102867791730163469987955990240688), (25, q 2530220097966459745249688112063042322967925887466638140988429731 3127026764076461539842202563215102867791730163469987955990240688)],
  [(25, q 468502711575856400120691336451942609684804705886953869227644125038 468531915250070933571516094921125461926125437503048351093002664203), (26, q 29203674214533450824758469182852241320731616094481865358539165 468531915250070933571516094921125461926125437503048351093002664203)],
  [(25, q 12693653501508836058463433835517277668988819280493118960631086 12694468224756047838504183728059170031971142339640277332522091), (26, q 814723247211780040749892541892362982323059147158371891005 12694468224756047838504183728059170031971142339640277332522091)],
  [(25, q 121640662409216838452075306666716082806576809343589591905708934 121648522495540221935307613576641396938428596092288524967058279), (26, q 7860086323383483232306909925314131851786748698933061349345 121648522495540221935307613576641396938428596092288524967058279)],
  [(25, q 506455133656467122732082614013664855521526464337231761264553454 506514182234754735985495305569489938198699942388002080458221899), (26, q 59048578287613253412691555825082677173478050770319193668445 506514182234754735985495305569489938198699942388002080458221899)],
  [(25, q 643444612043905201465060681671729935008046396672818457589453891206 643527216410667550991037507467152920452687008401305487310611574311), (26, q 82604366762349525976825795422985444640611728487029721157683105 643527216410667550991037507467152920452687008401305487310611574311)],
  [(25, q 6691239607936618828827548738626965512536587521632259591292550462 6701557530912334303164201613999237286551735134692686193045582547), (26, q 10317922975715474336652875372271774015147613060426601753032085 6701557530912334303164201613999237286551735134692686193045582547)],
  [(25, q 2851980139199604559654488519228821784185990136145472078 2857292582941600379299670331409299024746201634573664443), (26, q 5312443741995819645181812180477240560211498428192365 2857292582941600379299670331409299024746201634573664443)],
  [(25, q 1731416551054961843557018902296432210656499053181138 1803820255459264973757005676699314442482995518652053), (26, q 72403704404303130199986774402882231826496465470915 1803820255459264973757005676699314442482995518652053)],
  [(26, q 22500748134507646449858755053019525 22572617645858186238513795199667466), (27, q 71869511350539788655040146647941 22572617645858186238513795199667466)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(24, q 1049069294648346865229017483598957151185183992949890185774661 47547733749469326558793635841737036154442265798469947012773424), (25, q 46498664454820979693564618358138079003257081805520056826998763 47547733749469326558793635841737036154442265798469947012773424)],
  [(25, q 7113723601920980547327681638729943049583490064200368396803670974 7124221325946595269222033874894026723732234594796588147667936019), (26, q 10497724025614721894352236164083674148744530596219750864265045 7124221325946595269222033874894026723732234594796588147667936019)],
  [(25, q 2505618042605831191645641383603717812132353087353912625555814 2509320236170361689062819933481932788854476991544771356985559), (26, q 3702193564530497417178549878214976722123904190858731429745 2509320236170361689062819933481932788854476991544771356985559)],
  [(25, q 1846986206850615837612768385179960527693363264496295297829782 1849716038596989846027295841108413531090075728685888355389967), (26, q 2729831746374008414527455928453003396712464189593057560185 1849716038596989846027295841108413531090075728685888355389967)],
  [(25, q 6282722140026529796904718119344045859229169250562605446563125214 6292335784566506237130209320316765159311859183500135390088319459), (26, q 9613644539976440225491200972719300082689932937529943525194245 6292335784566506237130209320316765159311859183500135390088319459)],
  [(25, q 3599485376872881137749618844606963780088089222515338288096849214 3605035800269276843288524148482745669042846662585401784860213459), (26, q 5550423396395705538905303875781888954757440070063496763364245 3605035800269276843288524148482745669042846662585401784860213459)],
  [(25, q 101599095117235590174324015663023766448952575057316149471840526 101899950728653021627580219251051680660885104683598864870776731), (26, q 300855611417431453256203588027914211932529626282715398936205 101899950728653021627580219251051680660885104683598864870776731)],
  [(25, q 1862077958225315947122171384244081549901725152303618442 1868191506119423174407343597076343819084817503129050177), (26, q 6113547894107227285172212832262269183092350825431735 1868191506119423174407343597076343819084817503129050177)],
  [(25, q 26286981638295040159814453231245377898886308806274 27427832157940462437080350716865723469980829789069), (26, q 1140850519645422277265897485620345571094520982795 27427832157940462437080350716865723469980829789069)],
  [(26, q 14710315771604868064493387290318975 14758716978664966050796176225118974), (27, q 48401207060097986302788934799999 14758716978664966050796176225118974)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(25, q 1 1)],
  [(25, q 707860336746797847835693234390546612140545533473992608187923012886 709131907090613017390907709324471333133170540977904318330742685391), (26, q 1271570343815169555214474933924720992625007503911710142819672505 709131907090613017390907709324471333133170540977904318330742685391)],
  [(25, q 249324788081816346612527387982835633554206274254223131230855646 249773127920070896783430735128301767478853925319955810903796451), (26, q 448339838254550170903347145466133924647651065732679672940805 249773127920070896783430735128301767478853925319955810903796451)],
  [(25, q 26255252719997929881562373762648828719339994012930097027765314 26302476780347695751715934829583968925112271920760940500611309), (26, q 47224060349765870153561066935140205772277907830843472845995 26302476780347695751715934829583968925112271920760940500611309)],
  [(25, q 2076978186110195827006272087925901418796771681851061534732218446 2080822418826026629549967337208310479219419473105105726339608251), (26, q 3844232715830802543695249282409060422647791254044191607389805 2080822418826026629549967337208310479219419473105105726339608251)],
  [(25, q 6805257916813678943030156254436196413105288760462043390878887376674 6817934214707881863084766445668966003843289777889916213508444141469), (26, q 12676297894202920054610191232769590738001017427872822629556764795 6817934214707881863084766445668966003843289777889916213508444141469)],
  [(25, q 10109741794777963161659669343987440055126823977141209780729960614 10142933955388867074168789397042587646046729107507681850678074359), (26, q 33192160610903912509120053055147590919905130366472069948113745 10142933955388867074168789397042587646046729107507681850678074359)],
  [(25, q 4309030298980668629395106528162831741220040357994011766 4324566315564207217962141206384983270053303553747924671), (26, q 15536016583538588567034678222151528833263195753912905 4324566315564207217962141206384983270053303553747924671)],
  [(25, q 2615657882996633897076624039136697570226585334444586 2730116041550302204210691296684770088473627208821841), (26, q 114458158553668307134067257548072518247041874377255 2730116041550302204210691296684770088473627208821841)],
  [(26, q 34051302721291516445286131793591425 34164083338252838206697055345913602), (27, q 112780616961321761410923552322177 34164083338252838206697055345913602)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(25, q 20563838628406128318331959299068126188286527493338284957396574734 21384203475877481975758211041236849800900108959602305014757175579), (26, q 820364847471353657426251742168723612613581466264020057360600845 21384203475877481975758211041236849800900108959602305014757175579)],
  [(25, q 24751433871031995518079854750566466234101029090291237865001555822 25784650266398298960619997960264591457651844152031089471315901707), (26, q 1033216395366303442540143209698125223550815061739851606314345885 25784650266398298960619997960264591457651844152031089471315901707)],
  [(25, q 95898291768471668071895365879720161664979977180051209398467762 99901639645083588051634687534713927869460641643330351160902597), (26, q 4003347876611919979739321654993766204480664463279141762434835 99901639645083588051634687534713927869460641643330351160902597)],
  [(25, q 70690270275291031744877012588557752398526817291800967583789506 73641324239933457722671013690759421214151434728879029320042861), (26, q 2951053964642425977794001102201668815624617437078061736253355 73641324239933457722671013690759421214151434728879029320042861)],
  [(25, q 5592085024965081443931798222400701362106883403946603339557875534 5825858899530769517350156430434088929236955530202864942382840379), (26, q 233773874565688073418358208033387567130072126256261602824964845 5825858899530769517350156430434088929236955530202864942382840379)],
  [(25, q 2617507986230714630237290629331488304126319111196597980233807859278 2726965917885276717930302333882770489783526687543451250252962227643), (26, q 109457931654562087693011704551282185657207576346853270019154368365 2726965917885276717930302333882770489783526687543451250252962227643)],
  [(25, q 3888120713158222435009069239171154066775988677189551320378540458 4056864488958966285793729962138524160149355775862887588909939473), (26, q 168743775800743850784660722967370093373367098673336268531399015 4056864488958966285793729962138524160149355775862887588909939473)],
  [(25, q 1657178528048208219057601557621276472922221021333933402 1729694740488717488724905996802821980430504351692796937), (26, q 72516212440509269667304439181545507508283330358863535 1729694740488717488724905996802821980430504351692796937)],
  [(25, q 1003072034891260026004122224230975848556584173383942 1091963219756370204592864368243604897735019744461927), (26, q 88891184865110178588742144012629049178435571077985 1091963219756370204592864368243604897735019744461927)],
  [(26, q 13584059079226002243289205953441975 13664592227691275092513286568458094), (27, q 80533148465272849224080615016119 13664592227691275092513286568458094)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(10, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(25, q 21524141740654608965877694700820671320035945265690156214 22586159509689943903263715264496685542626816143237892959), (26, q 1062017769035334937386020563676014222590870877547736745 22586159509689943903263715264496685542626816143237892959)],
  [(25, q 3903729225788652345173797853375049217211233443096849634 4103745154515202693630706614447004182330954648413311229), (26, q 200015928726550348456908761071954965119721205316461595 4103745154515202693630706614447004182330954648413311229)],
  [(25, q 1374983528064389539821122587920130538421094243430074 1445436671486735756287923319826006919489198795429369), (26, q 70453143422346216466800731905876381068104551999295 1445436671486735756287923319826006919489198795429369)],
  [(25, q 1013552532756974255731723674856257528697551349873162 1065486722454242118069617230322622650372844105202497), (26, q 51934189697267862337893555466365121675292755329335 1065486722454242118069617230322622650372844105202497)],
  [(25, q 3447691994655363622286933215952894637503367918829345474 3624556468010407902526055327908847471733839145998164269), (26, q 176864473355044280239122111955952834230471227168818795 3624556468010407902526055327908847471733839145998164269)],
  [(25, q 37529620046025775684177078914403643828331398095720360006 39455373841803050215255642183446478401468576040418847111), (26, q 1925753795777274531078563269042834573137177944698487105 39455373841803050215255642183446478401468576040418847111)],
  [(25, q 55746228962420743369476998337275507958433934884446866 58697141752889786709109187653347193076575219314924021), (26, q 2950912790469043339632189316071685118141284430477155 58697141752889786709109187653347193076575219314924021)],
  [(25, q 1831807166375556752900188606468881628967398749830844386 1929447556302302111727988414278899733705153485619318141), (26, q 97640389926745358827799807810018104737754735788473755 1929447556302302111727988414278899733705153485619318141)],
  [(25, q 14371781526723408818764654195860730611934 15799176944021879079128191018174496263779), (26, q 1427395417298470260363536822313765651845 15799176944021879079128191018174496263779)],
  [(26, q 15143857324263558356253737962628675 15242639908899194917070234109188742), (27, q 98782584635636560816496146560067 15242639908899194917070234109188742)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(18, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 1 1)],
  [(26, q 17306701226438377773045043780529328766844903675 17359949559680042782052307420605461460557514742), (27, q 53248333241665009007263640076132693712611067 17359949559680042782052307420605461460557514742)],
  [(26, q 3144151269994615046598164479625729458792601425 3154179835558208843094178019725202273397028002), (27, q 10028565563593796496013540099472814604426577 3154179835558208843094178019725202273397028002)],
  [(26, q 85188056730356310388768514701196421178225 85459782769096808801285407234155031405794), (27, q 271726038740498412516892532958610227569 85459782769096808801285407234155031405794)],
  [(26, q 816339900710673313757043083776118182447525 818943820456901171272062031776212507955786), (27, q 2603919746227857515018948000094325508261 818943820456901171272062031776212507955786)],
  [(26, q 2777002808849799712772868452392688843745359425 2785870587422257512402884735795387860708731522), (27, q 8867778572457799630016283402699016963372097 2785870587422257512402884735795387860708731522)],
  [(26, q 30229242456009532399108358710868712978710779075 30325797507015969796846438263518001498169686918), (27, q 96555051006437397738079552649288519458907843 30325797507015969796846438263518001498169686918)],
  [(26, q 44967258689883544948129963127454812760854825 45115214018142049085991121072809372187836498), (27, q 147955328258504137861157945354559426981673 45115214018142049085991121072809372187836498)],
  [(26, q 1478097238939108452199911310130575040295503825 1482992814297878615428146464150952994616177058), (27, q 4895575358770163228235154020377954320673233 1482992814297878615428146464150952994616177058)],
  [(26, q 3447004807700299336662294583445436884206825 3467440389459772498195932796235228221671378), (27, q 20435581759473161533638212789791337464553 3467440389459772498195932796235228221671378)],
  [(26, q 60841495973361475059025 65902497619949750237346), (27, q 5061001646588275178321 65902497619949750237346)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)],
  [(27, q 1 1)]
]

/-- (C2) witness for `(1, 0) / e2`. -/
def c2w2 : List (ℕ × ℚ) := [(27, q 1 1)]

/-- (C3) witnesses: entry `a` is for `((y, 1) ∘ z_a) / e1`. -/
def c3w2 : List (List (ℕ × ℚ)) := [
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(0, q 1 1)],
  [(1, q 1 1)],
  [(2, q 1 1)],
  [(3, q 1 1)],
  [(4, q 1 1)],
  [(5, q 1 1)],
  [(6, q 1 1)],
  [(7, q 1 1)],
  [(8, q 1 1)],
  [(10, q 1 1)]
]

def y : Fin 3 → ℚ := ![q 2274691481464049 5000000000000000, q 602793242587973 1250000000000000, q 1 50]

def e₁ : Fin 3 → ℚ := ![q 1003883019401 1000000000000, q 260280393933 250000000000, q 963015339293 1000000000000]

def e₂ : Fin 3 → ℚ := ![q 779999999921 1000000000000, q 779999999921 1000000000000, q 129999999987 250000000000]

def lam : Fin 3 → ℚ := ![q 20874647890139383 27988626836321740, q 2400441832917297 27988626836321740, q 235676855663253 1399431341816087]

def Zq : Fin 3 → List (ℚ × ℚ) := ![Z0, Z1, Z2]

def pairs : Fin 3 → List (List (ℕ × ℚ)) := ![pairs0, pairs1, pairs2]

def c2w : Fin 3 → List (ℕ × ℚ) := ![c2w0, c2w1, c2w2]

def c3w : Fin 3 → List (List (ℕ × ℚ)) := ![c3w0, c3w1, c3w2]

end MaxLeafFormal.DSTCert