Exact global Y/Z certificate: logs 3
Definitionmme_released_global_yz_logs_3matrix-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 476 → Entry :=
![mkLog (23074225017/1000000000000) 6 (-3769039084614) (-3769039084493),
mkLog (1138758281/10000000000) 4 (-2172646651460) (-2172646651379),
mkLog (289597846017/1000000000000) 2 (-1239262056305) (-1239262056264),
mkLog (352758173063/1000000000000) 2 (-1041972518976) (-1041972518935),
mkLog (47520067663/250000000000) 3 (-1660308818955) (-1660308818894),
mkLog (28920701043/1000000000000) 6 (-3543197641279) (-3543197641157),
mkLog (1659706193/1000000000000) 10 (-6401114684548) (-6401114684347),
mkLog (33130259/1000000000000) 15 (-10315063524146) (-10315063523845),
mkLog (14957/125000000000) 23 (-15938644877821) (-15938644877360),
mkLog (56937895700613180235800942958899213/2000000000000000000000000000000000000) 6 (-3558941334871) (-3558941334749),
mkLog (56937932399386819764199057041100787/2000000000000000000000000000000000000) 6 (-3558940690330) (-3558940690209),
mkLog (433167147590830387216598932512151610898993391/250000000000000000000000000000000000000000000000) 10 (-6358092521281) (-6358092521080),
mkLog (6228614334140630969025494059330342889101006609/125000000000000000000000000000000000000000000000) 5 (-2999159847568) (-2999159847467),
mkLog (433167147674822334602098932512151610898993391/250000000000000000000000000000000000000000000000) 10 (-6358092521087) (-6358092520886),
mkLog (11438084132607927560601586866375297/250000000000000000000000000000000000) 5 (-3084512416912) (-3084512416811),
mkLog (11438084132594388670691586866375297/250000000000000000000000000000000000) 5 (-3084512416913) (-3084512416812),
mkLog (1732668790480631013558896972423236431105109627/1000000000000000000000000000000000000000000000000) 10 (-6358092405784) (-6358092405583),
mkLog (11438084132681415892088086866375297/250000000000000000000000000000000000) 5 (-3084512416906) (-3084512416805),
mkLog (11438084132703488455485086866375297/250000000000000000000000000000000000) 5 (-3084512416904) (-3084512416803),
mkLog (24914455229752598041885036129204409568894890373/500000000000000000000000000000000000000000000000) 5 (-2999159932130) (-2999159932029),
mkLog (1732668790477631947726896972423236431105109627/1000000000000000000000000000000000000000000000000) 10 (-6358092405786) (-6358092405585),
mkLog (2314452571224478041673083909045763/1000000000000000000000000000000000000) 9 (-6068582089812) (-6068582089631),
mkLog (2314452571966745637078083909045763/1000000000000000000000000000000000000) 9 (-6068582089491) (-6068582089310),
mkLog (5479159713690047141456985593625789226706723749/2000000000000000000000000000000000000000000000000) 9 (-5899950707348) (-5899950707167),
mkLog (80395927895663648712641136659338786273293276251/1000000000000000000000000000000000000000000000000) 4 (-2520791752184) (-2520791752103),
mkLog (5479159713756906254358985593625789226706723749/2000000000000000000000000000000000000000000000000) 9 (-5899950707336) (-5899950707155),
mkLog (5479160580170771662607087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5899950549207) (-5899950549026),
mkLog (5479160580075293735761087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5899950549225) (-5899950549044),
mkLog (5479159713766445859006985593625789226706723749/2000000000000000000000000000000000000000000000000) 9 (-5899950707334) (-5899950707153),
mkLog (80395927894842875335284136659338786273293276251/1000000000000000000000000000000000000000000000000) 4 (-2520791752195) (-2520791752114),
mkLog (5479159713680589417174985593625789226706723749/2000000000000000000000000000000000000000000000000) 9 (-5899950707350) (-5899950707169),
mkLog (80395909224533423439967742934874218179095379671/1000000000000000000000000000000000000000000000000) 4 (-2520791984424) (-2520791984343),
mkLog (80395909227910279724627742934874218179095379671/1000000000000000000000000000000000000000000000000) 4 (-2520791984382) (-2520791984301),
mkLog (28930956806776749464399540832991/12500000000000000000000000000000000) 9 (-6068571731771) (-6068571731590),
mkLog (5479160580189850871903087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5899950549204) (-5899950549023),
mkLog (5479160580275789194101087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5899950549188) (-5899950549007),
mkLog (28930956806419526042387040832991/12500000000000000000000000000000000) 9 (-6068571731784) (-6068571731603),
mkLog (3012020917511901660800543659363/31250000000000000000000000000000000) 14 (-9247163400667) (-9247163400386),
mkLog (15756889237742059955972580983067751/4000000000000000000000000000000000000) 8 (-5536771958628) (-5536771958467),
mkLog (15756889237495294073596580983067751/4000000000000000000000000000000000000) 8 (-5536771958644) (-5536771958483),
mkLog (12132950991232357237495843734222944264299388049873978523/125000000000000000000000000000000000000000000000000000000000) 14 (-9240144042659) (-9240144042378),
mkLog (255887853645685185030504313509996285594608774575126021477/62500000000000000000000000000000000000000000000000000000000) 8 (-5498182559004) (-5498182558843),
mkLog (15756889319247003963420580983067751/4000000000000000000000000000000000000) 8 (-5536771953455) (-5536771953294),
mkLog (15756889236373564382196580983067751/4000000000000000000000000000000000000) 8 (-5536771958715) (-5536771958554),
mkLog (255887854473398880269544331115014251210768598387626021477/62500000000000000000000000000000000000000000000000000000000) 8 (-5498182555769) (-5498182555608),
mkLog (4425270180726488089405640842586356706430323238987373978523/31250000000000000000000000000000000000000000000000000000000) 3 (-1954688041826) (-1954688041765),
mkLog (255887854472630814407231831115014251210768598387626021477/62500000000000000000000000000000000000000000000000000000000) 8 (-5498182555772) (-5498182555611),
mkLog (15756889973973286467426228930686249/4000000000000000000000000000000000000) 8 (-5536771911903) (-5536771911742),
mkLog (15756889983332915801702228930686249/4000000000000000000000000000000000000) 8 (-5536771911309) (-5536771911148),
mkLog (255887852644216233068379313509996285594608774575126021477/62500000000000000000000000000000000000000000000000000000000) 8 (-5498182562918) (-5498182562757),
mkLog (15756889977951084778522228930686249/4000000000000000000000000000000000000) 8 (-5536771911651) (-5536771911490),
mkLog (15756889980591901321794228930686249/4000000000000000000000000000000000000) 8 (-5536771911483) (-5536771911322),
mkLog (48191943610444681852821049443749/500000000000000000000000000000000000) 14 (-9247171515471) (-9247171515190),
mkLog (170617559799362748955975732119629/1000000000000000000000000000000000000) 13 (-8676085998679) (-8676085998418),
mkLog (236088220897191851336479491166605989391627/1250000000000000000000000000000000000000000000) 13 (-8574448556875) (-8574448556614),
mkLog (236088220897312547328979491166605989391627/1250000000000000000000000000000000000000000000) 13 (-8574448556875) (-8574448556614),
mkLog (170617559804854685643975732119629/1000000000000000000000000000000000000) 13 (-8676085998646) (-8676085998385),
mkLog (4176135339340634867985651820741046198108373/625000000000000000000000000000000000000000000) 8 (-5008365390916) (-5008365390755),
mkLog (4176135339598209547303151820741046198108373/625000000000000000000000000000000000000000000) 8 (-5008365390855) (-5008365390694),
mkLog (47217632766156874774878857301417503736657739/250000000000000000000000000000000000000000000000) 13 (-8574448798592) (-8574448798331),
mkLog (835226771277161131793486441744264621263342261/125000000000000000000000000000000000000000000000) 8 (-5008365746018) (-5008365745857),
mkLog (47217632767344791758378857301417503736657739/250000000000000000000000000000000000000000000000) 13 (-8574448798567) (-8574448798306),
mkLog (236088220897232083333979491166605989391627/1250000000000000000000000000000000000000000000) 13 (-8574448556875) (-8574448556614),
mkLog (47217632767336745358878857301417503736657739/250000000000000000000000000000000000000000000000) 13 (-8574448798567) (-8574448798306),
mkLog (835226769733236503447486441744264621263342261/125000000000000000000000000000000000000000000000) 8 (-5008365747867) (-5008365747706),
mkLog (341240078470475563159383552925341/2000000000000000000000000000000000000) 13 (-8676071466658) (-8676071466397),
mkLog (341240077271984534599383552925341/2000000000000000000000000000000000000) 13 (-8676071470170) (-8676071469909),
mkLog (515516237476875032237082336926469429659371/62500000000000000000000000000000000000000000000) 17 (-11705508313417) (-11705508313076),
mkLog (7341041768567335148253052866331030570340629/31250000000000000000000000000000000000000000000) 13 (-8356293892418) (-8356293892156),
mkLog (72307527033657453434697559349923/250000000000000000000000000000000000) 12 (-8148287964870) (-8148287964629),
mkLog (72307527064984738532697559349923/250000000000000000000000000000000000) 12 (-8148287964437) (-8148287964196),
mkLog (515516237113043752487082336926469429659371/62500000000000000000000000000000000000000000000) 17 (-11705508314123) (-11705508313782),
mkLog (72307526979662725933197559349923/250000000000000000000000000000000000) 12 (-8148287965617) (-8148287965376),
mkLog (72307527002867503415697559349923/250000000000000000000000000000000000) 12 (-8148287965296) (-8148287965055),
mkLog (824758617804279875781535970687437308738903/100000000000000000000000000000000000000000000000) 17 (-11705589985080) (-11705589984739),
mkLog (11744036605905423680676200224162162691261097/50000000000000000000000000000000000000000000000) 13 (-8356432695686) (-8356432695425),
mkLog (824758619156561706381535970687437308738903/100000000000000000000000000000000000000000000000) 17 (-11705589983440) (-11705589983099),
mkLog (33130259/4000000000000) 17 (-11701357885286) (-11701357884945),
mkLog (8248101/2000000000000) 18 (-12398674746673) (-12398674746312),
mkLog (8248101/500000000000) 16 (-11012380385533) (-11012380385212),
mkLog (487091143253759463/125000000000000000000000) 18 (-12455373037405) (-12455373037044),
mkLog (11071561703256804591/125000000000000000000000) 14 (-9331689204384) (-9331689204103),
mkLog (38063004980475690927/500000000000000000000000) 14 (-9483120565025) (-9483120564744),
mkLog (38063004912353059893/500000000000000000000000) 14 (-9483120566814) (-9483120566533),
mkLog (487091150215196211/125000000000000000000000) 18 (-12455373023113) (-12455373022752),
mkLog (19031502443869704267/250000000000000000000000) 14 (-9483120567461) (-9483120567180),
mkLog (38063004948651980079/500000000000000000000000) 14 (-9483120565861) (-9483120565580),
mkLog (194848070420011347/50000000000000000000000) 18 (-12455313434738) (-12455313434377),
mkLog (22145391938608475877/250000000000000000000000) 14 (-9331586761027) (-9331586760746),
mkLog (1948480702459754283/500000000000000000000000) 18 (-12455313435631) (-12455313435270),
mkLog (248622741/500000000000) 11 (-7606426726355) (-7606426726134),
mkLog (1765988142351746883/31250000000000000000000) 15 (-9781064267567) (-9781064267266),
mkLog (819901004423984101/15625000000000000000000) 15 (-9855199147080) (-9855199146779),
mkLog (1639802008405516733/31250000000000000000000) 15 (-9855199147350) (-9855199147049),
mkLog (882994069479809477/15625000000000000000000) 15 (-9781064269488) (-9781064269186),
mkLog (3978171078518399277/3906250000000000000000) 10 (-6889510927915) (-6889510927714),
mkLog (7956342153054735333/7812500000000000000000) 10 (-6889510928416) (-6889510928215),
mkLog (163980229732632599/3125000000000000000000) 15 (-9855198971157) (-9855198970856),
mkLog (6365075383141132011/6250000000000000000000) 10 (-6889510667508) (-6889510667307),
mkLog (1639802008700484379/31250000000000000000000) 15 (-9855199147170) (-9855199146869),
mkLog (1639802297473809813/31250000000000000000000) 15 (-9855198971067) (-9855198970766),
mkLog (31825376466764902843/31250000000000000000000) 10 (-6889510681614) (-6889510681413),
mkLog (35319388913600427/625000000000000000000) 15 (-9781074854711) (-9781074854410),
mkLog (1765969426359640537/31250000000000000000000) 15 (-9781074865651) (-9781074865350),
mkLog (147483823/31250000000) 8 (-5356056160057) (-5356056159896),
mkLog (11197231620367316691/500000000000000000000000) 16 (-10706696806571) (-10706696806250),
mkLog (391200639377306033493/1000000000000000000000000) 12 (-7846289985526) (-7846289985285),
mkLog (78240127865629963661/200000000000000000000000) 12 (-7846289985652) (-7846289985411),
mkLog (11140054167719261633/500000000000000000000000) 16 (-10711816280626) (-10711816280305),
mkLog (19017303217667522439/50000000000000000000000) 12 (-7874429024130) (-7874429023889),
mkLog (391200659703401013731/1000000000000000000000000) 12 (-7846289933568) (-7846289933327),
mkLog (391200638934900096801/1000000000000000000000000) 12 (-7846289986657) (-7846289986416),
mkLog (380346063407093306411/1000000000000000000000000) 12 (-7874429026618) (-7874429026377),
mkLog (1876038742173420524939/250000000000000000000000) 8 (-4892298416094) (-4892298415932),
mkLog (190173031697402126307/500000000000000000000000) 12 (-7874429026650) (-7874429026409),
mkLog (195600312788349309731/500000000000000000000000) 12 (-7846290020804) (-7846290020563),
mkLog (391200625785612534011/1000000000000000000000000) 12 (-7846290020270) (-7846290020029),
mkLog (190173032262698600969/500000000000000000000000) 12 (-7874429023678) (-7874429023437),
mkLog (4890007824931580607/12500000000000000000000) 12 (-7846290019736) (-7846290019495),
mkLog (2239459576589078023/100000000000000000000000) 16 (-10706690888824) (-10706690888503),
mkLog (12289053797/1000000000000) 7 (-4399046348105) (-4399046347964),
mkLog (52691269424945706661/1000000000000000000000000) 15 (-9851060781853) (-9851060781552),
mkLog (26345635093146255681/500000000000000000000000) 15 (-9851060767404) (-9851060767103),
mkLog (9318749743389112361/200000000000000000000000) 15 (-9974044173688) (-9974044173387),
mkLog (1036336884002384792897/1000000000000000000000000) 10 (-6872063010496) (-6872063010295),
mkLog (2912109294513543729/62500000000000000000000) 15 (-9974044173789) (-9974044173488),
mkLog (23296871665385791603/500000000000000000000000) 15 (-9974044289286) (-9974044288985),
mkLog (46593743335500445347/1000000000000000000000000) 15 (-9974044289185) (-9974044288884),
mkLog (64771055390537144367/62500000000000000000000) 10 (-6872063008329) (-6872063008128),
mkLog (8096383283956116351/7812500000000000000000) 10 (-6872062840335) (-6872062840134),
mkLog (259084265091324585373/250000000000000000000000) 10 (-6872062840317) (-6872062840116),
mkLog (26345435563537078327/500000000000000000000000) 15 (-9851068340968) (-9851068340667),
mkLog (9318748665208544213/200000000000000000000000) 15 (-9974044289388) (-9974044289087),
mkLog (52690871122345294513/1000000000000000000000000) 15 (-9851068341058) (-9851068340757),
mkLog (4728862141/1000000000000) 8 (-5354070667655) (-5354070667494),
mkLog (1731218566207151853/500000000000000000000000) 19 (-12573537843511) (-12573537843130),
mkLog (39070740658954889001/500000000000000000000000) 14 (-9456989511429) (-9456989511148),
mkLog (216402329857700883/62500000000000000000000) 19 (-12573537801543) (-12573537801162),
mkLog (20791642632328939371/250000000000000000000000) 14 (-9394665087543) (-9394665087262),
mkLog (20791642634842934361/250000000000000000000000) 14 (-9394665087422) (-9394665087141),
mkLog (865609245267951327/250000000000000000000000) 19 (-12573537887220) (-12573537886839),
mkLog (8316657053283535047/100000000000000000000000) 14 (-9394665087501) (-9394665087220),
mkLog (41583285262898082249/500000000000000000000000) 14 (-9394665087585) (-9394665087304),
mkLog (19535371546125319911/250000000000000000000000) 14 (-9456989449150) (-9456989448869),
mkLog (865609244765152329/250000000000000000000000) 19 (-12573537887801) (-12573537887420),
mkLog (251399499/500000000000) 11 (-7595320074201) (-7595320073980),
mkLog (16574693/4000000000000) 18 (-12393927905236) (-12393927904875),
mkLog (16574693/1000000000000) 16 (-11007633544096) (-11007633543775),
mkLog (119821/1000000000000) 23 (-15937266874705) (-15937266874244),
mkLog (5768526299/250000000000) 6 (-3769044277477) (-3769044277356),
mkLog (56929608354113180235800942958899213/2000000000000000000000000000000000000) 6 (-3559086896092) (-3559086895971),
mkLog (56929645052886819764199057041100787/2000000000000000000000000000000000000) 6 (-3559086251458) (-3559086251337),
mkLog (113859253407/1000000000000) 4 (-2172792212635) (-2172792212554),
mkLog (432301538307726811290098932512151610898993391/250000000000000000000000000000000000000000000000) 10 (-6360092846852) (-6360092846651),
mkLog (6218846648975892246775244059330342889101006609/125000000000000000000000000000000000000000000000) 5 (-3000729274005) (-3000729273904),
mkLog (432301538355391531070098932512151610898993391/250000000000000000000000000000000000000000000000) 10 (-6360092846742) (-6360092846541),
mkLog (11417292489975598621230586866375297/250000000000000000000000000000000000) 5 (-3086331826735) (-3086331826634),
mkLog (11417292489959545736330586866375297/250000000000000000000000000000000000) 5 (-3086331826736) (-3086331826635),
mkLog (1729206353499559208250896972423236431105109627/1000000000000000000000000000000000000000000000000) 10 (-6360092731036) (-6360092730835),
mkLog (11417292490048207054470586866375297/250000000000000000000000000000000000) 5 (-3086331826729) (-3086331826628),
mkLog (11417292490072039414360586866375297/250000000000000000000000000000000000) 5 (-3086331826727) (-3086331826626),
mkLog (24875384486660347402063036129204409568894890373/500000000000000000000000000000000000000000000000) 5 (-3000729358798) (-3000729358697),
mkLog (1729206353498571338410896972423236431105109627/1000000000000000000000000000000000000000000000000) 10 (-6360092731037) (-6360092730836),
mkLog (289095047019/1000000000000) 2 (-1240999762542) (-1240999762501),
mkLog (2261761301799532335012083909045763/1000000000000000000000000000000000000) 9 (-6091611432235) (-6091611432054),
mkLog (2261761301780453125716083909045763/1000000000000000000000000000000000000) 9 (-6091611432243) (-6091611432062),
mkLog (5385972216256156017846985593625789226706723749/2000000000000000000000000000000000000000000000000) 9 (-5917104623769) (-5917104623588),
mkLog (79359591011661263919744136659338786273293276251/1000000000000000000000000000000000000000000000000) 4 (-2533765969642) (-2533765969561),
mkLog (5385972216332472855030985593625789226706723749/2000000000000000000000000000000000000000000000000) 9 (-5917104623754) (-5917104623573),
mkLog (5385973093509228496195087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5917104460891) (-5917104460710),
mkLog (5385973093404292845067087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5917104460911) (-5917104460730),
mkLog (5385972216342012459678985593625789226706723749/2000000000000000000000000000000000000000000000000) 9 (-5917104623753) (-5917104623572),
mkLog (79359591008594281025412136659338786273293276251/1000000000000000000000000000000000000000000000000) 4 (-2533765969681) (-2533765969600),
mkLog (79359572164187040547039742934874218179095379671/1000000000000000000000000000000000000000000000000) 4 (-2533766207137) (-2533766207056),
mkLog (79359572167544981383135742934874218179095379671/1000000000000000000000000000000000000000000000000) 4 (-2533766207095) (-2533766207014),
mkLog (28272320917688322506224540832991/12500000000000000000000000000000000) 9 (-6091600656790) (-6091600656609),
mkLog (5385973093528307705491087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5917104460888) (-5917104460707),
mkLog (5385973093623703751971087636476163320904620329/2000000000000000000000000000000000000000000000000) 9 (-5917104460870) (-5917104460689),
mkLog (28272320917390209860974540832991/12500000000000000000000000000000000) 9 (-6091600656801) (-6091600656620),
mkLog (174014655461/500000000000) 2 (-1055468575988) (-1055468575947),
mkLog (2312193941238944367613043659363/31250000000000000000000000000000000) 14 (-9511577823395) (-9511577823114),
mkLog (14192086680232835822000580983067751/4000000000000000000000000000000000000) 9 (-5641365106962) (-5641365106781),
mkLog (14192086680182694800376580983067751/4000000000000000000000000000000000000) 9 (-5641365106965) (-5641365106784),
mkLog (9347937449302541829245843734222944264299388049873978523/125000000000000000000000000000000000000000000000000000000000) 14 (-9500913291117) (-9500913290836),
mkLog (232116224623600781981754313509996285594608774575126021477/62500000000000000000000000000000000000000000000000000000000) 9 (-5595683621387) (-5595683621205),
mkLog (14192086680433399908496580983067751/4000000000000000000000000000000000000) 9 (-5641365106948) (-5641365106767),
mkLog (14192086680633963994992580983067751/4000000000000000000000000000000000000) 9 (-5641365106933) (-5641365106752),
mkLog (232116225510455548618856831115014251210768598387626021477/62500000000000000000000000000000000000000000000000000000000) 9 (-5595683617566) (-5595683617385),
mkLog (4190765337954810523788265842586356706430323238987373978523/31250000000000000000000000000000000000000000000000000000000) 3 (-2009136000736) (-2009136000675),
mkLog (14192087471666491989578228930686249/4000000000000000000000000000000000000) 9 (-5641365051196) (-5641365051015),
mkLog (14192087480190465665658228930686249/4000000000000000000000000000000000000) 9 (-5641365050595) (-5641365050414),
mkLog (232116223611378907947254313509996285594608774575126021477/62500000000000000000000000000000000000000000000000000000000) 9 (-5595683625748) (-5595683625566),
mkLog (14192087473972978984282228930686249/4000000000000000000000000000000000000) 9 (-5641365051033) (-5641365050852),
mkLog (14192087478285106843946228930686249/4000000000000000000000000000000000000) 9 (-5641365050730) (-5641365050548),
mkLog (36994645727499291737821049443749/500000000000000000000000000000000000) 14 (-9511590185440) (-9511590185159),
mkLog (35558243371/200000000000) 3 (-1727145356169) (-1727145356108),
mkLog (114105939244106848699975732119629/1000000000000000000000000000000000000) 14 (-9078383249620) (-9078383249339),
mkLog (170496140543273123256479491166605989391627/1250000000000000000000000000000000000000000000) 13 (-8899941449052) (-8899941448791),
mkLog (170496140561091878008979491166605989391627/1250000000000000000000000000000000000000000000) 13 (-8899941448948) (-8899941448687),
mkLog (114105939358146879115975732119629/1000000000000000000000000000000000000) 14 (-9078383248621) (-9078383248340),
mkLog (3539627966777690983665651820741046198108373/625000000000000000000000000000000000000000000) 8 (-5173730022325) (-5173730022164),
mkLog (3539627967353830720663151820741046198108373/625000000000000000000000000000000000000000000) 8 (-5173730022162) (-5173730022001),
mkLog (34099214387546266854878857301417503736657739/250000000000000000000000000000000000000000000000) 13 (-8899941851440) (-8899941851179),
mkLog (707925263614338491573486441744264621263342261/125000000000000000000000000000000000000000000000) 8 (-5173730488110) (-5173730487949),
mkLog (34099214388734183838378857301417503736657739/250000000000000000000000000000000000000000000000) 13 (-8899941851405) (-8899941851144),
mkLog (170496140549212708173979491166605989391627/1250000000000000000000000000000000000000000000) 13 (-8899941449017) (-8899941448756),
mkLog (707925263866176892075486441744264621263342261/125000000000000000000000000000000000000000000000) 8 (-5173730487755) (-5173730487594),
mkLog (228218033946954196759383552925341/2000000000000000000000000000000000000) 14 (-9078356277423) (-9078356277142),
mkLog (228218033984967540231383552925341/2000000000000000000000000000000000000) 14 (-9078356277257) (-9078356276975),
mkLog (24201218707/1000000000000) 6 (-3721352287355) (-3721352287234),
mkLog (271970665849995300737082336926469429659371/62500000000000000000000000000000000000000000000) 18 (-12344982900548) (-12344982900187),
mkLog (4573151342753134000503052866331030570340629/31250000000000000000000000000000000000000000000) 13 (-8829572116317) (-8829572116056),
mkLog (53276024543419607971197559349923/250000000000000000000000000000000000) 13 (-8453729787953) (-8453729787692),
mkLog (53276024608808208586197559349923/250000000000000000000000000000000000) 13 (-8453729786725) (-8453729786464),
mkLog (271970662005445646987082336926469429659371/62500000000000000000000000000000000000000000000) 18 (-12344982914684) (-12344982914323),
mkLog (53276024535793021666197559349923/250000000000000000000000000000000000) 13 (-8453729788096) (-8453729787835),
mkLog (53276024528541513376197559349923/250000000000000000000000000000000000) 13 (-8453729788232) (-8453729787971),
mkLog (435062476964257181781535970687437308738903/100000000000000000000000000000000000000000000000) 18 (-12345191098153) (-12345191097792),
mkLog (7314958218183728505276200224162162691261097/50000000000000000000000000000000000000000000000) 13 (-8829856961886) (-8829856961625),
mkLog (435062478664610849781535970687437308738903/100000000000000000000000000000000000000000000000) 18 (-12345191094245) (-12345191093884),
mkLog (1162460711/1000000000000) 10 (-6757216218164) (-6757216217963),
mkLog (16634057/4000000000000) 18 (-12390352699109) (-12390352698748),
mkLog (16634057/1000000000000) 16 (-11004058337969) (-11004058337648),
mkLog (11385376563/500000000000) 6 (-3782278324152) (-3782278324031),
mkLog (22725608977/200000000000) 4 (-2174824929217) (-2174824929135),
mkLog (289860147437/1000000000000) 2 (-1238356722560) (-1238356722519),
mkLog (353277718467/1000000000000) 2 (-1040500793519) (-1040500793478),
mkLog (189975876177/1000000000000) 3 (-1660858182403) (-1660858182342),
mkLog (28813507893/1000000000000) 6 (-3546910977796) (-3546910977675),
mkLog (164078439/100000000000) 10 (-6412580865004) (-6412580864803),
mkLog (33046877/1000000000000) 15 (-10317583489475) (-10317583489174),
mkLog (30187/250000000000) 23 (-15929560107930) (-15929560107469),
mkLog (7101744141118926301035884677401029/250000000000000000000000000000000000) 6 (-3561120510365) (-3561120510244),
mkLog (7101761469506073698964115322598971/250000000000000000000000000000000000) 6 (-3561118070349) (-3561118070228),
mkLog (404954567503871566008364834803275514622659977/250000000000000000000000000000000000000000000000) 10 (-6425441315134) (-6425441314933),
mkLog (6263971640779881959751129874187897110377340023/125000000000000000000000000000000000000000000000) 5 (-2993499306009) (-2993499305908),
mkLog (404954567499747927321614834803275514622659977/250000000000000000000000000000000000000000000000) 10 (-6425441315144) (-6425441314943),
mkLog (183157314541753309562806942273937809/4000000000000000000000000000000000000) 5 (-3083704214288) (-3083704214187),
mkLog (183157314541899872611426942273937809/4000000000000000000000000000000000000) 5 (-3083704214287) (-3083704214186),
mkLog (202477260251165017791488768641243121929813063/125000000000000000000000000000000000000000000000) 10 (-6425441431200) (-6425441430999),
mkLog (183157314543049792252558942273937809/4000000000000000000000000000000000000) 5 (-3083704214280) (-3083704214179),
mkLog (183157314533222618334602942273937809/4000000000000000000000000000000000000) 5 (-3083704214334) (-3083704214233),
mkLog (3131986691667425456000142484742057503070186937/62500000000000000000000000000000000000000000000) 5 (-2993499027822) (-2993499027721),
mkLog (202477260259617589998488768641243121929813063/125000000000000000000000000000000000000000000000) 10 (-6425441431159) (-6425441430958),
mkLog (4616238993362472191374596694675041/2000000000000000000000000000000000000) 9 (-6071322156776) (-6071322156595),
mkLog (4616238993324458847902596694675041/2000000000000000000000000000000000000) 9 (-6071322156784) (-6071322156603),
mkLog (5396754141019927524844849657788665652103051281/2000000000000000000000000000000000000000000000000) 9 (-5915104771783) (-5915104771602),
mkLog (80614555908406976051879798233197132847896948719/1000000000000000000000000000000000000000000000000) 4 (-2518076051418) (-2518076051337),
mkLog (5396754108571674998665706362419681339402976579/2000000000000000000000000000000000000000000000000) 9 (-5915104777796) (-5915104777615),
mkLog (5396754108590681670401706362419681339402976579/2000000000000000000000000000000000000000000000000) 9 (-5915104777792) (-5915104777611),
mkLog (5396754141029430860712849657788665652103051281/2000000000000000000000000000000000000000000000000) 9 (-5915104771781) (-5915104771600),
mkLog (80614555906076201020051798233197132847896948719/1000000000000000000000000000000000000000000000000) 4 (-2518076051447) (-2518076051366),
mkLog (80614552702585876501193235435277141160597023421/1000000000000000000000000000000000000000000000000) 4 (-2518076091186) (-2518076091105),
mkLog (80614552705169532466821235435277141160597023421/1000000000000000000000000000000000000000000000000) 4 (-2518076091154) (-2518076091073),
mkLog (4616245752281887687254223927959717/2000000000000000000000000000000000000) 9 (-6071320692615) (-6071320692434),
mkLog (5396754108543016036869706362419681339402976579/2000000000000000000000000000000000000000000000000) 9 (-5915104777801) (-5915104777620),
mkLog (4616245752168741381990223927959717/2000000000000000000000000000000000000) 9 (-6071320692640) (-6071320692459),
mkLog (11981033531264911546929194394223/125000000000000000000000000000000000) 14 (-9252744156069) (-9252744155788),
mkLog (7543354030607302077528937493405421/2000000000000000000000000000000000000) 9 (-5580235544876) (-5580235544694),
mkLog (7543354025944417409896937493405421/2000000000000000000000000000000000000) 9 (-5580235545494) (-5580235545312),
mkLog (10052473974982077841689073844908584528027440668294702069/100000000000000000000000000000000000000000000000000000000000) 14 (-9205106694236) (-9205106693955),
mkLog (186019819414674100569167591118962489589383022131705297931/50000000000000000000000000000000000000000000000000000000000) 9 (-5593925060472) (-5593925060290),
mkLog (7543354028025364248086937493405421/2000000000000000000000000000000000000) 9 (-5580235545218) (-5580235545036),
mkLog (7543354029328519447962937493405421/2000000000000000000000000000000000000) 9 (-5580235545046) (-5580235544864),
mkLog (186019822677671161832542150477708076428575247531705297931/50000000000000000000000000000000000000000000000000000000000) 9 (-5593925042931) (-5593925042749),
mkLog (3608176956119714242109073896288701099454014289668294702069/25000000000000000000000000000000000000000000000000000000000) 3 (-1935673178413) (-1935673178352),
mkLog (186019822677044456648092150477708076428575247531705297931/50000000000000000000000000000000000000000000000000000000000) 9 (-5593925042934) (-5593925042753),
mkLog (30173424773484854272797800944801/8000000000000000000000000000000000) 9 (-5580235258165) (-5580235257983),
mkLog (30173424630295216874717800944801/8000000000000000000000000000000000) 9 (-5580235262910) (-5580235262729),
mkLog (186019820236358998301317591118962489589383022131705297931/50000000000000000000000000000000000000000000000000000000000) 9 (-5593925056055) (-5593925055873),
mkLog (30173424772582315883565800944801/8000000000000000000000000000000000) 9 (-5580235258195) (-5580235258013),
mkLog (30173424772782870756325800944801/8000000000000000000000000000000000) 9 (-5580235258188) (-5580235258006),
mkLog (5990286203193421712992657276479/62500000000000000000000000000000000) 14 (-9252782644714) (-9252782644433),
mkLog (349344967694743723072873113504991/2000000000000000000000000000000000000) 13 (-8652597858527) (-8652597858266),
mkLog (371105909295634514276001741383445369109416393/2000000000000000000000000000000000000000000000000) 13 (-8592170246987) (-8592170246726),
mkLog (371105909360714607980001741383445369109416393/2000000000000000000000000000000000000000000000000) 13 (-8592170246812) (-8592170246551),
mkLog (349344967723562200408873113504991/2000000000000000000000000000000000000) 13 (-8652597858445) (-8652597858184),
mkLog (6657598871856277937572148681197335130890583607/1000000000000000000000000000000000000000000000000) 8 (-5011996389269) (-5011996389108),
mkLog (6657598868451138236716148681197335130890583607/1000000000000000000000000000000000000000000000000) 8 (-5011996389780) (-5011996389619),
mkLog (37110587272793925719475540764613981182808747/200000000000000000000000000000000000000000000000) 13 (-8592170345524) (-8592170345263),
mkLog (665759750399632530044238155458518768817191253/100000000000000000000000000000000000000000000000) 8 (-5011996594727) (-5011996594566),
mkLog (37110587272883774245875540764613981182808747/200000000000000000000000000000000000000000000000) 13 (-8592170345522) (-8592170345261),
mkLog (371105909293338385268001741383445369109416393/2000000000000000000000000000000000000000000000000) 13 (-8592170246993) (-8592170246732),
mkLog (371105909294436533924001741383445369109416393/2000000000000000000000000000000000000000000000000) 13 (-8592170246990) (-8592170246729),
mkLog (37110587272873791076275540764613981182808747/200000000000000000000000000000000000000000000000) 13 (-8592170345522) (-8592170345261),
mkLog (665759751455376803218638155458518768817191253/100000000000000000000000000000000000000000000000) 8 (-5011996593141) (-5011996592980),
mkLog (349346602335469217516552116870793/2000000000000000000000000000000000000) 13 (-8652593179379) (-8652593179118),
mkLog (349346602373627636108552116870793/2000000000000000000000000000000000000) 13 (-8652593179270) (-8652593179009),
mkLog (3948763410983925825151783819057662548242697/500000000000000000000000000000000000000000000000) 17 (-11748960908187) (-11748960907846),
mkLog (61103929713357579953537191135238837451757303/250000000000000000000000000000000000000000000000) 12 (-8316640016762) (-8316640016521),
mkLog (560191802937718680435915881145719/2000000000000000000000000000000000000) 12 (-8180378508312) (-8180378508071),
mkLog (560191802605257847075915881145719/2000000000000000000000000000000000000) 12 (-8180378508905) (-8180378508664),
mkLog (3948763409277485593151783819057662548242697/500000000000000000000000000000000000000000000000) 17 (-11748960908619) (-11748960908278),
mkLog (560191802127740151299915881145719/2000000000000000000000000000000000000) 12 (-8180378509758) (-8180378509517),
mkLog (560191802290391288419915881145719/2000000000000000000000000000000000000) 12 (-8180378509467) (-8180378509226),
mkLog (987190841563984681135404481402262258117113/125000000000000000000000000000000000000000000000) 17 (-11748960919514) (-11748960919173),
mkLog (15274684965358684740202866636808737741882887/62500000000000000000000000000000000000000000000) 12 (-8316724955200) (-8316724954959),
mkLog (987190793405255055135404481402262258117113/125000000000000000000000000000000000000000000000) 17 (-11748960968297) (-11748960967956),
mkLog (33046877/4000000000000) 17 (-11703877850615) (-11703877850274),
mkLog (16579799/4000000000000) 18 (-12393619892672) (-12393619892311),
mkLog (16579799/1000000000000) 16 (-11007325531532) (-11007325531211),
mkLog (24801433419418963/6250000000000000000000) 18 (-12437190571223) (-12437190570862),
mkLog (1062425078965637153/12500000000000000000000) 14 (-9372929818016) (-9372929817735),
mkLog (1925429434181227593/25000000000000000000000) 14 (-9471482078440) (-9471482078159),
mkLog (481357357949497901/6250000000000000000000) 14 (-9471482079677) (-9471482079396),
mkLog (49602866851186299/12500000000000000000000) 18 (-12437190570974) (-12437190570613),
mkLog (192542942293185979/2500000000000000000000) 14 (-9471482084282) (-9471482084001),
mkLog (48135735613428707/625000000000000000000) 14 (-9471482083448) (-9471482083167),
mkLog (99205733615933987/25000000000000000000000) 18 (-12437190571846) (-12437190571485),
mkLog (2124982198775053981/25000000000000000000000) 14 (-9372867678697) (-9372867678416),
mkLog (99205728849462009/25000000000000000000000) 18 (-12437190619892) (-12437190619531),
mkLog (12348373/25000000000) 11 (-7613106790457) (-7613106790236),
mkLog (13882451304278115279/250000000000000000000000) 15 (-9798590650574) (-9798590650273),
mkLog (6672287347189002819/125000000000000000000000) 15 (-9838106284682) (-9838106284381),
mkLog (3336143670613374957/62500000000000000000000) 15 (-9838106285576) (-9838106285275),
mkLog (1735306413780046023/31250000000000000000000) 15 (-9798590650144) (-9798590649843),
mkLog (128770525152885062223/125000000000000000000000) 10 (-6878037070884) (-6878037070683),
mkLog (128770524733142457711/125000000000000000000000) 10 (-6878037074144) (-6878037073943),
mkLog (13344575580368787321/250000000000000000000000) 15 (-9838106218289) (-9838106217988),
mkLog (8048159011897411743/7812500000000000000000) 10 (-6878036923044) (-6878036922843),
mkLog (266891511822016851/5000000000000000000000) 15 (-9838106217485) (-9838106217184),
mkLog (533782986678065691/10000000000000000000000) 15 (-9838106286738) (-9838106286437),
mkLog (6672287340034299333/125000000000000000000000) 15 (-9838106285755) (-9838106285454),
mkLog (13344575589908391969/250000000000000000000000) 15 (-9838106217574) (-9838106217273),
mkLog (257541089147462899359/250000000000000000000000) 10 (-6878036920067) (-6878036919866),
mkLog (13882400007439021821/250000000000000000000000) 15 (-9798594345666) (-9798594345365),
mkLog (2776480002441764829/50000000000000000000000) 15 (-9798594345322) (-9798594345021),
mkLog (1192450581/250000000000) 8 (-5345450416531) (-5345450416370),
mkLog (9875318376819223041/500000000000000000000000) 16 (-10832324826608) (-10832324826287),
mkLog (199616838216450874511/500000000000000000000000) 12 (-7825963657404) (-7825963657163),
mkLog (199616837677434892053/500000000000000000000000) 12 (-7825963660105) (-7825963659864),
mkLog (9565567803327060129/500000000000000000000000) 16 (-10864193413829) (-10864193413508),
mkLog (101323710067193159523/250000000000000000000000) 12 (-7810895755179) (-7810895754938),
mkLog (7984673538184829089/20000000000000000000000) 12 (-7825963656211) (-7825963655970),
mkLog (39923367477824803543/100000000000000000000000) 12 (-7825963661549) (-7825963661308),
mkLog (202647426621380991651/500000000000000000000000) 12 (-7810895723168) (-7810895722927),
mkLog (3802090254034975937169/500000000000000000000000) 8 (-4879057116151) (-4879057115989),
mkLog (99808397726213528471/250000000000000000000000) 12 (-7825963871635) (-7825963871394),
mkLog (19961679542735654613/50000000000000000000000) 12 (-7825963871761) (-7825963871520),
mkLog (101323714116080655661/250000000000000000000000) 12 (-7810895715219) (-7810895714978),
mkLog (39923359079203681523/100000000000000000000000) 12 (-7825963871918) (-7825963871677),
mkLog (99808397701143017659/250000000000000000000000) 12 (-7825963871886) (-7825963871645),
mkLog (1975124869973685619/100000000000000000000000) 16 (-10832293843474) (-10832293843153),
mkLog (6267627703/500000000000) 7 (-4379210172222) (-4379210172081),
mkLog (22671670055551526269/500000000000000000000000) 15 (-10001247247662) (-10001247247361),
mkLog (22671670046048190401/500000000000000000000000) 15 (-10001247248081) (-10001247247780),
mkLog (21407885342654922371/500000000000000000000000) 15 (-10058604049442) (-10058604049141),
mkLog (528471134529205904907/500000000000000000000000) 10 (-6852375191418) (-6852375191217),
mkLog (1337992995918111273/31250000000000000000000) 15 (-10058603928363) (-10058603928062),
mkLog (10703943969720724151/250000000000000000000000) 15 (-10058603928141) (-10058603927840),
mkLog (10703942672515378169/250000000000000000000000) 15 (-10058604049331) (-10058604049030),
mkLog (528471133521852302899/500000000000000000000000) 10 (-6852375193324) (-6852375193123),
mkLog (264235596170186911959/250000000000000000000000) 10 (-6852375082024) (-6852375081823),
mkLog (6605889898493275429/6250000000000000000000) 10 (-6852375082897) (-6852375082696),
mkLog (4534288156564408567/100000000000000000000000) 15 (-10001257360454) (-10001257360153),
mkLog (21407887932313946401/500000000000000000000000) 15 (-10058603928474) (-10058603928173),
mkLog (22671440725802027627/500000000000000000000000) 15 (-10001257362969) (-10001257362668),
mkLog (2375833967/500000000000) 8 (-5349259578653) (-5349259578492),
mkLog (147965629691885733/50000000000000000000000) 19 (-12730553548601) (-12730553548220),
mkLog (3577453097815209171/50000000000000000000000) 14 (-9545127162513) (-9545127162232),
mkLog (147965628841708899/50000000000000000000000) 19 (-12730553554347) (-12730553553966),
mkLog (4314505527609236583/50000000000000000000000) 14 (-9357795560416) (-9357795560135),
mkLog (4314505529059538241/50000000000000000000000) 14 (-9357795560080) (-9357795559799),
mkLog (147979258776690783/50000000000000000000000) 19 (-12730461443042) (-12730461442661),
mkLog (6903208869860121/80000000000000000000) 14 (-9357795556695) (-9357795556414),
mkLog (2157252765292427751/25000000000000000000000) 14 (-9357795559726) (-9357795559445),
mkLog (3577835992105968957/50000000000000000000000) 14 (-9545020138384) (-9545020138103),
mkLog (73989630926165253/25000000000000000000000) 19 (-12730461422257) (-12730461421876),
mkLog (25005201/50000000000) 11 (-7600694441291) (-7600694441070),
mkLog (8233539/2000000000000) 18 (-12400441804295) (-12400441803934),
mkLog (8233539/500000000000) 16 (-11014147443155) (-11014147442834),
mkLog (6139230145638681/1562500000000000000000) 18 (-12447098309923) (-12447098309562),
mkLog (2629045267392055101/31250000000000000000000) 14 (-9383153891223) (-9383153890942),
mkLog (2382747667620967083/31250000000000000000000) 14 (-9481520351331) (-9481520351050),
mkLog (595686916351327887/7812500000000000000000) 14 (-9481520352261) (-9481520351980),
mkLog (122784602775250173/31250000000000000000000) 18 (-12447098311043) (-12447098310682),
mkLog (2382747669026762319/31250000000000000000000) 14 (-9481520350741) (-9481520350460),
mkLog (595686917390393931/7812500000000000000000) 14 (-9481520350516) (-9481520350235),
mkLog (122784602897493237/31250000000000000000000) 18 (-12447098310047) (-12447098309686),
mkLog (328651081948988799/3906250000000000000000) 14 (-9383091745803) (-9383091745522),
mkLog (122784596815900803/31250000000000000000000) 18 (-12447098359578) (-12447098359217),
mkLog (15280383/31250000000) 11 (-7623204806406) (-7623204806185),
mkLog (1728688148859997467/31250000000000000000000) 15 (-9802411829914) (-9802411829613),
mkLog (2647398704702520753/50000000000000000000000) 15 (-9846200747536) (-9846200747235),
mkLog (1654624192946515161/31250000000000000000000) 15 (-9846200746020) (-9846200745719),
mkLog (6914752594260018249/125000000000000000000000) 15 (-9802411830085) (-9802411829784),
mkLog (636723540171323181/625000000000000000000) 10 (-6889171370325) (-6889171370124),
mkLog (25468941605672955621/25000000000000000000000) 10 (-6889171370371) (-6889171370170),
mkLog (13236994486369444869/250000000000000000000000) 15 (-9846200674796) (-9846200674495),
mkLog (254689452993381145767/250000000000000000000000) 10 (-6889171225345) (-6889171225144),
mkLog (6618497237874850149/125000000000000000000000) 15 (-9846200675598) (-9846200675297),
mkLog (6618496775325975501/125000000000000000000000) 15 (-9846200745485) (-9846200745184),
mkLog (13236993537672263193/250000000000000000000000) 15 (-9846200746466) (-9846200746165),
mkLog (13236994476929671917/250000000000000000000000) 15 (-9846200675509) (-9846200675208),
mkLog (1591809092912475657/1562500000000000000000) 10 (-6889171217992) (-6889171217791),
mkLog (6914729138784175767/125000000000000000000000) 15 (-9802415222182) (-9802415221881),
mkLog (1179971619/250000000000) 8 (-5355970531450) (-5355970531289),
mkLog (11332779527491757151/500000000000000000000000) 16 (-10694664008033) (-10694664007712),
mkLog (12746005408909581957/31250000000000000000000) 12 (-7804556734032) (-7804556733791),
mkLog (101968042957924063431/250000000000000000000000) 12 (-7804556737105) (-7804556736864),
mkLog (21896426280824151057/1000000000000000000000000) 16 (-10729187118143) (-10729187117822),
mkLog (205967137534378279221/500000000000000000000000) 12 (-7794646747994) (-7794646747753),
mkLog (16314886852711920099/40000000000000000000000) 12 (-7804556738365) (-7804556738124),
mkLog (407872174100369021433/1000000000000000000000000) 12 (-7804556731543) (-7804556731302),
mkLog (411934271321059555431/1000000000000000000000000) 12 (-7794646757092) (-7794646756851),
mkLog (3745236057330849710091/500000000000000000000000) 8 (-4894123450855) (-4894123450694),
mkLog (205967135654262725871/500000000000000000000000) 12 (-7794646757122) (-7794646756881),
mkLog (81574417668406316259/200000000000000000000000) 12 (-7804556941801) (-7804556941560),
mkLog (407872070493467928159/1000000000000000000000000) 12 (-7804556985561) (-7804556985320),
mkLog (411934275306904528533/1000000000000000000000000) 12 (-7794646747416) (-7794646747175),
mkLog (50984011044320710623/125000000000000000000000) 12 (-7804556941770) (-7804556941529),
mkLog (22666191287707691151/1000000000000000000000000) 16 (-10694636114439) (-10694636114118),
mkLog (12534103689/1000000000000) 7 (-4379302054666) (-4379302054525),
mkLog (26716659248040025453/500000000000000000000000) 15 (-9837076064846) (-9837076064545),
mkLog (23856776299725113491/500000000000000000000000) 15 (-9950295078994) (-9950295078693),
mkLog (524183105150078980703/500000000000000000000000) 10 (-6860522316914) (-6860522316713),
mkLog (11928388201343301427/250000000000000000000000) 15 (-9950295074679) (-9950295074378),
mkLog (524183104992045066797/500000000000000000000000) 10 (-6860522317216) (-6860522317015),
mkLog (131045779752892198213/125000000000000000000000) 10 (-6860522290470) (-6860522290269),
mkLog (32761445047769285329/31250000000000000000000) 10 (-6860522287126) (-6860522286925),
mkLog (6679157719040893211/125000000000000000000000) 15 (-9837077126801) (-9837077126500),
mkLog (5964194099474424093/125000000000000000000000) 15 (-9950295074879) (-9950295074578),
mkLog (3339578863112126467/62500000000000000000000) 15 (-9837077125726) (-9837077125425),
mkLog (2394453241/500000000000) 8 (-5341453185561) (-5341453185400),
mkLog (1839776803492688387/500000000000000000000000) 19 (-12512719115782) (-12512719115401),
mkLog (78827524893737435677/1000000000000000000000000) 14 (-9448248321551) (-9448248321270),
mkLog (3679553607494358707/1000000000000000000000000) 19 (-12512719115644) (-12512719115262),
mkLog (84152171544633049973/1000000000000000000000000) 14 (-9382883832161) (-9382883831880),
mkLog (10519021444033472371/125000000000000000000000) 14 (-9382883832071) (-9382883831790),
mkLog (3679553918991301703/1000000000000000000000000) 19 (-12512719030988) (-12512719030606),
mkLog (84152171547686941571/1000000000000000000000000) 14 (-9382883832125) (-9382883831844),
mkLog (42076084676223932271/500000000000000000000000) 14 (-9382883858212) (-9382883857931),
mkLog (39413754525328403593/500000000000000000000000) 14 (-9448248522535) (-9448248522254),
mkLog (3679553925099084899/1000000000000000000000000) 19 (-12512719029328) (-12512719028946),
mkLog (508981933/1000000000000) 11 (-7583098037243) (-7583098037022),
mkLog (8333267/2000000000000) 18 (-12388402162537) (-12388402162176),
mkLog (8333267/500000000000) 16 (-11002107801397) (-11002107801076),
mkLog (22770513649/1000000000000) 6 (-3782288841075) (-3782288840954),
mkLog (7099662854181426301035884677401029/250000000000000000000000000000000000) 6 (-3561413620330) (-3561413620209),
mkLog (7099680182568573698964115322598971/250000000000000000000000000000000000) 6 (-3561411179599) (-3561411179478),
mkLog (56797372147/500000000000) 4 (-2175118038824) (-2175118038743),
mkLog (403294850953665793149864834803275514622659977/250000000000000000000000000000000000000000000000) 10 (-6429548262433) (-6429548262232),
mkLog (6245174567423626757364004874187897110377340023/125000000000000000000000000000000000000000000000) 5 (-2996504641016) (-2996504640915),
mkLog (182475545413366038436274942273937809/4000000000000000000000000000000000000) 5 (-3087433473844) (-3087433473743),
mkLog (201647367864349378121113768641243121929813063/125000000000000000000000000000000000000000000000) 10 (-6429548548142) (-6429548547941),
mkLog (3122587677361626944354767484742057503070186937/62500000000000000000000000000000000000000000000) 5 (-2996504514951) (-2996504514850),
mkLog (72212765371/250000000000) 2 (-1241844081920) (-1241844081879),
mkLog (4418685676148105984486596694675041/2000000000000000000000000000000000000) 9 (-6115060166101) (-6115060165920),
mkLog (5215695494450407381396849657788665652103051281/2000000000000000000000000000000000000000000000000) 9 (-5949230015844) (-5949230015663),
mkLog (78509247429048406280659798233197132847896948719/1000000000000000000000000000000000000000000000000) 4 (-2544538859529) (-2544538859448),
mkLog (5215695451222169465777706362419681339402976579/2000000000000000000000000000000000000000000000000) 9 (-5949230024132) (-5949230023951),
mkLog (78509244079881991267653235435277141160597023421/1000000000000000000000000000000000000000000000000) 4 (-2544538902188) (-2544538902107),
mkLog (4418693465645945224538223927959717/2000000000000000000000000000000000000) 9 (-6115058403248) (-6115058403067),
mkLog (343737144051/1000000000000) 2 (-1067878029846) (-1067878029805),
mkLog (6679009055187166498929194394223/125000000000000000000000000000000000) 15 (-9837099384923) (-9837099384622),
mkLog (5929142331571285334236937493405421/2000000000000000000000000000000000000) 9 (-5821022889196) (-5821022889015),
mkLog (5949717786234250710189073844908584528027440668294702069/100000000000000000000000000000000000000000000000000000000000) 15 (-9729581677574) (-9729581677272),
mkLog (145158363647797640742467591118962489589383022131705297931/50000000000000000000000000000000000000000000000000000000000) 9 (-5841952974969) (-5841952974788),
mkLog (145158366449480084895892150477708076428575247531705297931/50000000000000000000000000000000000000000000000000000000000) 9 (-5841952955668) (-5841952955487),
mkLog (3230810640551422959746073896288701099454014289668294702069/25000000000000000000000000000000000000000000000000000000000) 3 (-2046142746846) (-2046142746785),
mkLog (23716579339509768711365800944801/8000000000000000000000000000000000) 9 (-5821022466993) (-5821022466812),
mkLog (3339196203978137504180157276479/62500000000000000000000000000000000) 15 (-9837191715341) (-9837191715040),
mkLog (82453258541/500000000000) 3 (-1802376528809) (-1802376528748),
mkLog (127649315733478962952873113504991/2000000000000000000000000000000000000) 14 (-9659370955482) (-9659370955201),
mkLog (158453363552509639052001741383445369109416393/2000000000000000000000000000000000000000000000000) 14 (-9443197424906) (-9443197424625),
mkLog (4608677006359080350188148681197335130890583607/1000000000000000000000000000000000000000000000000) 8 (-5379814446678) (-5379814446517),
mkLog (15845331219403339967475540764613981182808747/200000000000000000000000000000000000000000000000) 14 (-9443197749030) (-9443197748749),
mkLog (460867533849993201427038155458518768817191253/100000000000000000000000000000000000000000000000) 8 (-5379814808574) (-5379814808413),
mkLog (127651736055410230676552116870793/2000000000000000000000000000000000000) 14 (-9659351994950) (-9659351994669),
mkLog (19323819093/1000000000000) 6 (-3946416794173) (-3946416794052),
mkLog (95090826030865151783819057662548242697/500000000000000000000000000000000000000000000000) 33 (-22383041437355) (-22383041436694),
mkLog (18823065994908396085537191135238837451757303/250000000000000000000000000000000000000000000000) 14 (-9494133164572) (-9494133164291),
mkLog (253661597475478579683915881145719/2000000000000000000000000000000000000) 13 (-8972656653332) (-8972656653071),
mkLog (23761894341798135404481402262258117113/125000000000000000000000000000000000000000000000) 33 (-22383496355075) (-22383496354414),
mkLog (4703812157237229003702866636808737741882887/62500000000000000000000000000000000000000000000) 14 (-9494548558627) (-9494548558346),
mkLog (328938607/500000000000) 11 (-7326492249026) (-7326492248805)]
private def refs0 : List (Bool × Fin 476) :=
[(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,30),
(false,31),
(false,32),
(false,33),
(false,34),
(false,35),
(false,36),
(true,3),
(false,37),
(false,38),
(false,39),
(false,40),
(false,41),
(false,40),
(false,42),
(false,43),
(false,44),
(false,45),
(false,46),
(false,47),
(false,48),
(false,40),
(false,49),
(false,40),
(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,62),
(false,63),
(false,64),
(false,59),
(false,65),
(false,66),
(true,5),
(false,67),
(false,68),
(false,69),
(false,70),
(false,71),
(false,72),
(false,73),
(false,74),
(false,75),
(false,76),
(true,6),
(false,77),
(false,77),
(false,77),
(false,77),
(true,7),
(false,8),
(true,8),
(true,8),
(false,8),
(true,78),
(true,78),
(true,78),
(true,78),
(false,79),
(true,80),
(true,81),
(true,82),
(true,83),
(true,84),
(true,85),
(true,86),
(true,87),
(true,88),
(true,89),
(false,90),
(true,91),
(true,92),
(true,93),
(true,94),
(true,95),
(true,96),
(true,97),
(true,98),
(true,97),
(true,93),
(true,99),
(true,100),
(true,101),
(true,97),
(true,102),
(true,103),
(false,104),
(true,105),
(true,106),
(true,107),
(true,108),
(true,109),
(true,108),
(true,110),
(true,111),
(true,112),
(true,113),
(true,114),
(true,115),
(true,116),
(true,108),
(true,117),
(true,108),
(true,118),
(true,115),
(true,119),
(false,120),
(true,121),
(true,122),
(true,123),
(true,124),
(true,125),
(true,126),
(true,127),
(true,125),
(true,128),
(true,125),
(true,129),
(true,130),
(true,131),
(true,126),
(true,132),
(true,133),
(false,134),
(true,135),
(true,136),
(true,137),
(true,138),
(true,139),
(true,140),
(true,141),
(true,142),
(true,143),
(true,144),
(false,145),
(true,146),
(true,146),
(true,146),
(true,146),
(false,147),
(true,148),
(false,148),
(true,149),
(false,149),
(true,150),
(true,150),
(true,151),
(true,151),
(false,152),
(true,153),
(true,154),
(true,155),
(true,156),
(true,157),
(true,158),
(true,159),
(true,160),
(true,161),
(true,162),
(false,163),
(true,164),
(true,165),
(true,166),
(true,167),
(true,168),
(true,169),
(true,170),
(true,171),
(true,172),
(true,166),
(true,173),
(true,174),
(true,175),
(true,176),
(true,177),
(true,178),
(false,179),
(true,180),
(true,181),
(true,182),
(true,183),
(true,184),
(true,183),
(true,185),
(true,186),
(true,187),
(true,188),
(true,187),
(true,189),
(true,190),
(true,183),
(true,191),
(true,183),
(true,192),
(true,193),
(true,194),
(false,195),
(true,196),
(true,197),
(true,198),
(true,199),
(true,200),
(true,201),
(true,202),
(true,203),
(true,204),
(true,198),
(true,205),
(true,202),
(true,206),
(true,202),
(true,207),
(true,208),
(false,209),
(true,210),
(true,211),
(true,212),
(true,213),
(true,214),
(true,215),
(true,216),
(true,217),
(true,218),
(true,219),
(false,220),
(true,221),
(true,221),
(true,221),
(true,221),
(false,222)]
private def refs1 : List (Bool × Fin 476) :=
[(false,223),
(false,224),
(false,225),
(false,226),
(false,227),
(false,228),
(false,229),
(false,230),
(false,231),
(false,223),
(true,223),
(false,232),
(false,232),
(false,233),
(false,233),
(true,224),
(false,234),
(false,235),
(false,236),
(false,237),
(false,238),
(false,239),
(false,240),
(false,241),
(false,242),
(false,243),
(true,225),
(false,244),
(false,245),
(false,246),
(false,247),
(false,246),
(false,248),
(false,249),
(false,250),
(false,251),
(false,246),
(false,252),
(false,253),
(false,254),
(false,249),
(false,255),
(false,256),
(true,226),
(false,257),
(false,258),
(false,259),
(false,260),
(false,261),
(false,260),
(false,262),
(false,263),
(false,264),
(false,265),
(false,266),
(false,267),
(false,268),
(false,260),
(false,269),
(false,260),
(false,270),
(false,271),
(false,272),
(true,227),
(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,285),
(false,279),
(false,286),
(false,287),
(true,228),
(false,288),
(false,289),
(false,290),
(false,291),
(false,292),
(false,293),
(false,294),
(false,295),
(false,296),
(false,297),
(true,229),
(false,298),
(false,298),
(false,298),
(false,298),
(true,230),
(false,231),
(true,231),
(true,231),
(false,231),
(true,299),
(true,299),
(true,299),
(true,299),
(false,300),
(true,301),
(true,302),
(true,303),
(true,304),
(true,305),
(true,306),
(true,307),
(true,308),
(true,309),
(true,310),
(false,311),
(true,312),
(true,313),
(true,314),
(true,315),
(true,316),
(true,317),
(true,318),
(true,319),
(true,320),
(true,321),
(true,322),
(true,323),
(true,324),
(true,318),
(true,325),
(true,326),
(false,327),
(true,328),
(true,329),
(true,330),
(true,331),
(true,332),
(true,331),
(true,333),
(true,334),
(true,335),
(true,336),
(true,335),
(true,337),
(true,338),
(true,331),
(true,339),
(true,331),
(true,340),
(true,341),
(true,342),
(false,343),
(true,344),
(true,345),
(true,346),
(true,347),
(true,346),
(true,348),
(true,349),
(true,350),
(true,351),
(true,346),
(true,352),
(true,353),
(true,354),
(true,349),
(true,355),
(true,356),
(false,357),
(true,358),
(true,359),
(true,360),
(true,361),
(true,362),
(true,363),
(true,364),
(true,365),
(true,366),
(true,367),
(false,368),
(true,221),
(true,221),
(true,221),
(true,221),
(false,222),
(true,8),
(false,8),
(true,369),
(true,369),
(true,369),
(true,369),
(false,370),
(true,371),
(true,372),
(true,373),
(true,374),
(true,375),
(true,376),
(true,377),
(true,378),
(true,379),
(true,380),
(false,381),
(true,382),
(true,383),
(true,384),
(true,385),
(true,386),
(true,387),
(true,388),
(true,389),
(true,390),
(true,391),
(true,392),
(true,393),
(true,394),
(true,388),
(true,395),
(true,395),
(false,396),
(true,397),
(true,398),
(true,399),
(true,400),
(true,401),
(true,400),
(true,402),
(true,403),
(true,404),
(true,405),
(true,406),
(true,407),
(true,408),
(true,400),
(true,409),
(true,400),
(true,407),
(true,410),
(true,411),
(false,412),
(true,413),
(true,413),
(true,414),
(true,415),
(true,414),
(true,416),
(true,416),
(true,414),
(true,417),
(true,414),
(true,418),
(true,419),
(true,420),
(true,416),
(true,421),
(true,422),
(false,423),
(true,424),
(true,425),
(true,426),
(true,427),
(true,428),
(true,429),
(true,430),
(true,431),
(true,432),
(true,433),
(false,434),
(true,435),
(true,435),
(true,435),
(true,435),
(false,436),
(true,148),
(false,148),
(true,437),
(false,437),
(true,438),
(true,438),
(true,439),
(true,439),
(false,440),
(true,441),
(true,442),
(true,441),
(true,443),
(true,443),
(true,444),
(true,443),
(true,443),
(true,445),
(true,444),
(false,446),
(true,447),
(true,447),
(true,448),
(true,449),
(true,448),
(true,450),
(true,450),
(true,448),
(true,449),
(true,448),
(true,451),
(true,451),
(true,452),
(true,450),
(true,450),
(true,452),
(false,453),
(true,454),
(true,455),
(true,455),
(true,456),
(true,457),
(true,456),
(true,455),
(true,455),
(true,458),
(true,459),
(true,458),
(true,460),
(true,460),
(true,456),
(true,457),
(true,456),
(true,460),
(true,460),
(true,461),
(false,462),
(true,463),
(true,464),
(true,464),
(true,463),
(true,465),
(true,465),
(true,466),
(true,467),
(true,466),
(true,464),
(true,464),
(true,466),
(true,467),
(true,466),
(true,468),
(true,468),
(false,469),
(true,470),
(true,471),
(true,472),
(true,472),
(true,470),
(true,472),
(true,472),
(true,473),
(true,474),
(true,473),
(false,475)]
def entriesOwner3 (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.