Exact global Y/Z certificate: logs 0
Definitionmme_released_global_yz_logs_0matrix-multiplicationmore-asymmetrynumerical-certificate
One component of the exact six-orientation Y/Z certificate: word enumeration and cached integer counts, finite entropy expressions, or outward-rounded logarithm intervals. All numerical data are connected to the published profile by the accompanying full proofs. Tables are split by orientation to fit publication and compilation limits.
Definition code
import Definitions.Def_mme_released_global_yz_expression_primitives
open BigOperators MME MME.ReleasedGlobalYZ
set_option autoImplicit false
set_option maxRecDepth 100000
set_option maxHeartbeats 16000000
namespace MME.ReleasedGlobalYZ
private def mkLog (q : ℚ) (k : ℕ) (lo hi : ℤ) : Entry :=
((q,q),(k,(lo : ℚ)/1000000000000,(hi : ℚ)/1000000000000))
private def logTable : Fin 472 → Entry :=
![mkLog (23074029039/1000000000000) 6 (-3769047578023) (-3769047577902),
mkLog (14234458127/125000000000) 4 (-2172648083583) (-2172648083502),
mkLog (72399479961/250000000000) 2 (-1239261801376) (-1239261801335),
mkLog (176379411787/500000000000) 2 (-1041970674907) (-1041970674866),
mkLog (95040673403/500000000000) 3 (-1660303157394) (-1660303157333),
mkLog (1445962827/50000000000) 6 (-3543247589552) (-3543247589431),
mkLog (165971607/100000000000) 10 (-6401108733513) (-6401108733312),
mkLog (33123453/1000000000000) 15 (-10315268976787) (-10315268976486),
mkLog (59829/500000000000) 23 (-15938628163379) (-15938628162918),
mkLog (3558614526243534456241460758266737/125000000000000000000000000000000000) 6 (-3558942446270) (-3558942446149),
mkLog (3558614537256465543758539241733263/125000000000000000000000000000000000) 6 (-3558942443175) (-3558942443054),
mkLog (1731632636998002155119472948883415228611635041/1000000000000000000000000000000000000000000000000) 10 (-6358690594790) (-6358690594589),
mkLog (24916403720635822790620557597672474771388364959/500000000000000000000000000000000000000000000000) 5 (-2999081727944) (-2999081727843),
mkLog (1731632637117159997518472948883415228611635041/1000000000000000000000000000000000000000000000000) 10 (-6358690594721) (-6358690594520),
mkLog (91502887979469448946966847407332743/2000000000000000000000000000000000000) 5 (-3084531925192) (-3084531925091),
mkLog (91502887979629125981850847407332743/2000000000000000000000000000000000000) 5 (-3084531925191) (-3084531925090),
mkLog (34632656687634435134207516025430244142935187/20000000000000000000000000000000000000000000000) 10 (-6358690480803) (-6358690480602),
mkLog (91502887978627213304008847407332743/2000000000000000000000000000000000000) 5 (-3084531925202) (-3084531925101),
mkLog (91502887978839848272576847407332743/2000000000000000000000000000000000000) 5 (-3084531925199) (-3084531925098),
mkLog (498328055016076620443404924896797095857064813/10000000000000000000000000000000000000000000000) 5 (-2999081766867) (-2999081766766),
mkLog (34632656686819804247367516025430244142935187/20000000000000000000000000000000000000000000000) 10 (-6358690480826) (-6358690480625),
mkLog (2314271169379555322180636049588671/1000000000000000000000000000000000000) 9 (-6068660470746) (-6068660470565),
mkLog (2314271169403199671010636049588671/1000000000000000000000000000000000000) 9 (-6068660470736) (-6068660470555),
mkLog (5487105344541680581985021407169062703385793391/2000000000000000000000000000000000000000000000000) 9 (-5898501602808) (-5898501602627),
mkLog (80388330836831582415388177163082770796614206609/1000000000000000000000000000000000000000000000000) 4 (-2520886252217) (-2520886252136),
mkLog (5487105227315004778949758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5898501624172) (-5898501623991),
mkLog (5487105227295925773677758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5898501624176) (-5898501623995),
mkLog (5487105344551220084621021407169062703385793391/2000000000000000000000000000000000000000000000000) 9 (-5898501602806) (-5898501602625),
mkLog (80388330845447184150016177163082770796614206609/1000000000000000000000000000000000000000000000000) 4 (-2520886252110) (-2520886252029),
mkLog (80388359412669047715743159993598014317519973899/1000000000000000000000000000000000000000000000000) 4 (-2520885896745) (-2520885896664),
mkLog (80388359405802852881675159993598014317519973899/1000000000000000000000000000000000000000000000000) 4 (-2520885896830) (-2520885896749),
mkLog (2314239795326541612995247006846223/1000000000000000000000000000000000000) 9 (-6068674027613) (-6068674027432),
mkLog (5487105227305465276313758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5898501624174) (-5898501623993),
mkLog (5487105227467555058021758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5898501624144) (-5898501623963),
mkLog (2314239795355160120903247006846223/1000000000000000000000000000000000000) 9 (-6068674027600) (-6068674027419),
mkLog (96394189003668980477763514060327/1000000000000000000000000000000000000) 14 (-9247064638351) (-9247064638070),
mkLog (15759270396838251164144937298039571/4000000000000000000000000000000000000) 8 (-5536620851442) (-5536620851281),
mkLog (15759270395477663475184937298039571/4000000000000000000000000000000000000) 8 (-5536620851528) (-5536620851367),
mkLog (24317804203136367142424693405524913034703629908061769317/250000000000000000000000000000000000000000000000000000000000) 14 (-9238007431664) (-9238007431383),
mkLog (509933109900027399529317668089969104119945769091938230683/125000000000000000000000000000000000000000000000000000000000) 8 (-5501789456308) (-5501789456147),
mkLog (24317804184455968038424693405524913034703629908061769317/250000000000000000000000000000000000000000000000000000000000) 14 (-9238007432432) (-9238007432151),
mkLog (15759270396716523851504937298039571/4000000000000000000000000000000000000) 8 (-5536620851449) (-5536620851288),
mkLog (15759270397233516563056937298039571/4000000000000000000000000000000000000) 8 (-5536620851417) (-5536620851256),
mkLog (509933125678131009995754671750259730040909598966938230683/125000000000000000000000000000000000000000000000000000000000) 8 (-5501789425366) (-5501789425205),
mkLog (8853941904344687710798350780285217440304441002033061769317/62500000000000000000000000000000000000000000000000000000000) 3 (-1954303784000) (-1954303783939),
mkLog (509933125058487529191754671750259730040909598966938230683/125000000000000000000000000000000000000000000000000000000000) 8 (-5501789426581) (-5501789426420),
mkLog (1969908986553695570218706904381173/500000000000000000000000000000000000) 8 (-5536620756539) (-5536620756378),
mkLog (1969908986623246546074706904381173/500000000000000000000000000000000000) 8 (-5536620756504) (-5536620756343),
mkLog (509933110373296079645317668089969104119945769091938230683/125000000000000000000000000000000000000000000000000000000000) 8 (-5501789455380) (-5501789455219),
mkLog (1969908986541160726266706904381173/500000000000000000000000000000000000) 8 (-5536620756546) (-5536620756385),
mkLog (1969908986509945483210706904381173/500000000000000000000000000000000000) 8 (-5536620756562) (-5536620756401),
mkLog (96395223203745806974078936355179/1000000000000000000000000000000000000) 14 (-9247053909545) (-9247053909264),
mkLog (85339278568729277627633993563669/500000000000000000000000000000000000) 13 (-8675728553424) (-8675728553163),
mkLog (378531942111963691207750565847681743128215547/2000000000000000000000000000000000000000000000000) 13 (-8572357278026) (-8572357277765),
mkLog (378531941989333333447750565847681743128215547/2000000000000000000000000000000000000000000000000) 13 (-8572357278350) (-8572357278089),
mkLog (85339278561683515504633993563669/500000000000000000000000000000000000) 13 (-8675728553506) (-8675728553245),
mkLog (6680603281327045707503787459993766756871784453/1000000000000000000000000000000000000000000000000) 8 (-5008546984016) (-5008546983855),
mkLog (6680603275409043910939787459993766756871784453/1000000000000000000000000000000000000000000000000) 8 (-5008546984902) (-5008546984741),
mkLog (378531997225090791696855672521036187175236591/2000000000000000000000000000000000000000000000000) 13 (-8572357132429) (-8572357132168),
mkLog (6680603542239574526381266097442592812824763409/1000000000000000000000000000000000000000000000000) 8 (-5008546944961) (-5008546944800),
mkLog (378531997206017328100855672521036187175236591/2000000000000000000000000000000000000000000000000) 13 (-8572357132479) (-8572357132218),
mkLog (378531942121664710275750565847681743128215547/2000000000000000000000000000000000000000000000000) 13 (-8572357278000) (-8572357277739),
mkLog (378531942121401850643750565847681743128215547/2000000000000000000000000000000000000000000000000) 13 (-8572357278001) (-8572357277740),
mkLog (6680603540788812748261266097442592812824763409/1000000000000000000000000000000000000000000000000) 8 (-5008546945178) (-5008546945017),
mkLog (341357907408470239274144434135169/2000000000000000000000000000000000000) 13 (-8675726229955) (-8675726229694),
mkLog (341357907353418440450144434135169/2000000000000000000000000000000000000) 13 (-8675726230116) (-8675726229855),
mkLog (411911556861734438543011264641168117728253/50000000000000000000000000000000000000000000000) 17 (-11706724905070) (-11706724904729),
mkLog (5876978343878483648226968664779631882271747/25000000000000000000000000000000000000000000000) 13 (-8355588361252) (-8355588360990),
mkLog (144603237807338007734926425884257/500000000000000000000000000000000000) 12 (-8148369676576) (-8148369676335),
mkLog (144603237828070372394426425884257/500000000000000000000000000000000000) 12 (-8148369676433) (-8148369676192),
mkLog (411911562392695070893011264641168117728253/50000000000000000000000000000000000000000000000) 17 (-11706724891643) (-11706724891302),
mkLog (144603237746564770353426425884257/500000000000000000000000000000000000) 12 (-8148369676996) (-8148369676755),
mkLog (144603237832578353342426425884257/500000000000000000000000000000000000) 12 (-8148369676402) (-8148369676161),
mkLog (823386264367729436462166142441070784137899/100000000000000000000000000000000000000000000000) 17 (-11707255316531) (-11707255316190),
mkLog (11743342302781381979077303645014529215862101/50000000000000000000000000000000000000000000000) 13 (-8356491817066) (-8356491816804),
mkLog (823386273136412228562166142441070784137899/100000000000000000000000000000000000000000000000) 17 (-11707255305881) (-11707255305540),
mkLog (33123453/4000000000000) 17 (-11701563337927) (-11701563337586),
mkLog (16430609/4000000000000) 18 (-12402658921561) (-12402658921200),
mkLog (16430609/1000000000000) 16 (-11016364560421) (-11016364560100),
mkLog (1949730570549078743/500000000000000000000000) 18 (-12454672183506) (-12454672183145),
mkLog (88507457995087282651/1000000000000000000000000) 14 (-9332423738511) (-9332423738230),
mkLog (15222885775575001427/200000000000000000000000) 14 (-9483272707033) (-9483272706752),
mkLog (15222885777563531583/200000000000000000000000) 14 (-9483272706903) (-9483272706622),
mkLog (974865322310913527/250000000000000000000000) 18 (-12454672145514) (-12454672145153),
mkLog (38057214358650598519/500000000000000000000000) 14 (-9483272709143) (-9483272708862),
mkLog (38057214443163130149/500000000000000000000000) 14 (-9483272706922) (-9483272706641),
mkLog (3900970576175070023/1000000000000000000000000) 18 (-12454285170286) (-12454285169925),
mkLog (11070812759036101543/125000000000000000000000) 14 (-9331756852433) (-9331756852152),
mkLog (1950485278393450501/500000000000000000000000) 18 (-12454285175256) (-12454285174895),
mkLog (497132539/1000000000000) 11 (-7606653889463) (-7606653889242),
mkLog (882717695234093317/15625000000000000000000) 15 (-9781377315199) (-9781377314898),
mkLog (26195491133253933679/500000000000000000000000) 15 (-9856776075749) (-9856776075448),
mkLog (26195491100220375653/500000000000000000000000) 15 (-9856776077010) (-9856776076709),
mkLog (28246966235693286849/500000000000000000000000) 15 (-9781377315617) (-9781377315316),
mkLog (509247049739107604439/500000000000000000000000) 10 (-6889430115760) (-6889430115559),
mkLog (509247049871241836543/500000000000000000000000) 10 (-6889430115501) (-6889430115300),
mkLog (13097744166240060523/250000000000000000000000) 15 (-9856776182667) (-9856776182366),
mkLog (509247036549279792629/500000000000000000000000) 10 (-6889430141661) (-6889430141460),
mkLog (5239097666967932181/100000000000000000000000) 15 (-9856776182577) (-9856776182276),
mkLog (13097745563087657051/250000000000000000000000) 15 (-9856776076019) (-9856776075718),
mkLog (13097745567806736769/250000000000000000000000) 15 (-9856776075659) (-9856776075358),
mkLog (101849407193766597463/100000000000000000000000) 10 (-6889430142801) (-6889430142600),
mkLog (28246918313438750559/500000000000000000000000) 15 (-9781379012163) (-9781379011862),
mkLog (28246918242652554789/500000000000000000000000) 15 (-9781379014669) (-9781379014368),
mkLog (2359539859/500000000000) 8 (-5356141473476) (-5356141473315),
mkLog (699817445174710533/31250000000000000000000) 16 (-10706710425885) (-10706710425564),
mkLog (12224328035321521647/31250000000000000000000) 12 (-7846346587871) (-7846346587630),
mkLog (6112164019005101013/15625000000000000000000) 12 (-7846346587651) (-7846346587410),
mkLog (695210014161846579/31250000000000000000000) 16 (-10713315955740) (-10713315955419),
mkLog (744859815959863659/1953125000000000000000) 12 (-7871745177851) (-7871745177610),
mkLog (139042002678730437/6250000000000000000000) 16 (-10713315956845) (-10713315956524),
mkLog (12224328043771659981/31250000000000000000000) 12 (-7846346587180) (-7846346586939),
mkLog (12224328037626104829/31250000000000000000000) 12 (-7846346587683) (-7846346587442),
mkLog (372429902410522473/976562500000000000000) 12 (-7871745192805) (-7871745192564),
mkLog (117225539296860270111/15625000000000000000000) 8 (-4892527709193) (-4892527709031),
mkLog (2383551385183412631/6250000000000000000000) 12 (-7871745188712) (-7871745188471),
mkLog (2444865437600621013/6250000000000000000000) 12 (-7846346657185) (-7846346656944),
mkLog (305608179652065477/781250000000000000000) 12 (-7846346657343) (-7846346657102),
mkLog (5958878586445780413/15625000000000000000000) 12 (-7871745167989) (-7871745167748),
mkLog (3056081796904751967/7812500000000000000000) 12 (-7846346657217) (-7846346656976),
mkLog (699811969485070101/31250000000000000000000) 16 (-10706718250369) (-10706718250048),
mkLog (384097197/31250000000) 7 (-4398879017489) (-4398879017348),
mkLog (13173888525088033413/250000000000000000000000) 15 (-9850979468549) (-9850979468248),
mkLog (26347777061998241241/500000000000000000000000) 15 (-9850979468100) (-9850979467799),
mkLog (581819988659001957/12500000000000000000000) 15 (-9975078100372) (-9975078100071),
mkLog (32388455044117914291/31250000000000000000000) 10 (-6871972621765) (-6871972621564),
mkLog (11636399955241525131/250000000000000000000000) 15 (-9975078084726) (-9975078084425),
mkLog (518215280623131407751/500000000000000000000000) 10 (-6871972621925) (-6871972621724),
mkLog (8097111686828977461/7812500000000000000000) 10 (-6871972877931) (-6871972877730),
mkLog (518215146171906220839/500000000000000000000000) 10 (-6871972881376) (-6871972881175),
mkLog (13174018900027482033/250000000000000000000000) 15 (-9850969572132) (-9850969571831),
mkLog (4654559982569497029/100000000000000000000000) 15 (-9975078084624) (-9975078084323),
mkLog (2364434883/500000000000) 8 (-5354069055218) (-5354069055057),
mkLog (21651840837161629/6250000000000000000000) 19 (-12573001543950) (-12573001543569),
mkLog (3125849249704002463/40000000000000000000000) 14 (-9456928727064) (-9456928726783),
mkLog (692858930423187693/200000000000000000000000) 19 (-12573001509839) (-12573001509458),
mkLog (8317543818065598479/100000000000000000000000) 14 (-9394558468037) (-9394558467756),
mkLog (16635087634220361657/200000000000000000000000) 14 (-9394558468152) (-9394558467871),
mkLog (692858875109534243/200000000000000000000000) 19 (-12573001589673) (-12573001589292),
mkLog (83175438079080003/1000000000000000000000) 14 (-9394558469259) (-9394558468978),
mkLog (831754381695932541/10000000000000000000000) 14 (-9394558468170) (-9394558467889),
mkLog (15629246646577176597/200000000000000000000000) 14 (-9456928701595) (-9456928701314),
mkLog (692858872494706989/200000000000000000000000) 19 (-12573001593447) (-12573001593066),
mkLog (100570279/200000000000) 11 (-7595215869002) (-7595215868781),
mkLog (16604077/4000000000000) 18 (-12392156651649) (-12392156651288),
mkLog (16604077/1000000000000) 16 (-11005862290509) (-11005862290188),
mkLog (120039/1000000000000) 23 (-15935449147197) (-15935449146736),
mkLog (23073909/1000000000) 6 (-3769052780379) (-3769052780258),
mkLog (3558095648837284456241460758266737/125000000000000000000000000000000000) 6 (-3559088265727) (-3559088265606),
mkLog (3558095659850215543758539241733263/125000000000000000000000000000000000) 6 (-3559088262632) (-3559088262511),
mkLog (113859060939/1000000000000) 4 (-2172793903040) (-2172793902959),
mkLog (1728168342464056294479472948883415228611635041/1000000000000000000000000000000000000000000000000) 10 (-6360693193039) (-6360693192838),
mkLog (24877330605014522759833057597672474771388364959/500000000000000000000000000000000000000000000000) 5 (-3000651127153) (-3000651127052),
mkLog (1728168342465044059053472948883415228611635041/1000000000000000000000000000000000000000000000000) 10 (-6360693193038) (-6360693192837),
mkLog (91336537103108136977386847407332743/2000000000000000000000000000000000000) 5 (-3086351564717) (-3086351564616),
mkLog (91336537103286922365280847407332743/2000000000000000000000000000000000000) 5 (-3086351564715) (-3086351564614),
mkLog (34563370800123481709907516025430244142935187/20000000000000000000000000000000000000000000000) 10 (-6360693078732) (-6360693078531),
mkLog (91336537102469053298008847407332743/2000000000000000000000000000000000000) 5 (-3086351564724) (-3086351564623),
mkLog (91336537102500661764376847407332743/2000000000000000000000000000000000000) 5 (-3086351564723) (-3086351564622),
mkLog (497546592683747761613554924896797095857064813/10000000000000000000000000000000000000000000000) 5 (-3000651166178) (-3000651166077),
mkLog (34563370799570333548467516025430244142935187/20000000000000000000000000000000000000000000000) 10 (-6360693078748) (-6360693078547),
mkLog (289095068449/1000000000000) 2 (-1240999688414) (-1240999688373),
mkLog (2261575615279203188528636049588671/1000000000000000000000000000000000000) 9 (-6091693533800) (-6091693533619),
mkLog (5394014146356240268865021407169062703385793391/2000000000000000000000000000000000000000000000000) 9 (-5915612612309) (-5915612612128),
mkLog (79351900275419809158076177163082770796614206609/1000000000000000000000000000000000000000000000000) 4 (-2533862884317) (-2533862884236),
mkLog (5394014027673072577901758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5915612634312) (-5915612634131),
mkLog (5394014027653993572629758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5915612634316) (-5915612634135),
mkLog (5394014146365779771501021407169062703385793391/2000000000000000000000000000000000000000000000000) 9 (-5915612612308) (-5915612612127),
mkLog (79351900284200921334514177163082770796614206609/1000000000000000000000000000000000000000000000000) 4 (-2533862884206) (-2533862884125),
mkLog (79351929116754938600735159993598014317519973899/1000000000000000000000000000000000000000000000000) 4 (-2533862520856) (-2533862520775),
mkLog (79351929113459040439997159993598014317519973899/1000000000000000000000000000000000000000000000000) 4 (-2533862520897) (-2533862520816),
mkLog (2261543719726431684863247006846223/1000000000000000000000000000000000000) 9 (-6091707637144) (-6091707636963),
mkLog (5394014027663533075265758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5915612634314) (-5915612634133),
mkLog (5394014027816165117441758379715258182480026101/2000000000000000000000000000000000000000000000000) 9 (-5915612634286) (-5915612634105),
mkLog (2261543719755050192771247006846223/1000000000000000000000000000000000000) 9 (-6091707637131) (-6091707636950),
mkLog (21751872113/62500000000) 2 (-1055466728772) (-1055466728731),
mkLog (74000030758078243421763514060327/1000000000000000000000000000000000000) 14 (-9511445049252) (-9511445048971),
mkLog (14194556408317096393328937298039571/4000000000000000000000000000000000000) 9 (-5641191100611) (-5641191100430),
mkLog (14194556406612357615856937298039571/4000000000000000000000000000000000000) 9 (-5641191100731) (-5641191100550),
mkLog (18756124089841594510424693405524913034703629908061769317/250000000000000000000000000000000000000000000000000000000000) 14 (-9497695879772) (-9497695879491),
mkLog (462262081678596125353317668089969104119945769091938230683/125000000000000000000000000000000000000000000000000000000000) 9 (-5599937009774) (-5599937009592),
mkLog (18756124077306750558424693405524913034703629908061769317/250000000000000000000000000000000000000000000000000000000000) 14 (-9497695880441) (-9497695880160),
mkLog (14194556407113751373936937298039571/4000000000000000000000000000000000000) 9 (-5641191100696) (-5641191100514),
mkLog (14194556408417375144944937298039571/4000000000000000000000000000000000000) 9 (-5641191100604) (-5641191100423),
mkLog (462262098169584133451754671750259730040909598966938230683/125000000000000000000000000000000000000000000000000000000000) 9 (-5599936974099) (-5599936973918),
mkLog (8385039747157246630354350780285217440304441002033061769317/62500000000000000000000000000000000000000000000000000000000) 3 (-2008717421240) (-2008717421179),
mkLog (462262097354819276571754671750259730040909598966938230683/125000000000000000000000000000000000000000000000000000000000) 9 (-5599936975862) (-5599936975680),
mkLog (1774319751545645889178706904381173/500000000000000000000000000000000000) 9 (-5641190987606) (-5641190987425),
mkLog (1774319751645924640794706904381173/500000000000000000000000000000000000) 9 (-5641190987550) (-5641190987369),
mkLog (462262081681729836341317668089969104119945769091938230683/125000000000000000000000000000000000000000000000000000000000) 9 (-5599937009767) (-5599937009585),
mkLog (1774319751533111045226706904381173/500000000000000000000000000000000000) 9 (-5641190987613) (-5641190987432),
mkLog (1774319751508041357322706904381173/500000000000000000000000000000000000) 9 (-5641190987628) (-5641190987446),
mkLog (74001240180223563742078936355179/1000000000000000000000000000000000000) 14 (-9511428705850) (-9511428705569),
mkLog (88895118251/500000000000) 3 (-1727150870253) (-1727150870192),
mkLog (57092312321238291483633993563669/500000000000000000000000000000000000) 14 (-9077693905303) (-9077693905021),
mkLog (273749977578947956491750565847681743128215547/2000000000000000000000000000000000000000000000000) 13 (-8896442539428) (-8896442539167),
mkLog (273749977588451830835750565847681743128215547/2000000000000000000000000000000000000000000000000) 13 (-8896442539393) (-8896442539132),
mkLog (57092312325990228655633993563669/500000000000000000000000000000000000) 14 (-9077693905219) (-9077693904938),
mkLog (5662109181848830498625787459993766756871784453/1000000000000000000000000000000000000000000000000) 8 (-5173958809294) (-5173958809133),
mkLog (5662109175666560237853787459993766756871784453/1000000000000000000000000000000000000000000000000) 8 (-5173958810386) (-5173958810225),
mkLog (273750043895170307512855672521036187175236591/2000000000000000000000000000000000000000000000000) 13 (-8896442297177) (-8896442296916),
mkLog (5662109469141014941123266097442592812824763409/1000000000000000000000000000000000000000000000000) 8 (-5173958758554) (-5173958758393),
mkLog (273750043866658684480855672521036187175236591/2000000000000000000000000000000000000000000000000) 13 (-8896442297281) (-8896442297020),
mkLog (273749977616963453867750565847681743128215547/2000000000000000000000000000000000000000000000000) 13 (-8896442539289) (-8896442539028),
mkLog (5662109468851146773631266097442592812824763409/1000000000000000000000000000000000000000000000000) 8 (-5173958758606) (-5173958758445),
mkLog (228370234154715237038144434135169/2000000000000000000000000000000000000) 14 (-9077689592692) (-9077689592411),
mkLog (228370234382808221294144434135169/2000000000000000000000000000000000000) 14 (-9077689591693) (-9077689591412),
mkLog (12100088411/500000000000) 6 (-3721395339213) (-3721395339092),
mkLog (216938499806826564243011264641168117728253/50000000000000000000000000000000000000000000000) 18 (-12347919661230) (-12347919660869),
mkLog (3664291894001301581951968664779631882271747/25000000000000000000000000000000000000000000000) 13 (-8827995994949) (-8827995994688),
mkLog (106546023368400504167426425884257/500000000000000000000000000000000000) 13 (-8453786341429) (-8453786341168),
mkLog (106546023384161543436926425884257/500000000000000000000000000000000000) 13 (-8453786341281) (-8453786341020),
mkLog (216938497930512365493011264641168117728253/50000000000000000000000000000000000000000000000) 18 (-12347919669879) (-12347919669518),
mkLog (106546023387914171834426425884257/500000000000000000000000000000000000) 13 (-8453786341246) (-8453786340985),
mkLog (106546023389415223193426425884257/500000000000000000000000000000000000) 13 (-8453786341232) (-8453786340971),
mkLog (433289206750222434162166142441070784137899/100000000000000000000000000000000000000000000000) 18 (-12349275325114) (-12349275324753),
mkLog (7315017199166941361877303645014529215862101/50000000000000000000000000000000000000000000000) 13 (-8829848898853) (-8829848898592),
mkLog (433289217457722128362166142441070784137899/100000000000000000000000000000000000000000000000) 18 (-12349275300402) (-12349275300041),
mkLog (1162583531/1000000000000) 10 (-6757110568562) (-6757110568361),
mkLog (4173211/1000000000000) 18 (-12386824794671) (-12386824794310),
mkLog (4173211/250000000000) 16 (-11000530433531) (-11000530433210),
mkLog (4554463621/200000000000) 6 (-3782209598923) (-3782209598802),
mkLog (28406419247/250000000000) 4 (-2174845768453) (-2174845768372),
mkLog (4529057739/15625000000) 2 (-1238358282420) (-1238358282379),
mkLog (353279584409/1000000000000) 2 (-1040495511733) (-1040495511692),
mkLog (94987662223/500000000000) 3 (-1660861086623) (-1660861086562),
mkLog (5762708113/200000000000) 6 (-3546909843884) (-3546909843763),
mkLog (328146037/200000000000) 10 (-6412613901579) (-6412613901378),
mkLog (33009241/1000000000000) 15 (-10318723005547) (-10318723005246),
mkLog (24153/200000000000) 23 (-15929419328758) (-15929419328297),
mkLog (56812713614508866178586917282841879/2000000000000000000000000000000000000) 6 (-3561142327681) (-3561142327560),
mkLog (56812963373491133821413082717158121/2000000000000000000000000000000000000) 6 (-3561137931509) (-3561137931388),
mkLog (1626373444407286753097547473710229267942254307/1000000000000000000000000000000000000000000000000) 10 (-6421402623721) (-6421402623520),
mkLog (25049167521575534584006445884969230232057745693/500000000000000000000000000000000000000000000000) 5 (-2993767504166) (-2993767504065),
mkLog (1626373444299702909168547473710229267942254307/1000000000000000000000000000000000000000000000000) 10 (-6421402623787) (-6421402623586),
mkLog (91578755625337808997532620241808523/2000000000000000000000000000000000000) 5 (-3083703140299) (-3083703140198),
mkLog (91578755625371494857082620241808523/2000000000000000000000000000000000000) 5 (-3083703140299) (-3083703140198),
mkLog (1626374391436609316743563593563294455663444627/1000000000000000000000000000000000000000000000000) 10 (-6421402041426) (-6421402041225),
mkLog (91578755625468430680632620241808523/2000000000000000000000000000000000000) 5 (-3083703140298) (-3083703140197),
mkLog (91578755625251714733480620241808523/2000000000000000000000000000000000000) 5 (-3083703140300) (-3083703140199),
mkLog (25049176665255945997505822805948723044336555373/500000000000000000000000000000000000000000000000) 5 (-2993767139137) (-2993767139036),
mkLog (1626374391478715223601563593563294455663444627/1000000000000000000000000000000000000000000000000) 10 (-6421402041400) (-6421402041199),
mkLog (2308279251118275510078186422999273/1000000000000000000000000000000000000) 9 (-6071252945061) (-6071252944880),
mkLog (2308279250865353833958186422999273/1000000000000000000000000000000000000) 9 (-6071252945170) (-6071252944989),
mkLog (1350362598668927692664418613573321667842747463/500000000000000000000000000000000000000000000000) 9 (-5914234950521) (-5914234950340),
mkLog (20152540951507993871852807096135765207157252537/250000000000000000000000000000000000000000000000) 4 (-2518130535649) (-2518130535568),
mkLog (1080290236105625120139877498453040121737933109/400000000000000000000000000000000000000000000000) 9 (-5914234805031) (-5914234804850),
mkLog (1080290236113228219615077498453040121737933109/400000000000000000000000000000000000000000000000) 9 (-5914234805024) (-5914234804843),
mkLog (20152540951600813311379807096135765207157252537/250000000000000000000000000000000000000000000000) 4 (-2518130535644) (-2518130535563),
mkLog (1350362598676055598422418613573321667842747463/500000000000000000000000000000000000000000000000) 9 (-5914234950515) (-5914234950334),
mkLog (16122028191182395630433884982652941278262066891/200000000000000000000000000000000000000000000000) 4 (-2518130819113) (-2518130819032),
mkLog (16122028192435131600711484982652941278262066891/200000000000000000000000000000000000000000000000) 4 (-2518130819035) (-2518130818954),
mkLog (923322645202844441305639333053789/400000000000000000000000000000000000) 9 (-6071241091327) (-6071241091146),
mkLog (1080290236107525895008677498453040121737933109/400000000000000000000000000000000000000000000000) 9 (-5914234805030) (-5914234804849),
mkLog (923322645216282569580839333053789/400000000000000000000000000000000000) 9 (-6071241091313) (-6071241091132),
mkLog (95855555068320065130644332235429/1000000000000000000000000000000000000) 14 (-9252668134442) (-9252668134161),
mkLog (7544326521723321679777830059388321/2000000000000000000000000000000000000) 9 (-5580106632932) (-5580106632750),
mkLog (7544326512473353253501830059388321/2000000000000000000000000000000000000) 9 (-5580106634158) (-5580106633976),
mkLog (20103262277000416857741553774118358469652474525140803599/200000000000000000000000000000000000000000000000000000000000) 14 (-9205190541438) (-9205190541157),
mkLog (372063091189875272406691553307882770538134870674859196401/100000000000000000000000000000000000000000000000000000000000) 9 (-5593862025196) (-5593862025014),
mkLog (7544326512799269201753830059388321/2000000000000000000000000000000000000) 9 (-5580106634115) (-5580106633933),
mkLog (7544326512523492629309830059388321/2000000000000000000000000000000000000) 9 (-5580106634151) (-5580106633969),
mkLog (372063083959031237191874542120739438911917818474859196401/100000000000000000000000000000000000000000000000000000000000) 9 (-5593862044630) (-5593862044449),
mkLog (7216085889214837306667265211005330782080294836325140803599/50000000000000000000000000000000000000000000000000000000000) 3 (-1935710320162) (-1935710320101),
mkLog (372063083964096803152674542120739438911917818474859196401/100000000000000000000000000000000000000000000000000000000000) 9 (-5593862044617) (-5593862044435),
mkLog (15088653492071143119102334304714791/4000000000000000000000000000000000000) 9 (-5580106603199) (-5580106603017),
mkLog (15088653492020903688294334304714791/4000000000000000000000000000000000000) 9 (-5580106603202) (-5580106603021),
mkLog (20103262261959004335341553774118358469652474525140803599/200000000000000000000000000000000000000000000000000000000000) 14 (-9205190542186) (-9205190541905),
mkLog (372063091211182606080091553307882770538134870674859196401/100000000000000000000000000000000000000000000000000000000000) 9 (-5593862025138) (-5593862024957),
mkLog (15088653491619780677430334304714791/4000000000000000000000000000000000000) 9 (-5580106603229) (-5580106603047),
mkLog (15088653492823165718822334304714791/4000000000000000000000000000000000000) 9 (-5580106603149) (-5580106602967),
mkLog (95855836034806655583904040111711/1000000000000000000000000000000000000) 14 (-9252665203302) (-9252665203021),
mkLog (174661034909974468454426269420011/1000000000000000000000000000000000000) 13 (-8652663405844) (-8652663405583),
mkLog (92777581968471165666635037632896946160601803/500000000000000000000000000000000000000000000000) 13 (-8592158340543) (-8592158340282),
mkLog (92777581930313155122635037632896946160601803/500000000000000000000000000000000000000000000000) 13 (-8592158340954) (-8592158340693),
mkLog (174661034867195872040426269420011/1000000000000000000000000000000000000) 13 (-8652663406089) (-8652663405828),
mkLog (1664403370619365354141355868764000803839398197/250000000000000000000000000000000000000000000000) 8 (-5011994194693) (-5011994194532),
mkLog (1664403370255072467197355868764000803839398197/250000000000000000000000000000000000000000000000) 8 (-5011994194912) (-5011994194751),
mkLog (185555180370568312757622069329054399254666133/1000000000000000000000000000000000000000000000000) 13 (-8592158251978) (-8592158251717),
mkLog (3328807327335491270686971875118532600745333867/500000000000000000000000000000000000000000000000) 8 (-5011994018625) (-5011994018464),
mkLog (185555180375288342259622069329054399254666133/1000000000000000000000000000000000000000000000000) 13 (-8592158251953) (-8592158251692),
mkLog (92777581930288294214635037632896946160601803/500000000000000000000000000000000000000000000000) 13 (-8592158340954) (-8592158340693),
mkLog (92777581925617986528635037632896946160601803/500000000000000000000000000000000000000000000000) 13 (-8592158341004) (-8592158340743),
mkLog (185555180370518590941622069329054399254666133/1000000000000000000000000000000000000000000000000) 13 (-8592158251978) (-8592158251717),
mkLog (3328807327030120716448971875118532600745333867/500000000000000000000000000000000000000000000000) 8 (-5011994018716) (-5011994018555),
mkLog (21832552874848709994552777012153/125000000000000000000000000000000000) 13 (-8652666909272) (-8652666909011),
mkLog (987261815687223454466007430419552050358893/125000000000000000000000000000000000000000000000) 17 (-11748889027060) (-11748889026719),
mkLog (15273773792619584400891207782770697949641107/62500000000000000000000000000000000000000000000) 12 (-8316784609452) (-8316784609211),
mkLog (1120376909382191554282842064381311/4000000000000000000000000000000000000) 12 (-8180384485294) (-8180384485053),
mkLog (1120376907382178059186842064381311/4000000000000000000000000000000000000) 12 (-8180384487079) (-8180384486838),
mkLog (987261824218708638841007430419552050358893/125000000000000000000000000000000000000000000000) 17 (-11748889018418) (-11748889018077),
mkLog (1120376909853281983758842064381311/4000000000000000000000000000000000000) 12 (-8180384484874) (-8180384484633),
mkLog (1120376908660345417942842064381311/4000000000000000000000000000000000000) 12 (-8180384485939) (-8180384485698),
mkLog (1974523648871520125800796925317445601063663/250000000000000000000000000000000000000000000000) 17 (-11748889018199) (-11748889017858),
mkLog (30547564648180352785754514600638179398936337/125000000000000000000000000000000000000000000000) 12 (-8316784050883) (-8316784050642),
mkLog (1974523649602759064300796925317445601063663/250000000000000000000000000000000000000000000000) 17 (-11748889017828) (-11748889017487),
mkLog (33009241/4000000000000) 17 (-11705017366687) (-11705017366346),
mkLog (4139797/1000000000000) 18 (-12394863805327) (-12394863804966),
mkLog (4139797/250000000000) 16 (-11008569444187) (-11008569443866),
mkLog (31742317851540453/8000000000000000000000) 18 (-12437301361195) (-12437301360834),
mkLog (21248159577203668029/250000000000000000000000) 14 (-9372945913498) (-9372945913217),
mkLog (77006471254222398873/1000000000000000000000000) 14 (-9471621097521) (-9471621097240),
mkLog (77006471238418165689/1000000000000000000000000) 14 (-9471621097726) (-9471621097445),
mkLog (3967789759099964697/1000000000000000000000000) 18 (-12437301354225) (-12437301353864),
mkLog (3080258865894107973/40000000000000000000000) 14 (-9471621092415) (-9471621092134),
mkLog (38503235778980002689/500000000000000000000000) 14 (-9471621093576) (-9471621093295),
mkLog (495973719949230873/125000000000000000000000) 18 (-12437301354100) (-12437301353739),
mkLog (84992603984489607903/1000000000000000000000000) 14 (-9372946317348) (-9372946317067),
mkLog (396778975860608241/100000000000000000000000) 18 (-12437301354349) (-12437301353988),
mkLog (493882287/1000000000000) 11 (-7613213354707) (-7613213354486),
mkLog (5553143652536510067/100000000000000000000000) 15 (-9798561273840) (-9798561273539),
mkLog (6672341964857874021/125000000000000000000000) 15 (-9838098098967) (-9838098098666),
mkLog (1334468391063674277/25000000000000000000000) 15 (-9838098100397) (-9838098100096),
mkLog (27765718248373296381/500000000000000000000000) 15 (-9798561274356) (-9798561274054),
mkLog (257537227926612862149/250000000000000000000000) 10 (-6878051912819) (-6878051912618),
mkLog (515074457501174804667/500000000000000000000000) 10 (-6878051909620) (-6878051909419),
mkLog (834042691053203553/15625000000000000000000) 15 (-9838098164376) (-9838098164075),
mkLog (515074389079092147957/500000000000000000000000) 10 (-6878052042459) (-6878052042258),
mkLog (26689367818888609881/500000000000000000000000) 15 (-9838098100486) (-9838098100185),
mkLog (26689367823658361199/500000000000000000000000) 15 (-9838098100307) (-9838098100006),
mkLog (26689366111317638037/500000000000000000000000) 15 (-9838098164466) (-9838098164165),
mkLog (257537192344268029869/250000000000000000000000) 10 (-6878052050983) (-6878052050782),
mkLog (27765799796811580227/500000000000000000000000) 15 (-9798558337341) (-9798558337040),
mkLog (2384875659/500000000000) 8 (-5345461110113) (-5345461109952),
mkLog (1234398848849534523/62500000000000000000000) 16 (-10832337746378) (-10832337746057),
mkLog (24950554958514645599/62500000000000000000000) 12 (-7826025771069) (-7826025770828),
mkLog (24950554961648356587/62500000000000000000000) 12 (-7826025770944) (-7826025770703),
mkLog (59836071774682943/3125000000000000000000) 16 (-10863336155279) (-10863336154958),
mkLog (3164778778139986063/7812500000000000000000) 12 (-7811397137335) (-7811397137094),
mkLog (24950554975750056033/62500000000000000000000) 12 (-7826025770378) (-7826025770137),
mkLog (24950554963215212081/62500000000000000000000) 12 (-7826025770881) (-7826025770640),
mkLog (25318230594114357341/62500000000000000000000) 12 (-7811397122761) (-7811397122520),
mkLog (29705919564998366233/3906250000000000000000) 8 (-4878986775664) (-4878986775502),
mkLog (25318231001496785781/62500000000000000000000) 12 (-7811397106670) (-7811397106429),
mkLog (124752770417129261/312500000000000000000) 12 (-7826025806142) (-7826025805901),
mkLog (12475277031528365389/31250000000000000000000) 12 (-7826025806959) (-7826025806718),
mkLog (37397544761248371/1953125000000000000000) 16 (-10863336157898) (-10863336157577),
mkLog (2531823022355303301/6250000000000000000000) 12 (-7811397137397) (-7811397137156),
mkLog (6237638513805613327/15625000000000000000000) 12 (-7826025807273) (-7826025807032),
mkLog (12475277040929498353/31250000000000000000000) 12 (-7826025806205) (-7826025805964),
mkLog (1234391185359313369/62500000000000000000000) 16 (-10832343954675) (-10832343954354),
mkLog (783427747/62500000000) 7 (-4379242996503) (-4379242996362),
mkLog (11338083871373341311/250000000000000000000000) 15 (-10001048883752) (-10001048883451),
mkLog (11338083842861718279/250000000000000000000000) 15 (-10001048886266) (-10001048885965),
mkLog (10708325369256189217/250000000000000000000000) 15 (-10058194686176) (-10058194685875),
mkLog (132120685839572726439/125000000000000000000000) 10 (-6852353224841) (-6852353224640),
mkLog (267708087038728691/6250000000000000000000) 15 (-10058194862460) (-10058194862159),
mkLog (2677080871575271203/62500000000000000000000) 15 (-10058194862016) (-10058194861715),
mkLog (264241371751612494751/250000000000000000000000) 10 (-6852353224567) (-6852353224366),
mkLog (669270335801258881/15625000000000000000000) 15 (-10058194685843) (-10058194685542),
mkLog (13212071124699280083/12500000000000000000000) 10 (-6852353032537) (-6852353032336),
mkLog (264241424039553166853/250000000000000000000000) 10 (-6852353026687) (-6852353026486),
mkLog (11337969955559485541/250000000000000000000000) 15 (-10001058930986) (-10001058930685),
mkLog (10708323482737131933/250000000000000000000000) 15 (-10058194862349) (-10058194862048),
mkLog (2267593990636703391/50000000000000000000000) 15 (-10001058931196) (-10001058930895),
mkLog (1187984293/250000000000) 8 (-5349202918471) (-5349202918310),
mkLog (589292726008808709/200000000000000000000000) 19 (-12734904876380) (-12734904875999),
mkLog (35798023461783237769/500000000000000000000000) 14 (-9544470696228) (-9544470695947),
mkLog (2946463522969046603/1000000000000000000000000) 19 (-12734904912720) (-12734904912339),
mkLog (86329761127603832119/1000000000000000000000000) 14 (-9357336162831) (-9357336162550),
mkLog (86329761124601729401/1000000000000000000000000) 14 (-9357336162865) (-9357336162584),
mkLog (46066129911831237/15625000000000000000000) 19 (-12734304782878) (-12734304782497),
mkLog (43164880558548236303/500000000000000000000000) 14 (-9357336162952) (-9357336162671),
mkLog (86329761085574394067/1000000000000000000000000) 14 (-9357336163317) (-9357336163036),
mkLog (7164596980230332381/100000000000000000000000) 14 (-9543773653811) (-9543773653530),
mkLog (2948232351883483143/1000000000000000000000000) 19 (-12734304770149) (-12734304769768),
mkLog (500350453/1000000000000) 11 (-7600201799173) (-7600201798952),
mkLog (16450053/4000000000000) 18 (-12401476220175) (-12401476219814),
mkLog (16450053/1000000000000) 16 (-11015181859035) (-11015181858714),
mkLog (1965022491026965469/500000000000000000000000) 18 (-12446859686515) (-12446859686154),
mkLog (84157321479854201161/1000000000000000000000000) 14 (-9382822636145) (-9382822635864),
mkLog (76263813298137038673/1000000000000000000000000) 14 (-9481312001017) (-9481312000736),
mkLog (76263812813937898083/1000000000000000000000000) 14 (-9481312007366) (-9481312007085),
mkLog (3930045022648404341/1000000000000000000000000) 18 (-12446859676186) (-12446859675825),
mkLog (7626381302277934559/100000000000000000000000) 14 (-9481312004627) (-9481312004346),
mkLog (1965022511568747191/500000000000000000000000) 18 (-12446859676061) (-12446859675700),
mkLog (84157287516463574039/1000000000000000000000000) 14 (-9382823039716) (-9382823039435),
mkLog (393004502705021471/100000000000000000000000) 18 (-12446859675066) (-12446859674705),
mkLog (489090041/1000000000000) 11 (-7622963952627) (-7622963952406),
mkLog (27661093665235558891/500000000000000000000000) 15 (-9802336512504) (-9802336512203),
mkLog (26474504680597970091/500000000000000000000000) 15 (-9846181195191) (-9846181194890),
mkLog (13830546829077757319/250000000000000000000000) 15 (-9802336512760) (-9802336512459),
mkLog (31837099094635840157/31250000000000000000000) 10 (-6889142407277) (-6889142407076),
mkLog (101878716627527717651/100000000000000000000000) 10 (-6889142411942) (-6889142411741),
mkLog (827328217799602363/15625000000000000000000) 15 (-9846181259820) (-9846181259519),
mkLog (254696758138030338837/250000000000000000000000) 10 (-6889142543200) (-6889142542999),
mkLog (26474502971947290367/500000000000000000000000) 15 (-9846181259731) (-9846181259430),
mkLog (13237252341478992421/250000000000000000000000) 15 (-9846181195102) (-9846181194801),
mkLog (13237252336758962919/250000000000000000000000) 15 (-9846181195459) (-9846181195158),
mkLog (101878704072249242331/100000000000000000000000) 10 (-6889142535180) (-6889142534979),
mkLog (13830581946097252199/250000000000000000000000) 15 (-9802333973672) (-9802333973371),
mkLog (2360014751/500000000000) 8 (-5355940229061) (-5355940228900),
mkLog (5666011013818822199/250000000000000000000000) 16 (-10694730851756) (-10694730851435),
mkLog (203915292300023224791/500000000000000000000000) 12 (-7804658703738) (-7804658703497),
mkLog (101957644981230715159/250000000000000000000000) 12 (-7804658715202) (-7804658714961),
mkLog (87590000902406859/4000000000000000000000) 16 (-10729138072768) (-10729138072447),
mkLog (8238237202565874521/20000000000000000000000) 12 (-7794701163350) (-7794701163109),
mkLog (203915289931126821813/500000000000000000000000) 12 (-7804658715355) (-7804658715114),
mkLog (205955935666774863719/500000000000000000000000) 12 (-7794701136147) (-7794701135906),
mkLog (749063329668374003927/100000000000000000000000) 8 (-4894101932814) (-4894101932652),
mkLog (205955932433043266003/500000000000000000000000) 12 (-7794701151848) (-7794701151607),
mkLog (203915285331206293279/500000000000000000000000) 12 (-7804658737913) (-7804658737672),
mkLog (50978821371969833951/125000000000000000000000) 12 (-7804658737145) (-7804658736904),
mkLog (10948750100267013973/500000000000000000000000) 16 (-10729138073913) (-10729138073592),
mkLog (12872245636451148459/31250000000000000000000) 12 (-7794701162772) (-7794701162531),
mkLog (101957642750206589603/250000000000000000000000) 12 (-7804658737083) (-7804658736842),
mkLog (50978821359435990549/125000000000000000000000) 12 (-7804658737391) (-7804658737150),
mkLog (11331997931323704053/500000000000000000000000) 16 (-10694732978149) (-10694732977828),
mkLog (6266921701/500000000000) 7 (-4379322821185) (-4379322821044),
mkLog (133575687217067557/2500000000000000000000) 15 (-9837133027356) (-9837133027055),
mkLog (6678784343493979851/125000000000000000000000) 15 (-9837133029955) (-9837133029654),
mkLog (238416145634615461/5000000000000000000000) 15 (-9950930812674) (-9950930812373),
mkLog (131050407124154202867/125000000000000000000000) 10 (-6860486979989) (-6860486979788),
mkLog (238416120493418359/5000000000000000000000) 15 (-9950930918125) (-9950930917824),
mkLog (65525203567165200847/62500000000000000000000) 10 (-6860486979911) (-6860486979710),
mkLog (131050433781006330159/125000000000000000000000) 10 (-6860486776580) (-6860486776379),
mkLog (65525216895591264493/62500000000000000000000) 10 (-6860486776502) (-6860486776301),
mkLog (6678726923394198607/125000000000000000000000) 15 (-9837141627380) (-9837141627079),
mkLog (3339363464390798993/62500000000000000000000) 15 (-9837141626574) (-9837141626272),
mkLog (598599931/125000000000) 8 (-5341475536216) (-5341475536055),
mkLog (3667922265084119493/1000000000000000000000000) 19 (-12515885196711) (-12515885196330),
mkLog (39412195839899649481/500000000000000000000000) 14 (-9448288070055) (-9448288069774),
mkLog (1833961132287636253/500000000000000000000000) 19 (-12515885196850) (-12515885196468),
mkLog (84131634599034825913/1000000000000000000000000) 14 (-9383127907289) (-9383127907008),
mkLog (42065817309439929203/500000000000000000000000) 14 (-9383127907053) (-9383127906772),
mkLog (1833960352734052169/500000000000000000000000) 19 (-12515885621916) (-12515885621534),
mkLog (2629113583589157093/31250000000000000000000) 14 (-9383127906387) (-9383127906106),
mkLog (84131634598017131939/1000000000000000000000000) 14 (-9383127907301) (-9383127907020),
mkLog (39412185442120317123/500000000000000000000000) 14 (-9448288333877) (-9448288333596),
mkLog (3667920710047727221/1000000000000000000000000) 19 (-12515885620667) (-12515885620285),
mkLog (508846987/1000000000000) 11 (-7583363201650) (-7583363201429),
mkLog (8364401/2000000000000) 18 (-12384673014721) (-12384673014360),
mkLog (8364401/500000000000) 16 (-10998378653581) (-10998378653260),
mkLog (2846509801/125000000000) 6 (-3782220124784) (-3782220124663),
mkLog (56796002791508866178586917282841879/2000000000000000000000000000000000000) 6 (-3561436509741) (-3561436509620),
mkLog (56796252550491133821413082717158121/2000000000000000000000000000000000000) 6 (-3561432112276) (-3561432112155),
mkLog (56796127671/500000000000) 4 (-2175139949866) (-2175139949785),
mkLog (1619759058512158590059547473710229267942254307/1000000000000000000000000000000000000000000000000) 10 (-6425477870214) (-6425477870013),
mkLog (24973957302273851696756445884969230232057745693/500000000000000000000000000000000000000000000000) 5 (-2996774524469) (-2996774524368),
mkLog (91237832833884531681468620241808523/2000000000000000000000000000000000000) 5 (-3087432814827) (-3087432814726),
mkLog (1619758238416784013237563593563294455663444627/1000000000000000000000000000000000000000000000000) 10 (-6425478376521) (-6425478376320),
mkLog (24973941494912674018477822805948723044336555373/500000000000000000000000000000000000000000000000) 5 (-2996775157423) (-2996775157322),
mkLog (4513289029/15625000000) 2 (-1241846033197) (-1241846033156),
mkLog (2209496640745955122034186422999273/1000000000000000000000000000000000000) 9 (-6114990553854) (-6114990553673),
mkLog (1305104333366953768130418613573321667842747463/500000000000000000000000000000000000000000000000) 9 (-5948325111994) (-5948325111813),
mkLog (19626198765580540013240807096135765207157252537/250000000000000000000000000000000000000000000000) 4 (-2544595572504) (-2544595572423),
mkLog (1044083628895673015195877498453040121737933109/400000000000000000000000000000000000000000000000) 9 (-5948324956641) (-5948324956460),
mkLog (15700954359137597020851484982652941278262066891/200000000000000000000000000000000000000000000000) 4 (-2544595868876) (-2544595868795),
mkLog (883809967119087828897639333053789/400000000000000000000000000000000000) 9 (-6114977755975) (-6114977755794),
mkLog (343738847789/1000000000000) 2 (-1067873073344) (-1067873073303),
mkLog (53441129431452223966644332235429/1000000000000000000000000000000000000) 15 (-9836929894540) (-9836929894239),
mkLog (5930247593850760121445830059388321/2000000000000000000000000000000000000) 9 (-5820836494738) (-5820836494557),
mkLog (11894253638300365555741553774118358469652474525140803599/200000000000000000000000000000000000000000000000000000000000) 15 (-9730017249730) (-9730017249427),
mkLog (290362736816854078195291553307882770538134870674859196401/100000000000000000000000000000000000000000000000000000000000) 9 (-5841794507090) (-5841794506909),
mkLog (290362727875093292702474542120739438911917818474859196401/100000000000000000000000000000000000000000000000000000000000) 9 (-5841794537885) (-5841794537704),
mkLog (6461318453948671216921365211005330782080294836325140803599/50000000000000000000000000000000000000000000000000000000000) 3 (-2046189613450) (-2046189613389),
mkLog (11860495748082238232070334304714791/4000000000000000000000000000000000000) 9 (-5820836447490) (-5820836447309),
mkLog (53441581206410233573904040111711/1000000000000000000000000000000000000) 15 (-9836921440882) (-9836921440581),
mkLog (41226659273/250000000000) 3 (-1802375801064) (-1802375801003),
mkLog (63807411054138250002426269420011/1000000000000000000000000000000000000) 14 (-9659641213778) (-9659641213497),
mkLog (39613709428441699491635037632896946160601803/500000000000000000000000000000000000000000000000) 14 (-9443188121510) (-9443188121229),
mkLog (1152169349935665770736355868764000803839398197/250000000000000000000000000000000000000000000000) 8 (-5379814361321) (-5379814361160),
mkLog (79227442203988734133622069329054399254666133/1000000000000000000000000000000000000000000000000) 14 (-9443187826825) (-9443187826544),
mkLog (2304339421980338445055971875118532600745333867/500000000000000000000000000000000000000000000000) 8 (-5379814047952) (-5379814047791),
mkLog (7975811952597188838302777012153/125000000000000000000000000000000000) 14 (-9659655560699) (-9659655560418),
mkLog (3864751949/200000000000) 6 (-3946419865413) (-3946419865292),
mkLog (32476500162509091007430419552050358893/125000000000000000000000000000000000000000000000) 32 (-22071062818701) (-22071062818060),
mkLog (4701901305827779821078707782770697949641107/62500000000000000000000000000000000000000000000) 14 (-9494954875796) (-9494954875515),
mkLog (507295771172753804098842064381311/4000000000000000000000000000000000000) 13 (-8972710710627) (-8972710710366),
mkLog (64953188684784300796925317445601063663/250000000000000000000000000000000000000000000000) 32 (-22071059918765) (-22071059918124),
mkLog (9403828210561205043004514600638179398936337/125000000000000000000000000000000000000000000000) 14 (-9494952153613) (-9494952153332),
mkLog (657757857/1000000000000) 11 (-7326673692958) (-7326673692737)]
private def refs0 : List (Bool × Fin 472) :=
[(false,0),
(false,1),
(false,2),
(false,3),
(false,4),
(false,5),
(false,6),
(false,7),
(false,8),
(false,0),
(true,0),
(false,9),
(false,9),
(false,10),
(false,10),
(true,1),
(false,11),
(false,12),
(false,13),
(false,14),
(false,15),
(false,16),
(false,17),
(false,18),
(false,19),
(false,20),
(true,2),
(false,21),
(false,22),
(false,23),
(false,24),
(false,23),
(false,25),
(false,26),
(false,27),
(false,28),
(false,27),
(false,29),
(false,30),
(false,31),
(false,32),
(false,33),
(false,34),
(true,3),
(false,35),
(false,36),
(false,37),
(false,38),
(false,39),
(false,40),
(false,41),
(false,42),
(false,43),
(false,44),
(false,45),
(false,46),
(false,47),
(false,38),
(false,48),
(false,38),
(false,49),
(false,50),
(false,51),
(true,4),
(false,52),
(false,53),
(false,54),
(false,55),
(false,56),
(false,57),
(false,58),
(false,59),
(false,60),
(false,61),
(false,62),
(false,60),
(false,63),
(false,60),
(false,64),
(false,65),
(true,5),
(false,66),
(false,67),
(false,68),
(false,69),
(false,70),
(false,71),
(false,72),
(false,73),
(false,74),
(false,75),
(true,6),
(false,76),
(false,76),
(false,76),
(false,76),
(true,7),
(false,8),
(true,8),
(true,8),
(false,8),
(true,77),
(true,77),
(true,77),
(true,77),
(false,78),
(true,79),
(true,80),
(true,81),
(true,82),
(true,83),
(true,84),
(true,85),
(true,86),
(true,87),
(true,88),
(false,89),
(true,90),
(true,91),
(true,92),
(true,93),
(true,94),
(true,95),
(true,96),
(true,97),
(true,98),
(true,99),
(true,100),
(true,98),
(true,101),
(true,98),
(true,102),
(true,103),
(false,104),
(true,105),
(true,106),
(true,107),
(true,108),
(true,109),
(true,110),
(true,111),
(true,112),
(true,113),
(true,114),
(true,115),
(true,116),
(true,117),
(true,108),
(true,118),
(true,108),
(true,116),
(true,119),
(true,120),
(false,121),
(true,122),
(true,123),
(true,124),
(true,125),
(true,124),
(true,126),
(true,126),
(true,124),
(true,127),
(true,124),
(true,128),
(true,129),
(true,130),
(true,126),
(true,131),
(true,130),
(false,132),
(true,133),
(true,134),
(true,135),
(true,136),
(true,137),
(true,138),
(true,139),
(true,140),
(true,141),
(true,142),
(false,143),
(true,144),
(true,144),
(true,144),
(true,144),
(false,145),
(true,146),
(false,146),
(true,147),
(false,147),
(true,148),
(true,148),
(true,149),
(true,149),
(false,150),
(true,151),
(true,152),
(true,153),
(true,154),
(true,155),
(true,156),
(true,157),
(true,158),
(true,159),
(true,160),
(false,161),
(true,162),
(true,162),
(true,163),
(true,164),
(true,163),
(true,165),
(true,166),
(true,167),
(true,168),
(true,167),
(true,169),
(true,170),
(true,171),
(true,172),
(true,173),
(true,174),
(false,175),
(true,176),
(true,177),
(true,178),
(true,179),
(true,180),
(true,181),
(true,182),
(true,183),
(true,184),
(true,185),
(true,186),
(true,187),
(true,188),
(true,179),
(true,189),
(true,179),
(true,190),
(true,191),
(true,192),
(false,193),
(true,194),
(true,195),
(true,196),
(true,197),
(true,198),
(true,199),
(true,200),
(true,201),
(true,202),
(true,203),
(true,195),
(true,202),
(true,204),
(true,202),
(true,205),
(true,206),
(false,207),
(true,208),
(true,209),
(true,210),
(true,211),
(true,212),
(true,213),
(true,214),
(true,215),
(true,216),
(true,217),
(false,218),
(true,219),
(true,219),
(true,219),
(true,219),
(false,220)]
private def refs1 : List (Bool × Fin 472) :=
[(false,221),
(false,222),
(false,223),
(false,224),
(false,225),
(false,226),
(false,227),
(false,228),
(false,229),
(false,221),
(true,221),
(false,230),
(false,230),
(false,231),
(false,231),
(true,222),
(false,232),
(false,233),
(false,234),
(false,235),
(false,236),
(false,237),
(false,238),
(false,239),
(false,240),
(false,241),
(true,223),
(false,242),
(false,243),
(false,244),
(false,245),
(false,244),
(false,246),
(false,247),
(false,244),
(false,248),
(false,249),
(false,250),
(false,251),
(false,252),
(false,253),
(false,246),
(false,254),
(true,224),
(false,255),
(false,256),
(false,257),
(false,258),
(false,259),
(false,258),
(false,260),
(false,261),
(false,262),
(false,263),
(false,264),
(false,265),
(false,266),
(false,267),
(false,268),
(false,258),
(false,269),
(false,270),
(false,271),
(true,225),
(false,272),
(false,273),
(false,274),
(false,275),
(false,276),
(false,277),
(false,278),
(false,279),
(false,280),
(false,281),
(false,282),
(false,283),
(false,284),
(false,283),
(false,285),
(false,285),
(true,226),
(false,286),
(false,287),
(false,288),
(false,289),
(false,290),
(false,291),
(false,292),
(false,293),
(false,294),
(false,295),
(true,227),
(false,296),
(false,296),
(false,296),
(false,296),
(true,228),
(false,229),
(true,229),
(true,229),
(false,229),
(true,297),
(true,297),
(true,297),
(true,297),
(false,298),
(true,299),
(true,300),
(true,301),
(true,302),
(true,303),
(true,304),
(true,305),
(true,306),
(true,307),
(true,308),
(false,309),
(true,310),
(true,311),
(true,312),
(true,313),
(true,314),
(true,315),
(true,316),
(true,317),
(true,316),
(true,318),
(true,319),
(true,320),
(true,321),
(true,320),
(true,322),
(true,322),
(false,323),
(true,324),
(true,325),
(true,326),
(true,327),
(true,328),
(true,327),
(true,329),
(true,330),
(true,331),
(true,332),
(true,333),
(true,334),
(true,335),
(true,336),
(true,337),
(true,327),
(true,338),
(true,339),
(true,340),
(false,341),
(true,342),
(true,343),
(true,344),
(true,345),
(true,344),
(true,346),
(true,347),
(true,344),
(true,348),
(true,349),
(true,350),
(true,351),
(true,352),
(true,353),
(true,346),
(true,354),
(false,355),
(true,356),
(true,357),
(true,358),
(true,359),
(true,360),
(true,361),
(true,362),
(true,363),
(true,364),
(true,365),
(false,366),
(true,219),
(true,219),
(true,219),
(true,219),
(false,220),
(true,8),
(false,8),
(true,367),
(true,367),
(true,367),
(true,367),
(false,368),
(true,369),
(true,370),
(true,371),
(true,372),
(true,373),
(true,374),
(true,372),
(true,375),
(true,376),
(true,377),
(false,378),
(true,379),
(true,380),
(true,380),
(true,381),
(true,382),
(true,383),
(true,384),
(true,385),
(true,386),
(true,387),
(true,388),
(true,386),
(true,389),
(true,386),
(true,390),
(true,390),
(false,391),
(true,392),
(true,393),
(true,394),
(true,395),
(true,396),
(true,395),
(true,397),
(true,394),
(true,398),
(true,399),
(true,400),
(true,401),
(true,402),
(true,403),
(true,404),
(true,395),
(true,405),
(true,406),
(true,407),
(false,408),
(true,409),
(true,410),
(true,411),
(true,412),
(true,411),
(true,413),
(true,413),
(true,411),
(true,414),
(true,411),
(true,415),
(true,416),
(true,417),
(true,413),
(true,413),
(true,418),
(false,419),
(true,420),
(true,421),
(true,422),
(true,423),
(true,424),
(true,425),
(true,426),
(true,427),
(true,428),
(true,429),
(false,430),
(true,431),
(true,431),
(true,431),
(true,431),
(false,432),
(true,146),
(false,146),
(true,433),
(false,433),
(true,434),
(true,434),
(true,435),
(true,435),
(false,436),
(true,437),
(true,438),
(true,437),
(true,439),
(true,439),
(true,440),
(true,439),
(true,439),
(true,441),
(true,440),
(false,442),
(true,443),
(true,443),
(true,444),
(true,445),
(true,444),
(true,446),
(true,446),
(true,444),
(true,445),
(true,444),
(true,447),
(true,447),
(true,448),
(true,446),
(true,446),
(true,448),
(false,449),
(true,450),
(true,451),
(true,451),
(true,452),
(true,453),
(true,452),
(true,451),
(true,451),
(true,454),
(true,455),
(true,454),
(true,456),
(true,456),
(true,452),
(true,453),
(true,452),
(true,456),
(true,456),
(true,457),
(false,458),
(true,459),
(true,460),
(true,460),
(true,459),
(true,461),
(true,461),
(true,462),
(true,463),
(true,462),
(true,460),
(true,460),
(true,462),
(true,463),
(true,462),
(true,464),
(true,464),
(false,465),
(true,466),
(true,467),
(true,468),
(true,468),
(true,466),
(true,468),
(true,468),
(true,469),
(true,470),
(true,469),
(false,471)]
def entriesOwner0 (i : Fin 2) : List Entry :=
((![(refs0),(refs1)] i).map (fun p ↦
let e := logTable p.2
((if p.1 then e.1.1 else -e.1.1,e.1.2),e.2)))
end MME.ReleasedGlobalYZ
Source
Exact released global candidate from primitive seed f8187420c24231b83d9d1fb7b327fee76cd50ada0af0525e77b3d3b0d8f4d4e6.