# Manifold: Census Knot K8_13

# Number of Tetrahedra: 8

# Number Field
x^38 - 25*x^37 + 65*x^36 + 945*x^35 - 4275*x^34 - 12366*x^33 + 99006*x^32 + 2167*x^31 - 1105021*x^30 + 1399706*x^29 + 6965345*x^28 - 16084184*x^27 - 24938004*x^26 + 96001125*x^25 + 36008974*x^24 - 355696744*x^23 + 82108999*x^22 + 846052176*x^21 - 514414642*x^20 - 1283977508*x^19 + 1137276818*x^18 + 1214283477*x^17 - 1380702226*x^16 - 693208084*x^15 + 985751996*x^14 + 239226318*x^13 - 420936998*x^12 - 62145519*x^11 + 110647496*x^10 + 19319082*x^9 - 18773109*x^8 - 5703590*x^7 + 1588927*x^6 + 890671*x^5 + 100821*x^4 - 16819*x^3 - 4269*x^2 - 85*x + 14 

# Approximate Field Generator
-0.160154550756694 - 0.185299418868257*I

# Shape Parameters
-320690944625118676369806768343763750867204893822513489861340935129786869001953409377917889823813300259932433254257277294028438275590214939592623834767033887738803078/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^37 + 227985709469809217025007494720263849916468319106675577437539753690889962242038841794022794585636975300336098742060245182132046542425775765841890726844287544779504228113/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^36 - 5576167741983977366570916611524815840260223201059277144384503245311883991369359763628350524971145855722032905152469806657937486416026129771347331747243673416656553809198/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^35 + 15386252421948019721013463237530924974119298816535884450112784303354276419604232752699154401280265976252341098268773161886384896458013688612817856754274606425490949461838/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^34 + 205849424779818370187686999583870074423021115329593979871362091716500947968800247888530976466855818185075001939060927748866078798162190879323579375004572989753623785992497/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^33 - 989440740630505513114464516428209012765530179260946935676214737382441267806622832626468085644228187392820363901688455519480908727190807674177439745223086786656734452668599/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^32 - 2523999310774838496662905587124053337528061984968037415293171618415256507446307366000856893308196770101991472774141425172095985337620207847346105111843250544662159471549369/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^31 + 7496759669141904443469880842230000718848254930875049844506044264438642530431106734552171549495927179832164914398516965313186949595359154772201559121023585483310593721332341/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^30 - 897127829594983514527665953192711473899244196655489018072477078553441593415664379981385042213101150304056631762182574790286416798548720927799804153068190821895069412000271/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^29 - 81430907839937067805318500212457119631631903320294088311075883189679525543062538043507151183083836107777791155518901323357894707186420322220486714817477657483191103355219666/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^28 + 365156668280902991613890067388735372087376252806278304399530276130127038806918192400040828114174534974680929853236580178358367503687138941937793925506412205790696637382765068/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^27 + 1468682090747345724364935171198089549537569657298506292471206251741084092890006096349775938339343061678888932719430459436622294571724977553971540181730115873571734122991751684/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^26 - 3906441574598776012645636336159640747531421995510382495775431204440623251014515435321442551833698242907101746954375913079450108607466273489224492133199833764343243496943237097/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^25 - 4703150003499380194855937250366392841253038904029216372699474806771146069157324578448220141571097162208310435486481371001198125159651458465940465362436078750361131686489815768/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^24 + 22469313990032365774198274718054845191558697990039542331026326921831484715368174866684024415693123376175910483994413288192350239673889582582586066619458236097123351960048865241/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^23 + 1060698657896975146181776709235072550567005333716393149754045675851242239788828997977922484080811107615318020449013805862203660758580903877752801041007323803976667646760530017/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^22 - 80377661880328327357549371199352630337774270094951670362344669925330157367935902932225222424201295234904237632697597491183404740861192641157591942665492001445494856597056801418/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^21 + 7108358747605110614432224950308223294821375847731611562652059539224829604570062086325614203994364729350476233302439219440468351914349709256721625047837033660866458201533695228/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^20 + 60925327938519492474124596220577657885313501108851179593923424596025015178311198083350024638620573967473435856934291146972477329738813332294723774586586804533084858177313924497/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^19 - 153739284928561460178483644940653172477401231142907751452755953032758281245689790430795319049759496270307062868890874650002073766297364139072320369056206067757321412344470971482/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^18 - 258322437989283505822322087908049605318787054578322276324337273062119454295101734883914271295041576187155582768296537228309291537895120030760202466576884437127270032178259497132/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^17 + 308517784316458364571329875355424662060721236634432792034875649355070420116550471691787419962757064587298894735403927359464661600669731869602320630259303829054814390598183564686/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^16 + 71238214048802470456539338941101326572052633910053336818210449846978522060401005644075264359584358859057728079798482594581520624458989654278306694309156620797304460852010496539/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^15 - 70569432938754804439723459814350333141481400861331119014378160475837723769877207010038582790413439024605869052325583849037900932245701277852238856993330533187010950502860082339/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^14 - 29903199072422726474910927186932062848285472937175789293986942863869426484682920497320584718913725978794912429997879376274088104451362861686237638102882357772893217562925834276/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^13 + 79269917824546093145907262535392193170656678479987890496654262799429369807986360130533113229299362440237832141522056292415827688079231779642111877873279111994057234771983232363/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^12 + 2131575713000496404175310401730953008470386798662743158279694755453738552306476221127661717783624036686949704120083356381857452751001448043951070036304301321611344440016873469/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^11 - 94905334790673279171767837827510636054230078392278738676358689406369799133931679184462007711805375821988262330126916139968122398326335393865517510850342829593177897556489952973/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^10 + 51995051584529888529689921391434456166553610709964522034439474857354368108129792613583135285512016239695094654193326686505313340856285264211504331844384303735093506787138531/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^9 + 7808409888108030945221967377612311699067285294106074044111091177167780953563676099030723333847843230044809616735564141989530938706017525341996408796956837001180499464894886643/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^8 + 219565350863496701739004892284271331498030005878318657853063086740602461280680847639829475149178021313803560670335890201079455762257853732665436159884624618466144927832522731/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^7 - 4049673111832928817106579750014576926103026130394936226135591055269923410967345595776300872473283203615097225194420130022332064740356970296180199096705667580030231027740248178/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^6 - 231836359672576757232711391746923995437622649979847133886552050438305914604206090548915471343047949693326339787129072097237477746038781454643693373754498950452722237097784211/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^5 + 84402817787258465058843595898038815016021233071539553537334194363564639765876491528742372433044270221161085661801551379377714025524563298452026499468182905103881678001890630/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^4 + 133425081470974883163912213568090197282495771074051369637469792872905832854375771682773871134601162583277679515665332697432653468172853687537209931407530953429719676154965092/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^3 + 537073813662613700808445918671466424076747877682351301323392804751179129107586165140230083115949745283557507056983131508437637170234478294068629029736822627077358800471287/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^2 - 1250717998736693333680754525260017484722229823284870193768980049629346915851504162846279502612366966866612070951443161062643995460566106416476026427344119469300911682884656/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y - 201757590110625973350958895503107556342639179915149648486954137953637146964482401523915970120852746728286978860711214497150076974644763316726787303658174747218115729667587/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005

-4958778261379302611564642128033001082298011797200052762786437737260064432104242419944030328659618507942104057994125275516060001559587247654129839299274853160247346301839/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^37 + 124659847219011512311256153585710419367653892397668146083573308860306357048475767545692467015350236197248761093579753372346564236851837160438608738354421387969162833149311/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^36 - 339742766410132921804073876040767109478027837719235313928761589399014868518910037753898122421628180891250921445542370407711432115407469967449986682009538767767936314863132/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^35 - 4637050341183863185672763923538677876805322134849916077498332222083970441677985570728739727569514857069993507579882831388285426793381592016509557819220406917455003785630776/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^34 + 21839133363266103539510061497781247904874086389471598520877755589383663526251569450017306239506536392983615218111315655509659136457298989635525276245248684351870095572123169/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^33 + 58219763983245692006275719746297055027024937232125420998273900830565145718521697238607054331350357469344191920765894971984238800293871701354630926827435745343851853264642653/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^32 - 498737847494239447172907168385458507696831345692088655777895558332660687776110701692631089448726097582102525987333968503559931097907812740802743458804923236018925624910235180/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^31 + 19781419470397766331046604354083084042109000637658470477450783830028757495084913350297011501521166213957155774007389495998202653691828751576440761782619978197464517477520433/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^30 + 5464352190248085855156366349436167435854416924719635560705838915486053048031303045515582928064812445183392679569960308173557183110113383482015894865212164104133851883069082030/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^29 - 2566027360447827531317144867388290318101850291560170149680260801597593423433956263340767760810395268937488431693409371295198706434251592895000501601504071826012866353307742379/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^28 - 33396021914428869791439896455755152832371847326414587123962541401762566258786786701004115631778557627255368194611501399331765262415630374482832674607708282985861597257412109146/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^27 + 84276765558330913385484635770904330840592008962195500470633910273827930113353574813532300903255646298718631528565408098398150940109910351008721024248800444935916634880874858611/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^26 + 111531119918516950198741778337232006502936252727283970081592174683984540607035189002295301246977445811813238462797430732693013773852086756656885905322823570438083299813702999800/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^25 - 490299657924948577979424751043731678198464614972516966073359167782079249048054125330059230127592619261368259619003008936082120700841936103683701588921733134220738431601206032008/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^24 - 109276925239709502970682092889946224271178145367956907050217278628372163081425260054172439437750103060388208518399993147096281004315768750455040361039927851436256723615450066441/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^23 + 590704194580400034148900414850303173180810713970855192444705420671605432885876680065354364963987985431834199683492414533939537709457316347484265803426619582666125144851435388190/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^22 - 652889124323168006649024651985494529209865693384258561235054460969528838491080988682505702380925902557762491608501069987018942248664978542311594200251891462340820973713485595258/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^21 - 4081206336043355105118885788356708051268569520067294003146313579694769218473206333390298259274552369192486950205756699702280240226167779057533838433084676262599549490338153853065/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^20 + 1034185855425751986229042271408469751997386711724078321100433429114338040812760056789519918929263650701381332186019883742895345070248480089394657050198858459720611142208015394250/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^19 + 5886227244719679517806322394295200113548787452558244772098883506931702576844031808217545649459530850048187269119159058346324462256613700691699735159243033646998618182005060418111/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^18 - 6402796597465848847503219523926820705868428517642334674255221131157931975564251553272068409234965278231039327913250448621146347926299122593678154024692944880022230246984305040600/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^17 - 5069236055042454814834330262679727078461887797304290918928542664553810318107211790054981152058654963742474005469930167731724314112700239117636493923996096192948892244525104427139/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^16 + 2483934797130215037065879177831066376154308586938816108259351997280663396130397578985007786819993422796276522471665122715406046800185429764958328073187034087295630167830862847970/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^15 + 2360520253472540283046778898945067650263062430026808136389829146924157439744227279251086926487729202455393842813214833184523094118183562861120485765123903411707799364939549707163/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^14 - 1703960775559170385992150660191170723672341973165228525524624422637194826171946337093119844925129457818723779088608045576672472036007420140468021941370936828624579191447710468337/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^13 - 155706982941031479637880425600846348413964565740184651404967085617594503781448890851824507307395371302858845636988798605734206343451614969819775782729192378099160006868226254867/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^12 + 2086845225486997123436785303647648629744941626253240499378892105738257097847958935102246252176868028436993756728030140888273947172331906571940856117159724606897972083949334952923/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^11 + 22495416676968601645277074232750872411376734165514752862059640204449198684174412917471782363280822169959201694823260595777022406544767393863320612614765165124642740357600516822/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^10 - 58503588083585966008329137732620702362324913185403809272461464216192021631047418670740086613931393145960989171821368326776532368094892306765998759964081922654668395412279166283/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^9 - 8439275460713285573361748802604976419178068615409939263211624238478541362016332060307995473916686582959231102873304110506716105812033912610900930034835178340540051549934397467/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^8 + 30083283017940637483514714545142335322609528626685546023761223441319602684139086158092296719606758148376840413705761390631221486631598585916426382696241018184035243333970294743/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^7 + 16105032755415425725638815502096117468342067869925239135291635514806272427927056224963369554599982280274125829206711398452307415774986386708184071967361414928131150167520451399/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^6 - 2996741355172682018100123943027292708088504326309561364767747675445956767164857864132261005084054130911392613118266916573553062517929485827577396323155293952262542369745460166/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^5 - 3087430001454388883935707406158805105332803182252689075281103764721610047336234516705517438295181832437649657081256961892037866759366924299019267849981273706665233252068660735/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^4 - 190193627470748262526978432886303652467131706971761077683855693468386029258038068319252207949547495889618566533730691393832269263390749045044651553016052448401380327992732518/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^3 + 27848707054720402104837979331153925274708906553412203388097811309308226975723078624264304156479796416383095044253695523042062628946496797329530036371263024285348436960480225/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^2 + 3006892162795882271790233866814066737965186988234911986121712878454991748400691983747713260978896316882128552179817000025820067932563929935814481399821190836455300304889005/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y - 1033206266552831801529017945143980999405952306602830320848362338265019028089239091805655004998537533358283080331271096289467846804134858518909906149417940145787436824349509/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601

-11769798149686122726877693456594969009292576965967594779443393735911840912409237296906368260410342863161648309500502400842430312737096193910098253024442970993222886649748/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^37 + 296117006635872027171038727396734480208150764701618732623222152593118702652682811030857644246449478484860163566759363776364018795531992451763782237071974644151251739251308/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^36 - 812443573493108044708708969816539414985979847591421538838640486564246048051641012211984128598809559254914194651983536933003486905109352222306183183712431500964190357180468/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^35 - 10985525195333009668944526713907744879721874883430858166477323062361192168689338231786852667158765272108513706168348304817795266549784751906501128893873548349665066621043367/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^34 + 52042476838416376946171258049119123383579535259298622297239931651242443005470321107753475797470000583194135728964923856329568678214405102601936289857068897372612459378956522/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^33 + 136983853977277264014032737765399889241454153629916771087599116268167014431375032809522252998528961460843990968928831130577022278930133344108085625861795109191117270226951561/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^32 - 1185748574748250235507109182620413865099598178144791948666507095152909471954312087764118184174837146761063686554962667306300243814030979109112463200521873130968809072085978589/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^31 + 18511578013830426313845277718377327073219192789876373429102265677446450223912044362898593626529128549077815688097291523607907285230025337751164983710164147118028755145220622/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^30 + 2589916405279453461005416503765250703708006970672012184818490415018471023549906992347656133827531717541495344186754537987469136235216708824835106239557659353440224915201417908/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^29 - 2058879937679851308638855401775040802718153814784338208886925837116848522126649719930176806293678711237127559838412167114908434654720979293157380640026651232112570423907313817/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^28 - 78714326880437064834764047457184597503643803217448219318389443324510266682749565131622991705235372291266562591075615608576095531334680651666772044073883444489504511388207529127/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^27 + 201373500090509498730552803381895805172777679374605404648901184750647508000231563197080182730046380496821332789828199465278796116951790197976454942409875216879252176721121112284/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^26 + 259598592603463186461628698539529018106875288919083326768184071968441414553429972108660526034963440298076186019927217041487493929562467207124161808693009115687655036667056518308/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^25 - 1166394473792005081221451657296562303141353444976664112498012344763677492465507342841368624858003130069064172189175778574517002739400184070197426176804651847792388431983161732143/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^24 - 232337053991248065206649965051802098721484461110298216319495929911861069295355101611026429473985258931625025425784821372291464812634255774629895117634611047727027276615403057554/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^23 + 1398837131852439594196639675710033116503167444287841054311239743910163841889665612139938648849255920633060461320389027633640075415759535061150376975932631586462971919407026746137/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^22 - 1638264784306137772910952182138109315442524309514666292964432931253377042156581480802644897832887545210595310437588305225545061040086277243829713573960353114991306803147253527083/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^21 - 1920979262556069367611907426970551696722696989863747930894999786017864709614890417681314950400194653622725467860851815836780698918310654764550687788893513963969731856019746029757/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^20 + 2514482814255101341025228755993104921479086495825301961107028299559689426096353221747579048439776503147186467285394509071940124353872300502277856209539506721718769834577781981572/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^19 + 13715379793342899657711474799717156675675929129672254088397298764317956470985988088676265544686924226661920477035597227231354050444482395168880529519386420837885917868863074650953/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^18 - 15406205520557357532851114962847417589651139650658231448028228218990010805222333682777609456913041648104875509878480987131859172551156793336123331125752447843273410992571870102382/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^17 - 11589803372762463567695268404125561650568872791420141329871613895221994788874609320340650685364441632118490127537626174365998162928874904426764485498754033216214286673535538552294/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^16 + 5932696567570362009197055681704314354558709507858674245965140854872459471071131702324283002631541857095106866945988132535115932607515053846709668333791361427763047336431698082349/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^15 + 1030268556063892186930331402080734755990268940858496786502556454969456639815119099538543452773138780821137055487590861352702654739760549605216728193802222582502003814851049417191/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^14 - 4040978341649902083596422074341180947944097076289452137146954199814825788836090108676322978186346580936920869696575972569148933373156683984388348310265290362904571412698878429316/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^13 - 277880793586635584553798602091703136998104861487726829247783958794089112016323485561916392978934295568474205688783480010010250063519175140229101189485471496959529546489423453217/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^12 + 983078842605995889416329506410421158920145904419898401068394682340344604514389333335265412077652376370950696302365568872702348741799482843757014312684549510051210278406375255387/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^11 - 48816505918357254917769708708379164576528069755023298115834271321017156066900713815813560098300729328147564771057106310658128737359760908678693685233413668777869938386987986158/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^10 - 82406094988169171708613285350629770921235867980700588076053054557588035677257805628343363510690800762164762073355656761742335161449052654948218636408919984392460362805984255403/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^9 - 3888277305403407253095293547683046292279247496244373490674715068012333453233770351620865033839849336372778596121433316857614846233411724025524458643916563142117197316200122939/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^8 + 23754612282291980123672787746619545149981191522282161051033036012695838597130965534133488794263615534149726400394438922205900630469473507239245081284805380624312020403125206492/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^7 + 33569896481796655405803723784089668996278621659052104770517432479891121263412998422856645899745474691977467240935268565589917738945715364622909892911780487634173315087335103737/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^6 - 7378570387822413059897305348032658283894004574508962404500638208338598513904034327482540823681175427160191818845201293077771785106462690506847111765453150101508092777550640566/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^5 - 1365969141578445201922846027655658415341772726538892340562647076390996866908328383974875541187254984747288536915159327279881615741447607600734560790897327036696468529441713323/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^4 - 255842482127740082119577017569045117863974422860230316976194666029702842767527574843066298694003395234680359389323504559994250470707790848224811191233934913684296636169369278/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^3 + 14701854990908247178013515627703405287197714351757830341889411088348263431500938955216799496169922703404390777985293207303366983900579647551595884079384976126796614446526739/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^2 + 1796871719251508695561325847007406097141019816715020352219126470073456596946858721683063494730532879606758680493228816915677890230504901923686288305218353751202493455694553/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y - 3498525625425124421549242618124598285092146608088094333430380046967650042629205475052333175856471366493671353213296713279575142070792031175179908650980290779945248794897582/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005

-52377740681432526423520723753337062204585884399562959765783381356872647621309753281176461135009857780724264878599679738656656508045372053686267841662332537231851207685493/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^37 + 1312432153664022153905497296967516195374608971100443495980669081261669920302001769261883441519260597559214368426471920240420204417728799911540506127090826676135725190120763/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^36 - 3506191256890567423148661104786535191719907014079464236434066680511051268480884264661346785571065826282933411772608374328771236821527982891087712471313481950000688172565703/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^35 - 16213624438653679315297850113852368921785262520699718832284162004991949825346107935925489014682363898943908295757842235308289741195212911307490556688864448466966168032602969/30208184726188105831058918756810124102113903391065840783900136349118247205747812929289285924023579786441457772629470399464906410522278293717672197071437512506041984434247360*y^34 + 225245412749022797856101049905252530378286169801691916384662742097407646233248099992910577990547335997143608621747595176669645077219442677419397954664158689287501146973272257/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^33 + 38084191307844466215436648775452550365028439027186948560905913569639778415738856674792030754645962352655758568560130143968117146479426873826387168542965165980526326916723401/5664034636160269843323547266901898269146356885824845146981275565459671351077714924241741110754421209957773332368025699899669951972927180072063536950894533594882872081421380*y^32 - 853224986221959122314788620955639219524965275568285472761402707539061625025246450403741756523532719350139002659635082778242241668799231816052505080422323968822781429714160329/15104092363094052915529459378405062051056951695532920391950068174559123602873906464644642962011789893220728886314735199732453205261139146858836098535718756253020992217123680*y^31 + 539734480807881368789125415645663467118401887635456269466793485648491702500108670199250885413224931069543954594788457292031809541349980238127836432957639027953915135695188033/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^30 + 3696310703040945606985870474930076463939784658732047401331039845728206982649316283406803113033344244931826733722784071031542315675694659507676450508570072696183838927632917765/6041636945237621166211783751362024820422780678213168156780027269823649441149562585857857184804715957288291554525894079892981282104455658743534439414287502501208396886849472*y^29 - 2765483369109291918381384149368690392788890539536099121828292213345455321014023417517768616132374074133330321031560844810322782573275812849142508823903160071330903928994563891/3236591220663011339042027009658227582369346791899911512560728894548383629187265670995280634716812119975870475638871828514097115413101245755464878257654019197075926903669360*y^28 - 333028188874736391016417197964994959576340957864231484664198920396058317064664060260065166738265234207105015611490954751778751273211608127290132744951294342041215014457240698717/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^27 + 59755094134419513090059011607780507416188514936876318449934820468143616526831635809163718017598694216638717399225277042191650555099559327381873818623560449461374558928365907981/6473182441326022678084054019316455164738693583799823025121457789096767258374531341990561269433624239951740951277743657028194230826202491510929756515308038394151853807338720*y^26 + 5623107272226780196880232796948228532905029493070944035398280219339557879929846117615266089137190368531898332770961467797066261629632948636146384299556198969231150519080754184/472002886346689153610295605575158189095529740485403762248439630454972612589809577020145092562868434163147777697335474991639162664410598339338628079241211132906906006785115*y^25 - 4764462786204186670323681376103313423783906681147785049760076137494706334639200346918737512708187380680561012384672105396098060315157925554849652727701535577109013334309927286953/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^24 - 28624488242427698577115204347318020646902074197456708301908906187130711138894631995614406993210202383211243495916899771720753474110731597437923838722434852031977744425401226707/2832017318080134921661773633450949134573178442912422573490637782729835675538857462120870555377210604978886666184012849949834975986463590036031768475447266797441436040710690*y^23 + 2086209725889017217138410489260961596701103437904452966248290748107835655882545822935428153477797077133449725582587153906472266701545992657023699526306174679890139367476573229417/11328069272320539686647094533803796538292713771649690293962551130919342702155429848483482221508842419915546664736051399799339903945854360144127073901789067189765744162842760*y^22 - 6699475678973315314276041566986620769411118368641580590426379883793035151616527181721439622056225370936377793951697803796537792330467163858401238245459837355847687504738745263523/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^21 - 3655691346697804244744922318412980464575001639067605040397908783422099175375784660017623156515925374336070338864804807045968390431743549070126051565110437272355856825700102194683/9062455417856431749317675627043037230634171017319752235170040904735474161724343878786785777207073935932437331788841119839471923156683488115301659121431253751812595330274208*y^20 + 14739568916417752842051206681332621582009686685927572821596242142348537160018683189177248903114747899133188929705660038630627573515427095378467141891296901324480783514058469411303/45312277089282158746588378135215186153170855086598761175850204523677370808621719393933928886035369679662186658944205599197359615783417440576508295607156268759062976651371040*y^19 + 756592781992494745039659248934753777744253045575428280954373347471084768022957042906805687660675326394246746123620462373182544180474658681763414697669126257855984508435723805477/1416008659040067460830886816725474567286589221456211286745318891364917837769428731060435277688605302489443333092006424974917487993231795018015884237723633398720718020355345*y^18 - 28479756270556135144854922438567233400093032685082718885224931066749528585466961449906585392750456534117554553606215681141173630177958600314084369246740536157507475106055979722941/45312277089282158746588378135215186153170855086598761175850204523677370808621719393933928886035369679662186658944205599197359615783417440576508295607156268759062976651371040*y^17 - 11813609676906273731909404900018907084414055137920848846021816319561303197950963447447123388945940748774081550396402760290022073074919648406109668987268329611894509733218483293023/30208184726188105831058918756810124102113903391065840783900136349118247205747812929289285924023579786441457772629470399464906410522278293717672197071437512506041984434247360*y^16 + 1084698248106683055631078479462382915581401831470949034220747862514142501455707131620872584182799257937282387108219316444830435878313356953846992776727353369457521980774088065537/1618295610331505669521013504829113791184673395949955756280364447274191814593632835497640317358406059987935237819435914257048557706550622877732439128827009598537963451834680*y^15 + 538845379935079082102178675579637130352620776063830003248330986959200935777824698911566717365546651177886096250767732747599352061830652739934136214856934891148063785576149319841/4531227708928215874658837813521518615317085508659876117585020452367737080862171939393392888603536967966218665894420559919735961578341744057650829560715626875906297665137104*y^14 - 3078501383192157323710245565313786441591263508528084915389747806387991012744004704894514640874129903545983839059541646442359970525185178591447314891232050230421580832534120136099/7552046181547026457764729689202531025528475847766460195975034087279561801436953232322321481005894946610364443157367599866226602630569573429418049267859378126510496108561840*y^13 + 198296854429811528219428461199442689858678759896145825955752844449529549738189296630161917851940692115698322066699294295434038986714554656203007619530062714455123776864302844499/15104092363094052915529459378405062051056951695532920391950068174559123602873906464644642962011789893220728886314735199732453205261139146858836098535718756253020992217123680*y^12 + 186301594126803379326031068276328560660103104168915474671668744464907702004681545828734029310654250201432704524205914239879415445014564730451732444204697171394579940096160415331/1294636488265204535616810803863291032947738716759964605024291557819353451674906268398112253886724847990348190255548731405638846165240498302185951303061607678830370761467744*y^11 - 426458153549978475265629081001125392182270606058678515894665671044636897633967885836088930145984407388276715558370402751737109643341666141354809554014709944671564259074177865051/30208184726188105831058918756810124102113903391065840783900136349118247205747812929289285924023579786441457772629470399464906410522278293717672197071437512506041984434247360*y^10 - 41964551580097414905506572293582381875330153247894155437042346532609752897648263866830486483302522769398024120786678506972905559681967532954404073035532984173760092467489568403/1294636488265204535616810803863291032947738716759964605024291557819353451674906268398112253886724847990348190255548731405638846165240498302185951303061607678830370761467744*y^9 + 65561304286065192003112805405585224696780923726978405661918727834280823641377448320140518375985536145234241731040698672367932198664828472233193187155809404921962556767841032397/45312277089282158746588378135215186153170855086598761175850204523677370808621719393933928886035369679662186658944205599197359615783417440576508295607156268759062976651371040*y^8 + 477679085698665117547581423687669741350273903772995219161315639610290297731225943586752693930448331379032339043277006691953460251933631450655124474437427773789370811389421708733/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^7 + 522183799527793759506417574366505797869953341436194988564925083904359315650816122696187014416080166291432300453940525850492840740745339364807952149350784583111244161882966247/944005772693378307220591211150316378191059480970807524496879260909945225179619154040290185125736868326295555394670949983278325328821196678677256158482422265813812013570230*y^6 - 51944820611690790217066021946264775423758759850117655195439690616959353005044172119653576766097352163952908369195117087996330923526556299881559431691035586763998102325477277963/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^5 - 322066997756317257346145767828262377911208321644683103711186690451028355240171590276340878012722303227605743966494858266049993915644029140209614368133371594441647337794701475/2589272976530409071233621607726582065895477433519929210048583115638706903349812536796224507773449695980696380511097462811277692330480996604371902606123215357660741522935488*y^4 + 579920843549962180380153372499448934760179907136939785357597297348314964142951719418586012427164541988887399109607643325820131517717102264647497826890625963299051902256953197/90624554178564317493176756270430372306341710173197522351700409047354741617243438787867857772070739359324373317888411198394719231566834881153016591214312537518125953302742080*y^3 + 201301452739310548198428203173652772230293353456588582518323228641728728729109695477988951766750035091568541837873586892550830763583631240180175454894963071640951495437375293/18124910835712863498635351254086074461268342034639504470340081809470948323448687757573571554414147871864874663577682239678943846313366976230603318242862507503625190660548416*y^2 + 1189101696558476614564882253210103312860117931017678017442527356421788835204324072457974358901549099927933358689801766784457165388174711499435116659087137171177097279804301/12946364882652045356168108038632910329477387167599646050242915578193534516749062683981122538867248479903481902555487314056388461652404983021859513030616076788303707614677440*y + 3895781036640335054318024572992976137446485423966179177786230908419808324246930925612167098471983725438163041794376059304064846061037876061725779028938131900983192976292289/12946364882652045356168108038632910329477387167599646050242915578193534516749062683981122538867248479903481902555487314056388461652404983021859513030616076788303707614677440

206929286230591759307599361334326601072955867783266584750885620423160247982612110457278696844781022048510151308868062339587769091564274871646903835731665021058805614691419/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^37 - 740590262680705630967042467867011697721967858369557197126377660407860060908814307824563672788288265428996355234343865430500847392499275604489017906390815009445000404931027/1941954732397806803425216205794936549421608075139946907536437336729030177512359402597168380830087271985522285383323097108458269247860747453278926954592411518245556142201616*y^36 + 13725915408666341965998250424531045099016793239449915004858862243631702243214638649251054805442399495811383609865359035852288973874231224876003419088100797687899035540022745/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^35 + 194762434363348494070976819511675022758211714496400465215601290510554764152294328414581000730550078313584751253287785234276327630202499571667869255980053832677503728776947157/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^34 - 894683482020709716338957740618094498173239150136866019218444270744559624598288191278673757761365188570991187920451003432027581692067402626171038889030073166333216807183389983/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^33 - 156845429350702852399675152570222043704259589121766693434168556526711857195208016145027614779386432717696497974458227268452242638842636095509417494797736917614830777656496532/849605195424040476498532090035284740371953532873726772047191334818950702661657238636261166613163181493665999855203854984950492795939077010809530542634180039232430812213207*y^32 + 10303701098693645946088112771164116154485312340673749842944931835984466724086376685488407938885804001002609016127635897660437868993420866389197022695796869056466847411817282109/6796841563392323811988256720282277922975628262989814176377530678551605621293257909090089332905305451949327998841630839879603942367512616086476244341073440313859446497705656*y^31 - 73506995366333271247830297838945411347337281874578394361891455739672931936256972967151105420400194566344478786357170006020294867598847127178519059230662900450268022270062263/1510409236309405291552945937840506205105695169553292039195006817455912360287390646464464296201178989322072888631473519973245320526113914685883609853571875625302099221712368*y^30 - 228360468423562085530334230931182132789719915020859006831433519933513085271191479032401623639833045665410651360923499383075350105221208305043480398324685918528692606661099486341/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^29 + 8375914452611346219799798440900847385858738027408596200627447276258956001212228506917218651038204289646748495462608199429437028492160423776404719632978314655529786056341091555/377602309077351322888236484460126551276423792388323009798751704363978090071847661616116074050294747330518222157868379993311330131528478671470902463392968906325524805428092*y^28 + 1422647545045866200718498196797503154955958638393653861710020429827777500783588711308883375070706848546160223789612419603320719215588810810628531300035844881331844861248625947363/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^27 - 1699060855275273711152804706507893691313554044812770371812865145817323885440051292381432925085954020976387056937283920720855128088315703595290743534309783478843476512073892424517/6796841563392323811988256720282277922975628262989814176377530678551605621293257909090089332905305451949327998841630839879603942367512616086476244341073440313859446497705656*y^26 - 310339994537468419930994702609269807950110586345710704536803370977917243695243742798242383228707118067542127900985443300355635075954619399151336588761447023918932611507744504310/849605195424040476498532090035284740371953532873726772047191334818950702661657238636261166613163181493665999855203854984950492795939077010809530542634180039232430812213207*y^25 + 2867998513535433108716352225798890949339469442706036656707981839286199396180137346522341527275329892681842610957599312051549624997474674548013035102595991454182005493259563862833/1941954732397806803425216205794936549421608075139946907536437336729030177512359402597168380830087271985522285383323097108458269247860747453278926954592411518245556142201616*y^24 + 396886482123228972209467536676243593691665273100582487867940268783083750381132249730884928300990842351526879498529986126791877455598261490265344047716874110592893470345735708576/849605195424040476498532090035284740371953532873726772047191334818950702661657238636261166613163181493665999855203854984950492795939077010809530542634180039232430812213207*y^23 - 3068891259637612652779972838033861093695300834755282479365279386076326646816580284457078355578892340254937620705023988067523208531326934024032774701372829572158191308893512220527/566403463616026984332354726690189826914635688582484514698127556545967135107771492424174111075442120995777333236802569989966995197292718007206353695089453359488287208142138*y^22 + 20842953207011545833625447042481250918049590563801751593316143944137938408084155718634535801717439168327144274504128326826848743832841277740905621340171236383005769610354871690989/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^21 + 86487288215138748233700758429584369555365360731558682828105493422235851177689135637418051183104566959453543076240335373792721612785771029553762440680342828231127678690807144008769/6796841563392323811988256720282277922975628262989814176377530678551605621293257909090089332905305451949327998841630839879603942367512616086476244341073440313859446497705656*y^20 - 19149800284121822249762346023151977614813745479416334420450339794471954527647059682804489115315863546736149492657898778333664112707784041787695920881858906850832693362466038755819/2265613854464107937329418906760759307658542754329938058792510226183868540431085969696696444301768483983109332947210279959867980789170872028825414780357813437953148832568552*y^19 - 16087812372372829369790884830839960610729195915767324042816526008726599227669824386363455933787819797096112984200306820808620171287872155713518810152521652947247180828390407780995/849605195424040476498532090035284740371953532873726772047191334818950702661657238636261166613163181493665999855203854984950492795939077010809530542634180039232430812213207*y^18 + 123237693661783087109547564670475601035865317078488767730825935265538472322821929782626130565652948160339409526687586021529383019301661351215615163745092044150518862076581934501043/6796841563392323811988256720282277922975628262989814176377530678551605621293257909090089332905305451949327998841630839879603942367512616086476244341073440313859446497705656*y^17 + 235203194839325951188333432678245474183401655819308320830751609516790374775083099159632202125922129823369910080873349029314289569491836338211408678852703769337271911268507744132515/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^16 - 12226130281404937137055795422974426283062892354295567800574563811404885757297287958341434179816426872886045905528129455586405350128095602741076235511793126037949294421133419977857/566403463616026984332354726690189826914635688582484514698127556545967135107771492424174111075442120995777333236802569989966995197292718007206353695089453359488287208142138*y^15 - 31390712887176019578721390587997524803887007565066788134959697246814879676890501356858819049953448768329811858059369044786768749724624879623222359163882189860838882353067212918927/3398420781696161905994128360141138961487814131494907088188765339275802810646628954545044666452652725974663999420815419939801971183756308043238122170536720156929723248852828*y^14 + 17104795518237827922999604455877012186776711953977331410537929116507925709648445234879191869588618097085775695698676785514018705196698572950041890917445197119565634853542727849617/1132806927232053968664709453380379653829271377164969029396255113091934270215542984848348222150884241991554666473605139979933990394585436014412707390178906718976574416284276*y^13 + 6306313562481689073756272987585169642113583967622081023802145614932028077110735191748096524526735380638388395583296567023997190178040323307767370509264941800517521664335607143363/2265613854464107937329418906760759307658542754329938058792510226183868540431085969696696444301768483983109332947210279959867980789170872028825414780357813437953148832568552*y^12 - 42705754114000418842554706765552721700656865533259358313656842020585236876972786140871116121677506673624102575066610209855376843916064701130765458323052263349262868010597987063687/6796841563392323811988256720282277922975628262989814176377530678551605621293257909090089332905305451949327998841630839879603942367512616086476244341073440313859446497705656*y^11 - 8417595151785654017117407844989029118147165214812515351125087355138962638006821852830454132847783383769860507322172467237246671666958459549468113484981857730212392045813828795425/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^10 + 3633200289322328555941131823907964613039548747139889196381112579878084323586337374182485948470891386606412042708618067457126785174096573207111498929979351596543527302220446684237/2265613854464107937329418906760759307658542754329938058792510226183868540431085969696696444301768483983109332947210279959867980789170872028825414780357813437953148832568552*y^9 + 164622294115565296667066820382969849827932701143087220296760160649504587411602650132871964560146309254839572576199072598114499553532985706363104028241358252066782699975532671789/755204618154702645776472968920253102552847584776646019597503408727956180143695323232232148100589494661036444315736759986622660263056957342941804926785937812651049610856184*y^8 - 404254698023234823966070475939463059044780466385902387157972051762068985882611221710086866094104639980638026725780400923866281758907114872982143962756642688482148963759949673867/1510409236309405291552945937840506205105695169553292039195006817455912360287390646464464296201178989322072888631473519973245320526113914685883609853571875625302099221712368*y^7 - 62540218205195696564613811152382716929118692025920093527687543500572727666908180960330027588536253799428605298487184670223691395694960231879268726723412042293566187601554091986/849605195424040476498532090035284740371953532873726772047191334818950702661657238636261166613163181493665999855203854984950492795939077010809530542634180039232430812213207*y^6 + 102878201014920893553280460295017451659279464113019809906091145878727587064916728825899605446056018224652139544099406571884602518669169205777329134809922844681084488654840144759/4531227708928215874658837813521518615317085508659876117585020452367737080862171939393392888603536967966218665894420559919735961578341744057650829560715626875906297665137104*y^5 + 160028779830445601635660567824455132780903902300881862164563258446632350647916164133281605354709478056979999232857666170772860079249981697056324511154973716335425639565190619911/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^4 + 20647037720149882260407972994720945812565429547106731244421969107100582100962749353784226266059100791416447292418644077050014743350181946786494020920218381293827823336946221309/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312*y^3 - 774469969420351024457004627231921997161216555377101071298594553400973202145758090339640633545967877860462571860318433317474318135642480130362770128872342604865220614818344661/4531227708928215874658837813521518615317085508659876117585020452367737080862171939393392888603536967966218665894420559919735961578341744057650829560715626875906297665137104*y^2 - 77663609075798176148266355064018783508364705859449040744473970291336023505606140304941967517383620325742463576200541708541669899515835210974566086511339428036116923858947565/1510409236309405291552945937840506205105695169553292039195006817455912360287390646464464296201178989322072888631473519973245320526113914685883609853571875625302099221712368*y - 47490362055031117684023885111045089675277256242280302459970043823980138848817092910272496031603905524958236985812460641325160886307667448200292761056464195050229453697683129/13593683126784647623976513440564555845951256525979628352755061357103211242586515818180178665810610903898655997683261679759207884735025232172952488682146880627718892995411312

599918042984637084238040323760066569859041673132948374272941798031301936894694899981004935823679304817601340897548774494694414886910149379636753396419749108606198210058/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^37 - 45197948971695396479987004722060601076930080554169986873096984566316982381307830352438508077488135986555360560093999838818031050883937150713574421689598111652532035535289/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^36 + 40705458334429293061528020216083095999838113729948584294192536553370277202261659023104632376754057633310129391327858745758841067822684006292826246093477307303952298698338/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^35 + 1686756707213314003355425825369202109866783389737540285151110702757332857806179214072027183430816658707360218226449551739163082072111682967209712171415223101828473371698851/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^34 - 7884964464161691901180011019782545853576239233172332201294201499629145576609491002296735620664675062939074030415324819135165437559575367836209985435434969916969164639829586/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^33 - 7118347610513731273600742760992144187650049854006304902200259833703390061480049518990720449382505676635413887111877937893393792512804102681379976263021212313001987826873386/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^32 + 180587075346440429663293574019987905992648974436052124745540170124110225395001085102566447069283226914051278940106177814232564843335999956704938665410762536421685426562175762/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^31 - 16680190766048578301086019813850775678091468193201009316119376768552403347119753663257483277832080780197631620477310970825809626361457425500773554369421226113848168945281069/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^30 - 397270327913052544772833819581789543463226094587491430623381004227757252780020109415325358057448234819575189309098262498662990111018569307255978429779711374849846350184166569/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^29 + 2744918748558627710931678150636206206004773588410086799371718281638997800523185226934859938478413296426632376448298100527436162475575976773940159899372574723472736551663671509/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^28 + 12218502929048504906122575585649893263229965635250200205170648560839744651707192555219073734681769695532911320383388338580902042198734455237437330525218796144110024202611242166/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^27 - 10110352615236352329830022985274282208567590956898995701307794418852047041054837299897898114013958505647194073647679824974426261286886390064270353272867197388115987305682731154/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^26 - 41400824102542731963559668647708173002701315116323665135311736690925494256102659446029747316375406010804848485041797354875424705761166556759251939426164758778209413949043019504/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^25 + 177426566449392626587490807794341795951119192609614368107056078234601042925819018702358878930565748968957831033656307311149224686267327208582816101406614457777648688191004859679/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^24 + 14835353158180865881067480094068375687109599657394504054957962781637362043945189315963441256049945485805246290961224805036455762986312983994864286087933484275910090267078587229/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^23 - 644908695935149659589856182063277844394737261208677078191067882455959543533469943409961237759670527266260420904437325745053239754958110236311677341696842394130057914413018445618/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^22 + 221407499201434505568468842383693580352725447122464668210723021354277787046483247309225846579858215723141237009362805540534501389328036422131313754802299632215175011273624246494/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^21 + 99764555879646101258800535799262464534690071723541325165234992856802145357756315137914080571069443219875990591813739326350087182207793353497271033678551098929101912744911986528/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^20 - 1096423582214204802373455120830713579662045349448299102173333689447187207008330610728733458374358220044485789948388230735182223018757165335464931275220599610944525921612565981418/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^19 - 2184141231635019423604212730308334259917871084278834491987606076165539748661265560369782239693950811123174940069810695535070632698398996678263815462249532668306853282363493264524/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^18 + 765236462618202367263809663551426072172367189003338889431935694083662691428756663203795781712113665424246340957099801610567551202122199852226550571619815111248190639600880682507/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^17 + 1922181844760591842221691029445783402851991780167727610170367218928400032960989867336653961531382171235530474568473052033188358828950813853450598148699217552660222954991286390402/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^16 - 2704615061551185915292850120254810757847481049620364391727629473764770782320651103433832718017868083609180962543585585749724367848732121145080148512649653467525578262461153496241/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^15 - 187803895255141466017885785298994757088099614686943437252919595649056118038798119898987422698939828160782403505142884969236388091427767510438729440653279871574686821905127211000/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^14 + 627738166940576429723579750389124490872514885406752479073806699225668113780447423400139852025419762353528232596235104473282455507392164350864565478161486190309920232601998268438/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^13 + 72130540404772923763646934473135786708154792699654584582569476136984469787639965230219008879100297939452287103137814491380229314967952342160506821512313691378557526649122845701/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^12 - 52323349358474142088564264959931648041474907543128626115250437682835347245796344836488444700744265643307425452654317464667502281195490245575531820843558968955314406219710154202/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^11 - 22647124631587704842355149551800397795646071203283518745844661610076591573705335705365922576049126447142244837524402835197861750750661191639651383933843835486329333106338100631/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^10 + 40652894221022555674816585502198983174561166755144663943701317168337709571922992383530777620281677136406484104273715107058599554630300210357768213033947571579245714959916756684/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^9 + 11607660265005260592223440367639470848335170608342533795676500308857226914813428750424278237516616499486572682963730595312818357642174475060387233477144635092338929486982844038/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^8 - 35589859921457437366857850587222114177237395127071136261961120023996171723227000452910074165325531351870808173110175180759350315075985151919237035670546435626535991419056615379/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^7 - 6220539609123330109146089251337027688778985335242841229235413448757319061109241016258363946442670321962585770248166058959792711734853706551507799115716451740041860578595514796/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^6 + 3661882812790213775766100097287025591620203052967273233458543779868180207518234156190959324092907167147950195127199188612338104588794872306570962935338375837545978080919657824/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^5 + 240475662131808987196964972198532546208763796039237813115305569486381711273953050364083908792705664518446689839338656207065339451950569851071159030889423511643448800951696380/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^4 + 11198656186997037522098733731248198254918468871573506701791000601950084328787073299094703275344171457182576405638710568866725111885371142334158887493503515503195754663387708/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^3 - 7402998825057499102462100136120728109552984085274707662111025766803554169516553347898698152394545507457154555452564565373339656966284626179491473761122997207477907063226048/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^2 - 3753286598708653259449209832562849487505366653311650142067600209464671726655559362802864812211938451856961880170437753520546252956719953905219522117637395707367579630578806/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y + 428355166385309874138139378313272388345969844031350493478609515038608501977044995641622124880849645462390470712992609932096898665167522146876666777207957299876767408105801/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335

3122838384155276010014332521771454961114898704818434030426982263907072540363244226573728487031594501091005486062994827326523795889632159420950064906601184972259583238986/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^37 - 78631368105984004113634097956396927184456247150286498899748438584548815843538605745026194447840086146505328717371131464413580396438861508684552315280952266563183966759631/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^36 + 217064438877289676402042449608796938231561349574034956037195016738670587420944446581477722282038115699582512220272270297740570683824673503532119186924148910839500873214841/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^35 + 2912923893085745753540473423829155920927224560110966834977474578802603529454941355716718641775651476170075736733378111597087194720789033876910350050549433199611520317277769/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^34 - 13875445753180684494539173833692627356901640759500376755155374838550385714903740221768453322464047377013086068429718170410146184568021342574863018195224078816197400936227819/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^33 - 36155308185782523612556088013271463344196006658305460739238144302162341155372057762238235145020643468613357983963474056743055923709144102310812259659728373982556686643888442/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^32 + 315823591882491884904154393606113637154103050795829052641422297514004927800962128770344623563437249960066017688850715300658214661074362164402817924465200078331683146537362323/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^31 - 5511133413986119665519890011120875218337190804800833612622024827713735989657522912237793833353101231298571505732820723269480762337600661459050173616477491572421420908097729/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^30 - 689068950364074753477450646376285159040516169509427613284260573909982632973659693748135148287145381516968673815909678604891925983343133589149624117363410456631492457034943709/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^29 + 554573950408353785418099355747514657486307078744682396344118245148464535113962431888422287591882753391987400275352111125116667321667675646438012740929635975189868921440028524/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^28 + 20892501256320207142937798581935390233524742844217531643906797603792598068824655883859208292494787649110321474805788556739136154440516287389902912630223368406551747703656816054/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^27 - 54044385206925457998665914584777084730893007274014269440569906162794805520435218695876135733438583486430483779032994793127737198672971111642333799936966201812439821059700061658/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^26 - 68389732566172730888392426890363072770822151781234438999724576143835983641765960634573132109464908883338112740820888707705092389590022129407933648477548409999683543379375134966/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^25 + 312739449345224791386131606818584472113486304832671688795759277227506046246232629555299351802146894412893236473265128553497017207607020302587505490670835403405533905757277109501/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^24 + 56925618159214939285924519537167472600571733249513883700434842748551982429567169035268186832548911031472139325220484245442860002842318837043411358595203725833359239199671887343/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^23 - 374928561591532248022068739087720070306353816052810709466921253720665554075162695889146276867600670288717240163804708762763831734162057952632197566213131610731358718593917938079/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^22 + 458461426304793355864184652426966451431573256981761458571640245155829794878842543176280777404724466385193739471296484190051311564921134340442996136975717117766955478035423399311/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^21 + 514661841121740810035661896740769572555001881757967756372585108341529386829334488656565868760188559910892678555696745249765730374234321236207996772061349747475229394653735543499/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^20 - 692115283543442548243270742320358792521466577930392076903965360441910893919399267583528662389194853603398204258423660542833389522713945980837707906905669793307155590103503852394/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^19 - 3668034819538699908789230366981723845188222068378144744437277663781843967384480731610782514186651508536915940470340980864131044268561609263491272273696517472459775411764477636846/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^18 + 4240442412508489240533450556971603171241513623354237525395577175134328595424161818712839751910473051884433987124033226478357251999387549468518921657945593086021225305441410369749/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^17 + 3075906308109635593232189863384439712962198426782635567593062728162407073297581856671018851313917693708188480521530359101493429699095374697758583575832765668986586613964039642743/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^16 - 1641278935865294092721151416694302573460327867091722750643183342332763654935877779059217734712706697300722180862043900568129203741531858801471209415360502063441092849835159627448/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^15 - 264015966815795414575635893162861327107399210499601748692035453790513879318594989331605291493794604614330902517920441056207272353033843427122417891839512504380105339760383796447/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^14 + 1128295936449028669336153880428312808856593394604403342377210089036273492844195872022599979963072869328368667451004022867454974752218335024284363819801190012104831222558714801277/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^13 + 52597097434064941168115819264978638061858554222758076500903118978233074693259669532629978972776879805098020634551932392149199670913439641669576795763632690007941429651973468669/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^12 - 278282801862848475505470765223735413434523462474638326696872581064345121012236410127724073825228876209929770772271433414019040710192094369251013879143756851494944297089867610655/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^11 + 52263225773688647803812350017512183829310296766513197024284618584215536109416078106754946265316584674584909670469946718919381878695442578709266236762705794130817948871767093666/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^10 + 23765348766218532718114996255489607041758231024404730150487360576946921902858545025161649396011404795245913850001806244278201300798815878430983179211543894967172672709474955881/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^9 - 408040206783409263639546490596861401153946581172017188537047665634401665085991734857697456420680786236883982429683880210842629853328314776211322231398599980448388238542558512/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^8 - 7019190584692431444999964896566353962011508597403263925715094201016698634445752567636330513084604310290281635179596263698325055040859111462283117244127010242823374861545409864/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^7 - 6655431411980602892177263534719431574972941183508878383878536667699220478831839733143731269515997314558428741258453786240202080835271186212423865076308178759734095292831557469/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^6 + 2346380066277867060996778947838142761801667530180643547327347364822961719213621987298341603205795573581253350711478749240088940638232142097100054933346915607958019523557645737/202286951291438208690126688103639223898084174493744469535045555909273976824204104437205039669800757498491904727429489282131069713318827859716554891103376199817245431479335*y^5 + 333004351058424845310248829056057729310886874679638354673521638488335043614348977021804008828820048749238332899126489222568249478529235937852232887754324126336273700981095453/121372170774862925214076012862183534338850504696246681721027333545564386094522462662323023801880454499095142836457693569278641827991296715829932934662025719890347258887601*y^4 - 64276039581034753922767563722923161514580591636512517549098626282337598521500100510016034677567647395118303676589581994955959460588116425159620958780393143811304115593747154/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^3 - 4461887573699667786902282264779770712784960143555433976542785205278129779087081614111211920681189859709493011028901937123714188721493608764031831632820462992410037340180658/40457390258287641738025337620727844779616834898748893907009111181854795364840820887441007933960151499698380945485897856426213942663765571943310978220675239963449086295867*y^2 - 587248640175362335101756711723014757117073569547781871957998399833168960940410019675684982046989874560935602786151019670336237054386969206656253791816009284573647602330796/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y + 330091102625615408323339465548572900807100944359168136433788962642458149521748185498033630174404107989793389248687546213715768181176977713085567482072572420395282770679014/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005

34710234666879781930242260232981524046990636359603088878961689540109287301675491749526050710586457939381496580143589687680004900486168258410220154717102818719768307694862301/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^37 - 867408834852407761294627716709758534628904319485284588066651311284381437785910413324819389834633966046058470223622413198845951726308917339578162269856957265278132678406844291/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^36 + 2247787506435458632179499750214776325000394566086465583268080502229307830687487956713862877001830427970666666408990449833034141977335646177965329831591372485706106359340806751/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^35 + 4688038654583095425400655371014012559956694165050398789350753874432767210857406423467883805407782479587663694050451902728419014242378122399579030584371787346626515972074619377/16992103908480809529970641800705694807439070657474535440943826696379014053233144772725223332263263629873319997104077099699009855918781540216190610852683600784648616244264140*y^34 - 148038715431902460785202590967804951306389607150211785292083048281895946907653143841591976215084711095517332109770756815934805794535252265368758283861241065079012238216038951969/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^33 - 107607545261410396249815639756826049627748714983758153109161923715835414860985287139302403082321683549999173680987100211383288822679391771579907971602050871918522848918736259433/29736181839841416677448623151234965913018373650580437021651696718663274593158003352269140831460711352278309994932134924473267247857867695378333568992196301373135078427462245*y^32 + 1715475632998496446245471672241142851825047999282459948988786479521838769867957768566943626422271563062866546491934692672790037101517589133219642624093225944131571727132284097779/59472363679682833354897246302469931826036747301160874043303393437326549186316006704538281662921422704556619989864269848946534495715735390756667137984392602746270156854924490*y^31 + 11773598581096296542182259457111774428463759975301397426307056836054148610671800172112263365142183378928236108323272089728738852449797633962071551865522948050289909960226570631/13216080817707296301088276956104429294674832733591305342956309652739233152514668156564062591760316156568137775525393299765896554603496753501481586218753911721393368189983220*y^30 - 7665068270081556693362160724304586022970935896026451740718710057956995903025997761353608644186792698792378152945987539950404466825168185999972504845502368848619500223974174002987/23788945471873133341958898520987972730414698920464349617321357374930619674526402681815312665168569081822647995945707939578613798286294156302666855193757041098508062741969796*y^29 + 191269607651731165066638629814406673594100564574580226527435530160215319827976622623675035302419774030887566301365408488462115570856633282396674126875283348780385887732838249548/472002886346689153610295605575158189095529740485403762248439630454972612589809577020145092562868434163147777697335474991639162664410598339338628079241211132906906006785115*y^28 + 241928876239157113735856523063409622813634779035281233166944646308914191373685888608187733645657380584527120969804845677430007080208120255949093337924918236940353872900897806703749/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^27 - 277720308638218856902726307124919825701154641803506093772834512434466226745426590306631440437644027510811659530054377203407845585828954375530046045828687771956549864158006424337229/59472363679682833354897246302469931826036747301160874043303393437326549186316006704538281662921422704556619989864269848946534495715735390756667137984392602746270156854924490*y^26 - 4434511470535707379529109748899519962962241283622905232724200170711251394138905711880254258250796620915324819096734396625688378197786868981484245208777074424813284159167489702536/606860853874314626070380064310917671694252523481233408605136667727821930472612313311615119009402272495475714182288467846393209139956483579149664673310128599451736294438005*y^25 + 3318749122209840893037498444690961569284189495261240604688130279882083259640533569714225550421734398264912028473336170039179459985440662635531328790491198915707752401728323432583401/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^24 + 319047062969436654162318847769676303362818447004511902769234902415159998163655439784855841758842733693720647962580527701943073320356377288965826255081751468287471917683456513641357/29736181839841416677448623151234965913018373650580437021651696718663274593158003352269140831460711352278309994932134924473267247857867695378333568992196301373135078427462245*y^23 - 1025455657222900807587347058961151712952994791380034087912090202157667857555540431429963990406217182238913614519837103789433634489435556023216445756104496345614814469732278236962691/9912060613280472225816207717078321971006124550193479007217232239554424864386001117423046943820237117426103331644044974824422415952622565126111189664065433791045026142487415*y^22 + 390753809785719710390638663764227103044866868359361241477970753494955537568324829107355289849589788067324361079410190176866336959147543566978143682451730961609667373433153925755493/16992103908480809529970641800705694807439070657474535440943826696379014053233144772725223332263263629873319997104077099699009855918781540216190610852683600784648616244264140*y^21 + 2929182886964771445936866083243767188619371908463808608162119214755398246871345942270748880697106022786461687562145446034495741438467948239606351743247129755448882793930361374132239/11894472735936566670979449260493986365207349460232174808660678687465309837263201340907656332584284540911323997972853969789306899143147078151333427596878520549254031370984898*y^20 - 417410369912566408167176341924736390478836884141825564853987529439388839110562973190001459334321703939978493223300203895109158257179711775412608275654386857793137156593271634520251/2832017318080134921661773633450949134573178442912422573490637782729835675538857462120870555377210604978886666184012849949834975986463590036031768475447266797441436040710690*y^19 - 11126442924362122182015873021925815990835203583694776281682791886891559035352248144873468787931226543971741935469519762597884625493371907816993985623628989745945816766742242586573844/29736181839841416677448623151234965913018373650580437021651696718663274593158003352269140831460711352278309994932134924473267247857867695378333568992196301373135078427462245*y^18 + 19432582598299378338494898847314613116612120737927898733071582909007115495701819118045506949272888498903257749280789640649112323379540711618771900554549691359161503134676023266992377/59472363679682833354897246302469931826036747301160874043303393437326549186316006704538281662921422704556619989864269848946534495715735390756667137984392602746270156854924490*y^17 + 42193053027429372819220376687715103309392441638106221683464238954618881738366288119625858549044955442282518957559076322589775353081476336887708715047728470146729731965616226277469733/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^16 - 3929545156515249233493748340040736108735588637840752129746848767444352992415330687957087363319228159802895937012930612451704574646350936718138760846368676795784604388977209842153122/9912060613280472225816207717078321971006124550193479007217232239554424864386001117423046943820237117426103331644044974824422415952622565126111189664065433791045026142487415*y^15 - 1211697927170359524847091060377269482725080475401683676502173097381065005527112806838852978185125162487699385412668768376955155920090357634465567610180271782536405009974900934511244/5947236367968283335489724630246993182603674730116087404330339343732654918631600670453828166292142270455661998986426984894653449571573539075666713798439260274627015685492449*y^14 + 2797127907323246203377655738550364924896389200718846424261699762856156696662338201944841028029264405265597535800622055275518536329358563064068738428406762769407792694573084789361113/9912060613280472225816207717078321971006124550193479007217232239554424864386001117423046943820237117426103331644044974824422415952622565126111189664065433791045026142487415*y^13 + 1416197223133078074821418921372291280765954697975516079374513081196384037813693548365864090295994548685391099885569217607443408406640808083461553948367333476376892251514862152350077/19824121226560944451632415434156643942012249100386958014434464479108849728772002234846093887640474234852206663288089949648844831905245130252222379328130867582090052284974830*y^12 - 1424632657264213968453096651315708903810514735775998881337322712619020431322897278307100135406041836817528429502376339979979018965981874626492448932267993454640972034297899661446005/11894472735936566670979449260493986365207349460232174808660678687465309837263201340907656332584284540911323997972853969789306899143147078151333427596878520549254031370984898*y^11 - 2269704972731707915926078198605717124423547103797018230880097557202677669769693863293748752468835837395562074917095668959555728145924354906169140827999182623679028332145114332821599/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980*y^10 + 123486740842742015140128389790205278288759902995632266799358471042013861741544605088584574075234482757179350874721047794973913160495621857350384528290692185362404454751991362767559/3964824245312188890326483086831328788402449820077391602886892895821769945754400446969218777528094846970441332657617989929768966381049026050444475865626173516418010456994966*y^9 + 39203202177047516233650679613922738213076740512090823843411378724561382157489435544017385194144547425466175827859386327160909523904749823744169817301138317245632503954880441894599/6608040408853648150544138478052214647337416366795652671478154826369616576257334078282031295880158078284068887762696649882948277301748376750740793109376955860696684094991610*y^8 - 68480565710527048266868562954858416903747934391651377610418855311839271863946638783314272922335843228006071547775486659317600179662973099160721592068656156205521742006800206677429/13216080817707296301088276956104429294674832733591305342956309652739233152514668156564062591760316156568137775525393299765896554603496753501481586218753911721393368189983220*y^7 - 50682014337372090965782658432770630602960690772685922214471044482267204839398194300501401503149365945240043754831981440888925149824384537175666941577102517396493568754831914693126/29736181839841416677448623151234965913018373650580437021651696718663274593158003352269140831460711352278309994932134924473267247857867695378333568992196301373135078427462245*y^6 + 16117125624902944161585885390300975668918461605651073897510114560901555430241793515499286195592243128650703197546658657718197192060912649279395838506442632195769976010588881654877/39648242453121888903264830868313287884024498200773916028868928958217699457544004469692187775280948469704413326576179899297689663810490260504444758656261735164180104569949660*y^5 + 6113054866397712191474743040954044641457762333372390431992050105263551566233923964139558293360165451869557906727516624791117086122672132044210684704042825359599456194236408711521/23788945471873133341958898520987972730414698920464349617321357374930619674526402681815312665168569081822647995945707939578613798286294156302666855193757041098508062741969796*y^4 + 87289510909099127550457304223760733881564760190064735709633694172815634272147216979408215654575480213943607007275283521644486333190444688210643505771757231552114964035577860099/2427443415497258504281520257243670686777010093924933634420546670911287721890449253246460476037609089981902856729153871385572836559825934316598658693240514397806945177752020*y^3 - 25903193624505779328388599249577314046345088767498240211510217978778027869984115888564167886566214814645682484757131500276864114300000610327532465534499297270145870591731377123/7929648490624377780652966173662657576804899640154783205773785791643539891508800893938437555056189693940882665315235979859537932762098052100888951731252347032836020913989932*y^2 - 15981658074269709877532173655867839004760229070613423404397333423657034587230039210692170237528003315752842565778121650833995487406150985541826072747863465933414477689822473731/13216080817707296301088276956104429294674832733591305342956309652739233152514668156564062591760316156568137775525393299765896554603496753501481586218753911721393368189983220*y - 8526426722503848023910141738860581791007533262041998989127766027109770017652169856607780387250623929691394812694860949398885860908648692706210721283495473440194741714478556431/118944727359365666709794492604939863652073494602321748086606786874653098372632013409076563325842845409113239979728539697893068991431470781513334275968785205492540313709848980


# A Gluing Matrix
{{-1,0,-2,-1,0,0,0,0},{0,1,-2,-1,0,0,0,0},{-2,-2,1,0,0,0,0,0},{-2,-2,0,2,-4,2,-2,1},{0,0,0,-1,2,0,0,-1},{0,0,0,1,-2,2,-1,1},{0,0,0,0,0,1,-1,-1},{0,0,0,1,-2,2,-2,0}}

# B Gluing Matrix
{{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,2,0,0,0,1},{0,0,0,0,1,0,0,1},{0,0,0,0,0,1,0,1},{0,0,0,0,0,0,1,1},{0,0,0,0,0,0,0,2}}

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

# f Combinatorial flattening
{-2, 3, 1, 2, 0, 1, 2, -1}

# f' Combinatorial flattening
{1, 0, 0, 0, 2, 0, 0, 0}

# 1 Loop Invariant
156570938763478119280491353249079481528784463888845886355566273945206059158374027973880408942081995455718946154491393611710086706653778496065297748109041737135554539774551/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^37 - 3901765270824427598643263858512864483850391695091358309167781662081708333476123012624892116071618553047973117189458870183418851127648582904099769176517112875460490688813411/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^36 + 9893049999508956885204045258513781198628009467410812599145936137190149778149195852480471802186201343895604650128114674003438146156193200003223631799185703645514771500723851/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^35 + 148086628242989514298279016526790457634812192400863266855238951103944648685200848424250824267880657857067090375123401053086766295992387287217298454585185878419301042309839449/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^34 - 656379305687941235953490592845391032620798265320249074145874244940367653459518338128923763421727677669234230743155866647769485128320293850484275203102227640853666181395959349/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^33 - 980697681130644978607636453891267570761455629805268789668231503422032855514938033013177967717889652858527022907832830033114522993370231917273973229443243664332118926774599181/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^32 + 7627061050940348951571672827037697109833989951614087631583797691220680557669953334712254490335715697807267026753000290870768076692528293871291416491291687503868034205879593869/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^31 + 1127398699777602689321617082206966222673985643060174610001787719729854605756741094697204913293324908016333119102711885899919333248334487864735627120909267163436640338806834849/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^30 - 34126055987150932452539997356598528900305958754370031935788937847189341698491147041284539748369041773002475024262732016871242872128348826480765315482090093714121101756451758405/26971593505525094492016891747151896519744556599165929271339407454569863576560547258294005289306767666465587296990598570950809295109177047962207318813783493308966057530578*y^29 + 103925726915152055418981008921857784186025725296972282059130580478752300649658338017690656833173152639768085851540333154916612823696823343157479380986923240230299266933194096448/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^28 + 1079206738226307059045553922280452976783271290485999398770532620878297100480239273721540744462493156262984603655656520473060458383283417119960594147951602221682395509973981206639/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^27 - 1210687664213963847481443494869055104382497152849360709829600668026991858009023282237740912371268729616039283384938392024418996274760494602234494916503831049910813924259378985724/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^26 - 1948721093901361814153974869233223014005049231718450845962557148109098742471934145048301623537432892804636200715926536961676873563072267237919807311354898089198405238006060239198/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^25 + 14478334895652518843689196803544796738111504335090610182085384926460572347318744290983872048516700243865316090348770858638077366746865445580978162712131956625429904321158438651901/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^24 + 2940971537345891721457771289250701823409220213523959287263681564499600266493114667358840840875273214369640924173997958385466165594194650864842513266132481476921727530060618281059/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^23 - 26756362353198938655198783000057709379535910845011793293097067028530396384558244483125106994265233954998313511258659902992053574407453508181172954511702867512422570648378391442916/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^22 + 11209072107926661562680878659263865475774114432212785004990848846832553882730368580525855332536911511631903073309015315569468030388251722304639214306410696410563418607082543302031/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^21 + 12635215316064575887681028568770402739272629401561047104674324860256909752173729959870177524896025451914665035872329656587106115254720810063656441375192642229177340514010982471880/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^20 - 37494672837184674506177531424145759036239224355712579970746213545196080114008234076398581855417544031423211957013561440568785239126304553639675865510748016272793500947133825123006/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^19 - 94459108514529791687573162963496500847559100437672094338591568400155520684303694967970873779211210502669902641341847016585644055406178561003150044760161636478151081023347646768163/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^18 + 83286593037374367490269031009164351779441240226036360270847543175994115787475794376546173749405072250605023761941248868731987193607859916704447329596295552557684152116260087359062/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^17 + 173372195020601942293739336048537782814674192048799586740327544778727418044621643375083933477649557939256500166451866753554648573287206006897961975779751696589477535462419131395713/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^16 - 100439219191725638138445836956661402839220933334545405084037539118557149036619227149920237924929335751697099736482442412549938518294929013571844251528409681641919921806654366694792/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^15 - 9253394202166995242566637958041342368995743165597871420458156759430057374194177682550437093842328105942939202256418167786504683386849882400598122484383832611772700484800825099513/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^14 + 70649127009183924533706858046229993970795064838532216414660183097952806541919105693403746612316799755009342107793388905252368237568480150212441908067535048519142796923540562886523/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^13 + 13516833785188253862840109159462147644085430035023006621719271163520803054813807147590818702751195115920452307216798418138246072679894550299722528277081053329673778396228100456981/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^12 - 5898983276173174394409618373452022173933409645559314664420751156908966095730837234926779571310403102907609921525264756763240879133187175982016407235671353212315743407959145847744/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^11 - 5147550637545705482573530866600313690496408926981762953436921297379195391510264662927525803436378484897939254667816332512676069598808548650180185404975769229188639341329433569299/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^10 + 1512997283440097675669104686985949966743993581427188696014475006229396931968320794913356258030965594421322485060791587495210072652619443122493220644420755174480784464169598660454/13485796752762547246008445873575948259872278299582964635669703727284931788280273629147002644653383833232793648495299285475404647554588523981103659406891746654483028765289*y^9 + 809353909899090788793353937330179651042708676699831111843721438724404818059779830534968481710522020617756481957495075786947598411957018569479764296321925754516699479223358435031/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^8 - 2560285417580344074463179810494731732856638737543754772495505762986047499897770651723088540008262186842691615467156661114858264447517635220081627742246138106612022292340970083201/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^7 - 283253674818691352020101154635774799938809620785225873313036544172121028665370597906708027802287802148416468324356549055317948482193210683008166936560467923479112094891201803817/67428983763812736230042229367879741299361391497914823178348518636424658941401368145735013223266919166163968242476496427377023237772942619905518297034458733272415143826445*y^6 + 242840773851386160947385101685908866385807451913028731872755406065743190489261449505512005317714377657765375874095494971263057943798250636738402012454992086156960891715443258351/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^5 + 18593610415274995623327055989251708124472278741962234803281904381533754818390714528018298154097874235147289919468098266982187965173691361599682834637369635595656764938258424085/26971593505525094492016891747151896519744556599165929271339407454569863576560547258294005289306767666465587296990598570950809295109177047962207318813783493308966057530578*y^4 + 4786410088803055274670693586451069393717142948147091540366586619638550965700015229471006180300190255116203234752172869661814308578969316854561219688217576253449202571973740801/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y^3 - 512335600990795658273157332343438521633731419734648048848951792851271459761517685438623806212712879175340022696401150304685066157766206269128464712216954671238390048127538489/26971593505525094492016891747151896519744556599165929271339407454569863576560547258294005289306767666465587296990598570950809295109177047962207318813783493308966057530578*y^2 - 295687844511135109188477647289352874359094740331722804377882652773845154347587902572788633583931656571604033481760598949083768455732363024690007762509879953674509960328466519/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890*y + 19976586162664571541431685648124466790718335152141555574078831397290550391102775199341045593162971235852922557625894525887788288420544708076954857571599817108088093573868999/134857967527625472460084458735759482598722782995829646356697037272849317882802736291470026446533838332327936484952992854754046475545885239811036594068917466544830287652890

# 2 Loop Invariant
24903500648271550139936912728702185201974742462038282336594304524848157750683015124707555002712636836990485582760553587514703264090953275676247205984065522050514583562834399243171073158263169706221978338141700343031672710881754163877961218948086247656188546996218262161877622166025047023028125096038726179/73159077678211037833347422665151391208630597978850701569131911918190792400970378229922054507392741387719310748606618733855543835200029379569556636249751804231219840232920080178836849056750899809515575061102213888944799948607361149735432086480461553244507055022647857023059185358110097688241364842420822700816*y^37 - 943791657814117662245237458221230715426650423561903096455832296647677722911387501558153164976383295995421106587838356773488520985478633837721515193035767062161217531399719955174050989478379743386054196873955021810524680980574660082882895791822102456481598297328375353973040572152505554347811747086519786257/109738616517316556750021133997727086812945896968276052353697867877286188601455567344883081761089112081578966122909928100783315752800044069354334954374627706346829760349380120268255273585126349714273362591653320833417199922911041724603148129720692329866760582533971785534588778037165146532362047263631234051224*y^36 + 1338904307716696706364625491950826927273570148720328518101024763408631693804723667740670717260782068088849640460336203279120220660993194792893778475204153124704521455787932279204075042313739900356062142792648678635655371044276825484139815273765049087495677687326243990179869675001163883117105904449152724795/54869308258658278375010566998863543406472948484138026176848933938643094300727783672441540880544556040789483061454964050391657876400022034677167477187313853173414880174690060134127636792563174857136681295826660416708599961455520862301574064860346164933380291266985892767294389018582573266181023631815617025612*y^35 + 34608264498102773069266201590483448217636544838942300314458551982259763749370331749161606768438621262399859700946738881082095686143387688918159831657857111691190859422753402708764898769169071779574211385476087822059248391502902126928827800825265275183889395418418930392933870400790053554277685662003496268301/109738616517316556750021133997727086812945896968276052353697867877286188601455567344883081761089112081578966122909928100783315752800044069354334954374627706346829760349380120268255273585126349714273362591653320833417199922911041724603148129720692329866760582533971785534588778037165146532362047263631234051224*y^34 - 8045125601191521248415848154178774447720218356030412416566465657383708585696239897710437886965524874089238537574306273263528703842780964132382740537913715294030795038712069382315943101111418111746616429834570259663859840127654028960286062163119399128253384410589801545939172298989966521964560291159018186915/5225648405586502702381958761796527943473614141346478683509422279870770885783598444994432464813767241979950767757615623846824559657144955683539759732125128873658560016637148584202632075482207129251112504364443849210342853471954367838245149034318682374607646787331989787361370382722149834874383203030058764344*y^33 - 69615896242885876909732007884804404467976987732651314979469470153346994692288087692694739356921114247980534145552364645614103875880056267948252736761194635530022076864737422051406574638297848467911224452014629889021578017666127538202605432461785535688985413178762831892142908984871996068495416445832547003749/18289769419552759458336855666287847802157649494712675392282977979547698100242594557480513626848185346929827687151654683463885958800007344892389159062437951057804960058230020044709212264187724952378893765275553472236199987151840287433858021620115388311126763755661964255764796339527524422060341210605205675204*y^32 + 155642536643926261434016935199871305977232135669352427383735622183726718050548862876136433558751023926501878088358285588320184984261385592353747200940061999968944217759156404022603644031367318935877506564182850467299246347932468456982533103797897896163233202512255572225179330999139825779979354676360351607065/4479127204788430887755964652968452522977383549725553157293790525603517902100227238566656398411800493125672086649384820440135336848981390585891222627535824748850194299974698786459398921841891825072382146598094727894579588690246601004210127743701727749663697246284562674881174613761842715606614174025764655152*y^31 - 308815682617916479520484935200234128125572272034701199953252351640857234726696138289568187111190659369684588911478122110168830746053022656676328344063214520605913475661326090449558643762210874546111955218784923154196339295499826079748973578795672382391156606343316806565955042979003804521083045421371059129741/36579538839105518916673711332575695604315298989425350784565955959095396200485189114961027253696370693859655374303309366927771917600014689784778318124875902115609920116460040089418424528375449904757787530551106944472399974303680574867716043240230776622253527511323928511529592679055048844120682421210411350408*y^30 - 5139624790323938154949381401361175602109109213367388636038693645434330847243416901463808341606077285702229421766709753475118496835488588482494466627628750337836236668474093300245733653268131353994831984384549250553556949192612241312599103404921322003914499326895370758620921015935944605095787659458700994552530/13717327064664569593752641749715885851618237121034506544212233484660773575181945918110385220136139010197370765363741012597914469100005508669291869296828463293353720043672515033531909198140793714284170323956665104177149990363880215575393516215086541233345072816746473191823597254645643316545255907953904256403*y^29 + 10549013331286395798951483955896041052595053433512480746510993748138651630560761790071488991203346355034476144181821121988100981036180507065830571081444379242618016299973309866206267086249202228521084998688377723125883250782097603152456649909558078422043223690660210326874723653733112913161355570759750412690731/18289769419552759458336855666287847802157649494712675392282977979547698100242594557480513626848185346929827687151654683463885958800007344892389159062437951057804960058230020044709212264187724952378893765275553472236199987151840287433858021620115388311126763755661964255764796339527524422060341210605205675204*y^28 + 162819311522497599994337323955529718341630394640409284391452964372220347989837933443223344445640294784816035731129735702973838369155229998706937560953578568477752332645769264904115459312254329354613661942662228482390381127814619143439594497243963590846051958947451177068791330431911242052626510074720987624863767/73159077678211037833347422665151391208630597978850701569131911918190792400970378229922054507392741387719310748606618733855543835200029379569556636249751804231219840232920080178836849056750899809515575061102213888944799948607361149735432086480461553244507055022647857023059185358110097688241364842420822700816*y^27 - 667773159330178981453061932319227169626913470915580786446662302374105218700550073712559501459026096074958029604509352504742672362731037450126247179422080920045659655315456241497046359517431165907968494745223189411009465630535089088670652421325001986131444761710975262897711507317119868581833680983252101770301305/109738616517316556750021133997727086812945896968276052353697867877286188601455567344883081761089112081578966122909928100783315752800044069354334954374627706346829760349380120268255273585126349714273362591653320833417199922911041724603148129720692329866760582533971785534588778037165146532362047263631234051224*y^26 - 379230769552793903481727427670179646750302590678123649818783556489786865187147425470534694673602503848725075430135559520693860763064291984833066186020914391959882473831138598210285361790271701171803606834692892121076787881231688418641922396533298659944666428011391649017990307753912872709498281625764846402498757/54869308258658278375010566998863543406472948484138026176848933938643094300727783672441540880544556040789483061454964050391657876400022034677167477187313853173414880174690060134127636792563174857136681295826660416708599961455520862301574064860346164933380291266985892767294389018582573266181023631815617025612*y^25 + 1903334715911478808973252716383718297368298955227467620652547307859445179644671293269636075600222359710572915929702020751718232712940119117642142593962355566800547998896621654452150200195056408075584904782057721458103491476997390067855298019620698340350189568859350382390130038191665466853223619483266114409377843/54869308258658278375010566998863543406472948484138026176848933938643094300727783672441540880544556040789483061454964050391657876400022034677167477187313853173414880174690060134127636792563174857136681295826660416708599961455520862301574064860346164933380291266985892767294389018582573266181023631815617025612*y^24 + 680983054941710449825087832444087626109103319003060599095828332830322718515442329986273246566627291378601210878988501272344723165419053977792014789527987300523383400495014422125195067121465181205374347654431713246906906825243191438974468648579176109546132098572505738728158128549656046940838638724788172586614513/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^23 - 8986257076156120220480903422875127706387684543513810789094317543043292172874771454565200627526227166434324825634847810670570288456510895066372495213167150868650369985517063136296484203009298675323854896238455811780798942193768720154362071058498413802246284572879800086520981554592824846120971208708686343447218349/73159077678211037833347422665151391208630597978850701569131911918190792400970378229922054507392741387719310748606618733855543835200029379569556636249751804231219840232920080178836849056750899809515575061102213888944799948607361149735432086480461553244507055022647857023059185358110097688241364842420822700816*y^22 + 2232400480063572141446585762259813691785429023740311868564182153778414961875620937932470435764400937934812793851980063443466091505322398794741587984574346904351284347201273470374009451045938481067210257142839807678629666710643240768972795929685664406187289242950358944468028856952474401012803728042186908413813543/36579538839105518916673711332575695604315298989425350784565955959095396200485189114961027253696370693859655374303309366927771917600014689784778318124875902115609920116460040089418424528375449904757787530551106944472399974303680574867716043240230776622253527511323928511529592679055048844120682421210411350408*y^21 + 60335754691187974931501623422423489744537050514087123826507125982578231197779144695910846961401020649572336444729183397110825165057688291788102954785496361453314709609919284886550494830010241138554846260991258338190650895258842451073057653204004451077865334545648002739800807978389064521109682202226584528156645879/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^20 - 1149479531897797546169180339148139128166256459414575719847603811648113467763965325895665539392592786465372204682899771246140273685739056611079990075095524956925457618285721285889421700756697566036349529751763406962148415422062634230715155545201169790742579976578326666835244481408004886466717944218446755278549336/4572442354888189864584213916571961950539412373678168848070744494886924525060648639370128406712046336732456921787913670865971489700001836223097289765609487764451240014557505011177303066046931238094723441318888368059049996787960071858464505405028847077781690938915491063941199084881881105515085302651301418801*y^19 - 41361595814624412560295524877420300727561202421808171908136655579431517112306113042016957956344721225936478477345852572353053549492659788102212085216552711674244061186096333288231525286586461653194594056612050070526765156725315436360392427012032581384114525315168881768888882578713257688250718964731047873807218701/109738616517316556750021133997727086812945896968276052353697867877286188601455567344883081761089112081578966122909928100783315752800044069354334954374627706346829760349380120268255273585126349714273362591653320833417199922911041724603148129720692329866760582533971785534588778037165146532362047263631234051224*y^18 + 109184115563377821922728422205507357648277799855991517669686379290167693321936815171881633567144409346807184142770238745006435711515811806163579037844322723658439874586138242399087449285987860374032368591987600515153530164473647247980790532530329567236151400437844025077954610774276793504246640264928763533804610525/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^17 + 2269790598943168478270469060582480662154057341189703917069700936521300218124230330033457006481626460845482070495260541435916220649937277766413080174864853933157592670081623240956522877268615327106341378439796709872482799495567806943971343976361950741519683348951486804749571643521347347055572620507467049339316943/7838472608379754053572938142694791915210421212019718025264133419806156328675397667491648697220650862969926151636423435770236839485717433525309639598187693310487840024955722876303948113223310693876668756546665773815514280207931551757367723551478023561911470180997984681042055574083224752311574804545088146516*y^16 - 5170665543910695302766210971333961411734981899642220619156862605020522555851707007263966271787038226537297920501873397679992233482642134162679053069012434228120489364532156673175113322068256887539782092519936289627099289812213351884117454668987090131450555197250285890325956843273706697495284470278679642190384377/9144884709776379729168427833143923901078824747356337696141488989773849050121297278740256813424092673464913843575827341731942979400003672446194579531218975528902480029115010022354606132093862476189446882637776736118099993575920143716929010810057694155563381877830982127882398169763762211030170605302602837602*y^15 - 19992059206147198528472395073160174488621230702369653527815759658078485154478675232290203027583184303044877234725199807369025105510045044188117139569386872402068238232582200875244317499767888468166557076907640639311443062956166344237093158384162801564740697586667339160508114278632638532200625508559552316417325081/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^14 + 27809703041360650070936971994122246133424365571967894890262231153107382807085368434332095105974192530306861919701105464577815809279054000572080123182784963628477041462444600657905440080639839521393126553008136673640987888597029889495814870145676824468849986751233726191131247234420501483592440837312738327426700751/73159077678211037833347422665151391208630597978850701569131911918190792400970378229922054507392741387719310748606618733855543835200029379569556636249751804231219840232920080178836849056750899809515575061102213888944799948607361149735432086480461553244507055022647857023059185358110097688241364842420822700816*y^13 - 200860125751486719769182575826464482502406625420916142517160435538028249419112760623885068507810387268484571210861487808210854443274920048098651796585056367332160800353395937773653123703788884842957066171708869911399740660811949849993499456041958082221041724994511565365551628174297173314310322316832159113885221/10451296811173005404763917523593055886947228282692957367018844559741541771567196889988864929627534483959901535515231247693649119314289911367079519464250257747317120033274297168405264150964414258502225008728887698420685706943908735676490298068637364749215293574663979574722740765444299669748766406060117528688*y^12 - 11111976272026651499183596811483076001163729763830444749264753971617758085263875302184094223274188477376981367217466822245811035183431026304340040539833785137313813581574348014669702356376599046032826554857524797291911536716692371862947066871194327340419599372799617628757416884281659730367097767242995564546990061/73159077678211037833347422665151391208630597978850701569131911918190792400970378229922054507392741387719310748606618733855543835200029379569556636249751804231219840232920080178836849056750899809515575061102213888944799948607361149735432086480461553244507055022647857023059185358110097688241364842420822700816*y^11 + 4559401315815548428474650380111147260380695100063083190109971574935605920038556641913771498012679162506941027306010127616744540039412833876501447976722271514919721081676028958194752698840123616838645938074458080480779021489633461922811324657477924243276882175142432904741299134520440068263004790524060576135307991/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^10 + 8287754066098152856530857151412533715366684727561543617371164832164222128493204512863071364867018909392765808936491311771514755148069635237883367010814729575107034573112889338237770851464690029100108924305370573924661707398330118575827779251724749337774006468811621963880257285964898555636796084487016924332414415/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^9 - 470330592688169525026784305027632671515787498970177471155510023116335182253943961648104003263624389327678451182625469147253453504979231275622162130502974767733615734546083010923199516811849189633855237472360175004332254585026939504132525413847477754193707951682977766765389056418032749701305321186034610751177649/109738616517316556750021133997727086812945896968276052353697867877286188601455567344883081761089112081578966122909928100783315752800044069354334954374627706346829760349380120268255273585126349714273362591653320833417199922911041724603148129720692329866760582533971785534588778037165146532362047263631234051224*y^8 - 210414111153484525999362359420813830652717551624236750711157590017951965047638159937139437697001344775603033027116861534737727153277929858661415236667680709076027760993814380589584621730151786643284140509202444523762931988778746252080386594115820919527370718053789069718401661091836892922242034059563020749145973/31353890433519016214291752570779167660841684848078872101056533679224625314701590669966594788882603451879704606545693743080947357942869734101238558392750773241951360099822891505215792452893242775506675026186663095262057120831726207029470894205912094247645880723991938724168222296332899009246299218180352586064*y^7 - 7169444973610869430062317421691194043086059945350413484557989841712956452708136417256694315371581011212110164031310866168691835572743982215892484554919082732304792218079715948607442037767223245939838761965463477840059667820965735326888092122019334259991141175924323232043445974592564965187470054021659713080855/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^6 + 89885948457066603476419248899059125206716409796225843000026649852490733394625019490655608577791967300166182476407629823530287000279510834152870385655954419781880928976161416187034259926189853759150600115565829325675930899462418439670942982281399319047605602067008493057318953300519880960020204430287254985018817/109738616517316556750021133997727086812945896968276052353697867877286188601455567344883081761089112081578966122909928100783315752800044069354334954374627706346829760349380120268255273585126349714273362591653320833417199922911041724603148129720692329866760582533971785534588778037165146532362047263631234051224*y^5 + 11292369914272122126708029196621225981752899594919044913768327297831498241025553141653288576847648508019339102585935621025784804286115261203919336937319750626549427779629791151401918052772375482139465114316351215481850419165155670557103268559399113692789256669619509390985460233469826665645715957928577715108643/109738616517316556750021133997727086812945896968276052353697867877286188601455567344883081761089112081578966122909928100783315752800044069354334954374627706346829760349380120268255273585126349714273362591653320833417199922911041724603148129720692329866760582533971785534588778037165146532362047263631234051224*y^4 - 5194372306704169418968171411315556514722110215345776600044726128747136011884831986664489141472704294562828467498969006534302247346038113566233235970565373274223661348537373524934072256679481196147804843234279684656491060305376173672489183241035739357648692100053130500741036167172733758390069062993396610568767/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y^3 - 480098939624355478742775087154824359056140729877425678157115374708568001613694992731865877656000446267793858505820452432803792063337324046616284723588865107610514506203623014585294906683019520987800506657565700008611367930986213199098939766780377614325200684610191623544973646762505079408304559232285506264049/73159077678211037833347422665151391208630597978850701569131911918190792400970378229922054507392741387719310748606618733855543835200029379569556636249751804231219840232920080178836849056750899809515575061102213888944799948607361149735432086480461553244507055022647857023059185358110097688241364842420822700816*y^2 - 4815774505421955211660834038486506030343420243103904508010054981557901261925777560835742265294064947757985451329978299322818797302711932979653548530310728283389878213954805691774065839777641417104602925181391155919125186789871883932608348726497715746904635384819609914617933277495957506778412988097087868983/219477233034633113500042267995454173625891793936552104707395735754572377202911134689766163522178224163157932245819856201566631505600088138708669908749255412693659520698760240536510547170252699428546725183306641666834399845822083449206296259441384659733521165067943571069177556074330293064724094527262468102448*y + 514171586929737217438465111022948190058518948360735921391452921969088514946222775299835480958430252627060845001046448825979795593809242410694386613786778878381711160098240307827750214078149726822128643134958785485390803098848164385453390770370591578493030769476367324166888785385689451600555153278082639767/15676945216759508107145876285389583830420842424039436050528266839612312657350795334983297394441301725939852303272846871540473678971434867050619279196375386620975680049911445752607896226446621387753337513093331547631028560415863103514735447102956047123822940361995969362084111148166449504623149609090176293032

# 3 Loop Invariant
68839039007955742418520392944579537589714540181639515716579653787062832652171365388493668202324964993790914131032879917321447892196016704291183158893296088108899043440576101046952310120050724268264938052907987691306471375379502624264886183003645166384737933339223720048670435539160045646616660929946685718743076684054002638880526238970149889591057732383794667997682516517173/273853634985961571385968378840588842562132113837062324323676895630101881276580155431192322684505159492178022474939132159119508869456174823674852587928939675359935866885034394605587930521068361316945702796079555900872315235376038758564911418278186287937363941657430440147568617414033803866494444274394881701184205497695043528217759062985870108842879486518691131369215859839600880*y^37 - 48304176869338263412651003461496858590378808870202025972573122405801409529679857428224976064517424612915012181081239162306568328320097833474421780726574913619032767317774890389508248586659526065328862065000679844949422513507663311073694713139223080409753599735184642184557630942493839415080686619530964183114382965629126556919618951674589133310585776459447056851763675691504399/7667901779606923998807114607536487591739699187437745081062953077642852675744244352073385035166144465780984629298295700455346248344772895062895872462010310910078204272780963048956462054589914116874479678290227565224424826590529085239817519711789216062246190366408052324131921287592946508261844439683056687633157753935461218790097253763604363047600625622523351678338044075508824640*y^36 + 64120440817235714136350770850688118102892041666652895753743565869085387393840298951211262153932473541275828794361787774520102916245393684885069877827510861221010143921450915446245401644541231378614774674210486053297997168282093189653054249838454586144304509244832035899319871145809485478606711478125366993861885030868485686504649620820104516268370729971521817688775716255118667/3833950889803461999403557303768243795869849593718872540531476538821426337872122176036692517583072232890492314649147850227673124172386447531447936231005155455039102136390481524478231027294957058437239839145113782612212413295264542619908759855894608031123095183204026162065960643796473254130922219841528343816578876967730609395048626881802181523800312811261675839169022037754412320*y^35 + 1813069151674762809286346697626357124332676832575831854655010115800479553500147023486165584883699465560833881932703983790634362724801678393323008606666455310852514072061113824929038537733907891448368368823502920329255001322503298515334078866920288654212588160233060446308283468006218984356966078052569164534171216355894031537326808432364957762593581358800801101901013251951872411/7667901779606923998807114607536487591739699187437745081062953077642852675744244352073385035166144465780984629298295700455346248344772895062895872462010310910078204272780963048956462054589914116874479678290227565224424826590529085239817519711789216062246190366408052324131921287592946508261844439683056687633157753935461218790097253763604363047600625622523351678338044075508824640*y^34 - 1043535741895181802886852621096460288834078288252905693831923544376780950127953895707464637618322599539201833087766843410692692960600991181969546953557985743719167877204241674965009419981736540398580678945001153978679259153448609773783930558481005762519772109400787284911240727934938174117770579274839595490801510083670913525524799365635902003629880246875288692988352439267320647/958487722450865499850889325942060948967462398429718135132869134705356584468030544009173129395768058222623078662286962556918281043096611882861984057751288863759775534097620381119557756823739264609309959786278445653053103323816135654977189963973652007780773795801006540516490160949118313532730554960382085954144719241932652348762156720450545380950078202815418959792255509438603080*y^33 - 5826329367340539767887152769353804640956572106919673336418060055612300337727650872039154952756511794328100731423180886829822331870214053973906660293758300884555751423565403855559921162919548679455606595838869795777173702238505085842030582587198740664593169506417009403995547274091037361639605724113036903031659349779708744233924780740527616139864537761989443858159881513013790487/1916975444901730999701778651884121897934924796859436270265738269410713168936061088018346258791536116445246157324573925113836562086193223765723968115502577727519551068195240762239115513647478529218619919572556891306106206647632271309954379927947304015561547591602013081032980321898236627065461109920764171908289438483865304697524313440901090761900156405630837919584511018877206160*y^32 + 12008602063933279752491473308918330585985706174415235943550289703627765033855413587396183745186149012649522355373333010539198196995772905298975480182004593014787504419829947262345239347703753020198253089931061123901316958175162452676158756576277249343618362559973077406417077430388682999268058323532460004377452499506079189200021494273057087315346750256413497768655006276976224037/479243861225432749925444662971030474483731199214859067566434567352678292234015272004586564697884029111311539331143481278459140521548305941430992028875644431879887767048810190559778878411869632304654979893139222826526551661908067827488594981986826003890386897900503270258245080474559156766365277480191042977072359620966326174381078360225272690475039101407709479896127754719301540*y^31 - 2593771282191120271396771717125919573470383847942492358156500601246787269630075801116782616197912672171554117509594263581056506949719313343219091810366623528262326603653567139542805356956804728379321075256965553908792575283427116143894600500685651041841836272837711835032171690271618814252617622720670995360212069189882763747029084199529836936792444544743837672363496092741332203/2555967259868974666269038202512162530579899729145915027020984359214284225248081450691128345055381488593661543099431900151782082781590965020965290820670103636692734757593654349652154018196638038958159892763409188408141608863509695079939173237263072020748730122136017441377307095864315502753948146561018895877719251311820406263365751254534787682533541874174450559446014691836274880*y^30 - 425389532584430420432079725297472967355851553032510402125719826006300272615507414723668881764844217899192847424894370241914659006895426570413412993908956101095833498250862230739770732457658469480273215927256821828155460680388709475959574319638284654300101846281020671029121765622631346247839823812005047558218270226374607556320247229354351391509481928398044507325163223468293899917/1533580355921384799761422921507297518347939837487549016212590615528570535148848870414677007033228893156196925859659140091069249668954579012579174492402062182015640854556192609791292410917982823374895935658045513044884965318105817047963503942357843212449238073281610464826384257518589301652368887936611337526631550787092243758019450752720872609520125124504670335667608815101764928*y^29 + 471141966750144058880777549136246287943922643453419925999619094757325241577189986492118957757723566076589752660665908239982395664034044139944290339935960866094923864735180147485402622744894555235471151588775622188946143844089464196869363413689630939332653998204514986118487658890449292102601103675623365238918600905718288547884012067986816504296531560624923868824273533409588992499/1277983629934487333134519101256081265289949864572957513510492179607142112624040725345564172527690744296830771549715950075891041390795482510482645410335051818346367378796827174826077009098319019479079946381704594204070804431754847539969586618631536010374365061068008720688653547932157751376974073280509447938859625655910203131682875627267393841266770937087225279723007345918137440*y^28 + 1889519485981862849988204695911052882390473180476495329922102983773831725017811036723276865011704455052848965579386340452646351196884658233006843311057091674808558136078624415224793681822920308217613236834540085417614337302098564708276307881781419642327205027307233167893037755117586514786321172603958633630281532911742913482731279134027940637328506188342768718210797173982865752083/1095414539943846285543873515362355370248528455348249297294707582520407525106320621724769290738020637968712089899756528636478035477824699294699410351715758701439743467540137578422351722084273445267782811184318223603489260941504155034259645673112745151749455766629721760590274469656135215465977777097579526804736821990780174112871036251943480435371517946074764525476863439358403520*y^27 - 31768189214218030489303417173414745104612217945848072742213098657523552929413968123647696827428586416900358035712499944627240109458379605206797266673060296656197363084065807651635149436303490492073827329031945031299442238998031330125810842502710285498450321409369195639923351012945890816442367647267724577302266687766069928584188987952481957158780348739719721195812350320671280338467/7667901779606923998807114607536487591739699187437745081062953077642852675744244352073385035166144465780984629298295700455346248344772895062895872462010310910078204272780963048956462054589914116874479678290227565224424826590529085239817519711789216062246190366408052324131921287592946508261844439683056687633157753935461218790097253763604363047600625622523351678338044075508824640*y^26 - 6567185951809086103147322533864407954973311994912957920750959917629596974616914423431350370163219714835432931149680836449264137221886360836802776552808097992332493648430176875309220365674192238200237841098131060877563854159598788155847511916687856508930280871906418911900459660286217143078470048301700940419754018014347873705045750955891857186023740986729240096929209162227422044887/1095414539943846285543873515362355370248528455348249297294707582520407525106320621724769290738020637968712089899756528636478035477824699294699410351715758701439743467540137578422351722084273445267782811184318223603489260941504155034259645673112745151749455766629721760590274469656135215465977777097579526804736821990780174112871036251943480435371517946074764525476863439358403520*y^25 + 187424242459664251993965634071781927862045726653683529509640814649427837569947405268459482139853428701110764076695644624481060347993401758157953137020004157303454851242494963824329394963687494888008864324263616343786780891295103763403743558361597733895776970173473551106898386094215429515433565473816857415867791831211436677697579998785390163331494488838408503935294972353871278468409/7667901779606923998807114607536487591739699187437745081062953077642852675744244352073385035166144465780984629298295700455346248344772895062895872462010310910078204272780963048956462054589914116874479678290227565224424826590529085239817519711789216062246190366408052324131921287592946508261844439683056687633157753935461218790097253763604363047600625622523351678338044075508824640*y^24 + 14361970071293784119901453327959540997332336730185471309789830428050148069114187199875861345890117936452370108813694380433604359285698125438772980244974888269744220307011447439565609590431195104874716493002923699047536920308340661144677475796696739855089363326424962656825155244922235364344390989949638126452415595580737206297805664655865344270352158034706104057700307431436591947343/1916975444901730999701778651884121897934924796859436270265738269410713168936061088018346258791536116445246157324573925113836562086193223765723968115502577727519551068195240762239115513647478529218619919572556891306106206647632271309954379927947304015561547591602013081032980321898236627065461109920764171908289438483865304697524313440901090761900156405630837919584511018877206160*y^23 - 114451893333276721160508076282268744761562179671111108253159553020005826034104491087715197052907875720739195060916217168759432598367082424735093501793131779632210707711543295492802505031982681496559856982385036409167476404275967593701280035430186179150305704179329462635157358072538773266920881836643145607462659924943442092322595802112329105538240132308621849089450001923304462380293/1277983629934487333134519101256081265289949864572957513510492179607142112624040725345564172527690744296830771549715950075891041390795482510482645410335051818346367378796827174826077009098319019479079946381704594204070804431754847539969586618631536010374365061068008720688653547932157751376974073280509447938859625655910203131682875627267393841266770937087225279723007345918137440*y^22 + 100329525455293966923481408908413356073032480169042775915273348730731981389632379415876577119379162240215022994952248020001418633653875150380245325496174109751495242725028793908121216206365920142839076295596222094997179855509741941176267509754562303858134561334320770118832720164476077249422487373974565626171962928586278886889199356518644747240250495176252622296063210800908365238027/3833950889803461999403557303768243795869849593718872540531476538821426337872122176036692517583072232890492314649147850227673124172386447531447936231005155455039102136390481524478231027294957058437239839145113782612212413295264542619908759855894608031123095183204026162065960643796473254130922219841528343816578876967730609395048626881802181523800312811261675839169022037754412320*y^21 + 321994352728459352354176557330652254762262824230342873675722412389681087178169980429345222746575021345736258969276462284857395475258337485770662097456633112087376677126908730410928835966714505481140464321614688355223336119957573201173084317738133266030570700383797695039734889641108225170728708702288259337553117329007218939238248781496567726818262138568810411115464879004765165128081/1533580355921384799761422921507297518347939837487549016212590615528570535148848870414677007033228893156196925859659140091069249668954579012579174492402062182015640854556192609791292410917982823374895935658045513044884965318105817047963503942357843212449238073281610464826384257518589301652368887936611337526631550787092243758019450752720872609520125124504670335667608815101764928*y^20 - 45279306880869589720793431956633061947238265795139053126084834777968018119557188193748557202012429240907972960524260140938095485632333913770957397144932277819517189453877382268143492502425520231237628068640236629635732626192349281286176097047463755520832935620884493203108358658816957908026299524339963204295064829696949281006602643060859741644371616265471999246312815593335939617057/319495907483621833283629775314020316322487466143239378377623044901785528156010181336391043131922686074207692887428987518972760347698870627620661352583762954586591844699206793706519252274579754869769986595426148551017701107938711884992396654657884002593591265267002180172163386983039437844243518320127361984714906413977550782920718906816848460316692734271806319930751836479534360*y^19 - 2389070709983734050824598465682753936444534147845079224392361845091416385117357793703716746589981686086239162875208353151978045573378350395842783841368973895347176879058777657646208588052942374274016591735673819975320749678620072259625368629399336253192108946990491808023395764114152127966194593968066208570245283776972109299515783354849036941127308218675319275372667077594520923714559/7667901779606923998807114607536487591739699187437745081062953077642852675744244352073385035166144465780984629298295700455346248344772895062895872462010310910078204272780963048956462054589914116874479678290227565224424826590529085239817519711789216062246190366408052324131921287592946508261844439683056687633157753935461218790097253763604363047600625622523351678338044075508824640*y^18 + 2323623074562574464323669398099718238184979247739381692963808098056089259175574893010457944726846344497909117094357953623900854297282726017751619440736042345420702487306787488870675279734809036391379281121595068644132065514409235073367527467085752614724899359014054086116864290822752958280803905439825349052550488370484472702189239293054873377877246326519127924432726801167552631892421/7667901779606923998807114607536487591739699187437745081062953077642852675744244352073385035166144465780984629298295700455346248344772895062895872462010310910078204272780963048956462054589914116874479678290227565224424826590529085239817519711789216062246190366408052324131921287592946508261844439683056687633157753935461218790097253763604363047600625622523351678338044075508824640*y^17 + 542720530299612957703396291581743564471411932752439196767228432207209447281630158217264310837622149868882177053453858554855548504197350263309504598026344162203127335234959834956821497352995534319359153052910387349289133910099295621799258788965022395221068381335689254195092909932942771393043285134367908883373322882762792964644975178738945084944621825982041902813758019358176515688713/1916975444901730999701778651884121897934924796859436270265738269410713168936061088018346258791536116445246157324573925113836562086193223765723968115502577727519551068195240762239115513647478529218619919572556891306106206647632271309954379927947304015561547591602013081032980321898236627065461109920764171908289438483865304697524313440901090761900156405630837919584511018877206160*y^16 - 57601277117495857198461282977574869368794469311723281913653401590560828321537238294445752340572822445485473693217401892432352376582956323811712768298442649814275349510298164433785568685055235211003621149532726485808686025424475638101080971232586479985351078616186025922183763003100759847936879351347691503762855522828632725868393572693931905643131544871315780219511739645536609760557/159747953741810916641814887657010158161243733071619689188811522450892764078005090668195521565961343037103846443714493759486380173849435313810330676291881477293295922349603396853259626137289877434884993297713074275508850553969355942496198327328942001296795632633501090086081693491519718922121759160063680992357453206988775391460359453408424230158346367135903159965375918239767180*y^15 - 2042137041556377848974473743925778906133631317444873457434216448888291415466106161559910520028840361539156097319615091048393446328000762971655808639690955381631057450133579237383919864566648069094507829105767939061103723004251466062054388715087043830082624987107157790182512544385411959566907612892551986592805940067815762476994081262194172617733531538841843397546229937195813095093/13692681749298078569298418942029442128106605691853116216183844781505094063829007771559616134225257974608901123746956607955975443472808741183742629396446983767996793344251719730279396526053418065847285139803977795043615761768801937928245570913909314396868197082871522007378430870701690193324722213719744085059210274884752176410887953149293505442143974325934556568460792991980044*y^14 + 645624265311785930694663160537702250071879708695998649043205399539856875502807204259300034178900854465969083116897645684422683289816541453910958373379346988996924223553172552505995658525022306146415676306552792929778184559277978153936375244439087017409218568893269911506523000995510021567880615015810010351882864444315060964042614276550937228312935879449666271316907122448283617988683/2555967259868974666269038202512162530579899729145915027020984359214284225248081450691128345055381488593661543099431900151782082781590965020965290820670103636692734757593654349652154018196638038958159892763409188408141608863509695079939173237263072020748730122136017441377307095864315502753948146561018895877719251311820406263365751254534787682533541874174450559446014691836274880*y^13 + 110592471015462660662527043621100370818553463739047584978367921597101260277919057319845204224193645262698147727254953740115241249061844957730141473941990564933233895091071016416170313603960870943270588602144099361784401281403199772279416142024713850198403482150004921096805476879916849401092243247420768666425622335234555948455910337348993315401760762563200890259570152702440975941671/2555967259868974666269038202512162530579899729145915027020984359214284225248081450691128345055381488593661543099431900151782082781590965020965290820670103636692734757593654349652154018196638038958159892763409188408141608863509695079939173237263072020748730122136017441377307095864315502753948146561018895877719251311820406263365751254534787682533541874174450559446014691836274880*y^12 - 161924006746313336946953764637066778376503205079125702339171818343017595978319274665310089953312407312264033585780818357916555478947494093387693463402121506593493359702179412304113565360743276840810735000277412334757701994499739393034307083975943090934654956552765847212051634389291323749685160043780737506421185614632931202909979840947950302762485790844625008189174014507643516367197/1533580355921384799761422921507297518347939837487549016212590615528570535148848870414677007033228893156196925859659140091069249668954579012579174492402062182015640854556192609791292410917982823374895935658045513044884965318105817047963503942357843212449238073281610464826384257518589301652368887936611337526631550787092243758019450752720872609520125124504670335667608815101764928*y^11 - 4859892510823406680348685990232981903721405280988475738737967462929003852447421131629518018723279726258553284000344774050197229149974391672943122446591389102909899241423649862716884545706142368467460840669611494588162270722572379183760116508502917895342787530799162563024585783390166186512456239034906283096967079007669166072754099539852045967005509525054001739925848350914287271809/547707269971923142771936757681177685124264227674124648647353791260203762553160310862384645369010318984356044949878264318239017738912349647349705175857879350719871733770068789211175861042136722633891405592159111801744630470752077517129822836556372575874727883314860880295137234828067607732988888548789763402368410995390087056435518125971740217685758973037382262738431719679201760*y^10 + 144989761849681642248053966205302048990715038304684712449810580694621857027478713812230273138491265662787582927182010272903604533741230086749798566867493475379389770734200313608956364612359840770305435291786678658541543863477589717887031953523527016851482575016675996508881754132361916360330765619526507471018136759723342115804030448574923501784645641355342575868696645112462712753/5324931791393697221393829588567005272041457769053989639627050748363092135933503022273184052198711434570128214790483125316212672461647843793677689209729382576443197411653446561775320871242995914496166443257102475850295018465645198083206610910964733376559854421116703002869389783050657297404058638668789366411915106899625846382011981780280807671944878904530105332179197274658906*y^9 + 1155865988043135224863658937776862300153322965498668762736803289703355218306686702091489800966822089024660909012451255635519874479578283012692569220310267077927609019028455381544146426737377507001588128161680158414456316466535846867963847992340234803792785676485419267659777981105972468635934155379795452604636167112334491529707532597408769043856698876535415470731514202594777793793/365138179981282095181291171787451790082842818449416432431569194173469175035440207241589763579340212656237363299918842878826011825941566431566470117238586233813247822513379192807450574028091148422594270394772741201163086980501385011419881891037581717249818588876573920196758156552045071821992592365859842268245607330260058037623678750647826811790505982024921508492287813119467840*y^8 - 11864506945974143438677193756722033004658192798266939073353504279142115229678552097174727939354469900855624690125453667186952874210472243395044596172910529505422214336063059456360756506807230877948858098618120998265126481177319653976868255773581583327993746003284272265309630222306081044135918087622515452452520491911813183604904936268820486489902941922805102655797726707531621610343/2555967259868974666269038202512162530579899729145915027020984359214284225248081450691128345055381488593661543099431900151782082781590965020965290820670103636692734757593654349652154018196638038958159892763409188408141608863509695079939173237263072020748730122136017441377307095864315502753948146561018895877719251311820406263365751254534787682533541874174450559446014691836274880*y^7 - 2165108352879675976942594614869428783130810497154811546919530049669491828327791530146254022243398672185306565177768731035086682575406872147200648082733853794681022468919792994935981316510205913699836801828593398561425718607272568078975008283019038935112157079076363798069756085663510153065256044352246323961649339625197367446937448914121207492876234321477601225905201720043169627229/1916975444901730999701778651884121897934924796859436270265738269410713168936061088018346258791536116445246157324573925113836562086193223765723968115502577727519551068195240762239115513647478529218619919572556891306106206647632271309954379927947304015561547591602013081032980321898236627065461109920764171908289438483865304697524313440901090761900156405630837919584511018877206160*y^6 + 542220234992127781901085269809819274549006638511897104960275310170056156210547797627087093681355005554387396397062929649713156203320551746261461719880699574820889078414979522113016545074602011593806904587563332932319479475924087023391204186934075981833905881167474523526452477352695124824065699170442570573745027167459525417016341478547288173391596670439937976935799577915845354989/1277983629934487333134519101256081265289949864572957513510492179607142112624040725345564172527690744296830771549715950075891041390795482510482645410335051818346367378796827174826077009098319019479079946381704594204070804431754847539969586618631536010374365061068008720688653547932157751376974073280509447938859625655910203131682875627267393841266770937087225279723007345918137440*y^5 + 144061027110410678221812930104188128117798598513619805557105200135317604350709752348145271471765089731350418923215974054359356385330977884555740682650949116391439071329165054937277033406530620213628946279694278046589870651799905995992028049175598712545573568887595638457707259800515200033668657058279907877595187592415163556470956536182279767099234215894087214600651024676358257087/766790177960692399880711460753648759173969918743774508106295307764285267574424435207338503516614446578098462929829570045534624834477289506289587246201031091007820427278096304895646205458991411687447967829022756522442482659052908523981751971178921606224619036640805232413192128759294650826184443968305668763315775393546121879009725376360436304760062562252335167833804407550882464*y^4 + 19667672683155129402455565712535521958815103282193817477692315958384232880661594456466462085453088632156104656332749546651018139188487210595732206803564191139785781210400408120854823754959868254984791330527917371478833370394512294511192065925899536454947963329457827174115655953049547324747892673318834627751702360356508702274904614121108427123136736903679381943845984407083681377/1095414539943846285543873515362355370248528455348249297294707582520407525106320621724769290738020637968712089899756528636478035477824699294699410351715758701439743467540137578422351722084273445267782811184318223603489260941504155034259645673112745151749455766629721760590274469656135215465977777097579526804736821990780174112871036251943480435371517946074764525476863439358403520*y^3 - 1870998428760494755007104352511029706727953433872724528290493173646198472728141480551126997778210836625810317221814140170013268812433134968410465432425132446684601264558425216248105698180661654355703108754105029147866975150570316583148292998287053472318697932342277775638060574577479387483788103601284607449339090270467200739960869655217652927709225672984905811612794944105513491/511193451973794933253807640502432506115979945829183005404196871842856845049616290138225669011076297718732308619886380030356416556318193004193058164134020727338546951518730869930430803639327607791631978552681837681628321772701939015987834647452614404149746024427203488275461419172863100550789629312203779175543850262364081252673150250906957536506708374834890111889202938367254976*y^2 - 1802653716344560819032674760411590960222430073709994131625514055959075651876684066485889729500423553392513266306244608872260909130863082399699327853645050968761833230064471774893823169127549738882497634079618461271095833911999937273962565649521186986725706495274398147490392795740497023168575570715751278554526647303983053822152575917564287315947118004773038895521945073839250637/2555967259868974666269038202512162530579899729145915027020984359214284225248081450691128345055381488593661543099431900151782082781590965020965290820670103636692734757593654349652154018196638038958159892763409188408141608863509695079939173237263072020748730122136017441377307095864315502753948146561018895877719251311820406263365751254534787682533541874174450559446014691836274880*y - 9687552285781629505548903291619984422409837217716928224651600890037786304248090327457508580586923484955288433668879854951553064433140808780567938841323299405978085470290934945275952459352670410722431736616859174161813021889437931733104963462072629214748338231786839114634330753012796866462638303557772525508277207978889382706555424509444306809066483169912684284019746957090761/547707269971923142771936757681177685124264227674124648647353791260203762553160310862384645369010318984356044949878264318239017738912349647349705175857879350719871733770068789211175861042136722633891405592159111801744630470752077517129822836556372575874727883314860880295137234828067607732988888548789763402368410995390087056435518125971740217685758973037382262738431719679201760

# 4 Loop Invariant
104246732016134870448141115126906668720774242376963339250800036664037276031095777691921121157698334161444374491877575710891415291010822175706165867094611150095966068595642805667513570011512560662590025337990810023939712374431828918599530849687733286628066187074873241420630029019869216576444460573187366605783289218707818362676487721128373023214689646885243714625701404113955801608617656963072894142656644690442861439100937515030252993123975724729957175639503238943714961136419395010161391638863701140476787674311033/623963825283337786516287043836542625489847104130965069857391999256798128197102350546361807082017585682301969641097199831370289305169068134372057827167515300609097036426339836570582127554414100067637796038904978417659248130361179627916475961963788225062951714145083099577473874200712147414801720171436501474698397012110846531144864227784616208776453665658570252864555695419672677812779782168148600453087317315907547591616957247179486880941339988672581139576166411649383626840842666776730509993082045607633089560112102400*y^37 - 1296341755850276898921905889105573648203417915326926942351142517286136931155384742133631558753469410560731290748881493644194815267310217344173342842491187327689770758134563334235571733917234605645829160775040103696362914451120229209752917817526012610975688944582072081903335248314514254298819514287336984067782263477294875067756759896026160240377332982376166879438246165274436933188982220362577547775938170642069150224636294539121923496777991025556375917898614093792656070943889188383391545212161896091649946887506009/311981912641668893258143521918271312744923552065482534928695999628399064098551175273180903541008792841150984820548599915685144652584534067186028913583757650304548518213169918285291063777207050033818898019452489208829624065180589813958237980981894112531475857072541549788736937100356073707400860085718250737349198506055423265572432113892308104388226832829285126432277847709836338906389891084074300226543658657953773795808478623589743440470669994336290569788083205824691813420421333388365254996541022803816544780056051200*y^36 + 6437352190480992943029626676456812204028770689393497633848323749151074442074400198062370137166329422632756335787324922160626329944887763130272627257532750255706107216071480851120016752619267791754924195535622641949865739778136410714308790498594965090871913498391005187390538539461552662023224756621749418024983019311530143533216171671747978862699314941998975178184206491551303022269367646153482019984767791943908615050248277011640863407383038656816383058071356114805823207343881614076814831727068270137881268453575513/623963825283337786516287043836542625489847104130965069857391999256798128197102350546361807082017585682301969641097199831370289305169068134372057827167515300609097036426339836570582127554414100067637796038904978417659248130361179627916475961963788225062951714145083099577473874200712147414801720171436501474698397012110846531144864227784616208776453665658570252864555695419672677812779782168148600453087317315907547591616957247179486880941339988672581139576166411649383626840842666776730509993082045607633089560112102400*y^35 + 6214311121388059088356685061966249093108236874923334439596851669692923964149198062895551610941755735036027542132943824067496590209745378652410845053708560687465232204200820838091062892532632110864999658508831444267624674994742080187321186517632036141769728313959657757059504976444237103940466194048756254504236902168609882968285194220249880559573025508305645068650709539556394452622866204016705250101426980953998228136840698223191438810077433167957370137285889070358394701404331515129333974656001599916362969690527787/38997739080208611657267940239783914093115444008185316866086999953549883012318896909147612942626099105143873102568574989460643081573066758398253614197969706288068564776646239785661382972150881254227362252431561151103703008147573726744779747622736764066434482134067693723592117137544509213425107510714781342168649813256927908196554014236538513048528354103660640804034730963729542363298736385509287528317957332244221724476059827948717930058833749292036321223510400728086476677552666673545656874567627850477068097507006400*y^34 - 61859731530292132590318953799355556549817483058906782400266341651635300449477526807013935131330913915922906509148130151503950780385116833996851057540619538611120817171951595586606668808564848147846040916024274265344862608448033681600207380754216044580409993730356572636535091101285576492498557329164875250266875493407471688013193489472142441091005594811398686944721460669025646114837950651203183818231979634844182539724219426293863373906403735396465408942261751823396615909346920764583694443796765361572991802585249251/89137689326191112359469577690934660784263872018709295693913142750971161171014621506623115297431083668900281377299599975910041329309866876338865403881073614372728148060905690938654589650630585723948256576986425488237035447194454232559496565994826889294707387735011871368210553457244592487828817167348071639242628144587263790163552032540659458396636237951224321837793670774238953973254254595449800064726759616558221084516708178168498125848762855524654448510880915949911946691548952396675787141868863658233298508587443200*y^33 - 674108085793482441374998905850505303276840203902720070904663216371875673134770766085144358812794618821667640218631329761893072828962086381029507309980359031103488727062767746588207320128582908664893642152742315280638271869906394987273871455427161117969714350097355383787953283594421542409190049823585117395480413193085915346415135435735192799357218031708037869445300862927766954827422986983082690877994655883231821648707350572610369795889585290941653397816900012445635621492968998840042149942029000179089856933724640573/311981912641668893258143521918271312744923552065482534928695999628399064098551175273180903541008792841150984820548599915685144652584534067186028913583757650304548518213169918285291063777207050033818898019452489208829624065180589813958237980981894112531475857072541549788736937100356073707400860085718250737349198506055423265572432113892308104388226832829285126432277847709836338906389891084074300226543658657953773795808478623589743440470669994336290569788083205824691813420421333388365254996541022803816544780056051200*y^32 + 1451587084929932550273498468282957301350652238391195891882913885978099889397314564341543433337414511940777281301437018947936882735545181988646314004201120256225665013546807646590102908797368760091181578176353188563678966835409635057323579101657709661180360675661043462717951108689469617542338352335007372685586254404832594593571037300572442899598641378481001128276410183836523366549819157531642609633787779597530501460831608378916520296201901057766763561399721953876599950623038822181508220716543136534481206191749291037/89137689326191112359469577690934660784263872018709295693913142750971161171014621506623115297431083668900281377299599975910041329309866876338865403881073614372728148060905690938654589650630585723948256576986425488237035447194454232559496565994826889294707387735011871368210553457244592487828817167348071639242628144587263790163552032540659458396636237951224321837793670774238953973254254595449800064726759616558221084516708178168498125848762855524654448510880915949911946691548952396675787141868863658233298508587443200*y^31 + 526353260798334619459438239754850945291319773822728068479272061919411402068799269209661793379779539751911147138187210331824588903138824196750734528728086875034133229409837271754700274930898735485476621636198327097123249214954672328868667142764258486828523457260847906249354442756208908616568906304945943023042147076734733698412248949196562538638794844365160413136452039126917372263294683563584229553024510732845399111350955961830927202567462811359944425571462509676381080771064226972608393537831870183891415737392428189/207987941761112595505429014612180875163282368043655023285797333085599376065700783515453935694005861894100656547032399943790096435056356044790685942389171766869699012142113278856860709184804700022545932012968326139219749376787059875972158653987929408354317238048361033192491291400237382471600573390478833824899465670703615510381621409261538736258817888552856750954851898473224225937593260722716200151029105771969182530538985749059828960313779996224193713192055470549794542280280888925576836664360681869211029853370700800*y^30 - 23064034351248297032062746400331902233668886035148528117160289916410540639303378373195547645024126314341545612656125140891269839742255961486238319438421113743631854696065334844313529091785876639364728974555662293328182197755146973265526485406679548605811321931719494305506355249797346619844813153514742626822955150087836225134042065404039302073068068244026871657533142255942856628587523837746154764304613946819210884215561663531615668269956488516114714947304108166683428370428897734486022111245893431140094270253621281533/124792765056667557303257408767308525097969420826193013971478399851359625639420470109272361416403517136460393928219439966274057861033813626874411565433503060121819407285267967314116425510882820013527559207780995683531849626072235925583295192392757645012590342829016619915494774840142429482960344034287300294939679402422169306228972845556923241755290733131714050572911139083934535562555956433629720090617463463181509518323391449435897376188267997734516227915233282329876725368168533355346101998616409121526617912022420480*y^29 + 43678113973317105200986730182118175151507212642582038896978577975763841809363624991055825903133712537009499248565499095896465616618434534272008463055120823382896240704850002706064775166205960528893901413619137170767696469699585090546199242249497735241084343769060817260442350230597561758964023573449904214948471564662137059460765155864598584465168942688682172465984100335594839623017541087746369838537984383692912868580963369754653586686254737880029647074723645221465598388157311729180950801306421109990849219708666104941/207987941761112595505429014612180875163282368043655023285797333085599376065700783515453935694005861894100656547032399943790096435056356044790685942389171766869699012142113278856860709184804700022545932012968326139219749376787059875972158653987929408354317238048361033192491291400237382471600573390478833824899465670703615510381621409261538736258817888552856750954851898473224225937593260722716200151029105771969182530538985749059828960313779996224193713192055470549794542280280888925576836664360681869211029853370700800*y^28 + 373331311199048650961011883648928275189068807217736104134033850832217797534168668520755865651233993168229385540308848930189095008723066355014791676470141033816731944909509364727635204038198247264567285920066658660243999990606738699266424585097695134116823377113689979178753057167211933634464553868777395507153017280385438875310024507682075433499348728167595982259055613665073413850227520537676876119331884461911809395678550491435776120709039151645627020797792795237565574446494355319723631743729136988156059348012849335911/311981912641668893258143521918271312744923552065482534928695999628399064098551175273180903541008792841150984820548599915685144652584534067186028913583757650304548518213169918285291063777207050033818898019452489208829624065180589813958237980981894112531475857072541549788736937100356073707400860085718250737349198506055423265572432113892308104388226832829285126432277847709836338906389891084074300226543658657953773795808478623589743440470669994336290569788083205824691813420421333388365254996541022803816544780056051200*y^27 - 1585178507272103870732073824467993144620478896196490399534737426135256682358465123862648143448881543015069366178847234130858406642098129155626834784251320732149958762075183404250859926692939964689640184397245609629427331036047937421250851789975861020528335913506119154824703651566080210445984862257158594534635089291954995822250496267835496642548146044996320756993542071240652343782586216504276739210063717521848637846492931010849919838502545942053475593292642430848340801870069687583405385459327794455141467484789605642889/623963825283337786516287043836542625489847104130965069857391999256798128197102350546361807082017585682301969641097199831370289305169068134372057827167515300609097036426339836570582127554414100067637796038904978417659248130361179627916475961963788225062951714145083099577473874200712147414801720171436501474698397012110846531144864227784616208776453665658570252864555695419672677812779782168148600453087317315907547591616957247179486880941339988672581139576166411649383626840842666776730509993082045607633089560112102400*y^26 - 1413322480739235114462265777949389699819334634001954560922487183692088646507417340637414753776929197432322441045482810018149230225169372810963897950564688838314978259198745953153001607494966997995941235403248538277967567075585864430712948680913307920975792847876437325087582639592939977816207223119094737670580686970274595798768469776460733605996981073122733339616696437710116278363393902841754035378867621284260639705130565698978299097991989496599407765432385277192064341292970087936015097598403821216530304577472235947449/311981912641668893258143521918271312744923552065482534928695999628399064098551175273180903541008792841150984820548599915685144652584534067186028913583757650304548518213169918285291063777207050033818898019452489208829624065180589813958237980981894112531475857072541549788736937100356073707400860085718250737349198506055423265572432113892308104388226832829285126432277847709836338906389891084074300226543658657953773795808478623589743440470669994336290569788083205824691813420421333388365254996541022803816544780056051200*y^25 + 9697132288340046648258429696445769903962823174535497296907349319400679189250253804897463009726504083378840691832548869179911593558749921060822568238545120116273316360643447160433949995238588558958674033107084648760782585492293280580116018555010244680049256050889114762886006254609987440174094746289176931512459505806508689037310649147878869054977288364468982532811862791373013495150994927112525422589350330278243363542672632494129337403687446455741081545356069854521672157041217572237877555482870105963965976479753422265683/623963825283337786516287043836542625489847104130965069857391999256798128197102350546361807082017585682301969641097199831370289305169068134372057827167515300609097036426339836570582127554414100067637796038904978417659248130361179627916475961963788225062951714145083099577473874200712147414801720171436501474698397012110846531144864227784616208776453665658570252864555695419672677812779782168148600453087317315907547591616957247179486880941339988672581139576166411649383626840842666776730509993082045607633089560112102400*y^24 + 317554444698481075075613387825643092632189422588874342991088003734430062592136277143762963524293051894127667351394014330112610209364911775695178359470659885533786458890699918852107800578489299801327805848023294964939390946083955400793048874149933846407000172679368300817251950596922707866675204273192569228374097384279202116935410230519314576537948669517031988584876493760943262595545291129623321732571905539138221041074960075328948979850819602798355025005422604014533488760969368324338961573814388702847986560714002548319/38997739080208611657267940239783914093115444008185316866086999953549883012318896909147612942626099105143873102568574989460643081573066758398253614197969706288068564776646239785661382972150881254227362252431561151103703008147573726744779747622736764066434482134067693723592117137544509213425107510714781342168649813256927908196554014236538513048528354103660640804034730963729542363298736385509287528317957332244221724476059827948717930058833749292036321223510400728086476677552666673545656874567627850477068097507006400*y^23 - 170096230072151089651048907835031754917062164508260558048659912181205827163092135671149267081383103553995455127887184028632798107183877279412929941021737780004945385757876237898828025447342207443962748222023895648271325483054334834487814379460353995480632115588227511559569909015303608965095378705909669165591441807444178043286606766311164647441717883933774414529446640219376548675463346554007673536440753443374009223091686290498282558366335729423082369626299292341820047724724998968727391256263259469896080437860966986931/2888721413348786048686514091835845488378921778384097545636074070633324667579177548825749106861192526306953563153227776997084672709116056177648415866516274539856930724196017761900843183122287500313137944624560085266940963566486942721835536860943464004921072750671681016562379047225519200994452408201094914234714800981994659866411408461965815781372470674345232652150720812128114249133239732259947224319848691277349757368597024292497624448802499947558246016556325979858257531670567901744122731449453914850153192407926400*y^22 + 233528123119119202645685212878455635084913063153792144115142898952046866514730981772151099093655677410707435031816082254002124506582495040419949884862693872129245637023504117281493170878828378823126582403629383135105641145743321449120305206079913480087563891989324500112551892955568933728986524542009192008785369902122660861855769044246806861327956591928196678412425060312810463319352904625138571139896867464529378892787123557893051048057290533970741504986385106703848127399591157059789539814250728320606608456674016136673/38997739080208611657267940239783914093115444008185316866086999953549883012318896909147612942626099105143873102568574989460643081573066758398253614197969706288068564776646239785661382972150881254227362252431561151103703008147573726744779747622736764066434482134067693723592117137544509213425107510714781342168649813256927908196554014236538513048528354103660640804034730963729542363298736385509287528317957332244221724476059827948717930058833749292036321223510400728086476677552666673545656874567627850477068097507006400*y^21 + 17964051046650559132683990424138631377703519424122654231115426439071366076436745137294243179948615548830603864026753854244617615578569299105207826206566680349200159189620482265449896143198165685380634106713489995116995099647586304137666485845214687873547291017136654647812990518278791127778602553281401026082314902811911516979107161801155780595614808651831531402733042145180999215865347302976764890473158828578403541255938341660618593932795739208881045536447462545257730231268019896990633824407360375609527101953032370319307/124792765056667557303257408767308525097969420826193013971478399851359625639420470109272361416403517136460393928219439966274057861033813626874411565433503060121819407285267967314116425510882820013527559207780995683531849626072235925583295192392757645012590342829016619915494774840142429482960344034287300294939679402422169306228972845556923241755290733131714050572911139083934535562555956433629720090617463463181509518323391449435897376188267997734516227915233282329876725368168533355346101998616409121526617912022420480*y^20 - 14142143350241605954438817600903241920441647971555078798549967491408206482284298578217786324383581084509102785015327221625868993705112797631530585140337552193723366111556795029097568580871845491107534344032641749702270070179414685738052030861648351779481653829136200209399317869027544803189325243016421094086483009279498454514971585925318190657708399252360664718054751352957889654616135954967465481579291240403063526525973955348201809461945691588166358548806865758494834702275979368596972812498056252953500601698114753159737/207987941761112595505429014612180875163282368043655023285797333085599376065700783515453935694005861894100656547032399943790096435056356044790685942389171766869699012142113278856860709184804700022545932012968326139219749376787059875972158653987929408354317238048361033192491291400237382471600573390478833824899465670703615510381621409261538736258817888552856750954851898473224225937593260722716200151029105771969182530538985749059828960313779996224193713192055470549794542280280888925576836664360681869211029853370700800*y^19 - 17741127579100845429288276776557153623360126609642699992358665639394437990228589878778038308909196075492214179961913997625891566037028400236551463822235345248612019068806049366586292937148967437440392240777013788514050810384844149420214988953512886666501242518259057695273962537330863276051834583995299072639697241686946684334244455926220907964737459291882427983553420221758933969913136828615961142727795791367849321315366739956382487036260672313705688416079646427910178186905231750483464629045537858578628083241122672497701/77995478160417223314535880479567828186230888016370633732173999907099766024637793818295225885252198210287746205137149978921286163146133516796507228395939412576137129553292479571322765944301762508454724504863122302207406016295147453489559495245473528132868964268135387447184234275089018426850215021429562684337299626513855816393108028473077026097056708207321281608069461927459084726597472771018575056635914664488443448952119655897435860117667498584072642447020801456172953355105333347091313749135255700954136195014012800*y^18 + 51081667852058650483240702325458030953225853171478257126494801940285947255519586445955288098647312552907356713938466192773941479473125585661236735788140462618055908046405555726482483240125296689839761417118763006120329471532909339241942809903386603555310917633390153905796675704339488965069936965875288017602242616714826661891051931052030256949511266094852089782873282734740012320332007240888957562333599983574553348949698394666323227268245088421213596709023703650969838404399642409707259722860369648611694015674794428183821/311981912641668893258143521918271312744923552065482534928695999628399064098551175273180903541008792841150984820548599915685144652584534067186028913583757650304548518213169918285291063777207050033818898019452489208829624065180589813958237980981894112531475857072541549788736937100356073707400860085718250737349198506055423265572432113892308104388226832829285126432277847709836338906389891084074300226543658657953773795808478623589743440470669994336290569788083205824691813420421333388365254996541022803816544780056051200*y^17 + 20496202610200607323571379144209741866070122846802400798140978403153484943069061295140478787071785877012004521218175867672822338611510463716824291403496431741976389673248258153824672482189153235405180254242853091804036557389677388630907412228674867895138262820855040096012018561372866162037107638181340189213345172316375755400894334711379087626396529105596875885858092500361508956055870867238828903300822867978987340957015084187407544015438340810912565656400082023689913896326261354176748339799688210779831973470309071403717/89137689326191112359469577690934660784263872018709295693913142750971161171014621506623115297431083668900281377299599975910041329309866876338865403881073614372728148060905690938654589650630585723948256576986425488237035447194454232559496565994826889294707387735011871368210553457244592487828817167348071639242628144587263790163552032540659458396636237951224321837793670774238953973254254595449800064726759616558221084516708178168498125848762855524654448510880915949911946691548952396675787141868863658233298508587443200*y^16 - 43121118967023986590621605735837168603698103187025270800062295930233152019054196373068219079917160777053778912128684753249622656275051336217982583462686220216270178062603055377269922582426472852755020362587052927694643102738829018359269703494206706594715217959187577580981904861937522251219113620292789315556833186505627728675605487401607003803186474173264807761013134952406354711611733875911385104546731072850860247615326755460791259257622382205030109757036812780130974758981237019696544845848215183049893358476329453017999/207987941761112595505429014612180875163282368043655023285797333085599376065700783515453935694005861894100656547032399943790096435056356044790685942389171766869699012142113278856860709184804700022545932012968326139219749376787059875972158653987929408354317238048361033192491291400237382471600573390478833824899465670703615510381621409261538736258817888552856750954851898473224225937593260722716200151029105771969182530538985749059828960313779996224193713192055470549794542280280888925576836664360681869211029853370700800*y^15 - 3683654695508095369186934172301378185330720240842255728728866733640436294042285876836834798659585426613825263588606966703597389320847430402803990053221933372001071661979125908062785501603512642711085048904885774049686134100583088695713585370873573722634825350921456674206160300553989954116201856686098135762310812364089754390510830619394774206990213533461828354049002139159649466135306818274036743085233077384975159159068541406224168571781626012208029766960529946466153570931862148671313999261074691154267705159762325718177/24958553011333511460651481753461705019593884165238602794295679970271925127884094021854472283280703427292078785643887993254811572206762725374882313086700612024363881457053593462823285102176564002705511841556199136706369925214447185116659038478551529002518068565803323983098954968028485896592068806857460058987935880484433861245794569111384648351058146626342810114582227816786907112511191286725944018123492692636301903664678289887179475237653599546903245583046656465975345073633706671069220399723281824305323582404484096*y^14 + 3533303321767682096274066894228954357930662332687808664772892388342779005748486985830376086357365518950536346126146611911061909640625008645678153779143283586830653663140736167533991674557122261074862100387881218207746274604198456370770910481505239051886559543412260512054754083357141042243579065026510040395274463989780191767853811229125061349259420507298729600871854098420043753836314273483564142507216817941449928982204324536510236830065465242630466146634083680415425141238836936610786215848136118110250533850484159893739/23109771306790288389492112734686763907031374227072780365088592565066597340633420390605992854889540210455628505225822215976677381672928449421187326932130196318855445793568142095206745464978300002505103556996480682135527708531895541774684294887547712039368582005373448132499032377804153607955619265608759313877718407855957278931291267695726526250979765394761861217205766497024913993065917858079577794558789530218798058948776194339980995590419999580465968132450607838866060253364543213952981851595631318801225539263411200*y^13 + 920968615503002281625701873733467373598320478806918218239023830094458000139420113083895379448314732060729295414533513934882348867698450129882653857853213515740949813170377396884200830028143163039461833544344974502792667421003033858116065582250861939324865195434725703385239635568202207451968207548985760489445056013387521928859791487810976154035638697980996307614790623007184974032063562441699171039794604712969973398313578821362807317045683862010541141813433615019338376391178289866564716171107146020307563862360968532303/14856281554365185393244929615155776797377312003118215948985523791828526861835770251103852549571847278150046896216599995985006888218311146056477567313512269062121358010150948489775764941771764287324709429497737581372839241199075705426582760999137814882451231289168645228035092242874098747971469527891345273207104690764543965027258672090109909732772706325204053639632278462373158995542375765908300010787793269426370180752784696361416354308127142587442408085146819324985324448591492066112631190311477276372216418097907200*y^12 - 524210697799284481499601470479395070892468521829230332259958681509009199003578660659041204017711608193308160075002529278268151113145296963177178477460744214798556859716950725082676033444243653841367795825110807476448794583310365908253544185942194345068249029321860778967527264555533567510149299309565593346506476813579209869165210209075877249096070507000296120512667531598767588880771374553520234219867381774900733913609067858555070572317348465868195628889160668219931650007252288764676984376569320415519251783664346930699/7799547816041722331453588047956782818623088801637063373217399990709976602463779381829522588525219821028774620513714997892128616314613351679650722839593941257613712955329247957132276594430176250845472450486312230220740601629514745348955949524547352813286896426813538744718423427508901842685021502142956268433729962651385581639310802847307702609705670820732128160806946192745908472659747277101857505663591466448844344895211965589743586011766749858407264244702080145617295335510533334709131374913525570095413619501401280*y^11 - 12173349441614426155739754214256745823912179948392531388766678374886236439217897501640341885096194701104363335295812876141396145634365216319755500441711131782975710234845365533783917731414133144929177344028995139073374835612349529546235818813212841140230491236743002248156763068005644808923347068267712587576299828981600437818584673159589939799648531633793776860791654012359454477095446990608478570940703173085420271021661926775147875845528782972039205244623546138647553698071601544184701996293260085028650300354542020971597/623963825283337786516287043836542625489847104130965069857391999256798128197102350546361807082017585682301969641097199831370289305169068134372057827167515300609097036426339836570582127554414100067637796038904978417659248130361179627916475961963788225062951714145083099577473874200712147414801720171436501474698397012110846531144864227784616208776453665658570252864555695419672677812779782168148600453087317315907547591616957247179486880941339988672581139576166411649383626840842666776730509993082045607633089560112102400*y^10 + 93272745001061811482117461730444784265330799120545999159739255637061937044869160513264892007457364448491213198142509311393558280805627172066905539294974077164683941562667676262996774263125346563224857776483550209920944756585265323251528146533632358979985908341221695028432946925205524854876806756334949873539624166886201478861116953790647708795195660374886833582346177880909054351442840992970653323148719299278682075769704972047698956529508505764102850003935910586053183754564366290554382312674737786332258583624477079437/5199698544027814887635725365304521879082059201091375582144933327139984401642519587886348392350146547352516413675809998594752410876408901119767148559729294171742475303552831971421517729620117500563648300324208153480493734419676496899303966349698235208857930951209025829812282285005934561790014334761970845622486641767590387759540535231538468406470447213821418773871297461830605648439831518067905003775727644299229563263474643726495724007844499905604842829801386763744863557007022223139420916609017046730275746334267520*y^9 + 1158070719689187266645946039543284757849459894989502982068202103369194840041728549443979968297511320195927185782546317451557836636046809519634763728795711701403333046075662140012252888381138069447317656244528973325299182176782123374957080821535848392710203828251053706412822556407485637009485779370314699710915091867020478277098541597385833626542742524571188581232278183321772264168338699330736652771530443899126809941478096243497491894416547548820533905728923804806233587805354634511753040719673113263278865908407194227087/207987941761112595505429014612180875163282368043655023285797333085599376065700783515453935694005861894100656547032399943790096435056356044790685942389171766869699012142113278856860709184804700022545932012968326139219749376787059875972158653987929408354317238048361033192491291400237382471600573390478833824899465670703615510381621409261538736258817888552856750954851898473224225937593260722716200151029105771969182530538985749059828960313779996224193713192055470549794542280280888925576836664360681869211029853370700800*y^8 - 10823367708914637135006481402355188966928444845015500790149146988617568171122672259047644702722495779401903302254443581384809372509962501301064663221158619038187238037407861136420269642826758256233665899370951758164260475033602413841194982061527461448669284087200913267793679870149596232941227340697843657914663209262986835574997295016454723370800770211585534439231267052834658518876397933776521623601172365710883366099897710289400756930612452060661836242826636963599740683432030042772942620952835694979618053423761374661/3714070388591296348311232403788944199344328000779553987246380947957131715458942562775963137392961819537511724054149998996251722054577786514119391828378067265530339502537737122443941235442941071831177357374434395343209810299768926356645690249784453720612807822292161307008773060718524686992867381972836318301776172691135991256814668022527477433193176581301013409908069615593289748885593941477075002696948317356592545188196174090354088577031785646860602021286704831246331112147873016528157797577869319093054104524476800*y^7 - 843967750509666287394216671820261760313344612765110798031177100200770881080626749653645136269673143850460852010181357896997946356617725108244092280556879127394798897160502396987922851335775559876828716930255118932378178482874854505806431537427543893912897626877991106303480385916899047099908644315235611890330520731203807360714921055843476792524182041431294764891001909911974556340894185689623705244292229333884845591931719138369328854987220260695337537123107667506031456370345933767490676235890017941669961782172217649427/623963825283337786516287043836542625489847104130965069857391999256798128197102350546361807082017585682301969641097199831370289305169068134372057827167515300609097036426339836570582127554414100067637796038904978417659248130361179627916475961963788225062951714145083099577473874200712147414801720171436501474698397012110846531144864227784616208776453665658570252864555695419672677812779782168148600453087317315907547591616957247179486880941339988672581139576166411649383626840842666776730509993082045607633089560112102400*y^6 + 36713550659834797707032642017544967385106159404955510157789329632290101815011496844668155166173657035018856844044119469566552290941123558298029779241215051648644543491558143324094984798525122109580320700833967046467225259375594639440270458745182520903737612201816472380622432166626163807504088738829609659065016316089188549064189466917558071246751361341210701400890254840481995576550927043285968736145661603392168881749756557977571253788764089049538521859260118025455800484062274972507997379158236054408874695618397377531/207987941761112595505429014612180875163282368043655023285797333085599376065700783515453935694005861894100656547032399943790096435056356044790685942389171766869699012142113278856860709184804700022545932012968326139219749376787059875972158653987929408354317238048361033192491291400237382471600573390478833824899465670703615510381621409261538736258817888552856750954851898473224225937593260722716200151029105771969182530538985749059828960313779996224193713192055470549794542280280888925576836664360681869211029853370700800*y^5 + 144857316113667866212012942339409496586045259939853668473953554912734591633540462553572593841562361613053874962607463793774314879039760985728997706349649696467853001113479896034171668667667578681443782530145642138932415983080029099924219701616100143308529626931626537313520829783690166722772102068406914833512057905634768563345900431331008046890696480506147137323232592798365066293990568582463828718161656337555006198637029924960522335192457385553248617084601960008626098503328996197060442303066245469118691147108749511/779954781604172233145358804795678281862308880163706337321739999070997660246377938182952258852521982102877462051371499789212861631461335167965072283959394125761371295532924795713227659443017625084547245048631223022074060162951474534895594952454735281328689642681353874471842342750890184268502150214295626843372996265138558163931080284730770260970567082073212816080694619274590847265974727710185750566359146644884434489521196558974358601176674985840726424470208014561729533551053333470913137491352557009541361950140128*y^4 + 10030335944647294300503981985280879275745167386370269928247652202002149552063052896457318581495246561906510436808329323032266350282163757571573082857316679057450268897452203094572828759220379850121753750219455190417353220486454551026543124916558304695973345272073252376773237085723771377478401332180928970403689100116052305701237114469295187281170822171586029853596921133856680313975980568122933328133273803446953579434441567975532239523336047110093823599940116600613696620429206714167942914421016031278733479681032432539/311981912641668893258143521918271312744923552065482534928695999628399064098551175273180903541008792841150984820548599915685144652584534067186028913583757650304548518213169918285291063777207050033818898019452489208829624065180589813958237980981894112531475857072541549788736937100356073707400860085718250737349198506055423265572432113892308104388226832829285126432277847709836338906389891084074300226543658657953773795808478623589743440470669994336290569788083205824691813420421333388365254996541022803816544780056051200*y^3 - 52663000969457793557814798879857512919035586214158341552117050727030478103051364636917335382155576134777872797163713733062258113831970881918848461483762541305802863523771933435932804609311040035419104650832144674506231775308887112427059300438559497704990522221348841610208435451060562224205464094796114370118492259605838911231115103786944974313769342775505254770495725430102313050460397261038122639724243409184713476701437370628140424199952834944717266725866889475124721557995849261987796304415455545975597362599014379/41597588352222519101085802922436175032656473608731004657159466617119875213140156703090787138801172378820131309406479988758019287011271208958137188477834353373939802428422655771372141836960940004509186402593665227843949875357411975194431730797585881670863447609672206638498258280047476494320114678095766764979893134140723102076324281852307747251763577710571350190970379694644845187518652144543240030205821154393836506107797149811965792062755999244838742638411094109958908456056177785115367332872136373842205970674140160*y^2 - 22616380948296730644857199055611452097649746354954503246821844237482076360412843184381162987433352409130538560108156554924167513165792340369422068436903338825884525046484407086273794548929809845944577719330120765804102248872830660121271048225497473519868570591472018786386720005441226317273658093870269720070877077762284190414109800680701252519770262892189202781747405666438090281618755513809515154974200225886342047865921120926191221610579000258658485577106192248141556422149313533183791951666079984727853689724777671/23109771306790288389492112734686763907031374227072780365088592565066597340633420390605992854889540210455628505225822215976677381672928449421187326932130196318855445793568142095206745464978300002505103556996480682135527708531895541774684294887547712039368582005373448132499032377804153607955619265608759313877718407855957278931291267695726526250979765394761861217205766497024913993065917858079577794558789530218798058948776194339980995590419999580465968132450607838866060253364543213952981851595631318801225539263411200*y - 3023691777248818389908539104597906271855894805432177796629948948056195110380876902343470544843960471390297223155812751235980882541870598446765314904537972331188591609892204628887291077430252647083320000719095490712998159550976221101567377055431643986652712953434299279957562444167167809106168525476932904516846651703555638715667956099398077454227734659114171047723529184494980865584078064248420761456589338194213346342612159458911890011650309686370214597421751133008124422289509197138403457081901883797558960437429707/44568844663095556179734788845467330392131936009354647846956571375485580585507310753311557648715541834450140688649799987955020664654933438169432701940536807186364074030452845469327294825315292861974128288493212744118517723597227116279748282997413444647353693867505935684105276728622296243914408583674035819621314072293631895081776016270329729198318118975612160918896835387119476986627127297724900032363379808279110542258354089084249062924381427762327224255440457974955973345774476198337893570934431829116649254293721600