Exact global Y/Z certificate: logs 1
Definitionmme_released_global_yz_logs_1matrix-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 (2884311719/125000000000) 6 (-3769027438136) (-3769027438015),
mkLog (113875467179/1000000000000) 4 (-2172649820891) (-2172649820810),
mkLog (289598989021/1000000000000) 2 (-1239258109447) (-1239258109406),
mkLog (88189275717/250000000000) 2 (-1041975552773) (-1041975552732),
mkLog (95040352963/500000000000) 3 (-1660306529009) (-1660306528948),
mkLog (7230066443/250000000000) 6 (-3543212691891) (-3543212691770),
mkLog (829856839/500000000000) 10 (-6401110174724) (-6401110174523),
mkLog (16571039/500000000000) 15 (-10314706844402) (-10314706844101),
mkLog (59863/500000000000) 23 (-15938060038510) (-15938060038049),
mkLog (11387489797936941344020649536507331/400000000000000000000000000000000000) 6 (-3558949180483) (-3558949180362),
mkLog (11387603637863058655979350463492669/400000000000000000000000000000000000) 6 (-3558939183604) (-3558939183483),
mkLog (346510797996724900538839747941225361403226109/200000000000000000000000000000000000000000000000) 10 (-6358158664437) (-6358158664236),
mkLog (4983163899936995406673057789805405038596773891/100000000000000000000000000000000000000000000000) 5 (-2999105175461) (-2999105175360),
mkLog (346510798071959362991839747941225361403226109/200000000000000000000000000000000000000000000000) 10 (-6358158664220) (-6358158664019),
mkLog (183005585451768223037603999004266061/4000000000000000000000000000000000000) 5 (-3084532966183) (-3084532966082),
mkLog (183005585454550207982007999004266061/4000000000000000000000000000000000000) 5 (-3084532966168) (-3084532966067),
mkLog (1353557968616958871144361354014189552699601/781250000000000000000000000000000000000000000) 10 (-6358158543318) (-6358158543117),
mkLog (183005585451881242246911999004266061/4000000000000000000000000000000000000) 5 (-3084532966182) (-3084532966081),
mkLog (183005585447350826071463999004266061/4000000000000000000000000000000000000) 5 (-3084532966207) (-3084532966106),
mkLog (19465448511803272414546273653121605369175399/390625000000000000000000000000000000000000000) 5 (-2999106997782) (-2999106997681),
mkLog (1353557968635089878762330104014189552699601/781250000000000000000000000000000000000000000) 10 (-6358158543304) (-6358158543103),
mkLog (462885531459764057721229867360839/200000000000000000000000000000000000) 9 (-6068592854370) (-6068592854189),
mkLog (462885531454024420562829867360839/200000000000000000000000000000000000) 9 (-6068592854383) (-6068592854202),
mkLog (2740540561838847944179587994992999435155687437/1000000000000000000000000000000000000000000000000) 9 (-5899600092789) (-5899600092608),
mkLog (40196881806521779638400373372043471064844312563/500000000000000000000000000000000000000000000000) 4 (-2520818672848) (-2520818672767),
mkLog (2740540561843577083367587994992999435155687437/1000000000000000000000000000000000000000000000000) 9 (-5899600092787) (-5899600092606),
mkLog (1370270537567249828631512910477144109049439977/500000000000000000000000000000000000000000000000) 9 (-5899599905491) (-5899599905310),
mkLog (1370270537548171596547512910477144109049439977/500000000000000000000000000000000000000000000000) 9 (-5899599905505) (-5899599905324),
mkLog (2740540561853156618242587994992999435155687437/1000000000000000000000000000000000000000000000000) 9 (-5899600092783) (-5899600092602),
mkLog (40196881804540613810845373372043471064844312563/500000000000000000000000000000000000000000000000) 4 (-2520818672898) (-2520818672817),
mkLog (20098435534294985149332367812636275140950560023/250000000000000000000000000000000000000000000000) 4 (-2520818939982) (-2520818939901),
mkLog (20098435533487474731863617812636275140950560023/250000000000000000000000000000000000000000000000) 4 (-2520818940022) (-2520818939941),
mkLog (2314454756127514856951405036669187/1000000000000000000000000000000000000) 9 (-6068581145786) (-6068581145605),
mkLog (1370270537569634607642012910477144109049439977/500000000000000000000000000000000000000000000000) 9 (-5899599905490) (-5899599905309),
mkLog (1370270537569614398225512910477144109049439977/500000000000000000000000000000000000000000000000) 9 (-5899599905490) (-5899599905309),
mkLog (2314454756160416737102405036669187/1000000000000000000000000000000000000) 9 (-6068581145772) (-6068581145591),
mkLog (96385846781107003100898036983123/1000000000000000000000000000000000000) 14 (-9247151184891) (-9247151184610),
mkLog (15757776845022194906002054175207071/4000000000000000000000000000000000000) 8 (-5536715628837) (-5536715628676),
mkLog (15757776846214742189934054175207071/4000000000000000000000000000000000000) 8 (-5536715628761) (-5536715628600),
mkLog (9697123452411066599031021922494665412439322747617156461/100000000000000000000000000000000000000000000000000000000000) 14 (-9241096174880) (-9241096174599),
mkLog (204894304888369379841077714898692183574666026652382843539/50000000000000000000000000000000000000000000000000000000000) 8 (-5497284024223) (-5497284024062),
mkLog (9697123458678841736531021922494665412439322747617156461/100000000000000000000000000000000000000000000000000000000000) 14 (-9241096174234) (-9241096173953),
mkLog (15757776846325892134602054175207071/4000000000000000000000000000000000000) 8 (-5536715628754) (-5536715628593),
mkLog (15757776845584624660570054175207071/4000000000000000000000000000000000000) 8 (-5536715628801) (-5536715628640),
mkLog (204894300499172690198485671930661731922704455702382843539/50000000000000000000000000000000000000000000000000000000000) 8 (-5497284045645) (-5497284045484),
mkLog (3539823772348772050366778122387848269090190194897617156461/25000000000000000000000000000000000000000000000000000000000) 3 (-1954798880815) (-1954798880754),
mkLog (204894300779804945638885671930661731922704455702382843539/50000000000000000000000000000000000000000000000000000000000) 8 (-5497284044275) (-5497284044114),
mkLog (7878888814722063036025863729249199/2000000000000000000000000000000000000) 8 (-5536715579057) (-5536715578896),
mkLog (7878888814665994175397863729249199/2000000000000000000000000000000000000) 8 (-5536715579064) (-5536715578903),
mkLog (204894304935034901627627714898692183574666026652382843539/50000000000000000000000000000000000000000000000000000000000) 8 (-5497284023996) (-5497284023835),
mkLog (7878888793979372891883863729249199/2000000000000000000000000000000000000) 8 (-5536715581689) (-5536715581528),
mkLog (7878888814695016382299863729249199/2000000000000000000000000000000000000) 8 (-5536715579060) (-5536715578899),
mkLog (48192780121582752594709541861767/500000000000000000000000000000000000) 14 (-9247154157717) (-9247154157436),
mkLog (170635380638036279106087820094329/1000000000000000000000000000000000000) 13 (-8675981555103) (-8675981554842),
mkLog (188966747670074028957913334205767534783815861/1000000000000000000000000000000000000000000000000) 13 (-8573939496768) (-8573939496507),
mkLog (188966747679609709126913334205767534783815861/1000000000000000000000000000000000000000000000000) 13 (-8573939496718) (-8573939496457),
mkLog (170635380543261033026087820094329/1000000000000000000000000000000000000) 13 (-8675981555658) (-8675981555397),
mkLog (3340748764835460226158588031738348465216184139/500000000000000000000000000000000000000000000000) 8 (-5008413135551) (-5008413135390),
mkLog (3340748764627209923078088031738348465216184139/500000000000000000000000000000000000000000000000) 8 (-5008413135613) (-5008413135452),
mkLog (188966764369889249026798507070852653433008721/1000000000000000000000000000000000000000000000000) 13 (-8573939408394) (-8573939408133),
mkLog (3340749424041574902248740568537110846566991279/500000000000000000000000000000000000000000000000) 8 (-5008412938228) (-5008412938067),
mkLog (188966764355731117675798507070852653433008721/1000000000000000000000000000000000000000000000000) 13 (-8573939408469) (-8573939408208),
mkLog (188966764478370305427798507070852653433008721/1000000000000000000000000000000000000000000000000) 13 (-8573939407820) (-8573939407559),
mkLog (3340749423809088435217740568537110846566991279/500000000000000000000000000000000000000000000000) 8 (-5008412938298) (-5008412938137),
mkLog (21329262994328289810353912100189/125000000000000000000000000000000000) 13 (-8675989037069) (-8675989036808),
mkLog (82531374380040706803211337449165761249239/10000000000000000000000000000000000000000000000) 17 (-11704917134567) (-11704917134226),
mkLog (1174216216565664930006672531983834238750761/5000000000000000000000000000000000000000000000) 13 (-8356592316259) (-8356592315998),
mkLog (2892517430448526708508674070971/10000000000000000000000000000000000) 12 (-8148213165946) (-8148213165705),
mkLog (2892517431000183265918674070971/10000000000000000000000000000000000) 12 (-8148213165755) (-8148213165514),
mkLog (82531374935252265043211337449165761249239/10000000000000000000000000000000000000000000000) 17 (-11704917127840) (-11704917127499),
mkLog (2892517431205866316718674070971/10000000000000000000000000000000000) 12 (-8148213165684) (-8148213165443),
mkLog (2892517429674482978898674070971/10000000000000000000000000000000000) 12 (-8148213166213) (-8148213165972),
mkLog (82532900134187933026862422780458050386333/10000000000000000000000000000000000000000000000) 17 (-11704898647779) (-11704898647438),
mkLog (1174253037507684919520905565844541949613667/5000000000000000000000000000000000000000000000) 13 (-8356560958862) (-8356560958600),
mkLog (82532900074760126026862422780458050386333/10000000000000000000000000000000000000000000000) 17 (-11704898648499) (-11704898648158),
mkLog (16571039/2000000000000) 17 (-11701001205542) (-11701001205201),
mkLog (4113743/1000000000000) 18 (-12401177238482) (-12401177238121),
mkLog (4113743/250000000000) 16 (-11014882877342) (-11014882877021),
mkLog (1946290724796102381/500000000000000000000000) 18 (-12456438008888) (-12456438008527),
mkLog (88537874556530772171/1000000000000000000000000) 14 (-9332080136550) (-9332080136269),
mkLog (19019555311622785209/250000000000000000000000) 14 (-9483748520183) (-9483748519902),
mkLog (38039110650578194803/500000000000000000000000) 14 (-9483748519464) (-9483748519183),
mkLog (1946290762564819713/500000000000000000000000) 18 (-12456437989482) (-12456437989121),
mkLog (38039110610821650243/500000000000000000000000) 14 (-9483748520509) (-9483748520228),
mkLog (38039110611815563857/500000000000000000000000) 14 (-9483748520483) (-9483748520202),
mkLog (243283067455623093/62500000000000000000000) 18 (-12456451462853) (-12456451462492),
mkLog (88535826326190708549/1000000000000000000000000) 14 (-9332103270763) (-9332103270482),
mkLog (1946264535172373481/500000000000000000000000) 18 (-12456451465151) (-12456451464790),
mkLog (496956807/1000000000000) 11 (-7607007443200) (-7607007442979),
mkLog (28253128824031523321/500000000000000000000000) 15 (-9781159171263) (-9781159170962),
mkLog (52453252903588672499/1000000000000000000000000) 15 (-9855588206062) (-9855588205761),
mkLog (26226626449434647691/500000000000000000000000) 15 (-9855588206152) (-9855588205851),
mkLog (28253128805154014853/500000000000000000000000) 15 (-9781159171931) (-9781159171630),
mkLog (1018431436447872140239/1000000000000000000000000) 10 (-6889491642830) (-6889491642629),
mkLog (127303929525897988409/125000000000000000000000) 10 (-6889491643067) (-6889491642866),
mkLog (52453249524514656727/1000000000000000000000000) 15 (-9855588270483) (-9855588270182),
mkLog (5092156482190556051/5000000000000000000000) 10 (-6889491780306) (-6889491780105),
mkLog (819582023599320709/15625000000000000000000) 15 (-9855588270753) (-9855588270452),
mkLog (13113312410624771163/250000000000000000000000) 15 (-9855588268234) (-9855588267933),
mkLog (509215645392148712017/500000000000000000000000) 10 (-6889491785858) (-6889491785657),
mkLog (5650656603104137989/100000000000000000000000) 15 (-9781153713777) (-9781153713475),
mkLog (4719377117/1000000000000) 8 (-5356078454911) (-5356078454750),
mkLog (699820852700599609/31250000000000000000000) 16 (-10706705556732) (-10706705556411),
mkLog (4889809726785506749/12500000000000000000000) 12 (-7846330531360) (-7846330531119),
mkLog (12224524321187975229/31250000000000000000000) 12 (-7846330531014) (-7846330530773),
mkLog (139347350407043179/6250000000000000000000) 16 (-10711122282070) (-10711122281749),
mkLog (11878035702912271063/31250000000000000000000) 12 (-7875083699895) (-7875083699654),
mkLog (3056131078184889629/7812500000000000000000) 12 (-7846330531705) (-7846330531464),
mkLog (23756071786003294211/62500000000000000000000) 12 (-7875083683891) (-7875083683650),
mkLog (29315501920862894621/3906250000000000000000) 8 (-4892216661657) (-4892216661495),
mkLog (11878035839623014237/31250000000000000000000) 12 (-7875083688385) (-7875083688144),
mkLog (24449047744539665231/62500000000000000000000) 12 (-7846330567737) (-7846330567496),
mkLog (24449047753756119827/62500000000000000000000) 12 (-7846330567360) (-7846330567119),
mkLog (23756071388159670817/62500000000000000000000) 12 (-7875083700638) (-7875083700397),
mkLog (195592382066914777/500000000000000000000) 12 (-7846330567171) (-7846330566930),
mkLog (24449047747611816763/62500000000000000000000) 12 (-7846330567611) (-7846330567370),
mkLog (349911186323785033/15625000000000000000000) 16 (-10706703384826) (-10706703384505),
mkLog (768037883/62500000000) 7 (-4399082777041) (-4399082776900),
mkLog (823357732665758153/15625000000000000000000) 15 (-9850991978407) (-9850991978106),
mkLog (6586861862508350021/125000000000000000000000) 15 (-9850991978227) (-9850991977926),
mkLog (11646169099816661109/250000000000000000000000) 15 (-9974238903695) (-9974238903394),
mkLog (32388146326720090259/31250000000000000000000) 10 (-6871982153522) (-6871982153321),
mkLog (5823084550499472953/125000000000000000000000) 15 (-9974238903594) (-9974238903293),
mkLog (11646167506096754753/250000000000000000000000) 15 (-9974239040540) (-9974239040239),
mkLog (259105169463397614591/250000000000000000000000) 10 (-6871982157962) (-6871982157761),
mkLog (129552610176241065931/125000000000000000000000) 10 (-6871981961558) (-6871981961357),
mkLog (32388152547902692073/31250000000000000000000) 10 (-6871981961440) (-6871981961239),
mkLog (13173611149040614499/250000000000000000000000) 15 (-9851000523757) (-9851000523456),
mkLog (232923350145580791/5000000000000000000000) 15 (-9974239040439) (-9974239040138),
mkLog (13173611163228032063/250000000000000000000000) 15 (-9851000522681) (-9851000522380),
mkLog (1182284797/250000000000) 8 (-5354012082973) (-5354012082812),
mkLog (69269073244973407/20000000000000000000000) 19 (-12573244298645) (-12573244298264),
mkLog (3126279220587959159/40000000000000000000000) 14 (-9456791183222) (-9456791182941),
mkLog (138538158177836083/40000000000000000000000) 19 (-12573244214279) (-12573244213898),
mkLog (332753344535958447/4000000000000000000000) 14 (-9394403410803) (-9394403410522),
mkLog (3327533460869675049/40000000000000000000000) 14 (-9394403406142) (-9394403405861),
mkLog (138538145383520119/40000000000000000000000) 19 (-12573244306631) (-12573244306250),
mkLog (3327533445580869809/40000000000000000000000) 14 (-9394403410737) (-9394403410456),
mkLog (3327533445741804601/40000000000000000000000) 14 (-9394403410688) (-9394403410407),
mkLog (1563141693222700313/20000000000000000000000) 14 (-9456789850694) (-9456789850413),
mkLog (13853814536340327/4000000000000000000000) 19 (-12573244306777) (-12573244306395),
mkLog (20116849/40000000000) 11 (-7595077010578) (-7595077010357),
mkLog (3317013/800000000000) 18 (-12393302327670) (-12393302327309),
mkLog (3317013/200000000000) 16 (-11007007966530) (-11007007966209),
mkLog (119927/1000000000000) 23 (-15936382612839) (-15936382612378),
mkLog (922974953/40000000000) 6 (-3769032635534) (-3769032635413),
mkLog (11385831291436941344020649536507331/400000000000000000000000000000000000) 6 (-3559094833943) (-3559094833822),
mkLog (11385945131363058655979350463492669/400000000000000000000000000000000000) 6 (-3559084835608) (-3559084835487),
mkLog (56929441057/500000000000) 4 (-2172795473623) (-2172795473542),
mkLog (345818107264275166468839747941225361403226109/200000000000000000000000000000000000000000000000) 10 (-6360159710351) (-6360159710150),
mkLog (4975348201885525508775557789805405038596773891/100000000000000000000000000000000000000000000000) 5 (-3000674827549) (-3000674827448),
mkLog (345818107281070182576839747941225361403226109/200000000000000000000000000000000000000000000000) 10 (-6360159710303) (-6360159710102),
mkLog (182672832107232264590603999004266061/4000000000000000000000000000000000000) 5 (-3086352890031) (-3086352889930),
mkLog (182672832108463240477107999004266061/4000000000000000000000000000000000000) 5 (-3086352890024) (-3086352889923),
mkLog (1350852145464936993820142604014189552699601/781250000000000000000000000000000000000000000) 10 (-6360159588973) (-6360159588772),
mkLog (182672832107323155266011999004266061/4000000000000000000000000000000000000) 5 (-3086352890030) (-3086352889929),
mkLog (182672832102776645611363999004266061/4000000000000000000000000000000000000) 5 (-3086352890055) (-3086352889954),
mkLog (19434918400607516549057992403121605369175399/390625000000000000000000000000000000000000000) 5 (-3000676654826) (-3000676654725),
mkLog (1350852145483460908645142604014189552699601/781250000000000000000000000000000000000000000) 10 (-6360159588960) (-6360159588758),
mkLog (72274016949/250000000000) 2 (-1240996231609) (-1240996231568),
mkLog (452346552481642353362829867360839/200000000000000000000000000000000000) 9 (-6091624050530) (-6091624050349),
mkLog (452346552474011060529229867360839/200000000000000000000000000000000000) 9 (-6091624050547) (-6091624050366),
mkLog (2693955885439581299743587994992999435155687437/1000000000000000000000000000000000000000000000000) 9 (-5916744576334) (-5916744576153),
mkLog (39678671465294258194256373372043471064844312563/500000000000000000000000000000000000000000000000) 4 (-2533794297824) (-2533794297743),
mkLog (1346978202555056319125512910477144109049439977/500000000000000000000000000000000000000000000000) 9 (-5916744383432) (-5916744383251),
mkLog (1346978202535978087041512910477144109049439977/500000000000000000000000000000000000000000000000) 9 (-5916744383446) (-5916744383265),
mkLog (2693955885453889973806587994992999435155687437/1000000000000000000000000000000000000000000000000) 9 (-5916744576329) (-5916744576148),
mkLog (39678671465613818581663373372043471064844312563/500000000000000000000000000000000000000000000000) 4 (-2533794297816) (-2533794297735),
mkLog (19839330313942503017470367812636275140950560023/250000000000000000000000000000000000000000000000) 4 (-2533794570954) (-2533794570873),
mkLog (19839330313104253195279617812636275140950560023/250000000000000000000000000000000000000000000000) 4 (-2533794570996) (-2533794570915),
mkLog (2261760311531352398955405036669187/1000000000000000000000000000000000000) 9 (-6091611870066) (-6091611869885),
mkLog (1346978202557441098136012910477144109049439977/500000000000000000000000000000000000000000000000) 9 (-5916744383430) (-5916744383249),
mkLog (2261760311507504608850405036669187/1000000000000000000000000000000000000) 9 (-6091611870076) (-6091611869895),
mkLog (2175174773/6250000000) 2 (-1055472447054) (-1055472447013),
mkLog (73991579494687815612898036983123/1000000000000000000000000000000000000) 14 (-9511559261988) (-9511559261707),
mkLog (14193037732450832746322054175207071/4000000000000000000000000000000000000) 9 (-5641298096354) (-5641298096173),
mkLog (14193037733102681360622054175207071/4000000000000000000000000000000000000) 9 (-5641298096308) (-5641298096127),
mkLog (7467565845898375735031021922494665412439322747617156461/100000000000000000000000000000000000000000000000000000000000) 14 (-9502356376379) (-9502356376098),
mkLog (185889447763709746140277714898692183574666026652382843539/50000000000000000000000000000000000000000000000000000000000) 9 (-5594626154356) (-5594626154174),
mkLog (7467565852166150872531021922494665412439322747617156461/100000000000000000000000000000000000000000000000000000000000) 14 (-9502356375540) (-9502356375259),
mkLog (14193037733754529974922054175207071/4000000000000000000000000000000000000) 9 (-5641298096262) (-5641298096081),
mkLog (14193037733553961170522054175207071/4000000000000000000000000000000000000) 9 (-5641298096276) (-5641298096095),
mkLog (185889443070370054829685671930661731922704455702382843539/50000000000000000000000000000000000000000000000000000000000) 9 (-5594626179604) (-5594626179422),
mkLog (3352204560055249524792378122387848269090190194897617156461/25000000000000000000000000000000000000000000000000000000000) 3 (-2009257617872) (-2009257617811),
mkLog (185889443436408122859685671930661731922704455702382843539/50000000000000000000000000000000000000000000000000000000000) 9 (-5594626177635) (-5594626177453),
mkLog (7096519286896793748633863729249199/2000000000000000000000000000000000000) 9 (-5641298037075) (-5641298036894),
mkLog (7096519286545798340933863729249199/2000000000000000000000000000000000000) 9 (-5641298037125) (-5641298036944),
mkLog (185889447824507164974027714898692183574666026652382843539/50000000000000000000000000000000000000000000000000000000000) 9 (-5594626154029) (-5594626153847),
mkLog (7096519265711713783883863729249199/2000000000000000000000000000000000000) 9 (-5641298040061) (-5641298039880),
mkLog (7096519286771438245883863729249199/2000000000000000000000000000000000000) 9 (-5641298037093) (-5641298036912),
mkLog (36995622159221631538709541861767/500000000000000000000000000000000000) 14 (-9511563791923) (-9511563791642),
mkLog (88896049899/500000000000) 3 (-1727140390002) (-1727140389941),
mkLog (114129122989973232464087820094329/1000000000000000000000000000000000000) 14 (-9078180092877) (-9078180092596),
mkLog (136513494766485356458913334205767534783815861/1000000000000000000000000000000000000000000000000) 13 (-8899087085599) (-8899087085338),
mkLog (136513494780740413744913334205767534783815861/1000000000000000000000000000000000000000000000000) 13 (-8899087085495) (-8899087085234),
mkLog (114129122932953003320087820094329/1000000000000000000000000000000000000) 14 (-9078180093377) (-9078180093096),
mkLog (2831533046611524156039088031738348465216184139/500000000000000000000000000000000000000000000000) 8 (-5173789820938) (-5173789820777),
mkLog (2831533046523617969442088031738348465216184139/500000000000000000000000000000000000000000000000) 8 (-5173789820969) (-5173789820808),
mkLog (136513514845374592299798507070852653433008721/1000000000000000000000000000000000000000000000000) 13 (-8899086938515) (-8899086938254),
mkLog (2831533775822519297148740568537110846566991279/500000000000000000000000000000000000000000000000) 8 (-5173789563406) (-5173789563245),
mkLog (136513514835871220775798507070852653433008721/1000000000000000000000000000000000000000000000000) 13 (-8899086938585) (-8899086938324),
mkLog (2831533778416939723200740568537110846566991279/500000000000000000000000000000000000000000000000) 8 (-5173789562489) (-5173789562328),
mkLog (14265942240448117324103912100189/125000000000000000000000000000000000) 14 (-9078193981334) (-9078193981053),
mkLog (4840177731/200000000000) 6 (-3721365925274) (-3721365925153),
mkLog (43605559884118659183211337449165761249239/10000000000000000000000000000000000000000000000) 18 (-12342910988637) (-12342910988276),
mkLog (731526843783011069151672531983834238750761/5000000000000000000000000000000000000000000000) 13 (-8829814553842) (-8829814553581),
mkLog (2131735217983615300148674070971/10000000000000000000000000000000000) 13 (-8453404067708) (-8453404067447),
mkLog (2131735217988619369858674070971/10000000000000000000000000000000000) 13 (-8453404067706) (-8453404067445),
mkLog (43605559683955870783211337449165761249239/10000000000000000000000000000000000000000000000) 18 (-12342910993227) (-12342910992866),
mkLog (2131735218989433311858674070971/10000000000000000000000000000000000) 13 (-8453404067236) (-8453404066975),
mkLog (2131735217438171701758674070971/10000000000000000000000000000000000) 13 (-8453404067964) (-8453404067703),
mkLog (43607609341288238146862422780458050386333/10000000000000000000000000000000000000000000000) 18 (-12342863989836) (-12342863989475),
mkLog (731573905876731376775905565844541949613667/5000000000000000000000000000000000000000000000) 13 (-8829750221849) (-8829750221588),
mkLog (43607609371312656406862422780458050386333/10000000000000000000000000000000000000000000000) 18 (-12342863989148) (-12342863988787),
mkLog (1162756871/1000000000000) 10 (-6756961480712) (-6756961480511),
mkLog (8343553/2000000000000) 18 (-12387168593871) (-12387168593510),
mkLog (8343553/500000000000) 16 (-11000874232731) (-11000874232410),
mkLog (4554056031/200000000000) 6 (-3782299095354) (-3782299095233),
mkLog (56813400619/500000000000) 4 (-2174835874171) (-2174835874090),
mkLog (289860368551/1000000000000) 2 (-1238355959730) (-1238355959689),
mkLog (14131140093/40000000000) 2 (-1040498574706) (-1040498574665),
mkLog (37995290503/200000000000) 3 (-1660855148664) (-1660855148603),
mkLog (2881377971/100000000000) 6 (-3546901544175) (-3546901544054),
mkLog (820312699/500000000000) 10 (-6412677769695) (-6412677769494),
mkLog (33069231/1000000000000) 15 (-10316907285097) (-10316907284796),
mkLog (120877/1000000000000) 23 (-15928492337523) (-15928492337062),
mkLog (56813391925709870048317497118221257/2000000000000000000000000000000000000) 6 (-3561130388326) (-3561130388205),
mkLog (56813409312290129951682502881778743/2000000000000000000000000000000000000) 6 (-3561130082296) (-3561130082175),
mkLog (101059059783596673476596197878979004270105229/62500000000000000000000000000000000000000000000) 10 (-6427216739551) (-6427216739350),
mkLog (1566215319965501280346297604117212683229894771/31250000000000000000000000000000000000000000000) 5 (-2993357291331) (-2993357291230),
mkLog (101059059783377219514908697878979004270105229/62500000000000000000000000000000000000000000000) 10 (-6427216739554) (-6427216739353),
mkLog (18315481055029036565321117530374449/400000000000000000000000000000000000) 5 (-3083717885642) (-3083717885541),
mkLog (18315481055093325844593517530374449/400000000000000000000000000000000000) 5 (-3083717885639) (-3083717885538),
mkLog (4042362692740799373994273226775244924998011/2500000000000000000000000000000000000000000000) 10 (-6427216664992) (-6427216664791),
mkLog (18315481055046169785059517530374449/400000000000000000000000000000000000) 5 (-3083717885641) (-3083717885540),
mkLog (18315481055052889595500717530374449/400000000000000000000000000000000000) 5 (-3083717885641) (-3083717885540),
mkLog (62648609617852424944028505563696475075001989/1250000000000000000000000000000000000000000000) 5 (-2993357342103) (-2993357342002),
mkLog (4042362692751406400116773226775244924998011/2500000000000000000000000000000000000000000000) 10 (-6427216664989) (-6427216664788),
mkLog (2307838788400549250141515443082593/1000000000000000000000000000000000000) 9 (-6071443781913) (-6071443781732),
mkLog (2307838788371817456701515443082593/1000000000000000000000000000000000000) 9 (-6071443781926) (-6071443781745),
mkLog (540111477332584153907908456213713278418893769/200000000000000000000000000000000000000000000000) 9 (-5914297087864) (-5914297087683),
mkLog (8061067610774486407192473902512843071581106231/100000000000000000000000000000000000000000000000) 4 (-2518124180370) (-2518124180289),
mkLog (540111477330683479603108456213713278418893769/200000000000000000000000000000000000000000000000) 9 (-5914297087867) (-5914297087686),
mkLog (84392410070817788368150335589266914095249249/31250000000000000000000000000000000000000000000) 9 (-5914297185768) (-5914297185587),
mkLog (8061067610643481533422073902512843071581106231/100000000000000000000000000000000000000000000000) 4 (-2518124180386) (-2518124180305),
mkLog (540111477329710974563908456213713278418893769/200000000000000000000000000000000000000000000000) 9 (-5914297087869) (-5914297087688),
mkLog (1259542216730117105803542817224390648404750751/15625000000000000000000000000000000000000000000) 4 (-2518123860772) (-2518123860691),
mkLog (1259542216722763153003449067224390648404750751/15625000000000000000000000000000000000000000000) 4 (-2518123860778) (-2518123860697),
mkLog (4615610757347515959428598379155519/2000000000000000000000000000000000000) 9 (-6071458258648) (-6071458258467),
mkLog (84392410070372317827962835589266914095249249/31250000000000000000000000000000000000000000000) 9 (-5914297185774) (-5914297185593),
mkLog (4615610757423247359796598379155519/2000000000000000000000000000000000000) 9 (-6071458258631) (-6071458258450),
mkLog (47908484240145308871263211654037/500000000000000000000000000000000000) 14 (-9253070764802) (-9253070764521),
mkLog (471560472256434879591172446648833/125000000000000000000000000000000000) 9 (-5580021667475) (-5580021667293),
mkLog (471560470951169789770172446648833/125000000000000000000000000000000000) 9 (-5580021670243) (-5580021670061),
mkLog (50301376510028360048912146933521594720608952298476555109/500000000000000000000000000000000000000000000000000000000000) 14 (-9204330934810) (-9204330934529),
mkLog (929436048242168168633453015397443935067455772701523444891/250000000000000000000000000000000000000000000000000000000000) 9 (-5594638194462) (-5594638194281),
mkLog (471560472242332385531797446648833/125000000000000000000000000000000000) 9 (-5580021667505) (-5580021667323),
mkLog (471560472262702785791047446648833/125000000000000000000000000000000000) 9 (-5580021667462) (-5580021667280),
mkLog (929436078543348045255850473375587491256458044451523444891/250000000000000000000000000000000000000000000000000000000000) 9 (-5594638161861) (-5594638161679),
mkLog (18041444935786597765119448531693313853955477230548476555109/125000000000000000000000000000000000000000000000000000000000) 3 (-1935642129687) (-1935642129626),
mkLog (929436078502457833629850473375587491256458044451523444891/250000000000000000000000000000000000000000000000000000000000) 9 (-5594638161905) (-5594638161723),
mkLog (15089938183314697843779987927561667/4000000000000000000000000000000000000) 9 (-5580021463955) (-5580021463773),
mkLog (15089938183013886577139987927561667/4000000000000000000000000000000000000) 9 (-5580021463975) (-5580021463793),
mkLog (50301376566436239288412146933521594720608952298476555109/500000000000000000000000000000000000000000000000000000000000) 14 (-9204330933688) (-9204330933407),
mkLog (929436048198271986316703015397443935067455772701523444891/250000000000000000000000000000000000000000000000000000000000) 9 (-5594638194510) (-5594638194328),
mkLog (15089938182813280026775987927561667/4000000000000000000000000000000000000) 9 (-5580021463988) (-5580021463806),
mkLog (15089938181960879384059987927561667/4000000000000000000000000000000000000) 9 (-5580021464045) (-5580021463863),
mkLog (23953687403023950918913504292167/250000000000000000000000000000000000) 14 (-9253093922432) (-9253093922151),
mkLog (87347141146140821552882046769667/500000000000000000000000000000000000) 13 (-8652473070213) (-8652473069952),
mkLog (92775984081143621858806655469130096365653187/500000000000000000000000000000000000000000000000) 13 (-8592175563465) (-8592175563204),
mkLog (92775984003287470187306655469130096365653187/500000000000000000000000000000000000000000000000) 13 (-8592175564304) (-8592175564043),
mkLog (87347141141544524994382046769667/500000000000000000000000000000000000) 13 (-8652473070266) (-8652473070005),
mkLog (1664411683838430399316716783409309903634346813/250000000000000000000000000000000000000000000000) 8 (-5011989199991) (-5011989199830),
mkLog (1664411685046024505381966783409309903634346813/250000000000000000000000000000000000000000000000) 8 (-5011989199266) (-5011989199105),
mkLog (92775984438415065071241575547932756792898769/500000000000000000000000000000000000000000000000) 13 (-8592175559614) (-8592175559353),
mkLog (1664411694195818373914456519979743493207101231/250000000000000000000000000000000000000000000000) 8 (-5011989193768) (-5011989193607),
mkLog (92775984429049210491741575547932756792898769/500000000000000000000000000000000000000000000000) 13 (-8592175559715) (-8592175559454),
mkLog (92775984064425417147806655469130096365653187/500000000000000000000000000000000000000000000000) 13 (-8592175563645) (-8592175563384),
mkLog (92775984078783594485806655469130096365653187/500000000000000000000000000000000000000000000000) 13 (-8592175563490) (-8592175563229),
mkLog (92775984440775092444241575547932756792898769/500000000000000000000000000000000000000000000000) 13 (-8592175559589) (-8592175559328),
mkLog (1664411693698554265871956519979743493207101231/250000000000000000000000000000000000000000000000) 8 (-5011989194067) (-5011989193906),
mkLog (174694185184887069370349768836201/1000000000000000000000000000000000000) 13 (-8652473626084) (-8652473625823),
mkLog (174694185171122931332349768836201/1000000000000000000000000000000000000) 13 (-8652473626162) (-8652473625901),
mkLog (3949290292202578785776476937919770443559183/500000000000000000000000000000000000000000000000) 17 (-11748827487666) (-11748827487325),
mkLog (61179412704985291552104568930564729556440817/250000000000000000000000000000000000000000000000) 12 (-8315405457750) (-8315405457509),
mkLog (279988577128939560380816588867073/1000000000000000000000000000000000000) 12 (-8180761751716) (-8180761751475),
mkLog (279988577596010433180816588867073/1000000000000000000000000000000000000) 12 (-8180761750048) (-8180761749807),
mkLog (3949290323875784719776476937919770443559183/500000000000000000000000000000000000000000000000) 17 (-11748827479646) (-11748827479305),
mkLog (279988576561482030150816588867073/1000000000000000000000000000000000000) 12 (-8180761753743) (-8180761753502),
mkLog (279988577629532470098816588867073/1000000000000000000000000000000000000) 12 (-8180761749929) (-8180761749688),
mkLog (1974645084368627968688607231271588128696893/250000000000000000000000000000000000000000000000) 17 (-11748827518929) (-11748827518588),
mkLog (30544889552552765630462575400949661871303107/125000000000000000000000000000000000000000000000) 12 (-8316871626203) (-8316871625962),
mkLog (1974645068510244012688607231271588128696893/250000000000000000000000000000000000000000000000) 17 (-11748827526960) (-11748827526619),
mkLog (33069231/4000000000000) 17 (-11703201646237) (-11703201645896),
mkLog (16630627/4000000000000) 18 (-12390558923825) (-12390558923464),
mkLog (16630627/1000000000000) 16 (-11004264562685) (-11004264562364),
mkLog (1984251863148197539/500000000000000000000000) 18 (-12437121429629) (-12437121429268),
mkLog (10615425827193281289/125000000000000000000000) 14 (-9373760806466) (-9373760806185),
mkLog (38519878142260227999/500000000000000000000000) 14 (-9471188954113) (-9471188953832),
mkLog (3851987871057393483/50000000000000000000000) 14 (-9471188939360) (-9471188939079),
mkLog (1984251851292892051/500000000000000000000000) 18 (-12437121435604) (-12437121435243),
mkLog (38519878853084586217/500000000000000000000000) 14 (-9471188935660) (-9471188935379),
mkLog (9629969674803150101/125000000000000000000000) 14 (-9471188939655) (-9471188939374),
mkLog (992125960841884193/250000000000000000000000) 18 (-12437121400129) (-12437121399768),
mkLog (21253652885137219651/250000000000000000000000) 14 (-9372687415911) (-9372687415630),
mkLog (496062969924057029/125000000000000000000000) 18 (-12437121421289) (-12437121420928),
mkLog (246985531/500000000000) 11 (-7613033621551) (-7613033621330),
mkLog (5552217170662566511/100000000000000000000000) 15 (-9798728126929) (-9798728126628),
mkLog (1668014424188494223/31250000000000000000000) 15 (-9838140703822) (-9838140703521),
mkLog (53376461578801373157/1000000000000000000000000) 15 (-9838140703732) (-9838140703431),
mkLog (11104434346094691043/200000000000000000000000) 15 (-9798728126499) (-9798728126198),
mkLog (1030114407032772299813/1000000000000000000000000) 10 (-6878085408221) (-6878085408020),
mkLog (32191075324555362143/31250000000000000000000) 10 (-6878085404966) (-6878085404765),
mkLog (26688230601003144749/500000000000000000000000) 15 (-9838140710792) (-9838140710491),
mkLog (1030114409799115951993/1000000000000000000000000) 10 (-6878085405535) (-6878085405334),
mkLog (53376461216314963561/1000000000000000000000000) 15 (-9838140710523) (-9838140710222),
mkLog (6672057691984418871/125000000000000000000000) 15 (-9838140704537) (-9838140704236),
mkLog (1030114409159995177179/1000000000000000000000000) 10 (-6878085406156) (-6878085405955),
mkLog (55522175031007605747/1000000000000000000000000) 15 (-9798728067054) (-9798728066753),
mkLog (11104435013832813983/200000000000000000000000) 15 (-9798728066367) (-9798728066066),
mkLog (4769558021/1000000000000) 8 (-5345501636527) (-5345501636366),
mkLog (15804480318330509/800000000000000000000) 16 (-10832073542524) (-10832073542203),
mkLog (7983525757083188161/20000000000000000000000) 12 (-7826107414575) (-7826107414334),
mkLog (7983525546485943541/20000000000000000000000) 12 (-7826107440954) (-7826107440713),
mkLog (95568531696499077/5000000000000000000000) 16 (-10865104871044) (-10865104870723),
mkLog (16222102576378320789/40000000000000000000000) 12 (-7810260064301) (-7810260064060),
mkLog (15967051509653578223/40000000000000000000000) 12 (-7826107414858) (-7826107414617),
mkLog (15967051516673486377/40000000000000000000000) 12 (-7826107414418) (-7826107414177),
mkLog (8111051171608542837/20000000000000000000000) 12 (-7810260078674) (-7810260078433),
mkLog (152079272245701539067/20000000000000000000000) 8 (-4879085639787) (-4879085639625),
mkLog (2595536328061861/6400000000000000000) 12 (-7810260096725) (-7810260096484),
mkLog (7983524523585041101/20000000000000000000000) 12 (-7826107569081) (-7826107568840),
mkLog (7983524524587885123/20000000000000000000000) 12 (-7826107568955) (-7826107568714),
mkLog (764548256079102671/40000000000000000000000) 16 (-10865104867765) (-10865104867444),
mkLog (8111051263870192861/20000000000000000000000) 12 (-7810260067299) (-7810260067058),
mkLog (15967049042657284103/40000000000000000000000) 12 (-7826107569363) (-7826107569122),
mkLog (399176225903469949/1000000000000000000000) 12 (-7826107569772) (-7826107569531),
mkLog (790238169555629947/40000000000000000000000) 16 (-10832055631764) (-10832055631443),
mkLog (501422011/40000000000) 7 (-4379186649324) (-4379186649183),
mkLog (22674953777468760873/500000000000000000000000) 15 (-10001102420036) (-10001102419735),
mkLog (10700351319269802771/250000000000000000000000) 15 (-10058939622490) (-10058939622189),
mkLog (528484262526697180113/500000000000000000000000) 10 (-6852350350261) (-6852350350060),
mkLog (1070035131689395989/25000000000000000000000) 15 (-10058939622712) (-10058939622411),
mkLog (21400703244379540197/500000000000000000000000) 15 (-10058939594181) (-10058939593880),
mkLog (528484259932276754061/500000000000000000000000) 10 (-6852350355170) (-6852350354969),
mkLog (264242058079072405173/250000000000000000000000) 10 (-6852350627220) (-6852350627019),
mkLog (528484116246050996943/500000000000000000000000) 10 (-6852350627053) (-6852350626852),
mkLog (11337648758396313417/250000000000000000000000) 15 (-10001087260724) (-10001087260423),
mkLog (10700351618626005777/250000000000000000000000) 15 (-10058939594514) (-10058939594213),
mkLog (11337648772651370703/250000000000000000000000) 15 (-10001087259466) (-10001087259165),
mkLog (2375842881/500000000000) 8 (-5349255826715) (-5349255826554),
mkLog (2967422677125299773/1000000000000000000000000) 19 (-12727816767565) (-12727816767184),
mkLog (8947349050869110671/125000000000000000000000) 14 (-9544711723447) (-9544711723166),
mkLog (2967422674122857947/1000000000000000000000000) 19 (-12727816768576) (-12727816768195),
mkLog (10793173459012466983/125000000000000000000000) 14 (-9357155169275) (-9357155168994),
mkLog (43172693913612948437/500000000000000000000000) 14 (-9357155167479) (-9357155167198),
mkLog (370920112422836871/125000000000000000000000) 19 (-12727837586434) (-12727837586053),
mkLog (43172693863572251337/500000000000000000000000) 14 (-9357155168638) (-9357155168357),
mkLog (86345387726644095703/1000000000000000000000000) 14 (-9357155168644) (-9357155168363),
mkLog (71577060469903057021/1000000000000000000000000) 14 (-9544735919972) (-9544735919691),
mkLog (185460057462435863/62500000000000000000000) 19 (-12727837579689) (-12727837579308),
mkLog (500406971/1000000000000) 11 (-7600088848724) (-7600088848503),
mkLog (4109651/1000000000000) 18 (-12402172448085) (-12402172447724),
mkLog (4109651/250000000000) 16 (-11015878086945) (-11015878086624),
mkLog (24562461858085569/6250000000000000000000) 18 (-12446872685117) (-12446872684756),
mkLog (42036335316320516809/500000000000000000000000) 14 (-9383829006689) (-9383829006408),
mkLog (38141098032547494061/500000000000000000000000) 14 (-9481070988261) (-9481070987980),
mkLog (3814109769776922363/50000000000000000000000) 14 (-9481070997038) (-9481070996757),
mkLog (982498496087678471/250000000000000000000000) 18 (-12446872662965) (-12446872662604),
mkLog (4767637129749296341/62500000000000000000000) 14 (-9481071014337) (-9481071014056),
mkLog (7628219545178315303/100000000000000000000000) 14 (-9481070996301) (-9481070996020),
mkLog (392999412471793611/100000000000000000000000) 18 (-12446872627248) (-12446872626887),
mkLog (42081485113665907327/500000000000000000000000) 14 (-9382755517114) (-9382755516833),
mkLog (1964997072629740413/500000000000000000000000) 18 (-12446872622022) (-12446872621661),
mkLog (244542199/500000000000) 11 (-7622975490446) (-7622975490225),
mkLog (3457204426751504847/62500000000000000000000) 15 (-9802461542536) (-9802461542235),
mkLog (26475188513330174673/500000000000000000000000) 15 (-9846155365666) (-9846155365365),
mkLog (26475188433089243991/500000000000000000000000) 15 (-9846155368696) (-9846155368395),
mkLog (5531527079498369433/100000000000000000000000) 15 (-9802461543133) (-9802461542832),
mkLog (509398826620279024803/500000000000000000000000) 10 (-6889132118417) (-6889132118216),
mkLog (63674853419870949069/62500000000000000000000) 10 (-6889132116967) (-6889132116766),
mkLog (6618797108862317841/125000000000000000000000) 15 (-9846155368607) (-9846155368306),
mkLog (509398824062009352471/500000000000000000000000) 10 (-6889132123439) (-6889132123238),
mkLog (26475188418929079753/500000000000000000000000) 15 (-9846155369231) (-9846155368930),
mkLog (13237594257845101023/250000000000000000000000) 15 (-9846155365576) (-9846155365275),
mkLog (264751885109701473/5000000000000000000000) 15 (-9846155365755) (-9846155365454),
mkLog (26475188437809298737/500000000000000000000000) 15 (-9846155368518) (-9846155368217),
mkLog (509398823387041523793/500000000000000000000000) 10 (-6889132124764) (-6889132124563),
mkLog (27657646541541102471/500000000000000000000000) 15 (-9802461140205) (-9802461139904),
mkLog (3457205814447600171/62500000000000000000000) 15 (-9802461141144) (-9802461140843),
mkLog (2360027373/500000000000) 8 (-5355934880804) (-5355934880643),
mkLog (22140167581422649/976562500000000000000) 16 (-10694400535087) (-10694400534766),
mkLog (25488618069859008453/62500000000000000000000) 12 (-7804689833527) (-7804689833286),
mkLog (1274430903767142649/3125000000000000000000) 12 (-7804689833312) (-7804689833071),
mkLog (1367793645132858497/62500000000000000000000) 16 (-10729722872265) (-10729722871944),
mkLog (25759760518747826283/62500000000000000000000) 12 (-7794108231285) (-7794108231044),
mkLog (6372154517268900523/15625000000000000000000) 12 (-7804689833558) (-7804689833317),
mkLog (3219969979158407551/7812500000000000000000) 12 (-7794108257896) (-7794108257655),
mkLog (468153250468999823383/62500000000000000000000) 8 (-4894126135223) (-4894126135062),
mkLog (25759760280592292539/62500000000000000000000) 12 (-7794108240530) (-7794108240289),
mkLog (2548861430715825657/6250000000000000000000) 12 (-7804689981150) (-7804689980909),
mkLog (79651919685388103/195312500000000000000) 12 (-7804689981457) (-7804689981216),
mkLog (1367793648266483941/62500000000000000000000) 16 (-10729722869974) (-10729722869653),
mkLog (12879880291885277123/31250000000000000000000) 12 (-7794108228761) (-7794108228520),
mkLog (25488614306374850209/62500000000000000000000) 12 (-7804689981180) (-7804689980939),
mkLog (5097722860648244953/12500000000000000000000) 12 (-7804689981303) (-7804689981062),
mkLog (1416994505511137691/62500000000000000000000) 16 (-10694383752735) (-10694383752414),
mkLog (783406361/62500000000) 7 (-4379270294862) (-4379270294721),
mkLog (333973156375961753/6250000000000000000000) 15 (-9837031402249) (-9837031401948),
mkLog (83493289049097011/1562500000000000000000) 15 (-9837031402787) (-9837031402486),
mkLog (149011014885024747/3125000000000000000000) 15 (-9950924612688) (-9950924612387),
mkLog (409513727006368593/390625000000000000000) 10 (-6860532875459) (-6860532875258),
mkLog (596044101859636409/12500000000000000000000) 15 (-9950924541687) (-9950924541386),
mkLog (6552219656344348203/6250000000000000000000) 10 (-6860532871760) (-6860532871559),
mkLog (596044059360525279/12500000000000000000000) 15 (-9950924612989) (-9950924612688),
mkLog (3276109063577250131/3125000000000000000000) 10 (-6860533105145) (-6860533104944),
mkLog (13104436246228183619/12500000000000000000000) 10 (-6860533105761) (-6860533105560),
mkLog (667953326122844307/12500000000000000000000) 15 (-9837020902402) (-9837020902101),
mkLog (133590665176682539/2500000000000000000000) 15 (-9837020902760) (-9837020902459),
mkLog (59857903/12500000000) 8 (-5341510453301) (-5341510453140),
mkLog (3683087793755734401/1000000000000000000000000) 19 (-12511759083411) (-12511759083029),
mkLog (4924562298936622731/62500000000000000000000) 14 (-9448686438504) (-9448686438223),
mkLog (92077194831172821/25000000000000000000000) 19 (-12511759083549) (-12511759083167),
mkLog (84125804068821856239/1000000000000000000000000) 14 (-9383197212162) (-9383197211881),
mkLog (8412580407441889341/100000000000000000000000) 14 (-9383197212095) (-9383197211814),
mkLog (92077189742957211/25000000000000000000000) 19 (-12511759138809) (-12511759138428),
mkLog (3365032162264405551/40000000000000000000000) 14 (-9383197212307) (-9383197212026),
mkLog (84125804073910071849/1000000000000000000000000) 14 (-9383197212101) (-9383197211820),
mkLog (78792997192587320301/1000000000000000000000000) 14 (-9448686433305) (-9448686433024),
mkLog (3683087573944820049/1000000000000000000000000) 19 (-12511759143092) (-12511759142710),
mkLog (508821561/1000000000000) 11 (-7583413170768) (-7583413170547),
mkLog (16719623/4000000000000) 18 (-12385221859710) (-12385221859349),
mkLog (16719623/1000000000000) 16 (-10998927498570) (-10998927498249),
mkLog (11385020251/500000000000) 6 (-3782309620225) (-3782309620104),
mkLog (56796688561209870048317497118221257/2000000000000000000000000000000000000) 6 (-3561424435554) (-3561424435433),
mkLog (56796705947790129951682502881778743/2000000000000000000000000000000000000) 6 (-3561424129434) (-3561424129313),
mkLog (113593394509/1000000000000) 4 (-2175129921354) (-2175129921273),
mkLog (100643402879166608840721197878979004270105229/62500000000000000000000000000000000000000000000) 10 (-6431338231053) (-6431338230852),
mkLog (1561516201553315691313047604117212683229894771/31250000000000000000000000000000000000000000000) 5 (-2996362102911) (-2996362102810),
mkLog (18247292578332667928479917530374449/400000000000000000000000000000000000) 5 (-3087447830008) (-3087447829907),
mkLog (4025736571518046915474273226775244924998011/2500000000000000000000000000000000000000000000) 10 (-6431338117694) (-6431338117493),
mkLog (62460647045774311972376005563696475075001989/1250000000000000000000000000000000000000000000) 5 (-2996362119183) (-2996362119082),
mkLog (288851140019/1000000000000) 2 (-1241843810032) (-1241843809991),
mkLog (2209053175825457847915515443082593/1000000000000000000000000000000000000) 9 (-6115191282573) (-6115191282392),
mkLog (522014491324526727883108456213713278418893769/200000000000000000000000000000000000000000000000) 9 (-5948377296966) (-5948377296785),
mkLog (7850535244155516611361873902512843071581106231/100000000000000000000000000000000000000000000000) 4 (-2544588472590) (-2544588472509),
mkLog (81564755863394976083337835589266914095249249/31250000000000000000000000000000000000000000000) 9 (-5948377400026) (-5948377399845),
mkLog (1226646542782288829825230317224390648404750751/15625000000000000000000000000000000000000000000) 4 (-2544588137626) (-2544588137545),
mkLog (4418037035100690362972598379155519/2000000000000000000000000000000000000) 9 (-6115206971895) (-6115206971714),
mkLog (343738184323/1000000000000) 2 (-1067875003491) (-1067875003450),
mkLog (26694918239500344458263211654037/500000000000000000000000000000000000) 15 (-9837890158373) (-9837890158072),
mkLog (370686200134946936678922446648833/125000000000000000000000000000000000) 9 (-5820713133416) (-5820713133235),
mkLog (29802174179315584372912146933521594720608952298476555109/500000000000000000000000000000000000000000000000000000000000) 15 (-9727782027668) (-9727782027366),
mkLog (725008865064812358570203015397443935067455772701523444891/250000000000000000000000000000000000000000000000000000000000) 9 (-5843032314480) (-5843032314299),
mkLog (725008899565172218161350473375587491256458044451523444891/250000000000000000000000000000000000000000000000000000000000) 9 (-5843032266894) (-5843032266713),
mkLog (16154642983312963499184698531693313853955477230548476555109/125000000000000000000000000000000000000000000000000000000000) 3 (-2046106237755) (-2046106237694),
mkLog (11861961962939561203099987927561667/4000000000000000000000000000000000000) 9 (-5820712833413) (-5820712833232),
mkLog (13346720821256712986163504292167/250000000000000000000000000000000000) 15 (-9837945473688) (-9837945473387),
mkLog (10306650029/62500000000) 3 (-1802377235986) (-1802377235925),
mkLog (31928419878815950221882046769667/500000000000000000000000000000000000) 14 (-9658866859083) (-9658866858802),
mkLog (39612564780797539617806655469130096365653187/500000000000000000000000000000000000000000000000) 14 (-9443217017167) (-9443217016886),
mkLog (1152183668770097811961966783409309903634346813/250000000000000000000000000000000000000000000000) 8 (-5379801933682) (-5379801933521),
mkLog (39612565401962648958241575547932756792898769/500000000000000000000000000000000000000000000000) 14 (-9443217001486) (-9443217001205),
mkLog (1152183679715034709680706519979743493207101231/250000000000000000000000000000000000000000000000) 8 (-5379801924182) (-5379801924021),
mkLog (63856717070797258681349768836201/1000000000000000000000000000000000000) 14 (-9658868780365) (-9658868780084),
mkLog (19324166943/1000000000000) 6 (-3946398793235) (-3946398793114),
mkLog (41480407535726776476937919770443559183/500000000000000000000000000000000000000000000000) 34 (-23212652727525) (-23212652726844),
mkLog (18930393392438470569604568930564729556440817/250000000000000000000000000000000000000000000000) 14 (-9488447450552) (-9488447450271),
mkLog (126666624779324116260816588867073/1000000000000000000000000000000000000) 13 (-8973951924733) (-8973951924472),
mkLog (20592347259748188607231271588128696893/250000000000000000000000000000000000000000000000) 34 (-23219807240621) (-23219807239940),
mkLog (9397691831567678973212575400949661871303107/125000000000000000000000000000000000000000000000) 14 (-9495604907135) (-9495604906854),
mkLog (328784969/500000000000) 11 (-7326959430099) (-7326959429878)]
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,25),
(false,26),
(false,27),
(false,28),
(false,29),
(false,25),
(false,30),
(false,31),
(false,32),
(false,33),
(false,34),
(false,35),
(true,3),
(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,48),
(false,39),
(false,49),
(false,39),
(false,50),
(false,51),
(false,52),
(true,4),
(false,53),
(false,54),
(false,55),
(false,56),
(false,57),
(false,58),
(false,59),
(false,60),
(false,61),
(false,55),
(false,55),
(false,62),
(false,63),
(false,59),
(false,64),
(false,64),
(true,5),
(false,65),
(false,66),
(false,67),
(false,68),
(false,69),
(false,70),
(false,71),
(false,72),
(false,73),
(false,74),
(true,6),
(false,75),
(false,75),
(false,75),
(false,75),
(true,7),
(false,8),
(true,8),
(true,8),
(false,8),
(true,76),
(true,76),
(true,76),
(true,76),
(false,77),
(true,78),
(true,79),
(true,80),
(true,81),
(true,82),
(true,83),
(true,84),
(true,85),
(true,86),
(true,87),
(false,88),
(true,89),
(true,90),
(true,91),
(true,92),
(true,93),
(true,94),
(true,95),
(true,96),
(true,97),
(true,91),
(true,91),
(true,98),
(true,99),
(true,95),
(true,100),
(true,100),
(false,101),
(true,102),
(true,103),
(true,104),
(true,105),
(true,106),
(true,105),
(true,103),
(true,107),
(true,108),
(true,109),
(true,110),
(true,111),
(true,112),
(true,105),
(true,113),
(true,105),
(true,114),
(true,115),
(true,116),
(false,117),
(true,118),
(true,119),
(true,120),
(true,121),
(true,122),
(true,123),
(true,123),
(true,120),
(true,124),
(true,122),
(true,125),
(true,126),
(true,127),
(true,123),
(true,128),
(true,129),
(false,130),
(true,131),
(true,132),
(true,133),
(true,134),
(true,135),
(true,136),
(true,137),
(true,138),
(true,139),
(true,140),
(false,141),
(true,142),
(true,142),
(true,142),
(true,142),
(false,143),
(true,144),
(false,144),
(true,145),
(false,145),
(true,146),
(true,146),
(true,147),
(true,147),
(false,148),
(true,149),
(true,150),
(true,151),
(true,152),
(true,153),
(true,154),
(true,155),
(true,156),
(true,157),
(true,158),
(false,159),
(true,160),
(true,161),
(true,162),
(true,163),
(true,162),
(true,164),
(true,165),
(true,166),
(true,167),
(true,162),
(true,168),
(true,169),
(true,170),
(true,171),
(true,164),
(true,172),
(false,173),
(true,174),
(true,175),
(true,176),
(true,177),
(true,178),
(true,179),
(true,180),
(true,181),
(true,182),
(true,183),
(true,184),
(true,185),
(true,186),
(true,177),
(true,187),
(true,177),
(true,188),
(true,189),
(true,190),
(false,191),
(true,192),
(true,193),
(true,194),
(true,195),
(true,196),
(true,197),
(true,198),
(true,199),
(true,198),
(true,194),
(true,194),
(true,200),
(true,201),
(true,198),
(true,202),
(true,202),
(false,203),
(true,204),
(true,205),
(true,206),
(true,207),
(true,208),
(true,209),
(true,210),
(true,211),
(true,212),
(true,213),
(false,214),
(true,215),
(true,215),
(true,215),
(true,215),
(false,216)]
private def refs1 : List (Bool × Fin 472) :=
[(false,217),
(false,218),
(false,219),
(false,220),
(false,221),
(false,222),
(false,223),
(false,224),
(false,225),
(false,217),
(true,217),
(false,226),
(false,226),
(false,227),
(false,227),
(true,218),
(false,228),
(false,229),
(false,230),
(false,231),
(false,232),
(false,233),
(false,234),
(false,235),
(false,236),
(false,237),
(true,219),
(false,238),
(false,239),
(false,240),
(false,241),
(false,242),
(false,243),
(false,243),
(false,240),
(false,244),
(false,245),
(false,246),
(false,247),
(false,248),
(false,243),
(false,249),
(false,250),
(true,220),
(false,251),
(false,252),
(false,253),
(false,254),
(false,255),
(false,254),
(false,256),
(false,257),
(false,258),
(false,259),
(false,260),
(false,261),
(false,262),
(false,263),
(false,264),
(false,254),
(false,265),
(false,266),
(false,267),
(true,221),
(false,268),
(false,269),
(false,270),
(false,271),
(false,272),
(false,273),
(false,274),
(false,275),
(false,276),
(false,277),
(false,278),
(false,279),
(false,280),
(false,279),
(false,281),
(false,282),
(true,222),
(false,283),
(false,284),
(false,285),
(false,286),
(false,287),
(false,288),
(false,289),
(false,290),
(false,291),
(false,292),
(true,223),
(false,293),
(false,293),
(false,293),
(false,293),
(true,224),
(false,225),
(true,225),
(true,225),
(false,225),
(true,294),
(true,294),
(true,294),
(true,294),
(false,295),
(true,296),
(true,297),
(true,298),
(true,299),
(true,300),
(true,301),
(true,302),
(true,303),
(true,304),
(true,305),
(false,306),
(true,307),
(true,308),
(true,309),
(true,310),
(true,311),
(true,312),
(true,313),
(true,314),
(true,315),
(true,316),
(true,308),
(true,313),
(true,317),
(true,313),
(true,318),
(true,319),
(false,320),
(true,321),
(true,322),
(true,323),
(true,324),
(true,325),
(true,324),
(true,326),
(true,327),
(true,328),
(true,329),
(true,330),
(true,331),
(true,332),
(true,333),
(true,334),
(true,324),
(true,335),
(true,336),
(true,337),
(false,338),
(true,339),
(true,339),
(true,340),
(true,341),
(true,342),
(true,343),
(true,343),
(true,340),
(true,344),
(true,340),
(true,345),
(true,346),
(true,347),
(true,343),
(true,348),
(true,349),
(false,350),
(true,351),
(true,352),
(true,353),
(true,354),
(true,355),
(true,356),
(true,357),
(true,358),
(true,359),
(true,360),
(false,361),
(true,215),
(true,215),
(true,215),
(true,215),
(false,216),
(true,8),
(false,8),
(true,362),
(true,362),
(true,362),
(true,362),
(false,363),
(true,364),
(true,365),
(true,366),
(true,367),
(true,368),
(true,369),
(true,370),
(true,371),
(true,372),
(true,373),
(false,374),
(true,375),
(true,376),
(true,377),
(true,378),
(true,379),
(true,380),
(true,381),
(true,382),
(true,383),
(true,384),
(true,385),
(true,386),
(true,387),
(true,386),
(true,388),
(true,389),
(false,390),
(true,391),
(true,392),
(true,393),
(true,394),
(true,395),
(true,394),
(true,392),
(true,396),
(true,397),
(true,398),
(true,399),
(true,400),
(true,401),
(true,402),
(true,403),
(true,394),
(true,404),
(true,405),
(true,406),
(false,407),
(true,408),
(true,409),
(true,410),
(true,411),
(true,410),
(true,412),
(true,412),
(true,410),
(true,413),
(true,414),
(true,415),
(true,416),
(true,417),
(true,412),
(true,412),
(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,144),
(false,144),
(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 entriesOwner1 (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.