# Manifold: Census Knot K8_80 # Number of Tetrahedra: 8 # Number Field x^27 + 24*x^26 + 233*x^25 + 1344*x^24 + 5150*x^23 + 14291*x^22 + 26481*x^21 + 24606*x^20 - 27579*x^19 - 148491*x^18 - 270174*x^17 - 238702*x^16 + 54729*x^15 + 475819*x^14 + 653353*x^13 + 341264*x^12 - 242478*x^11 - 585813*x^10 - 429780*x^9 - 20794*x^8 + 221848*x^7 + 170345*x^6 + 24643*x^5 - 33147*x^4 - 17696*x^3 - 992*x^2 + 1280*x + 256 # Approximate Field Generator -0.234309962000117 + 1.03624259568555*I # Shape Parameters -5502661756444242153356087874241828640899214680843432839701/3896426828034124067524924613656252228432576200704985040896*y^26 - 29689372591097863849555146261690929358508683703222629594487/974106707008531016881231153414063057108144050176246260224*y^25 - 976092908686646697345724090435379912006377286370743144054797/3896426828034124067524924613656252228432576200704985040896*y^24 - 1151085432427992061825706344509892308318659008158494637325537/974106707008531016881231153414063057108144050176246260224*y^23 - 6655675102230808252865247732666876961460877976086280237095235/1948213414017062033762462306828126114216288100352492520448*y^22 - 25711629222561458199827081037807888066670221014778962434195015/3896426828034124067524924613656252228432576200704985040896*y^21 - 3831683999710926836759347058666716841036739628252155286836827/1298808942678041355841641537885417409477525400234995013632*y^20 + 36177832328920118655481170564180758907002503049048913516839771/1948213414017062033762462306828126114216288100352492520448*y^19 + 245659972221403049430688662201255235234507093973386088693612879/3896426828034124067524924613656252228432576200704985040896*y^18 + 106023202832702204252519316716870820469724227988387319007752817/1298808942678041355841641537885417409477525400234995013632*y^17 - 1444998017794032002565857115547259202488682681398419138973287/1948213414017062033762462306828126114216288100352492520448*y^16 - 344013772314644072413389790663393018987292653180808039980674601/1948213414017062033762462306828126114216288100352492520448*y^15 - 1189391017870619560719873350316563675789225502518304776283223013/3896426828034124067524924613656252228432576200704985040896*y^14 - 640134188874901627327782842831667895848595379016395532230189995/3896426828034124067524924613656252228432576200704985040896*y^13 + 882588871848434607279366467849162829395473553954299129274365639/3896426828034124067524924613656252228432576200704985040896*y^12 + 479873693077836803956539679940047199073569827682692405289677679/974106707008531016881231153414063057108144050176246260224*y^11 + 206210014814036796240055552994096501969011098660580653844124745/649404471339020677920820768942708704738762700117497506816*y^10 - 546419722011528707454985288599652497960566040194910850725112655/3896426828034124067524924613656252228432576200704985040896*y^9 - 193394941741815732599971758664498556177211591842529130318464353/487053353504265508440615576707031528554072025088123130112*y^8 - 476289900482155654474341046675499776223243083585323375902287247/1948213414017062033762462306828126114216288100352492520448*y^7 + 5133409074831238765957854253389971558745726919764479493546873/81175558917377584740102596117838588092345337514687188352*y^6 + 221350052555506625360133380864191846566770432700119718614352353/1298808942678041355841641537885417409477525400234995013632*y^5 + 220558171152592018034090773846799062517311516359268265467900669/3896426828034124067524924613656252228432576200704985040896*y^4 - 120627865833869589661677663956158166625316198902951757022385061/3896426828034124067524924613656252228432576200704985040896*y^3 - 18168519832755833250704270644434682705752205716986137901442929/974106707008531016881231153414063057108144050176246260224*y^2 + 268082806340087747806788190191722337959948912532973915016725/243526676752132754220307788353515764277036012544061565056*y + 28177019421121662930834432410050517532836952942685143438943/20293889729344396185025649029459647023086334378671797088 -385454111581160024734060684735523757423074303461015333385490935/2659960714604628696763681869589334854609972019681269787918336*y^26 - 2251599593512383342160309957006011493837776111149228748823490135/664990178651157174190920467397333713652493004920317446979584*y^25 - 84097735567091175275507991832855492936804637827099326464411346079/2659960714604628696763681869589334854609972019681269787918336*y^24 - 116175518804379188422601058424001488853860326379727535453757854325/664990178651157174190920467397333713652493004920317446979584*y^23 - 845143708013517553905071190889260108609842288730932363913258273329/1329980357302314348381840934794667427304986009840634893959168*y^22 - 4436171090317405828643478375484732204610738753526025165787253206253/2659960714604628696763681869589334854609972019681269787918336*y^21 - 7392658008029788512913884698025477658899946860728390749751860638979/2659960714604628696763681869589334854609972019681269787918336*y^20 - 2396827532879386262268545395952488003784079503946895898084599882523/1329980357302314348381840934794667427304986009840634893959168*y^19 + 13673469693714339496478031256901754965489704768402995551293779755429/2659960714604628696763681869589334854609972019681269787918336*y^18 + 48564047887024430852076465271128157830776151534904482276508780705081/2659960714604628696763681869589334854609972019681269787918336*y^17 + 36664319939333622467133847882676577787120453384569308663884592017375/1329980357302314348381840934794667427304986009840634893959168*y^16 + 22738911281241447694045439565240860531310238340648283102850283565605/1329980357302314348381840934794667427304986009840634893959168*y^15 - 49965123888401563914335584247562247842342410433041450117090448493239/2659960714604628696763681869589334854609972019681269787918336*y^14 - 151721038241158923541188733384969976560567409614776060420003000674609/2659960714604628696763681869589334854609972019681269787918336*y^13 - 155573708660632745806744474716514413599380480588244648227187181249339/2659960714604628696763681869589334854609972019681269787918336*y^12 - 8201801908587741694304498853838585796699923187749232226305809530709/664990178651157174190920467397333713652493004920317446979584*y^11 + 57157290018549157907293059200072013539716871451405782547870840243193/1329980357302314348381840934794667427304986009840634893959168*y^10 + 153286712322647745610128004894527621607836180248285573905456802100507/2659960714604628696763681869589334854609972019681269787918336*y^9 + 4273937061485074886041823553687246091078978541653358514041272614527/166247544662789293547730116849333428413123251230079361744896*y^8 - 17701870595143793732313108962159908555256511173525952720235798529765/1329980357302314348381840934794667427304986009840634893959168*y^7 - 1970721157840444361671446502114760672354319539515642647319185041007/83123772331394646773865058424666714206561625615039680872448*y^6 - 25639309508588599188005804680516914340722934910765473100748999284687/2659960714604628696763681869589334854609972019681269787918336*y^5 + 6782092596734146294079316343944488321228018311337024402064329636615/2659960714604628696763681869589334854609972019681269787918336*y^4 + 8476890562908072678874576171010932427919099774993178970269286847905/2659960714604628696763681869589334854609972019681269787918336*y^3 + 359976224266937496092890519144318964519759833507629768874045094643/664990178651157174190920467397333713652493004920317446979584*y^2 - 33286364360050288655733610485970291646614668350744387567268301581/166247544662789293547730116849333428413123251230079361744896*y - 2427448062349476449619241554680437834626470985503337469399068203/41561886165697323386932529212333357103280812807519840436224 -1312084758935866956154480726279411067835039729828495626259247/23865614321709009913590163258644544899149529229318033375488*y^26 - 3823446282163704882177506780371386249813362921876143768756927/2983201790213626239198770407330568112393691153664754171936*y^25 - 284677152424664283677008663176657680698234251526484480249603399/23865614321709009913590163258644544899149529229318033375488*y^24 - 97977141001722039155020396813515422175935363048838040378668737/1491600895106813119599385203665284056196845576832377085968*y^23 - 2839483874010417126039970989970355015692415111452481675606234177/11932807160854504956795081629322272449574764614659016687744*y^22 - 14844776052501149315918944738932632548926758943614102152635261917/23865614321709009913590163258644544899149529229318033375488*y^21 - 8178115517670992164595832396496205426329296775337077768589659941/7955204773903003304530054419548181633049843076439344458496*y^20 - 7704394899945144798312967045062505716456850096708428658373753801/11932807160854504956795081629322272449574764614659016687744*y^19 + 46786155983582919054123219194616307159364528092558762756579889845/23865614321709009913590163258644544899149529229318033375488*y^18 + 54217643533980779951294358597639685359724018844290276879851306407/7955204773903003304530054419548181633049843076439344458496*y^17 + 121305245783246336507141048239505285640010921000424491926755936761/11932807160854504956795081629322272449574764614659016687744*y^16 + 73156238964492625412813494018889305030439055464351678831434952809/11932807160854504956795081629322272449574764614659016687744*y^15 - 172460398897334848666243553137641362997415851646160158812143287879/23865614321709009913590163258644544899149529229318033375488*y^14 - 505696778565662255766851373638002166698898484618809407276024940021/23865614321709009913590163258644544899149529229318033375488*y^13 - 509407090566289797017001410869827328300590076652729068202082640183/23865614321709009913590163258644544899149529229318033375488*y^12 - 1521156147659378784154621149128080538997705029525231939334222185/372900223776703279899846300916321014049211394208094271492*y^11 + 64189037795970830126642031613053335682606780371166823285055155059/3977602386951501652265027209774090816524921538219672229248*y^10 + 503723826066825472997181571636634823748614501869557749613081284155/23865614321709009913590163258644544899149529229318033375488*y^9 + 54352034536072173567998171534899809376041009656262832998754683439/5966403580427252478397540814661136224787382307329508343872*y^8 - 61137078781601730157438682156205565115618550761980534485585704653/11932807160854504956795081629322272449574764614659016687744*y^7 - 8624157895605055212139148311861513629559355885950034247281996939/994400596737875413066256802443522704131230384554918057312*y^6 - 27043433824431280470905925511921027259768892909809863071403060973/7955204773903003304530054419548181633049843076439344458496*y^5 + 23475864253637659705432963392931604877918538111044555997733433635/23865614321709009913590163258644544899149529229318033375488*y^4 + 27343284852345969140919813532834543967390739926772867303117771493/23865614321709009913590163258644544899149529229318033375488*y^3 + 275612110873266811568121935472924160231870200192728463993029453/1491600895106813119599385203665284056196845576832377085968*y^2 - 54113884980187742759966260971613694816912056227929864829385037/745800447553406559799692601832642028098422788416188542984*y - 2543835406635003948583783563240720607368866341891531371127371/124300074592234426633282100305440338016403798069364757164 -y^26 - 23*y^25 - 210*y^24 - 1134*y^23 - 4016*y^22 - 10275*y^21 - 16206*y^20 - 8400*y^19 + 35979*y^18 + 112512*y^17 + 157662*y^16 + 81040*y^15 - 135769*y^14 - 340050*y^13 - 313303*y^12 - 27961*y^11 + 270439*y^10 + 315374*y^9 + 114406*y^8 - 93612*y^7 - 128236*y^6 - 42109*y^5 + 17466*y^4 + 15681*y^3 + 2015*y^2 - 1023*y - 256 y + 1 8854862360502347178181775228320560024709309855932544988299/62150037296117213316641050152720169008201899034682378582*y^26 + 618580757693568999791807826056959945621531017081426099439901/186450111888351639949923150458160507024605697104047135746*y^25 + 5748026924730564905126926348527360636760251802159864075260097/186450111888351639949923150458160507024605697104047135746*y^24 + 31602618238878568954115216635375085766379065735707969461024639/186450111888351639949923150458160507024605697104047135746*y^23 + 57139491434372221967144163267480350428054410836330072285823305/93225055944175819974961575229080253512302848552023567873*y^22 + 298226479016291129575956304034206702880789740764677622247660283/186450111888351639949923150458160507024605697104047135746*y^21 + 245576551431555554650414741135220971903410300587588600815125809/93225055944175819974961575229080253512302848552023567873*y^20 + 101498611718818009594575406840081232292025593093146898494396555/62150037296117213316641050152720169008201899034682378582*y^19 - 947948986828118463400634173845502666483841340205128661788155785/186450111888351639949923150458160507024605697104047135746*y^18 - 1633740032193870615401582176685047814778459583952556141084407998/93225055944175819974961575229080253512302848552023567873*y^17 - 1617007513191699685018233713515094056110487064986335073243181103/62150037296117213316641050152720169008201899034682378582*y^16 - 1447087489316332172759978824986045689333972817285814000799739125/93225055944175819974961575229080253512302848552023567873*y^15 + 3501294842988270940306608343184218571014591754836635249505250261/186450111888351639949923150458160507024605697104047135746*y^14 + 5068476095023871071100916933964137360702806911532266678497156880/93225055944175819974961575229080253512302848552023567873*y^13 + 5073015427116479598925130081119341754567909800853848241897824725/93225055944175819974961575229080253512302848552023567873*y^12 + 1867740837009227795452760653326570732516952693099994126953172819/186450111888351639949923150458160507024605697104047135746*y^11 - 3872908299771264719770824733353220173630052238152684284380532709/93225055944175819974961575229080253512302848552023567873*y^10 - 3348419017155902985821355116548726009193110210196465120989284895/62150037296117213316641050152720169008201899034682378582*y^9 - 4287053549438843116035502815915024791798656906881308437552292047/186450111888351639949923150458160507024605697104047135746*y^8 + 1238256982676156329116126199534270026601071823910737271933821775/93225055944175819974961575229080253512302848552023567873*y^7 + 2062284916027486243801837355317324545446545460306671131739547819/93225055944175819974961575229080253512302848552023567873*y^6 + 532832570702193977425035212655646806410363900446085915184598251/62150037296117213316641050152720169008201899034682378582*y^5 - 79059953010111397184527205820949320831631542113608703614235887/31075018648058606658320525076360084504100949517341189291*y^4 - 271035310164243366938086627615097197778748073632287971139743460/93225055944175819974961575229080253512302848552023567873*y^3 - 86264742998329495171409973969460339160607681081926247947852735/186450111888351639949923150458160507024605697104047135746*y^2 + 17199369417684864089688979731971056200229171160661468968401696/93225055944175819974961575229080253512302848552023567873*y + 4813170076090513520003293141305473781428793003996502534687921/93225055944175819974961575229080253512302848552023567873 261250793139953956031171314496148885020943931745055044214747/41561886165697323386932529212333357103280812807519840436224*y^26 + 1522646336136813212705119503472454954049831741488381732429895/10390471541424330846733132303083339275820203201879960109056*y^25 + 56688144977928973488006023612149863356788566721435498253949411/41561886165697323386932529212333357103280812807519840436224*y^24 + 78045864388750763786888318524695108089411259060406755627654797/10390471541424330846733132303083339275820203201879960109056*y^23 + 565500689392470431272340898618586340304460874296954556627457901/20780943082848661693466264606166678551640406403759920218112*y^22 + 2956603890497408672402173376677080912489369329262382782987438873/41561886165697323386932529212333357103280812807519840436224*y^21 + 4887059521743662618847825800990881671692527702411446721042959431/41561886165697323386932529212333357103280812807519840436224*y^20 + 1535325828438401609315487897348295522482668890289394755485177671/20780943082848661693466264606166678551640406403759920218112*y^19 - 9315721512404413433182715554522553690539753207616839460271018033/41561886165697323386932529212333357103280812807519840436224*y^18 - 32395752409537657350063213229785536772613984523514262075388835237/41561886165697323386932529212333357103280812807519840436224*y^17 - 24164277813323120881100065874258827708794689772632474805383964267/20780943082848661693466264606166678551640406403759920218112*y^16 - 14577744420219968567422443585855555725152903348469965062428295265/20780943082848661693466264606166678551640406403759920218112*y^15 + 34338621928073542769359413891740577320416836872478775886137984251/41561886165697323386932529212333357103280812807519840436224*y^14 + 100729704912123760863652400345365257092873938332794340974038961501/41561886165697323386932529212333357103280812807519840436224*y^13 + 101488393631041317591426723458940698738207832613317902395037186207/41561886165697323386932529212333357103280812807519840436224*y^12 + 4853771887809867111594123406089122957720668110117781019590112653/10390471541424330846733132303083339275820203201879960109056*y^11 - 38355500079866775323681928429707670380306603330873930416433093013/20780943082848661693466264606166678551640406403759920218112*y^10 - 100354736475163667066921739701500743576707143698327014313202077455/41561886165697323386932529212333357103280812807519840436224*y^9 - 1353887659702276706365112377561510485828032732748578946479510425/1298808942678041355841641537885417409477525400234995013632*y^8 + 12176657439514701929288249188593357226290707504204905588208524529/20780943082848661693466264606166678551640406403759920218112*y^7 + 322178642891856408071989750213613717315901527824096361352565729/324702235669510338960410384471354352369381350058748753408*y^6 + 16167570040403620221738926083082490007122783999327930247060394451/41561886165697323386932529212333357103280812807519840436224*y^5 - 4678027256235852565803624930701382119731233707297957538257644795/41561886165697323386932529212333357103280812807519840436224*y^4 - 5449359390888902746680242939523918192582802824141918453601708365/41561886165697323386932529212333357103280812807519840436224*y^3 - 219621597549886151153764847589452645645639281294871897007727179/10390471541424330846733132303083339275820203201879960109056*y^2 + 21585236681938450237716929032405656028353979390897039130535745/2597617885356082711683283075770834818955050800469990027264*y + 1521588082929454732599958988136458057392447340478170417778651/649404471339020677920820768942708704738762700117497506816 2281072804565628963311266273348317579555896531172638113549/53271460539529039985692328702331573435601627744013467356*y^26 + 53173224772140087041304696769731009057123378738299643787177/53271460539529039985692328702331573435601627744013467356*y^25 + 164945049344747178443822094800989626783990729333938062943375/17757153513176346661897442900777191145200542581337822452*y^24 + 908223335803074326679763691756712971479030325253265546758711/17757153513176346661897442900777191145200542581337822452*y^23 + 4934757433724258588969352280941943738166712200394115962537541/26635730269764519992846164351165786717800813872006733678*y^22 + 25796603820924577783400058078424376025274290278979519683902633/53271460539529039985692328702331573435601627744013467356*y^21 + 10656702819148334850122536595464713143479114817524103694177835/13317865134882259996423082175582893358900406936003366839*y^20 + 26754780356499664155695700341292859241736758860656932825606095/53271460539529039985692328702331573435601627744013467356*y^19 - 81337301562159810226493492531931245268760307367654136488843929/53271460539529039985692328702331573435601627744013467356*y^18 - 141323023868889663340627350844181280820572699480492865435073233/26635730269764519992846164351165786717800813872006733678*y^17 - 421496354975304431157763489278731822044651055146818784246498397/53271460539529039985692328702331573435601627744013467356*y^16 - 21171967520460230449524985194643111296667744011021370766014375/4439288378294086665474360725194297786300135645334455613*y^15 + 99945805236176184023655784306620217916843629179252861921734309/17757153513176346661897442900777191145200542581337822452*y^14 + 219665670405193232154962724578119994474443661914717448441914033/13317865134882259996423082175582893358900406936003366839*y^13 + 221212119552249472799018679155601900888553199466354747039034634/13317865134882259996423082175582893358900406936003366839*y^12 + 168822707426190428648679920268329627396845199098603417215595057/53271460539529039985692328702331573435601627744013467356*y^11 - 334638263546424702299442259376076841843845524743119063417790087/26635730269764519992846164351165786717800813872006733678*y^10 - 875025374470261444898734773340999356416118874476637920794773343/53271460539529039985692328702331573435601627744013467356*y^9 - 377475613062115014215944741579752831727940153535251648793479573/53271460539529039985692328702331573435601627744013467356*y^8 + 35424743304421248468660820714503710267910992144035306127483313/8878576756588173330948721450388595572600271290668911226*y^7 + 179766708693955779764515384036728768902652079117701531726425903/26635730269764519992846164351165786717800813872006733678*y^6 + 46953781995351143711599572130551900918511751229564737157770787/17757153513176346661897442900777191145200542581337822452*y^5 - 10200666508673640651044145235702271289891073517252633054293058/13317865134882259996423082175582893358900406936003366839*y^4 - 11871743489668012411191520273932276837046644285437905704538250/13317865134882259996423082175582893358900406936003366839*y^3 - 7653684423537238151027497176652578013387413991426043597341795/53271460539529039985692328702331573435601627744013467356*y^2 + 250620011481902260107896591745408067806791444360456182615872/4439288378294086665474360725194297786300135645334455613*y + 211966783687857619105625272129051307830218801313790987296256/13317865134882259996423082175582893358900406936003366839 # A Gluing Matrix {{1,2,4,2,0,-1,1,0},{0,1,2,2,0,-1,1,0},{0,0,1,2,0,-1,1,0},{2,4,6,3,-1,-2,1,0},{0,0,0,-1,0,0,0,0},{0,0,0,-2,0,1,0,0},{2,4,6,2,0,-1,1,0},{0,0,0,0,0,-1,0,2}} # B Gluing Matrix {{1,0,0,0,0,0,4,0},{0,1,0,0,0,0,2,0},{0,0,1,0,0,0,0,0},{0,0,0,1,0,0,4,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,2,2,1},{0,0,0,0,0,0,6,0},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {5, 3, 1, 5, 0, 2, 6, 0} # f Combinatorial flattening {-3, -1, 3, 0, -3, 4, 2, 4} # f' Combinatorial flattening {0, 0, 0, 0, 0, 0, 0, -2} # 1 Loop Invariant -69340307619389409790686082898213231304561070134414206611790099/2597617885356082711683283075770834818955050800469990027264*y^26 - 404379252289376257878080531035720449040827242797982387045643985/649404471339020677920820768942708704738762700117497506816*y^25 - 15067998003239074108864273268752634723496597058739155034218540763/2597617885356082711683283075770834818955050800469990027264*y^24 - 20763605027920462641837037109685025829743417666666353449257245495/649404471339020677920820768942708704738762700117497506816*y^23 - 150605692289929635664925130882375317418849026413901631062529942357/1298808942678041355841641537885417409477525400234995013632*y^22 - 788219110319463482555331347396058701539530832061572169175418360561/2597617885356082711683283075770834818955050800469990027264*y^21 - 1305644622114233404762878814180018033876245183949134308752372568759/2597617885356082711683283075770834818955050800469990027264*y^20 - 413565424340445454301671957549487224738919426741410486477745923619/1298808942678041355841641537885417409477525400234995013632*y^19 + 2469772461399685154962198422040952381740689968160166679635942175529/2597617885356082711683283075770834818955050800469990027264*y^18 + 8635126586989918986115311193064020089699438650866607940046560216965/2597617885356082711683283075770834818955050800469990027264*y^17 + 6460900176515416361358378020555261400117892547508722429689936552463/1298808942678041355841641537885417409477525400234995013632*y^16 + 3925474057223747416343923940674548534927054150370194936153073621281/1298808942678041355841641537885417409477525400234995013632*y^15 - 9085945453111964841586915952783181419701024615343206358211567776323/2597617885356082711683283075770834818955050800469990027264*y^14 - 26883654910104920055495541556704025543714288706237954909983079969133/2597617885356082711683283075770834818955050800469990027264*y^13 - 27206297663832856041434008210613470061939686948409144737476203300303/2597617885356082711683283075770834818955050800469990027264*y^12 - 1334593109890325340164604322187686660123861881407723875700527682695/649404471339020677920820768942708704738762700117497506816*y^11 + 10210486984548138876162613874854544127472280633700172231967092996733/1298808942678041355841641537885417409477525400234995013632*y^10 + 26878547985820317728785712566651305040884103585923960933887563026647/2597617885356082711683283075770834818955050800469990027264*y^9 + 1462379880523535141275537019544099261918773975413446328575847090305/324702235669510338960410384471354352369381350058748753408*y^8 - 3222946244882369232641709770116861150595486514187292708908815656681/1298808942678041355841641537885417409477525400234995013632*y^7 - 690566298596772420356067292142329831468876524864001482125112998891/162351117834755169480205192235677176184690675029374376704*y^6 - 4370322067782269400533936445143475135621012412982790721763442202891/2597617885356082711683283075770834818955050800469990027264*y^5 + 1238356143723215166794143096856666837785212751355075534035842551083/2597617885356082711683283075770834818955050800469990027264*y^4 + 1466006794032329369714895767556764887120811523265296361447086878013/2597617885356082711683283075770834818955050800469990027264*y^3 + 59781514098334189218545957346825911361303453820445841006659235225/649404471339020677920820768942708704738762700117497506816*y^2 - 5793472186618255674263807953503992952530685964667304291601827021/162351117834755169480205192235677176184690675029374376704*y - 411110044960391984347128059701898076640626199226803745531125477/40587779458688792370051298058919294046172668757343594176 # 2 Loop Invariant -527982950121379497159899440314747241594724318715797451408368466155201216028307537235819738172046316215026022314836847992198329216633753817168500021819/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^26 - 12308138543069077087686333268808834764303161388860268470675595849779471056038921958841278350880053169672381749435364437502640477350278025441083811589031/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^25 - 12727440228877337260552599206645303919799308546871422196817891464328079513887491536059579249478969906635450376170577168535692407665101104765259786254123/11304561808216047540906235597753931529737781206647787376367643248309591433034796080013608462858591808992728615544220930582030015981235874893470729344*y^24 - 210249424165255254490996822307845533788515820738243487484873930944091017916467865259791085583875202793760914444027943764275777684414715454339947190713013/33913685424648142622718706793261794589213343619943362129102929744928774299104388240040825388575775426978185846632662791746090047943707624680412188032*y^23 - 1142418823128977789424252919173882948922511447998718959908077677995595612231003803692710794789106849448082233899973988489568658010323672276091321372692353/50870528136972213934078060189892691883820015429915043193654394617393161448656582360061238082863663140467278769948994187619135071915561437020618282048*y^22 - 5972148534405783472512636797963417469620360781173107129774173857237518118188868231770670872718961958589034949516997702504290496503557239157072852821464315/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^21 - 1233623072905605940954596018523215315004193240232626134276632263330698514723920788305009448412517851655284915020908545940070650289088956136304327575619567/12717632034243053483519515047473172970955003857478760798413598654348290362164145590015309520715915785116819692487248546904783767978890359255154570512*y^20 - 6194455262122799551878537673433202168305045055386106592817908644956272951136025668287286974416769407326301303753033928768969364997278102212142566021623745/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^19 + 18830294605958324494302622568202836454034481999588923780169801094721836103852748208399896789223070726477452334003963819824854488577520174617553689706071255/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^18 + 32719679294831390392627413307680432971341133458385840156331726233967842456918513277368527539857247665363177437090796622091875250540290351346624610024461963/50870528136972213934078060189892691883820015429915043193654394617393161448656582360061238082863663140467278769948994187619135071915561437020618282048*y^17 + 97584979933368170755447294698209836072672325285916674200088822276449989991132242088467768333956050579248164057557536245746833570261538909184588457045687575/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^16 + 4901372965190167321128763385322528713695051348503810711800529927576516491507755767499591912791773610944589042202776722066158392913787316846646447726978205/8478421356162035655679676698315448647303335904985840532275732436232193574776097060010206347143943856744546461658165697936522511985926906170103047008*y^15 - 7714390403723986404905282979814863817388107418902466654779758629253631113430415095351844855850265280212951795607335321156095670114322771084259215902429297/11304561808216047540906235597753931529737781206647787376367643248309591433034796080013608462858591808992728615544220930582030015981235874893470729344*y^14 - 6357531910868574572345452219103520347552632676848331859968208308433097897491215663255281479644594593121765716206623678929732538054907210301794345649659827/3179408008560763370879878761868293242738750964369690199603399663587072590541036397503827380178978946279204923121812136726195941994722589813788642628*y^13 - 3200833836607191985789320748543309529625551272754471050879893414287400174112791343499865864036122815004827371913243302533170888629872774625164140492301771/1589704004280381685439939380934146621369375482184845099801699831793536295270518198751913690089489473139602461560906068363097970997361294906894321314*y^12 - 39055226347455209422800842247144944498299944133101915916698010356600666602019654846320089304495520067918295910822828924684442949191410145343284595875863655/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^11 + 77491440992860575123572108569550450788962826237339881670477240256946616222162114849995397851558855113154308765421932120659292748492767527524814011069753445/50870528136972213934078060189892691883820015429915043193654394617393161448656582360061238082863663140467278769948994187619135071915561437020618282048*y^10 + 202585884177267046132163653148648596846549620373692259996260595767652426842933146766156550938678846658571646120461123768382018509609215814884241216512222337/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^9 + 87361580401443503938361176146110830924331449631619715096861045635619970261454740499832133195048572316242996831818057701202038748817601020501376826495997415/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^8 - 8206504568206404285487719163514773841551303237035244118247128591111389849375738409387567074055730451512865286469731084843198582812606189310733540908575061/16956842712324071311359353396630897294606671809971681064551464872464387149552194120020412694287887713489092923316331395873045023971853812340206094016*y^7 - 41621330790334668853452938464571538905852627987143651494783305264739137746953023611411420586318007247549121504487858115430535910668587395852366482800592005/50870528136972213934078060189892691883820015429915043193654394617393161448656582360061238082863663140467278769948994187619135071915561437020618282048*y^6 - 10864776019182440691708445886229604838844427545826661603259256568093850449903498706803212734221860475867813703087444708400597442091689324250571853495513689/33913685424648142622718706793261794589213343619943362129102929744928774299104388240040825388575775426978185846632662791746090047943707624680412188032*y^5 + 1182206249543006206072775145494391773062963298482151554803139661947593098660534191722085205794673336016414639860585415998590265973576758151087314629087009/12717632034243053483519515047473172970955003857478760798413598654348290362164145590015309520715915785116819692487248546904783767978890359255154570512*y^4 + 2747841671750302637324092935647292127166108030725438535307762970679960072777588191699883861859002375708051249907279447038465453385324620187537157780677137/25435264068486106967039030094946345941910007714957521596827197308696580724328291180030619041431831570233639384974497093809567535957780718510309141024*y^3 + 1769003825463914485372976804805953764101250606828734278077950038989810409734458940796613146764168946386483179233757746280316478237353858121874983058619669/101741056273944427868156120379785383767640030859830086387308789234786322897313164720122476165727326280934557539897988375238270143831122874041236564096*y^2 - 29010381609937838701662768006919272558018858637277800902948391052514205737924911735756141751167879124524440334395680249458733646534790310204073817714831/4239210678081017827839838349157724323651667952492920266137866218116096787388048530005103173571971928372273230829082848968261255992963453085051523504*y - 1531280896738630007576028068520896945061026845213739435133049271951806575090883902302585580819131322456089180795828962076148847206720835546069731006316/794852002140190842719969690467073310684687741092422549900849915896768147635259099375956845044744736569801230780453034181548985498680647453447160657 # 3 Loop Invariant -8547006762107165383615435398965649993638687992840139278552390704585267706171766091741728893383462055622195876233831232715410232627849289473411885122933119117466297072310133031536205642429976528475/11090977392346197715124527862633165347316890550943803423020357827745255198738646397122513203753525280261171561146738910352904360900880475368942533893064219808614508052135215424302497706559618865152*y^26 - 691821560019765392630131839769900101073896583756840941434751719021880061348841612877093572655975453531438712045638020368598281667932213854110534712849931865774217259911042232941944091128128318723/38510338167868742066404610634142935233739203301888206329931798013004358328953633323342059735255296112017956809537287883169806808683612761697717131573139652113244819625469498001050339258887565504*y^25 - 1854295366645232417154750523603731743090642497359341580583369592812202351821095117942113327602335705812245317824310436268629534194580770404628621525467603404013214346520403374889581291929918247320003/11090977392346197715124527862633165347316890550943803423020357827745255198738646397122513203753525280261171561146738910352904360900880475368942533893064219808614508052135215424302497706559618865152*y^24 - 1276334471454063816039420961021485316537723700602088108343989535063782129040186184014356052380367843859649436687344117346974142215380422744348172169736841334828120950418734491455368960408068749510075/1386372174043274714390565982829145668414611318867975427877544728468156899842330799640314150469190660032646445143342363794113045112610059421117816736633027476076813506516901928037812213319952358144*y^23 - 2054879021749758907014184204319755368447783959845307064478831825341075966083421912554231154461576503776336873299754803592231864509783706279770503121048780461810938450412333980403147181624199427968997/616165410685899873062473770146286963739827252830211301278908768208069733263258133173472955764084737792287308952596606130716908938937804187163474105170234433811917114007511968016805428142201048064*y^22 - 32226999193517881187490549505098763316654122438812477924374686599337899663069247292489336155847490611907184105483182520173199150106193970799637153657634622180667673478091375251886198830255116067880091/3696992464115399238374842620877721782438963516981267807673452609248418399579548799040837734584508426753723853715579636784301453633626825122980844631021406602871502684045071808100832568853206288384*y^21 - 159770045221077198236506736788654708583261640074813472279433042112024679895195090284805540209947117378235956388815002469856649407602336991727826462471714055396562372867854173571711088113426286089693011/11090977392346197715124527862633165347316890550943803423020357827745255198738646397122513203753525280261171561146738910352904360900880475368942533893064219808614508052135215424302497706559618865152*y^20 - 50148956151901791379979294271570301573746964006301842700616705714829524513485574780898299639744667455856424981377152035978966941256593135873973657727096964889321648407845986864026956294582854435452937/5545488696173098857562263931316582673658445275471901711510178913872627599369323198561256601876762640130585780573369455176452180450440237684471266946532109904307254026067607712151248853279809432576*y^19 + 101603156188947576974662542460287590587076590682571260072554396183762948894569293866037358695055738280439485886197251593945752322950062985310423385239961189678223829876108350945923180196620268086075283/3696992464115399238374842620877721782438963516981267807673452609248418399579548799040837734584508426753723853715579636784301453633626825122980844631021406602871502684045071808100832568853206288384*y^18 + 1059365425245932327052151992352270572151444966504722436586402346520804756186390354234916628994902748391751279760697114430604088106045491808447753620104769023833963912997516587662964508255255959786662929/11090977392346197715124527862633165347316890550943803423020357827745255198738646397122513203753525280261171561146738910352904360900880475368942533893064219808614508052135215424302497706559618865152*y^17 + 789929002555229293358113566841215159198131901258268574025552221954528827282469612064579598724346200144415486755078932742330450040195173695473771386015937795436281307583546131017982636572503492008146625/5545488696173098857562263931316582673658445275471901711510178913872627599369323198561256601876762640130585780573369455176452180450440237684471266946532109904307254026067607712151248853279809432576*y^16 + 476169156952570467216894295604597057325650341381480330537168051453270441992684184587304096106789945018548457599132206912306383572099238652055219922737413103043875026936059522030704464053512111783066013/5545488696173098857562263931316582673658445275471901711510178913872627599369323198561256601876762640130585780573369455176452180450440237684471266946532109904307254026067607712151248853279809432576*y^15 - 1123822683057435793604107270954409047538872616057281850218686835428998363049152177145395244245745035340979197237187848607819201202090163554071695727539649716093276103757304626469061587410732323634139971/11090977392346197715124527862633165347316890550943803423020357827745255198738646397122513203753525280261171561146738910352904360900880475368942533893064219808614508052135215424302497706559618865152*y^14 - 1097842416037605546771182776286285447911453415103555676073758364981994975260639037641167167600569458630049651713528965837357916290103041489455860928376694979515715087794451158738270292130904430113286507/3696992464115399238374842620877721782438963516981267807673452609248418399579548799040837734584508426753723853715579636784301453633626825122980844631021406602871502684045071808100832568853206288384*y^13 - 1105569600029393898772297240574655496463581778883157027414377158634252516873552530283310356866616644913210003627449448583442631017284085680563298034933738871082080921848536014547769390166836378876524249/3696992464115399238374842620877721782438963516981267807673452609248418399579548799040837734584508426753723853715579636784301453633626825122980844631021406602871502684045071808100832568853206288384*y^12 - 2928861329452113992321868941209651113789352151712211644781139104278438397243430310117246655771364667145757042421074781795811710507710755586837015023083910982178253220074740076960795189919684546952857/51347117557158322755206147512190580311652271069184275106575730684005811105271511097789412980340394816023942412716383844226409078244817015596956175430852869484326426167292664001400452345183420672*y^11 + 1254485924101050558433746400204646719680515385865100134135901832964875840896589157090723350724737788861505726847617121997551414234227550497858221380003338897376500497029350730516455563676768235149714869/5545488696173098857562263931316582673658445275471901711510178913872627599369323198561256601876762640130585780573369455176452180450440237684471266946532109904307254026067607712151248853279809432576*y^10 + 3280001248167693191383196803497041557760554946523351664568784082005486200465696515767240779738125527588861010869876532296926372442932385385407438387619945985649014423403607153846797728354648640171660935/11090977392346197715124527862633165347316890550943803423020357827745255198738646397122513203753525280261171561146738910352904360900880475368942533893064219808614508052135215424302497706559618865152*y^9 + 117887223613906439097637292942958487939006997911156522160155069267884854466342176386334882885979709704032744130423619391978821911658755002710520748596954547672480310199730407020904190348398508395005039/924248116028849809593710655219430445609740879245316951918363152312104599894887199760209433646127106688430963428894909196075363408406706280745211157755351650717875671011267952025208142213301572096*y^8 - 398545253489943230430594760707630890571001047205291397867730137560221588319581022937376116885377877130276946228588582532274036693705895467817828464715185895298005744531475286047999322273871678953788009/5545488696173098857562263931316582673658445275471901711510178913872627599369323198561256601876762640130585780573369455176452180450440237684471266946532109904307254026067607712151248853279809432576*y^7 - 168475862257219744460797602151565674062777967636589785094854655593818641950621815324173281603265502085029099149925116610497464967703499695044621479554895530910354115243475858404461854426999639758584147/1386372174043274714390565982829145668414611318867975427877544728468156899842330799640314150469190660032646445143342363794113045112610059421117816736633027476076813506516901928037812213319952358144*y^6 - 175941715183982258763391827120527260036333496560473895582862283720131225178357074032034929487641897261551544854380082135365617774595373050916679693228755584409473132600343579830960540601717130666841233/3696992464115399238374842620877721782438963516981267807673452609248418399579548799040837734584508426753723853715579636784301453633626825122980844631021406602871502684045071808100832568853206288384*y^5 + 153148857143501580736930579275351225503157593959858526528606160063926729035089196827631649128852139061713439037801447354182298329302108330106932069761317706317537958712620348046765245044509424507504215/11090977392346197715124527862633165347316890550943803423020357827745255198738646397122513203753525280261171561146738910352904360900880475368942533893064219808614508052135215424302497706559618865152*y^4 + 19777769499334490021515314272820033583359452490820349847265948653718940016710335599493779058138422516633352264622152276651302901865289393074348124483725903646194624969700537716164391736275932971427577/1232330821371799746124947540292573927479654505660422602557817536416139466526516266346945911528169475584574617905193212261433817877875608374326948210340468867623834228015023936033610856284402096128*y^3 + 1192897639030642032551855956246214306553126431184515438024192660086002077300264571081828648404535922837706402617651884262745835865883635273192466550859399032317728868594064391831065431147599400535637/462124058014424904796855327609715222804870439622658475959181576156052299947443599880104716823063553344215481714447454598037681704203353140372605578877675825358937835505633976012604071106650786048*y^2 - 704959268824693770806785353143283712727983222728170575644141970940012217989621885702997771037893220827772323647402787040475334997692614135857682669937248800859282913962530191386399420415353795180711/693186087021637357195282991414572834207305659433987713938772364234078449921165399820157075234595330016323222571671181897056522556305029710558908368316513738038406753258450964018906106659976179072*y - 3098291932103989650234541278876365586514893471112098263038139102917557256608382168023613490040159947147253286176784093022646512423548215142935106772669056734038452840268482009119770685731224437637/10831032609713083706176296740852700534489150928656058030293318191157475780018209372189954300540552031505050352682362217141508164942266089227482943254945527156850105519663296312795407916562127798 # 4 Loop Invariant 127510472099034005227922122164242580254872183985242716358254571508698403842184132628210233231185210900201080897806000242765427436409270237095672627220919264444609567053832523750401385776802550125412572866329688333344938407146542351940069236988428245184818021438293630188481688290660483494497/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^26 + 74265174007274579319663510001652191082872414395830196814529695956812793835509870025171776348090573454820131335545473760466345448280527207503171648998195177382106338933343120735728369334628202243802669678701742706611806962620619996670555099026338920252632647138168299599243068343791462120031/2606405879869564996757685589264323149520328702661453337318565035282757105195552408193164260689984683066178699652805545121495574955299147679584424570336534138563560857553993692834438013068185027687617323753090673810678722616635583585137849594068313008687733230888204635419062406288812611968*y^25 + 3069038634207362290906597703277387898774015161981127393763428550074052799584554057170892068720384922398292836024016061583105566750610446085188411502974316588638905915621605513853942357948121946951229124691653068553692003576102613686985375672596409602697774832822694439519295527445531667287787/11584026132753622207811935952285880664534794234050903721415844601256698245313566258636285603066598591405238665123580200539980333134662878575930775868162373949171381589128860857041946724747489011944965883347069661380794322740602593711723775973636946705278814359503131712973610694616944942080*y^24 + 25325309944572388273026627290356331907418739538912212419338048724850165188628641477488110326056252828764338799671160350488084520013434983252913441417744765074212089309869931490494710085759553642497135024692677084576281654306871711312356133364335268068755181738333162986063412886733809757905809/17376039199130433311717903928428820996802191351076355582123766901885047367970349387954428404599897887107857997685370300809970499701994317863896163802243560923757072383693291285562920087121233517917448825020604492071191484110903890567585663960455420057918221539254697569460416041925417413120*y^23 + 137455136380053604562379802771088127329186966302087741470343211027793894579831466767763638054771759744830510352255522288135033002859461680204887863559972431912308166115827541203834867339923583099551287301827663409791193800894662285408116729732308396951481998583716277631116793040542401421820859/26064058798695649967576855892643231495203287026614533373185650352827571051955524081931642606899846830661786996528055451214955749552991476795844245703365341385635608575539936928344380130681850276876173237530906738106787226166355835851378495940683130086877332308882046354190624062888126119680*y^22 + 1435545353713274334910655884773132394968063889160002413847287397484231093036344862553064828616198108636610279360312915516627109441590305741276385017504489300974330531407178259298872247529717610055560248837363293167784122019939007615855410089509648163720067854197629681136489485622841781971105159/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^21 + 473360240909066754435519334386811474313406520133363159312153391429602229981387069872309215322044908792746360606810893070865044075535891781139060276944969893864535566148447011535940221090217575615557890501792031410754915654143387984085695589647621878967987683750400818600377990474880538571912493/20851247038956519974061484714114585196162629621291626698548520282262056841564419265545314085519877464529429597222444360971964599642393181436675396562692273108508486860431949542675504104545480221500938590024725390485429780933084668681102796752546504069501865847105637083352499250310500895744*y^20 + 147217735070020026374511943649622940030738982610642022778400737779581875369211407662395621623026039766240191958698345184002446931109051889912678887970621944075737120190077354174578903901023994031713471326356452431682134640667128114480072294214978187000100763135486003440273099569241550451787013/10425623519478259987030742357057292598081314810645813349274260141131028420782209632772657042759938732264714798611222180485982299821196590718337698281346136554254243430215974771337752052272740110750469295012362695242714890466542334340551398376273252034750932923552818541676249625155250447872*y^19 - 4553661630656096303526496673676114724462715521606214008769104159197112703094801177251391744582411266644391650910595276998747466061464577109794646031594680428631986209368948820102006530716963449311948974414425447228135299685879523836079607648153842741312725225380279952206236621444133564526187333/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^18 - 15733404829271696060889768398650146068938685570446234156067002261401645112806691393789132706417548789499793791149245257952455219504885118669009210950700311359405363392176444255051596388950355924336813344198696428082184315170183939378403917886435143849598758907612759087344016820713462219982359089/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^17 - 2338308887358920458633783476782790414208991660309129746150972192909474345505130512912117702567737553595277019988681630675563528980778652951470265996779699290311729745739693609602934102133250661075671874376239509391455795308982682684296454497258990259678073117949148187191972284340082046829741299/10425623519478259987030742357057292598081314810645813349274260141131028420782209632772657042759938732264714798611222180485982299821196590718337698281346136554254243430215974771337752052272740110750469295012362695242714890466542334340551398376273252034750932923552818541676249625155250447872*y^16 - 2330364968903054140850076641570206939104652511550001662934241434814007094101418892043043322337360567459200193947804979732988862748611008857555881403192855816386048367462827788624923646141820267043719804578607286579605486501445756415701422916567219379586797460551147510863588949760300358554498711/17376039199130433311717903928428820996802191351076355582123766901885047367970349387954428404599897887107857997685370300809970499701994317863896163802243560923757072383693291285562920087121233517917448825020604492071191484110903890567585663960455420057918221539254697569460416041925417413120*y^15 + 1869772091243942455947705895613357357980213926230628387468468424153223705249995603284486039783335453544103784168914257461324553615234080337374358179296474401201485037541597759108873985577981521910425720188947794003108466734519139178445293143103307808230554712154805719233976457067741580150571073/11584026132753622207811935952285880664534794234050903721415844601256698245313566258636285603066598591405238665123580200539980333134662878575930775868162373949171381589128860857041946724747489011944965883347069661380794322740602593711723775973636946705278814359503131712973610694616944942080*y^14 + 48847349098666965553706907327368444945031278145850840868477907213802177282242097685432247422300746504983963250054163437434159572871502176427997716130730211913930185177484397055848756657550231594667545994148460370806880610203051617519648810267102901002838011321419059788926258264361854549832978163/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^13 + 48944239753121441539763121067344427845889073603073645331567317326633762667190896425661785685163587305548774037540552458107541250934962621488202564172580867207872128834329125691010324160092980532043336322899136264516827971885735318906326757606985371262507310699710191149792582612977689750410732657/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^12 + 2264782506637939520651292578285815279422813896941395875988285433265802737000574920592272744865402419598629499561381073436284685453495656425965897875920361360634692846111697532444728975440735315104067985115803926524083881013630611111581042470620817353493174501709040436442074368415125208175753551/26064058798695649967576855892643231495203287026614533373185650352827571051955524081931642606899846830661786996528055451214955749552991476795844245703365341385635608575539936928344380130681850276876173237530906738106787226166355835851378495940683130086877332308882046354190624062888126119680*y^11 - 4665172937143257941553035699589752237167367353104227749787350278655673843636701057421667171952423971921056822705956378790926844530599609391083692936337606065007175882762937206645527636022481446183539689572698599499074494523980893654940212045117302718816655922251056022419161987686320558535940909/13032029399347824983788427946321615747601643513307266686592825176413785525977762040965821303449923415330893498264027725607477874776495738397922122851682670692817804287769968464172190065340925138438086618765453369053393613083177917925689247970341565043438666154441023177095312031444063059840*y^10 - 48451397012878972878523621569623544364542275256334194344982378263959949430461638594227810381341185215672551158824583756744648276143983300562196939979593701683024063118371806533411473825428555118341843979979217427997637090991394302123509703623843731895615095154030666918069995204282030482598284473/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^9 - 10348619061118441163476588890863842039909853742435700444979304820819060408172974423931263233902276193046020452988355912034720611780218970556483941077655224766040082745532351739068654543417255207586521768895443035291501214893702851941981985304629412229852959417680210536339006009670338585585467511/52128117597391299935153711785286462990406574053229066746371300705655142103911048163863285213799693661323573993056110902429911499105982953591688491406730682771271217151079873856688760261363700553752346475061813476213574452332711671702756991881366260173754664617764092708381248125776252239360*y^8 + 397864302987667196003147614376333933141829023660550928334847219462790624403986996606802346279145363701123817106423639790464106023223439453243727593015993903955255818897229979538130550926484115874184518265365492488892828085528865136874130109959375646697852861327777332135232115295303356537693823/3475207839826086662343580785685764199360438270215271116424753380377009473594069877590885680919979577421571599537074060161994099940398863572779232760448712184751414476738658257112584017424246703583489765004120898414238296822180778113517132792091084011583644307850939513892083208385083482624*y^7 + 4975486867657594469447561196838867901463003759819410993165395711842773848963882825254506996117482188594199845591180273584524437847897927874060021178282274921470356801031564775982412393274868404736904389751919002601563200885519888309376416113648535524795240380700198694103001954000888946897940683/26064058798695649967576855892643231495203287026614533373185650352827571051955524081931642606899846830661786996528055451214955749552991476795844245703365341385635608575539936928344380130681850276876173237530906738106787226166355835851378495940683130086877332308882046354190624062888126119680*y^6 + 2570534798253390950875854540638722568550847067598063924227524838541368988722812891692305044537591851970363467693481691218206706278636323769305078493555914555785207128456371392733012913553628699536803812441109654010052482654070457792947558532066124956534259719877817034029110183296089606819844461/34752078398260866623435807856857641993604382702152711164247533803770094735940698775908856809199795774215715995370740601619940999403988635727792327604487121847514144767386582571125840174242467035834897650041208984142382968221807781135171327920910840115836443078509395138920832083850834826240*y^5 - 2294102212711897394510369313478788510353476365551826821004887864604744944676381377991209856297202981158617484510583032155813923830443102387678074233452597130086632343909499737346665808528578179607408041084838795177367122464902945301064594846327621457437408526624575019410801716756905922956011779/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^4 - 653792626099561865793807357357740942508115562828088102746680089092424203060986000655888211455501012631457422455337806221720122028320174011872916288225319940600200161841422154872692577320069691149714616324342214570162428983832529193995552929357969933918955338666059573742603512042301084411229991/26064058798695649967576855892643231495203287026614533373185650352827571051955524081931642606899846830661786996528055451214955749552991476795844245703365341385635608575539936928344380130681850276876173237530906738106787226166355835851378495940683130086877332308882046354190624062888126119680*y^3 - 414323971559491054781102986790320237800117887822762876897999644149733042141640146286131331988265953147102484146884274306357316850321223020404324352146353074033924899702423488569939852011129583270222177121085567753561164597985325298865502845973104221143628798743434432537862041218257401798483439/104256235194782599870307423570572925980813148106458133492742601411310284207822096327726570427599387322647147986112221804859822998211965907183376982813461365542542434302159747713377520522727401107504692950123626952427148904665423343405513983762732520347509329235528185416762496251552504478720*y^2 + 6919257231777416192947501373201785125102271350913647741630021386087535346697214936604094852487289284178435613160199225489660089151472315514152330459672029985756418399858357044702768099824295983166742159244880634175110160358851720489490715201508654744456745808220718376936230199611703093044563/4344009799782608327929475982107205249200547837769088895530941725471261841992587346988607101149974471776964499421342575202492624925498579465974040950560890230939268095923322821390730021780308379479362206255151123017797871027725972641896415990113855014479555384813674392365104010481354353280*y + 2892672559415554940161262817523053757625589102585023313496522099542177996167552226854376314691857864569335742837950924322660637686486817206889326585576307213690459064049026906850456906399881311159833490657178404237238588791528739925430022485734050572548764728884125252924948093632859049473889/6516014699673912491894213973160807873800821756653633343296412588206892762988881020482910651724961707665446749132013862803738937388247869198961061425841335346408902143884984232086095032670462569219043309382726684526696806541588958962844623985170782521719333077220511588547656015722031529920