# Manifold: Census Knot K8_159

# Number of Tetrahedra: 8

# Number Field
x^26 + 24*x^25 + 175*x^24 + 434*x^23 + 151*x^22 - 49022*x^21 - 359929*x^20 - 1059034*x^19 + 641753*x^18 - 187284*x^17 - 8789151*x^16 - 20426106*x^15 - 39279888*x^14 - 45674862*x^13 - 21570572*x^12 + 33886206*x^11 + 98596773*x^10 + 91124884*x^9 + 17266069*x^8 - 43968930*x^7 - 53513193*x^6 - 19463708*x^5 + 5047636*x^4 + 5090439*x^3 + 1145059*x^2 + 86898*x + 1159 

# Approximate Field Generator
0.252065450632620 + 1.42757658384565*I

# Shape Parameters
-21431421700100469600323033193402637356828494813163536764084395732789618213174599380647/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^25 - 511642195097698379913216204317953519893103517776090891397112476627726627808034255925769/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^24 - 460697263510142716413979295175831670012742613658033417198089145448408368556371994786181/15414943291929477668516443299009960593735825909020056686579102495794708097422051882564999*y^23 - 4415435821108842766060911305917281268932273223160970690911698296906169151006779505929251/61659773167717910674065773196039842374943303636080226746316409983178832389688207530259996*y^22 - 2093726862311551007004082239586088378088620647071675598172163744134639639012546772819147/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^21 + 1050913979471461733773380548780592270556280568729090547793666505312945972061124452577403141/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^20 + 3790384552283018563555275847609802109712243419876215882326296474703783690067510567066405133/61659773167717910674065773196039842374943303636080226746316409983178832389688207530259996*y^19 + 5432168599839643676314314816323324997155118780867757536784997696764678471718090089534227123/30829886583858955337032886598019921187471651818040113373158204991589416194844103765129998*y^18 - 16553985208652025446000559023620029468261282291872269163056607554465593273881298214317209067/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^17 + 6000289420586283402017237377703743406923223049578075769373577386937866956869818713750709463/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^16 + 93949682427682701449236202005015860927789961929876990486407525762508484574423550454512864205/61659773167717910674065773196039842374943303636080226746316409983178832389688207530259996*y^15 + 103384439044296803028314569243831197579002174379541265852439528419261663883871305883669812957/30829886583858955337032886598019921187471651818040113373158204991589416194844103765129998*y^14 + 197129957840486012294781655065021060569138369774990698642804750774516905539516193695854787131/30829886583858955337032886598019921187471651818040113373158204991589416194844103765129998*y^13 + 438554588939181570368684386772436480541258550807924813561202219407377042864365893215780807891/61659773167717910674065773196039842374943303636080226746316409983178832389688207530259996*y^12 + 173815617456680373496654375266306645881252704686375278818783281514867399835485735536881356899/61659773167717910674065773196039842374943303636080226746316409983178832389688207530259996*y^11 - 96510996108632107400904350293642766441697210506044476620541831928479840684953997291835146964/15414943291929477668516443299009960593735825909020056686579102495794708097422051882564999*y^10 - 2015125320445835837942499105827251366187033156333213612381498228801833260775011004596370069835/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^9 - 1691515948978083966740313258138918484050128106742454749841506809794724247462662331437952724657/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^8 - 73957745192851599735769560822229963638490534448276854491536323260883609384269322343606622413/61659773167717910674065773196039842374943303636080226746316409983178832389688207530259996*y^7 + 120412559893933954437285677523055437130602933189553071400444128104099268585951022331849660548/15414943291929477668516443299009960593735825909020056686579102495794708097422051882564999*y^6 + 1022465803570823772420053927467356603189974008004617943535442378363749335028751026252646882719/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^5 + 282964562905249242907141216514463932007131010500329249891562610501729026224867368696800921277/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^4 - 145792088297475462502545792863719039291568183850864539368165884703760492676346214264161837737/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^3 - 11275411300569710707636804906820481541744902925378817849630535216722653043544774154246917893/15414943291929477668516443299009960593735825909020056686579102495794708097422051882564999*y^2 - 12532953668910716005413500345741142746368721121056692914158744414469550813808648844214455245/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y - 264223870855419451751308154484351938019986610790835512938133079848695448819834150182975321/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992

-49688842641789123850992568362982140511964720788954415956234972976498324315441296101575/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^25 - 1164538786398852972529121810938267445141431440064623494520708546133255133720398844014297/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^24 - 1006296773925720911419018654011759070399595020289651508357607555245160191539807430043943/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^23 - 8638753260069029327662807895128816509494045540408636524229483531792919620308400011235187/493278185341743285392526185568318738999546429088641813970531279865430659117505660242079968*y^22 + 635148765998941732668171786505650899341561683957008613430846052001850579570622441864149/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^21 + 2432788696106695383479930989914739384879520212846665182035349937600832539892958661134938245/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^20 + 8257917679672610270198455850396984300851460767419281836568331914627284871178552787080760153/493278185341743285392526185568318738999546429088641813970531279865430659117505660242079968*y^19 + 10962444303511072646906275725029452222173347250278352511215397462325402458478064645062877573/246639092670871642696263092784159369499773214544320906985265639932715329558752830121039984*y^18 - 53335292739160795957695524603532232615832082381266233715262017743803079624544780373414732259/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^17 + 46749001633248293801882109343940788841979241333588324952819165090588823000168871725737170839/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^16 + 196845416126314971299802070957251073897754390800114109864766019197293746563986725321307350141/493278185341743285392526185568318738999546429088641813970531279865430659117505660242079968*y^15 + 203760154040999063892409832719276344630454141085766645176807213146349220613101454920287191675/246639092670871642696263092784159369499773214544320906985265639932715329558752830121039984*y^14 + 390790914811320133166803135607401495705676746788947339201570414570793999847838467107417222249/246639092670871642696263092784159369499773214544320906985265639932715329558752830121039984*y^13 + 760255888629201343734214482228431839269622118446560150178981956531259508236654388794555929055/493278185341743285392526185568318738999546429088641813970531279865430659117505660242079968*y^12 + 234279649995565267705243592337155248375517135757339106499027347026131881421424499622170721539/493278185341743285392526185568318738999546429088641813970531279865430659117505660242079968*y^11 - 223182308939965498714140999573763239440760230973144065099592576351281124359692127726559081761/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^10 - 3897250666955432491963685887894894330670255085387359207180420875264237686100653483966084821755/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^9 - 2721998294061087882896841222148294400633711436611894114642593054488904512275596503059405232873/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^8 + 43549992413592031197865742104432441961227246097356265165188507336238965995241870494509649831/493278185341743285392526185568318738999546429088641813970531279865430659117505660242079968*y^7 + 120612179382279515098341200883433728575119727379736087541962741097457423061623712546107304481/61659773167717910674065773196039842374943303636080226746316409983178832389688207530259996*y^6 + 1724397773168545221906932619491858134727964097348263247665688674869003986756235182528785652495/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^5 + 316094319592145826756006299185124480900452683370278217271737261715323285071572389254553589997/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^4 - 265992929766238684466337911886534804911337617905536951127803481653041497967705774184880518737/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y^3 - 17260191028378511380777447363746930501878408333028260259539390339653583944379213975286593725/123319546335435821348131546392079684749886607272160453492632819966357664779376415060519992*y^2 - 14873437292213342238776454184478825079894211127329539139211096635649896209287941254399161549/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936*y - 256301510625165148677495550501925554425880915302050480969866850914186897954151347639084409/986556370683486570785052371136637477999092858177283627941062559730861318235011320484159936

-151270905897605246529500487009451539160001500959794110601561345898339856990834721462943306983523048132580158462558728818179877467451/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^25 - 3567939544961884027716619016821462650769612542973347432633554053535602392449191328212314154182110273668932182309777293306295348847782/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^24 - 24983839234357859815212222769996575558151473194959379938786505756989940695205792529900179857357227398457745108429992607458803622032228/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^23 - 55010246756261841254587308615213737217693726594565736081696214760180218571920794841280414076619501729408610805532839217740944035819080/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^22 + 2121884296856032071573137676754154053794156575812844810943348793035800847926855570799974828174682216332724898818998450161090469903380/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^21 + 7419957901465162130135870827588348407760988043960548440618957791272582344610465783643553352762332058432225127358151652285509748485556577/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^20 + 51379079912769576729833288837213075905060802327992780010008124337535472945859080828273497443424164747503338735555792515156558746229086935/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^19 + 138316707390497662224961944415914332574011133726755705172930482049513189669348514955800050644919577958177404348253822344387642047579079592/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^18 - 158834674335143376765193578729871435360864204699893656028295316092291551721585469149553087489359032951281572879160116767207817379808200449/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^17 + 81103141109033285243551108742233326328813724241882197345983826920302133565096649861582763667025569657226477173901758944865290672464600311/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^16 + 1306609599876969950949504785728221709292669645951510560430745356083312345320962364257337569270535601212192811812817750986631349285876371545/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^15 + 2545378913822144095096894053700172636219165549829509423256058753403369069774947132107515052678866168152605858026559215703168821528159298075/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^14 + 4775783155313020934028472159087331211877165688751773912804092675238776532650709961150332657619758133687176745896255788477407038489934359116/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^13 + 4689577512186645465091788254760368252121809997497440710901093986850818139546859749778584910430849191390124285921078315796865124679531327204/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^12 + 858476734947057964871537243568570606031283188105563844632415058133042738399017897603906125827664559990741147522405679790747143725590168341/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^11 - 5989438404958915737178263530399449900286170832317800806224156957674692176093945207559211193718408374649153475086014535686899314672172525923/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^10 - 12623959964361892533993140394618337126173641910091850624909324522453982680640525798271942829366156488016785395872567964512982987540451157431/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^9 - 8088808844058498710220123810100194524919446050578764060476614283932212098059590664376686369617957922738435459066933854493853281447099521414/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^8 + 1928592540697700391261212997836382853625846168737418273030087474519767996901145355606592234707575264930438302094083711431993562672460371739/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^7 + 6819343076523823898766084921775291561074223863749280856428597673199987092823138813789361216497039116530868274596268893670330608389198550926/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^6 + 5318606099379131664049478581227202023364903924926837936352037385689201430974101623675629289719048969944076880675334271447951857156377341197/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^5 + 161709523357474333086902498784590801243190403126331964276732439583746082768620731707179691788790347869514486521991825704805560297551824770/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^4 - 1420610561854537837780375088205977122289687955805181879159480859070346926881375713120263728193964976232155181274889621908582480947697664335/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^3 - 325573447730830846717934902170026241586218004111984651153775267813574264427806735819643229599559738414322833127578504508921642147095302267/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^2 + 56146507013641320764541457713006010325083231805699716622214234435074491848878280506993708919713613928345301516786496955779463180932381597/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y + 13851437912137483418160720829390783154666538510632930475575705039660727109710591852559494216371423673296119833361892917040570874605360503/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771

254068267020190431460683650844231282185151397093383302022350941914245628297261461292452664662076906187800028232779065869876926553/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^25 + 6024373015034831211708220555705862690690818388365674635922289774410435783350356035169260621338169879616831892757006233456051955799/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^24 + 5343764523650846617605074746223763298594760219609248854409902989098533883824223133449868778463474091383028019147695988736635688821/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^23 + 49254539994626844385172356728207996272523264236985769338211651644805264271670144958766396277459618790762471563859025047887098243821/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^22 + 13527382447539587890044440627198039150504700621779356074638003158214996418505678350140385166248721062126525972961969084619048643797/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^21 - 12453429412963722048808647089238924201370487914366403816288979910791159733532828573264262259084581482226486692612907335902927864831707/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^20 - 43930470607756587263919383879503699599096699869307970242883042415894388340542635808688090731134031360000141951331947438539370823061239/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^19 - 61242366572624846743204841717928057893179114137025164518231193973844855976621676985205529809875511098216830489210403063853929467474255/1473281290673161871585559184692586892859857257553273018583295502294743672790457243594908799592590185310869728180310417631118840521076*y^18 + 226429336744910361122166525599383019184116802393314296852476880420222025595048447476251149861260391800257421651805136682503269757645309/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^17 - 128324101823911766741916021797638977833847657713918725104678682147028146472867326618368558203175438329389402172925312103951492824445081/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^16 - 1076903638340607256332827092957716367870067874594132215074593126475231286722496099087248533492012082774676036611211990729140100397263035/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^15 - 1158132959807940564047452107069257663902090119054310269805991298411687309680688886486325410946220732810064953194817626297467933550530797/1473281290673161871585559184692586892859857257553273018583295502294743672790457243594908799592590185310869728180310417631118840521076*y^14 - 2196398762337589551043816124582026202692931005029264245910793253737497453324342683053295942423572609091924563491780671574006316207387507/1473281290673161871585559184692586892859857257553273018583295502294743672790457243594908799592590185310869728180310417631118840521076*y^13 - 4674998262307979484637698795755799912261177679451144320889147799419253746078126896412205560930257515338680131517334229203458587115354025/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^12 - 1656638757694527320924198977174510786365853184809462772437992223632005023686570155757387846847827192264659358404888144333076481694339221/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^11 + 1162283565525445982595987822931555525453819146452781758066388280134237269271875968421106175043821893410486000592238144057269670375976419/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^10 + 22392441320104849253126939412138366028494553504661486046537025234123611000550480029214932898499579468083072134039383396930073191035737605/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^9 + 17579610754955721037179078539150655761844276722296101168896356761708612664232731351947907455934985239152342792297193759025439815331914039/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^8 + 227524764467944536184809059788024241914868147526920042196812961678668221817815545416766849731907134935154652544728612794870439125050903/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^7 - 688947740708659857105503040845763091745181603472953485746103750263009448288616897800862106205432697554060846211974574100603059073084157/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^6 - 10736342704366663443551804172530453658528702864944060644925429667830318273646098833258354398612968949425776214727046438278516375797271073/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^5 - 2496131547849555016255092954771330644406739425499281241537675802017734360914671955640542572791112066123113394025120560018068783995733907/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^4 + 1772615925828542811313282423585742546656512669883010820289414548286526332532386131290254502236585414645226296566450244478927662934935055/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^3 + 107110060858875693867809903444223082448387352976351665576225162562707683645537451642941890460808661570793128990590810557449202499443123/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^2 + 85951805626804188018255280885394216044257004989854737066038577144143122747186410746094967085154908769498124662577527500943328395938739/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y + 7480704855044987241894066813869073300348777444019805813222176098835428288182371750517632139505358323949569262273758630720511550093175/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304

88939626502968298020058623930268937303810066057753104854296640169190232084038349124801496094543730272473562182811587460248248560085/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^25 + 2112995605698487381933104237796280240789391090587842278100563243063077976217382940701164808646597489736892360161648521130159165068797/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^24 + 15052150855306625243845217992512841998862963529766172528997260751523922521408516347730974235436958607580906395647457881291269137151843/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^23 + 34947108929705134771179041973216829739166578067582526116452303870272819740898814395928487362604794466605389381595599984655476429765829/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^22 + 4920266659181223155942827422644901379853467986140506529880789167417024871622127992215224939904621880700169585722325162000871526481914/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^21 - 4361324771687266150651954253345756478814918411315415501370361364601112553302920299383863437090917168011954837931457122283689535788460768/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^20 - 30955065908413968743969619297531569219167903603953130803802666504089446783468383159621811163740787864381760909852862165919682275746319928/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^19 - 86679043663764568858975670790090799302842101787398088540182263817439027676107310738688297655651666507563146047558779179384720291522583684/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^18 + 78167454446948895591403666242252688425739329158863964818042172215115275407931005744657217725437005247962895915240245593641920696471641025/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^17 - 35297459625372485812252256897891394576855451213916707492689011241980770849184890716256724357317680924514558004434216452939649777577828111/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^16 - 772992768977999093265590959872641792165579782352625630417550311798000763063503658269005537299806997466308907384172261219172033776842899330/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^15 - 1629875270710196433730420707876802007824600177903176177456213453786951749455470654553143916590144020368671901055902673720346105531079892468/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^14 - 3096241260841544453927892093351934049484441488773338355581969776782728276066326689126612090648434994034997316811570065958574056936348452732/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^13 - 3305720367976163753975274117226031743440569575183417605626030993468182083094502807972695438287746559906605309263194898967263780985795648728/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^12 - 1105506105596268308554414946816618032335731302775296513545593551014202674439946971010426510394798091384461124694868333681154740280904470624/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^11 + 3299239118092399581713213592915733430193828846800827651730336546211106369043972227404153706054064859454863899085217419628265209862078659521/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^10 + 7980011114734631424831343831547027190270312672644364247474072940949466980169747307217417965549421417022981260855102682688675171630491552459/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^9 + 6165031953516609953351396276541767872225031789368513577245763498759079969548002772867323759651859587354246475344175554723223577492481689052/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^8 + 10332986822116078739837932465331789052488225778757313103014714956252264549906805447756701554108448949824198101958900958074836319502575874/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^7 - 3951499507294880172996104406669293437541331178558706977950380209542355575374720265155887057566845984339478422047121459261917910423721639953/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^6 - 3814766494942301698588879732055571203906350425698310289497884101930841126106673436181270942160800532742742565448387481153028275105451975328/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^5 - 795193941863832264793860458737816596630265491313791986854894790654381030563177219363451421559726210100581510535693291712450305034507169455/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^4 + 662055123336367629813667768281917288937581794789094680129950372451059902706970612191702222508707388702585461711415215455025644685680043828/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^3 + 302775689781271880459862242850007188480134482200143108977711841560278908303600374419491257855097761052356018789181090263876392778785169614/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y^2 + 27989075738036495883650518849082226496360946529002632470163456483676667961282452357013676175989984023893767803910057189786466529224335926/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771*y - 436072744193742158396715296939158744222070387139196803307952076550201682287545508507976669373435126261415721381188873468031395830865331/426883253972548652291915773764677052206143640376060857134509871789901979191034986331624824681953006193824503740244943508616684040981771

-20360714626184140913509345373759228710005993984082530167002776935633731012488039596418815097499828537322638254782793704405202642/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^25 - 479853432648863315074970508128832996646789314573017369793046864561410589689272835184283302836820700853348315475614460377695884759/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^24 - 3356147226871129712245218311212841833853478714110822900369228315187772738687947578162009439161490252617011477225800479962829889096/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^23 - 7397376924548903508341114004977793122846965362953239623703516135204908540953618250106929762928839786674390933866217404782858764767/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^22 + 38886963874700945763090090250237559541144795535947857583579950482391714130232902298102175713014682808389914265458659895921001411/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^21 + 997909710314252081231691245682974520458098260502827447541861653112976552739075936293141203628635298940105631957957927791893484312033/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^20 + 6896902493448068989392763815740279055673105267697365406759766841750971662742013373086409123640123904025735165429717357567988972771309/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^19 + 18605286817928510846441585115906719139295349858942505918836268077233295570878410914897404236371313126930807726933223988753647414169542/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^18 - 20936073762072950496971011976144446745220273021557049930785850721614013834239683950701208852928274454735188485861246229065578094893092/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^17 + 13353338671638379590318707191675656309495355109584551623890567768755440305743541213995335836847063513480284913658221285478042898391041/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^16 + 172729870428698546268283578309592217698840789790591041060759462817790647116911702561999975993236240763641602179361253373027160381032354/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^15 + 341453235104615417294800342035464949528207650548273482604664906332699428880842771859187533661535233612597177212468795569295217550245228/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^14 + 656653745422351765007745469344135825843071511680774964692942304938657978180846889981501757843659851036892989415322316667488599479314154/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^13 + 654843296118862813353072982940131823269885746475554778583074604070921354921276082673136438445441901817108915978816006446308468947792229/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^12 + 173914656970114256139702356119437417587493654683543823966464807889107546146560627499693782663363383044550861716576461355285257570985497/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^11 - 746120328893276975512162811391359594757617050465637762031192840181569594286684474633107823675687944041962880975756425606936546929471780/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^10 - 1677201430859796863671235845580989246802153354633804915299218675677184097172247806945368595403261998704956362153047895832039388491808198/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^9 - 1145350013182519656111724678200084106184638965954983733863999970563229112502723732073773034000314296795319467527629535228160671609873969/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^8 + 101101073591160253268291352998012144094384831764949177863010045178165519506278743687904736587951078475301220074955046409545186766604289/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^7 + 819197945834899652309358350049013655283832685589141803000138166880889614486861021463405682242346458394730167600264922835998450073060168/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^6 + 731412677061919876585078969616068975452324273046759890913020287664023425688171307868253422231659966094419684875569357282681706387640040/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^5 + 95863914939711730042477035312730415128839801701780747414745624140022161740631176895890346169033764535901605322479598484569142900139007/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^4 - 125975617578886748114037953480185136869541601050607099880849135507015177851596209350576265111265461112244563296370489334841373432226603/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^3 - 45374476126568100584865806092463568688368149071680276515781257956474329735156718799821931352833645433881522820901952740967682132740353/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^2 - 4583943839872139628758894083720592382789597981655203594548550858227068676765004186682318820748082372486368861822535092896574022982641/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y - 30978201433789732668172722212905992605881999988252336033545045080108900014445028377018187838364601872022901670122671530235951998162/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269

-21961686310698591236286587961759910228440340599564468141555941550988552192314756890726442196898076904987276068927666880756925732/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^25 - 520282437952022338508617115710754258267069069787451799646756428489065742832644479089056756821595447949428802857696349940600442187/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^24 - 3682538312689830808250100225672666095689002100675632310401341337392107162284173812080828985999623244727977224618724700853511730707/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^23 - 8398062278661194400135765731702561941239687912248312735938247038450954132655371637621035958374174717955914333903325178832076254692/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^22 - 758417520179693799857010383264341708190118993750792155460845696553979993065434611110567277788700069401512192349499991794535620218/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^21 + 1076771312699933619848130303162926167879164601724175370776738636846724792634273676200191331146839842112445942655908226557523143034941/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^20 + 7571380545194809574604907782328836977055013741341270742814263356156504699994617088994326574275526527737235643617241846094444838159319/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^19 + 20928718831639742761020619730398131590112905983464046002987605181144244591216358396040837958596146734964926832491975163428601579083348/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^18 - 20487558283586596537514648610396805679021283752152384614575152270946029656872708375774940354209312791447624622635650994514518677252181/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^17 + 10647154473415714533769070777504906647986914875417063085005027868769738271804041632517119314011968175529036525115245900047343122017728/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^16 + 189303438256233227692749060386943790814161062804957760269443882207725095672832003869420411420867964353312091089828813363329000278262297/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^15 + 390779171035329574104224049583875369496465382546781228927102398936461266954478827325268488054097438823118718781317830253498386805750603/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^14 + 743153004290274379728789202785366040659661351109045690510873037142922253034905708238771880328775375240644288531597272840477502391645164/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^13 + 776815704090625359978557729211324053855910613708119258636069918478910186562720738415400112373537858743983124490280863904821482172851391/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^12 + 240398789316730986986426373232075069466953538694513692590114693678539335694249159571014333667949675676811214022335632610320080146828428/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^11 - 813188470912615263510364773647657415830070180754074234238922436446444241624767018486999012179771466759435624527585278455961370872469168/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^10 - 1910138441735161987559789179541645746768357953750377141919228288666444132633968915987381618387455939843013485609502754803061622231625320/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^9 - 1418077630430962412054567427994443646841621624791025910443152174355460624295113592405849121169158818882517775324756334589453620916765743/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^8 + 46727393058767949593427372243550074698629344428210696607147058829007177604412070026479812692761346250375022620293192030055192054912994/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^7 + 942145212054310879283052532768676824652423694638431330717343723009375377404723899133175414471844519881536428383272743517200212941828757/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^6 + 880007082131175305393440226098466008494119651456850707393972087267889056491112302627197871427713853568661126426136877154055845806235641/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^5 + 159660562945645088458358926668274008641633589462558948713923083949143640002411825364647208038592069478006583537910453754611711961445524/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^4 - 157079593425358773262108927432524465334459999221597848964992930934146740410671701596493719887881267705534240078110852111712671959937423/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^3 - 60294502086651512284341092923294752100050837538950825782804705839603825591096364582833938027372068109637764629192606930191073998675279/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^2 - 5412898992661656156802519087692168886189003877555141904103770266610984687077682595053912290371325757438691950303417747912365751134744/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y + 265267002800556716333444387989399350872706098524364331947831548690723245075021619317124682241255168888704012268627235167227871308027/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269

858790909313112400687257580797487225241943057581073025714543269581335869918843844376154775331181316382852559227019733904114204173/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^25 + 20423256966212096091314124133998325334596254243625266066806183236257593930362385439094149300145979582259565832030473756875512772259/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^24 + 18232040421513409611152083092615548035502251415784554888321047751326041085595312919403441332285827943928145037952741335003071431139/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^23 + 170777603803174633530563351958329226310455838008582059288060466415880161259612732319839381541638370109910862179757813423697588007593/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^22 + 59491549946828734838456203288550715884233319653853771474978593949094544567271247362797633872817393929545110326022694204528094998393/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^21 - 42106169451879915207164130459582299011013539181852943481827743241769079501613700698039036632679656255569392225544217385443540316790919/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^20 - 149953721312719689857544016590679211627505496796242879945392539308166227873010244634814517808334611676051869338867871000149657381004563/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^19 - 211376125246028416195113570409538208077480858560741024695871158576883000468614128405493683061101296938375893988781803955048986773677535/1473281290673161871585559184692586892859857257553273018583295502294743672790457243594908799592590185310869728180310417631118840521076*y^18 + 726855590140577647243010501742670132638228913007774507318302068004694901550455809182740410939414676339317094126571453193680723759084193/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^17 - 338557021902014286554158790980159133356861951578485966699566427645497876065822302206500230193352127803976198066145210409233344572921261/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^16 - 3709294581784100918459468274813981455781480977448050250012745815675877425115218962775835666271002566095953948825175787662442822407363895/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^15 - 4001316862374302827365370235397521052988570194265825304931090874799761113932761689692691060181964764142004391483600853102296100521051453/1473281290673161871585559184692586892859857257553273018583295502294743672790457243594908799592590185310869728180310417631118840521076*y^14 - 7602457946607616372108320841420240812806263442054871964516445344843883409852406601559085908889744052763974609163737240560770004677542531/1473281290673161871585559184692586892859857257553273018583295502294743672790457243594908799592590185310869728180310417631118840521076*y^13 - 16456890299167326516269849672257897431544553441724383114400094637987010542468303292326894483764291981546320031352849451659508543472484005/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^12 - 5985823139881956548628527688687542802119887227434782035311035139813073412098376258582433345988114681320369853597277154854263142788647993/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^11 + 3930238271445004744995232344106035102798106515415379827841099111634168972936955124689911107264438701640651209178599339361807331523229565/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^10 + 77875469872323652708091241108654110108141379882180428402012974157667387728637907322454191268478882499435331492901923883645346427348705785/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^9 + 62356603889806590712810359027773276358781987117753112488772635548874810879894132131615351245453509456483073323741138843629507239750316707/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^8 + 1278707328306297941589960915193665599486104781729559481650930399769580778613749389110146568259153511286473093513604777173144438371931171/2946562581346323743171118369385173785719714515106546037166591004589487345580914487189817599185180370621739456360620835262237681042152*y^7 - 2381939444384784227040070941469484271483780628411949539135190500408644952081384413578271177974520452381502715867839542480180292684090496/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^6 - 38090616819453701385566394847813250653534455558047440991479061612396806282337825269060511886067498411987085755095438906438467624699072101/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^5 - 9184231714754003043307682364823779849300412398188337600655213161318716489093338039431525185123603956791932242465762808144667524547732335/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^4 + 6106230233591959392966344816344048976095988876640446253767334073432139513758986755511127636988803419174757360566040333930710333792072619/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y^3 + 397396847096514714070309866959550683398648536179230005002783390849644649815100965890738194702132522439590199903236649656100856839036851/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^2 + 343649134133269742303553413450601184669745577812945637965425401133638608952791457922989500353724149333888329486836764774607505418009519/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304*y + 9094718631487239251114528080855369671472633966942274563729283235597090840825749097629510558951634277300734271049289388919470404047955/5893125162692647486342236738770347571439429030213092074333182009178974691161828974379635198370360741243478912721241670524475362084304


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

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

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

# f Combinatorial flattening
{5, 9, -5, 3, -3, 0, 4, 8}

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

# 1 Loop Invariant
1708881995644251469595245710847772313417252468003714438889519808141781354121679238303980236074518176491071962637422361064552063291/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^25 + 41232381403248423404002151041978682515866060612086388782466445861465643096160277610920811652722476310659605834039419193760411106455/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^24 + 151974558518431663941640616344969832985509458996270944084237578176066742925538074061104695317369960828218225438887720423865227042356/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^23 + 385721604915117329499856193248956766370090458523235975358361032163238262322679029310332841935995255957539728215342263826464303329714/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^22 + 294251119626079080346187436967592472322196983135867406268745046657301325815544916285738886893475191154243369612728503673491870187821/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^21 - 83862027909828927570758933759849008147303944518067799107148108362614113772795042864282678640713115949491538772098151751630086666910973/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^20 - 312897626773688649474079111760597486441991185804811752220605561450288606964885888123286943577765669339828102201506461425531814132104941/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^19 - 935353678393397895705992571222299411984850569419428693453158942972628426975960241907816361136939305053917948915187096361390163440424793/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^18 + 985657358639552702312196148459529288193987578199095945734395290990275126447077351411843388557953849870614527610031586289068225082026185/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^17 + 133049762825024993221063429548974493468871659440759385505857179967167766812983451578578487566944088443731860064367267366681015547347489/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^16 - 7750827761277038668708507595695143552125878264297546421324556169741887547877108867911734784873389539738877908092233289455343575533600843/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^15 - 18271318221392838639399033061116919342136300318007956838426725234154933046251156121612757253194953374171328874532796236914401069723011681/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^14 - 34222328926203829192885343056143565868520927088849676585300882357840490334686641794845625197117332629384091034521866063865588947644801529/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^13 - 40612734996248256047142417941185848065977664386610818911354134021960760586786504491038036571685085652052624450167164125121978113438690996/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^12 - 18060204597272350136931873835620411426741030697256638190410814857502860330694328898305539397641412012564923060421532462829887741395850866/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^11 + 31371187908282092703385517939005700653727554453180257700091617391511516156880050944711213531729783914248277117703953460420908048209797142/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^10 + 176695702592063892111284299127791700605427875271485382900543687068890670824717301076381131288505052993261296721248595116463379312429682997/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^9 + 163700817589775625344080917307905652077310793433233370739317808795524960203214901764859751302449514282991947179697016475329690406747022917/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^8 + 10808539285914387656181183565246791938554708413103457779874432758483572873727489404858663600987435563179132756933491780816829052060135941/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^7 - 42861625927181374817915731842870114502782158393117168545685421141349142294520689653296835451167030283226290464612118221524955060308688308/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^6 - 95661327176513885825531142474333545354783580835796465577584019118188804704827707218797177876654299847773180803177832421960626285113606619/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^5 - 31322869450821517257839357575682675639729981280721383027114900449209434706837429376115586736813252609824269441707965837031089013815864075/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^4 + 14836109147452614754109462511497408990643987088284255198833771413860978734634128369118167107794153257522547845436265264805270786383688477/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y^3 + 4438602020430666096758819319073085493765961023096234766046522759205722477609411848965769721728075240401667719478837314903551855457960879/368320322668290467896389796173146723214964314388318254645823875573685918197614310898727199898147546327717432045077604407779710130269*y^2 + 1044439752216194296496515863278479383083847912134176528747603902884645367457348169097205907311261023399934832565304328420393890462113463/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538*y - 14946697487672239148895619258617758633215179512399867142676877122065466695485032679224005053979909539370390600294997584642096008600831/736640645336580935792779592346293446429928628776636509291647751147371836395228621797454399796295092655434864090155208815559420260538

# 2 Loop Invariant
389230421907660930341337014616204398353078959295420740908358153612845758931127487116048844485226979141173519349161928515623658159945909047802425901896970235811524184188654042715393093012837420160234445908333949/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^25 + 9270214136338298353548635697446524972097113447750973534431115801018574629065950564392773888943267863355637268359311663933258645510925544293284488223445903583711550857367826946077289028539205694712389317143085749/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^24 + 66418266409323417766593952713137228671174970427909205172011947659803559925419756191378818910862480071760408878679680890426323873209650804943644155283673496064834785687795296265031701780711566779559965752016149539/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^23 + 52263177572909657264609696799428592230686986910142239675145226420465806233931295442519755770170863331631943387426118836878069086706509564031590606431527895452589501325216131446856206881160097729638266273868630769/4272688913708837404856423490612093500552304391491031638553284992209722429787635709561312574450561393230360572648582649123899287231405344295738186897051078892997613836381058232274835329704469090919773191255429632464*y^22 + 30253656937408823798822711513070058723345865106064676518997107611727940417539659919340558134413014348786553066207488223035565233366181262597149128995862952704201222509416286002345072285817615011786055909053994411/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^21 - 397626310813933039892263040752913228996174697297427609254093169680001781217101346483708724840315883089376214359381653879740046997218760438134910804982687888058592623617464206063880025606526815500397604400588723435/267043057106802337803526468163255843784519024468189477409580312013107651861727231847582035903160087076897535790536415570243705451962834018483636681065692430812350864773816139517177208106529318182485824453464352029*y^20 - 136598531501579832522296763013866849022257002949232566301433841967635349041730002420901905890737936604778655027058267227341882370158382118412290043767968657114801485623785891562640563777307108650026460423057929999513/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^19 - 16135470313546679707082547692250821483740290913145215773267450121292683782612082952392706936169825765527791805741173840026008875818546109446760522076816829481748322087459629114629908401843977735605174615843133568409/534086114213604675607052936326511687569038048936378954819160624026215303723454463695164071806320174153795071581072831140487410903925668036967273362131384861624701729547632279034354416213058636364971648906928704058*y^18 + 53387043858575579894870584242808136773104209168046416317310597445486117354334912097314548759233170211458974790122458682406359765398315736395473218004280328254839801478361324732391371518544579801139899427090784944885/2136344456854418702428211745306046750276152195745515819276642496104861214893817854780656287225280696615180286324291324561949643615702672147869093448525539446498806918190529116137417664852234545459886595627714816232*y^17 - 66261723843233622985782534595581371689804877534140796083714377519946542721273040856154058387796358466049017417823236274923835761185030751633455667787121000511722523408016265501799270589657629991135116769055859729645/6409033370563256107284635235918140250828456587236547457829927488314583644681453564341968861675842089845540858972873973685848930847108016443607280345576618339496420754571587348412252994556703636379659786883144448696*y^16 - 1697256751762718895687867869904848839541560444402148246489583530918968859864608799733809040759625182713407393800709159574389146410702882782822312075155334566765923549373662511048782408409254450101916497122075375446275/6409033370563256107284635235918140250828456587236547457829927488314583644681453564341968861675842089845540858972873973685848930847108016443607280345576618339496420754571587348412252994556703636379659786883144448696*y^15 - 2444146357639012432195499056047929619796884573798487325136804528250123140059822227192954122082634756565241518138033657295896089642507528843790595969743278189504816215068458811512823128683449275902669612002211350005155/4272688913708837404856423490612093500552304391491031638553284992209722429787635709561312574450561393230360572648582649123899287231405344295738186897051078892997613836381058232274835329704469090919773191255429632464*y^14 - 13952874933760706407245456647098367720192072682996802507416592096562750176939023487379159476773266874565128046407360140036784167803137898829633904337649276867212372181417338598796947339936081975649506224533833232061129/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^13 - 7619468707581903597844994659137171047944145239402932821983077430271702367043565835618900371630034537657618827049693359953482568284878879903815153270665510794786671778049343313344566641013165497256653016087040082076457/6409033370563256107284635235918140250828456587236547457829927488314583644681453564341968861675842089845540858972873973685848930847108016443607280345576618339496420754571587348412252994556703636379659786883144448696*y^12 - 1409763998582959278388378984308238599471028732680945324269906887471511097832556389912912217652602026210247464434231091971293065019966232277363606570048803670721913634453520223209437487221631682176465359375858227021185/3204516685281628053642317617959070125414228293618273728914963744157291822340726782170984430837921044922770429486436986842924465423554008221803640172788309169748210377285793674206126497278351818189829893441572224348*y^11 + 3549786420296760339863593862360947667882090864923688335627263102257921530472051302318718185355996597307913066850190235196169371817155823858588603405854418167511706597328416272485228278980971251310555199524206263203225/3204516685281628053642317617959070125414228293618273728914963744157291822340726782170984430837921044922770429486436986842924465423554008221803640172788309169748210377285793674206126497278351818189829893441572224348*y^10 + 8941105060630316853892950313703794696434266722221495486636748077294359852832643234515958924826345128677169529773664467259744177384717414448019444710747421589226218594649329948359083622056706006088817129858487631128283/3204516685281628053642317617959070125414228293618273728914963744157291822340726782170984430837921044922770429486436986842924465423554008221803640172788309169748210377285793674206126497278351818189829893441572224348*y^9 + 4826599248155292166697899227003683230658334141814878118210905023996321980910311579127424111267647183575893329947899121806775168909180253988720594820999136548312057851667630835623676995941217574848794742007298274756305/2136344456854418702428211745306046750276152195745515819276642496104861214893817854780656287225280696615180286324291324561949643615702672147869093448525539446498806918190529116137417664852234545459886595627714816232*y^8 + 1487214054884797183971057811450419153087662207834994090476251249816132080687747937062200887030038275998725367388028115375641783451710706071715100800697362317020607329248099938223237231716245927442537299327982177151243/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^7 - 2167866961812364469216975834173233430713609051192124134518360337106993175863859375169404054618762423069595664148876074842323301731106547413048440664313822714163548423749187864542342553927585070790249238808856802977317/1602258342640814026821158808979535062707114146809136864457481872078645911170363391085492215418960522461385214743218493421462232711777004110901820086394154584874105188642896837103063248639175909094914946720786112174*y^6 - 367452051396993686645497288377017229411984665806536290977940026505004881778827635613664883724453252289923775534136167319594624094580608805053039050765944554260802955813750309189733271014015441222132618706584900857854/267043057106802337803526468163255843784519024468189477409580312013107651861727231847582035903160087076897535790536415570243705451962834018483636681065692430812350864773816139517177208106529318182485824453464352029*y^5 - 4374387655841724068723156047354008528682988585631468333261767442730161654029567543529953265947368203161636647925846089131954060121539178007253568644163345549999554741948581532621405631133647256400686933761641124374613/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^4 + 2735171046587070297315823763384957495853676712309027224261347311212185511325902320480077918556636639943128417614518646018607345440954844314936816103982205901238830173409246337794791238246809900698303390480462056424663/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392*y^3 + 733805166563461658975906898014069561545181988954560619156742772790668304546141201615457810107195857035989641123752472922222026084697333029607022096449556783488970767678215001624018779361791329748413801733041280123101/6409033370563256107284635235918140250828456587236547457829927488314583644681453564341968861675842089845540858972873973685848930847108016443607280345576618339496420754571587348412252994556703636379659786883144448696*y^2 + 87724706582813837790801815389362404285559439749522030016388849273986136988774732796907811914259157400936004181291934873493564398102956290474822625189227176259478304549956182443979738674875753218417950638321151184473/6409033370563256107284635235918140250828456587236547457829927488314583644681453564341968861675842089845540858972873973685848930847108016443607280345576618339496420754571587348412252994556703636379659786883144448696*y + 25167206531289408617296549243491321674977387931047364933478166483861148936089682460270416712911674927791892478149438660529611787330958579641063501000424754032198858186106144344462761413335269455847791030185954221311/12818066741126512214569270471836280501656913174473094915659854976629167289362907128683937723351684179691081717945747947371697861694216032887214560691153236678992841509143174696824505989113407272759319573766288897392

# 3 Loop Invariant
-616841096706347501073069054256436759921163491460684215274025192906359486245426300804301763069057644678482479333772516443050029620997826955137640388649312538614693858091816657805887024288272897232803786513843118328833063184185066822324723498618840213/57524000651612031768023383943477313081757524275511810055368613445451803262299075056393375026909452049126039137910151360387986914273883682865133233708043388738123096716674289693359773776217679462767920620816266315090348768091015470296545398514361797653528*y^25 - 29350690097730024495947311519477514531677692254882828658701655422102120612602403438134984036847248933518855522704826989114436333017455373727991182500686360046280722151813622007034233427713045707418503596779345486903827912221914722282057350111280649787/115048001303224063536046767886954626163515048551023620110737226890903606524598150112786750053818904098252078275820302720775973828547767365730266467416086777476246193433348579386719547552435358925535841241632532630180697536182030940593090797028723595307056*y^24 - 419511763242446825313872460143734444626990826794540064997892695688374092937973827715708993605643096787890911592666717325611451586231053833501154887767825386939557821277896227054635319937865665793721388187953537279885286285180200391215413029248725592179/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^23 - 982856465279779523877186081333177159469942761351940260570292780400904493683255991868061968460350795064398305533873519269794446746590853795906538942821343829800594321364818201094997414342987370572324901727309860631443447121055627920150076022324487648325/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^22 - 165103464935558702223789858989877994790388331632931650798073814513180256497517217522702193069428963976830264330095402399944144651062818436166620312031933756511095452790622797119749458627495121683502331971364410318147551665518524353079266773941207396629/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^21 + 120992504542995145775962819919208259756653680949625224377131661637400130236560967036076151755296400838802099347439515217400732608717505325345761796324787650529622681907970912465199882817750876278310586922610396067756882654140604132443914207396777880891977/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^20 + 862798734348790026750750929287693445060837781019577501217705578700153714909656778690713628071203236164385289531395338643546956305060721154810261972188598847101197149798335129764793270496753761084842006634722047122157269138733433842491995329619876895146641/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^19 + 2432031676076716007985861915427886009027575592206444561312213632556137215485361729769634388513532575253573640070631974365060788300309590505099902052012546044415782658924960687053055017807625099511666397375051583322091948546567164745035312606497857190062029/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^18 - 2095861091603680951398489507647319709931427839960576698795496742027713129994002784582875564089428505117117364659641476973105624435801907002743834289052967941143879816382984278313054171807486212996112039517409035295904690754199885169182521229067004444680641/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^17 + 891251385849259034356139083700913237957844030967326777527556904529623014406822022665212122485166959701355888322780405800098998306206896159714001835251182085341551345435141286087499912703388280788063532135919648773537969096404760689212822651734315613869865/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^16 + 21530180497601843739634408603077689110538092811709476949541807170679336281790510712220392590504359376666321372997772501969008876777383697388927918714733165874663833394511159407850489168595207279571947304370652518193727761467197016485398973720932499339449517/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^15 + 45863531140635300590030104361015352385545644716721130469670530966285180442948949016788175022072263146866124247681008201579151324524535681520337111186024022625433277266516664056107345566061037626844210367604739642513988346480380898078226139374882516256340063/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^14 + 21809497899588297562879338070811235791941286589219737473924210978713164173500079977139831543023419913838832107170266533903340217289677943027739607225395669047359042081825944495765653404970285742622959864327202401334606728177396388101668892762155116636996229/57524000651612031768023383943477313081757524275511810055368613445451803262299075056393375026909452049126039137910151360387986914273883682865133233708043388738123096716674289693359773776217679462767920620816266315090348768091015470296545398514361797653528*y^13 + 47167788102835460821475246167364953199860977752091668943170572537597583370747936636488593476654294275249382976275082804050973367872345129857242117323557709096909884206891238161881420704281744207443905289710955368409424002695712783554427390434044540962024995/115048001303224063536046767886954626163515048551023620110737226890903606524598150112786750053818904098252078275820302720775973828547767365730266467416086777476246193433348579386719547552435358925535841241632532630180697536182030940593090797028723595307056*y^12 + 16634672719311969398034642179839763744674167865858898153960336958752583476207862205076328731986484379492349994085485771017202314903605959153190437511978176650097814359078420114175062348913232028123653495365921924029087992476581742253529090852141536655927203/115048001303224063536046767886954626163515048551023620110737226890903606524598150112786750053818904098252078275820302720775973828547767365730266467416086777476246193433348579386719547552435358925535841241632532630180697536182030940593090797028723595307056*y^11 - 11324703234659554639368362422296115672026787195070917274169678626171646896442260332512480670599756059815278303977034251229882441567517897153472922600191800548173755316974000889068558753268222650141277740179696469075041586370201043462245452015182244357942489/28762000325806015884011691971738656540878762137755905027684306722725901631149537528196687513454726024563019568955075680193993457136941841432566616854021694369061548358337144846679886888108839731383960310408133157545174384045507735148272699257180898826764*y^10 - 448280412459083529966135746526328937292714412648024882665448523530404658934609594451622053994458671753563324537502637901561893433312745767211065771155317244065818361919471557884143003608375185392426386679997343335348422836895312628482788527114842674315118033/460192005212896254144187071547818504654060194204094480442948907563614426098392600451147000215275616393008313103281210883103895314191069462921065869664347109904984773733394317546878190209741435702143364966530130520722790144728123762372363188114894381228224*y^9 - 44346784045319438689250054527099272593758406177081149383909349407436374391108029148323299553679638931169650331406599170098936757977996426442712305973053694858304219728174344211096452871417286944205167209080549818096469517241747191140772119805630008491141161/57524000651612031768023383943477313081757524275511810055368613445451803262299075056393375026909452049126039137910151360387986914273883682865133233708043388738123096716674289693359773776217679462767920620816266315090348768091015470296545398514361797653528*y^8 - 4953518369491241288948638148128532074451421573615924679477400872077027895735956884111373301228960061095264005930565925082308089787234231081357838585144379262521896673799336980209759513226701246958819518054883172125351946323102495348370231252568883212184783/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^7 + 109325638999933905813094988029812697210327014489334549375822939802330386242146199412934821819609884698398844764135401495873205375341224849120630761392410556485984693902387644618676188046423210852153482492507469741262288215301939557027875666115496288363123459/230096002606448127072093535773909252327030097102047240221474453781807213049196300225573500107637808196504156551640605441551947657095534731460532934832173554952492386866697158773439095104870717851071682483265065260361395072364061881186181594057447190614112*y^6 + 217294268219364963879739682678728730626698367564015383557235776759338623395601695953245435614583068727999430556639270410830678828563875468602407817293057606131056568800072527687089217706938574164499277286716041638964826155289210971651759823948041823120324333/460192005212896254144187071547818504654060194204094480442948907563614426098392600451147000215275616393008313103281210883103895314191069462921065869664347109904984773733394317546878190209741435702143364966530130520722790144728123762372363188114894381228224*y^5 + 49944197207215738404299838629589884410403202684553457019912235018887730539999428386076579162314755931630616236915266559549806339827622693165748349438603667246103089253430506751189859446336154699640356358329860164726259821990081834971452405417322433931024867/460192005212896254144187071547818504654060194204094480442948907563614426098392600451147000215275616393008313103281210883103895314191069462921065869664347109904984773733394317546878190209741435702143364966530130520722790144728123762372363188114894381228224*y^4 - 35215104991340853978795994764823713536158003058825423615005390570873234800688158685816735666571871576738523474775616876110816501106250751660286262775754380482556584005118266159572115659687150861455787388941511409887985328531726187223099542401985584708556101/460192005212896254144187071547818504654060194204094480442948907563614426098392600451147000215275616393008313103281210883103895314191069462921065869664347109904984773733394317546878190209741435702143364966530130520722790144728123762372363188114894381228224*y^3 - 4364502085561986853484038885217337627460894201890786782022307288190191813474766263729394738634163657093376340729663121608239850603724455914795785731936148679262309129989852240317441859503916527464936603965417442022514849823571176745150472163391743583620883/115048001303224063536046767886954626163515048551023620110737226890903606524598150112786750053818904098252078275820302720775973828547767365730266467416086777476246193433348579386719547552435358925535841241632532630180697536182030940593090797028723595307056*y^2 - 1932198642468993907670770948350391021678085264361217765167269656183562785660219479164981950698084646073159114354469173626382086399795492613629334411769409444934832609295459123225277753236091621781849280227196863877178076550058962500879965818386877035296309/460192005212896254144187071547818504654060194204094480442948907563614426098392600451147000215275616393008313103281210883103895314191069462921065869664347109904984773733394317546878190209741435702143364966530130520722790144728123762372363188114894381228224*y - 15604728355417905939787883245906346979235967210588922756572708946000890602185189262712989458106257873749130904930250216738722560391228241947525668472875778254822336798107295435313104773401254494098579897328701182361230146572479737872306259919207464118973/460192005212896254144187071547818504654060194204094480442948907563614426098392600451147000215275616393008313103281210883103895314191069462921065869664347109904984773733394317546878190209741435702143364966530130520722790144728123762372363188114894381228224

# 4 Loop Invariant
-10964530771873961403603121109693037983850490814124622654280960705371673029626674478971113431590077291925306754400984394288553667405686994830749423930510426091170444485577756482245454251883693490367884317558768615955174759564631854642218320288666423430148641896767074937073616723134867482595542032566075606608213176222331493852626539943/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y^25 - 130290364691033972656827753562559635216489258508301917705192440975275158184259094638921831158562539423495950375780385464831399164284116693476681671984304332555965311383075764043735620708913744029543741641311652453061216389932396644138841277096140715218883604638715594230632986522836942511739949107792611281218576886646370077882377838947/120114981583520615040758186732668659840582886117620057733061601394465650891221189299296454932818124734132583010731324419616501836388624347295356348032124384686381835692910810195740254373458287800694378084482915052940839479128782258599048739121718934295932777640385381588768211530057080212009108019808730334698039335951665337242828364746240*y^24 - 1857766253108303777578779105185294751548137117464933693976317737985963864605679383047571535828261253262665556103498409680672749319721215362505018298557893537898175710587743363934998989429390738631124855159888231074633700353330619141746813554550976957648860964487817975356720191225773378327885767348720485854092802825826701791770437590023/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y^23 - 4323570573645717432220496726489411443244759077840265932781764371728673091107627416345632510862129989277991322911294493131036551085717513178869636145511637430676143697737995232750950190554282070103419702553497353219877190774957740696701191144309306206081192125180729406863857992872365949563499116660570821230547405993153018251471597616841/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y^22 - 643114508931242295362431193125760615557953038247834876481840199069555228680909115266411006719880448838063275787984150415652572464446382844841554484089534736575412194989215508748792974898692463125187698815628133317237397131556180084694472421754055025200800452721278884717129877840911351248713856202501755092853072374203574399323977405557/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y^21 + 44804706141587926450838712232161573377662059508335661750208564169391569429142608932871699756691572007511670290758571615475671287335538055442745861955933917755109318464542383329215342199867598171300260214761147951444760503393683449371271643541282345860549189997455641817352740471566131820065853244413013324781657923061479388814799484723293/20019163597253435840126364455444776640097147686270009622176933565744275148536864883216075822136354122355430501788554069936083639398104057882559391338687397447730305948818468365956709062243047966782396347413819175490139913188130376433174789853619822382655462940064230264794701921676180035334851336634788389116339889325277556207138060791040*y^20 + 1910268344485847191749299337915402555248833776256626052292066454311831094963704442366333344695057713118258246394840645539370100181818659491756892955693813477142310275779791936925831192661899876425808108382263037819105125769052477740588496533009526315875278857603705847882514668940423498532903293102040500243274640186009070631180127851424289/120114981583520615040758186732668659840582886117620057733061601394465650891221189299296454932818124734132583010731324419616501836388624347295356348032124384686381835692910810195740254373458287800694378084482915052940839479128782258599048739121718934295932777640385381588768211530057080212009108019808730334698039335951665337242828364746240*y^19 + 10717200397396527708559405649560192460486650488878764614552069788541314430218360681903956285510236102153195111182222713081793969714570984863230596344853287072173529523753565177039070546143003704435721556631889807554674354254173342420838755626749806043504542485826310290598942962611048372238981877387981736118242274714605230717347443949350991/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y^18 - 4773208973618629186863008363724900278417725209772632434284501251099050503780154355079584420834836547830662559521350151055501056186953288783893886213461475674139526824548490228086662344489933355099028832529482490774894431341203797185332230085397752342558805294064300330518680520107269666223637350323078294168939487740007618154778445519105981/120114981583520615040758186732668659840582886117620057733061601394465650891221189299296454932818124734132583010731324419616501836388624347295356348032124384686381835692910810195740254373458287800694378084482915052940839479128782258599048739121718934295932777640385381588768211530057080212009108019808730334698039335951665337242828364746240*y^17 + 4284603280660952110425260694503019640306180747104814640061712630594485612187989021245248182397899815749413044084778335096254213939737002024670052402280976235577839957842270083223458040639560355850408774023166346410228834848091268793688826638773778196497946979648001802374827631741620962974511025254592411943468936471640210545793641071443683/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y^16 + 5958673083417847610740644791515616076557544354212769489617291478609397304119754796660387706272490428355400764093098865728988925405736172465268050422409389460800251534162622234592936855430293635400479867405490086038752372619476267800919756799736223032039604377107334718997635137226850197109240003962194626374119306042440557418834514272590381/15014372697940076880094773341583582480072860764702507216632700174308206361402648662412056866602265591766572876341415552452062729548578043411919543504015548085797729461613851274467531796682285975086797260560364381617604934891097782324881092390214866786991597205048172698596026441257135026501138502476091291837254916993958167155353545593280*y^15 + 50416656411185465927183227219169840093249743449247788149518202655069369040288196870579393633443293829826895793477643716180173804598300844491778723520343454165527631033490164580270205215429355227912728511187395450300499062971482556519522476204266666387223210735358494816521974078434107570206938668952056667259263776056157065204402692353357403/60057490791760307520379093366334329920291443058810028866530800697232825445610594649648227466409062367066291505365662209808250918194312173647678174016062192343190917846455405097870127186729143900347189042241457526470419739564391129299524369560859467147966388820192690794384105765028540106004554009904365167349019667975832668621414182373120*y^14 + 23968423515965032265917206126760738113858286537805926912946624130251836914879766060577519321628096551507845582693291341768241985699723099278214817132022969235634703366152106514042242745022833840464537209048292253113875209667447444902358955286620509848150432748749130299301357985592248748874322253278126777692213750832521738189524470102639571/15014372697940076880094773341583582480072860764702507216632700174308206361402648662412056866602265591766572876341415552452062729548578043411919543504015548085797729461613851274467531796682285975086797260560364381617604934891097782324881092390214866786991597205048172698596026441257135026501138502476091291837254916993958167155353545593280*y^13 + 136931559943560995813765383579939722569077073078142141796646424259200035465817269717822008104730988382911436164645171502100013978334664737684349938981890459750621594941778734362780978631161909890847101619272435701726399921501644728711566914207703674704284643142669580877085741717028117681091227152083502251549713216896273816758177148391843139/80076654389013743360505457821779106560388590745080038488707734262977100594147459532864303288545416489421722007154216279744334557592416231530237565354749589790921223795273873463826836248972191867129585389655276701960559652752521505732699159414479289530621851760256921059178807686704720141339405346539153556465359557301110224828552243164160*y^12 + 70012933911937289849835383198718548157948977984776004702619549149459869899768445901650305221263385504670521194503348968034822537719551292505182619773975354634926643112289804301820598198931930996531658234809642506040486357782707566071942159738484120351947556664115093872951264006013558950893667764731199185393168953454717661567033819712683637/120114981583520615040758186732668659840582886117620057733061601394465650891221189299296454932818124734132583010731324419616501836388624347295356348032124384686381835692910810195740254373458287800694378084482915052940839479128782258599048739121718934295932777640385381588768211530057080212009108019808730334698039335951665337242828364746240*y^11 - 4498038612183299110913930456607963551950021731174739375183503457269967772853507874526819927797663327419137317374762894648309657790110389191167575051331956307570620210810370476672091066774689044403562453578444264792096941472853625408690594497984832627090689970397697141400213948282311117961897072973167915998684827901385934941068157481291177/2669221812967124778683515260725970218679619691502667949623591142099236686471581984428810109618180549647390733571807209324811151919747207717674585511824986326364040793175795782127561208299073062237652846321842556732018655091750716857756638647149309651020728392008564035305960256223490671377980178217971785215511985243370340827618408105472*y^10 - 164472849582950890479068446042311972809732671705350370677540539158300464845708280087354984803925656068109601466844939847541949131816350610795046490262951325765048033752146770435648029311693838131735974937971129079686625894682744367472207471279803039621583164769136856721293550151698123506731729532661138535546911462122748351218396032367640263/40038327194506871680252728910889553280194295372540019244353867131488550297073729766432151644272708244710861003577108139872167278796208115765118782677374794895460611897636936731913418124486095933564792694827638350980279826376260752866349579707239644765310925880128460529589403843352360070669702673269576778232679778650555112414276121582080*y^9 - 191990209272589338418836441782268554852516436082837931142252304575890577473074036861609062174917103797987049118870813090209805379826887613566886759053622108358604316266304023958788288999834694908968604510775190933726201036242715510824367843135503444474958707801233835646914717588943648184619180537113253051074408240177232473423974903339416803/60057490791760307520379093366334329920291443058810028866530800697232825445610594649648227466409062367066291505365662209808250918194312173647678174016062192343190917846455405097870127186729143900347189042241457526470419739564391129299524369560859467147966388820192690794384105765028540106004554009904365167349019667975832668621414182373120*y^8 - 2143901777664350218916272851696497964651303874526855233116160492660251228292821946945367622253798837793814750736413194967316053600359134075397564261211246630768189830894935506043415849935221663518432331685828214239608698269067779250295795997000222702629290352375648655064711331566094899824250257524931329627552971773220075499150408857918573/60057490791760307520379093366334329920291443058810028866530800697232825445610594649648227466409062367066291505365662209808250918194312173647678174016062192343190917846455405097870127186729143900347189042241457526470419739564391129299524369560859467147966388820192690794384105765028540106004554009904365167349019667975832668621414182373120*y^7 + 53967724495026334717041096542834844841018648616798464917067509869472763242867761577766709171597141668827365996636204969081027557479297713794809752182781510201335592011857983604412312511854432721093609637888657934810787085260693545717955638166501024520256542355882943371715966198943383975312725357007225996967813492941077453599864782451071543/26692218129671247786835152607259702186796196915026679496235911420992366864715819844288101096181805496473907335718072093248111519197472077176745855118249863263640407931757957821275612082990730622376528463218425567320186550917507168577566386471493096510207283920085640353059602562234906713779801782179717852155119852433703408276184081054720*y^6 + 15788324450127642971176876619290519358123010802600291007074123655625435287668288507268218562525860838358399536942007520052572258493324370634197947142629957688080626907264633807639294115634548446832539156832602262015322624857691188871983791967565211201050758617615115257017282693745875166362363766535870141379853002700792082428173528779577649/8007665438901374336050545782177910656038859074508003848870773426297710059414745953286430328854541648942172200715421627974433455759241623153023756535474958979092122379527387346382683624897219186712958538965527670196055965275252150573269915941447928953062185176025692105917880768670472014133940534653915355646535955730111022482855224316416*y^5 + 5070881015025557752104203788531100100198021637353804079260897063521990575532063417170504288643169986878104005919096932443547090563724037459248436558045611455137971331039653766688214091966163458523881217906036224246123053704275577764818319827011800301331531382616116746820866783913805343013041263869114592867974521003667804599864029225104335/12011498158352061504075818673266865984058288611762005773306160139446565089122118929929645493281812473413258301073132441961650183638862434729535634803212438468638183569291081019574025437345828780069437808448291505294083947912878225859904873912171893429593277764038538158876821153005708021200910801980873033469803933595166533724282836474624*y^4 - 79890147817874775568621065597211860761702807330414543737156966428045034601590593179808900383994536969475150831492765592293156528999720730182104902683224164447176542627643419447467477888967645439464772634035822099813881145072239490298345429578609989149770392032221983569120051385073628317663604174181748383708871498290142892001988107626580803/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y^3 - 18536934113744036931336974200189055343297884064437060933382084229726620365904372482914534281740259355363275114917510985259672147099177047797105249589754412229851311885326464443542285045800581164478408846357658451220649301849969960061315344494472372551321351707510161337039794420497295025262643949684292477658852561186694693852876958612897807/120114981583520615040758186732668659840582886117620057733061601394465650891221189299296454932818124734132583010731324419616501836388624347295356348032124384686381835692910810195740254373458287800694378084482915052940839479128782258599048739121718934295932777640385381588768211530057080212009108019808730334698039335951665337242828364746240*y^2 - 3761008533619456158801836979687062154350919745854511314852777892895046345950023133535870562675326163678129696348374242738739875936586531369762079656892993828392498365001404575227075784694908352157363705455789992257212426618517457998916135504030568123586763101361490135849546293296404363646998998456633443832458314325496734709046677952667293/240229963167041230081516373465337319681165772235240115466123202788931301782442378598592909865636249468265166021462648839233003672777248694590712696064248769372763671385821620391480508746916575601388756168965830105881678958257564517198097478243437868591865555280770763177536423060114160424018216039617460669396078671903330674485656729492480*y - 13250473073486991470333219961633548326846443301053401061056686023324638817837784961554756454417253592831649976992769913161095773913232177242364073253559694858671432549177783954558643348914303194917266103889480263201729360585036274145164919212143714144412728350089563621417097271080340112825857348030594185932524552058705326135333797603381/60057490791760307520379093366334329920291443058810028866530800697232825445610594649648227466409062367066291505365662209808250918194312173647678174016062192343190917846455405097870127186729143900347189042241457526470419739564391129299524369560859467147966388820192690794384105765028540106004554009904365167349019667975832668621414182373120