# Manifold: Census Knot K8_62 # Number of Tetrahedra: 8 # Number Field x^27 + 117*x^26 - 1352*x^25 - 2316*x^24 + 135827*x^23 - 935622*x^22 - 699598*x^21 + 50761615*x^20 - 332765777*x^19 + 933276628*x^18 - 392673794*x^17 - 4241778217*x^16 + 9143021412*x^15 + 1923008315*x^14 - 23920058558*x^13 + 9954286863*x^12 + 50876457812*x^11 - 18056512367*x^10 - 70449531681*x^9 + 66013708280*x^8 + 15750166104*x^7 - 19030875633*x^6 - 3549503593*x^5 + 9538022588*x^4 + 5971064977*x^3 + 1670359242*x^2 + 206469295*x + 8036575 # Approximate Field Generator -0.190903131304422 + 0.246052424630076*I # Shape Parameters 4087582194354714487005216492725723996115904817985305376590400866276421640442139194134312881111664182546620933171297582205377368872724513110412926136729181662694700760352158361/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^26 + 477541556777422812747659081010635351708931904478125305493100471543688848293588516602474356234940274789166683665145529802475176755487354221008770591433889114481984885080975950367/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^25 - 5608833371742848870855857459416207999781176149263275139901779827026958235471831855500387241092812043996187068080305857121319372411512488966184214596729088053772249396279936040722/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^24 - 8497935099597026587781313316194133947768278710276405366698079167653199078612907767467437677795773353793311036402703282482691183570145663127414801544082619562457185408628397646606/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^23 + 556662408295047011850556894661672733018320092289373893319384883707359346832929894528294229335416785071668006887074109785171892065495229726804846732286638161821802871681685041033487/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^22 - 3920536218042520194576363919482803532975741898111223197181192561886535577292513197830332927076633548894746803099013935014507572679982778448599553047755024516140260793943566168465037/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^21 - 727354900635232563490737044684438056875496556568912218096775658608382636437565303780399147310860604569861313142096289643455226210388746996057472768499697376389085597611722519223711/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^20 + 41572643577301675154291488143792773771376372071960560149961879855803046267623357897134690436260192863144165874533623921196526331808057152452739431352380371780140220411221426064720417/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967*y^19 - 1396093814896082976385487303555789287096640539806510018085393884296738275308577749820620705104141161864141713264276134997685431892053038447874921990479617336484312847518571221747563277/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^18 + 150227855900721424418124641661969835028033071181383547729714587238102191888239643191935784672449412212142948087549680819628896423232157805520066502176800747720482705793177969500484254/2743287360042406993191886819196556848491640239592300286781078045460222989980112635742263627210493905440673906164956460202420381838661836916757560459424158386832937717352613207181105*y^17 - 2307242735606712769491018249529768863244812360159736682871461897298801124593729484859668772877528844169951143923786130311716838558613565127558102569966909002008065683050613104726756649/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^16 - 5645057242433452914302526421772477253404279460786491308018618803402160889449865211549391515306407199239515997407206460535827496716096754601039688290729063562306521422261999656025328349/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^15 + 13431922484769401906346586644649529795907818171071503746762000487149245776268769770301632055039472010208840375097998685752397822593826255935432228818999363932533792228802681832619289344/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^14 + 175432616328831466919871043258562490264131333067798458059740850761942174752792471819248536023166255282741103494653162745182847794462907910313697962928049855320999203268699376380846005/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967*y^13 - 3625163655652887684550495754359067866168412324678462177254328336293255873791728752580991161238807879357650171789433338887844121005105221865217787919709330425906733433248038781310354309/2743287360042406993191886819196556848491640239592300286781078045460222989980112635742263627210493905440673906164956460202420381838661836916757560459424158386832937717352613207181105*y^12 + 19206187589524585540901160334168490447912682362875876348820823624616820837614533349107724323194755892198481007315980775705042651643084994172229497084193124315914833988178711168042550996/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^11 + 197873929552181173782880833189455961073669852587680603835601155209093415430452802072570746226869960431239827605322911476979770608833673197680522084446044391697001995812770644374383947087/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^10 - 11996146781639885776492911431166752170689937222453155985226777791049453342705038823351746981434212634044993150914629945095582530109254699555822673725100633485070951587288433731985880418/8229862080127220979575660457589670545474920718776900860343234136380668969940337907226790881631481716322021718494869380607261145515985510750272681378272475160498813152057839621543315*y^9 - 89664043010019336863867396481619543027255919559742501600047023192000594142839625582334785688156136847438400197364832091743193140816434969730813604086044750986201242081161853390554577042/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^8 + 63260761733554915660621439086403582829466615911586184968017918425509249414495022563494043942625272125311167274561467145660296306381735780015685880404707937406347771893130507090354818670/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967*y^7 + 9308355868822306649552328325827948760157756151341185615381771276870185512115563488238771326190285055938131805739364488606713055579711933144376174365069656336206089589473070141830932209/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^6 - 79196846736805523034911626618356477686577245513560569217644728940117310460734054618152005441822434677073790860758154260618408543767078617962157275679557374556533453597910255568129258433/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^5 - 606063762217482811418841610582805717109183548084924434167800164130887960734028716465269834428822690177017124047706280259777190575772852976505972286279644260364891411092447351060487058/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^4 + 13033603089018673569289344904073466849275653813449168443010188925304086592804310973676754633811958026285450230071053337379239551617504400067855705396248491439524115314254602672403703861/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^3 + 17587799724585482784512690003523137917559018143628519264182395831410458081270193443364041431436640938581171057078915277495730004810015557453974045940793766373316619445110357641134972177/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^2 + 56346427394913374869268097942003176140440007351059264022417875877437534406401979888480406904391285703114836158613014458182546711288958997029688706499767357834680777320532577748205851/1105503861509626698748969315198612461332452036850628473777449361603373443723328972612553999025124409655196947260504842171124631487221934279887375110514213081261034602515232187968505*y + 45071507698601362521492346125859018764357355189585437195259567228259129769724413819592365478816489735117311774016153899820836924408300314218839606066236230006207198491368635381088171/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967 -738326932896147022467108174759070977754961965897962571522526640383591339705485904871702765201589696105251718442334935694280112205383339474397913507291224571018257841004846432/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^26 - 86252940646113251530258718651977030328574292452708585063331631714247659364492078973782865429627452952022021346307696100813165789555618110853874268610143188469935770361907236734/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^25 + 1013558575021478546044306658293562401046450376194414668258765803695340532881885489456459597532590359686814550202823937198386930021381290689414844375333325007707215816744206418349/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^24 + 1529773525862279885077073245452563950528219845219558199638890222807621102734148639553088508927357778412542526089536549128176148025994285424187691280452890515535422906403099158142/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^23 - 100557611380188163476344025001813285307931649409955431727811811284477115747221371935797943135077285964984200050546099505873234403224954455057981262515529040290440332737101543077939/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^22 + 708677785260321250430898600090910491712981587869848729512901688466751695538862884111866993543547111697948063127120742828820613204391442452711912137894272615387303835421518099865249/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^21 + 130191676345129740068053461221787110983913371363135495371799574074596072453196207426929818108701074269474598873552920563350104800255046137148343687027503988766027910270750530726147/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^20 - 7509740228199486573462221357273579030735387720575461503152725856819676517155314650975586586474136307457927643367309439743885767039507164648324942160257353689654403887341557800012406/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967*y^19 + 252367627099496324785558370429050835752702364587831947793855385523308087458197100118653499006771635313447878334656665156880317011547076908667301965271692803087838912708723894825444124/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^18 - 244638771704200059265218002906384682687476462269065007858432692462425756559588742049411082342732663098207940016543748357704482388511915766727891173459304958096071586398909236894289027/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^17 + 420243721520012487906360309814070088446990407142953596919057195696269140105952981274320091927269773856350011177783778741005863217811032610919253376633025102106206029220419938180718428/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^16 + 1019222868751706638052298069519784940703047984290136369265716324778946491157135299927072659500758548149486342880823539821047252796995448122998868738695415128734925205678493885068005008/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^15 - 2431531379372785282361937299972985728661999008066544816172449439488397013594683917406258833568163999950595890014769554733076889804075984786107292136951292477014202989794992234263972613/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^14 - 25118923466147611754422198398556060829106363722092123289726674386757529302812018833480245716010541700689688299347606456630514546114626157482846763090730915590380569063277890585161918/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967*y^13 + 5897216545431045848669078902902047189481073186636835438305928850752078372696317913493245196825756388889521113599247456618969193717078958927817266294732238920349255710901534187379058002/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^12 - 3500711851334926162345191575696228933901794784456525249558434862268732364079394126877072460653919240747192357334527423186909088317723366230729814787419146149350016567066558666594334312/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^11 - 35701527765563900930436596554679116074270824192092272836479127340458257067014723315424004992080057023006572140080046180074327359254130812685838194190180877337286856037712787077222906244/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^10 + 6563082140016904297784404207309173067755442481033473854834756281483773630424328903548836025166321443483297493694210798605734647443855408113959869294858886731553346132854332435131176468/24689586240381662938726981372769011636424762156330702581029702409142006909821013721680372644894445148966065155484608141821783436547956532250818044134817425481496439456173518864629945*y^9 + 5390480576745915591812493478641677887926530814363691195053783791717418334599482895191859786529180930604285812918938470676505383933769377677405029669537282196773366559382377287222090843/8229862080127220979575660457589670545474920718776900860343234136380668969940337907226790881631481716322021718494869380607261145515985510750272681378272475160498813152057839621543315*y^8 - 11463506601230685994497569458694722211338283854092147193306339792085024059437883023678029008820597195772018233431134598028498940143288885754802052745992364394084171752541892774481697034/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967*y^7 - 1553827484582123359501639215289091817791462648874783683485026226241122447110293992286025648608007186564067053959930526902690647593166097173540544748637527126011060583959886334963150813/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^6 + 14401294001450344910690380874379698912886273753791862765512531888755593950783708484663571285782171138108076368059527814766982957093714034018054328644691383689835396585361741687370931276/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^5 + 93044473421703293273689978011644662045040095441628140808185104316128005430029739930915927262939121646788163589677268357382646317454593363188764143636521619163788681550122997332229961/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^4 - 788281892940733783017005591318622889036089438071865429005841567667201770675250024911568634184852607673988615232281162658412962864581190336139036270277645732933074354505978018859565639/8229862080127220979575660457589670545474920718776900860343234136380668969940337907226790881631481716322021718494869380607261145515985510750272681378272475160498813152057839621543315*y^3 - 3174716829293833368915218656367135445079209405324942182842450267419399798966696196281628675913929503591487453046380987874384770590788069461403264161803270652637002050608503515625012994/74068758721144988816180944118307034909274286468992107743089107227426020729463041165041117934683335446898195466453824425465350309643869596752454132404452276444489318368520556593889835*y^2 - 9563036418369351386973260166876754898952566889732933426881389061711963290281911574120306249398458800233124120974838213924762640517477681707543496383179555874924093181898644821494872/1105503861509626698748969315198612461332452036850628473777449361603373443723328972612553999025124409655196947260504842171124631487221934279887375110514213081261034602515232187968505*y + 434760700893513595482555903421586353779503400684539895391970716254100664396924414440440843902284415402038074519502093633957360972728893010569903104456353704357853815706577177370692/14813751744228997763236188823661406981854857293798421548617821445485204145892608233008223586936667089379639093290764885093070061928773919350490826480890455288897863673704111318777967 -2860506049092149140311814035347393209139861968358667165973943663241484675266776653746366736714108771872117318396425971973992659405278733263405671919683907801962347873481064486/403263241926233827999207362421893856728271115220068142156818472682652779527076557454112753199942604099779064206248599649755796130283290026763361387535351282864441844450834141455622435*y^26 - 1002502093496668417506832377221583719608085045738837145716559276997229021005575109702025459952448795283198516660675952269567855556179922906755024398478528784220613465763152722351/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^25 + 11781644146194302702130505702617580117055074449876815923990608945382531565073348959653487129294568901566189428474981159612344420331941313640592162582277600157949971722805830574886/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^24 + 17772427993403771812116870037046747392704301315397427531764282053050946372394715781369470658154805439491137973994277280256932206277040791068385566680383328811133744618399637899818/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^23 - 55659486389304462631376301021283097357894078727241011098828908354879009090273170210575589485565151002659292023375049946851866705159329818203343067945021008947049663781614893376526/57609034560890546857029623203127693818324445031438306022402638954664682789582365350587536171420372014254152029464085664250828018611898575251908769647907326123491692064404877350803205*y^22 + 8238097066189148773067446487582561381479777069001499784700580796644327008549891295724017873872394829947929291175285907108233572716173863204168041502091321328964239865920681005749396/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^21 + 4536234460064309237532884084418226833154589813488319493929078618940260451802252704848673382068596743339623192220054770267505735012307833195319964634334838717645111456004638281533414/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^20 - 87294036080706245545405849352296934709897923132169398830420058895792294294880886392390638557234616686177373736355017854500517985373668104800556480573252206338469270053025494030750570/241957945155740296799524417453136314036962669132040885294091083609591667716245934472467651919965562459867438523749159789853477678169974016058016832521210769718665106670500484873373461*y^19 + 977901981428107390936794897682211999121876814888958551808274327811769801325047348814710931432791082321113595438848179979128488834977548753733196652579690726046058868595476939562203982/403263241926233827999207362421893856728271115220068142156818472682652779527076557454112753199942604099779064206248599649755796130283290026763361387535351282864441844450834141455622435*y^18 - 8531374138300218283286275620018050212986201328515848221304330995979405468343987558858312309972622449830671006129967843254517779042194188463926004586653271624490534904773599559654065109/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^17 + 4879659768592252837455681451566796559039275566479527193000754789426505756688018891810663762528151544504547902459091911081236800993461317950543577556191883799723122135281558655260032152/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^16 + 11858594410941910392403586893292815355267497437798555855997754765864773191997881942130345418470758694508347591711500217168310784397341223701753831610144017432332450454520471914397962697/403263241926233827999207362421893856728271115220068142156818472682652779527076557454112753199942604099779064206248599649755796130283290026763361387535351282864441844450834141455622435*y^15 - 28284839834658509725887370136383097319609697209503105100434666489230149139271708359923749490935259651493707753165239343347002046570761091505968512775122624705001151343621561394499458672/403263241926233827999207362421893856728271115220068142156818472682652779527076557454112753199942604099779064206248599649755796130283290026763361387535351282864441844450834141455622435*y^14 - 100689833041540745502551976196626147491607366069780652523122470655023609147756580083244682062635885479500849234643099533227859176948747191641321680381187470047781038899744676484102409/80652648385246765599841472484378771345654223044013628431363694536530555905415311490822550639988520819955812841249719929951159226056658005352672277507070256572888368890166828291124487*y^13 + 29426631139476984507919726929980377718575671996404731616389164915869339120240597318753007572938453030450365666503602923434476009382851458242924993658909731220840397262201642276071220122/172827103682671640571088869609383081454973335094314918067207916863994048368747096051762608514261116042762456088392256992752484055835695725755726308943721978370475076193214632052409615*y^12 - 122255768202617198871045185130517092059424696564505446560467658348944826335976542503278182932914529471637535398467261875166774760671136814653770542696171605024673979965688075497528504924/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^11 - 415740432827037223699143610880632296086335493380930504955602982711842147318470799628847871328637049906064289255016960347510995962354040978749017137791378531045759583143738586675182135856/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^10 + 32822888957821121481587568827199403489529507067006217477329082458834579659282150346403795948159398063317930681159940460010037520393029678895218316478409825796688410173475144929428047958/172827103682671640571088869609383081454973335094314918067207916863994048368747096051762608514261116042762456088392256992752484055835695725755726308943721978370475076193214632052409615*y^9 + 565708886213030259933927025844145889075987509073428219301484768354657582436577124711055528448657479026874609118293053170071765702490282537631818053684797397770684279426500238047099379603/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^8 - 133658777767343513358339600515219439370929217859428776107044724696105696726760230655196504193364827204164287405608543776935833293302659524833179364784738848266740769415160765060044843137/241957945155740296799524417453136314036962669132040885294091083609591667716245934472467651919965562459867438523749159789853477678169974016058016832521210769718665106670500484873373461*y^7 - 2091951231844366433249575081424948613137785758858766990544405940837788561492416347593156274912679473731436363897999583280519159088582703162951977302203301545868677498527994894031516923/134421080642077942666402454140631285576090371740022714052272824227550926509025519151370917733314201366593021402082866549918598710094430008921120462511783760954813948150278047151874145*y^6 + 169271898466300029658786388794272869254965535245858388214903672730825151212420769248174980110095114436353129376205952037637498100957403816250859716430661619323417782668033955491203738534/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^5 + 669847548391164663724333466446964615435996852907394142732233000838785632941730824743170253822492860906189265138773546707600233047390811989127258459172723405527020757507808243850960929/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^4 - 11630935831230600622783951887500840833871857488833926687177385663934981677564807794193138624539909372991216839929352325532995935582159394777200568773559110321192964450009796073739269877/172827103682671640571088869609383081454973335094314918067207916863994048368747096051762608514261116042762456088392256992752484055835695725755726308943721978370475076193214632052409615*y^3 - 38726249214959779430089768815742043993482740894734963648788843194056965572712031512812165045060767436671975403738009235589351977635620749546109849515140912444291279517706628522432197216/1209789725778701483997622087265681570184813345660204426470455418047958338581229672362338259599827812299337192618745798949267388390849870080290084162606053848593325533352502424366867305*y^2 - 33577401328043395795151037217118550201445461243546632230974015792622016364771344817692597706997488724589355904102006014383257740144111225716495498310176200544966892311662064834832851/6018854357107967582077721827192445622810016645075643912788335413173922082493679962001682883581232897011627823973859696265011882541541642190497931157244048997976743947027375245606305*y + 98095898739395274732676573650940493618431512878208832466153656549293105685558891531349128646173546100334701623472072242332457044961802468233009081507992426208962241444963138445697829/241957945155740296799524417453136314036962669132040885294091083609591667716245934472467651919965562459867438523749159789853477678169974016058016832521210769718665106670500484873373461 -14400140781689147712144086878098402658573844110226814866270611641170102653767992237346077790844033547402779101442045258685237373971629312901533027252838868702704984650347997040206/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^26 - 1682020499701400228216859189789042793780222502353416547027970150780493440676963803992797738398222389083408538492094321791076435784115385626759869468076424050474818811543822985072204/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^25 + 19795680821881437108347201104735006178338688325597743139409104831532727352338630283553766603834040340053872405041081463431967618819756026721202840441894217418900985920783616403642166/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^24 + 9839789556735490250667627019800810143579777332433482571213882707007674163462439128581454458021990250573446692115106540070807249500386351499345903537287343374961255808480136269309380/120881860205324647192203215933168598906044730501538875216893491641986541964277671248928549827579529745681119405596340436235573157567898379002155198620341769652438667340055959929152519383*y^23 - 1961803106046284204164649581421533493785061840185354514963345126918138792892298968936108529017984303284571455257320808295281674022887078578518901245895978623239214995389032543386092677/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^22 + 13853778927416136847730783675572446604603682832107318842095755033466617269707473753553477679609395521800451056600986037315471919341941240971399159036086160882190511213960600333834475353/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^21 + 7398687973136585475509171374187219047514889402047986677433809473588758968063548528004379396777154300090500097129612487461803111935344650067563586370171377440335634393882947550651132192/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^20 - 81390145923371729083112694607559662672298808466956483287063448586717418409437802966592901379481174672224787515307964154864228179301685300991188509995498034296309202279951109687561464817/40293953401774882397401071977722866302014910167179625072297830547328847321425890416309516609193176581893706468532113478745191052522632793000718399540113923217479555780018653309717506461*y^19 + 4934043241252199205223249878133297276319855423923076089800297816012008748049429836683167400476686930431184715848738351511101736812035232288959888451686673167788533005693934843674766401362/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^18 - 14391990689786496367595622159583023694449846333584591378509312455569810913509135523267846324162494186299516618645685235238701287454429659335991468547821186070322937981336645112372459832133/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^17 + 2804402296094545864507452982748461682413901405252477122770351418394628672216739715744254168282680816431783754832128147226133010895239799139298066708925534798905974043983539098241362601643/120881860205324647192203215933168598906044730501538875216893491641986541964277671248928549827579529745681119405596340436235573157567898379002155198620341769652438667340055959929152519383*y^16 + 19850672253691244655269334036852009147988308750101378861284304325062429795343625308645713778572593619445534890724062740686529242180412322412478697936213610443457887650462466900776831827026/120881860205324647192203215933168598906044730501538875216893491641986541964277671248928549827579529745681119405596340436235573157567898379002155198620341769652438667340055959929152519383*y^15 - 47759749494284265265212698049675398686339964237161646846507265357118839428299853568862047990450473529903948670002039912065053862600749725911386156206273109417671634334631337018061787691619/120881860205324647192203215933168598906044730501538875216893491641986541964277671248928549827579529745681119405596340436235573157567898379002155198620341769652438667340055959929152519383*y^14 - 315566873813660134105348743051963210581314772790479369153368720110883823849504342171038918534885373271595119580024019826746190762514959080435543694446769591173048866088201933097418649186/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^13 + 345550707999184464448077961892409952844216813857112201378406033128671651715166852071608180157448963488848500114997261762558628630541292490882491882361927098579088236094732399330010295034266/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^12 - 210372096122818883815091684418743119824074014165073616706876206955462620258510056434721093650738142214393032039939583786722525630970067987954353175509758290482448454017739014753299054037778/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^11 - 694386267620853203087836268934224786809499510967133231239880884072083116965732610831751423742749479589380189736601367090054343267588993339138345360901697097773291013584123640687863373984323/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^10 + 396312328425083817925319714502095218075890124306778762924686637431787161435076638214924717519952545503901402386380188850908879894742639783575428329044142532665390469271715881774735130498473/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^9 + 942841121818791053080005376516221976618285679376682932229185323485074381110556497832255142825549497008673358446930064650792703649590286673610395698848410312628215871570265562640821089068796/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^8 - 378857691884843434554210894678817848457316115759430142398873949059021788309205358464389965380163270015814248869781168571233174798220431198131391918810698741270283373978688311331073235255268/120881860205324647192203215933168598906044730501538875216893491641986541964277671248928549827579529745681119405596340436235573157567898379002155198620341769652438667340055959929152519383*y^7 - 13493014203871107668644942660675024448540150526441126510605707906239350068843571218730397021252121842217407333883643432352844955276973826642364846126838582625240982756852656260856281340622/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^6 + 285017037851246768555553164105995115822725403541859988444231951033049404688174483151053840742032160579905458169794596946968453716952535022070562740879188510228529898355876543760100550379181/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^5 - 3304090935167995445106334461174624062106308594973757457904228976667655324147647971341477869781551723350682391109066155610998442846179220092128793657264005534261238107160135288782224396496/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^4 - 139427454440426383956106630195999132039818402625442705679973523617651686571219888302576168261962123260788707590090626806450600002293930123594322648470238827752197467947474033967548229684443/362645580615973941576609647799505796718134191504616625650680474925959625892833013746785649482738589237043358216789021308706719472703695137006465595861025308957316002020167879787457558149*y^3 - 19669095979278824366883875241999627114930428756987061334744795371739583711937689187917850779153048253053390582244397753953224645661939360332292961829052813226985542934941839108507905733047/120881860205324647192203215933168598906044730501538875216893491641986541964277671248928549827579529745681119405596340436235573157567898379002155198620341769652438667340055959929152519383*y^2 - 170996057137264038196374872684449212826425527590891490920312796902219896744898493087829328353354803306252674264376076788796451884158326814561959206846918408104540993350078128379214284762/5412620606208566292188203698500086518181107335889800382845977237700889938699000205175905216160277451299154600250582407592637604070204405029947247699418288193392776149554744474439665047*y - 114809615718797156485417267785478478848613846693394067257752531104719482141572067393631761391896836266619812746084546026535521858266831757758591069172064666739344670735217428709204980782/120881860205324647192203215933168598906044730501538875216893491641986541964277671248928549827579529745681119405596340436235573157567898379002155198620341769652438667340055959929152519383 -68482236723880284202245737717233147926108239004509198994712169625376109605817447764834431201157579893480358466914646464642710263073594714489798931268186535684152028990660527115559384/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^26 - 7977013873662645980278132637558529058350817187984766321892717711300479918877436207093737063707336139594832418363494647313520880554380450347177821711118298552079880372066231894610071645/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^25 + 96719668439368016218866443741280301222380411520668216614721164826225833928281129299509805195157957169676262637382147594451085851536204945214984790982363602968502686058630913500902144860/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^24 + 109446178388502071288165767858986737892075223370252908199219835459051594021272497750640144512931252736657312811369354840599959672219539491562583193219014832957673800284817137645857414102/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^23 - 9368440463104219956050870959648491668315101681765737026236820973036163150051956113924644388211396102015131890444551430465482421587321357901358501989330601243937618671873181404704598784742/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^22 + 68903857398167464959472324313946095273662497001142559698233943961925932765910903757020815298596891092685715312957911250257455904764327877615154097446335342705288196602762483003306092098202/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^21 + 4425380897136266508347396953582109542111051199531174839661857060291157366140635754207285834463520030827124947760615456670430720527082948060176687754180101755265533069362322787768133090795/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^20 - 3490268380015140981722576184585058870610766026653840416159814554575722038022726389494082103245470284468604387988617526191127808167682708084157157199759221454020237361026747071662081546525216/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^19 + 24590477405073874283478458301555910028978737386454079053590530521702558946575683227721633675526825497002496585107401774288946642685294490766914449059324997603613136338335361835961808362457315/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^18 - 25419128290832380623216727819413461498687153969321795730229663563673579340986645274879967440700256095166723253813247939477312292691888747865266858582152292478254215420277727294372559363569815/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^17 + 63775886116868049723662812241555275001172318959642166334065634944134750459821100884539381013192819959961810007151464701958591136265500096758284644761520582818880300963778709777050060149676439/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^16 + 88389674031878129990079780168176784608728151317230272132356586637892131756049995528020102400040248955257929589378478198404334580337341603792665381850936170618290160850652385550533606205322923/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^15 - 256271064193494242178782892929086152505989049670258924625923985159671857140415018875585453581259522339558810355723346216912822916465158129283055552168278573110437497180472307840842616340904369/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^14 + 237365708941405261726986472863567552863566305599559133915976024863004818438318550364495229373363716545141081690893823471010124340332419025449532453404760830385541870338924827770548363788471549/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^13 + 530310971926296221472778346713890047877897375421244080521791258008216648835894513120687529995996350265605427768119309599851913509213050133557899808193050981718470697360104242410745505986579961/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^12 - 8573970813625866713362153108773873784519203257410388759763895272922730264069119812045665854379669196942666450562575409706211187700658558452785806787527422424577760060265040792180491626200607/22788114464133837116612531072081023169377290908892606010991355740808280695393560373769995854931546803225757118726273647831626542277757453525316992356701910149048926971931054486134621168499*y^11 - 2863319405705865292919792872686666162754112879747407272541455613308082432465118133476534409670926428570787569800489531744502045316264689598074370789505487214384603121875734836931595799776348374/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^10 + 947831124562556448594336340591341746751983962209160317094379855441669202268705450845735390264494821277274675374485687986777086171367709461724508673946740313718249953547361362417151688416846101/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^9 + 407626109656086036399971941819110161154571166338117087214842561772033089410549315809211158340495434657930972900426899183994869628129611425877998096081670545048590742588174204020221796618202208/448166251127965463293379777750926788997753387874887918216163329569229520342740020684143251813653753796773223334950048407355321998129229919331234183015137566264628897114644071560647549647147*y^8 - 6643652052812956602277713381258191461419633083372039162059569524312696951917869518572591141003239321048862609648463920138197262921420297697530476648044807896888194375666010285352862620167821026/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^7 + 1946097456349448731847388217950674677842349095039732384446532461432288283571165181126681732031625341710548871590722247418887657026873563984789276647723594150830265139644344574548049384209802858/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^6 + 895585999567909131921167125836310562661858022340431303271385213254207926798095975488591806017577120440452844974227967233747737535356475468884877225430869626962617347786246061227402031123479235/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^5 - 339168811265935607566569330712907695322062245404472028839159501421259446855397544308556142002240002660678129171713173185804723796297882485646319082772170534410705334167283701353797351303688838/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^4 - 6571518367190737389837224321287073424097441660458478257348683377114998252093498326518177988493971045294170963795464116741942140651599152157902662847316141754845143180478606646303330055287755/49796250125329495921486641972325198777528154208320879801795925507692168926971113409349250201517083755197024814994449823039480222014358879925692687001681951807180988568293785728960838849683*y^3 - 154311264262591517674421163640020099590462030928328047430910213508518182849781704653354549564146702821592047720880221771131758093200192295148410921584998724075224282545983746288791431507424743/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^2 + 217848757611481574152841279166643859556235152936944494833739038871744595894334968412533989962227929495630099812708088558003713543537461707349674985129260134514693519128074073663481714687178/60201436718681927905080865668034941805668365535432705432021939792881577359472540091899839795863937077178492686784334860689520865420344317522106084285615493975845672746743233493221312639169*y + 7660703209190127880649183771486979981542205287362594672915738540658754066505286119988963483325873994723485677858871960063608846915425138314868049484003259714195644976106625775522186300513243/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323 10338622980120395032095528038193251275174389450907181919718793115764756992421316599476357066036264926312516674999938076989113009546907351184548424829006757783008503151797687585889881569/364359162167035921657517759311503479455173504342283877509740786939783600038647636816208463724500501836776630571314389355179876784479063924416293390791306841373143293354205630178806457863130511*y^26 + 10861320010030483488401785059446108384079552836820108789470339202243381484563817461070449650875263485587195676577560938482895039693048993778330072292924144026452190369682411502871494123891/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^25 - 128748501809573365877181198448273352812104499132426328323330753014194951780662935861716424326474853427520795012980211209447324670285475387144264234945102861309088686016054612156408084523209/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^24 - 180646618708112614016230462928039572699733457176947147977729591155883438926086413328750853698385703784443893162703361940548189328522803819658046811792901183692956568788556634860346452748147/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^23 + 4229478434728948286935128160808832838685642729608600662336581784678141319135764483524026976589748953879115524250841480650250931910279256322046882486021215937689412622581559689800205848444263/1093077486501107764972553277934510438365520513026851632529222360819350800115942910448625391173501505510329891713943168065539630353437191773248880172373920524119429880062616890536419373589391533*y^22 - 90499316830583216952787097159891505259437534240225004593507121149656611508410095236124375782937718734960167664370867630069186148005859498628744725731410551904893046075725153126305669415507159/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^21 - 40638501475202022186732103872614747053269803094019811645657160621983940068480228052120134312147885986494831720891275041061594128696680820185075366732153010592596552547576502889389586075284349/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^20 + 4735009171853330508525138569133911533321620363086371211091103234502106071666636408342971194387612754080011547572490541728383886491766914077510558353265013732693952197230701894189085663048934462/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^19 - 10749257198671825584797224076289481626078193053012536661027399932546940082799370315353898097529281398025809739513028922953610280621787207209863899178233351187183434814139997598824391378927976729/1093077486501107764972553277934510438365520513026851632529222360819350800115942910448625391173501505510329891713943168065539630353437191773248880172373920524119429880062616890536419373589391533*y^18 + 95552487496523171908140112476194103838472282989944307918191748617930546621903431266403028600371928780540439064359522907978181061324548747015281347847296467209515475863876889419663787697143988794/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^17 - 62205158715019272253481045985820596096800452376758878334258380189620918581939423375137251160812280288900553808081249928987599444840728784807622773625833708336066810061036535775058992762969351569/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^16 - 42067612336404497421856088336345141122553224514573850089927434327554806786308345643078320175216186365523043627271698045469434535901294290972847160114214785378351768872816130064683811950979846979/364359162167035921657517759311503479455173504342283877509740786939783600038647636816208463724500501836776630571314389355179876784479063924416293390791306841373143293354205630178806457863130511*y^15 + 318038654386201708835479976672559142066277525399836085161458395904821285543504622279234156553434154200538402207769255126469973212355006702820971799350934486788070670496482067069053407541677992333/1093077486501107764972553277934510438365520513026851632529222360819350800115942910448625391173501505510329891713943168065539630353437191773248880172373920524119429880062616890536419373589391533*y^14 - 25715926507056398037100101078096860559447645364040997011574180567679471103054532713086671941798167863634635620363484174485793640621974247826253975101200110522633888964224261105117176584930159702/1093077486501107764972553277934510438365520513026851632529222360819350800115942910448625391173501505510329891713943168065539630353437191773248880172373920524119429880062616890536419373589391533*y^13 - 2212728310619286835485301965894090269240532259189723965908202149550239604193421898734123039225744835867907915249239264025329816472125058065418727838795018490991981548280921237456726212416294958177/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^12 + 25912495448784672247318628693299920538913084682929471862118341916691727141275820161441140114680044640516203580603659416338349806499707017095528246092282817973626743473707343659588678485295464175/55580211178022428727417963284805615510111212526789066060807916651831396616064893751625019890178042653067621612573381427061337136615450429148248144357995958853530332884539841891682341029969061*y^11 + 4335497832216256858720404776659509439571182011847206047208193944112046851075141268963775724833519315801509534478531887163988049682183776251202327088080927447354206863592633619789604706557680121185/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^10 - 2871420265777982110521168419414915283733941081389083394131439400236031515673908384135051010123823672901564485630468730179973841625612887228341177057301742939704503784382846691181103433862089638193/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^9 - 5805975583056461512481264541883644701284611919694823396434183537101712740348683039887562104559894443369083865565196756359600045065272308820058090623466989848917976975577457826975618943621089099905/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^8 + 7744353569213756523690946833507717026077070138248006346509412386884991380933217479782732172444482442100788495262236478435302374757760521814249030589893226994624162314400843423563577774769887035755/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^7 - 199634580257478575994159642976261254949495115829585240882743003195452165683310481525624292847864034421446644677267962799944389760058274024927836843880306738577151374187513363911467431766810017592/1093077486501107764972553277934510438365520513026851632529222360819350800115942910448625391173501505510329891713943168065539630353437191773248880172373920524119429880062616890536419373589391533*y^6 - 1674302909863512969231183377473570450218281064174255945418188819617783904797457542045729586298068060594271491307911152709152641991977895774855748225518407755139739433413522128711964221756703434042/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^5 + 145598951321937656776698371235471393072934901232229543967361406367929902771796057291822694427489400885416624995326486060163472352824656702135347616006408971773403859568137016708120414408908905120/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^4 + 853532189338255768867585717783948637515822579020057127932806631459345871770773495469231982841763581401109936486349913991178396471866791526931840276118963434704498928901756696743778233142542884033/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^3 + 319122353769163653957450513253469917264671292065127923574833861387018818104426603122640446949924380292252814411080496911908041762800034074452380661335040057808407789459151939604538564636536189936/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599*y^2 + 316097283219194145347134614392891397149128316204287573199457919935304822706646929940751613178908301566341168915497788542652416136892589131036750529605803845491754751841436422899783128837228333/16314589350762802462276914596037469229336127060102263172077945683870907464417058364904856584679126947915371518118554747246860154528913310048490748841401798867454177314367416276662975725214799*y + 4245121460258954308371042670965525597664836920686287216885118894220442572992303901151679383043831972069035476888362939737581340670514385792738617899370939241973208886297541684668823973535410035/3279232459503323294917659833803531315096561539080554897587667082458052400347828731345876173520504516530989675141829504196618891060311575319746640517121761572358289640187850671609258120768174599 -68482236723880284202245737717233147926108239004509198994712169625376109605817447764834431201157579893480358466914646464642710263073594714489798931268186535684152028990660527115559384/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^26 - 7977013873662645980278132637558529058350817187984766321892717711300479918877436207093737063707336139594832418363494647313520880554380450347177821711118298552079880372066231894610071645/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^25 + 96719668439368016218866443741280301222380411520668216614721164826225833928281129299509805195157957169676262637382147594451085851536204945214984790982363602968502686058630913500902144860/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^24 + 109446178388502071288165767858986737892075223370252908199219835459051594021272497750640144512931252736657312811369354840599959672219539491562583193219014832957673800284817137645857414102/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^23 - 9368440463104219956050870959648491668315101681765737026236820973036163150051956113924644388211396102015131890444551430465482421587321357901358501989330601243937618671873181404704598784742/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^22 + 68903857398167464959472324313946095273662497001142559698233943961925932765910903757020815298596891092685715312957911250257455904764327877615154097446335342705288196602762483003306092098202/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^21 + 4425380897136266508347396953582109542111051199531174839661857060291157366140635754207285834463520030827124947760615456670430720527082948060176687754180101755265533069362322787768133090795/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^20 - 3490268380015140981722576184585058870610766026653840416159814554575722038022726389494082103245470284468604387988617526191127808167682708084157157199759221454020237361026747071662081546525216/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^19 + 24590477405073874283478458301555910028978737386454079053590530521702558946575683227721633675526825497002496585107401774288946642685294490766914449059324997603613136338335361835961808362457315/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^18 - 25419128290832380623216727819413461498687153969321795730229663563673579340986645274879967440700256095166723253813247939477312292691888747865266858582152292478254215420277727294372559363569815/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^17 + 63775886116868049723662812241555275001172318959642166334065634944134750459821100884539381013192819959961810007151464701958591136265500096758284644761520582818880300963778709777050060149676439/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^16 + 88389674031878129990079780168176784608728151317230272132356586637892131756049995528020102400040248955257929589378478198404334580337341603792665381850936170618290160850652385550533606205322923/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^15 - 256271064193494242178782892929086152505989049670258924625923985159671857140415018875585453581259522339558810355723346216912822916465158129283055552168278573110437497180472307840842616340904369/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^14 + 237365708941405261726986472863567552863566305599559133915976024863004818438318550364495229373363716545141081690893823471010124340332419025449532453404760830385541870338924827770548363788471549/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^13 + 530310971926296221472778346713890047877897375421244080521791258008216648835894513120687529995996350265605427768119309599851913509213050133557899808193050981718470697360104242410745505986579961/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^12 - 8573970813625866713362153108773873784519203257410388759763895272922730264069119812045665854379669196942666450562575409706211187700658558452785806787527422424577760060265040792180491626200607/22788114464133837116612531072081023169377290908892606010991355740808280695393560373769995854931546803225757118726273647831626542277757453525316992356701910149048926971931054486134621168499*y^11 - 2863319405705865292919792872686666162754112879747407272541455613308082432465118133476534409670926428570787569800489531744502045316264689598074370789505487214384603121875734836931595799776348374/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^10 + 947831124562556448594336340591341746751983962209160317094379855441669202268705450845735390264494821277274675374485687986777086171367709461724508673946740313718249953547361362417151688416846101/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^9 + 407626109656086036399971941819110161154571166338117087214842561772033089410549315809211158340495434657930972900426899183994869628129611425877998096081670545048590742588174204020221796618202208/448166251127965463293379777750926788997753387874887918216163329569229520342740020684143251813653753796773223334950048407355321998129229919331234183015137566264628897114644071560647549647147*y^8 - 6643652052812956602277713381258191461419633083372039162059569524312696951917869518572591141003239321048862609648463920138197262921420297697530476648044807896888194375666010285352862620167821026/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^7 + 1946097456349448731847388217950674677842349095039732384446532461432288283571165181126681732031625341710548871590722247418887657026873563984789276647723594150830265139644344574548049384209802858/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^6 + 895585999567909131921167125836310562661858022340431303271385213254207926798095975488591806017577120440452844974227967233747737535356475468884877225430869626962617347786246061227402031123479235/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^5 - 339168811265935607566569330712907695322062245404472028839159501421259446855397544308556142002240002660678129171713173185804723796297882485646319082772170534410705334167283701353797351303688838/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^4 - 6571518367190737389837224321287073424097441660458478257348683377114998252093498326518177988493971045294170963795464116741942140651599152157902662847316141754845143180478606646303330055287755/49796250125329495921486641972325198777528154208320879801795925507692168926971113409349250201517083755197024814994449823039480222014358879925692687001681951807180988568293785728960838849683*y^3 - 154311264262591517674421163640020099590462030928328047430910213508518182849781704653354549564146702821592047720880221771131758093200192295148410921584998724075224282545983746288791431507424743/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323*y^2 + 217848757611481574152841279166643859556235152936944494833739038871744595894334968412533989962227929495630099812708088558003713543537461707349674985129260134514693519128074073663481714687178/60201436718681927905080865668034941805668365535432705432021939792881577359472540091899839795863937077178492686784334860689520865420344317522106084285615493975845672746743233493221312639169*y + 11694199469341817050289601771245321082521985778236585936861208506781819749589946306146252749648757778894444687873422395729806744898588207588849157131139497810577305050138422419568014247337566/4033496260151689169640417999758341100979780490873991263945469966123065683084660186157289266322883784170959010014550435666197897983163069273981107647136238096381660074031796644045827946824323 -37810785074928874335513652450000895249379622080562706594147349446020234441726251660222388630928964171995651910072604322646780314193062608631183895589498005896382453669441260525173822/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^26 - 4418402113633331654094875401394321103546620136034983568816941670788643718262040155468151687563322679017602790932935563029954315658705873153009758176425216477994890074692349758552524306/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^25 + 51758386842510214994442378880307460046426528222835017011310026896308501264860868095822245219961494635399468770568088599721963249773166590664403975360431260057608654407672463998342883763/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^24 + 80120090542022979752873820930574459804214204563960223152392262629804747689981983875613212328793016617896885526717160510205290794290100524139067471676260247752264147282035256672494858020/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^23 - 5147553810397154296621730815031018442160647191490897566928077560284970912568881161771447855280047404351561464983519802657342113389244241530589935025206674861780314135143961431300339780757/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^22 + 36119203379856636408222462246725010460872961177052693003467876406063542024535162448520321329254063786984881333798740245851466445815423470584569648723685760079384656056662119237063749079211/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^21 + 7088161637304696508995982891334181406542450955423896932060482064984381661884113991039338607376778837352502271481501347267151707691092028058917279961010575807635079634837914974175688257038/615279090531613602148538338946187625573186854540100362296766605001823578775626130091789888083151763687095442205609388491453916641499451245183558793630951574024321028242138471125634771549473*y^20 - 1922578113613076089304735022204322488581098702750103230465132061844904200541759018156487055238919823091293108919006588402865435892813708773503429938236229541295679891513372609186647990548720/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^19 + 12859448772929244086772117613687054595457757747698045581854680132560019651559828550215292362856238885704997166364299806933175461094536589285416656449063174942324251222110755804873821920833147/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^18 - 12378120402775582735172782173979519082781131528870431115547146394831713013059435859559757022177984862230528099169192660582391063746722320559096483778894322123967312275148135651047716167330932/615279090531613602148538338946187625573186854540100362296766605001823578775626130091789888083151763687095442205609388491453916641499451245183558793630951574024321028242138471125634771549473*y^17 + 20148828701971568529768494770469352714689763904784622218813859769682537634525524362035421042189472220762162791735525987284863015442261861281335992253077001254599245911634281127779252787170319/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^16 + 52536638469190196012434554475688230972848428881841251571874880958654644961521977296259691171601437553940708213870176119571629105303260455924853999180680394426669610561357244784496110035618303/615279090531613602148538338946187625573186854540100362296766605001823578775626130091789888083151763687095442205609388491453916641499451245183558793630951574024321028242138471125634771549473*y^15 - 122784238617426779435641778915982492152714037631363028513670026989756768226772082247064839506767123191641873330390185706701856985674432808747049780297435725643038822611533987474585667152005683/615279090531613602148538338946187625573186854540100362296766605001823578775626130091789888083151763687095442205609388491453916641499451245183558793630951574024321028242138471125634771549473*y^14 - 20612480111360428273987234016862907209301211828789685238116947765826929637352370348472869859069379206984678681856994332334209197434535358787872361770911164370704699100852181972744408946524718/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^13 + 302929104327363465891136511263438158015142967523015102750693035570330885705215218748221176935121495750505103253786954841096575935170306699527508117470029648796696888442386117892505341181907647/615279090531613602148538338946187625573186854540100362296766605001823578775626130091789888083151763687095442205609388491453916641499451245183558793630951574024321028242138471125634771549473*y^12 - 168415920932929378713988294562264548959959145577513149814252669989759619158792506626880956868701429338569256813622578759051350146550052909887099567591309593528215667776539058476652818118873163/615279090531613602148538338946187625573186854540100362296766605001823578775626130091789888083151763687095442205609388491453916641499451245183558793630951574024321028242138471125634771549473*y^11 - 1857035232901497375344644655358828368702617916024411596207891535659097239982547976226069344613836287743313170627929540642042890552496504936034635313633667309920487880049016032704279539199612121/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^10 + 316573934849499083417775443576296982337963219592349381296641120936633749536434813159765274570133099527841363523332391286688458338740316005647900371998592320803933549370522616456336290736627578/615279090531613602148538338946187625573186854540100362296766605001823578775626130091789888083151763687095442205609388491453916641499451245183558793630951574024321028242138471125634771549473*y^9 + 282482348218203733341594606077463950531980411999868085911174952608074099587344727382858317960181271065189000360730149391191075248391564839539325736922258449246031528178188688172844380112950369/205093030177204534049512779648729208524395618180033454098922201667274526258542043363929962694383921229031814068536462830484638880499817081727852931210317191341440342747379490375211590516491*y^8 - 2862478303083532709670905418811931103709457610195859840830637261232976789038174557978617740853504548672074330716695812919997905429604553239673870779268587591489912800664389036571298405930152344/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^7 - 206591597963718865031431228247247701027323366111366412666485858015072951788024859458093956569866338858319982522671166460994533197189048721466818071359754527285795084532738440164762229531418508/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^6 + 758639672462348529019327373156189827436728306198327746731241401342451913431258585684685047912272840020753874042036909051164941786514270629912463769863800068119016237111776047515767437956145277/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^5 + 47852511962511725615578593149307675482086062650809484917307951960914818622387731344183479064415007184369861284459524022931139429022073211706404506385268210741175215213663311103994425569597677/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^4 - 1576319326183157590773978706337303585514940964843121550826974348813805316029546703280355616594029871225115498754025583331142538532323432138114191835129333240255679372555744007912104350423349/7596038154711279038870843690693674389792430302964202003663785246936093565131186791256665284977182267741919039575424549277208847425919151175105664118900636716349642323977018162044873722833*y^3 - 172557808429989657638514837529318391326428691158129330888316254612747012368876624802920985728655019288838360402352886050265503459365940569274970977979025800199706172124895197337077956619377966/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419*y^2 - 502982684630645052140586526153923929382479985480972246188073532614318754318871815128553968062428852002749769228638153385772938280139944360148177563974824991999710154531781226581900146934246/27549810023803594126053955475202430995814336770452255028213430074708518452639975974259248720141123747183378009206390529468085819768632145306726513147654548090641240070543513632491109173857*y - 232486370671020518248119312436654441011838910257182273541075790298979846123767289444569114634462051216536192199932255211985849956338514267143635957670673454990111427181886888515444644182906/1845837271594840806445615016838562876719560563620301086890299815005470736326878390275369664249455291061286326616828165474361749924498353735550676380892854722072963084726415413376904314648419 # A Gluing Matrix {{-1,1,0,0,0,0,0,0},{2,-1,-2,1,0,0,0,0},{0,-1,-1,1,0,0,0,0},{0,1,2,3,2,-4,2,3},{0,0,0,2,2,-3,1,2},{0,0,0,-1,-1,1,0,-1},{0,0,0,2,1,-2,2,2},{0,0,0,3,2,-4,2,3}} # B Gluing Matrix {{1,0,0,0,0,0,0,0},{0,2,0,0,0,0,0,0},{0,0,1,0,0,0,0,0},{0,0,0,2,0,0,0,2},{0,0,0,0,1,0,0,2},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,2},{0,0,0,0,0,0,0,4}} # nu Gluing Vector {1, 2, 1, 6, 4, -1, 4, 6} # f Combinatorial flattening {13, -50, 25, -24, 0, -1, 1, 24} # f' Combinatorial flattening {64, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 995017735633126423164152727686323165443061646701684304070692661156526941447170167406452177637548851483829535366880830946812989259397793479583385449285575210043988361762618109200289627/13444987533838963898801393332527803669932601636246637546484899887076885610282200620524297554409612613903196700048501452220659659943876897579937025490454126987938866913439322146819426489414410*y^26 + 116969055325659388290155952882860473394443350171134566662372136880823578523387171859265360155177538605680505645380189089084801526897213276686681710920520352035275613773632705120982819649/13444987533838963898801393332527803669932601636246637546484899887076885610282200620524297554409612613903196700048501452220659659943876897579937025490454126987938866913439322146819426489414410*y^25 - 640399331734290784844960016550511133277151195017869211220400735601516669239950204578444255598190815563369684006576485990859754867585365230372765630182719214376711323192241654597507339647/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^24 - 1532202287475564385379031218452973014652415658570101687897307881599878236072117127598229394168406954745917275380429929128031539133397015788919155024616482726830912594888514771529536882966/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^23 + 67011694177611474511260577528617991332071440090931691441715767666746874461906623130128729459610790715359041261412207652961971193678009596759554378569323589749089477375309310539475802310032/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^22 - 427821628295403644693240770908400039316859979692783059160621983796994160037020733619844423964445570466519613892774388127171250938468187726772375953803210118171386657347367498879040331936512/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^21 - 136479773931654184019683076834078599921811259606001110715737809695441333851668822713946973258422024459561475270137100467055543321407373129881674596563051838304331146634929334305060559253749/1493887503759884877644599259169755963325844626249626394053877765230765067809133402280477506045512512655910744449833494691184406660430766397770780610050458554215429657048813571868825165490490*y^20 + 10044900456155710366514425957829742028334213986550887162716955692242318085524571090739461012873129244686320538866170260063668894627308733337777212544486666667713372620055378603046857176255867/2688997506767792779760278666505560733986520327249327509296979977415377122056440124104859510881922522780639340009700290444131931988775379515987405098090825397587773382687864429363885297882882*y^19 - 151476528233764839221314629437701749893260873986060854112637087765223115800352298332894508431611851253102870836616159650442694412933903586259871084400775562530099124554021867511045832905457897/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^18 + 123170768434911016171910138712202288831874540108319057944733480672775635887180322215045427735157030829694442280081807708945099819127592209829573523490719952812810286819332058303580604790367601/2240831255639827316466898888754633944988766939374439591080816647846147601713700103420716259068268768983866116674750242036776609990646149596656170915075687831323144485573220357803237748235735*y^17 + 80293623167512187214048194746698541723680741392679862250324176347613325399267380112446003867509774108942326170901036991453844722010180951542642709995631352413119414005312215649274329641433141/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^16 - 1508893281359514377485906949264524793541347400203147853865756471677756455218697052057969455850004692212219822852647781900856309109285060880367411324528063081149622222728549434494408867389763323/4481662511279654632933797777509267889977533878748879182161633295692295203427400206841432518136537537967732233349500484073553219981292299193312341830151375662646288971146440715606475496471470*y^15 + 2245674430279096775924953243688562692664734520291853255877490027700213731835732004388401030105039180410194460704754291843893747600148540305844341870433541440783639316397422918689459518845589673/4481662511279654632933797777509267889977533878748879182161633295692295203427400206841432518136537537967732233349500484073553219981292299193312341830151375662646288971146440715606475496471470*y^14 + 1505376373617438726506890940657058873332329708003520859859362942840122745871094119287916320328396778278067462903212261860801982831103646636544119200674866197140179496839335166168808739301360307/2688997506767792779760278666505560733986520327249327509296979977415377122056440124104859510881922522780639340009700290444131931988775379515987405098090825397587773382687864429363885297882882*y^13 - 7874859590930328676972795714152098470844713043505199525933800361752740180198169635860610118991380163067663744496235676402017811901950618578210597302474912114231917889663933004308362024907766067/4481662511279654632933797777509267889977533878748879182161633295692295203427400206841432518136537537967732233349500484073553219981292299193312341830151375662646288971146440715606475496471470*y^12 - 2638081698560806772962258666090097855832023322226918378725653441178589622916776899970477080051007423122435836430969161799270388703115240963400097662536206881283346822582999041730146103048413/8440042394123643376523159656326304877547144781071335559626428052151215072367985323618516983307980297491021155083805054752454274917687945750117404576556263018166269248863353513383193025370*y^11 + 29680822485993488743369760897057595601645282590926842969263359994058729242477419871280326058464044228614922317976379698382490087512982941212482229118022757248692005887493002820836131531746295397/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^10 + 1688434461225879939526973444432639387354060423153658450927680963644158171947759220680597360078771572074472827755969514327037320762548381452456587179916003217745570262296206820347715767372229536/2240831255639827316466898888754633944988766939374439591080816647846147601713700103420716259068268768983866116674750242036776609990646149596656170915075687831323144485573220357803237748235735*y^9 - 14645379089962447100323032290986601895342826326698887635273010887916841521937688411447090250631075730127527777706653021150167973666401942818810660022227302989116881693138383521137163163414522242/2240831255639827316466898888754633944988766939374439591080816647846147601713700103420716259068268768983866116674750242036776609990646149596656170915075687831323144485573220357803237748235735*y^8 + 2730157780341935680663622329833331173166504639999088957407177232686930340509381841915659953071184324559024580837005162871769352230195394913876114506476025999481379113262878580477394311642059177/1344498753383896389880139333252780366993260163624663754648489988707688561028220062052429755440961261390319670004850145222065965994387689757993702549045412698793886691343932214681942648941441*y^7 + 31961719155219076263507514063170603393775747008140073980572957606172333455209018876661784693324662726113817391619658761552748146799585368117295955166467597388181198203362913578730475019815394254/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^6 - 8222159640000161157366846793568590350573538865202534154892013020205095546043988775802140857309138704192728073227292660614190372589943077814477915287289609166800664352335519586806781017203113238/6722493766919481949400696666263901834966300818123318773242449943538442805141100310262148777204806306951598350024250726110329829971938448789968512745227063493969433456719661073409713244707205*y^5 - 23194269617997013749545974710831270964849152376137882556360267195112620173174246219493617312070178455743904989029993276532131494540119421736608232858855535484264240853039534188142518488163538111/13444987533838963898801393332527803669932601636246637546484899887076885610282200620524297554409612613903196700048501452220659659943876897579937025490454126987938866913439322146819426489414410*y^4 + 2296581068057902085290614160234002150987266440153049672151197841672263165428587569469554908041037121261465741400310085217620056242397763470581963244169980196394317817394277887038794743674644686/2240831255639827316466898888754633944988766939374439591080816647846147601713700103420716259068268768983866116674750242036776609990646149596656170915075687831323144485573220357803237748235735*y^3 + 13315685633073503718807936855863160287022423292853399947597909220863799149962878986392367095964590036424237614545930153226953209603231664826816777373128761897170858087640773327680054523486337059/13444987533838963898801393332527803669932601636246637546484899887076885610282200620524297554409612613903196700048501452220659659943876897579937025490454126987938866913439322146819426489414410*y^2 + 35991563441911498473293923480704615877217354596283944306825889661172538271831424071629854350637370500133269986814921853072058582025280664192676139186165651824121040899478774080115091939422307/200671455728939759683602885560116472685561218451442351440073132642938591198241800306332799319546456923928308955947782868965069551401147725073686947618718313252818909155810778310737708797230*y + 3619439313620755480995156920170025223124382850569256428643641133110049633545416830175921369734618530982663608647053453274710657613616996193433381176976281172096098119514656129314237409807167/2688997506767792779760278666505560733986520327249327509296979977415377122056440124104859510881922522780639340009700290444131931988775379515987405098090825397587773382687864429363885297882882 # 2 Loop Invariant -7501452477103580637038252931860148412559385205020348115768059187340249184997801107712254744525039399598638042401877104212246825923993063281011877598073376029005021375592678065771558460062612122908211714565831973632893921644436872755266842035071584558886471999001517/3011712861880139027223611045034947880801528095944565396787816313721957962672654212718028855610302353002100762805510250769949039195711690489250180559026278284570710895163915687588546162279512988434580083273284530010545390098820247053558848415632459260694482079120669173584490*y^26 - 63140161346530457540013002965382868313938384627110117296525659617290247872029983036113020479397411839305594419651722903732728911877736247047035670826908705712642379690106169160272081945034330522930287631134147956291515530780607148091679759715987299397189284558265615063/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^25 + 736320555380662114450433612720640939343141747552487181969299487335093284295485926087449308491856492124840411885334918480912004209054010898901968343626151343899135713098528246985395720323173553380632372958537235190491688144463131706517461644224212945479365352831764657563/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^24 + 1181230458719642900358900568598942015710730540302051532310611279757549366341704835004660896008646360445938314277770390147891873907343209201113329447389255939204469276203852307759441891657629823010541693046213689836125031221775642315763408442094467361564826061324966502579/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^23 - 12248438732734207511152429743166239561933578352517852850396169384710109852319101942438929608045700315445754512640726897433458830822208446226019025003111523370446790857187871877477194023144989381280238727789824075902861838674359885835500173829189586141348946216970197682013/36140554342561668326683332540419374569618337151334784761453795764663495552071850552616346267323628236025209153666123009239388470348540285871002166708315339414848530741966988251062553947354155861214960999279414360126544681185842964642706180987589511128333784949448030083013880*y^22 + 256198818114962863365554305866526560568199589809227837226255765701101560647027416790243635196866430024863978877072825474846270683734962123548145623561732246406147021510595761363190896097393342665754998035437129154806246480943357116536572776731620888384564658823309878676729/108421663027685004980049997621258123708855011454004354284361387293990486656215551657849038801970884708075627460998369027718165411045620857613006500124946018244545592225900964753187661842062467583644882997838243080379634043557528893928118542962768533385001354848344090249041640*y^21 + 165011063181159356819029214641777966534348920054933669653707329695996807430269389745386560842529029912542793376220729517572809041649466172534994490630245251747367910226642343261537465938581957515279888122009962218090764840239284077521117465816967688523200334019768260021591/108421663027685004980049997621258123708855011454004354284361387293990486656215551657849038801970884708075627460998369027718165411045620857613006500124946018244545592225900964753187661842062467583644882997838243080379634043557528893928118542962768533385001354848344090249041640*y^20 - 5491928459475340802304298832470555889728237423256471865318965674022078434441188840739152135680963209224546285760924389349228450621510436880700404821162863162227600854137858608716228933989891173272816786723336678954072072098948050578807119164110120305785941345630032418607887/43368665211074001992019999048503249483542004581601741713744554917596194662486220663139615520788353883230250984399347611087266164418248343045202600049978407297818236890360385901275064736824987033457953199135297232151853617423011557571247417185107413354000541939337636099616656*y^19 + 3799400171723908342799725466448368383026255771044113031856147923441388743331160709991729896976615649395500173947703564623096142179251284848196740501809066977891805971437974512688144917165354055274855747306387473883844105283467289132213300449656726094371489710150841033889966/4517569292820208540835416567552421821202292143916848095181724470582936944008981319077043283415453529503151144208265376154923558793567535733875270838539417426856066342745873531382819243419269482651870124909926795015818085148230370580338272623448688891041723118681003760376735*y^18 - 521064652346763199364422566560066511600255159702220774257622293077522993654796978795572939977972514084332034035968570118155859556868534880937839063082912180505874560944792485228771365533673303472576978131864220095913275495663306609089932539279859869540542735291701502545228687/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^17 + 258316331870803025624290804623315407521025665829276582516937666992460189879205039362680023094146241779900798372726930883355422738660454606669483606858686572082737054119301030818378935220306602855736332161358241716214524110218832683692679577438780910711760102767310508615649201/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^16 + 189835924634571896544174385396475602319965093400314788523917823187537679735864680381586693827090713586999039244053359718329812305456014711123156037314833850077385049687139656745040824609308329454020697072539507739068236544449749820396111128659792927823855519082624038733739699/18070277171280834163341666270209687284809168575667392380726897882331747776035925276308173133661814118012604576833061504619694235174270142935501083354157669707424265370983494125531276973677077930607480499639707180063272340592921482321353090493794755564166892474724015041506940*y^15 - 143493438502275055324145980136178087161380582186380484606792079954789241697142945357117093576772697303212481048515603524360476974841044206393413144029668862358695023230977225850517840305371353029263430186133953345390449216402638059578163545881848417614691752267415439284781873/6023425723760278054447222090069895761603056191889130793575632627443915925345308425436057711220604706004201525611020501539898078391423380978500361118052556569141421790327831375177092324559025976869160166546569060021090780197640494107117696831264918521388964158241338347168980*y^14 - 483665641327531277719051789945824461148909732916379168473920024868873126207837718315342295121186743590938345517231635765977048540538570344575377747125202025175071301679704359089326737241308719480407766483816717009152324074810525527216902953089513556567917407739520290397965/178471873296600831242880654520589504047497961241159430920759485257597508899120249642549858110240139437161526684770977823404387507894026103066677366460816490937523608602306114820061994801748917833160301231009453630254541635485644269840524350555997585818932271355298913990192*y^13 + 3273965737047325748819410251128029187193601532737345682415513226308314760778057702948532246351908693735567263113002422047107525418207826680446974866500980213926610890175074228619652654060224179067161470995962718085617094024220096383223556985547253271501914854022678884406184043/54210831513842502490024998810629061854427505727002177142180693646995243328107775828924519400985442354037813730499184513859082705522810428806503250062473009122272796112950482376593830921031233791822441498919121540189817021778764446964059271481384266692500677424172045124520820*y^12 - 112709112343644335989972757733070086981447593268947584843655522983970963962283691754276418160515731162123426308056962831600015274016836119474722337240810948554317593740690999442181438140798548000286067821889295045923015414420710173068505000621470218081108223088555896331810293/3675310611107966270510169410890105888435763100135740823198691094711541920549679717215221654304097786714428049525368441617564929187987147715695135597455797228628664143250880161125005486171609070632029932130109934928123187917204369285698933659754865538474622198248952211831920*y^11 - 27117001924433742512746464111367257428543273096991037265221554495099453490268564129201721622283666041858137538539970242196513925465391024221163084250861487552990314071897483372741654334053956071030057571900679050072702744371191226100596044228390102088111792297972300230102877603/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^10 + 12563178670152167506571850955492351508605788627981318648595183056216258764557258505960392102500638429403534662307175787854420305903206955746623506256701187492116245889374256974974852031538229013959492795262043673642214817497497678306025750541775713963839989248830755277728202473/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^9 + 37386997153712301085568981680129107033579540533841144189527055359206738239367716709898075382317539197253013452583103982717951697403562218083001928730373116532922593578090398385717550756560001208724444950605061164165471667949008029360217540613700642447081921721824243364569630799/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^8 - 1981992707085397491791560246905281618427821464714861038757814895377050259616897437783347157253127800814967630658766145798964659704090268605469971069554041951269587670111671875018950798343877662423775874106829198638561397246672687813865281280967674364050778523303196078075856119/10842166302768500498004999762125812370885501145400435428436138729399048665621555165784903880197088470807562746099836902771816541104562085761300650012494601824454559222590096475318766184206246758364488299783824308037963404355752889392811854296276853338500135484834409024904164*y^7 - 1811296946111285918147077934583487541685402190252927625749412936236898567460552167179876172781261615769159341538566318974723173222802503703363804176058623355522481353203458177402229790027172810001737803980808181597050046584867720022669938094699083946235302657312324883107401557/72281108685123336653366665080838749139236674302669569522907591529326991104143701105232692534647256472050418307332246018478776940697080571742004333416630678829697061483933976502125107894708311722429921998558828720253089362371685929285412361975179022256667569898896060166027760*y^6 + 737111453404205128879537331955139592624169230282686107334004888639721419714911273750661288624830771075886008080420842025460383113856590440025026864507811031743807866462923062920038752403549733985341463940718210261778801453541163859583429379337152717336367363075215889809785662/13552707878460625622506249702657265463606876431750544285545173411748810832026943957231129850246360588509453432624796128464770676380702607201625812515618252280568199028237620594148457730257808447955610374729780385047454255444691111741014817870346066673125169356043011281130205*y^5 + 733830523304086978794868116375435137449209373035541992814025477790956631959993562380144510601383655463643346251381705669236812519804687656630150315363355781546067956236997531577084267066848031444244607614457027600914570535005578233380909855938167836882331855248475197636991087/216843326055370009960099995242516247417710022908008708568722774587980973312431103315698077603941769416151254921996738055436330822091241715226013000249892036489091184451801929506375323684124935167289765995676486160759268087115057787856237085925537066770002709696688180498083280*y^4 - 1366712738160857825917545780218317536195872435497696589276569112034330123511907864340736423957586707486369419752034972102117321881797300542762695602360909517669524818243005381440074080818269004681196799216645736218010184559963657917913289217474441977208978683749029832278561293/54210831513842502490024998810629061854427505727002177142180693646995243328107775828924519400985442354037813730499184513859082705522810428806503250062473009122272796112950482376593830921031233791822441498919121540189817021778764446964059271481384266692500677424172045124520820*y^3 - 1359927771838171200239503688684765991389716814658335334923377945607924409134754105854967238262159550438990780964977255636900897661347651464263130264723125068029695268228066440348783229678167846714703674498515627687908792282118170055309516030449450824153043549567043346362494369/108421663027685004980049997621258123708855011454004354284361387293990486656215551657849038801970884708075627460998369027718165411045620857613006500124946018244545592225900964753187661842062467583644882997838243080379634043557528893928118542962768533385001354848344090249041640*y^2 - 2574531911516415267442398425382234814724945212937938167992417656044724293464634671723096325902035641183473378834481917721149055691605554280978877070613753202229280758134054276459236207794402531665298054279509075093891814612100358701018847659648143994741401656018975188930913/1078822517688408009751741269863264912525920511980142828700113306407865538867816434406458097532048604060454004587048448036996670756672844354358273633084039982532791962446775768688434446189676294364625701471027294332135662124950536257991229283211627197860709998490985972627280*y - 1147765832326319499363312876359345789327942686815497354595381859824060367484740935402478629424121135989399440551238196554725935082308714284618949527583925773508587244885912858966330043056926283693299763892400109742262018525764823151824254714827046261658898653520621695852486483/10842166302768500498004999762125812370885501145400435428436138729399048665621555165784903880197088470807562746099836902771816541104562085761300650012494601824454559222590096475318766184206246758364488299783824308037963404355752889392811854296276853338500135484834409024904164 # 3 Loop Invariant 1978950175227512730187571219834414276754635003164689330988300634568655631859763219998938800446662044601996948387086008192412332335033449235761489146900817461704177127758242189421763538764966566570544940150886632160575345328368935808536339277277308871625060728878369133465401755770693394270072763080245339450597/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472*y^26 + 115506262726841867895277310313332596776916662630611588626660563001369836760411371101956747456934270335664039193035463452813753923921331078812114473286470588568810766742849722645302170684697558182700353192608080048549531358179755083769036307775837173374698080889857136552051500817069751464009213739864409288339561/369466563184221350721106894593883694881087053076921055830540717940392376141846491094936630475699666942847338905872789077412022447383757395859844559455371133996158304070819942775461435359330784641960524314471276374107444768222710233527940557689479812221567030902003839318247976666455377245771309151648159366552855720736*y^25 - 1368403450876107854622081432568442980617956488705178948882954409752288871357410654926951832813548766237137779756092612722355915563319768241144502278469645988092876495918144456910139642611566341633088901210844747830667723592215807471895107566376612550536053938569182970453444807231349928121005737488758577021013945/369466563184221350721106894593883694881087053076921055830540717940392376141846491094936630475699666942847338905872789077412022447383757395859844559455371133996158304070819942775461435359330784641960524314471276374107444768222710233527940557689479812221567030902003839318247976666455377245771309151648159366552855720736*y^24 - 3860242489592813045096887523781332789415337513386535618463470019019452686117275499436235438447903265441153056135976133416871923149913378965866039335558113129179316379066554732060918851897764865193406976869548891299097171869679480516475017729491856503911852403825903209746105720095990968365416153316486704908519271/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472*y^23 + 134924160157511051409221662683527302528462135592685799402425058192130175925169521701596659075416651931065551800377503219355170356114002612483627403176235384605297253329858236965739949815126679718338252225521313097941146889223282407274001017246068577044450329528844271860493462695425446846780230854407493696253476725/369466563184221350721106894593883694881087053076921055830540717940392376141846491094936630475699666942847338905872789077412022447383757395859844559455371133996158304070819942775461435359330784641960524314471276374107444768222710233527940557689479812221567030902003839318247976666455377245771309151648159366552855720736*y^22 - 1923044502536575370283948214176819168341420811843497436436441736613822985796968529249661560610000848077755567980087546283848440823361747206745009862454175716091394205593004859591931674791432318574838248925148580306349856051471050995977146867311807123710665637642875005081883986466820910063778201056781180887789476257/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472*y^21 - 292541788226868688844857631243659802379788610050615545180558869042989132277239208905194228098167477559019752488469315386202360780732220890799362297236966318638455377782703790457259713780395056547524281041787848633449824047730104244016054529445213528197425162396126201665636529777882161101738751031137619535455876189/246311042122814233814071263062589129920724702051280703887027145293594917427897660729957753650466444628564892603915192718274681631589171597239896372970247422664105536047213295183640956906220523094640349542980850916071629845481806822351960371792986541481044687268002559545498651110970251497180872767765439577701903813824*y^20 + 25177100213591031234013573566731943614878425121280010573915989562831428244263920403009840721033589494546274219783014608313744654890577736568509866963617218093078340512251276387683955595401753516872595747792298930458140260367738991132310938696868708882566815838080588265202894811981643405989647453058526987051735830051/184733281592110675360553447296941847440543526538460527915270358970196188070923245547468315237849833471423669452936394538706011223691878697929922279727685566998079152035409971387730717679665392320980262157235638187053722384111355116763970278844739906110783515451001919659123988333227688622885654575824079683276427860368*y^19 - 685214649382460341410177761382562326354894265145334649935302709541401483333163877073695706529544044270889374172417163958391623785576997250854504648764859254818304059598583538173668609817584844810631695471064205610516156673477930122980371593837776981968649736984434395422188557775427305160610088419887108696198268835815/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472*y^18 + 112636388427220741896534846652415974270182735912561072335422422023881855942474660187050089636198021081094757776912921593812677496219702292868735559979018777632962422008722476732668099905168892387492415854756726603824390389040982843124927644591451915152067752514610445726677810044861194843744103970755977134436011937423/41051840353802372302345210510431521653454117008546783981171190882265819571316276788326292275077740771427482100652532119712446938598195266206649395495041237110684256007868882530606826151036753849106724923830141819345271640913634470391993395298831090246840781211333759924249775185161708582863478794627573262950317302304*y^17 - 1307098970656424097615148682054744228860604648843409997036622363729335142048498147381620738340779228103380609653615679502189328579194659308629173900150263276154467336186125757085401168478454595142647864002229820837188901222758918813921495066170445555817083798109339730833990959014586925232674384164643794798674634157675/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472*y^16 - 2689860844222035528013862037112926830681066858941345602322664480344155663221129854808984997201115791231740936293700342445044100542213468162471914867429965221843024552991880053507730430072603636432833296063098176790685854002234607097795836391904323795423712193639369667896285617470751664518064597405151806964182038040971/246311042122814233814071263062589129920724702051280703887027145293594917427897660729957753650466444628564892603915192718274681631589171597239896372970247422664105536047213295183640956906220523094640349542980850916071629845481806822351960371792986541481044687268002559545498651110970251497180872767765439577701903813824*y^15 + 3374303498716624308687381395691496117184502198655816473327341628125582043062352320140572727927783110350967021496425765534410419489996356158004949214032719815493893132172687875548633873909098529770258268182693659129210699677751938930481303743023040769880542316455353972685739574547369947819917202927589432585185683930415/123155521061407116907035631531294564960362351025640351943513572646797458713948830364978876825233222314282446301957596359137340815794585798619948186485123711332052768023606647591820478453110261547320174771490425458035814922740903411175980185896493270740522343634001279772749325555485125748590436383882719788850951906912*y^14 - 23002647307445708317429080806054021548059737513975866334931013442878735300477943024776736436673416474871459395229263493589249710092877955635283036186982669006202683501100492249096532918764384168387833655325232358432953216547182970758650987783354627045720111056260601914933659536790103254425200894982810083864377270015/11545830099506917210034590456058865465033970408653782994704397435637261754432702846716769702365614591963979340808524658669125701480742418620620142482980347937379947002213123211733169854979087020061266384827227386690857649006959694797748142427796244131923969715687619978695249270826730538930353410989004980204776741273*y^13 - 2620154078340858902666883059528995343162277293131170318892242044009352287824821346443408006926474791167392748402640465907942148441895611310159362420884870893181265686433117124039298892833333970716159897791911442028434096606365754560496987010162035906307444018559512951619061723927508558192922739801756148058035880553195/41051840353802372302345210510431521653454117008546783981171190882265819571316276788326292275077740771427482100652532119712446938598195266206649395495041237110684256007868882530606826151036753849106724923830141819345271640913634470391993395298831090246840781211333759924249775185161708582863478794627573262950317302304*y^12 + 181942949541355478098591218644036310691896380099746287806639914363228256944402921840810372423219065320018298696128220517396766499373933067037973788474727352525441202823026768438104644310889643173002871241895090413124302104334121186910426808867252559708962791367269641102975460828523173703806470441201507355672722872859/4174763425810410742611377340043883557978384780530181421814019411755846058099960351355216163567227875060421908540935469801265790365918162665082989372377074960408568407579886359044761981461364798214243212592895778238502200770878081734778989352423500703068554021491568805855909340863902567748828351996024399622066166336*y^11 + 46330448768271654247305649799177619504682398301786631163190486298718947957733779309255572622706414067025616951865799121347090419299761219000190684656309737929374909401108838650550574425235244849033561732570337459116950398996434424248371973129774482171135279217182060404393468471331608889248476165360011989908802730180923/369466563184221350721106894593883694881087053076921055830540717940392376141846491094936630475699666942847338905872789077412022447383757395859844559455371133996158304070819942775461435359330784641960524314471276374107444768222710233527940557689479812221567030902003839318247976666455377245771309151648159366552855720736*y^10 - 3367499597115987164898231738395443028304442036750663254294795783671148920436338748525619618157178845427755288443970076924665081204670237858332654589962116681530024199587930416491045303788498915587612821616248020912344361571251562913880036174208867384260042370236484092031541725666978172657803816737106412449588584981217/41051840353802372302345210510431521653454117008546783981171190882265819571316276788326292275077740771427482100652532119712446938598195266206649395495041237110684256007868882530606826151036753849106724923830141819345271640913634470391993395298831090246840781211333759924249775185161708582863478794627573262950317302304*y^9 - 647832935305527490342526433899357346226210158211935310350885538681490598716001362977429764335224680181622759917317911877864611730218367632175713431863775728895840214150986520743125546277567365893233239345534162525136014384656795621625072075481309867079584564117500104462683101176684291653753210569626951024929752783974/3848610033168972403344863485352955155011323469551260998234799145212420584810900948905589900788538197321326446936174886223041900493580806206873380827660115979126649000737707737244389951659695673353755461609075795563619216335653231599249380809265414710641323238562539992898416423608910179643451136996334993401592247091*y^8 + 82099111079124158799561746468629938947145012673489285637392742476173140374572632037053666061119858024284270505427028482783184559210420399179995494455291937039410893769614388161362626362926607062782745801105915463553997750289395552605085784050984664627029866094875488147189852636728778408525530973201143844848663805123491/369466563184221350721106894593883694881087053076921055830540717940392376141846491094936630475699666942847338905872789077412022447383757395859844559455371133996158304070819942775461435359330784641960524314471276374107444768222710233527940557689479812221567030902003839318247976666455377245771309151648159366552855720736*y^7 - 2741988746593230707033998074425978016503078080345760399856427144708604230702444943602976166364277543542081936220277288706544076420388882437210912106537529288913658049954292773852340627298243001699536412114020547919235969220524065963372411049129105505340047290477127075106315481801731056758938041414903603928616015058399/184733281592110675360553447296941847440543526538460527915270358970196188070923245547468315237849833471423669452936394538706011223691878697929922279727685566998079152035409971387730717679665392320980262157235638187053722384111355116763970278844739906110783515451001919659123988333227688622885654575824079683276427860368*y^6 - 36462957491417957910390141795336251940443210584990750537472394028345023434801681787653522332441071890716786903563899554519209658427617354303802673757722728501991154370047908403702827104107357096074712381016035471748856576823319181067737987540292755512509312348579372967720492101437017937457207864237954585272593422707797/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472*y^5 + 2659904112787915217376166263266555956199822461422685729598255817198492225147537205412779639132625125857390973970778382946767645359787551665702500428113133193809133124940085929968298185934856163997791198796847589465927133090119434917412392885160657425351983873719335108825177084007244674428260171269808140042548107837999/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472*y^4 + 3092442811352418024484744020539634828749820908349900721454303639340654273360105241935789122493700514164567015051389308439600409984192752434813086527597435910642999923389322707273716199356382317599299745350874429539567086523296912793236221991700373046349249548882653326468810229984552316595638087717949315439830394780865/123155521061407116907035631531294564960362351025640351943513572646797458713948830364978876825233222314282446301957596359137340815794585798619948186485123711332052768023606647591820478453110261547320174771490425458035814922740903411175980185896493270740522343634001279772749325555485125748590436383882719788850951906912*y^3 + 3450262186488660222942983111671241081940830054279731333724473470557637968039436762914085900816610108479566736874425998130044131629633810005698971518027896533902326886335559885616461624398833311078803700362620761770378730996422350858742456623833779358025401131656556669235957825939981522812632154889396532497072979454873/369466563184221350721106894593883694881087053076921055830540717940392376141846491094936630475699666942847338905872789077412022447383757395859844559455371133996158304070819942775461435359330784641960524314471276374107444768222710233527940557689479812221567030902003839318247976666455377245771309151648159366552855720736*y^2 + 1175928662008715937799560458911977833372805295841980782802355729971932956633528830407649516998510224694799243030899662668705718787939738359387474431719625715222810565936718732989654447455729214069740596414271605772765763747393496476743366507838052653577742219421029258972371980424637988183817616598825022970781235049/689303289522801027464751669018439729255759427382315402668919249888791746533295692341299683723320274147103244227374606487708997103327905589290754775103304354470444597147052132043771334625617135526045754318043426071095979045191623570014814473301268306383520580041051939026582046019506300831662890208298804788344880076*y - 3500754301179368128556855072379890537245440103774013343972884513266935333972688649567125113303272513091651551496117329256443708228398855555241434382125660077422433404666873036588407418833741878186428968747581681296814021933936266880156678891090328392295654597745225451785151500503373523621445464527595953143778581529/738933126368442701442213789187767389762174106153842111661081435880784752283692982189873260951399333885694677811745578154824044894767514791719689118910742267992316608141639885550922870718661569283921048628942552748214889536445420467055881115378959624443134061804007678636495953332910754491542618303296318733105711441472 # 4 Loop Invariant -44139668848695347326178840448346580790293856376080753898464108580299710263047851852415878791341063535503357705411678481131883065269484253722082285298268074445835413991450709503926196217611126860749430501801621708071008120947380605434042918792547730815737736887439267635441597529357600638764623710051980120077239803904116350767993925160650158924418792749814661750126808203892110503085490543410369/99313787914730966540533675507304744032362793170867941076719764877924808502501608068638652323063864092962236797442787525317765280007321218509355588507873635539371475747360931939192860227429711023028313069092026580305027966205879077426191630063270631272037052941561694968925689677414772845015459424809795528278957866884041185609712392325056453292377504176259262748632096928945529271176488564154059797644800*y^26 - 570166106541749471072258830959835337992944602256380181547708663004202333616560429708102552084316125382589383646217295611395226088145841815131541972239717405590823118279256971603336062361659710144044544520840863112316312075187646124020179805793970967915626473790486602223217763402262395320963494824691207754602181877751784079215130950482262000233144871055284160684305651555516988525465053823047357/11034865323858996282281519500811638225818088130096437897413307208658312055833512007626516924784873788106915199715865280590862808889702357612150620945319292837707941749706770215465873358603301224780923674343558508922780885133986564158465736673696736808004116993506854996547298853046085871668384380534421725364328651876004576178856932480561828143597500464028806972070232992105058807908498729350451088627200*y^25 + 127025792837180023248880442173117238380610760892514147084984832864823329902416567299899501484478719200337785961973166595408281143795953952586658953576283416334980428175819843611862195135363567359501032695856746575969397067507803724126005507242686613565006479492022876235645753994671208957113515278158896490447473458897505017242550712097740169270483010248763538844812104100557361272670768379495097211/198627575829461933081067351014609488064725586341735882153439529755849617005003216137277304646127728185924473594885575050635530560014642437018711177015747271078742951494721863878385720454859422046056626138184053160610055932411758154852383260126541262544074105883123389937851379354829545690030918849619591056557915733768082371219424784650112906584755008352518525497264193857891058542352977128308119595289600*y^24 + 7125850056140890976896272309567064842251470156205199138837608410960774650417974524878581874706002794604529868647484476894569841790989119087671023058762341371548333574056150184990525846756105029750309664057753801219846954132136649481018296075667141177244791096308973864272971674684764907848511737757691088453507263738482100125615547431493552633481318826646573387561997275387205260098283200990345583/12414223489341370817566709438413093004045349146358492634589970609740601062812701008579831540382983011620279599680348440664720660000915152313669448563484204442421434468420116492399107528428713877878539133636503322538128495775734884678273953757908828909004631617695211871115711209676846605626932428101224441034869733360505148201214049040632056661547188022032407843579012116118191158897061070519257474705600*y^23 - 6061917746713112518994767866145571027611975968462274749866448932632106210491089008344193984156456930946980421776308435703572074328246066511623295098629084750215896583513230793484339491752688507709217217234222752272808971315617180752146269505889182154587974687982500702530640047341462241966733833521653004148698885074338936946073705492430431264295194306989615892210000515931610490937788855519432146793/99313787914730966540533675507304744032362793170867941076719764877924808502501608068638652323063864092962236797442787525317765280007321218509355588507873635539371475747360931939192860227429711023028313069092026580305027966205879077426191630063270631272037052941561694968925689677414772845015459424809795528278957866884041185609712392325056453292377504176259262748632096928945529271176488564154059797644800*y^22 + 3390685107109268816325743298358018516624480330826942331805704082534338738893408906467515411575364881018279189073512634698782758434127965411222777190722814037687593679517617743660362682964813079194050690479181006892707240932646489498888195203269091998717961536751328943481632425973591640000210496212308574043107192727796543685519304218784075979293574260556730888221425306131817011049178005579464556413/7356576882572664188187679667207758817212058753397625264942204805772208037222341338417677949856582525404610133143910187060575205926468238408100413963546195225138627833137846810310582239068867483187282449562372339281853923422657709438977157782464491205336077995671236664364865902030723914445589587022947816909552434584003050785904621653707885429065000309352537981380155328070039205272332486233634059084800*y^21 - 798251613354499203319261164068138390440269629619067164244670186751971675405511794805191179532624940728454214515778768634548328637515909497613066898936200007765377902331926355035996283756501664124054576620860325201168370795283191676739323397673328969127741335533063889207148056575233105860367964144935606860931226021361764356071760578378018886388495821542960273914499730402324666719723188529546387203/99313787914730966540533675507304744032362793170867941076719764877924808502501608068638652323063864092962236797442787525317765280007321218509355588507873635539371475747360931939192860227429711023028313069092026580305027966205879077426191630063270631272037052941561694968925689677414772845015459424809795528278957866884041185609712392325056453292377504176259262748632096928945529271176488564154059797644800*y^20 - 60185158240295871054672954262809166325313181348043281588680108737743429173027943310591490796746347252128668624323659726965244834999978438819617669149762236900387583905761613279786514969978408865569635862127448155723009553182830687295266091327523837598263209383428697038489482126295535124366813215071287529459978189292673828178459491558015032985269859250342965464306981599132399178533654355373980362379/2648367677726159107747564680194793174196341151223145095379193730077994893400042881830364061948369709145659647931807667341807074133528565826916149026876630281049906019929624851711809606064792293947421681842454042141467412432156775398031776801687216833920988078441645199171351724731060609200412251328261214087438876450241098282925663795334838754463400111366913673296855918105214113898039695044108261270528*y^19 + 1363288066930297734535656804775141697666549490032863137613940910154615671345837797875138186715230304040773409378521911505475575668221962744869521711839048415565479955289538216666468335320041026022030559089349541205519079208325038226750450863190593216220415761203556498534765768844967317083043782187041900065115674435506296168160718714035471472742040983036919536009931544477249395624911563931818111644979/8276148992894247211711139625608728669363566097572328423059980406493734041875134005719887693588655341080186399786898960443147106667276768209112965708989469628280956312280077661599405018952475918585692755757668881692085663850489923118849302505272552606003087745130141247410474139784564403751288285400816294023246488907003432134142699360421371107698125348021605229052674744078794105931374047012838316470400*y^18 - 13497487346210493566665058137527004025437456477015427206347981484724555508990816894428346016566010784947771610484734701264692502614593252794514451857521615129947518107339665025156328581258244783124955424558917110918378371863308673356577340133566877919806404577725747047448696665616648774963410243591474560336164413967285638459374173980457985902390457334451521723493123062822398266205820269787414357609/25543669731155083986762776622249162559764092893741754392160433353375722351466462980616937325890911546543785184527465927293663909466903605583681992928979844531731346642839745869133966107878012094400286283202681733617548345217561491107559575633557261129639159707191793973489117715384458036269408288274124364269279286750010593006613269630930157739809028851918534657569983778020969462751154466089007149600*y^17 + 25174997568284231432850776945534711933070722583329586766062445256405709000213760334735961028042929365362091837567213245707638527594465386502232105634220022204100972437989158961880787826924036559487752233719335468988873400726729329909351614198380480718952910396677870874345499121843618530248523676453929573655814948957700421226482520661289676632181396841843166550158602317371434649234616378762791109747513/49656893957365483270266837753652372016181396585433970538359882438962404251250804034319326161531932046481118398721393762658882640003660609254677794253936817769685737873680465969596430113714855511514156534546013290152513983102939538713095815031635315636018526470780847484462844838707386422507729712404897764139478933442020592804856196162528226646188752088129631374316048464472764635588244282077029898822400*y^16 + 335041232913283361116711778226982161819500222159684729140911138572781859271912713937841478504809679407420677953803185060218411737037522765474589566273624259796720545168839157543017879923123386365964239113681360493084644359882616015644279119956039934674065486169102339645389925211308188294794670767414736843978432838196360606907533083523404250519010240583959009202184191041775029159654241570782986089824731/198627575829461933081067351014609488064725586341735882153439529755849617005003216137277304646127728185924473594885575050635530560014642437018711177015747271078742951494721863878385720454859422046056626138184053160610055932411758154852383260126541262544074105883123389937851379354829545690030918849619591056557915733768082371219424784650112906584755008352518525497264193857891058542352977128308119595289600*y^15 - 1078516955660919450059690688797342820672600503070486404118161351980759431189375380068345707816727174351372710561570596955715078471081569325187083747533481605805349487896949509649079450210045200604616766829880321082637635717614437196612005559722943991861956430888690208089734673157269574507904673030224746396684132706954903986689152422868381334487864967378253019205861174716871804731891184184219228328249201/198627575829461933081067351014609488064725586341735882153439529755849617005003216137277304646127728185924473594885575050635530560014642437018711177015747271078742951494721863878385720454859422046056626138184053160610055932411758154852383260126541262544074105883123389937851379354829545690030918849619591056557915733768082371219424784650112906584755008352518525497264193857891058542352977128308119595289600*y^14 + 97820228358519077671493403509870780186017815857320211526465900887941278317579915569230326614914919431618575574913116294403360714588304235828191889795565716719641058570078145570960597360401646498817936088894797101249301232049017942923005490121766884780077728277078506545147328950965183872275240902135220077391630729703549353771629548106582546836905160645226271238316677534347583634007241848921731990613161/39725515165892386616213470202921897612945117268347176430687905951169923401000643227455460929225545637184894718977115010127106112002928487403742235403149454215748590298944372775677144090971884409211325227636810632122011186482351630970476652025308252508814821176624677987570275870965909138006183769923918211311583146753616474243884956930022581316951001670503705099452838771578211708470595425661623919057920*y^13 + 1051229769654275518511707022586660268592720785661519665557432019919607006215745126346626326843780181879876106164284988342945066559814825852013125605096959447279567694520188968557322426523006698838107612958499204012235084346878662252242609587057503203854332153072704279392456513956680628564326137213971546695753979958056653210754946973239653828567066126926291222472538225867088325734015075780756258942266977/99313787914730966540533675507304744032362793170867941076719764877924808502501608068638652323063864092962236797442787525317765280007321218509355588507873635539371475747360931939192860227429711023028313069092026580305027966205879077426191630063270631272037052941561694968925689677414772845015459424809795528278957866884041185609712392325056453292377504176259262748632096928945529271176488564154059797644800*y^12 - 41674672485054599120983203708498738762656446619923509555327665245795799785568508822534646116076959910274077734384790608842639165874506827891361818196601421583654594291161092623024887022302705068106383696471596976720153665752938153303966403549677699951706638077743948280787066409851523676486143200922353585841625800455825264067007963171933669307215242386440393813909144600388098664036004826987462913230671/3366569081855287001374022898552703187537721802402303087346432707726264695000054510801310248239453020100414806692975848315856450169739702322351036898571987645402422906690201082684503736523041051628078409121763612891695863261216239912752258646212563771933459421747854066743243717878466876102218963552874424687422300572340379173210589570340896721775508616144381788089223624710017941395813171666239315174400*y^11 - 1750448997606848542009393458634429192094260844625922383426234028455195152174092103099765171917410375459515948524569928981167526566043553985855924924689108186156252937838743203444932585653199715747254135304418388840639110510013233976627844400718368163630030576785423523904475090453243878722152515892076448842263079223895036932958571353987016315627569477640248084213428731506486850556707377113193418140683243/99313787914730966540533675507304744032362793170867941076719764877924808502501608068638652323063864092962236797442787525317765280007321218509355588507873635539371475747360931939192860227429711023028313069092026580305027966205879077426191630063270631272037052941561694968925689677414772845015459424809795528278957866884041185609712392325056453292377504176259262748632096928945529271176488564154059797644800*y^10 + 395810880244215764736434491125488733308082237026646465399893417988558789392403734813103716455058394366640631212590492803738318220516873638224198329215917139955027577502132001992642515350617963500386655112258582822522327025785838681024804417079525219872688360427746513634576117955291420975865603613357159685161569200637725494590241426927627776103475838428261164923267476994623630461585371612092228229571353/16552297985788494423422279251217457338727132195144656846119960812987468083750268011439775387177310682160372799573797920886294213334553536418225931417978939256561912624560155323198810037904951837171385511515337763384171327700979846237698605010545105212006175490260282494820948279569128807502576570801632588046492977814006864268285398720842742215396250696043210458105349488157588211862748094025676632940800*y^9 + 4346113012752767671226418493432897393275506687323441056703742807278617891377514828337005174574018983758703592420692130967432336540514875255763562961311571739093773677557009807552595709196102233838605537435507356830786450582569120297644101294040338743149417605154037706302099750316533084212210793968387286163031609267942941119555631777097674991212617667223962711861907933840131192802797935006439942868294453/198627575829461933081067351014609488064725586341735882153439529755849617005003216137277304646127728185924473594885575050635530560014642437018711177015747271078742951494721863878385720454859422046056626138184053160610055932411758154852383260126541262544074105883123389937851379354829545690030918849619591056557915733768082371219424784650112906584755008352518525497264193857891058542352977128308119595289600*y^8 - 101027599046357726766568065314244390883547600101924719257514407388825945505612949986873277812316653214524746391602714833203400444239514847902496227287349834574837893125122321008811447959487876127440010250343909825760724234495952748196707635011622537551331274492684125790519530636044840863433070724285076539386682788119922835882760815793979194183350397015825621282258795790230498160366507606042432813813065/1986275758294619330810673510146094880647255863417358821534395297558496170050032161372773046461277281859244735948855750506355305600146424370187111770157472710787429514947218638783857204548594220460566261381840531606100559324117581548523832601265412625440741058831233899378513793548295456900309188496195910565579157337680823712194247846501129065847550083525185254972641938578910585423529771283081195952896*y^7 + 3886077808372959744201806476039074349718040024663981312394821055545108435719914836417284996383515707382967458647165256266233805792918029354090330618513209175149880797901872172643780135072960834367580475322557453932610210765133973408612785069708915426485873025353911169163188148428216892424040752590021836832764084614018262858845427404335987142913837022806641286136984787703471046799115712266071439518004653/198627575829461933081067351014609488064725586341735882153439529755849617005003216137277304646127728185924473594885575050635530560014642437018711177015747271078742951494721863878385720454859422046056626138184053160610055932411758154852383260126541262544074105883123389937851379354829545690030918849619591056557915733768082371219424784650112906584755008352518525497264193857891058542352977128308119595289600*y^6 + 91834049360634462224508156390644995665388227471760107701856518907685968232559416111746978220937044610357383966683794584453847293834342484312620285784664286124389638741213896008782963971094678875332235637633011095620335535915885871158498056374875405283759782983814820397368503867208592103806762372684371460725676016194446036344035648992512820492463177664905278251916806546877355845257279763298180503329403/11034865323858996282281519500811638225818088130096437897413307208658312055833512007626516924784873788106915199715865280590862808889702357612150620945319292837707941749706770215465873358603301224780923674343558508922780885133986564158465736673696736808004116993506854996547298853046085871668384380534421725364328651876004576178856932480561828143597500464028806972070232992105058807908498729350451088627200*y^5 - 510560906479878578017021851083436726896283681715372804691275655121579540242877011584102372576790460297690874319474012166579103787642945042520621427043926841524468575291396585206691746513434910242081329078562403927119010614815794398850028903710177371628321886218151678945094766214945163474361491766481611638307417973161910416612615237407637741276411832178166119329202401424462735340074930226510921407610203/99313787914730966540533675507304744032362793170867941076719764877924808502501608068638652323063864092962236797442787525317765280007321218509355588507873635539371475747360931939192860227429711023028313069092026580305027966205879077426191630063270631272037052941561694968925689677414772845015459424809795528278957866884041185609712392325056453292377504176259262748632096928945529271176488564154059797644800*y^4 - 64576192504251874374587537441459443044141652762209539428843096992491396693365534662016976292973956989490067609926438971633321433798301239000456474344671728963118399685691038269655014619047788460480351675155775031336831952166990074703209997610211296333018290245987838817975213831942956112220772882925132473118942694193504046604665008501430143192492808539056512054801208860724681924381865269557677095195817/16552297985788494423422279251217457338727132195144656846119960812987468083750268011439775387177310682160372799573797920886294213334553536418225931417978939256561912624560155323198810037904951837171385511515337763384171327700979846237698605010545105212006175490260282494820948279569128807502576570801632588046492977814006864268285398720842742215396250696043210458105349488157588211862748094025676632940800*y^3 + 49687612274463361328586971183517671192635067946364096022445536689489516674410858123472579941975958032875001159088296677522818606945772916146965995690147064492571216518960345078397957804402379672037322795110767136474192174932950965964387426641191155622224637930695230730427516331927232357088868837528103708607809182239456004499939894178813579086328150609594102531308768980840910335142431305428404348609257/99313787914730966540533675507304744032362793170867941076719764877924808502501608068638652323063864092962236797442787525317765280007321218509355588507873635539371475747360931939192860227429711023028313069092026580305027966205879077426191630063270631272037052941561694968925689677414772845015459424809795528278957866884041185609712392325056453292377504176259262748632096928945529271176488564154059797644800*y^2 + 265935260796155854944682848051021368498077165696212517692601500729239975845630636401354461746528479123610652935275442568023455891736313646174769655481761059877838913980651873514842823071803689351547982329401899478809910520446837224069042792874643044575813007279520435139455685455689944193702322589974502489482046965428470454991167023562601764736929123126000398798194627190815113598442684861694015232737/494098447336969982788724753767685293693347229705810652122983904865297554738813970490739563796337632303294710435038743907053558607001598102036594967700863858404833212673437472334292836952386622005115985418368291444303621722417308842916376268971495677970333596724187537158834277002063546492614225994078584717805760531761398933381653693159484842250634349135618222630010432482316066025753674448527660684800*y + 2935764033962318482159087863448226460060164813573707145489411445575276000361838868617802040149326584810544903752265650649100704343894032406942158646535119603952976702793428754854963527278553020942819630824350057765942895063133978340262203227693739590671969486779706407012102970678235628828780290654612866121170252405423922163639735934712646650388627378444388345331470557440573741539900374527933266827619/19862757582946193308106735101460948806472558634173588215343952975584961700500321613727730464612772818592447359488557505063553056001464243701871117701574727107874295149472186387838572045485942204605662613818405316061005593241175815485238326012654126254407410588312338993785137935482954569003091884961959105655791573376808237121942478465011290658475500835251852549726419385789105854235297712830811959528960