Exact global Y/Z certificate: logs 5
Definitionmme_released_global_yz_logs_5matrix-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 477 → Entry :=
![mkLog (23074791869/1000000000000) 6 (-3769014518456) (-3769014518335),
mkLog (113875210987/1000000000000) 4 (-2172652070650) (-2172652070569),
mkLog (11583949263/40000000000) 2 (-1239258998421) (-1239258998380),
mkLog (176378340163/500000000000) 2 (-1041976750601) (-1041976750560),
mkLog (47520233993/250000000000) 3 (-1660305318756) (-1660305318695),
mkLog (1807542721/62500000000) 6 (-3543198246624) (-3543198246503),
mkLog (414926097/250000000000) 10 (-6401115772091) (-6401115771890),
mkLog (33141603/1000000000000) 15 (-10314721176738) (-10314721176437),
mkLog (1871/15625000000) 23 (-15937909706527) (-15937909706066),
mkLog (28468814970130620751238244377502599/1000000000000000000000000000000000000) 6 (-3558946002429) (-3558946002308),
mkLog (28468790523369379248761755622497401/1000000000000000000000000000000000000) 6 (-3558946861150) (-3558946861029),
mkLog (216525083430491614855645365762392568589013849/125000000000000000000000000000000000000000000000) 10 (-6358362616853) (-6358362616652),
mkLog (3114663872205738939540655212287027368910986151/62500000000000000000000000000000000000000000000) 5 (-2999045316570) (-2999045316469),
mkLog (216525083448760269316770365762392568589013849/125000000000000000000000000000000000000000000000) 10 (-6358362616768) (-6358362616567),
mkLog (91500331353300553442447047666832909/2000000000000000000000000000000000000) 5 (-3084559865970) (-3084559865869),
mkLog (91500331351644751827253047666832909/2000000000000000000000000000000000000) 5 (-3084559865988) (-3084559865887),
mkLog (433050227832245794042894886266137615974700419/250000000000000000000000000000000000000000000000) 10 (-6358362476058) (-6358362475857),
mkLog (91500331352233129055901047666832909/2000000000000000000000000000000000000) 5 (-3084559865982) (-3084559865881),
mkLog (91500331352290657367995047666832909/2000000000000000000000000000000000000) 5 (-3084559865981) (-3084559865880),
mkLog (6229330469691774280065867040926795259025299581/125000000000000000000000000000000000000000000000) 5 (-2999044879078) (-2999044878977),
mkLog (433050227769109657618394886266137615974700419/250000000000000000000000000000000000000000000000) 10 (-6358362476204) (-6358362476003),
mkLog (289287076503574914390718913866807/125000000000000000000000000000000000) 9 (-6068649477000) (-6068649476819),
mkLog (289287076502372430106718913866807/125000000000000000000000000000000000) 9 (-6068649477004) (-6068649476823),
mkLog (548581974938993388619314382860692570560548437/200000000000000000000000000000000000000000000000) 9 (-5898735924130) (-5898735923949),
mkLog (8038905538426358395084846114844403479439451563/100000000000000000000000000000000000000000000000) 4 (-2520877239165) (-2520877239084),
mkLog (548581974939947292888714382860692570560548437/200000000000000000000000000000000000000000000000) 9 (-5898735924129) (-5898735923948),
mkLog (1371454932260248731834204660613205201189787483/500000000000000000000000000000000000000000000000) 9 (-5898735927840) (-5898735927659),
mkLog (1371454932257863971160704660613205201189787483/500000000000000000000000000000000000000000000000) 9 (-5898735927841) (-5898735927660),
mkLog (548581974941847018269714382860692570560548437/200000000000000000000000000000000000000000000000) 9 (-5898735924125) (-5898735923944),
mkLog (8038905538044360105154646114844403479439451563/100000000000000000000000000000000000000000000000) 4 (-2520877239213) (-2520877239132),
mkLog (548581974940901197158114382860692570560548437/200000000000000000000000000000000000000000000000) 9 (-5898735924127) (-5898735923946),
mkLog (20097270998942617306646568463330332423810212517/250000000000000000000000000000000000000000000000) 4 (-2520876883253) (-2520876883172),
mkLog (20097270997752459494607818463330332423810212517/250000000000000000000000000000000000000000000000) 4 (-2520876883312) (-2520876883231),
mkLog (2314264696818067366332551216240433/1000000000000000000000000000000000000) 9 (-6068663267553) (-6068663267372),
mkLog (1371454932260208316045204660613205201189787483/500000000000000000000000000000000000000000000000) 9 (-5898735927840) (-5898735927659),
mkLog (2314264696766047205194551216240433/1000000000000000000000000000000000000) 9 (-6068663267576) (-6068663267395),
mkLog (96374746075550500742091332345063/1000000000000000000000000000000000000) 14 (-9247266360980) (-9247266360699),
mkLog (7879831494031436539422051361923693/2000000000000000000000000000000000000) 8 (-5536595939988) (-5536595939827),
mkLog (7879831456560960910692051361923693/2000000000000000000000000000000000000) 8 (-5536595944743) (-5536595944582),
mkLog (96987471889103774744112507534771327014300410848647441937/1000000000000000000000000000000000000000000000000000000000000) 14 (-9240928743726) (-9240928743445),
mkLog (2048747373538887885362189306704381468172380779651352558063/500000000000000000000000000000000000000000000000000000000000) 8 (-5497379529410) (-5497379529249),
mkLog (96987471913680680798112507534771327014300410848647441937/1000000000000000000000000000000000000000000000000000000000000) 14 (-9240928743473) (-9240928743192),
mkLog (7879831456487230192530051361923693/2000000000000000000000000000000000000) 8 (-5536595944753) (-5536595944592),
mkLog (7879831456511312307010051361923693/2000000000000000000000000000000000000) 8 (-5536595944750) (-5536595944589),
mkLog (2048747423778598097779504799937783344600305648651352558063/500000000000000000000000000000000000000000000000000000000000) 8 (-5497379504888) (-5497379504727),
mkLog (35397732234928839918131665183301515860213013160848647441937/250000000000000000000000000000000000000000000000000000000000) 3 (-1954813160965) (-1954813160904),
mkLog (2048747423620910404456504799937783344600305648651352558063/500000000000000000000000000000000000000000000000000000000000) 8 (-5497379504965) (-5497379504804),
mkLog (15759664296789245311067815346027057/4000000000000000000000000000000000000) 8 (-5536595856945) (-5536595856784),
mkLog (15759664295475621202931815346027057/4000000000000000000000000000000000000) 8 (-5536595857029) (-5536595856868),
mkLog (96987471901639623558112507534771327014300410848647441937/1000000000000000000000000000000000000000000000000000000000000) 14 (-9240928743597) (-9240928743316),
mkLog (2048747381689849952704189306704381468172380779651352558063/500000000000000000000000000000000000000000000000000000000000) 8 (-5497379525432) (-5497379525271),
mkLog (15759664296134412423295815346027057/4000000000000000000000000000000000000) 8 (-5536595856987) (-5536595856826),
mkLog (15759664296438241544275815346027057/4000000000000000000000000000000000000) 8 (-5536595856968) (-5536595856807),
mkLog (48187982670841674124051703933343/500000000000000000000000000000000000) 14 (-9247253709757) (-9247253709476),
mkLog (42660150701783660372274290054161/250000000000000000000000000000000000) 13 (-8675950951314) (-8675950951053),
mkLog (188967303957070003575188026002089493426304373/1000000000000000000000000000000000000000000000000) 13 (-8573936552937) (-8573936552676),
mkLog (188967303985093610199188026002089493426304373/1000000000000000000000000000000000000000000000000) 13 (-8573936552789) (-8573936552528),
mkLog (42660150856291273242274290054161/250000000000000000000000000000000000) 13 (-8675950947692) (-8675950947431),
mkLog (3340797724804662562423438097408632506573695627/500000000000000000000000000000000000000000000000) 8 (-5008398480270) (-5008398480109),
mkLog (3340797713826046366642438097408632506573695627/500000000000000000000000000000000000000000000000) 8 (-5008398483557) (-5008398483396),
mkLog (18896718763168336065731829565549185691048863/100000000000000000000000000000000000000000000000) 13 (-8573937168522) (-8573937168261),
mkLog (334079435211137966754754635972925164308951137/50000000000000000000000000000000000000000000000) 8 (-5008399489818) (-5008399489657),
mkLog (188967303971130544797188026002089493426304373/1000000000000000000000000000000000000000000000000) 13 (-8573936552863) (-8573936552602),
mkLog (334079435296318386377754635972925164308951137/50000000000000000000000000000000000000000000000) 8 (-5008399489563) (-5008399489402),
mkLog (18896718763643519161131829565549185691048863/100000000000000000000000000000000000000000000000) 13 (-8573937168497) (-8573937168236),
mkLog (6825921506411990913996851287697/40000000000000000000000000000000000) 13 (-8675907382016) (-8675907381755),
mkLog (6825921530679301182236851287697/40000000000000000000000000000000000) 13 (-8675907378461) (-8675907378200),
mkLog (2064344822156733959034148374930268208620597/250000000000000000000000000000000000000000000000) 17 (-11704403298352) (-11704403298011),
mkLog (29382399053397076270914740890330231791379403/125000000000000000000000000000000000000000000000) 13 (-8355673193000) (-8355673192738),
mkLog (11567736572681693849238748900719/40000000000000000000000000000000000) 12 (-8148414840131) (-8148414839890),
mkLog (11567736570909635416918748900719/40000000000000000000000000000000000) 12 (-8148414840284) (-8148414840043),
mkLog (2064344797110316143034148374930268208620597/250000000000000000000000000000000000000000000000) 17 (-11704403310485) (-11704403310144),
mkLog (11567736567909750442198748900719/40000000000000000000000000000000000) 12 (-8148414840544) (-8148414840303),
mkLog (11567736571490990343958748900719/40000000000000000000000000000000000) 12 (-8148414840234) (-8148414839993),
mkLog (515816755976613359994208906044416094619923/62500000000000000000000000000000000000000000000) 17 (-11704925536544) (-11704925536203),
mkLog (7339082621442749974647478462893583905380077/31250000000000000000000000000000000000000000000) 13 (-8356560803935) (-8356560803673),
mkLog (515816752447476572994208906044416094619923/62500000000000000000000000000000000000000000000) 17 (-11704925543386) (-11704925543045),
mkLog (33141603/4000000000000) 17 (-11701015537878) (-11701015537537),
mkLog (16456243/4000000000000) 18 (-12401100000374) (-12401100000013),
mkLog (16456243/1000000000000) 16 (-11014805639234) (-11014805638913),
mkLog (486696909366441167/125000000000000000000000) 18 (-12456182728811) (-12456182728450),
mkLog (11066044524789330059/125000000000000000000000) 14 (-9332187648391) (-9332187648110),
mkLog (9515918749433407981/125000000000000000000000) 14 (-9483102962332) (-9483102962051),
mkLog (475795937244822253/6250000000000000000000) 14 (-9483102962809) (-9483102962528),
mkLog (486696911603847539/125000000000000000000000) 18 (-12456182724214) (-12456182723853),
mkLog (4757959371888870937/62500000000000000000000) 14 (-9483102962927) (-9483102962646),
mkLog (9515918754281121787/125000000000000000000000) 14 (-9483102961823) (-9483102961542),
mkLog (243441209565105959/62500000000000000000000) 18 (-12455801640674) (-12455801640313),
mkLog (11073298834902572911/125000000000000000000000) 14 (-9331532316365) (-9331532316084),
mkLog (60860300977359963/15625000000000000000000) 18 (-12455801663906) (-12455801663545),
mkLog (62150177/125000000000) 11 (-7606515350494) (-7606515350273),
mkLog (28252620507363434039/500000000000000000000000) 15 (-9781177162943) (-9781177162642),
mkLog (409791776045212821/7812500000000000000000) 15 (-9855586405790) (-9855586405489),
mkLog (26226673702288663149/500000000000000000000000) 15 (-9855586404441) (-9855586404140),
mkLog (7063155121531602119/125000000000000000000000) 15 (-9781177163694) (-9781177163393),
mkLog (254605832262384004831/250000000000000000000000) 10 (-6889499603534) (-6889499603333),
mkLog (127302913352681157923/125000000000000000000000) 10 (-6889499625360) (-6889499625159),
mkLog (26226685477039503079/500000000000000000000000) 15 (-9855585955480) (-9855585955179),
mkLog (254606016420431009139/250000000000000000000000) 10 (-6889498880228) (-6889498880027),
mkLog (13113336840525818793/250000000000000000000000) 15 (-9855586405251) (-9855586404950),
mkLog (509212033352910301297/500000000000000000000000) 10 (-6889498879222) (-6889498879021),
mkLog (28251722379394357727/500000000000000000000000) 15 (-9781208952640) (-9781208952338),
mkLog (5650344567434048417/100000000000000000000000) 15 (-9781208936436) (-9781208936135),
mkLog (2359669507/500000000000) 8 (-5356086528679) (-5356086528518),
mkLog (11198064219111173481/500000000000000000000000) 16 (-10706622451782) (-10706622451461),
mkLog (391149332409976388469/1000000000000000000000000) 12 (-7846421146692) (-7846421146451),
mkLog (195574666370882310099/500000000000000000000000) 12 (-7846421145844) (-7846421145603),
mkLog (5573215366177654089/250000000000000000000000) 16 (-10711244044597) (-10711244044276),
mkLog (76024458819977354697/200000000000000000000000) 12 (-7875017530561) (-7875017530320),
mkLog (2229286148928752241/100000000000000000000000) 16 (-10711244043495) (-10711244043174),
mkLog (391149332704899261117/1000000000000000000000000) 12 (-7846421145938) (-7846421145697),
mkLog (391149332729476167171/1000000000000000000000000) 12 (-7846421145876) (-7846421145635),
mkLog (190061155793177715453/500000000000000000000000) 12 (-7875017484559) (-7875017484318),
mkLog (7504805737070163297927/1000000000000000000000000) 8 (-4892211698780) (-4892211698619),
mkLog (190061155842331527561/500000000000000000000000) 12 (-7875017484301) (-7875017484060),
mkLog (391149307046609340741/1000000000000000000000000) 12 (-7846421211536) (-7846421211295),
mkLog (391149307169493871011/1000000000000000000000000) 12 (-7846421211221) (-7846421210980),
mkLog (380122317497101336893/1000000000000000000000000) 12 (-7875017469010) (-7875017468769),
mkLog (195574653541737349911/500000000000000000000000) 12 (-7846421211441) (-7846421211200),
mkLog (22395921807884697957/1000000000000000000000000) 16 (-10706631677988) (-10706631677667),
mkLog (12288453027/1000000000000) 7 (-4399095235896) (-4399095235755),
mkLog (13174330982195091391/250000000000000000000000) 15 (-9850945883198) (-9850945882897),
mkLog (1317433098455964417/25000000000000000000000) 15 (-9850945883018) (-9850945882717),
mkLog (4655550986719594001/100000000000000000000000) 15 (-9974865196903) (-9974865196602),
mkLog (518233958013804646437/500000000000000000000000) 10 (-6871936580815) (-6871936580614),
mkLog (23277754999805447817/500000000000000000000000) 15 (-9974865194059) (-9974865193758),
mkLog (727429841748828837/15625000000000000000000) 15 (-9974865196801) (-9974865196500),
mkLog (20729358308445675629/20000000000000000000000) 10 (-6871936581399) (-6871936581198),
mkLog (64779227914040810643/62500000000000000000000) 10 (-6871936840739) (-6871936840538),
mkLog (259116910977536594999/250000000000000000000000) 10 (-6871936843358) (-6871936843157),
mkLog (26348927179723533759/500000000000000000000000) 15 (-9850935817639) (-9850935817338),
mkLog (186222040036276427/4000000000000000000000) 15 (-9974865193856) (-9974865193555),
mkLog (2634892715371345319/50000000000000000000000) 15 (-9850935818626) (-9850935818325),
mkLog (2364552779/500000000000) 8 (-5354019194229) (-5354019194068),
mkLog (692346069260903303/200000000000000000000000) 19 (-12573741994007) (-12573741993625),
mkLog (39051388284798729229/500000000000000000000000) 14 (-9457484950425) (-9457484950144),
mkLog (1730865170890568567/500000000000000000000000) 19 (-12573741995313) (-12573741994932),
mkLog (41568157687407579317/500000000000000000000000) 14 (-9395028943584) (-9395028943303),
mkLog (16627263000478051253/200000000000000000000000) 14 (-9395028948064) (-9395028947783),
mkLog (3461729986444556871/1000000000000000000000000) 19 (-12573742097960) (-12573742097579),
mkLog (83136314988317520413/1000000000000000000000000) 14 (-9395028948233) (-9395028947952),
mkLog (8313631499485129063/100000000000000000000000) 14 (-9395028948154) (-9395028947873),
mkLog (78102751675430333979/1000000000000000000000000) 14 (-9457485269161) (-9457485268880),
mkLog (3461729720067771101/1000000000000000000000000) 19 (-12573742174909) (-12573742174528),
mkLog (502597709/1000000000000) 11 (-7595720491273) (-7595720491052),
mkLog (2081787/500000000000) 18 (-12389136718102) (-12389136717741),
mkLog (2081787/125000000000) 16 (-11002842356962) (-11002842356641),
mkLog (119923/1000000000000) 23 (-15936415967019) (-15936415966558),
mkLog (11537335973/500000000000) 6 (-3769019715613) (-3769019715492),
mkLog (28464651396130620751238244377502599/1000000000000000000000000000000000000) 6 (-3559092263470) (-3559092263348),
mkLog (28464626949369379248761755622497401/1000000000000000000000000000000000000) 6 (-3559093122316) (-3559093122195),
mkLog (113858556691/1000000000000) 4 (-2172798331753) (-2172798331672),
mkLog (216092367137203550291270365762392568589013849/125000000000000000000000000000000000000000000000) 10 (-6360363074472) (-6360363074271),
mkLog (3109782448670139098387030212287027368910986151/62500000000000000000000000000000000000000000000) 5 (-3000613785245) (-3000613785144),
mkLog (216092367156037627175020365762392568589013849/125000000000000000000000000000000000000000000000) 10 (-6360363074385) (-6360363074184),
mkLog (91334058722550923125179047666832909/2000000000000000000000000000000000000) 5 (-3086378699687) (-3086378699586),
mkLog (91334058721639971314723047666832909/2000000000000000000000000000000000000) 5 (-3086378699697) (-3086378699596),
mkLog (432184795335634654825144886266137615974700419/250000000000000000000000000000000000000000000000) 10 (-6360362933187) (-6360362932986),
mkLog (91334058722256494015075047666832909/2000000000000000000000000000000000000) 5 (-3086378699690) (-3086378699589),
mkLog (91334058722300954786735047666832909/2000000000000000000000000000000000000) 5 (-3086378699689) (-3086378699588),
mkLog (6219567625732345488318492040926795259025299581/125000000000000000000000000000000000000000000000) 5 (-3000613346566) (-3000613346465),
mkLog (432184795339092714843144886266137615974700419/250000000000000000000000000000000000000000000000) 10 (-6360362933179) (-6360362932978),
mkLog (144548066933/500000000000) 2 (-1240996003069) (-1240996003028),
mkLog (282699911012477368695218913866807/125000000000000000000000000000000000) 9 (-6091683066453) (-6091683066272),
mkLog (282699911010092608021718913866807/125000000000000000000000000000000000) 9 (-6091683066462) (-6091683066281),
mkLog (539270872965554200617314382860692570560548437/200000000000000000000000000000000000000000000000) 9 (-5915854653701) (-5915854653520),
mkLog (7935258746823597465797446114844403479439451563/100000000000000000000000000000000000000000000000) 4 (-2533854224287) (-2533854224206),
mkLog (539270872966508104886714382860692570560548437/200000000000000000000000000000000000000000000000) 9 (-5915854653699) (-5915854653518),
mkLog (1348177177260443284017204660613205201189787483/500000000000000000000000000000000000000000000000) 9 (-5915854657523) (-5915854657342),
mkLog (1348177177258058523343704660613205201189787483/500000000000000000000000000000000000000000000000) 9 (-5915854657525) (-5915854657344),
mkLog (539270872967462009156114382860692570560548437/200000000000000000000000000000000000000000000000) 9 (-5915854653697) (-5915854653516),
mkLog (7935258746502131727009646114844403479439451563/100000000000000000000000000000000000000000000000) 4 (-2533854224327) (-2533854224246),
mkLog (19838154087286454064074568463330332423810212517/250000000000000000000000000000000000000000000000) 4 (-2533853860330) (-2533853860249),
mkLog (19838154086774922899608818463330332423810212517/250000000000000000000000000000000000000000000000) 4 (-2533853860356) (-2533853860275),
mkLog (2261566842458620298814551216240433/1000000000000000000000000000000000000) 9 (-6091697412882) (-6091697412701),
mkLog (1348177177255673762670204660613205201189787483/500000000000000000000000000000000000000000000000) 9 (-5915854657527) (-5915854657346),
mkLog (21751723423/62500000000) 2 (-1055473564528) (-1055473564487),
mkLog (73978617637328153780091332345063/1000000000000000000000000000000000000) 14 (-9511734457503) (-9511734457222),
mkLog (7097532829211483762484051361923693/2000000000000000000000000000000000000) 9 (-5641155224817) (-5641155224636),
mkLog (7097532791077431670296051361923693/2000000000000000000000000000000000000) 9 (-5641155230190) (-5641155230009),
mkLog (74694610424393158388112507534771327014300410848647441937/1000000000000000000000000000000000000000000000000000000000000) 14 (-9502102618176) (-9502102617895),
mkLog (1858686226488944498619689306704381468172380779651352558063/500000000000000000000000000000000000000000000000000000000000) 9 (-5594738190201) (-5594738190020),
mkLog (7097532791052359972668051361923693/2000000000000000000000000000000000000) 9 (-5641155230194) (-5641155230013),
mkLog (1858686267985420382326504799937783344600305648651352558063/500000000000000000000000000000000000000000000000000000000000) 9 (-5594738167875) (-5594738167694),
mkLog (33521530800661299093649915183301515860213013160848647441937/250000000000000000000000000000000000000000000000000000000000) 3 (-2009272975044) (-2009272974983),
mkLog (1858686267778578876895504799937783344600305648651352558063/500000000000000000000000000000000000000000000000000000000000) 9 (-5594738167987) (-5594738167805),
mkLog (14195067068602807948103815346027057/4000000000000000000000000000000000000) 9 (-5641155125475) (-5641155125293),
mkLog (14195067066797645718887815346027057/4000000000000000000000000000000000000) 9 (-5641155125602) (-5641155125421),
mkLog (74694610436929007202112507534771327014300410848647441937/1000000000000000000000000000000000000000000000000000000000000) 14 (-9502102618008) (-9502102617727),
mkLog (1858686222941299284257689306704381468172380779651352558063/500000000000000000000000000000000000000000000000000000000000) 9 (-5594738192110) (-5594738191928),
mkLog (14195067067800513624007815346027057/4000000000000000000000000000000000000) 9 (-5641155125531) (-5641155125350),
mkLog (14195067068251804181311815346027057/4000000000000000000000000000000000000) 9 (-5641155125499) (-5641155125318),
mkLog (36990021766899325145551703933343/500000000000000000000000000000000000) 14 (-9511715183248) (-9511715182967),
mkLog (35558496589/200000000000) 3 (-1727138234976) (-1727138234915),
mkLog (28533840448101943352774290054161/250000000000000000000000000000000000) 14 (-9078125429950) (-9078125429669),
mkLog (136513956623282762487188026002089493426304373/1000000000000000000000000000000000000000000000000) 13 (-8899083702373) (-8899083702112),
mkLog (136513956580516283901188026002089493426304373/1000000000000000000000000000000000000000000000000) 13 (-8899083702686) (-8899083702425),
mkLog (28533840613228069004274290054161/250000000000000000000000000000000000) 14 (-9078125424163) (-9078125423882),
mkLog (2831586060279894552761438097408632506573695627/500000000000000000000000000000000000000000000000) 8 (-5173771098510) (-5173771098349),
mkLog (2831586060415321734950438097408632506573695627/500000000000000000000000000000000000000000000000) 8 (-5173771098462) (-5173771098301),
mkLog (13651381667760435449931829565549185691048863/100000000000000000000000000000000000000000000000) 13 (-8899084727512) (-8899084727251),
mkLog (283158231927051764926954635972925164308951137/50000000000000000000000000000000000000000000000) 8 (-5173772419682) (-5173772419521),
mkLog (136513956609027269625188026002089493426304373/1000000000000000000000000000000000000000000000000) 13 (-8899083702477) (-8899083702216),
mkLog (283158231961027356248054635972925164308951137/50000000000000000000000000000000000000000000000) 8 (-5173772419562) (-5173772419401),
mkLog (13651381668235618545331829565549185691048863/100000000000000000000000000000000000000000000000) 13 (-8899084727477) (-8899084727216),
mkLog (4565783716060442295836851287697/40000000000000000000000000000000000) 14 (-9078044554613) (-9078044554332),
mkLog (4565783703705681815436851287697/40000000000000000000000000000000000) 14 (-9078044557319) (-9078044557038),
mkLog (12100672261/500000000000) 6 (-3721347088663) (-3721347088542),
mkLog (1090951003423851625034148374930268208620597/250000000000000000000000000000000000000000000000) 18 (-12342166400969) (-12342166400608),
mkLog (18316354528607746211914740890330231791379403/125000000000000000000000000000000000000000000000) 13 (-8828274665584) (-8828274665323),
mkLog (8522642572863003295318748900719/40000000000000000000000000000000000) 13 (-8453908279342) (-8453908279081),
mkLog (8522642572542772997718748900719/40000000000000000000000000000000000) 13 (-8453908279380) (-8453908279118),
mkLog (1090950973902621065034148374930268208620597/250000000000000000000000000000000000000000000000) 18 (-12342166428029) (-12342166427668),
mkLog (8522642569900873042518748900719/40000000000000000000000000000000000) 13 (-8453908279689) (-8453908279428),
mkLog (8522642570121031372118748900719/40000000000000000000000000000000000) 13 (-8453908279664) (-8453908279403),
mkLog (272375546411507400994208906044416094619923/62500000000000000000000000000000000000000000000) 18 (-12343495315525) (-12343495315164),
mkLog (4570757912717106746897478462893583905380077/31250000000000000000000000000000000000000000000) 13 (-8830095618907) (-8830095618646),
mkLog (272375548538036720994208906044416094619923/62500000000000000000000000000000000000000000000) 18 (-12343495307718) (-12343495307357),
mkLog (290625743/250000000000) 10 (-6757179864048) (-6757179863847),
mkLog (208567/50000000000) 18 (-12387273231029) (-12387273230668),
mkLog (208567/12500000000) 16 (-11000978869889) (-11000978869568),
mkLog (2277004693/100000000000) 6 (-3782309337924) (-3782309337803),
mkLog (56813306081/500000000000) 4 (-2174837538181) (-2174837538100),
mkLog (144930852297/500000000000) 2 (-1238351350476) (-1238351350435),
mkLog (353277473823/1000000000000) 2 (-1040501486017) (-1040501485976),
mkLog (47494203689/250000000000) 3 (-1660853241898) (-1660853241837),
mkLog (28813394471/1000000000000) 6 (-3546914914221) (-3546914914100),
mkLog (1640770559/1000000000000) 10 (-6412589294545) (-6412589294344),
mkLog (33061863/1000000000000) 15 (-10317130115223) (-10317130114922),
mkLog (60421/500000000000) 23 (-15928781929986) (-15928781929525),
mkLog (3550825686549650998050644026733723/125000000000000000000000000000000000) 6 (-3561133573160) (-3561133573039),
mkLog (3550837573575349001949355973266277/125000000000000000000000000000000000) 6 (-3561130225486) (-3561130225365),
mkLog (50544737971965362653297087459023926681219501/31250000000000000000000000000000000000000000000) 10 (-6426915810728) (-6426915810527),
mkLog (783065232496824384759667134944931510818780499/15625000000000000000000000000000000000000000000) 5 (-2993411471155) (-2993411471054),
mkLog (50544737970933896946484587459023926681219501/31250000000000000000000000000000000000000000000) 10 (-6426915810748) (-6426915810547),
mkLog (183159613365572805493862894117796473/4000000000000000000000000000000000000) 5 (-3083691663277) (-3083691663176),
mkLog (183159613365550789660902894117796473/4000000000000000000000000000000000000) 5 (-3083691663277) (-3083691663176),
mkLog (1617432090977577890791707121468465917928857311/1000000000000000000000000000000000000000000000000) 10 (-6426915516511) (-6426915516310),
mkLog (183159613365800733725394894117796473/4000000000000000000000000000000000000) 5 (-3083691663276) (-3083691663175),
mkLog (183159613373887813184986894117796473/4000000000000000000000000000000000000) 5 (-3083691663232) (-3083691663131),
mkLog (25058094467118189717146490702706723582071142689/500000000000000000000000000000000000000000000000) 5 (-2993411190718) (-2993411190617),
mkLog (1617432091113470226816707121468465917928857311/1000000000000000000000000000000000000000000000000) 10 (-6426915516427) (-6426915516226),
mkLog (4616588727886452889466205454172339/2000000000000000000000000000000000000) 9 (-6071246397857) (-6071246397676),
mkLog (4616588728494613197590205454172339/2000000000000000000000000000000000000) 9 (-6071246397725) (-6071246397544),
mkLog (337343650558509946965959734804437395067065497/125000000000000000000000000000000000000000000000) 9 (-5914966871004) (-5914966870823),
mkLog (5038348466290509831890761305511766386182934503/62500000000000000000000000000000000000000000000) 4 (-2518088213660) (-2518088213579),
mkLog (337343650557915968096709734804437395067065497/125000000000000000000000000000000000000000000000) 9 (-5914966871006) (-5914966870825),
mkLog (1079499696127025905135459847718569506484482751/400000000000000000000000000000000000000000000000) 9 (-5914966857720) (-5914966857539),
mkLog (1079499696138430299425059847718569506484482751/400000000000000000000000000000000000000000000000) 9 (-5914966857710) (-5914966857529),
mkLog (5038348466370455524035136305511766386182934503/62500000000000000000000000000000000000000000000) 4 (-2518088213644) (-2518088213563),
mkLog (337343650557317360853209734804437395067065497/125000000000000000000000000000000000000000000000) 9 (-5914966871008) (-5914966870827),
mkLog (16122714533025433092386243582404755593515517249/200000000000000000000000000000000000000000000000) 4 (-2518088248338) (-2518088248257),
mkLog (16122714532879316146909043582404755593515517249/200000000000000000000000000000000000000000000000) 4 (-2518088248347) (-2518088248266),
mkLog (4616595064113713946697686954475889/2000000000000000000000000000000000000) 9 (-6071245025366) (-6071245025185),
mkLog (1079499696134688077852259847718569506484482751/400000000000000000000000000000000000000000000000) 9 (-5914966857713) (-5914966857532),
mkLog (1079499696142216953390659847718569506484482751/400000000000000000000000000000000000000000000000) 9 (-5914966857706) (-5914966857525),
mkLog (4616595062888482100445686954475889/2000000000000000000000000000000000000) 9 (-6071245025632) (-6071245025451),
mkLog (95848978204923178249828996713751/1000000000000000000000000000000000000) 14 (-9252736749026) (-9252736748745),
mkLog (7544127596817384240722335512258763/2000000000000000000000000000000000000) 9 (-5580133000763) (-5580133000581),
mkLog (7544127596541600014106335512258763/2000000000000000000000000000000000000) 9 (-5580133000799) (-5580133000618),
mkLog (5032017275021209200338298430097167039394397687281160037/50000000000000000000000000000000000000000000000000000000000) 14 (-9203957332126) (-9203957331845),
mkLog (92923443779227632951969339312257152459468034712718839963/25000000000000000000000000000000000000000000000000000000000) 9 (-5594855134961) (-5594855134779),
mkLog (7544127596315930275348335512258763/2000000000000000000000000000000000000) 9 (-5580133000829) (-5580133000648),
mkLog (7544127597444136655794335512258763/2000000000000000000000000000000000000) 9 (-5580133000680) (-5580133000498),
mkLog (92923443977100464072394340904740364871727607312718839963/25000000000000000000000000000000000000000000000000000000000) 9 (-5594855132831) (-5594855132650),
mkLog (1804228665748397228915128853877813703129409960287281160037/12500000000000000000000000000000000000000000000000000000000) 3 (-1935595475882) (-1935595475821),
mkLog (92923443976161276052044340904740364871727607312718839963/25000000000000000000000000000000000000000000000000000000000) 9 (-5594855132841) (-5594855132660),
mkLog (15088258241096637556147321915751341/4000000000000000000000000000000000000) 9 (-5580132798787) (-5580132798605),
mkLog (15088258239893307252303321915751341/4000000000000000000000000000000000000) 9 (-5580132798867) (-5580132798685),
mkLog (5032017274394416759638298430097167039394397687281160037/50000000000000000000000000000000000000000000000000000000000) 14 (-9203957332251) (-9203957331970),
mkLog (92923444181608422658519339312257152459468034712718839963/25000000000000000000000000000000000000000000000000000000000) 9 (-5594855130630) (-5594855130449),
mkLog (5032017273767679910088298430097167039394397687281160037/50000000000000000000000000000000000000000000000000000000000) 14 (-9203957332376) (-9203957332095),
mkLog (15088258240344557783979321915751341/4000000000000000000000000000000000000) 9 (-5580132798837) (-5580132798655),
mkLog (15088258314657242997759321915751341/4000000000000000000000000000000000000) 9 (-5580132793912) (-5580132793730),
mkLog (95846646837834387201711461024711/1000000000000000000000000000000000000) 14 (-9252761072660) (-9252761072379),
mkLog (8734605165786986841102227318159/50000000000000000000000000000000000) 13 (-8652485543375) (-8652485543114),
mkLog (46387875670907197718395701412369495804705297/250000000000000000000000000000000000000000000000) 13 (-8592178072084) (-8592178071823),
mkLog (46387875669739548095645701412369495804705297/250000000000000000000000000000000000000000000000) 13 (-8592178072109) (-8592178071848),
mkLog (832193830787631655262234383275511254195294703/125000000000000000000000000000000000000000000000) 8 (-5012003632981) (-5012003632820),
mkLog (832193830985576503487359383275511254195294703/125000000000000000000000000000000000000000000000) 8 (-5012003632743) (-5012003632582),
mkLog (185551662416016312468325707076083196849517881/1000000000000000000000000000000000000000000000000) 13 (-8592177211233) (-8592177210972),
mkLog (3328781192506462983721717023889685303150482119/500000000000000000000000000000000000000000000000) 8 (-5012001869764) (-5012001869603),
mkLog (46387875670931928432395701412369495804705297/250000000000000000000000000000000000000000000000) 13 (-8592178072084) (-8592178071823),
mkLog (185551662430127030797325707076083196849517881/1000000000000000000000000000000000000000000000000) 13 (-8592177211156) (-8592177210895),
mkLog (3328781193783387483330717023889685303150482119/500000000000000000000000000000000000000000000000) 8 (-5012001869381) (-5012001869220),
mkLog (185551662647200325643325707076083196849517881/1000000000000000000000000000000000000000000000000) 13 (-8592177209987) (-8592177209726),
mkLog (174685768472361653100829314202237/1000000000000000000000000000000000000) 13 (-8652521806939) (-8652521806678),
mkLog (174685768496159798407829314202237/1000000000000000000000000000000000000) 13 (-8652521806803) (-8652521806542),
mkLog (1974551740085378808024829911072109926881427/250000000000000000000000000000000000000000000000) 17 (-11748874791469) (-11748874791128),
mkLog (30549061667039971241916458095232265073118573/125000000000000000000000000000000000000000000000) 12 (-8316735045923) (-8316735045682),
mkLog (1120366028086959906241918629715789/4000000000000000000000000000000000000) 12 (-8180394197515) (-8180394197274),
mkLog (1120366029204815281425918629715789/4000000000000000000000000000000000000) 12 (-8180394196518) (-8180394196277),
mkLog (1974551739927863441524829911072109926881427/250000000000000000000000000000000000000000000000) 17 (-11748874791549) (-11748874791208),
mkLog (1120366028521371686393918629715789/4000000000000000000000000000000000000) 12 (-8180394197128) (-8180394196887),
mkLog (1120366028739455091465918629715789/4000000000000000000000000000000000000) 12 (-8180394196933) (-8180394196692),
mkLog (7898207113648833345968527589969464096013569/1000000000000000000000000000000000000000000000000) 17 (-11748874772059) (-11748874771718),
mkLog (122209604576036025859307005526918535903986431/500000000000000000000000000000000000000000000000) 12 (-8316625736691) (-8316625736450),
mkLog (7898206839755884619968527589969464096013569/1000000000000000000000000000000000000000000000000) 17 (-11748874806736) (-11748874806395),
mkLog (33061863/4000000000000) 17 (-11703424476363) (-11703424476022),
mkLog (16572861/4000000000000) 18 (-12394038441295) (-12394038440934),
mkLog (16572861/1000000000000) 16 (-11007744080155) (-11007744079834),
mkLog (1984406985249177493/500000000000000000000000) 18 (-12437043256066) (-12437043255705),
mkLog (21253248193551520367/250000000000000000000000) 14 (-9372706457129) (-9372706456848),
mkLog (1203570815592865129/15625000000000000000000) 14 (-9471334656863) (-9471334656582),
mkLog (38514266087856491213/500000000000000000000000) 14 (-9471334657151) (-9471334656870),
mkLog (1984406978333057457/500000000000000000000000) 18 (-12437043259551) (-12437043259190),
mkLog (308114127469806529/4000000000000000000000) 14 (-9471334661153) (-9471334660872),
mkLog (38514266161463768739/500000000000000000000000) 14 (-9471334655240) (-9471334654959),
mkLog (1984406975369006013/500000000000000000000000) 18 (-12437043261045) (-12437043260684),
mkLog (2125154924594762981/25000000000000000000000) 14 (-9372786398581) (-9372786398300),
mkLog (992203450016349239/250000000000000000000000) 18 (-12437043299009) (-12437043298648),
mkLog (247004287/500000000000) 11 (-7612957684763) (-7612957684542),
mkLog (11104324494432748791/200000000000000000000000) 15 (-9798738019142) (-9798738018841),
mkLog (26688326976712835547/500000000000000000000000) 15 (-9838137099629) (-9838137099328),
mkLog (53376653958195192441/1000000000000000000000000) 15 (-9838137099540) (-9838137099239),
mkLog (1030105358160663138381/1000000000000000000000000) 10 (-6878094192596) (-6878094192395),
mkLog (257526340051696949061/250000000000000000000000) 10 (-6878094190610) (-6878094190409),
mkLog (26688310331083334517/500000000000000000000000) 15 (-9838137723334) (-9838137723033),
mkLog (1030104036736156823949/1000000000000000000000000) 10 (-6878095475402) (-6878095475201),
mkLog (13344163490741178447/250000000000000000000000) 15 (-9838137099450) (-9838137099149),
mkLog (53376620657397147687/1000000000000000000000000) 15 (-9838137723423) (-9838137723122),
mkLog (1030104039950814211827/1000000000000000000000000) 10 (-6878095472282) (-6878095472081),
mkLog (2668831032631381317/50000000000000000000000) 15 (-9838137723512) (-9838137723211),
mkLog (55523104257516787221/1000000000000000000000000) 15 (-9798711331061) (-9798711330760),
mkLog (55523104276594872609/1000000000000000000000000) 15 (-9798711330717) (-9798711330416),
mkLog (4769521347/1000000000000) 8 (-5345509325739) (-5345509325578),
mkLog (9875017756668115907/500000000000000000000000) 16 (-10832355268637) (-10832355268316),
mkLog (199608016990652405257/500000000000000000000000) 12 (-7826007849171) (-7826007848930),
mkLog (99804008467120542797/250000000000000000000000) 12 (-7826007849454) (-7826007849213),
mkLog (9554849156818991733/500000000000000000000000) 16 (-10865314586830) (-10865314586509),
mkLog (202806106303688724629/500000000000000000000000) 12 (-7810112996283) (-7810112996042),
mkLog (99804008404441298727/250000000000000000000000) 12 (-7826007850082) (-7826007849841),
mkLog (99804008517263938053/250000000000000000000000) 12 (-7826007848951) (-7826007848710),
mkLog (6337690849608314563/15625000000000000000000) 12 (-7810112991925) (-7810112991684),
mkLog (3801866400186964865969/500000000000000000000000) 8 (-4879115994405) (-4879115994243),
mkLog (202806107394307571447/500000000000000000000000) 12 (-7810112990905) (-7810112990664),
mkLog (49901996257626463491/125000000000000000000000) 12 (-7826008009285) (-7826008009044),
mkLog (199607985036773778371/500000000000000000000000) 12 (-7826008009254) (-7826008009013),
mkLog (4777424575275533663/250000000000000000000000) 16 (-10865314587486) (-10865314587165),
mkLog (202806109851333938991/500000000000000000000000) 12 (-7810112978790) (-7810112978549),
mkLog (99803997285143400709/250000000000000000000000) 12 (-7826007961493) (-7826007961252),
mkLog (2468786065546605597/125000000000000000000000) 16 (-10832342458056) (-10832342457735),
mkLog (6267924407/500000000000) 7 (-4379162834219) (-4379162834078),
mkLog (5668298440479651197/125000000000000000000000) 15 (-10001180042416) (-10001180042115),
mkLog (22673193916353110793/500000000000000000000000) 15 (-10001180035604) (-10001180035303),
mkLog (10705735656492091761/250000000000000000000000) 15 (-10058436556485) (-10058436556184),
mkLog (528482979189901937097/500000000000000000000000) 10 (-6852352778598) (-6852352778397),
mkLog (4282294262121653609/100000000000000000000000) 15 (-10058436556596) (-10058436556295),
mkLog (21411477478484846337/500000000000000000000000) 15 (-10058436268531) (-10058436268230),
mkLog (21411477492740339199/500000000000000000000000) 15 (-10058436267866) (-10058436267565),
mkLog (264241489425073011943/250000000000000000000000) 10 (-6852352779241) (-6852352779040),
mkLog (528483111827759356099/500000000000000000000000) 10 (-6852352527620) (-6852352527419),
mkLog (52848311169233217391/50000000000000000000000) 10 (-6852352527876) (-6852352527675),
mkLog (4534511289745393957/100000000000000000000000) 15 (-10001208151475) (-10001208151174),
mkLog (2141147749986808563/50000000000000000000000) 15 (-10058436267533) (-10058436267232),
mkLog (11336278059237359241/250000000000000000000000) 15 (-10001208166041) (-10001208165740),
mkLog (2375915477/500000000000) 8 (-5349225271289) (-5349225271128),
mkLog (9268210408123331/3125000000000000000000) 19 (-12728354532386) (-12728354532005),
mkLog (447308265453690241/6250000000000000000000) 14 (-9544844033040) (-9544844032759),
mkLog (1853642060359373/625000000000000000000) 19 (-12728354543858) (-12728354543477),
mkLog (107907921657873883/1250000000000000000000) 14 (-9357375823188) (-9357375822907),
mkLog (134884902063742419/1562500000000000000000) 14 (-9357375823252) (-9357375822971),
mkLog (1159206291992507/390625000000000000000) 19 (-12727767759780) (-12727767759399),
mkLog (33721225541735409/390625000000000000000) 14 (-9357375822487) (-9357375822206),
mkLog (16860612772431329/195312500000000000000) 14 (-9357375822394) (-9357375822113),
mkLog (55951857139346277/781250000000000000000) 14 (-9544158853128) (-9544158852847),
mkLog (4636825352477719/1562500000000000000000) 19 (-12727767719988) (-12727767719607),
mkLog (3127249/6250000000) 11 (-7600183038499) (-7600183038278),
mkLog (8244501/2000000000000) 18 (-12399111306054) (-12399111305693),
mkLog (8244501/500000000000) 16 (-11012816944914) (-11012816944593),
mkLog (982270906441933797/250000000000000000000000) 18 (-12447104333559) (-12447104333198),
mkLog (42067599560874085437/500000000000000000000000) 14 (-9383085539787) (-9383085539506),
mkLog (3812369635002030073/50000000000000000000000) 14 (-9481527337300) (-9481527337019),
mkLog (38123696500867415543/500000000000000000000000) 14 (-9481527333344) (-9481527333063),
mkLog (1964541819484956897/500000000000000000000000) 18 (-12447104330199) (-12447104329838),
mkLog (9530924142391910313/125000000000000000000000) 14 (-9481527331542) (-9481527331261),
mkLog (1191365511534066071/15625000000000000000000) 14 (-9481527336800) (-9481527336519),
mkLog (392908363016846139/100000000000000000000000) 18 (-12447104332439) (-12447104332078),
mkLog (42064236448653323713/500000000000000000000000) 14 (-9383165488410) (-9383165488129),
mkLog (1964541753474063867/500000000000000000000000) 18 (-12447104363800) (-12447104363439),
mkLog (244484789/500000000000) 11 (-7623210283215) (-7623210282994),
mkLog (13828850605568093003/250000000000000000000000) 15 (-9802459163553) (-9802459163252),
mkLog (26475047429967809947/500000000000000000000000) 15 (-9846160694570) (-9846160694269),
mkLog (6618761856311937507/125000000000000000000000) 15 (-9846160694748) (-9846160694447),
mkLog (203759868605378090649/200000000000000000000000) 10 (-6889130459810) (-6889130459609),
mkLog (1018799342564324581183/1000000000000000000000000) 10 (-6889130460264) (-6889130460063),
mkLog (52950061824236246813/1000000000000000000000000) 15 (-9846161318472) (-9846161318171),
mkLog (509399022389564896107/500000000000000000000000) 10 (-6889131734103) (-6889131733902),
mkLog (52950061843116486489/1000000000000000000000000) 15 (-9846161318116) (-9846161317815),
mkLog (509399022059160701777/500000000000000000000000) 10 (-6889131734751) (-6889131734550),
mkLog (26475031032479651341/500000000000000000000000) 15 (-9846161313926) (-9846161313625),
mkLog (55316856347049281501/1000000000000000000000000) 15 (-9802432879632) (-9802432879331),
mkLog (2765842817588467071/50000000000000000000000) 15 (-9802432879547) (-9802432879246),
mkLog (4720059919/1000000000000) 8 (-5355933784843) (-5355933784682),
mkLog (4533190528319394921/200000000000000000000000) 16 (-10694646643220) (-10694646642899),
mkLog (40785042741196360859/100000000000000000000000) 12 (-7804610050376) (-7804610050135),
mkLog (25490651711680883413/62500000000000000000000) 12 (-7804610050437) (-7804610050196),
mkLog (21878695498889696929/1000000000000000000000000) 16 (-10729997203058) (-10729997202737),
mkLog (103055132504766438101/250000000000000000000000) 12 (-7793952084904) (-7793952084663),
mkLog (407850427524776241509/1000000000000000000000000) 12 (-7804610050099) (-7804610049858),
mkLog (101962606909397218607/250000000000000000000000) 12 (-7804610049823) (-7804610049582),
mkLog (3297764193122192829/8000000000000000000000) 12 (-7793952099165) (-7793952098924),
mkLog (3745102302478779903591/500000000000000000000000) 8 (-4894159164823) (-4894159164662),
mkLog (412220523689023571949/1000000000000000000000000) 12 (-7793952100260) (-7793952100019),
mkLog (203925184199210927481/500000000000000000000000) 12 (-7804610195070) (-7804610194829),
mkLog (407850368085053430187/1000000000000000000000000) 12 (-7804610195838) (-7804610195597),
mkLog (206110269509503455971/500000000000000000000000) 12 (-7793952063071) (-7793952062830),
mkLog (10939347743177479969/500000000000000000000000) 16 (-10729997203631) (-10729997203310),
mkLog (203925184098933031553/500000000000000000000000) 12 (-7804610195562) (-7804610195321),
mkLog (407850367709011320457/1000000000000000000000000) 12 (-7804610196760) (-7804610196519),
mkLog (22666352198873299721/1000000000000000000000000) 16 (-10694629015293) (-10694629014972),
mkLog (12534736991/1000000000000) 7 (-4379251529633) (-4379251529492),
mkLog (13357511408043768147/250000000000000000000000) 15 (-9837137318091) (-9837137317790),
mkLog (667875570342327683/12500000000000000000000) 15 (-9837137318181) (-9837137317880),
mkLog (11927113032248656459/250000000000000000000000) 15 (-9950401982438) (-9950401982137),
mkLog (262091887280072852331/250000000000000000000000) 10 (-6860521039861) (-6860521039660),
mkLog (5963556459256640097/125000000000000000000000) 15 (-9950401991974) (-9950401991673),
mkLog (131045943884866788757/125000000000000000000000) 10 (-6860521037993) (-6860521037792),
mkLog (2981778257762860493/62500000000000000000000) 15 (-9950401982539) (-9950401982238),
mkLog (131045947304111363629/125000000000000000000000) 10 (-6860521011901) (-6860521011700),
mkLog (131045947246645068253/125000000000000000000000) 10 (-6860521012339) (-6860521012138),
mkLog (208710907940438001/3906250000000000000000) 15 (-9837138313775) (-9837138313474),
mkLog (5963556461651069071/125000000000000000000000) 15 (-9950401991573) (-9950401991272),
mkLog (11927112917316065707/250000000000000000000000) 15 (-9950401992074) (-9950401991773),
mkLog (6678749060080088467/125000000000000000000000) 15 (-9837138312879) (-9837138312578),
mkLog (1197214487/250000000000) 8 (-5341463320285) (-5341463320124),
mkLog (1841014986185167929/500000000000000000000000) 19 (-12512046335136) (-12512046334755),
mkLog (9848848847140312221/125000000000000000000000) 14 (-9448714436382) (-9448714436101),
mkLog (92050749334697559/25000000000000000000000) 19 (-12512046334860) (-12512046334478),
mkLog (21029597818788721599/250000000000000000000000) 14 (-9383285331620) (-9383285331339),
mkLog (3682029194440745079/1000000000000000000000000) 19 (-12512046546414) (-12512046546032),
mkLog (84118391271593403639/1000000000000000000000000) 14 (-9383285331662) (-9383285331381),
mkLog (84118393285357511097/1000000000000000000000000) 14 (-9383285307723) (-9383285307442),
mkLog (78790774763169672543/1000000000000000000000000) 14 (-9448714639628) (-9448714639347),
mkLog (230126825765509929/62500000000000000000000) 19 (-12512046541577) (-12512046541196),
mkLog (508783251/1000000000000) 11 (-7583488465223) (-7583488465002),
mkLog (3330883/800000000000) 18 (-12389129572824) (-12389129572463),
mkLog (3330883/200000000000) 16 (-11002835211684) (-11002835211363),
mkLog (22769807263/1000000000000) 6 (-3782319863518) (-3782319863397),
mkLog (3549783818580900998050644026733723/125000000000000000000000000000000000) 6 (-3561427031904) (-3561427031783),
mkLog (3549795705606599001949355973266277/125000000000000000000000000000000000) 6 (-3561423683248) (-3561423683127),
mkLog (113593272387/1000000000000) 4 (-2175130996435) (-2175130996354),
mkLog (50336992431247556347734587459023926681219501/31250000000000000000000000000000000000000000000) 10 (-6431034412452) (-6431034412251),
mkLog (780715855727297620129542134944931510818780499/15625000000000000000000000000000000000000000000) 5 (-2996416212106) (-2996416212005),
mkLog (182477834451166989522678894117796473/4000000000000000000000000000000000000) 5 (-3087420929569) (-3087420929468),
mkLog (1610782493675636327792707121468465917928857311/1000000000000000000000000000000000000000000000000) 10 (-6431035197240) (-6431035197039),
mkLog (24982889891167423263594990702706723582071142689/500000000000000000000000000000000000000000000000) 5 (-2996416912270) (-2996416912169),
mkLog (288852561503/1000000000000) 2 (-1241838888880) (-1241838888839),
mkLog (4419035861574428325138205454172339/2000000000000000000000000000000000000) 9 (-6114980918203) (-6114980918022),
mkLog (326027226214139572855959734804437395067065497/125000000000000000000000000000000000000000000000) 9 (-5949088122502) (-5949088122321),
mkLog (4906765122071753876670886305511766386182934503/62500000000000000000000000000000000000000000000) 4 (-2544551666712) (-2544551666631),
mkLog (1043287133474616779755459847718569506484482751/400000000000000000000000000000000000000000000000) 9 (-5949088113310) (-5949088113129),
mkLog (15701647772607751168140243582404755593515517249/200000000000000000000000000000000000000000000000) 4 (-2544551706072) (-2544551705991),
mkLog (4419044853453301811045686954475889/2000000000000000000000000000000000000) 9 (-6114978883399) (-6114978883218),
mkLog (343736784921/1000000000000) 2 (-1067879074627) (-1067879074586),
mkLog (53432990049989971830828996713751/1000000000000000000000000000000000000) 15 (-9837082211706) (-9837082211405),
mkLog (5929994674030847402514335512258763/2000000000000000000000000000000000000) 9 (-5820879144764) (-5820879144583),
mkLog (2982597584394825180588298430097167039394397687281160037/50000000000000000000000000000000000000000000000000000000000) 15 (-9726983691115) (-9726983690812),
mkLog (72477625213566552910419339312257152459468034712718839963/25000000000000000000000000000000000000000000000000000000000) 9 (-5843353207457) (-5843353207276),
mkLog (72477625514220308180969340904740364871727607312718839963/25000000000000000000000000000000000000000000000000000000000) 9 (-5843353203309) (-5843353203128),
mkLog (1615554448181753609676128853877813703129409960287281160037/12500000000000000000000000000000000000000000000000000000000) 3 (-2046050435015) (-2046050434954),
mkLog (11859992887258903304587321915751341/4000000000000000000000000000000000000) 9 (-5820878846349) (-5820878846168),
mkLog (53430006114588242704711461024711/1000000000000000000000000000000000000) 15 (-9837138057705) (-9837138057404),
mkLog (164906228951/1000000000000) 3 (-1802378276049) (-1802378275988),
mkLog (3192753921065181042752227318159/50000000000000000000000000000000000) 14 (-9658894442043) (-9658894441762),
mkLog (19806188467566874971395701412369495804705297/250000000000000000000000000000000000000000000000) 14 (-9443221759251) (-9443221758970),
mkLog (576080743139187456308984383275511254195294703/125000000000000000000000000000000000000000000000) 8 (-5379821186433) (-5379821186272),
mkLog (79224979929613396621325707076083196849517881/1000000000000000000000000000000000000000000000000) 14 (-9443218905863) (-9443218905582),
mkLog (2304330151748819675640217023889685303150482119/500000000000000000000000000000000000000000000000) 8 (-5379818070905) (-5379818070744),
mkLog (63845807867795584378829314202237/1000000000000000000000000000000000000) 14 (-9659039633729) (-9659039633448),
mkLog (3864762641/200000000000) 6 (-3946417098874) (-3946417098753),
mkLog (77341018856264524829911072109926881427/250000000000000000000000000000000000000000000000) 32 (-21896502295309) (-21896502294668),
mkLog (9405537680045689699166458095232265073118573/125000000000000000000000000000000000000000000000) 14 (-9494770385711) (-9494770385430),
mkLog (507262328495024027377918629715789/4000000000000000000000000000000000000) 13 (-8972776636231) (-8972776635970),
mkLog (309532742359929968527589969464096013569/1000000000000000000000000000000000000000000000000) 32 (-21895957238575) (-21895957237934),
mkLog (37642269635487442526307005526918535903986431/500000000000000000000000000000000000000000000000) 14 (-9494235766148) (-9494235765867),
mkLog (657792407/1000000000000) 11 (-7326621167409) (-7326621167188)]
private def refs0 : List (Bool × Fin 477) :=
[(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,27),
(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,49),
(false,50),
(false,49),
(false,51),
(false,52),
(false,53),
(true,4),
(false,54),
(false,55),
(false,56),
(false,57),
(false,58),
(false,59),
(false,60),
(false,61),
(false,60),
(false,62),
(false,56),
(false,60),
(false,63),
(false,64),
(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,99),
(true,93),
(true,97),
(true,100),
(true,97),
(true,101),
(true,102),
(false,103),
(true,104),
(true,105),
(true,106),
(true,107),
(true,108),
(true,109),
(true,110),
(true,111),
(true,112),
(true,113),
(true,114),
(true,115),
(true,116),
(true,107),
(true,117),
(true,107),
(true,118),
(true,115),
(true,119),
(false,120),
(true,121),
(true,122),
(true,123),
(true,124),
(true,123),
(true,125),
(true,125),
(true,126),
(true,127),
(true,123),
(true,128),
(true,129),
(true,130),
(true,125),
(true,131),
(true,132),
(false,133),
(true,134),
(true,135),
(true,136),
(true,137),
(true,138),
(true,139),
(true,140),
(true,141),
(true,142),
(true,143),
(false,144),
(true,145),
(true,145),
(true,145),
(true,145),
(false,146),
(true,147),
(false,147),
(true,148),
(false,148),
(true,149),
(true,149),
(true,150),
(true,150),
(false,151),
(true,152),
(true,153),
(true,154),
(true,155),
(true,156),
(true,157),
(true,158),
(true,159),
(true,160),
(true,161),
(false,162),
(true,163),
(true,164),
(true,165),
(true,166),
(true,167),
(true,168),
(true,169),
(true,170),
(true,171),
(true,170),
(true,172),
(true,173),
(true,174),
(true,169),
(true,175),
(true,174),
(false,176),
(true,177),
(true,178),
(true,179),
(true,180),
(true,181),
(true,180),
(true,179),
(true,182),
(true,183),
(true,184),
(true,185),
(true,186),
(true,187),
(true,188),
(true,189),
(true,188),
(true,190),
(true,191),
(true,192),
(false,193),
(true,194),
(true,195),
(true,196),
(true,197),
(true,198),
(true,199),
(true,200),
(true,201),
(true,200),
(true,202),
(true,196),
(true,200),
(true,203),
(true,204),
(true,205),
(true,206),
(false,207),
(true,208),
(true,209),
(true,210),
(true,211),
(true,212),
(true,213),
(true,214),
(true,215),
(true,216),
(true,217),
(false,218),
(true,219),
(true,219),
(true,219),
(true,219),
(false,220)]
private def refs1 : List (Bool × Fin 477) :=
[(false,221),
(false,222),
(false,223),
(false,224),
(false,225),
(false,226),
(false,227),
(false,228),
(false,229),
(false,221),
(true,221),
(false,230),
(false,230),
(false,231),
(false,231),
(true,222),
(false,232),
(false,233),
(false,234),
(false,235),
(false,236),
(false,237),
(false,238),
(false,239),
(false,240),
(false,241),
(true,223),
(false,242),
(false,243),
(false,244),
(false,245),
(false,246),
(false,247),
(false,248),
(false,246),
(false,249),
(false,250),
(false,251),
(false,252),
(false,253),
(false,254),
(false,255),
(false,256),
(true,224),
(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,269),
(false,270),
(false,271),
(false,272),
(false,273),
(false,274),
(true,225),
(false,275),
(false,276),
(false,277),
(false,275),
(false,278),
(false,279),
(false,280),
(false,281),
(false,280),
(false,277),
(false,282),
(false,283),
(false,284),
(false,285),
(false,286),
(false,287),
(true,226),
(false,288),
(false,289),
(false,290),
(false,291),
(false,292),
(false,293),
(false,294),
(false,295),
(false,296),
(false,297),
(true,227),
(false,298),
(false,298),
(false,298),
(false,298),
(true,228),
(false,229),
(true,229),
(true,229),
(false,229),
(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,312),
(true,315),
(true,316),
(true,317),
(true,318),
(true,317),
(true,314),
(true,319),
(true,320),
(true,321),
(true,322),
(true,323),
(true,324),
(false,325),
(true,326),
(true,327),
(true,328),
(true,329),
(true,330),
(true,329),
(true,331),
(true,332),
(true,333),
(true,334),
(true,335),
(true,336),
(true,337),
(true,338),
(true,339),
(true,338),
(true,337),
(true,340),
(true,341),
(false,342),
(true,343),
(true,344),
(true,345),
(true,346),
(true,347),
(true,348),
(true,349),
(true,347),
(true,350),
(true,347),
(true,351),
(true,352),
(true,353),
(true,348),
(true,354),
(true,355),
(false,356),
(true,357),
(true,358),
(true,359),
(true,360),
(true,361),
(true,362),
(true,363),
(true,364),
(true,365),
(true,366),
(false,367),
(true,219),
(true,219),
(true,219),
(true,219),
(false,220),
(true,8),
(false,8),
(true,368),
(true,368),
(true,368),
(true,368),
(false,369),
(true,370),
(true,371),
(true,372),
(true,373),
(true,374),
(true,375),
(true,376),
(true,377),
(true,378),
(true,379),
(false,380),
(true,381),
(true,382),
(true,383),
(true,381),
(true,384),
(true,385),
(true,386),
(true,387),
(true,386),
(true,383),
(true,383),
(true,388),
(true,389),
(true,390),
(true,391),
(true,392),
(false,393),
(true,394),
(true,395),
(true,396),
(true,397),
(true,398),
(true,397),
(true,399),
(true,400),
(true,401),
(true,402),
(true,403),
(true,404),
(true,405),
(true,397),
(true,406),
(true,407),
(true,408),
(true,409),
(true,410),
(false,411),
(true,412),
(true,413),
(true,414),
(true,415),
(true,414),
(true,416),
(true,416),
(true,414),
(true,417),
(true,418),
(true,419),
(true,420),
(true,421),
(true,422),
(true,423),
(true,424),
(false,425),
(true,426),
(true,427),
(true,428),
(true,429),
(true,429),
(true,430),
(true,431),
(true,432),
(true,433),
(true,434),
(false,435),
(true,436),
(true,436),
(true,436),
(true,436),
(false,437),
(true,147),
(false,147),
(true,438),
(false,438),
(true,439),
(true,439),
(true,440),
(true,440),
(false,441),
(true,442),
(true,443),
(true,442),
(true,444),
(true,444),
(true,445),
(true,444),
(true,444),
(true,446),
(true,445),
(false,447),
(true,448),
(true,448),
(true,449),
(true,450),
(true,449),
(true,451),
(true,451),
(true,449),
(true,450),
(true,449),
(true,452),
(true,452),
(true,453),
(true,451),
(true,451),
(true,453),
(false,454),
(true,455),
(true,456),
(true,456),
(true,457),
(true,458),
(true,457),
(true,456),
(true,456),
(true,459),
(true,460),
(true,459),
(true,461),
(true,461),
(true,457),
(true,458),
(true,457),
(true,461),
(true,461),
(true,462),
(false,463),
(true,464),
(true,465),
(true,465),
(true,464),
(true,466),
(true,466),
(true,467),
(true,468),
(true,467),
(true,465),
(true,465),
(true,467),
(true,468),
(true,467),
(true,469),
(true,469),
(false,470),
(true,471),
(true,472),
(true,473),
(true,473),
(true,471),
(true,473),
(true,473),
(true,474),
(true,475),
(true,474),
(false,476)]
def entriesOwner5 (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.