# Manifold: Census Knot K8_57

# Number of Tetrahedra: 8

# Number Field
x^40 + 22*x^39 + 145*x^38 - 470*x^37 - 6928*x^36 + 29802*x^35 - 20301*x^34 + 366865*x^33 + 772812*x^32 - 3949223*x^31 - 12233283*x^30 - 56119268*x^29 - 78862748*x^28 + 114692993*x^27 + 388128257*x^26 + 940110674*x^25 + 166296878*x^24 - 3697955432*x^23 - 1433624387*x^22 + 6258151401*x^21 + 866850575*x^20 - 5634893107*x^19 + 1044668061*x^18 + 2391760306*x^17 - 1382966093*x^16 - 198558269*x^15 + 612032822*x^14 - 191440162*x^13 - 145834408*x^12 + 84307095*x^11 + 19956448*x^10 - 17569964*x^9 - 403280*x^8 + 1498704*x^7 - 20650*x^6 - 67967*x^5 - 513*x^4 + 1818*x^3 + 52*x^2 - 20*x - 1 

# Approximate Field Generator
0.139662073143227 - 0.593552940545443*I

# Shape Parameters
256595524940443391001921088226470288186074183083863729670638999993849002533157839041766621235256139601509377002423244240751386781808266886733546480411148846174967353343193750366178066394395450779598303/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^39 + 2851780943512877134813163551754817163927067852052516855208587758891739711024922786968905250018224539709205622267873978574958469477344611841490396447860935518481767733194344513070795842949645667248395837/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^38 + 1750269467637605058819548347934082151053999268680705026598800523239512232474588393333997509521627821046650234671393558426812912481756555428453239339218255786295460744380372595796804712387935623671070764/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^37 - 111824016862462700435215676482776448466415139797924640293230769366334649861541402936569939746578405900501720672807979122156683089686241749507329555238713770378611397254882248479859434553061864424023949499/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^36 - 1803147899124185613407993335479695589461595594479943921584634754946623818691104130811875766481731601906665162440662723916100053786651538639568295027932277984382170745852878875081812533369603221417402613343/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^35 + 3618106617429797024711163745949530118385119964086374353467391957096734669523786770183524348702734939084784779039633871220026322229154189680714652450196834576814420927587422619352721814650809687814213339347/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^34 - 1780742389831674130826099926478459825916919888453859496604825520303936313632946093414600915573502154750730077861592250458593434568477298859350874845458600513424890723026801851341944763014027567049376865009/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^33 + 46663581708034666097045053027382092768476864328770643736861989413142351588143424378988897875516299593976124755012624417176598746905309209045824091050585336307237285449865282631145973567671256464196768041786/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^32 + 219564670127253231412140151435516089466722961495526530095014797005083582677141179438965752096512526965364049019864641469683208339561672627327306072959299902443489454240629971695591166052510072454195538154211/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^31 - 481641203289641751956079025977291076985261578205155783145905847890562131497683768089532548047624851837581456950223298093736594535164145494016220054725782676831792760220729573161385099686732200162738681534603/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^30 - 78100166705516245652758349002835340722993806153622564797040302950209862201331553762932396669991667224369771066711558760295574782440045603153792213528100154515634628317218239695542343708743098248326323993209/204208094045859345905563662322141147964674420858859843475663856641013906233113710384960519092726269905099277379105923052069884196349563614789855042771850247301121091994219663549557874091812988194402*y^29 - 7582712534890740800683895551378419542179577928950899198429231062421977598411550032606819585453531407999858731012162818513841300792038975167208801476647742468162365956357597621146637641807139159781870890042060/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^28 - 23693158586623934260109346746682916438569912080834334986273614260654182069748157247416443884037128403622823013158755603234738571193518647331514893920122228600746532892618782890471711600982645910847540594975999/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^27 + 12010951191689447374013953443884215035325202194489375467766456069131993432163755928528446239980878491760118653111038406869338906227699282433840880365416628838438639848362119950995228858294218809473895495047987/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^26 + 105043491590591623839907934815426433386593417559743050024714376346153474535789053743304154374052339405186357793249088868027931424199990251791518945090708269681197788010188251431179706874754468361869733955906735/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^25 + 132577633576569550467562993071763444560957467656469611321206394921251436870444941431640612412960305822566101217487862149745782474287110748749842285606891116820462235592009264126142828862891872539865348184676161/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^24 + 103140329022232274200560748160244156643319655372449326053327657398128536461416637614199069490701954002440638374691706547260084241221648259677368535438477882436512715292215257349738996165196479349263314294440193/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^23 - 925186009064878352842080805999574586061538140964746861279878605720716822997523233413182149206042981689728168027112982055923953874202481368295708154141873848866136409910444350168037893293977562144543594692951969/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^22 - 578421825917334884122862198260005150601837352887094133068186644334281162711187975054991642861490358914148786061199552642987548528445451371859416349396558649212587852799760069909978619322915466357801378127694477/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^21 + 736847773020754008840774093445769265234290604590090367925486942675429892495304109810702780534684755933467971832635854388380743480355308147103912081247881498169850044393060696426036873216134697702275621903262712/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^20 + 557445250775970575455359752823577162922664303096509494170958888847081203516801452776820890470169643590237708912393619266830065970087100350169447064321791294409944170289822416929490258496788424519560331759358161/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^19 - 1318632795164558601823738222334087565060901842867706648984875499778376861397891098992466679963534400712123718247399979976686225272490078585670773674662001601235635149011945459967640075748479898641637930790648651/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^18 - 15756358146352185540667414187209497373224600964458570933376490136365521363785201991353748371138216753781433896056020621370326188287001388823253254921578193473385805391781343805738685101853194185976286647231729/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^17 + 303187670370404411515443924781398302684681798310608476262285949862545338268685810754113470339779006892673809114001776491234487119130190962868522605094876637389807630214460488741454835461665541967636487867982571/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^16 - 217194242476803372078836910955745998043773934917389933233483213981534772476183637464632714122209663751194612645575059683716849853284901300435817621596925618352384983747323069209819128737711976061559117826934767/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^15 - 9118068883654124002168774058794681805918184566087785744024516823461024334201260089999504263682498397032278472130665817402418158538620669246881132887800959775277012321270919275466848266333483797058622688204101/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^14 + 134303921592030177878119024971376460430019208015814677524917789863351012474624032855282858939508066098791219164320878411931985780811088961657707326989957929662312468687708510143903888735894273241331313014567371/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^13 - 9306975694223060156647057742777798134178182170397816583583601635265696361498929220361753598526600858017902231421747939441600776764884458070062851353977534755698578602992028422107078216548384706052749364192973/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^12 - 41645410215896215882652348772858641120837000745954282186310492086723873595816742167201240318191002546970254853612052547664267972764717618834994634162164664270875095879273808942336324073729724945942310176980723/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^11 + 6091335966723710226997584687105926260029508152796991561650677890046074670535998844927621320770426894623432186019857253202041960771646859004816379139358324912548441543210741516275389211138189838673058626482245/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^10 + 3940396219750427396893293874742731172846357892817431151381174787745712101450301495279188281023570077667355141757641164768669565151532626261982832858639740654999371891725732466615085041831967744330882223816837/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^9 - 1361533091551422732765044944563330352785682047104866940395332589691604600065828041863294763813754370205071342283528599739481630139029748059344080195180958176610246181609787278378260637873937178338305090005841/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^8 - 359956008885034037281896374575151247111779174635412876432762248076192171892123211568836848903050181167533304426166404219358708880832181329284139903521807505247945326152226286196655023370016306573770684726048/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^7 + 10097197537653568586287995689256487450177027683137478505453533012822899905756300494543682396133834024053800852146583508645817760837228205665841889377437065026085030260356436233707914214053337148889115107606/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^6 + 22404423782568741497166560253082533766044206923092340426970099355049078111631162643069797563006863407073380590253409892820854543116799430941191696636142611798269592541266988256861697321367479048245382198682/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^5 - 667324319277856262275624515276924238441553763458099772682316511619768683722591115534386791103359850657291268550378059079584459728965553807685145498013743238632675498612047684327455513499100817893032921085/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^4 - 1784927172995069580108673644227487215314828711630276141443229502597558745810195320462524051054194917486693815235689948778214576889707644561549417493362860934402705365173406981747119784752941696828737263245/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^3 + 64876026189917387509736921300058549947542408078917092125850968051417929818313475244903938639081652647541257354007045662062553884342328842908783294667947973995694795310810693058932912740568840737478894717/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^2 + 13967388632956331737148614948792686999485644026385008639095121630417267110554225928306112504756920302356736427710733182988786509125247185457039600784632233258759803876429402694321016339014022526911214146/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y + 1140180993602424241234524366004384032774084319757316374998529060450461058527864604989562769806145280546495114080757985955946578746077546001058152054194713997070586853587480836512686148656636591964057503/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286

-6268388248865132693855171883042935463590137789381120942012800595083661132050869733127659465348734731103046161989197201913508005808824624418909459970487016758008154973805266267145833181547404322026848/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^39 - 3065149437628347217226115733531777301799531447343240387117055320185785938920140135382522707557713528913641353189974664287070603422042208258411550816558545193851451597656733140879628760340506608933316497/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^38 - 20690433461257840180257481745647739899989058316910847413366967235440159388959265785702081581991260634278042347503301739999807800755067986999338498617432337699933589118931563460339307016542470388492334029/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^37 + 60133100377536725793244029168175236390560056472698649136279106772896983958297696260746448186944965539286362414212257705711662332083625993811932137573317734872433414368764623460677864641924650067365993799/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^36 + 484535532044212911671436514857350715294594150291700292591599396564617159519116852247315513214421156128963857645213336417403460986790001401625919651512326824715303092327128135414563404742452871120641500976/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^35 - 3890381571770730342352685421513945509794775544773382442784306938734321146078556050609831720208873061930888301688427056813333151416635785632816387664973179790566887813630897081519499055156919379095138659419/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^34 + 1915996691689455490118192818568851722302983435421213972483662697588752540579953970693096112852658310807653380696209311252673998677666957431310109835241633858886010462071500658014595933407536842357121736555/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^33 - 50149109895327496538415104856149414391741927485882313218009654385517732315694323951762489526914437744852271270046425936460530135270239216216264665678702536687308771952581263290134119154233404541984625671465/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^32 - 117945280067284540517612889060477375066801658655905388077530040218458744518931007213831491059429257494971783896124879863233530391909594740877545313868919684888441412798317034429485604728002160687151284951491/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^31 + 258999186163962587864649928566249595658928537547661447053384499895620531479983324695152388934502564232474568539110005962955237389559522527118149945554309058392179459884595584604945185072865600522092266494829/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^30 + 1907632051342919600544107314287241666428633208098560850143597787438353881409062454440572552422797818054898644178821315201490237623163645520979052062814492229806730199755862246008308303721185873960438241503/9282186092993606632071075560097324907485200948129992885257448029136995737868805017498205413305739541140876244504814684184994736197707437035902501944175011240960049636100893797707176095082408554291*y^29 + 8146835962056595508298219327274347166367780690459831369901792399723358464866203860911148184441070502814159447346948436585545334835094990896221304096840094485759068406276341273483102639611533062995507850591535/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^28 + 1156194969705092843224243604396509569109330937445217100565902776894572434071504956333723569634361625341245491051879874327637164839047047959244017202477374071454334551132931320291275158265421496643870778919507/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^27 - 6475437458374747088193486141183241398424156423928094293829314095654808524597765488585611585996399261543065336592636438361423317227740862203725202092387504495237192466766920065898960976116129741452643929658317/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^26 - 28240273147852527258161213528145058163015555866271410304417252137282320994021409352647853642634377969496044220411214094548614747967259055158506471161971602553131002698375888906122359959629662847974656565770904/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^25 - 142407028124937643143801864530111555284986648680346221093570216731708443723667744692439312171124185048188864074594912581725983003916235617171999273321412531165397075103336717860390026994424118602524933585979067/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^24 - 55091287822522103445085613484793499364844843185665756681127121329803845928310920476127089062158666768223563695767716152892322870808047304266826290885217371236514334240841910518553118637031235422708877944188185/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^23 + 248873005420645664666482160181148179339050447261747614088055045925917248928002102756703589052734878155745782048691394145543695187297748073270688648899425851373285001092377087773988269701961869169909685123220847/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^22 + 310506892656941028056809079610966285281012736338706196729019341237994558174050545151219610532555551494176569552750045640011677874936851477433501213210580649895128549620524870337911001836666361973853356282170427/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^21 - 396886680379262410486678750654586160119443695544300319138845140944195298851530745796712020695896996631190972252155645265584815881620027108354343364890934171251090717462051788999841064106382094395499444169189910/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^20 - 149858500172144931457474238066992475362533986208316191443545342385438062083460354851197168318104026409613723878632085019420278521096118286304198621372235239248957499574939565564375476099219857159591597447009785/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^19 + 711064000102683409963258701949887168096955351858800175889699075482209831057671574686849408590509008496306573604159515269344028693639293661996541099066473739547170497593248815055715263891417537233297305648506359/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^18 + 8567502802318753854321347372270393171374515443370967517022968650243457902345870865229797662081856066686019290379687512572153105761926807128213886526875346488818556872156489479121459479355243385089019395296178/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^17 - 163814256186998657500033728837307905424242878248749712839989735281272410498108233079097224559174726969631339481749985697251729482356203828627242431477569794510135900182509451076212366645465940074908384090334937/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^16 + 58466965059058721388191930418127278842868997424835738191614420343347304992342114891471432067000214584883988792564788448970697566079148680256448041732638755540351493120802359533853219420370086567388539008178764/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^15 + 54526898935675945974459633686397061200818325984725372143080930841864283390173043259960769223983222630111160598244225316237983056232388430756191168999891427370408844739627952590652485611935917724777685421937665/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^14 - 36249597800623815240709854747112721195323987146123481724619531396189835418408061428732718786445893079895131086951461479591492766423101591070675747068182103929939329778771994259703865209085492652139219166461647/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^13 + 9965779646960212297699451891192239383130870937964330663824524908134570947362799747299046115148300346674292875428273036275444549673139230933462683603837563283068835801390208710774865527760057002050975171681619/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^12 + 22540491771573469113537732849990142665684547034764076239759390647283891037420701791051065803796800756603159729806897027151384639711196728535427194006460061671367221506118528489366947529640594209793664992695875/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^11 - 299564179985364788231812817713627769762131417157883004163533507936767245974977627969948682365795773649854312721425303906016970500034945489577312146176482375877287243663751251428952353165742453938474903727751/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^10 - 2139727184870736404337013430788333111723157388278963476583804461206468834256566177729578856906343507941402451066365462151932654184292950332172484688900516044678022284367317719729577642925027723152330644335233/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^9 + 739622023150263509631008968960643558394146631127482576020433223787051432301796099130280091603574780114662060648172437881193578035606495554390156877514487588273368564084821557110344751782877519311838288942391/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^8 + 197115615987521598951313897713744403856306493469909459950557045694069949591090594610289690676163710879577199839529821475937235556964101640673030290032497758420660036251105293122218425528685729069672384929105/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^7 - 61036759529710837918081918887359849366912253596164575453056853663233921356184155753630715315633551421596612923930067094330414160495587594908003757820109655924495480218614988956010291820192864095201235464317/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^6 - 12286172880258258113362566469471726306198319782623689811916892558626064971131474429557913813184515037632667784578396445885911845767404070587917923303359457334792579928553875027113202211583765741414701218498/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^5 + 2037603987309754797621237529286960454455865111150430524068459500950647707391659881957668599543492047326789709811496599741462500468172139493059166848905712362955848262827406786790866224787541805306699115396/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^4 + 987891846574363497491345158616859543335122391184290572085673382129500986446255528695062890933068091661351825062753294807434891049678234561252710596715115160785564735740925426296228464851233421147340311063/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y^3 - 18457761234797178500022138418018313966118725370457399423081479777775051062017556558167349021912417344225110352446131114478911264400424864463171848398288280080783638485442296686943805099412031373781814012/4390474021985975936969618739926034681240500048465486634726772917781798984011944773276651160493614802959634463650777345619502510221515617717981883419594780316974103477875722766315494292973979246179643*y^2 - 15648929559486987276760655849521888331583830723781785271251373229236266530660282382256806000915555935632231057220183365813505952869300151722939356893906312754511354661750083109417654904318959855607227907/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286*y - 634773021510482966515117082004293378188019130967206360374798550841032880576843629082324803101655710315662285298864913371286637163690821153369262380645095352122453766592985464950085532758632631311995405/8780948043971951873939237479852069362481000096930973269453545835563597968023889546553302320987229605919268927301554691239005020443031235435963766839189560633948206955751445532630988585947958492359286

-1834055068150859393294461315110230346202098899741992206790095087700402476711783785950113116322788180848690046347385830884630495296145553717538535893981463887372840977885780099000692692366020890011026629/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^39 - 81525397935327088552586105315190218857740170401553918827237283209124497701203382887546786905290039033226151119280464001197921840435995216868109288244697987631380956808251668621922250174989166709773318357/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^38 - 550255782418546196094063626591451395300737755905305471212812477476985352850383742152875042601961950930166531038358235363638087311627328028951510862371524556354340781253383797348268269667563615679286456909/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^37 + 1599958440429993309610110166817866871138424423064371684088272373955874846955374458695113725484609371624024138585826880593789703180865371283826004848840329589788993292145817275542559033721130827233804783197/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^36 + 12886695083371226384382213846270534815871932681159733938443981287389443175271427381861647831990716077727037988524881518887818494390999419484093700718949595494450085122760840642655467410831504015519763265539/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^35 - 20701287337134711569093805908460250614322748039520263705915237766185747184760248064747054722399881449487552519505399085491185135370250192474062620356560892366878996321606382930494371795240463971423942810899/3991340019987250851790562490841849710218636407695896940660702652528908167283586157524228327721468002690576785137070314199547736565014197925438075835995254833612821343523384333014085720885435678345130*y^34 + 51130230601805720404185577164529830237466617869885111568742234084555357052464459552933337210168750117112255669924518855791823779582951015648185114748011928180716920663239477625718152835630818680403390428093/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^33 - 1334172095280078889411273326761239982321571842722273647248509377909045772893112074887645554240139313067358676478367416531414791699662884259228992636055090999707488823921946426526727992157332622798527942057469/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^32 - 3135548305096940673846446350842697477684407729023312792989925225945299782904791096862759108712810511469436870042552664121544492460071542369400569422649987868330886287396438639880989865789116043847589549518379/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^31 + 6889651990589255834531156158383932372275231171268980967616482592722495280020545353221510770722683774321678719200450035592359411984966932267616486585825908751044750381304844823450105175980800822066193733300053/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^30 + 557902974185261068628080973686073572661199402128429893645086672063410883172034145298758286840825453715195061179640051002568394147642174489664301974748396970909143446397638058369395187720893482746880032869196/232054652324840165801776889002433122687130023703249822131436200728424893446720125437455135332643488528521906112620367104624868404942685925897562548604375281024001240902522344942679402377060213857275*y^29 + 216668423330967256539080047609712341077689782351814651932249887205905530534321928152003728260404161704563577666465771567074095216407446994097609360722943456967478006880840740467578697997215085424180683888364011/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^28 + 338123940820197442375012009190927716465215674504346852471035953337754883953898611503794334257585355019479936023959897862419492423106901423716279245055948919478365202851485012039791407432692457398726173165106661/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^27 - 172240911915765667208845271664372047513717781062748020813566696711873671699051717992062903532045508737608680021165658865672692382914427749909053524373416545327435204862848172528432732906405910593188099509695046/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^26 - 30027419926842272890952543112039164804637603185425143943739518788801978289562012417919324946876110094771552262092190005339548101222020513217499962210900432024756663926034575124688506838616533033026890709085703/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^25 - 3786912345723911014884420084696464345400994393550219787504683169754628407010560008886174905929931392953898156798995017487618042175861308728403886721100777136019890909252195670078326501379263654107394120012986567/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^24 - 1463721119984329655029368862550662822700011604716862484129195112393976619770934615933699641344452704360165146121312753240873243709073595022187701377491401744528868784810677132299900856074446561261681187094924493/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^23 + 1323461242872226232782447350038757151049183374109395059965675119820394411289469129038105371918404277377654898556590408260952939851409057049410682734660329192381716301961688069213711322052046279083797971807188113/1995670009993625425895281245420924855109318203847948470330351326264454083641793078762114163860734001345288392568535157099773868282507098962719037917997627416806410671761692166507042860442717839172565*y^22 + 8242525971149418201219980779058040456953092680187623370139840835759332200959261489343522195030091382510873102961886962751640358655684594324267157718808050220198968315571986252296877777710678156612043624397655731/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^21 - 10548769985966573270999719652881888771302151433766406884259928820958498807873189938411023184629121753892258817499558849428629825826098089067406089640826310318535043214862553988718111177736050932494516076458148933/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^20 - 3968231980472941407052376433313200179768935933065505840652916622195664210628349348617707826096004383838432506175606673093003842023488815779655038409080897766933114795979392515510256306985012685290359239697341331/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^19 + 18880397513632766652775594148009238022201035045183490152780483347784018335914885076184825663252607897163741486475263881303853499236048510317388428795091451095006830338321673333862397001411466436846669109091829447/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^18 + 212488418820351788745382843389361578048411360265642678092232998776401456309053806926696028908142719803279764869263029378848384402964929306579719807882997315447427346973120781153070480700299968382709570708992458/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^17 - 4338820975386218997738680538308707907840211789676370510907219391842755317733266038631049805333139906630773650524672588055689031719432088497020700109723491347447757295801765991232435160260720313204748164749621343/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^16 + 1558171466378200233479153728112045146548637548391548030889888693562491855414148244660191229299457788723425382160730380709144650343605116872995688976020477566969322308853260474342677949953958339710130253666100546/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^15 + 1431029108588547488359174123407812213704708749246049433857256387705430290160802162451438047246759100467367502488861063082494267686304745233601713552424785760812239248115019702969919820235516372534026089873770821/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^14 - 961187139842500520262864901695265308338410733875565055652838031520417712270286369152147032535177746054813399473461688705775718706691703209943702773746377021092796438864896816812945501355736409721871155322599702/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^13 + 268784447755996671768682572265564017395782310861120690559430372193728731623404100755218040162165062362630280939524356876466852734183384137754009909596536124755221563057718965476537573263267467521436598779069893/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^12 + 119111389973742575094034293811064496440963574457741399504689132405142799755805451233768346802669537844202990687211402651936136532888600841112598156248097580106827698198351577493671216506761061488281250794346193/3991340019987250851790562490841849710218636407695896940660702652528908167283586157524228327721468002690576785137070314199547736565014197925438075835995254833612821343523384333014085720885435678345130*y^11 - 17497016574566445284376439273968133852107216833093809159031920979265204935618048155688792749344929954020071537616735016074630139388579688076178131833369984824057002081624204220227332010324184905148819859286763/1995670009993625425895281245420924855109318203847948470330351326264454083641793078762114163860734001345288392568535157099773868282507098962719037917997627416806410671761692166507042860442717839172565*y^10 - 56329683365729260945305292971422365899133569453566506075117561982310967550067375815874737285378014813799557152591236140188468445439912075572619441109346835958060117335541159792930785730206634133985142879887147/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^9 + 19523994546028487542874545171216190200373872784529707340295164388148524451668069039553612693268198577056749844569380483931616099892081677158708172303249153402578276631151614093544521331214528246719517496003027/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^8 + 5142346721771697788350151572050921279783588716841176485608486732866104603232744790182531835050149297280356706672819595550300505457958882868590749559010158584095044865917771363561865616954102162949831361957409/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^7 - 1589308635901036357455382721705304704760188445402814204318558483000772791579077689299211862802393420311740308282139378709914541439617349806971216085537117055998661668463063004717322552175016126615747137309378/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^6 - 320536589234348953827293446023563452618042592387065794239897960116034135227069623007682043286903591245489200736148035845816788701413889463315126288648973421019392041753298142976172007660229630016652901271471/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^5 + 52391053350912190416557877826704330557326778410419940684344430697435816125963971210638374253938994282873893841021564114017051858068781230066314095922182357835319760960905833460508295469533675308732700067021/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^4 + 25510504615982348537179181458540460040166930892322823717908118598771272651326823654758625324639346157693598565994926592106172373651873578124143252123456760888490967139672358859535733801669912180244847277673/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y^3 - 458494336360824718020437970393191876253395018625150270184778330578100171845737978002405279400265754329305344018927637394006856166313997387364091816593526764160494153353226488843239683166394781423788937154/9978350049968127129476406227104624275546591019239742351651756631322270418208965393810570819303670006726441962842675785498869341412535494813595189589988137084032053358808460832535214302213589195862825*y^2 - 397477318979826797418045836178139031330176302244589747823681765469735036311411457149381632958113910540997231051373132218333493355062411744612033520113641957733300400464470246651210375949764574149902303947/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650*y - 16255796370114419972915865654047384389395468347011360693095199405916007853836234707569731957569514476751964425386003516096170784810559642797432627848446235880020680373547786592392465900955804931846022719/19956700099936254258952812454209248551093182038479484703303513262644540836417930787621141638607340013452883925685351570997738682825070989627190379179976274168064106717616921665070428604427178391725650

952149267591550827003435945475515805347326102977146858956133585018074772251640300899952863848980585993624893884464974000596388925763168786956667716366689092695253547133939543312887115573099351325550097691/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^39 + 42297660644224638633110209658863143021332620616634727048297157389799347047272241219211878583755366136515349615307344688731989953339543954075293680897302280991262139154248663096826124933030672220101433716303/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^38 + 285063020724608083366853314971191738740030707619779155970040804341200505575126682580681548916828666082452863878620615803463928732105243161032664432560267423394264069187985555347068175328847966812769320209311/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^37 - 834989345857529391904730895383249692657937558078022600797009501815089807581955499376108628492156282375182695863399976747651014722586581821191693559883775087676986132680109055014496118651221469054904937866313/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^36 - 6685963549163724911951607879514311960660808837756326936279732399179543361428016347600878374657533917094291006195573795250695500250176692481189696552451735262338129378449588325818510522601295315951295589877431/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^35 + 10785246674196874782744473617099608091838712733944700542850037657486006495714173096088990751412334222138536366600111058887888412767150228945394872697487956931345842385438962566690385878426838125386081896854441/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^34 - 27146239667786546043110960507909201682889804930391958186441325333361987965104054464838110831506679530226343072233885399516702278370390833346343319710018961883985416153594324927191407568877795440079609825784247/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^33 + 692538618218190697516054545316456229065671099391028314955092079889839768891505788212479338795933632953337523111431367285718166464926049210133751829226618598970689393327637265537769233066592301446685450273677501/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^32 + 147117001814328562140808277612946175219721937987180285113301765842827706845125277800429296666950455072641649384861002246248965832944069644646067271332020628136275089873050674249879757736854586947639502606348831/7164455335877115278964059671061120229842452351814135008485961261289390160274037152755989848260035064829585329321041213988188187134200485276161346125611482426335014311624474877760283868989357042629508350*y^31 - 3591456681739235936710530688515604535819984687279034002311827867566904993320115839769185960514492756082086776413357249402491363200588479625059620538296600663630409748027876705327596323168033187317232636230452037/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^30 - 288725466885528940129810382925485128639965864609391452251172473527447469417677145655647934818477949514828568565516006297978586916478001871345945701361782756003100946795860517349910553254713731958928166704135434/916383822030793814751216934670608401491476463604133547597041556676549904221097775352510329428609136199133007238737829696163605331118666721369474504438677984763780900324060740178640959987010784522378975*y^29 - 112079920300718967812215934554866747444677144472166109141562600014714313642916632621768498242492761539959632467114842341814923316701186635151280054259884729349060786595703533932746131874978951135849208442839228919/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^28 - 173703420039164974783115453959989355615273057814340830279404731012213896824275607295351658022017065728157763551572633681829086545296860598915952799609796336076586112664949953853636204751598213610676366504373399719/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^27 + 91274075933016212383942838097609399527391631567209045992556891039517499976649889627346998144253207056641094013079983627256333160007371574434103764848314874696929752752365959801658038585190085974723077078391226534/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^26 + 15589457387700012587946315110521988893177557962352502867536224279830582597277868587221368177235531658740880533691565170756239723437659930933856182847439955225130210912795484700898050688477693303259973147992213678/1576180173892965361372093127633446450565339517399109701866911477483665835260288173606317766617207714262508772450629067077401401169524106760755496147634526133793703148557384473107262451177658549378491837*y^25 + 1954875362446635699628246655446358445838857598815307635877134705646589893467093995360847756706104881737769191354438854407626640731684084479280027138676590489885650905465651899551978692492022056472086656263103512093/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^24 + 724813903214866713980896965517339972825567601718914194481354972625805591921612262643494848467612407681665489558187197942537262449246514269352974389126807996197110447184653181842737372343932322257692033541796355347/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^23 - 690550363138199771069647564715865841643520618408710633084166549840883496517084165543547025990904461262174044361303701594918088069584717437456889103231403673917915713074521094629405529327974102415096418639323230302/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^22 - 4205965356306159529612535816556404041932184075031326996681245899573392280036043215322202895193540050916150365483473156398430359278792396217175308005320856478601722056798639741847578386411188416615641145297634398599/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^21 + 5534111248980840477502742362188398955641474706015091983474012920798789818400979615884840553248976707524365035237345849658922059563552920774206890596967273413443275919893432403990165394464292111531641038151613164782/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^20 + 2021940456769127407502237133796812003791460477086884395497523065125103661031649171804855141733266867519338803459066060585457437892924630696913909491241020327625681548559320917560204045218270628031353608369326580199/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^19 - 9925472974459516415840265617320163811049789264329821585767382238811269286672046983354351988223159170695043362936777921640893427657739859770052024411138712872867945777632777070569449552584118480249195972902155519463/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^18 - 81757234337993879092198963790496169165513889006328431222502402953277866116716645919012209477912848340447994059325530167347701997012721211708433554951829606125522222555232983844539385103124080200619562935407591782/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^17 + 2280633110169208320138659540978400041855552391325691735782075450457736005429054086012008173747016360736896969797613746234319666686598793347174092406890520727714820401773934887169454884673310873590137633284400989772/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^16 - 824494198792408103825761798299352843124677167395816375639434046944491637753457830367119826702724610963846838059306897245812096872277260069488492948977874064559762924200216931333867008014145634837035084165444426084/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^15 - 747383007571254761968947065929828697843383356044307357618424095578516034508041111885147332043377016063706710852720597423187273914373986075162530505888628373697457353379092026221456340595884862260428426833125006309/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^14 + 504941196365230228317245075695138940917124683867012560471998294163058858662203279761977465385778381445079222217034014056341985605600889947524028879825785010332241109850335363244567571186138888162704364100778357483/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^13 - 145423396851726515017608786941095206753545261343041836027261811635269903051030889252893671186023599694552730751145405989704684628364202839090129300602689747721720099171479412523210368895309949441817398356800272997/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^12 - 62555508401491767977777523570725736102639463637338965517932351683277481932386583572063321221413127868783102022691741910517569892125577248333879641909645817150492241676168466121276847995652703827765594671260252547/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^11 + 9352444212534205930983767678169858420828626296342904267551045625529391565754598929156278017791992381130079717257744247570990428569218094395983029968173954079760828707518198117488004364469469085120067989093385977/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^10 + 29671545864321552395054564064488983699606168811736898222125418932830594741173906400378910021986585213932322674172489212494735112415011105738199955277155874971422874176781998684462583519998130982970878763387902163/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^9 - 10410448177616615861635165206122250455850318571405021595063358916036229931460929433940636721313223826909668973440936941971650568881973089650239226740133754039669133192177947077927937527366556960314918622966280433/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^8 - 2731371832238480748241243430000001553703492471366438926524056070312984548017303686157180237615175285405788743032755622450517098210020027578883496069415232895788500352143415717958231576484818515379744656823140936/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^7 + 850700576138328151591805542524541372213106343019786760542663194188346458044674338267407609177804421279233445011496929023955434804212123485476977032615498808692316023892055588022562232849830628754791527103457987/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^6 + 171843318386331161376390693586538288982506742203434814608317383434337468776104118148092330384282353260505184181048707091240628998729493827733389306394958196207313482508738453124488533456377832790191646123035659/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^5 - 28153236157670859595942231305423844820138269684622614255271041117556750422289312375695466439278802379430146727888321249259000285826418593747156406715906078087008252104867072462476380994714709887324894354087684/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^4 - 13743786417426843104633730243476971897207960472669693984442182622100753003258831715125629271563624462322220197767330989761071457339641534039078623377791067738995930678160009514362198189531144886977137033713317/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y^3 + 244400726830444446977087768214951530663233560457050480878000183004766637785283439881430687411539106411980045505776505063148150947664246810437494402851580516101180345244455414964648678900486698106318899607091/39404504347324134034302328190836161264133487934977742546672786937091645881507204340157944165430192856562719311265726676935035029238102669018887403690863153344842578713934611827681561279441463734462295925*y^2 + 215252901991435019866745790625471478213011502362108394831297908658418458447333486189834733344104166912398875310580468891207174942275234118539321473164164618862658745566210347713405896798203892239152386368213/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850*y + 8822236740588572856206729188624793710933592177966810373176687269686995342162113903887069865767398384682934613414382243149318035239168748936374522193746743847238499820851172389756327835221761767676585529401/78809008694648268068604656381672322528266975869955485093345573874183291763014408680315888330860385713125438622531453353870070058476205338037774807381726306689685157427869223655363122558882927468924591850

16679991069231164541652667833473826498364461928347533646809992643036313561126594378699493176380543121603975841917771825246719171707075180685290050474575064541348373696738645798672517503789321542107645/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^39 + 185405465898936206399775270013575443162006689977056410188192320299563448601924432132620749375347621825210486012415599505264813147064899387374753269653190653916477869364676569654737889619090557336449146/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^38 + 1252085366334000435646840313070222810328613604475967759522458225014127206425778395779693744199719578334005381539167819960392178536307180621512487677677958173904240707173484721295448130329218322331431344/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^37 - 3631178289769620745966416057164680020527894893521259793365850143736906815571478994456159560445421949284470599998402456039448992958634226776906316571823736805364096390982226712134298907365216649500052446/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^36 - 58621004270606043441756632201088938698689239143124992137612994798655382257372028391428971293248850861704174042161787261918004362198506912812093007894096557094677681029499601281828323608074427598082348725/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^35 + 470046282124026017110727090145232051383241492454706239417637147446500463082871417154433192138269433062888589680701271562025454394402258703134870195877778700224665924875316959236579009213980047709155806799/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^34 - 229800758806407489717290910040062582309510119105761664024001978478419080595017510987558886551660733956951917015981080499296050495962211920068229363162527262410652282935172095894536460018177057591718547907/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^33 + 6065058145781554400603171086026049065512597205903715036410156197424376626237416496200764436563807753115198199234168363225939895020174253458012031970077078708241320780083608536860339780009536280792161218183/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^32 + 14291445795409902116060659506451763441116721687907548285863886145145453279579285824221761076516185944640684380122352392678705344465118484504008605372595827334238444702394390835175698594202973029350038151013/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^31 - 31294343138518893206476647981066722844857238872718483147868062574724432179426464896186296368461275550038263632658912849278987907100812935392499669252119261203196919024411627215222649442795582473704974873738/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^30 - 5082261048309757207480408381737018235680142015213043235974443339437820629263076191843711217660664448198704710137787524222806842941547416719027108050972104041931277239092224308078137690378407701600629749105/18564372185987213264142151120194649814970401896259985770514896058273991475737610034996410826611479082281752489009629368369989472395414874071805003888350022481920099272201787595414352190164817108582*y^29 - 986367907134752382492300798905577301469926947489386481963872423478038013392867599948915505011781446114397166815749693116779527178092154824252598191628794638591145087398792142241062629094557393535536037670115/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^28 - 1542622808088787150901873249765599725388801593092628574616458714384107463186862512624635947160846993569295068515752659183799126725508768688969818118907463953901553943727081461049339667119301480195571998673495/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^27 + 779693223291014377234025970265826469975067114894480866352544936015323270812437885403217228968523011684466269111804211134973236800697823266265256084292173535224888719095677564451137258450986101785437888145879/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^26 + 6837857229535821519471247301381723449425978418614563211321344825945177058661542963848148678601201230192780571722338460501373302065990560187903156502098838343196977167000696316463943933044420221987451087075099/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^25 + 17255911340751896408867438041104626735742497834867392046827580174708983294318954821565571178127377415836447957638681248106545230959749975986054625667363949148119548604505668006981881041220532650224311362942637/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^24 + 6741127579971386970000133378267691383057794645502500905960489578805100376300448165304658781926831175639942039915760635825214346731419625678171777144924791752336679306936403688633002007708373555292496049061507/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^23 - 60168488040778873720569256644953277954963952334680502078553329765434874145602021188194611540719522111152730904715681734098974812526983770160580066689487548100016294296932656510193268288917662016329234487279597/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^22 - 18910745287776616355336990981223419778677980761224663262286944243993157857761051815709996203665737651482297357911798961221873238103003361652981500655045856923761538124148954975986338351297597320591405205706069/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^21 + 95802457487085649235865793739497203330165018689942965830778950982380457394515916491783613239091966542654407124858162344403429287639245628652435943036560660144248199502448773978047103215452055916180581245748843/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^20 + 36666996633066866084082333544184558972485229021770254344651760942853173056965739767161660030072099681831943571083687614979068285248904927237586265163781695490709566921825972134962756562540901979708396880407117/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^19 - 42879946728159558274433354995301277523370078472586897730699532894873497172406487666017339663449658977367071258885342711479763859165371529565943250118865835792017464609430943585787236864203410835300281162744529/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^18 - 2452801628297745357542651941618702119951956600072108377614757934608958378277540609229191779686255633723302886381064134904747704556798239942371943848072053240712824649714858737374495284242926205769369212846537/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^17 + 19767920523502502618868176239045438466468162413599507801110343717683419814950708970632444632993569009429672835069628322164336059046942073555687740107506273774678347193957912727397416350090359302630103721239514/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^16 - 6973926791726320022516572359107238025930510069816840126257164709728865333011378471462429222603907264746977533091952271645451083560786891348312700050186032711200250537297105505675051847616218553873238570121335/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^15 - 6623000691179246201749070249054214475333106386965338942464908097662453054089353901018381761838013208982779295475343330360846405689040179725527230732730759034730827477064669935343307870652392064698341435944445/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^14 + 8719972726151335452097951738562470667869580755896436807877716616525384430324995853340678219600719967592719018777941103463793708377639039224333053369382879700981468095472309800818382016884730692448704895912689/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^13 - 584198445642203716351462974336773185571626137103711226069746328269661338590105218907053701959183526145066083977221638171663954383664590963436783788359487657563300114992350951982284965176749906444887802200761/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^12 - 1361871445967255909636090302513518646880041018151035130949669728676838640160486855223682790502912237274196511526513024578490524829454706594117880007463101596628584393340643058263190215583072537464862615692041/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^11 + 390911364222094265073573446790463555304552496948310342007796533251841460753649828290382623627302361545752462719369057310945414773274562172858441250369804599836111725229528190639568805868627073556052127735286/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^10 + 259622605677410902647640522961327286781274974505482347758001877613014086191768508036895428830726985509335857477367528345545178824226894758581606982624012436291074397067347926965806015698299167658130673063537/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^9 - 175383339416926135989244700140539100452477048794864320340577858202458943233334358926284554545515412437647185088747533310706735317059377739488767505848749288601265603091451933306701911582472470905402306453657/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^8 - 48169601165162285095669948959483422044915950576512135662729883637342755618477176314739591755943088556782063935267217979131894590127542366762322410032990139512629726103826990913477722679139483720829190297299/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^7 + 7167321843854807684027017424015958936767710683075071362612619121277008246769851336625313168696853151304916796099514816814574806359065917160820359747220528847949200249240141621684999301362896662695442873594/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^6 + 3020056687875997985089831080358786985417907394444978206242965879993515411633498109659720219169856732070349367140844394513691605076074553987152152498058745180156649669733739000661929059005202222150234515515/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^5 - 469588560055036622094251857303968329074863359458707484768617772216801379421825534648232952809010576121459106776266019786121776921461362601638506305253721848847568285553561074444036567918508605586084101413/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^4 - 119698452084967325013276957991839230994317007860909518245951857576881979573353948192809299066737750375184389333936367010535128876733632661650941964942811772792449868799414855959069708663488163597715062537/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^3 + 3814574952430740713651109790522961989403131147201963149181551985857009550412908897640614595957110749340141840948787698109487721607815892049344554280225513843936952670521098000388403811052334065652946513/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^2 + 935986109137892164673197060702466208852881867417076768933865795923859948972534345069995450520862861933004772969564937722777471998449823403734022489414529422175677387172531736899020310160329074851979866/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y + 40711955843937166755199584566118415583446615921431255703252359476832080075933702667687379598616698992601047325597784177757811533716270579935649823025023455656701160946881549782626332264787011189783981/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513

60646005189532147097395597998212389351334400861590751229628260409073848965620116635809994778745350705260190066967359356734614852653275861336828114646442769546596561821579948922099434072064189162275073631/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^39 + 677678998548068795246984659619812176941173940822626932842315744369536121571090421164982176522203780283473799907790893906887584482447266297793716044866531543177682793226017428805973918390690417885518883617/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^38 + 4634678006823513896123161498420752955770828409732649995944688545120664974412804473216556206141100446102857976676545636684074029530434534543515594047034587054448006801910327457399243087404471206326223501239/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^37 - 25201453045514390711879990618824749800483979775414562182339596196449068952356801906891829812429936932776544914422462687225402558937951988821079350680081317482485411931557327839377161148660237737652661336059/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^36 - 428449887634150123686368591445023053138323017978242905706445027423952974942345850689735015050897812457795166823980931675914367295214826290658056832668206342425401599594431572527148878229728989852448732739771/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^35 + 165682550748922376703335290253932461180796718238209310801840060123556927059870524778242694719341313453759347310689258097211762552648095544680554472768127330936304760805965494918390061288175911980137228528070/1576180173892965361372093127633446450565339517399109701866911477483665835260288173606317766617207714262508772450629067077401401169524106760755496147634526133793703148557384473107262451177658549378491837*y^34 - 337835507829951164132821720311465388277926522856266848458284060649082081459386314495454400086890480073375113224097883062431539478599771853161098441973020622958293017007225900112760321248534985060745051234523/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^33 + 11046094023467962873001337429635251788283528206954410761254747380423437467598131247091156785675214377669481096075346330587066386348651489615351689763413270032898718350230712248430834429415455930154586672756999/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^32 + 54555803429569414803996452324680365423957017945091185686964217811384479887781720006598380868942930944802469243263937560600332637838991694514128411454230458884354402757983353836988190732106894250873555049249973/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^31 - 109675715962727141822937170020951999994580351461996535669076484453515110000682079513480887907486075374065351058657363854393562350091763051981988589832394322130543742268424336974329117757315173224905748674567316/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^30 - 18960359161736419458671787495578464965494001746768324741211262073777074945052326115190099700182709498726356567958709256793324043081247863712226835482222975148035232154713384093913410671330038661620343352606829/366553528812317525900486773868243360596590585441653419038816622670619961688439110141004131771443654479653202895495131878465442132447466688547789801775471193905512360129624296071456383994804313808951590*y^29 - 1849015465171775723052299542423156969879104302107808618593346110480729287007435802440940398963713989971079257769775646479814515373802865806951411900689839761892380207658227489070105569479724361174444315725959271/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^28 - 6116365957677561620943316669559192579885276954471847725309739309098445559381939991446339290877670903243794303664522930156571566738947639984136551200517056671209694768450060078540708823493374460417438595803683447/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^27 + 2310825112492574916891268956929743085842813537554460024968366733496957088266926683041121686247938020310543296097988169488045852027050072466561232255622992360081218024545443098421970588038443874373194983907471092/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^26 + 4956302984299688858149344281389321295397764358460772260687613221120029565684808545034857382241681056650272554950288539058713567223537812625453175379261719554116865742109837005056963667388307731078056046788992265/3152360347785930722744186255266892901130679034798219403733822954967331670520576347212635533234415428525017544901258134154802802339048213521510992295269052267587406297114768946214524902355317098756983674*y^25 + 32891234460055979894436886202309158448756990055239940941990766396055049932730565036924381153289557014090575768496984208966758539978286681550311168291694183973754564483914402145578772357802697624329483374141789487/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^24 + 34300554193756682788233515051002691437425323498923570117707858736246243198809545913443519497026931199291605705779555020285382117671561171291186420925679170250244120090538594962595057978282346884732038165209110781/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^23 - 41720108785277652742776566009563416768186325419204645657633386530745472956713185793895942470661116191879580947882206261681895308770566914501419828941359761837062439867850239848251280231475819118995739227155742435/3152360347785930722744186255266892901130679034798219403733822954967331670520576347212635533234415428525017544901258134154802802339048213521510992295269052267587406297114768946214524902355317098756983674*y^22 - 14261448475357065634957868907397999589765549057503120552007730222133551608361211369763772153742883869554260825996437958901212107395226765460950060111047906582527250655274727967823286396721984874560747008734078337/1432891067175423055792811934212224045968490470362827001697192252257878032054807430551197969652007012965917065864208242797637637426840097055232269225122296485267002862324894975552056773797871408525901670*y^21 + 157560232648637799975999575990947078665926050873024559722506802945762030481998578094216852110615091584454207636151162346791957323060560188027455749122726148213373834503104873093663566107229584101797907091354869956/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^20 + 152061799617321706135360708324318281298245512686741913502949219267710791621768344655240861202072589494528948428769259114454828248857194732088504691362003344276974857379799951835423086637333112337149492102678174649/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^19 - 275864701232692284343908018957681376192803561751861298490966234819197017851512243174020046823751817702979342142113112674805583172847512424530389948776334105506715530410394401895911201057517100742174505726958701499/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^18 - 11173973284261432081320914562299450577601107632729101911235104642461443804416560211352364209408354112828522340583745248792150085775543628634256369359487783498878899712499451181117917480152936012166042975393703576/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^17 + 63290722037763556819468738582307384130119962583566083210483653082704379659575303162802552471023007225085737796665060300549907259864262549978425543162160585733242482081689115133180473511085779771268112276849180731/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^16 - 3908978196507103433133567685810954195785573837729220500013920424709178875087707437298778285207323901126963284818322534741920018845249462588196145353028325255696082419565771877460575237494575128829133439435824919/1432891067175423055792811934212224045968490470362827001697192252257878032054807430551197969652007012965917065864208242797637637426840097055232269225122296485267002862324894975552056773797871408525901670*y^15 - 21973729621277056136922851167058861654048704024612463535773368913090343241228748700492997337045885479321627807241072148759684659290347854592118596030781583157702542489306461669795189297396055673117782886051624517/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^14 + 28340567778862065880218649294800744309329806074456900435786915883165517002982679403844212796326625705516149467348982600547392539667347475522945252393892169636814173452703641732987180788903906014706997913689016013/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^13 - 1435815663071225457476022233625782272613795148010556140585767418189508825447715966457497657453823525165986479462156642617128707913798438956260374436167152616671184880751441835234611969524300213300173601833004518/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^12 - 1747217565063114798220225579123794716951058991641978102863349983440106360504282909603370709502480406085682044303470696099954188393858062260222108901678147039235865742013385036256259461047723785397937978751244765/3152360347785930722744186255266892901130679034798219403733822954967331670520576347212635533234415428525017544901258134154802802339048213521510992295269052267587406297114768946214524902355317098756983674*y^11 + 214002773195476137753648520523624966838002606459560467840798920569900303593630825389786216169585744371687546261618257094904198821795882674001654765639276839841382567529435333743254920113869378009708189964903410/1576180173892965361372093127633446450565339517399109701866911477483665835260288173606317766617207714262508772450629067077401401169524106760755496147634526133793703148557384473107262451177658549378491837*y^10 + 793573444542951251921761508072743689132921891514033610428743222762036899805761452220474516723362510582099146683752924718529582797661931133338698574143572627584224177729382270395493414663023001947462499529071864/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^9 - 244899239342301206552264055574116735675258794461861177151012601327603946665772438972999837643807734532590014413376004284831670571226165315804504376247942799776577196300048144925645139100228119247244330739124719/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^8 - 64404238154974647898395786022745115162672514511493142516122918742400165994426774152159635631220461940173011726894749852215689937106031796867096945215027908745933774159377428481706135422466823001897646048369068/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^7 + 18888773322405450684163996707039802749075423124524514437245752173391327163834797586308183912682169006639415280234512936722818607108943138867361031667360365212771199541816032451321636125015463795860629111892266/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^6 + 3493620663262794295436541866815313042053522427166298066012859512777620380335823732221252815648264625930487883137962542854494453322459546780640821140712499801135771720959957182211141491152262552593203436764012/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y^5 - 1190188398092018897937545735257808853475903093410065345643704768792879952948453331047148596259030581854308525679555529822997165937905172510882785776681935803073084368892914247623683391515842452794900136352829/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^4 - 257546556708712196443868540887987274597588119508602883391247571899409334496444769270914809048031562207927050628702094265819145710607798304400657433055891752771663556779096774345761411912958168321412649562551/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370*y^3 + 1143079808027196484479210874999816507527205771165234630534551651744034398433023763112386343988618646819563433829276154776141900279910656984848234352645449463275441644069474215982402408906759689149816708131/1432891067175423055792811934212224045968490470362827001697192252257878032054807430551197969652007012965917065864208242797637637426840097055232269225122296485267002862324894975552056773797871408525901670*y^2 + 1817894424252780226339294859511678862371773803459125967071259052150423142590589972836432620832116238942909454713798022783425775382184036604349076056297537019890490257324313008423928856801779762876360855517/7880900869464826806860465638167232252826697586995548509334557387418329176301440868031588833086038571312543862253145335387007005847620533803777480738172630668968515742786922365536312255888292746892459185*y + 145675068005793263220756496503754936749263922305769784447785325272269981707407255304534853653255930162577405451142921867083608547175881344003686973903901438868715002194605862423783818356625046205955918803/15761801738929653613720931276334464505653395173991097018669114774836658352602881736063177666172077142625087724506290670774014011695241067607554961476345261337937031485573844731072624511776585493784918370

-225365044767977435125507775783143120425939523291886421319094020085037021431114212694402029644071119145188058125299099523418430566652071101481511569597921969561503932916320047236552501145716873072986/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^39 - 9984355023102416492146158666836911996554766560849441115718654213778891503902464573406991767755850539202312327689950270561607461800112991897863838547764626459592126726327997434130189591598720934823523/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^38 - 66869344839378687567090391013868007596233635108515984626316434730867180583402041505274829834769119377933033446557075468499521776222658847817848525840568625035880892396416883844294338874415696381288503/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^37 + 201696066233459523982212819969439496254489209219956601913694704877972301270045926249122992219868177674500317721297433811295606091066379936340267694167755060577736771697818999268079165537716312872830335/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^36 + 1576557246090394888954829179158838424251062058910214933063951051568252632450108595336580164656752021482964361183815199754772800197447539608769202506835973808147281746336148962975423542069622530808225900/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^35 - 12954629763468857839653225126128531348286868056720907877166020262132192542119526538292583894690550366611863096339312578651792403252641506005751608413283415093625875864797505703609758343713746558396318743/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^34 + 7192099930697239870942223796863127270480616919201919952517587827325837115694251717385863694461087157509854168591736350289021285543522221020729579940135166464537097467193407910831807015114707758314327407/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^33 - 164286537988865266176014275228807966453881738920710426429922046709371804135153219135149015973684357274070588835385623060610805115002452288379783519843504162587397552496312318960881676804458683547073794791/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^32 - 373205240043104485467773687660038483402426389321820906940192184496441987058245534872656851846264926915690487405833533622159461030206643669239992929232806578683567975714532597588315735516164441769275777271/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^31 + 861608245862287192291482816109575878914475603021536170647966040292488760471083925511152163085502245264211155117307847932794154841564950872747296721937525109650243948810143331782325430220938515407369967428/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^30 + 67144353467930985948690716403101081877869560478753797839072813083182880235400189423260042953868428853405942132494042238902727032650475111765449618243484011479713778875021672690582903972781986552044082671/9282186092993606632071075560097324907485200948129992885257448029136995737868805017498205413305739541140876244504814684184994736197707437035902501944175011240960049636100893797707176095082408554291*y^29 + 26171810869337893158191436769895734346414114911225372110202218111064042770969766909593966118969366480061640473832748093016336816020469350444255015530511991432449954084405064889580890473806088852060887126283/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^28 + 39519162556395064990286530606187064681440718420964158789939260360406378678990000393380745887843146139806845972364452518305579255974520098218250070309354604457425455999852688071278593133383499402991565869507/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^27 - 22832341876952284853121196950042333020275428261919828107679600225349387188286236125448463903051225158859060379903677495427267931840063767343018626277842308954338556270828575085938826511274178119725334037054/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^26 - 90891344837863089157431280639254845384935679558452074582084765272869501573587790124633834769485515854626206542972683290335214312586445554896389923753912301922249588162490553102453910150773414800729302837212/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^25 - 451277899452583129086190474156590302775995529017004724859920398990687990404422540518280508070377477212570452122314795362161135432683677726177079735275004626056622240941667811112501958834380256174973076134411/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^24 - 143471772294501475030489030407388706005286812531497267698207182182103873162227746797368734196496823817850439750644394177665446214195110729586032970398632823420033232693420549785984561196982958334544601292081/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^23 + 822179557710703122765135178952825811281033624855223152328011643575975738683777425496839949332530784817152332484450315286192195958613257272367393794667466560623083337237471585530305473535438730201513127246643/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^22 + 894683438835306335640475723589239128950325271727293286820660887834893838844200277638274934776425658051244412117940324703241524087790459350589758378669192648967105343884727343698321451182582257901446627927685/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^21 - 1341986698510409419214179073004470042535392652291138255568478652772070968524904318430548162401956986267698385253114316346681550712075709152492044315374860142727024770274511433128554785787428542187205507733597/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^20 - 398637267805646303726907251592589138477743862138648092724084289750051082540970817434580701663509788658112552285111068712379300951136643788797267517507685543573888562439482756006045128130436458471363777896880/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^19 + 2417332138148533585020396583616750284703793724141714591594480343079635669524132661062634857708284600206771425100262629737668611132436922729337412299563074443559741295214581471979984269878605606294914271416139/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^18 - 50920233295996637524788295120505892804375771175817182912475814364485734126750301214620623623570780090081073546707365416232958434536756753291204420770339141851022965075858715780702459220638552916545836460010/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^17 - 545937507621530672342540758084792031314694919675875557132153249661584275193444343482686291639258887473125661661869890779679291202490956781476581271340943115940672794283890526610775745538203107448329885061979/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^16 + 226882356568858619339564075148258155894494699244056479242798556040918718209712659083334604467602100757402672141145830485668222643318259451584835880080860517778956878628916636351687118105215197630773819082544/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^15 + 157929201644433725965208213572880874429602186768627184646509432085885093577671133519969143910514248618255241702656885186023974357236528189236975764300768862673653771123100007891300862155957739581196268137599/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^14 - 124800662479163911934795126014704117012842418799902156347937178952672544814117382394608193719618033915092352230044983974844674375150363903291685478603194654300529113504388516567386683085870820623020702181974/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^13 + 47979493084809981180315018487578858862217197455566628437132212704920892921875175897405034999320925330555382494892652793935962125507799153391704660887811300002241091547841188476691607500690190364283772224681/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^12 + 72560727826295271801046953904663693101162964303035909909318618389754237707496947258019044287289377704343562545368785203972105778169425234493575854665246351972142949874939600167651145193214291639245405205133/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^11 - 13309362742573304749927786106308654470524415309946074708936981419599147318602419890202058666753283114138235323254102644695509063807664443278371272027590381369451515507657963239730156887261296555127802501574/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^10 - 6545743893374662052070196807537313909541706625595203451621238990651995102079534778463484825496423558685145572890819143326477817968739123632841875860045171669429885037334327685842121876549183723525825729652/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^9 + 2893333979734340664381505174581444336910448070745017246397655299610504423306526974009628913459978869171624375743574679219617459027306645786286922237409947459124564797768393235831850941610312232043650859666/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^8 + 550463111385657289476766132489025153336038854038265773562229198948534442500689537671960609268790333621464400192669496583391685354010076346465023252065260782028313831071817680543807154597838992300014013943/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^7 - 237248494506111457384742204785185777978685062465283495251700592595559115949958032833114225827127443126183903437810196919717084982656871628349625062503821704957722356202041901887335397218933085110137206049/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^6 - 35219696398464171410381234476321805877899800337352910218844592521404672751120302701512114164279635952234263452099469824816176874763547590883379790938248775550100616469229404447928267329887536059590490279/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^5 + 8213950370819564442629659376277735529205188214369343895400244015536806587558974567142822597029450228382579584442558461492850576868944556648574681876095979858364582458179139631493287739750745966489376638/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^4 + 3077044915460406662074717352901457878084367551582687696364171686823796660570875278221879925806439369754627726116630619632087104687408704310543319824237118424519834888899213539322560566603306007272375883/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^3 - 90443241807768149892623075754335712003463824075017743646370411212674926372928601273285295571057910547800557363786480582314035174504288474964985948480748539254910574269683252986384323837918493003580148/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^2 - 50190573655433794705819048037036936813769185273001895417116039851668436353089337635726621168577951285058660740816204417908412186060215372365449025572088951221112273134219683578608421847506809941474365/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y - 1505823901733654211567725227818320155506641562441623769957932156961168539632199950076660335948833810360290776612142419200729124601175200519157240142577888393712109580963284911462550347610747172660385/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026

606808828099889044837992105263469585005048799484707553073841544890983880557892443236469898121922396370086590290254547767109381879126252107404291938146635519951809238774153248029358497433006853548929/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^39 + 13543580529417756821639240277855250318017718590953203662292601591004670578398771172875303700843701487293007727759413229883328095218535213869172477847294975303270472350590604464811345346535011394343369/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^38 + 92326718701168351243598427349810100484053599449199034399530739124048280632182520633907149270384536404430603963323186273629736201365950119460882461981766760292263032635412870773146329985213611621794947/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^37 - 127696292632457590917008816814097050474569863492635407615554075931782224013235317714256764244389132065403867973903432560107078080740482409355584342053051458866704771238066106689082247115479996186089055/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^36 - 4283258273547616306563243933544617180756284145969795844134308885747479500799125862141398240570644045286982233171471885217460008324259522864653606864293983663608638485859924428651020620865250852539098499/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^35 + 16710996996479435040982678082093619528213633071308270148539981878265574094148340777163364244853088561506304126375970467084429625231702983978949823331776504415189884756984462976105466622357651591517590203/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^34 - 7084305654566517182999488903367062221195944108455032547761308635753867440246809112868107153637714699865283398531438244909027483255016034212419517749965363655314883010786012587306611506935568014796208867/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^33 + 220713773177498097021470529089410491131765243483000521878523970081056785157236061285214609757821414325745644584130439283254679321948651097323964658487065135354195886753154705343641577035056595073150464473/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^32 + 269689621348669477296233803929049832539113173280407279692926723281719930988474405236206256399764030362006586377824741131781814942223779521230549151750312471318322685014274917304198810994565268661618746240/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^31 - 1109493286685618625701215041563355268240222626470949769503117584118645352369753766623398501811467806565706449769116359952127083498566743601887563657234223745734283448636362285265454597285276946611818713285/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^30 - 188780485746063428895258687164535233341262705449417231921210686700905727246091757047276815952344687748190380314650620270823789561800338857111423785443215101567986041502454861245814658264323341832182806415/18564372185987213264142151120194649814970401896259985770514896058273991475737610034996410826611479082281752489009629368369989472395414874071805003888350022481920099272201787595414352190164817108582*y^29 - 36693258165782784976522619418590740307423137934769999581061324730730257369273485697660347369632138988388115765154482022495226759416453755777695828249692947018707337834263693090140131513727702063423107891905/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^28 - 29888950817249069789967584744179792521995631616861285650976579008164125258354017555701842758131498762813000096506905754007513100087764410359052067372417015358332811720978039653817487027175141354891948030527/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^27 + 24787956478547981389286263147339542630729810798712906318654756003372779295940577942627255406882128785003912820074194871827123636735227036747878298417017239058683461758758566812734980792753447450411602128277/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^26 + 249636369887376140153842766006484553173728869490984557607371525089476971572037202782934566133217660588368665413323000366719306369772191067638087148456640380109016978051333531611152405716688834048867781568197/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^25 + 650751305187902307507027771839788534474443205687689922716600215890038039182794281292275058970721661887450678235574111123715310744619402608711666286123962314017122838912510626699265615935603793834925054770109/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^24 + 157341661288756889693565182515507893860885164893690124560140649057063474364847913553543602075814662650608290638987468753810064552727932833978042884593971818555403044382357391885872752686704818901766361942782/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^23 - 2126227608218499198111499825436697331867797349469756455689557021631518988946033985002927736525272008287340039709554491517870471252438097530184088882223437306641018205824523616902425254658987417670173403993091/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^22 - 767845593547234559673303222924086838449561311528193580543820210706118941596872133948250039264485154910194075061292275330299557725422638129020238190041252388075130697771797912346721941315018155230855531089347/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^21 + 1631159913489479554792025598411931830237653912164923679216256839366475095741039188263164565273962127325678122157084398230075807131961174501969549531021014200410847203543235029852104669930815363298089787690577/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^20 + 1518069106676462433651529673848319192124315100240603084493371828021894335942402598685276663365934984420228128586768336453676368861493862753452854598848921705143584086018700916663299872957856278253934419341261/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^19 - 1438076673918995169456640661246217734721077785203232449526668777503695977993813490077242065488096891234412152060356100988049624691931812872730163085203658015154800168335328390021791399079881062734231369495590/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^18 - 116387254485690072665510272358153507598407613044378528053857392684677320202694055574483413396793699047195660199332879076996790525141513368308501500143673963677839870107796644248830936903050551503782795124488/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^17 + 664450121680662301406733107657494729715747713163993757837762747100195568887317306876072063441758945422026896519680207493360392677249847136342401966765995793914425542825772935810898516170607636525404307519014/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^16 - 433033988676317743892777579567497811314904396398013643539792127909066632563442564723619425041076998883728979872491792761165260787032993733265127442640534214859561234472447771883832029436562822415150692242733/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^15 - 117820362359610900242626914408614731641919568352841673638430629742507321915433599520537365905618069770640957394646017912992278624252773472296766585190450122285892242511723308108129253381354891896956382321751/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^14 + 292409614246998292919156988203515616617142159434077758899368368277987974887791137494073010765234800069987009053137411181511247675230288958207892179829349104366963503985863562901547078580844047019762545208831/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^13 - 28450466105293418216960513589390506801651836058522375990856614695509565965773038081615124519932222165144907227938944701565182919339198951366597506658934949854123960644157380487732038524364226339050371869637/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^12 - 46338188511268775180648097049134835798893800160425276825994415395708408950940864512995423224005601761463662135890747696235915908707799777161054770132824718783371655019836069715665778101248349800130163842363/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^11 + 11095031249866648045170761593283099767547187831525308972556524369954608202438657211173175540819510507136128497841791840705468851870366315952417218094542794546843239367829479514165169494663561519069682811357/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^10 + 8725333593735476051200004087788035582970160946833075416465231529207786249422224036716459676307001642168547769608436352046885388372651090022806081576436553857871483107900661298790992372220818487697480353389/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^9 - 2543323077577104050986311704166881857657021675143117834253670969615725408053647703767017116061722480746933035146713092478370027024448844914473175944748271519502166443537231595747739837756096378577809618207/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^8 - 770451226250535321975787960027706600875904843950128903510896226120099803659358014851962453309405444739295458311648424245104875256698996610255151256243970581491850431430036803480684332008303047904007824525/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^7 + 199768895538935273889865208498201013705908210988846218844880182014802735735888609041044374458628619220301610601454454640193654559857609830374050835182040254438410128773128507809888188155307791243223949882/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^6 + 44210766172355278256539341041277340695431384351754889672739838662806195900910430515185226611878679896644289018470835447461359277695554460560105584274200779263274077307662019889570034768965218567102099509/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^5 - 12436473619304281194191249762826076518603279459036660939438680504638659254681190305972085962856864396770989999526689056003200518901189927127214189426848669038227957121332176211380516019189534722618045525/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^4 - 1622670768573437129184095228915072537245065165681201571847401675208000852737236629669996396375079981136256799981706099626073158673547624088851147887188437436084575990355624520562037857063197041925183930/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^3 + 103341896042609536319443506812660680933568070317417950976612602001821864270440590581330197608380960423866608539237624067823381844256182416871947618414068020583525184404343763975141867281247198022689253/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^2 + 47150660387069929155141566605747444132535633656725443770589308904316179256260439927815530620538914511690705559140079875062387591134151178453614107422374746877970355349683459649834038369421641756767949/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y + 1504336900234790973451843890010578994439739852515282596553117982404613157286664300189472504459179912761887408626529640793470607822789193897029507228895393308980331620960840769573736183910031272477846/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513


# A Gluing Matrix
{{2,0,4,-6,-4,0,-2,-2},{0,1,4,-6,-4,0,-2,-2},{2,2,11,-18,-12,0,-6,-6},{0,0,-3,6,4,0,2,2},{0,0,-2,4,4,1,2,2},{0,0,0,0,1,1,0,0},{0,0,-1,2,2,0,1,0},{0,0,-1,2,2,0,0,2}}

# B Gluing Matrix
{{1,0,2,0,0,0,0,0},{0,1,2,0,0,0,0,0},{0,0,6,0,0,0,0,0},{0,0,0,1,0,0,0,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,1}}

# nu Gluing Vector
{0, -1, -4, 4, 4, 1, 1, 2}

# f Combinatorial flattening
{3, 5, 2, 6, -5, 6, 1, -2}

# f' Combinatorial flattening
{0, 0, 0, -4, 0, 0, 0, 6}

# 1 Loop Invariant
17955743028271994320954216391630590897664121772930229564197628333090574371114051667917946419386546224433649235505212945817143856414309796283922621437915816901909224061465957832407675937744940453144717243/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^39 + 199557150427702522778845086478418303063896054810637991983829520381290890271723040419514386742294797933318453760485905486092621240473400276322076613959424818243532303254711023506971071043595325030867089087/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^38 + 2694448264790227663155685861533501943906623755750644523869204851308233248192019646817126253736679965038429653601154428482476093562451877156471005400420356632825786719267917019014438489708208778727818580525/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^37 - 3912880719582504479508586792604085140223166956755106247357684047522808344618384132694329209503028701676216857847364144211754037745664694258954538240681663002162647123512553471769963345192667109754822271078/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^36 - 63089535245378681040530129999553585081621122308728248056646076637627711727862917375809741155047657447403737501234447140463463486854666747202806868398759278205641723077966152017121141510757191121735972550791/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^35 + 506390287843205792673488534600491835729435291827891141968924723206916618388839580771362932202184011940080079825664800145792235217858088166962889091865926161196254350255764243447942270160233965234561805839389/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^34 - 124614834215627998701203667935952520210612612575878279953577950282322797242366220852699635735467455171816923993350849556224998172533424432978633786266472959753183781471828763924257762484177106597277171852732/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^33 + 3265290464785561502589273756321083254839925560157227237944908033471241526027131831733377025988897926877246442494874600935865113920232530795345443744894016070253876695990004125011649339007948958551967434247913/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^32 + 7681622449915300452782693592738566578721501512955953294753415691114135545115613846080835097886597110169020817662474881280105403000642854295877582592416614563911535525564668490980175498003818781636466811920428/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^31 - 67413572432784024567529603156886806502042110685987834813975849297146608848604314993344955155866932750142770213901116767717611040549776590868551809991288906746037683397073133009708510218526883250830654912944021/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^30 - 2732621396229207622405851887305249940492785443831851573204045169685265534937844421950415419461566316593219848403102558873470381960224762731634706762303461552559939491053882951242749508922987287401069272472800/9282186092993606632071075560097324907485200948129992885257448029136995737868805017498205413305739541140876244504814684184994736197707437035902501944175011240960049636100893797707176095082408554291*y^29 - 530582469540873488692861580178967300029386616562273546637283352541941007963685736046706980849478450319787325290967302278193674295138368091980345579554557464383576267603901507680180888140051409760562812153860509/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^28 - 828816839795314875985212726640658864285702376179137889976732764340763040455408137350923449556150098265089598485203279230303141348947314489301977390002351603277201976471340079622294882824135041143598045290257203/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^27 + 1682004168832810968279428774958388738243184307307273880473892128736992807240849333193680955992357227217402711915253585434830432947738688106881720300706667932484849574756477675397862784907238855555404235707385639/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^26 + 3676013769848426105304843011214100837780010775242009202726352948437967399062643831160500888597598266821325553129090529369515159323199126943539467957044806791175044450658574800759602669916596198151658507602666245/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^25 + 18554087050258459097636468186963105152558249858012353929915145269861035885704301929438157537989822573596108026889817682649995144535953502764203490464463216855779887012324669052466426355412550286676460300875362607/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^24 + 3605064647192018351359408367345817477958466730210638541254685831226029480694588269064321818101947748376170688460387049318751086173951376730090007221397397693786504712477527730461475728661873796277018741621148193/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^23 - 64757819079279612007967285503950554275988506386882937549984706370105091041634233369789621998405791335748883733944536232627572440694144835202735761805591373309159388083052588379741400350721932804044256212453169727/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^22 - 40484087521905709127497363260226482796581372468525127124572905263944002913131679852186620466229704082373170808390026438596511674270847729039921007801001219082419283502951110534630362596018722237685397769940092279/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^21 + 51577119269486022883045595777186005437100290770967013176166350136182768865782140324891260362789310839779038109644737404739471020322128996978412327790599979491487066453742897916712223279844602909424740653576424291/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^20 + 39047486901955271694207078737634927593169422579278482028411500020871070532625628084115806529147363465643731108815661570871513463393367985787553229887746655147187465285231866521951273505165514444930173884499708989/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^19 - 92292870067937570078075006756377706396879683401712811076149069838830233267002772370221376146678826872422437082980480185681755537360560539410186200009303884534167136025205540637624808765867378650557148647977179415/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^18 - 2251112400888185874197772689645802787707105859871895322886576733597426176644535542833992852688552817469289025658590288525936576897522111547539049920449096429615864767739714477102787976191150064102535416526491285/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^17 + 42437403849728203708090061003524609133230262223196847301427410661437722628348663304589968712518928235038589303368580710068515995570613916005615799942628136893587443680140645376569229688139448530756073216480549561/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^16 - 15173479103814679090946913445126761427981575009343967734383400903951791706505350839134012842413631883691202764122780785538863146949348523540935327783814518102426540174774914950665694347224806492104493530036378359/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^15 - 7021309278732991136828933381124304521362049899778771812479476549221112315279879758980748166135011969945290001682905309696893316091111780363164445165781635323901441684498656423558576643620123215818206805719480895/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^14 + 9392530483946973938876288365571914641771202418935699841836703030770494560508077057910703067449162014235833561560104370907438369371441455102021635163773424801205239981868468124721411548778334614167199569590785083/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^13 - 1299228610497351328442130757938333510051295589066507454156286787525497854773004033205935446687106283866374729784174298002061325708322401233659616134068036695325823813691795257603406278906829491844207369159560895/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^12 - 1457394072241699197411004670851338331407862506500914831689546276415845993354681754166382469756118586084905039908070106016109181501050477154504929100347149161407669307473013516532861611850280151757223189780655017/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^11 + 850502150218447175756901916633034584306665828795181550803273812316446884739272463216989257293527818510957824828712646022450381505382858818524074507865664591830257210897751751694565514657889947168120276053044015/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^10 + 276015676254881156158832625338141191879659276501009704111060241722886969757527711271653379143980094768054253159983578837131205058710626694484332595115757181303450261439075785618146191033910123130382999026911007/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^9 - 94957863319509370839932148230765160979879467435146561185591479253500189193806910840029546458402473535961494545455200039162922757133913797763437426414954883017252245621972588876471903000462128595897143036714110/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^8 - 25242568109545898931005427284769516507778252815071757128481110791667775866418362323218872426178092094875792680240136435981889056488984890302373346091239831169270298086814697914542423394537829840146193746023456/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^7 + 15438182616075789637036176924007779215066303302906783329790568076047373346184983229790596933933530590711195320621686671839842334335265907876801541495076518978554678135013086508726478776100924204900797001114813/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^6 + 3143759181838004472753765825822368706931075409556073053303064384855318395136542515426411053442818033106531262333273319070573025018381597445155038760911061352773517384895247599023987799091477149626161169668171/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^5 - 506419091309765327232551250551154857034477419703498274437783301533739455163372290886465736382426088754981305995471104346973761925209998917562176649650117982946588248506533038120514928864245920837561623760847/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^4 - 62285741008858302939067457931805065081516224637680616181976079566839407714277759781561943781954732501842590538780026370699719662835616481857267168156859090367603167881382465892218509060027730994125204182830/399134001998725085179056249084184971021863640769589694066070265252890816728358615752422832772146800269057678513707031419954773656501419792543807583599525483361282134352338433301408572088543567834513*y^3 + 4357842888788978107920381211379573783692237278445775803312603783481466004157281701400249901632723064575819314891816000722336558770785822668498968442898415551618827719299440027980158594444191750263063818523/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y^2 + 1932646411062378112692402878160231061105256160433570786227982933004216245840513308235102431487549379804329483510058347889928800967652898038836747548063447853683457565588340082943165111110248506457174487203/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026*y + 79602929528681045564848528779795151617056732429956317346693273479396598304201082427793114700719170232345006924512392718085195276668726609307444392729039898350782774587862402261693679495192289774683916187/798268003997450170358112498168369942043727281539179388132140530505781633456717231504845665544293600538115357027414062839909547313002839585087615167199050966722564268704676866602817144177087135669026

# 2 Loop Invariant
-893241159035681513095271476342215737876471300473272492780869778559639695586548800503776168098828017160383444106537864482956807290169955468440741255547932387049706472867706095049838043631984433982536368781985233865762263422107109148823713374254776309853818793400428719036386087379644513212505633677908288899325228662143904396409570655923302471538303572089/362773226137098623098983563131533530977319228642868191816503507228574154801256733695432358900467318137300344507277974515246638550286254054821414866045809199571882023871005585899871119339265359378279770111494627666465146058216092055063651323236784813491889981793515639213475594761273957268881690087114980485927130690584377848411824899714533255468392532256*y^39 - 29782285299732916713238967269342779130196211727337702942370043148061728627254992559441767227541630908555438255684660756716498582385953325089950908456542696587545712659861045523438032236904951783507155157700730099046593210745932790522226506622201962991355336555662846757107539894601590712993671089646261032215095477299373833575267804795139325111344536380105/544159839205647934648475344697300296465978842964302287724755260842861232201885100543148538350700977205950516760916961772869957825429381082232122299068713799357823035806508378849806679008898039067419655167241941499697719087324138082595476984855177220237834972690273458820213392141910935903322535130672470728890696035876566772617737349571799883202588798384*y^38 - 9139430142545302638749920479836762320760783643842482350953260329663488527385844910868115219738029376021831179693507709503678395838951880333240553597893884329739957871459392281323461967583477172044365619276636968422018993157804259724756867368629275815485678937625426452044160937101380044201888806817957543301738410153910800028810933061113967113796293889213/24734538145711269756748879304422740748453583771104649442034330038311874190994777297415842652304589872997750761859861898766816264792244594646914649957668809061719228900295835402263939954949910866700893416692815522713532685787460821936158044766144419101719771485921520855464245097359587995605569778666930487676849819812571216937169879525990903781935854472*y^37 + 1167798156516371103460445473373509298239552466575173505381251087082025056079635950652169490091322981526161923253096220276547722848211773410239331900422363729470911488013704246199910414561741082349033022351318364568707359294894751533830299132628914007277832018464497851191244180401636904140925973559217812670337617204967639071856958714218365984850698153686833/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^36 + 6277000950499658615621811431203622512318999022846012106993021378808202666045569680400352904297875885714621277902190044183264156206692360751115836440080932481459596644599394142612968199852042632491766386778429400188548179785135414452893731536148180137719930521875817637395969045261323994007602884970118529963102085706398824818039566178229010331262068514826637/362773226137098623098983563131533530977319228642868191816503507228574154801256733695432358900467318137300344507277974515246638550286254054821414866045809199571882023871005585899871119339265359378279770111494627666465146058216092055063651323236784813491889981793515639213475594761273957268881690087114980485927130690584377848411824899714533255468392532256*y^35 - 12594899914281293863807044065080078033822570755695983419832539337855054492708056985984228927288518054053748796822852221029830929093633848128898959912413068169218140943211567976951248489283214022533039970670959982528993790156047544451675453618045992734952022204189440275811493167945654471039907106090852154500429902762560526542353227345832699993853643127106827/181386613068549311549491781565766765488659614321434095908251753614287077400628366847716179450233659068650172253638987257623319275143127027410707433022904599785941011935502792949935559669632679689139885055747313833232573029108046027531825661618392406745944990896757819606737797380636978634440845043557490242963565345292188924205912449857266627734196266128*y^34 + 6198494691492617626357413480585998382542538345123376578862400898037380804798683291690427640971167172722470503503973536979357967369657543692077710551213669066752322775847476469925469729772926748581536182027606025052814197622076847111058500837952804817600921115443060295766691830814631594236898274676415677077155887253434116109722588752414339885183877225657777/181386613068549311549491781565766765488659614321434095908251753614287077400628366847716179450233659068650172253638987257623319275143127027410707433022904599785941011935502792949935559669632679689139885055747313833232573029108046027531825661618392406745944990896757819606737797380636978634440845043557490242963565345292188924205912449857266627734196266128*y^33 - 60916117857624166154661421268880130517194001702851717543717305868335831188745553831262026519862716708363126045187991721098466563220069907147242351285191388908344346322848065975362982571296208719515406530796452809194472453038441760652812340891219406527048115125761049582846675994310473000568201686464907124404600801339601441748023850502408313110389677970936595/68019979900705991831059418087162537058247355370537785965594407605357654025235637567893567293837622150743814595114620221608744728178672635279015287383589224919727879475813547356225834876112254883427456895905242687462214885915517260324434623106897152529729371586284182352526674017738866987915316891334058841111337004484570846577217168696474985400323599798*y^32 - 2293024104806480271178344823172475226531254716577533379921925836581798154656424684241888357288273577842413772266487090476442461324085816299133176302467478722446888593229735957653428465529276458411567627407788862445018760469939231530192400461353630181703874288300569868259663514550008673079886122458937072952842715190289940575878505530364621452430120654910290155/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^31 + 209578201767661838400092330687654169779745136828520769606269552520767614841025337545878126249147342359150587159144658517421770920275575629635294585831327738427545408685859502361815142516775445160441458654417155259007289821917897363912766080920386907302093285437119367915050141167229416278926041764292815308070008097723652746663564139571325474042044676140188931/22673326633568663943686472695720845686082451790179261988531469201785884675078545855964522431279207383581271531704873407202914909392890878426338429127863074973242626491937849118741944958704084961142485631968414229154071628638505753441478207702299050843243123862094727450842224672579622329305105630444686280370445668161523615525739056232158328466774533266*y^30 + 271881337718149374237203616886474546688509844028461748479407544192832505435997429321749631955509848619674018106794193606147751181251378793298948233440257136831859569971530052820749598756865448024657941836005878667569518808310050864891505078137743208885211694005971108650245886326791230519406917211520143462913959774490469113981691002501737206572507549986220891/8436586654351130769743803793756593743658586712624841670151244354152887320959458923149589741871332979937217314122743593377828803495029164065614299210367655803997256369093153160462119054401519985541390002592898317824770838563164931513108170307832204964927673995198038121243618482820324587648411397374766988044816992804287856939809881388710075708567268192*y^29 + 13198432440608686634783271288865843297312610439258044954511080286525817930888829795226120645816223901044271994274507959983507558364143881862827260435529967099466011944565129353511247942353176146836720841925477942756366518894660915209500111885985209951600194113868281874378953620323371588076370037485057081708108413166151293599076280971468811250715762307431875123/90693306534274655774745890782883382744329807160717047954125876807143538700314183423858089725116829534325086126819493628811659637571563513705353716511452299892970505967751396474967779834816339844569942527873656916616286514554023013765912830809196203372972495448378909803368898690318489317220422521778745121481782672646094462102956224928633313867098133064*y^28 + 82481268400602111037991728172587379828284640094018594039759045122833502083263258934485862729991534468836889202294145489098334034995890146034306006266853736246200942699275869862085513504286167474520215372493139764573016757059711471521331784996873403931079126352936365599634232890125273829524816183815517978367660732444538854640971605301545403723335533594395672749/362773226137098623098983563131533530977319228642868191816503507228574154801256733695432358900467318137300344507277974515246638550286254054821414866045809199571882023871005585899871119339265359378279770111494627666465146058216092055063651323236784813491889981793515639213475594761273957268881690087114980485927130690584377848411824899714533255468392532256*y^27 - 2613119621224284853945654323317707533498498806167894036432690943383442434372145615362393450913781638983136513895606669799494620044084054244602924206945105007876386250984918059043512422104806410732427227976282508116128327750168494090819844562221450748785354133137649305932240816849997554958539401269413399942037028140590078422779873879102512859156505161107915290/11336663316784331971843236347860422843041225895089630994265734600892942337539272927982261215639603691790635765852436703601457454696445439213169214563931537486621313245968924559370972479352042480571242815984207114577035814319252876720739103851149525421621561931047363725421112336289811164652552815222343140185222834080761807762869528116079164233387266633*y^26 - 365684756531892654240014561943523822587262188337960457939192637907865711511339752246444446437267061812513457083863939906229735205236949371592041600401826796314563011484053544893684719762925032678243098592117753494643494752629751077667560659448306651587049842570455991471461584293652537217316819890581648410751689505101671149777297641358929714562644543294633123159/362773226137098623098983563131533530977319228642868191816503507228574154801256733695432358900467318137300344507277974515246638550286254054821414866045809199571882023871005585899871119339265359378279770111494627666465146058216092055063651323236784813491889981793515639213475594761273957268881690087114980485927130690584377848411824899714533255468392532256*y^25 - 461544808217733897781067782106143798561090564657097683358805833020018349659058831197484707868895842934408490471457463790616276736154140907718388066940827092801827705902853296911652887011668684219014461310089937245363562462438673733985104004770056307490299525724914973292855047890231704022900429580599085254762488931578126081885939797688269002347116326616186960197/181386613068549311549491781565766765488659614321434095908251753614287077400628366847716179450233659068650172253638987257623319275143127027410707433022904599785941011935502792949935559669632679689139885055747313833232573029108046027531825661618392406745944990896757819606737797380636978634440845043557490242963565345292188924205912449857266627734196266128*y^24 - 359100341185667835842782063402257150035743123522398366328085224144112576391402262328904203409545799206916521334988423403018843526303833076033220470493806990580237167576903966091938269712959121615319249600285084523789888123890407466694924392959525570840121091600936535019876294915764781870663001786762110983566161172721323915655383602859859578421686965670083338425/362773226137098623098983563131533530977319228642868191816503507228574154801256733695432358900467318137300344507277974515246638550286254054821414866045809199571882023871005585899871119339265359378279770111494627666465146058216092055063651323236784813491889981793515639213475594761273957268881690087114980485927130690584377848411824899714533255468392532256*y^23 + 9662157496208649442666444101136823511223619220809997829793745973289185213317586326841097178534675397566754428709895629701320077085301387952399013207357183814728467091929362028382189060198283786209992973541359142362142818432905941100736120672999071090733998374458376793467449229855128440110161534130571263606668177356969395087088498137128616091851094750032517810573/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^22 + 2013983049688693052119804970458787699705538568296188420372377237593039532077995447650647793432471959143980895442903042248199710733622057328253932926688039240228076089941079372646560169683605830026801114239565623358211416722805059960185181489476329789962067780848880463657412858639495718473764352364242033046391163707860549217017991531566203538106775271762896332373/362773226137098623098983563131533530977319228642868191816503507228574154801256733695432358900467318137300344507277974515246638550286254054821414866045809199571882023871005585899871119339265359378279770111494627666465146058216092055063651323236784813491889981793515639213475594761273957268881690087114980485927130690584377848411824899714533255468392532256*y^21 - 7694437757337415100261826088288023056670886713520816458599173069407045775408723683697368472180138396391975366961939643452598978990644286704717689288891712804396766783499070784520207320146701467222380983652239303265481425934697670308425920571918380708236259878278402781517161970333540015027169251295667997007752805660401877567657557237013494786793766982278134367125/544159839205647934648475344697300296465978842964302287724755260842861232201885100543148538350700977205950516760916961772869957825429381082232122299068713799357823035806508378849806679008898039067419655167241941499697719087324138082595476984855177220237834972690273458820213392141910935903322535130672470728890696035876566772617737349571799883202588798384*y^20 - 5824220616695991874104200243830791781858590092828063813819173956337192233448489637302849978048714203192749595906351308413816909449665484313500540634200062369938679857916180145435191840240873622195904663322062712971852138447596661383976436004861328053616336283205921259784961547990702770453630364296793421146327234109619014777609898827889238900953816401542529612231/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^19 + 13767448678115486059565512822657389545280792714874122676243902969916342860676037779855022754019853097495805810489925917333796424443771043294090916146508198736545833326834327164810620859242506546340646093073403362710403618611369548172948003481135793889314467653623140159759161771805760881244468226483034022068044246415775546475331076774790289993408764391076876803945/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^18 + 6922103261402239863692395769606627822562220574296997964102101985466878128458276872041080979199205232538138795310197694288720523218004493894589633523613642900978401116384656386936972528982419546425305415836977296071663928156593227757449917941483663175049991917896005538725518238262726910340931595154795097830124093837135235691090271187298815077556493284311071069/22673326633568663943686472695720845686082451790179261988531469201785884675078545855964522431279207383581271531704873407202914909392890878426338429127863074973242626491937849118741944958704084961142485631968414229154071628638505753441478207702299050843243123862094727450842224672579622329305105630444686280370445668161523615525739056232158328466774533266*y^17 - 1054904385967048630064777166576471064761566547222687609767550448164001510796737838751508973630954110045529356761946394875591423666251625005317252168914207716679680006239436040810673130418962489994070683522614090020943977245854027909537393519435899696299468697028259814013439637641431324578249174956595873611037125484529994853200771929161794449378954844881403801137/181386613068549311549491781565766765488659614321434095908251753614287077400628366847716179450233659068650172253638987257623319275143127027410707433022904599785941011935502792949935559669632679689139885055747313833232573029108046027531825661618392406745944990896757819606737797380636978634440845043557490242963565345292188924205912449857266627734196266128*y^16 + 2265677293068893397494508125930496559463988809216511538199735422140944230994479550236056425175890114540623423818320143665994345252554329691489304611750532859385219008821591949195887657228722321547303977458382255447295323416790287020480496095659914148882825599422975849479201441735748021272177626185336493842997970213465367308791969468029164457648742412048720861017/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^15 + 8648470796340534076100524887463626689617557494097453134248139534283825856011681639984161549742258208581400522974030469485255152932707096151244237346408335928567907816904728989334844976745865497769312184626966740109053030505307087614793735036603963989471287689212861315180809069440543167704802050665142943695157351943031774673005610856402550892168288754652907569/8994377507531370820635956110699178453983121371310781615285210923022499705816282653605760964474396317453727549767222508642478641742634398053423509075515930567897901418289394691732341801799967587891233969706478371895830067559076662522239289005870697855170825994880553038350634580858031998402025374060701995518854479931844078886243592554905783193431219808*y^14 - 1401360405432258047903632516306740122099612939597240699537974355253418280660996916202231632725664530774498980371731302290765671973052649552832396718053262237414015021567964559050044396027612828038269155162417145657804594360330635595413527799224929799404687430713181264387265621414040333387783514100021857842515727298857048199264006551165173108152350303503455879785/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^13 + 97073932969670663486655704049473575302862055219877282338749938381660145592828317082039081409184100191071184720627828137674402918992592265366063227399629036255238052098078643331929651731815709688136170311618299861935983077417474393633998455826967369594840139940680708441855025604120299815610640995537763999352411006945552699607153143856913777575210138539429729263/544159839205647934648475344697300296465978842964302287724755260842861232201885100543148538350700977205950516760916961772869957825429381082232122299068713799357823035806508378849806679008898039067419655167241941499697719087324138082595476984855177220237834972690273458820213392141910935903322535130672470728890696035876566772617737349571799883202588798384*y^12 + 434619843663487731140277652854493488345885942978788827723796888285062486376880521812033071461198366506723058723566077113906004357375618939181706777011611238747807644779951774342887784519577064292811959882290624229595022483672831506200849596523780469461704566629030061597018015939672163961486348451214394157739227544343075398130702538329187164961557953694394620981/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^11 - 63480604693030417593452884988262861371856490637245241499376508698773748966304367249280848397869332272084919508097961700627967451757153374926416243150541367949318424732318295136502630252519634417159384347258791044573617064217844847352052550844450767801832328897216015763595127825107730306798408681637460717679674725610048629857462808262391689609856935399045937091/544159839205647934648475344697300296465978842964302287724755260842861232201885100543148538350700977205950516760916961772869957825429381082232122299068713799357823035806508378849806679008898039067419655167241941499697719087324138082595476984855177220237834972690273458820213392141910935903322535130672470728890696035876566772617737349571799883202588798384*y^10 - 41133423109288885764598437787452086334032775765881908513167235100611861692359191174679452128288798211291510902917503331266050193417693121645277695905330203205138941957638750233940207028871014072042410989773602228761325056836088448322066545266408959512288151224784621684224117242651641736498958248954731195795821640078038863310641603802584926200734224384250133161/544159839205647934648475344697300296465978842964302287724755260842861232201885100543148538350700977205950516760916961772869957825429381082232122299068713799357823035806508378849806679008898039067419655167241941499697719087324138082595476984855177220237834972690273458820213392141910935903322535130672470728890696035876566772617737349571799883202588798384*y^9 + 3543873528525331286713130721696479121493743774891725119462798923233606344609003439556848652631804345649105610697228868918744990535785294380641274003822419998379423642428738224653086467027585016113604409716667154822418268939996938056069466316126265985243037535499006577242213145293452614254619216062994145887387590079728779549947327549005266961084340494942540179/136039959801411983662118836174325074116494710741075571931188815210715308050471275135787134587675244301487629190229240443217489456357345270558030574767178449839455758951627094712451669752224509766854913791810485374924429771831034520648869246213794305059458743172568364705053348035477733975830633782668117682222674008969141693154434337392949970800647199596*y^8 + 3758705496473104437480684431762632092037174228202269991743859719902181565711527785963933759791953696906094442695847983175774100221303846024682705920033903997411291727286633667140754066730001779299402710237315639113682291304186366716984484095608023792952804735110067965153122021326846339175004383249111409308200316534345711235251455317239969016600204622357637253/544159839205647934648475344697300296465978842964302287724755260842861232201885100543148538350700977205950516760916961772869957825429381082232122299068713799357823035806508378849806679008898039067419655167241941499697719087324138082595476984855177220237834972690273458820213392141910935903322535130672470728890696035876566772617737349571799883202588798384*y^7 - 104778356769955404934286724427976354315838149654405847051045456270381223919099933129818222418813641604185523311014756750630132170491093781215573742005793952617043971495786776738195333093687649529846094016045706482272155221727595870718287214388253393274279777125134668226995548603784913509788130391176195446769401002765742684407338059184421876012489800174556551/49469076291422539513497758608845481496907167542209298884068660076623748381989554594831685304609179745995501523719723797533632529584489189293829299915337618123438457800591670804527879909899821733401786833385631045427065371574921643872316089532288838203439542971843041710928490194719175991211139557333860975353699639625142433874339759051981807563871708944*y^6 - 14647334415386371317277101045063630454107250495530983140037297098992407190052815500031173035683020710113896461530939568772059135604613561722552666483550415278651748013027263057705770869683455377145610013397923899295597617439916186051605688305315953408319113976107053718156571101286150212227054301577341145645300917402536317188207914477641174353402739485549624/34009989950352995915529709043581268529123677685268892982797203802678827012617818783946783646918811075371907297557310110804372364089336317639507643691794612459863939737906773678112917438056127441713728447952621343731107442957758630162217311553448576264864685793142091176263337008869433493957658445667029420555668502242285423288608584348237492700161799899*y^5 + 6888862003798523353010396394096643187481788120680301296512341172202149171984713962655286581997593633285955835039569230920722589616977098461934365747029065216147264993765989264195656292198744187973416011992603600443194072025302148315713762969714926584497703389006618904443649164026837793772139769731265623409259214691486469327381847574685056627166967038866915/98938152582845079026995517217690962993814335084418597768137320153247496763979109189663370609218359491991003047439447595067265059168978378587658599830675236246876915601183341609055759819799643466803573666771262090854130743149843287744632179064577676406879085943686083421856980389438351982422279114667721950707399279250284867748679518103963615127743417888*y^4 + 18626895748037427734741263313626081142237640328547968223246565579058520892526604204393978953583859736257115126380150615541553376331712020166865686425050926794107586625611157363787718328291769771584662879751014894477274020239119800549857590150735852432025477967395267112928985841537046350529502991112273971134717685132407395906771477633969104519960410644676121/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^3 - 657132309946826973549458239015350606209768383860644613818218889775909982649374609313943167809202146605157058779451432491781716852389824860567291798429223799107322417110602594050299673621790543251376129519815883840653333748440920844408865049494444842904955971883529762825044954746435160973401501305170266220494626990349559683081552045989530866242265066888671/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768*y^2 - 48258745107201492600228365155810805646604645694169670975745349087035293219136728641887687409835527527987233774010260980174972611510984774208037381258174347521552550537034088179642118663834372017006594707646601447577883070229285972129214773074289179699105983357531092989615634941374256345950824833922468851868591750532224940136964099868694633234547936129453/181386613068549311549491781565766765488659614321434095908251753614287077400628366847716179450233659068650172253638987257623319275143127027410707433022904599785941011935502792949935559669632679689139885055747313833232573029108046027531825661618392406745944990896757819606737797380636978634440845043557490242963565345292188924205912449857266627734196266128*y - 6265818594527770672278360657373947463825987109586733757472663154596095519283638467757060416592631520502906844343955564657726252007934779175549711445391595878768534260506642700818741320295920776454855101376508658751318013200424247688238654298752508531329651475631015138635120692213729613568764587592255874409489566813444830891710695709789836786070584263471/1088319678411295869296950689394600592931957685928604575449510521685722464403770201086297076701401954411901033521833923545739915650858762164464244598137427598715646071613016757699613358017796078134839310334483882999395438174648276165190953969710354440475669945380546917640426784283821871806645070261344941457781392071753133545235474699143599766405177596768

# 3 Loop Invariant
-209675844088342581507869480894427842700679317854890181580677488720739312143440082616888900278341138319236245872178265722104808758954402372591665405094032474593957254039620981554624188714634487093543239239472749300676949699443854829073216266547787560155568039207063230577677893032321642382031200605406961370311200399987681543320177134476720628004619724014783711012595389165217237143711349634801488571314816456440851783729016984662787/122278044277823013310195927361738820511526138245123099403529729831101580263017661334033439404145127892869864341370137863502930185898257950784005857039838613651068792053088230544310120182686073549147507931263574696729680205199087261598290247739524177567407336514521615802249513567784393640864104434113875143678954913575131757953888995762605626555295286948615936351489758286086150458202360501030156892742520923119217607034505312415552*y^39 - 9320621298104118684127400028971540192496686443663399346371711915667968381709899280727101559165210570959584614153109035999927158351453621020813373287385702191213237036203412546825514323284251132920200134335414934113104708030222347063326520030672278043056996660897955630390076731217673996016382103896793634436552987388960275627682742283155946430935697739929058839519282265989067803401175376392842408927541091418951504249605670777096843/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^38 - 62915150068886138538870720364738059429563463669818982327196605287643279350748850507868299264750070503813235051521300454208338959080114275548608977990080832263654634032621786600066506492411489161049717339364525649778245723404478791784340512504212297138084700804932617506128829017881812202404196914301290867759668827811604870298436457057161609796079250807762291899278105059978779738752386620590271176240735733737221798228624666760345565/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^37 + 182854566426197384896281527152586529566264705618408941785296432569718473785655650653305993195773045491152552394273835325707522610759672250547615714135814725988399587066339213139701850697813262971779127646910513378968095432998575798040470179060991751068185360630055594590013456306729718626526096809977536739592410729871713833684250996019153741404309556493632799539142091209426881087211927317088294653613706886040503763538449402445590299/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^36 + 736651221929747321313954017869754715848648898713271934390716822099319195023749547947053836047120186445842450296684834847533416681051343420578134109147134880385586053263610788259866161170351938813042509125700614968342116981036619785466769845260423653003525080617344895854488917151435296052541778064232415307032769687016482367357298463885912584150673508793310370027505297131034909599482952647872613853978091328600546754368495807185681071/61139022138911506655097963680869410255763069122561549701764864915550790131508830667016719702072563946434932170685068931751465092949128975392002928519919306825534396026544115272155060091343036774573753965631787348364840102599543630799145123869762088783703668257260807901124756783892196820432052217056937571839477456787565878976944497881302813277647643474307968175744879143043075229101180250515078446371260461559608803517252656207776*y^35 - 11830718836615230835564743502968756669852222081969532443599721574594061725931968656956224676481952964098147461373324745091205908682819371124657172999482605241428428862142884241027745916312959269400909824551284967604137698874599910133262418360315132755929045708382289484711700613332021864623455228264412838486503891164580979714037441126659872423102721364351053048551046565831678151907849591076858130471166061533381805218880652104327440701/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^34 + 5838069545636363064388881264361603338876279188707330531849875166281591082327554214526086342477177114002987129616981850553547133205179750516256554732891736029900774598712434390818502191056890267658122221844201550958084514459749905995629248623575675619234614215878584071312278220175694251530539759647846442696699358358465964730010522287964618952596636041426291741438974699437106286665355776997660792126208245954704971319855831352670709263/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^33 - 152530585184098083824299059102387698937208408681304448377632282069232901028921961865838316190968635968052243215787473159787448216103974007754675371594808347922643811061613226864737822319248306037445978362024566167112734208354307385624574985670083633277695226293040665620308162827599860857217646374372065662691571648473359937439429347705181705392417609086878689956220223240680512921006939376962830938038241502827186964462535436757849284015/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^32 - 358590698975437639030431381907960065917055903156216210475996631787217965946583648318241700238336519180871121516689269059270573967447243674244049240012603556259486704433554672667833596523561820230783857318216801760777105054783479248016790265586075058158218723694144116137873750922116198857801359812876988238096642889218656347182799410797072605531386073755331087927540711298149571359171737803656853124909664299695778696392956529511379698337/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^31 + 787445769330771314238712543600718952514419929752941923876627744779659559760508076813308440285045360567834625833621818796102801392541013319551685105900974799496399380288141310566939529765258500430731153191509360984684999198403907335769607722939310845805687385663457002759667544920899430280028104390867778544948353032224235213779461271332856075720081677080415440899418488506658076478840507757449809171246568108466777392236706975068501250215/122278044277823013310195927361738820511526138245123099403529729831101580263017661334033439404145127892869864341370137863502930185898257950784005857039838613651068792053088230544310120182686073549147507931263574696729680205199087261598290247739524177567407336514521615802249513567784393640864104434113875143678954913575131757953888995762605626555295286948615936351489758286086150458202360501030156892742520923119217607034505312415552*y^30 + 1993517575276764861784837088223077670278824072553215767332773896756497111155249959527604321710407035259588327204569168277380501981560978512975483856552379531728759165178444635599139460007233092922936436846607444930257694351612412383643379430115135685350334677346117841065772696172179404543611607847746664042242244540202783325429250224739738728928641808578104854981430465406999628192691795641316523983340174791960607024039150410182252869/88864857760045794556828435582659026534539344654885973403728001330742427516727951550896394915803145270981006062042251354289920193240013045627911233313836201781299994224628074523481191993231158102578130763999690913320988521220266905231315587020003036022825099211134895205123192999843309332023331710838572052092263745330764358978117002734451763484952970166145302581024533638144004693461017805981218672051250670871524423716937000302*y^29 + 24775828044295770696064135217630664340699733387591429673142304211789225321103477115880888877065741061051917901339964393019474333647803469350234659256418287818081899032528886843959749928273568375096469760000702621109438123853132797486762374449709807086315715615144110593400111746842220212094233284715005193840639307065425911337906344604629132746289410921753572460120998224939742586952239814056891805881083091547653727949329352516181092319025/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^28 + 38680409210954922990594731769672675594292095678001928103152484598285810017721390432993585577148824007461922812055798363886005621430363812144282722661016816501991365847732727948127385855236480318471323312132176377438312028998787657379086582434973084826433518981858765234855063065148552180182563035733534058336794126245576010168545300912298124050712890523799610018658736582914236363958983225315280426503861902168093409831744377779292825200591/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^27 - 4916209050771894144254436199278940186086919911350788206084038518775773289170706838864653966833737494469250172178422407482630579601307693896762007792520542235590661613712070340221142180242647082347063723007022876551772422031682480072695710209708293651991157964497226628434167777637680355542013667509161486828714834952459340870262093924453238038852217786583153816932775817886400318432121380717705957390376501814870786671346721767444830596389/30569511069455753327548981840434705127881534561280774850882432457775395065754415333508359851036281973217466085342534465875732546474564487696001464259959653412767198013272057636077530045671518387286876982815893674182420051299771815399572561934881044391851834128630403950562378391946098410216026108528468785919738728393782939488472248940651406638823821737153984087872439571521537614550590125257539223185630230779804401758626328103888*y^26 - 85817086899137829221303533946593872483053983658253068009117169353560878754838993791354888266764306360342175638957758399850659917361882324571431422537682597549723538965290473433912505818656024089449156904582895301501796159848722576047158550059452728098085383401872430790113496636898774523395213451719861707452641485880976564245798444766251907126850927925541794145941461185573070859113380838365978527787099313825871549595370453462173818990843/122278044277823013310195927361738820511526138245123099403529729831101580263017661334033439404145127892869864341370137863502930185898257950784005857039838613651068792053088230544310120182686073549147507931263574696729680205199087261598290247739524177567407336514521615802249513567784393640864104434113875143678954913575131757953888995762605626555295286948615936351489758286086150458202360501030156892742520923119217607034505312415552*y^25 - 433083135837136769276037261360140802054160015973270081850154563988207371550389489559045649654200371050731518130570221061455535701753955865720678710629161107654931625395102230166390790844830933701044208227886502544532103887216574446293971738596357870946958600095538597984912654044488413771004358303931980980093172413288156476306282531913238590126742594105289244052960941841054378307637480910895238544539855138993174259589936805098178811211585/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^24 - 412345658994560376941259925356498592553693431220725923964661926032376124451873013864680541778628123772475099050778399419562788344596813427095942784366486087691743008657607988616729807058049288351479792749068941576436764241547362583418534905710625486759503152676183971566025389489557622649541283476990262638445499921094872759637584236695878497858506446002865206694910675247239244241345143756237313348822893303308938360316961257070254729901/600874910456132743539046326101910665904305347641882552351497443887477052889521677317117638349607508073070586444079301540554939488443528013680618462112229059710411754560630125524865455443174808595319449293678499738229386757735072538566536843928865737431977083609442829495083604755697266048472257661493243949282333727641925100510511035688479737372458412523911235142455814673642016993623393125455316426253174069381904702872261977472*y^23 + 17187453890254601097672071801503520007337905296595234080064936328775594939929687332209925805593728511848775698619042757536341489769934674981586345813539364358254164985506766102070816098208855578712804493317202812125164817718295959159582991616945757279847506488349702988644856903546018213271160582071619054369130583583049502104778747803310004391501619984456822778516339225038791679926428008939345382704346215102431143670034245499592562636353/2779046460859613938868089258221336829807412232843706804625675677979581369614037757591669077366934724837951462303866769625066595134051317063272860387269059401160654364842914330552502731424683489753352452983263061289310913754524710490870232903171004035622894011693673086414761671995099855474184191684406253265430793490343903589861113540059218785347620157923089462533858142865594328595508193205230838471420930070891309250784211645808*y^22 + 25492468615736604979336930486743395574936995724189874291358128535445933783208297765957778348646104771068561613076658687781713662061084376571303030664022248892759724820801959693430683029836487378140351215697070216033779872189158070269683499880231414246505523481528097443921648897551684521108855933606786710667262244249611647657758573324950016375678615533563050514019620269476852561404015083011317871943626081787140444722247846398894040526457/6609624015017460178929509587121017324947358824060708075866471882762247581784738450488294021845682588803776450884872316946104334372878808150486803083234519656814529300166931380773520009874922894548513942230463497120523254335085797924231905283217523111751747919703871124445919652312669926533194834276425683442105671004061176105615621392573277111097042537763023586567013961410062186929857324380008480688784914763200951731594881752192*y^21 - 602549390941566030411680713899145034220470454285652020737549584902676996497384854114634326309506853566553349814310416304792317429020216865935080037269949250567963078406215432720500114661228386910032566874974045326669229106915928975472114407402499827176871009780034621297328643114600625629365693963373650031521147706358436579590291965916258444332001477490300618505656392878954218603605164828193464049313769750999053398228802711259022324040033/61139022138911506655097963680869410255763069122561549701764864915550790131508830667016719702072563946434932170685068931751465092949128975392002928519919306825534396026544115272155060091343036774573753965631787348364840102599543630799145123869762088783703668257260807901124756783892196820432052217056937571839477456787565878976944497881302813277647643474307968175744879143043075229101180250515078446371260461559608803517252656207776*y^20 - 227026765157618460633937603721005728382716625105423185922909352795089215802401630430833543204420093718458851464941212874985621296582606454425037014215094043501665342337275208514089046811126694915684621607673698813613759251450782240904040230345532632580975071829414820628286219488319543552039597981829546232305276574434721764327551198968845713933512079487782694861334234047754736359791292988863521956362789692212347862335131353944155864572323/61139022138911506655097963680869410255763069122561549701764864915550790131508830667016719702072563946434932170685068931751465092949128975392002928519919306825534396026544115272155060091343036774573753965631787348364840102599543630799145123869762088783703668257260807901124756783892196820432052217056937571839477456787565878976944497881302813277647643474307968175744879143043075229101180250515078446371260461559608803517252656207776*y^19 + 2156508041448199949095450481269568999775275806868145910466003179526968380995447953535623972589256896321145356841367140698856558153758089492608730244110794152375427510694702895536252938809515750447358988481702533007176908997236923472737357190967921581435307781156923459858014230040167690086900646842125091286099435194371447297955820861090900685184114488724696247752070216953891303962310755479289351153433256568538682183973676880484395610535783/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^18 + 558019083799994500994926867357267087794292055207069410215155186601079587530141679030906428929958897419431758063029366220208529192336977362620819779246204680909552524347744868980939157417802017428834426533856532756932787266077586435356679482128805051957071023030677657496249152879537110744244113992918588746225496841879120385391524058852797510105465380437544727016536878379466666837248560754145458741726618338720418496040663589813136156059/2779046460859613938868089258221336829807412232843706804625675677979581369614037757591669077366934724837951462303866769625066595134051317063272860387269059401160654364842914330552502731424683489753352452983263061289310913754524710490870232903171004035622894011693673086414761671995099855474184191684406253265430793490343903589861113540059218785347620157923089462533858142865594328595508193205230838471420930070891309250784211645808*y^17 - 123878194288109903915881152367922172263077863218201540939047268062351871139717920803579914722328647423602334569012476219378872415785617165776139916108049100365958160318771736400385152064405013536489290900900127319526228906170097529850869713547742449617073088189009782246896978217903903228361090358350546243575466980061929150290799758072816152992790414369583974765067946694321230685196101316784049648401595334352769666924429026388930934386087/30569511069455753327548981840434705127881534561280774850882432457775395065754415333508359851036281973217466085342534465875732546474564487696001464259959653412767198013272057636077530045671518387286876982815893674182420051299771815399572561934881044391851834128630403950562378391946098410216026108528468785919738728393782939488472248940651406638823821737153984087872439571521537614550590125257539223185630230779804401758626328103888*y^16 + 177964451888950924984306765430491249065263602356613211449968002801364265133259051168390975267460881838888390321445806504015178447822660177520732291780379296715233652495888264755682215882713111576340553464117363949115507898899648220150308342535803852332968225966148134758955446851972607563470497283932533615301636456309694684166063153123870853644230777802293824552051653067474718842828749948088506772325866907250402731478081465416363724141339/122278044277823013310195927361738820511526138245123099403529729831101580263017661334033439404145127892869864341370137863502930185898257950784005857039838613651068792053088230544310120182686073549147507931263574696729680205199087261598290247739524177567407336514521615802249513567784393640864104434113875143678954913575131757953888995762605626555295286948615936351489758286086150458202360501030156892742520923119217607034505312415552*y^15 + 163405634223855052059055291721111925943296632385762034517421005991432228937717773801455033446560452588155727890340066766085949337058528972039655139716790459070953104542529057583110652886079550640048565469423969137801707175811563297908551836881497762498255516902406159979789402778026330167510840896371825735732697459337416516411442820374605936307666919265207866171598692903554554155459266983372876739395837397175642671972953367264028713007949/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^14 - 54895968522297034121148892253308768497015432896686650849253652933477629699059756293812932483656282749842484809968731659899508108940172124738279933300680646211949201589125338132553095199934083015040899085206029942171683212724088200020110255408683755459820689592919016266155016640428250667084208429640171743428145875238460921289825991385838597873153424253780043776712883735661648341612569665285117047708317768864364399109096500916907811873245/61139022138911506655097963680869410255763069122561549701764864915550790131508830667016719702072563946434932170685068931751465092949128975392002928519919306825534396026544115272155060091343036774573753965631787348364840102599543630799145123869762088783703668257260807901124756783892196820432052217056937571839477456787565878976944497881302813277647643474307968175744879143043075229101180250515078446371260461559608803517252656207776*y^13 + 30677926126817016562184646544379851729744209226689075714603196934437200792822005953673898675535904695911419805688918169926186472081804371239928719914258500271788510596738030755192937235744805232946959763182452463101942664838640899702605166075931054479619799230271292932273086482053977703354554084773714836896470929728675416843253918495887628296848791658454444651807751227204742762455281810340316651987483784233214483979470504200981316919557/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^12 + 68009795111756078549756115188923147630591383100004964059898460337846435035896139071254286939782753639905294187906229876159818714154196822534193194755638636558192811314914168395888812121981179756771359432409130910653985086101012895065400021565979930164594914575341432574458440253240827393475142563182246536576054004583573958139272211277174173743500480233765417049619345684031215424110839511030685079934188742846646308221591998225395926843641/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y^11 - 4991944357943418253837124252474417505338176862469156708812357016229774871161085614628919397365250903388407991026452599885193956394310858401748776838121694863172107331156537451494869419860600768311606248739885338832377803264047017263152202406469114056170881782361411275371020141204475416878902150442286845781449345960081682754819631088861643172897091370344287350225426821247578889930130978379921104499205531598510173125299206166934781329525/61139022138911506655097963680869410255763069122561549701764864915550790131508830667016719702072563946434932170685068931751465092949128975392002928519919306825534396026544115272155060091343036774573753965631787348364840102599543630799145123869762088783703668257260807901124756783892196820432052217056937571839477456787565878976944497881302813277647643474307968175744879143043075229101180250515078446371260461559608803517252656207776*y^10 - 803663988184164118708141038648106519776875423205191134596269601402837071276749812886402678281546150096303095349279347663323737635619350514703041899601491736100278320580221693047655304660343095163548256637847794452806974145876544936864365681858979808390136595003013587362929621868184866089894165568211946710864218587378557290554745640930038135546248347286491291341788081887549608017400484692882728379950318021390268002572647180732382146863/15284755534727876663774490920217352563940767280640387425441216228887697532877207666754179925518140986608733042671267232937866273237282243848000732129979826706383599006636028818038765022835759193643438491407946837091210025649885907699786280967440522195925917064315201975281189195973049205108013054264234392959869364196891469744236124470325703319411910868576992043936219785760768807275295062628769611592815115389902200879313164051944*y^9 + 202538551720744619323817319451785341021947788837682784755935647558656906882173048934966854933990619608633001547354787495919624192891869777122977627853824689834264178034126735777912497835692898760066284660743116139691432556369874914269204606913383854108349499414752451192001213515863851646191111076295683704604056187873022709926121222589120912902661447627683475499233636710930410726796948226568511493323452112204480946774640658809170820453/11116185843438455755472357032885347319229648931374827218502702711918325478456151030366676309467738899351805849215467078500266380536205268253091441549076237604642617459371657322210010925698733959013409811933052245157243655018098841963480931612684016142491576046774692345659046687980399421896736766737625013061723173961375614359444454160236875141390480631692357850135432571462377314382032772820923353885683720283565237003136846583232*y^8 + 53289783425714189451259690281446442286812359475167448605292241362215152488680758627915862185834256879120026234336093477505259238421019735683548037517739430838600359168604274612366577239644371205143165607794472442600672977518775179684869128350797300310326495560711522839267953832778487479853966856148691046344060095299583526010503796122841737150924927343229959615271987797790526842831595296229126214102067607823834131678061297396125506347/11116185843438455755472357032885347319229648931374827218502702711918325478456151030366676309467738899351805849215467078500266380536205268253091441549076237604642617459371657322210010925698733959013409811933052245157243655018098841963480931612684016142491576046774692345659046687980399421896736766737625013061723173961375614359444454160236875141390480631692357850135432571462377314382032772820923353885683720283565237003136846583232*y^7 - 45308565682453427677585788598586725205892015411161451637226629131520043329042270799730587575805945329578783387342168132911060078005877547837923846535633722239155505856427828535512365211599453405794808997738142446098719821923381514714985181976820414444760400973045999840218086329120491861456299157845601422267975691931702290704827137428584952198606307277529249568215192922424142053817044985080623214031399478699159540909822525447995662461/30569511069455753327548981840434705127881534561280774850882432457775395065754415333508359851036281973217466085342534465875732546474564487696001464259959653412767198013272057636077530045671518387286876982815893674182420051299771815399572561934881044391851834128630403950562378391946098410216026108528468785919738728393782939488472248940651406638823821737153984087872439571521537614550590125257539223185630230779804401758626328103888*y^6 - 36506845876327559920820132240151005339265838258870673265329542473811145081816209959754762440452876778822358088228961706705206098300611581268832412784791562731125133861119101216211604335584210135057094243584770213838855796886421923409837621557295295457100211571107246577456085209133441471137506580439205923753673494365361216558117358532818186978221891520757856720265662845234242839615956375978786998679516149783612081426748027730786136023/122278044277823013310195927361738820511526138245123099403529729831101580263017661334033439404145127892869864341370137863502930185898257950784005857039838613651068792053088230544310120182686073549147507931263574696729680205199087261598290247739524177567407336514521615802249513567784393640864104434113875143678954913575131757953888995762605626555295286948615936351489758286086150458202360501030156892742520923119217607034505312415552*y^5 + 5972196210906046990310813893325517606585260544142054911450062493222187125592370596535401420923226725201608392049879557836942461239286004372294449347497813649106607920001956861198208756988234318183250618216449473222622447247088928643278949107302798949078422216992681785506038111252530513830561889806174748346624707684586297714346331431790394354712157421830385215811949129351020826388918638379430005873924541873664807396196963259698591955/122278044277823013310195927361738820511526138245123099403529729831101580263017661334033439404145127892869864341370137863502930185898257950784005857039838613651068792053088230544310120182686073549147507931263574696729680205199087261598290247739524177567407336514521615802249513567784393640864104434113875143678954913575131757953888995762605626555295286948615936351489758286086150458202360501030156892742520923119217607034505312415552*y^4 + 264046848847246725899594594089104783242820237900643868781461536116219053542446689165156108707004997888645868863272289626826572911566194309052942483736029415842776186355771437887088152498464584643392484534380585873343527850638642741872443287732143885702001770974724982993676138048964583793848828507009033367039060747537133019911007422403213476999622848027424125152256822395469583302703106897944552757184459255377502462706507859766393581/22232371686876911510944714065770694638459297862749654437005405423836650956912302060733352618935477798703611698430934157000532761072410536506182883098152475209285234918743314644420021851397467918026819623866104490314487310036197683926961863225368032284983152093549384691318093375960798843793473533475250026123446347922751228718888908320473750282780961263384715700270865142924754628764065545641846707771367440567130474006273693166464*y^3 - 52420471756699643759783002985777628509851342059234918585815879660940015374067598236957342538622426943693058074881645989057883409739649346984551248791250930258888206567184014208200786891366109043174216974261031946262754907797879726331025147926763852613813136268348407532729984596729996599252156132771677053042549655064133892370270589665905559561029000571459002402692514910502969688536564774895913845732525747275698327350040766716416263/122278044277823013310195927361738820511526138245123099403529729831101580263017661334033439404145127892869864341370137863502930185898257950784005857039838613651068792053088230544310120182686073549147507931263574696729680205199087261598290247739524177567407336514521615802249513567784393640864104434113875143678954913575131757953888995762605626555295286948615936351489758286086150458202360501030156892742520923119217607034505312415552*y^2 - 45211248391450895062094470726405916919325696617204602523050116603725299301646011575282019447016250497655754004461483801134857530995007711560667984826811862893779272712763340563857501296111449055843798874078657671434671732500686860616154923179152936691416470555273890863119730042994799618819176558323729846305581500896017961528077362578656200919880667446341467112984035590683980018291794069837608937316586267202648921013898954734075619/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104*y - 1844806052065781287687558866472231897600611457276537473923431426907431452671548556599032601577410317427894495736416343411917147025350414270259137826345411758938022384743239303237776510806307463638883287703031899523986826860136172331735496986179020296261620399880926572539731226782352731648284935055330926376558118133665770558623223726593949333148542482823246572623934536871356491148940519463330934045767476870672356232915316730740787/244556088555646026620391854723477641023052276490246198807059459662203160526035322668066878808290255785739728682740275727005860371796515901568011714079677227302137584106176461088620240365372147098295015862527149393459360410398174523196580495479048355134814673029043231604499027135568787281728208868227750287357909827150263515907777991525211253110590573897231872702979516572172300916404721002060313785485041846238435214069010624831104

# 4 Loop Invariant
-55736733230881269448361406098555469673134913817095679218950213147317147732797744723933931305169864694050000695504528296544040514389169465259356298246828254557687877478342719455259078352234157773894956749520509384670749775856264010278691258136245802784272521476899943408696492256950653479388560979947473880989550070377144562650013095392632440442169369421572444254516104344978306627882022672072203019167246538446176484152278747414203014212223882317697893939187228075085499424575813617554894917665399917011916929153020377621508423233654150193022685549914620869762870642762124371552196001/130977313092536494178832749116268856450977721659217007178843465959382888702150961774951114023611013919310216555381320258471741706200578016784904218153939756395171080101074971969148098652727961619277822677914258355979965156273785600775227344925897693266982275496687628103218013984471988715601454307508170058982593916459396688705438420193582671038667141097668471139630408822426847240811012152722029441695637629449549836676058060581697384449878813813616213314936642503553921270080953831438044242911318948095542019046866852501980622674069203421657669715749168373547598487806056934551461120*y^39 - 9911162095186913917974453067921401372159778921555086230664937974116680711687891030066761740504180157887770843876939007952341350256971619061320315364723192077969049878234420269389700278275735816313621155771142124718794501220225513336900006779505126973951926625626265160551911386470605330540329854278277215939771068659809168436273161439780673447229135991990659434503199732241482423705889728765947881495570254003146952127709159064711689096092292322309903981875846304189796662877111174510215990053790302390001483487059069756258311270413891370089762858587394129194419436310222543699748737287/1047818504740291953430661992930150851607821773273736057430747727675063109617207694199608912188888111354481732443050562067773933649604624134279233745231518051161368640808599775753184789221823692954222581423314066847839721250190284806201818759407181546135858203973501024825744111875775909724811634460065360471860751331675173509643507361548661368309337128781347769117043270579414777926488097221776235533565101035596398693408464484653579075599030510508929706519493140028431370160647630651504353943290551584764336152374934820015844981392553627373261357725993346988380787902448455476411688960*y^38 - 18248456149647824211627785507087080427896059263587003529318862189833949549751746545172532604513353121415327428842666414060599758063205652881233230812727338273785824881865213174465439502260376009975693645647392158601293095832254642029703500444674217925713414712631576258632106373641990577235329805472702084784727181456283216273489453209002749633841627033836214357416916058869214645443611729435090425324287726630385435684224115068353722332830793907956499128177168964023177200682551131724626164599532538459269978120414832452746576322766962968118268483029953173173693305842020458935771673679/285768683110988714571998725344586595893042301801928015662931198456835393531965734781711521506060394005767745211741062382120163722619442945712518294154050377589464174765981757023595851605951916260242522206358381867592651250051895856236859661656504058037052237447318461316112030511575248106766809398199643765052932181365956411720956553149634918629819216940367573395557255612567666707224026515029882418245027555162654189111399404905521566072462866502435374505316310916844919134722081086773914711806514068572091677920436769095230449470696443829071279379816367360467487609758669675385006080*y^37 + 582993985348106976533420960904141555484861667171186688890695849853386862526026468441573201577254132285849260048554069741941028877727806556750255526823381535447244273888869948984562873365064649410234025202355665465966242595735536508992255148823161328210513295025550968573288385756750237629828228788760431026384308869901983111665500928808862685375789276249641160285651508255001997881049228643576528326822107740707725127829860050757575144486552570623720782041784712239669575650723115558739638611540985367877551588568271365189419186517062237275956033213211068671449284377996524834207165529077/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y^36 + 522221692894898891855474937294793456395094490136880328742083571006667510500193802002077606327340185626492460595599270119848684253077557672026113245123201745489103060707525226003225461756415718264056358980737118312694022413430724389381967736906658319760313773587972186103718831252208466036877186991225375603975776726974821833496522592350844952726026484295322466759097875992046429329737352856283279695555713580774305570687690022694136870639135907489157897602212614876647421441816239965135638145415414605456805556433944559903888100318416061645251898141672678859962331795696284550430003675899/174636417456715325571776998821691808601303628878956009571791287945843851602867949033268152031481351892413622073841760344628988941600770689046538957538586341860228106801433295958864131536970615492370430237219011141306620208365047467700303126567863591022643033995583504137624018645962651620801939076677560078643458555279195584940584560258110228051556188130224628186173878429902462987748016203629372588927516839266066448901410747442263179266505085084821617753248856671405228360107938441917392323881758597460722692062489136669307496898758937895543559620998891164730131317074742579401948160*y^35 - 37725520818861760317751936398268351831776875070290178243122498738446981946821006553345141744393240737643509958464569228812634847608508232521530803339977848099971696418516742575397422983042993483802137047259256780240071745028855984027427472735343534779889455791626048520104342665828248159927811334625809996116389202359359555053981760824183199740113840045802416554166453704168093657002479891049461054822396337776004451575265584046570441270393594972757897704876649848238782321410881776801458515482587013287862375281068659877477860721829805437843319344183590891243233130753481761912923209987943/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y^34 + 18576658285480740078719886875306259094588551856537316613157870131694263768788903959560247931244640884155534098087711807328928883711827819048959842959053512279671076711759061882113678093280158733013988683849170318169711179632008128994356416616175411721023628925727980718866001213745948766681029990998582033395925591775658878213207638308147074261659832197080481528872090833296310845592408095772634528939343018723609333856245770437932667099107757227846272253654625504046391863469110373069717295521104652668912039198672084723189077848678637871342785816062235235307992471889338373243927018601847/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y^33 - 97309313334986555067868993895044556593399531157849713984331421095560335218969106502943619627211248767084642565975492418556815177971199495105892631414464258220974227254993946357134168300200131341728664382784463167929027118490388097226993546756389226347461724005981227597969690442615528064952587334337726643650577136744411781488551636223009000065292099003386629719623211754871418308422686465458710097769211368425569731843223727997091299682247286589776857725514803658965332882750773882513131129963318012417912469274769933747667444388480161604036615440893366177540625927199785701690616202217097/628691102844175172058397195758090510964693063964241634458448636605037865770324616519765347313332866812689039465830337240664360189762774480567540247138910830696821184485159865451910873533094215772533548853988440108703832750114170883721091255644308927681514922384100614895446467125465545834886980676039216283116450799005104105786104416929196820985602277268808661470225962347648866755892858333065741320139060621357839216045078690792147445359418306305357823911695884017058822096388578390902612365974330950858601691424960892009506988835532176423956814635596008193028472741469073285847013376*y^32 - 76301612122667948915256315965554711965479467959962054699974288258341581449814813109580531055677431068203458125087261120202535089259572373777232621798257308893137469426844619044345848133931723937915870587680536708239651000780314459315653662052097695017637859468239426921998964128181532221411231668731531973403625843548140093001417536775585958028292939106543573399858332927427548098039797303795465924125422883336148610811900319156803087024730088002266699868550546347697488027736456918924474047767077458756751207051869912001301472942257196265217467809346891326943570784217669998468895427486267/209563700948058390686132398586030170321564354654747211486149545535012621923441538839921782437777622270896346488610112413554786729920924826855846749046303610232273728161719955150636957844364738590844516284662813369567944250038056961240363751881436309227171640794700204965148822375155181944962326892013072094372150266335034701928701472309732273661867425756269553823408654115882955585297619444355247106713020207119279738681692896930715815119806102101785941303898628005686274032129526130300870788658110316952867230474986964003168996278510725474652271545198669397676157580489691095282337792*y^31 + 627736170843071457434163738580319292490154037114125723636651165067899768491303291923313612403967759670410702636803839380498112976291834178044978272412844539766288750306728965554539599310368174381739975811947757378034165463008818498045519409266107596997165673653635758739435883677008016916850582918828405596518766793865798662853966678501948544731372419428651372745741193095265784072532713473001020886746014594735253925453266071966570054240869214706137916759467880427921263339550277695155973766287992118112938993997487709874899269302547567712192156631754583989901538694926493813342475409442667/392931939277609482536498247348806569352933164977651021536530397878148666106452885324853342070833041757930649666143960775415225118601734050354712654461819269185513240303224915907444295958183884857833468033742775067939895468821356802325682034777693079800946826490062884309654041953415966146804362922524510176947781749378190066116315260580748013116001423293005413418891226467280541722433036458166088325086912888348649510028174181745092153349636441440848639944809927510661763810242861494314132728733956844286626057140600557505941868022207610264973009147247505120642795463418170803654383360*y^30 + 875312525957414842834520578341846804108480676036913391412823080034836780014308171277006595593533893821158864310238551076832586831182171958714194438288270846631339920317338575712823582306859480187440051848778343872967968946846593006211903892834576795154389186384435863526405681778728543052322915072758935377272332795528298858678845866117949007338503151017395849292307901457336370611747748483775300786139158366263150939774667948150541256643985969643985119437956747009441226572483162311053495808327011618214204746928351795359859933017761389100022301119491142991121859635730655282234235220586963/157172775711043793014599298939522627741173265991060408614612159151259466442581154129941336828333216703172259866457584310166090047440693620141885061784727707674205296121289966362977718383273553943133387213497110027175958187528542720930272813911077231920378730596025153723861616781366386458721745169009804070779112699751276026446526104232299205246400569317202165367556490586912216688973214583266435330034765155339459804011269672698036861339854576576339455977923971004264705524097144597725653091493582737714650422856240223002376747208883044105989203658899002048257118185367268321461753344*y^29 + 79058064090044301968493264264561201740713236640006276531537801295962327140274368961457372218926547081598322935118887657486677559806371691801277157788738671878585062135840825632798679586803444993241688515427270600604058777965559503257311157674732890873817610874927719730881117831016595776158605503477683971370110088365776495937051090426454751215146121748834406093541133409982482306516552046510890705852902595257380169409988145109219095614728908458870986915600094716354374737306706617571804485623627800211291142572525738960749375988720487553158991075933414610799558207533278776232546237592279131/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y^28 + 24700900616590581019725770567902672386686453144501854714492187431447744343960021145457493762512698968398938679192298860865100385168483868679788661229223457493033068424171449999165140987207057619680010638817667866579243203699061255735253708622082634717482355423394211684775677533140986774842511918450245139100468928288437933636940250850750973780620791452960254653660942074959025224463535140177262156822996941028778648948544742382801944530431538737454565233563068169399948605561927020404008552900488635138951260529013038623514084529829292571829075829785668679780150145901002802050919450000050265/628691102844175172058397195758090510964693063964241634458448636605037865770324616519765347313332866812689039465830337240664360189762774480567540247138910830696821184485159865451910873533094215772533548853988440108703832750114170883721091255644308927681514922384100614895446467125465545834886980676039216283116450799005104105786104416929196820985602277268808661470225962347648866755892858333065741320139060621357839216045078690792147445359418306305357823911695884017058822096388578390902612365974330950858601691424960892009506988835532176423956814635596008193028472741469073285847013376*y^27 - 62619484280513232210757140775412369159999002641201952611219804900522052887287516437380981864854842323367900398394572087902138592508723167284352784372498957070888650884374951839670006205202777128724744628471848467687425731185328480525389686236082909425195736860421211355379668190986940548001799174472888893085432335499905323745296441768858975359409711888315019529572029975686114992558953976787748788241592827947710722443344695225413435533456698880348094856384707285328721117589683109332168178526558954122476808332008473229931863988671246866147539768207648875956728647850782115319259467155108211/1571727757110437930145992989395226277411732659910604086146121591512594664425811541299413368283332167031722598664575843101660900474406936201418850617847277076742052961212899663629777183832735539431333872134971100271759581875285427209302728139110772319203787305960251537238616167813663864587217451690098040707791126997512760264465261042322992052464005693172021653675564905869122166889732145832664353300347651553394598040112696726980368613398545765763394559779239710042647055240971445977256530914935827377146504228562402230023767472088830441059892036588990020482571181853672683214617533440*y^26 - 15210175527983933778801258674485474245883189702335330602232187597165229589612820759175062022326058449286411928579259323481787900172360933804042119554979205299071807580613714812783644636571693154561574720654368000761931247868882844768566733700752133542905252393032525687873194314982806165039426150215886141137416155614411976085820390583333998738111608137037705961891900036771743144033190914348884405022751189296789836853970327445570301078512230267210644420991117548305116743852613700429752482854706872110467906587724369363699810234920537117888192568741365247752087577278466317409316249508832763/87318208728357662785888499410845904300651814439478004785895643972921925801433974516634076015740675946206811036920880172314494470800385344523269478769293170930114053400716647979432065768485307746185215118609505570653310104182523733850151563283931795511321516997791752068812009322981325810400969538338780039321729277639597792470292280129055114025778094065112314093086939214951231493874008101814686294463758419633033224450705373721131589633252542542410808876624428335702614180053969220958696161940879298730361346031244568334653748449379468947771779810499445582365065658537371289700974080*y^25 - 276448345042736230644942981726097805308417663529125598014509398185137119621356605823363747783509013912194813076937738242030420552717630150392825516769496296046919708050892555167724185536767789749677342280476849701120972213621545082006000853299495955658860123232341101106254423091216837427366328440553727671539148373798766298347546218356663518532492396447033627331799020063421432237826955189095397425872771878102046737219550990208114729794565028819017066528369964223827565590010786143324491228451886699256401596896272898524051381734893131881619001802022205041045940039834920005552232623912837367/628691102844175172058397195758090510964693063964241634458448636605037865770324616519765347313332866812689039465830337240664360189762774480567540247138910830696821184485159865451910873533094215772533548853988440108703832750114170883721091255644308927681514922384100614895446467125465545834886980676039216283116450799005104105786104416929196820985602277268808661470225962347648866755892858333065741320139060621357839216045078690792147445359418306305357823911695884017058822096388578390902612365974330950858601691424960892009506988835532176423956814635596008193028472741469073285847013376*y^24 - 35835468456580471936965309408966998784688722128872723976002633005434240634169319264636865670845463573929978659703577128575215075205508277567553009124469807241190189441482603877434208918893899601397255247544616100179982858832619959655897149248179583942798501005395036933455413615136834466960377210985450385719113456208137564294909561975306237300160563187533956424073461303798213230143673213111207485279011297002472863810466413379671379637457575866259182924892238616196309290577422234127399131488631860579164269719412760450416286278214289623685089228950283413008615068702821241952814222292069645/209563700948058390686132398586030170321564354654747211486149545535012621923441538839921782437777622270896346488610112413554786729920924826855846749046303610232273728161719955150636957844364738590844516284662813369567944250038056961240363751881436309227171640794700204965148822375155181944962326892013072094372150266335034701928701472309732273661867425756269553823408654115882955585297619444355247106713020207119279738681692896930715815119806102101785941303898628005686274032129526130300870788658110316952867230474986964003168996278510725474652271545198669397676157580489691095282337792*y^23 + 482300970538830073184952231853733238510647468753117186857308286205810946834203895460476526621816339450697899102561018742405969461392472555798925302683971843567726859844873160382183771455510385453195892967321891619687048748982321934723713811808561846152502775488673773573812358822975545841423998835770569056040797882189306190877747266861288960890477241388359421587613069278139957214837464874038135164815146666812275108649181003875262796350338197334787559554913833452881389905341805842634751595883464684281244993158819583431139196882675134853191028233274602513919283173674157179484187496249515119/314345551422087586029198597879045255482346531982120817229224318302518932885162308259882673656666433406344519732915168620332180094881387240283770123569455415348410592242579932725955436766547107886266774426994220054351916375057085441860545627822154463840757461192050307447723233562732772917443490338019608141558225399502552052893052208464598410492801138634404330735112981173824433377946429166532870660069530310678919608022539345396073722679709153152678911955847942008529411048194289195451306182987165475429300845712480446004753494417766088211978407317798004096514236370734536642923506688*y^22 + 3014491649589157924003270851671267603378259069842582078925761724323539570159480503529686349793883713035110570179554475113570688796620843261766867442156786091786136723347985326604149175733757680685869077825044711971837472973098145146573342235469211941386585840908072269964258516173710106709349441230891296720475681944869870768880807171377314820622126700240105392407133787985538701640076293046761302948202489757785154782593114062102178203762214874183145356204880770419420875562208944069546890594493053208786652223154099987738260655581430380679056717677369890062818007791779460331296650557272341949/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y^21 - 80020546941297261873087524808695050976994492812328578641926272987181475902194276707961770682426354526807577497993265060409637990580697524212445971484535123366275723163872777670990916339607248757446165480742303379417914425541454774493795901509844184139733915244981728546919075010458536629506863843951543614164273743441899696892062843660996889038100086937804983501908355453381456054380290502897071812728262134437544138721110991191420324984964373339167175059372732342062304471787085971910859175052640345398080867276636588416825915402337686957469126535019097266188387016860675580841809622406051093/32744328273134123544708187279067214112744430414804251794710866489845722175537740443737778505902753479827554138845330064617935426550144504196226054538484939098792770025268742992287024663181990404819455669478564588994991289068446400193806836231474423316745568874171907025804503496117997178900363576877042514745648479114849172176359605048395667759666785274417117784907602205606711810202753038180507360423909407362387459169014515145424346112469703453404053328734160625888480317520238457859511060727829737023885504761716713125495155668517300855414417428937292093386899621951514233637865280*y^20 - 484048068505874754686155187105274288077206307356020520304330512648887774152171512843902002465295922768205103667176349546520700078643410715327268824643480502111005755949286701764218752371253684862619717742939766144593937890512351382283339102288276717002319340619551489349118206694346378548119180889292439152668105662245087263988331789239332020757458623186773587425216743458179721964003987684670114713100741641569126949989808836704428077278772690233229522692483520848214918903251314265374439767188913090450760940888294629202392783210382265519360545669212562446881924879916642774125191185843402039/523909252370145976715330996465075425803910886636868028715373863837531554808603847099804456094444055677240866221525281033886966824802312067139616872615759025580684320404299887876592394610911846477111290711657033423919860625095142403100909379703590773067929101986750512412872055937887954862405817230032680235930375665837586754821753680774330684154668564390673884558521635289707388963244048610888117766782550517798199346704232242326789537799515255254464853259746570014215685080323815325752176971645275792382168076187467410007922490696276813686630678862996673494190393951224227738205844480*y^19 + 6872530828795498194399200558536992412889025038484755531298852274723375787356657056217736778472644935880138605053667375438530505571446747174640123730855577805151763388806721662790817287143387376526255757959712855754018420172913185007570933572163091089607441930548154373935165188147868343905111950276789349533393447286636388595558703730002633358403081048499389410658735165906971393597141113180624369476365319186485342162051145476633186272019774082767738544725045598316526304452976636418390791569066305919357051349942634758525102056736513812068133573970265136019339924500300299589675862947756091321/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y^18 + 13575324707872981611739922496681746282458005955578349259930222819667186041183305482511146145680100643039118971070994334707486225787223572524109785480701655113331021076707899943279103141428238238506550352116586465347307970171488449662048552556878652929200641466864141676584223361446580073404077151095981071365942598689749838694845376022773876615146781173105701266099712240013976249914050151973838623720489044359229866968343240936501953835007572094296066964579179633420815939773337484450332925275660359934879959159601793968412483607650099337167252944533717185817508004753879006285384666818401299/261954626185072988357665498232537712901955443318434014357686931918765777404301923549902228047222027838620433110762640516943483412401156033569808436307879512790342160202149943938296197305455923238555645355828516711959930312547571201550454689851795386533964550993375256206436027968943977431202908615016340117965187832918793377410876840387165342077334282195336942279260817644853694481622024305444058883391275258899099673352116121163394768899757627627232426629873285007107842540161907662876088485822637896191084038093733705003961245348138406843315339431498336747095196975612113869102922240*y^17 - 315906609937850509754280727230725338703336136258084457433649203350185248231768833753929571505223587686229236350176256494639068789436995903772312849878084024614806740261011953360030352558031068813838084878454148625883485310435299044925701938769529352405316971051264961099983022185511141210491471059094683771497804978533753154640461333190437407092300824094362746846200659747892603125549266741746624257949182115101929293788277613087060938783427039992226491322759138776443456584806843457409906998952607383481537212582372919802916609773665369946942913653224373764960679365106521487872662312813673589/314345551422087586029198597879045255482346531982120817229224318302518932885162308259882673656666433406344519732915168620332180094881387240283770123569455415348410592242579932725955436766547107886266774426994220054351916375057085441860545627822154463840757461192050307447723233562732772917443490338019608141558225399502552052893052208464598410492801138634404330735112981173824433377946429166532870660069530310678919608022539345396073722679709153152678911955847942008529411048194289195451306182987165475429300845712480446004753494417766088211978407317798004096514236370734536642923506688*y^16 + 188724812180563391441484500095310935172932607247050622520221675973983944287189801179602608304052817088410810268197942781373678250286641651922891729331990106816980701439988292030602941411677702187148327841923772888630100822650622020173289634486127976004353284507406601477859860945768553659538340718787113417543322154325457649253399672274336959356601731786595264369573641548843785534348544639593875697243967387434424197373168583383420365723498618551767976233573186179599488646057007212753022859872072825741669082533034733108957723699240314552308448838248400110613574683850667568943083206122188111/523909252370145976715330996465075425803910886636868028715373863837531554808603847099804456094444055677240866221525281033886966824802312067139616872615759025580684320404299887876592394610911846477111290711657033423919860625095142403100909379703590773067929101986750512412872055937887954862405817230032680235930375665837586754821753680774330684154668564390673884558521635289707388963244048610888117766782550517798199346704232242326789537799515255254464853259746570014215685080323815325752176971645275792382168076187467410007922490696276813686630678862996673494190393951224227738205844480*y^15 + 4312401139548713146687935136148451350745642925337564448812212365870115141623353245765945617201226045092746449535211796629719333659966373106941039232401277980182640903643316604421008386946368854260997374777159861588515144858480776300871636619371680368977649173150331025038132536114027817349914685041196369836417063009701733133056650134308522009750742727265802801400471848213625948143542467285085463949921058437567619036933410146109032288709497997493507881225705521555297768681044477461445681074130295578689419447730026513528817360952140053248645373412157517650933599215367209568311583502292683/25978971191908064961090793213144235990276572891084365060266472586985035775633248616519229227823672182342522291976460216556378520238131176882956208559459125235405834069634705183963259236904719660022047473305307442508422840913808714203350878332409459821550203404301678301464730046506840736978800854381785796822993834669632401065541504831784992602710837903669779399596114146597060609747638774093625674385911595923877653555581764082320142370223896954766852227756028265167719921338371007888537701073319460779281061629130615372293677224608767620824661761801487941860680691796242697762273280*y^14 - 174929671609057013262763871273681649659020158724244128657211002841651857191433606037431086601559203530139074390473099712270387870750471910481031438194167094161568677615457560926098039132005460444453471184853248849002580114652033473611180029947586626377680601666774372644130944568601153801038148091146375907228765642168310808310411670735993050978745665524521157807557220324321247847995439223237279452593558804716754443527258339498889097336387111546572709803315124396752242307837036917287885245633116152234921988674837212552535661901279350260788498957216334719650831920725485234451881624991553297/785863878555218965072996494697613138705866329955302043073060795756297332212905770649706684141666083515861299332287921550830450237203468100709425308923638538371026480606449831814888591916367769715666936067485550135879790937642713604651364069555386159601893652980125768619308083906831932293608725845049020353895563498756380132232630521161496026232002846586010826837782452934561083444866072916332176650173825776697299020056348363490184306699272882881697279889619855021323527620485722988628265457467913688573252114281201115011883736044415220529946018294495010241285590926836341607308766720*y^13 + 97206982241043097126894236974157761707400255905210203118796563534785628136901674069604592756006563970027629449134241350710236403781984720406957664737057963258822648243626828230929350557966751346477744510325831177817480880869362489047312852423465477836714850464934055704203053955865183347471620225552082462568239806002563349117087906140270750113484985893559427622050024670653147702241601903252066637082989360791144654894941015982945381073939374840304220229080703519792387041069346987912217251687803899243636773441933482699913730503923026321148087459614527735826078076785886724742766706517307223/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y^12 + 43375222983894213651230568712966739805971974744751541459395727354450187694291731695522611223110683309326360385118694543613845278179389036798160053159873855181784393855114353686844255658194506120578155756104670927301999189656120215739616911555739667217334750390435749775794833393233550282290474571767081570159435003520555551317572031759457881338914219889547749390487064480202174520560102340375010787876591566632165311562810764316025243949003394521651130324211994370431123828929311407075706905641194206119415692971968314091925367746180639137019977392668459261065752910870196150722157657520595227/628691102844175172058397195758090510964693063964241634458448636605037865770324616519765347313332866812689039465830337240664360189762774480567540247138910830696821184485159865451910873533094215772533548853988440108703832750114170883721091255644308927681514922384100614895446467125465545834886980676039216283116450799005104105786104416929196820985602277268808661470225962347648866755892858333065741320139060621357839216045078690792147445359418306305357823911695884017058822096388578390902612365974330950858601691424960892009506988835532176423956814635596008193028472741469073285847013376*y^11 - 3966739272156779148155665989301698072105644863594913078115870236780268010896988882944012902566114394460494063402749541780663388207088463605249592760388525321003809852539925807357314452267133562538571487128052974188023651088361789769984172811768828754721001566939633987088380889040345049771034902889779127162615358128080362624034452552977564306896472260647362054710309857676938989049344843086152308139308182332470290490285026758704196683498067956710530741116777267828826834209187970768455863091637030689146831769803751378145177370780828144295165519650482084911024153468163729679912978791856837/196465969638804741268249123674403284676466582488825510768265198939074333053226442662426671035416520878965324833071980387707612559300867025177356327230909634592756620151612457953722147979091942428916734016871387533969947734410678401162841017388846539900473413245031442154827020976707983073402181461262255088473890874689095033058157630290374006558000711646502706709445613233640270861216518229083044162543456444174324755014087090872546076674818220720424319972404963755330881905121430747157066364366978422143313028570300278752970934011103805132486504573623752560321397731709085401827191680*y^10 - 2564058850510212752683622458703730068347499862323135854679874557174907886168851647153124559987394356639787533797100912901979928477962252976945118290111987156630057989354961305352607524568949300981398216648898246168857448244388443761430412027508755855342263923385590986461199111550274870660501758897375781210883171603357923381921679054044814596621266251635183102984351719276001068698293867876828359167414999335345634822511246776657069930365097091584399788351523915887501161629113948569963134182429987883621107239200526213427959699308970041796322738119345896046339519463160043893687675848854937/196465969638804741268249123674403284676466582488825510768265198939074333053226442662426671035416520878965324833071980387707612559300867025177356327230909634592756620151612457953722147979091942428916734016871387533969947734410678401162841017388846539900473413245031442154827020976707983073402181461262255088473890874689095033058157630290374006558000711646502706709445613233640270861216518229083044162543456444174324755014087090872546076674818220720424319972404963755330881905121430747157066364366978422143313028570300278752970934011103805132486504573623752560321397731709085401827191680*y^9 + 221430996032089264568610569581416626057919465069517295591473285433485549816591862582376888335523259674328490030457166584362678301703239308528758176202845097381659753480709119216764221729535094500524329484464937992842370929912273514660260492852330230650949362470629804881660786856191617881179218245539596762899984779057097452426604245259320268537307054236676277659959827621179666921022573025195391902612185198048794220809475612433973268336472854633159628292134739802456119093545355957577775920325939213601780430083444524080048040122468276118652732646852699705958037182106604205241464052919061/49116492409701185317062280918600821169116645622206377692066299734768583263306610665606667758854130219741331208267995096926903139825216756294339081807727408648189155037903114488430536994772985607229183504217846883492486933602669600290710254347211634975118353311257860538706755244176995768350545365315563772118472718672273758264539407572593501639500177911625676677361403308410067715304129557270761040635864111043581188753521772718136519168704555180106079993101240938832720476280357686789266591091744605535828257142575069688242733502775951283121626143405938140080349432927271350456797920*y^8 + 58497549513997549072849128669412562414009188174780810659759245460172005859029753008815339792341905203368758798573963622756941409065404801099268357202665560556238187621520561646275756965711792016459356551090164604556254605681477109530894528114536406363318186793780468344630638711828821296818144963993061444867285733294144201656652902317819100332820186035378334920653844856881265999844442058376098797135456310642800015388865885744818562691012097344986601665263848142267133714544280604261791816567487731701278370342630611921284839774295579353742248170736710827109964980871957864524879272384887/49116492409701185317062280918600821169116645622206377692066299734768583263306610665606667758854130219741331208267995096926903139825216756294339081807727408648189155037903114488430536994772985607229183504217846883492486933602669600290710254347211634975118353311257860538706755244176995768350545365315563772118472718672273758264539407572593501639500177911625676677361403308410067715304129557270761040635864111043581188753521772718136519168704555180106079993101240938832720476280357686789266591091744605535828257142575069688242733502775951283121626143405938140080349432927271350456797920*y^7 - 52405726300981154647964280350812541534540768605732323787402388536481456757022921175305556637801182651366889208513179114670776344070588805156660361968393705831512077908291946912549561590483644621838490689641302316468927393996227843485854595867820856419393897815982161199688086163564572440737895396782544355032187222589035978060554671197410465315112002330641979063211982133180703976916472559390759846604396021420474957883247051759365507064370066014900127606439471544987577591012149213309873579941434787782190252898104580883729627617040819992687996455378274126260912921926259828844201915802741/142884341555494357285999362672293297946521150900964007831465599228417696765982867390855760753030197002883872605870531191060081861309721472856259147077025188794732087382990878511797925802975958130121261103179190933796325625025947928118429830828252029018526118723659230658056015255787624053383404699099821882526466090682978205860478276574817459314909608470183786697778627806283833353612013257514941209122513777581327094555699702452760783036231433251217687252658155458422459567361040543386957355903257034286045838960218384547615224735348221914535639689908183680233743804879334837692503040*y^6 - 29151289445098150547648465565975934423182917436164300535388528809964342725364122985691177967811955610640801214310472257603246034990857905398250320945747600068008008229441995030037215767196063320910471529594943146259285944891445963115468379131824969778724075896359265305950202346463607563728852481297953990537928501954754693374406220661246475527699843450239033152488680379290865606449743811461085631349794261231743313551814428470124408292772360057458186916027652352778506248176326963547442300725602492371402320652024048584516895627905910418505522430641839270941815929065844422415325824937859/392931939277609482536498247348806569352933164977651021536530397878148666106452885324853342070833041757930649666143960775415225118601734050354712654461819269185513240303224915907444295958183884857833468033742775067939895468821356802325682034777693079800946826490062884309654041953415966146804362922524510176947781749378190066116315260580748013116001423293005413418891226467280541722433036458166088325086912888348649510028174181745092153349636441440848639944809927510661763810242861494314132728733956844286626057140600557505941868022207610264973009147247505120642795463418170803654383360*y^5 + 287832453035411564004959261411257033006997458247775755484169155640910760034014788688923128976256447591969523419549819581569052277403883539169231181241258566756365232833434105204748555470211627371780630930503510929299625256415869833619377341919508218270596769514312077850891049842177261327114163309947575735699414170862901696491290893877440005580753568706023657331376511047279676134550775104520013423057961979040287523010633684053430425497533239291076374314413111002572796249202864730101676345987734848494762135179285999404329093416322482406025993870060068150990510029908095975513167018493/23814056925915726214333227112048882991086858483494001305244266538069616127663811231809293458838366167147312100978421865176680310218286912142709857846170864799122014563831813085299654300495993021686876850529865155632720937504324654686404971804708671503087686453943205109676002542631270675563900783183303647087744348447163034310079712762469576552484934745030631116296437967713972225602002209585823534853752296263554515759283283742126797172705238875202947875443025909737076594560173423897826225983876172381007639826703064091269204122558036985755939948318030613372290634146555806282083840*y^4 + 1029921097524753408527843441222853264577959324856794351497393212094228006855886679689959537869580836649844731301444772385127893725215236885892226735979799550186898041315615609970694061640676114473785455051471876723221833940379779488840066974852825373334967453798907543855302539105781748720597567155225807115177440116931799192203553729390591244757123756930665216404195126065652345571049785881197954598682132009033937600322991910295304771399815774146028994454828369044791536391692125113831616430171551127346584601706719285304408696974668407409853276558880576456492247453523866964003631171389/349272834913430651143553997643383617202607257757912019143582575891687703205735898066536304062962703784827244147683520689257977883201541378093077915077172683720456213602866591917728263073941230984740860474438022282613240416730094935400606253135727182045286067991167008275248037291925303241603878153355120157286917110558391169881169120516220456103112376260449256372347756859804925975496032407258745177855033678532132897802821494884526358533010170169643235506497713342810456720215876883834784647763517194921445384124978273338614993797517875791087119241997782329460262634149485158803896320*y^3 - 11113201591999046240952818356447369315397743607346313800954229915231172012630090563063126455549669404353211471766074199583800404065959844249326691976096206220344623182609920339314401856145461913248751138791658895476619770966004299590322180541079660063582702425789896902216058414429764029087987715732163670647864335206850851979414309185037373919634361193104770172742901142846409771379824963985146516265464566189020473448098970762699670648127281354770642727986210912215323759689785729500918085856019634535321856984008850151306169597647260080170844463235213858661274144627089496301117950951/104781850474029195343066199293015085160782177327373605743074772767506310961720769419960891218888811135448173244305056206777393364960462413427923374523151805116136864080859977575318478922182369295422258142331406684783972125019028480620181875940718154613585820397350102482574411187577590972481163446006536047186075133167517350964350736154866136830933712878134776911704327057941477792648809722177623553356510103559639869340846448465357907559903051050892970651949314002843137016064763065150435394329055158476433615237493482001584498139255362737326135772599334698838078790244845547641168896*y^2 - 144121704638034856607445498266799184336477779950705218131459121680988679786082474437460476344670244700481696097441807018201012298371346847403844731833951501347452664812618215725743813894299122682136723973359519708191131321561103339058901415938531214989641317532893826321759973290161280145481820909231037793685868346277340585009500565917149087649828122424841299706261410396361966357403397639674624319962707168171991611715390143717188052729550318558078103580413695207036087777525260652757153697750302912586721618801041089110460794551616570288359915648877849718134209892673364128882348472049/3143455514220875860291985978790452554823465319821208172292243183025189328851623082598826736566664334063445197329151686203321800948813872402837701235694554153484105922425799327259554367665471078862667744269942200543519163750570854418605456278221544638407574611920503074477232335627327729174434903380196081415582253995025520528930522084645984104928011386344043307351129811738244333779464291665328706600695303106789196080225393453960737226797091531526789119558479420085294110481942891954513061829871654754293008457124804460047534944177660882119784073177980040965142363707345366429235066880*y - 1178347110585124111146833671474024979267926453358062618684272690629518719965788718331495198690234259391919835789255817040145338404155899560585003125246040024894185402432236937674317893625057821696344829287440810802116322634593078226577538873229009987343339457103231764844244848150718504747701779230981002970056785521378645415543817801643158458622759201685752386273514250707550002018736839665399663615403844724940498887565225381690437579870226951274990159962765333621955070464368282678451447685920547724940395991536510872256574937975167512801266213904793936601111528578217703809317287457/628691102844175172058397195758090510964693063964241634458448636605037865770324616519765347313332866812689039465830337240664360189762774480567540247138910830696821184485159865451910873533094215772533548853988440108703832750114170883721091255644308927681514922384100614895446467125465545834886980676039216283116450799005104105786104416929196820985602277268808661470225962347648866755892858333065741320139060621357839216045078690792147445359418306305357823911695884017058822096388578390902612365974330950858601691424960892009506988835532176423956814635596008193028472741469073285847013376