# Manifold: Census Knot K8_45

# Number of Tetrahedra: 8

# Number Field
x^32 + 4*x^31 - 137*x^30 + 330*x^29 + 2336*x^28 - 7425*x^27 - 19236*x^26 + 65110*x^25 + 103272*x^24 - 315019*x^23 - 388502*x^22 + 944506*x^21 + 1002929*x^20 - 1817009*x^19 - 1765530*x^18 + 2232269*x^17 + 2164615*x^16 - 1724629*x^15 - 1849220*x^14 + 811303*x^13 + 1046354*x^12 - 192196*x^11 - 373371*x^10 - 214*x^9 + 80233*x^8 + 10500*x^7 - 9993*x^6 - 2146*x^5 + 716*x^4 + 185*x^3 - 31*x^2 - 7*x + 1 

# Approximate Field Generator
1.25316029924189 - 0.176642835413045*I

# Shape Parameters
108048928858683713553600881343968104303784698597819153016422179881277088029/14914206870957352995164952860638619614103749215955545079657826115866865029*y^31 + 471651626701830329967898234304680218262909592794578436036174382160365602367/14914206870957352995164952860638619614103749215955545079657826115866865029*y^30 - 14631350256427151846675825109851205852223028544780360925053951815728054169804/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 + 30311109931441637428400769097638226201526363656141647455309899041794485048718/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 + 263597705591580712969868248085757572837903886629975029204901363050041430449816/14914206870957352995164952860638619614103749215955545079657826115866865029*y^27 - 706477752413955983845064772184026227528253656586299489934574191528154243059691/14914206870957352995164952860638619614103749215955545079657826115866865029*y^26 - 2338136634684675606141027443681937081261036326200805588873591649289170744571677/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 + 6191077974220972777892060409447122094382722515061079446551910112676505170804298/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 + 13428544077329079404167363265680967599520386037928900486852253276222507427567980/14914206870957352995164952860638619614103749215955545079657826115866865029*y^23 - 29220526487056086514629493403342501104927147395147303338610405041621203400225659/14914206870957352995164952860638619614103749215955545079657826115866865029*y^22 - 52676075445763956627464918136400028420954293290468164918304507586665220118003238/14914206870957352995164952860638619614103749215955545079657826115866865029*y^21 + 83261861463359838092834948173977663998215707339748307551977114826211425595378627/14914206870957352995164952860638619614103749215955545079657826115866865029*y^20 + 138849426003914932403042398226177771907189184471184630604714472054375023416267618/14914206870957352995164952860638619614103749215955545079657826115866865029*y^19 - 147077036737543098158208713817641183761289095859251983812340153599174301204825681/14914206870957352995164952860638619614103749215955545079657826115866865029*y^18 - 244733712994853936955091404690083411705271189705522244637398773471862070855680307/14914206870957352995164952860638619614103749215955545079657826115866865029*y^17 + 154901293710251067489998751529845793644782019200018040626844882435718629281061024/14914206870957352995164952860638619614103749215955545079657826115866865029*y^16 + 291206557804802337467381386802651993450049249134751860816992870507291165440883274/14914206870957352995164952860638619614103749215955545079657826115866865029*y^15 - 84156880218545506716322763261614154118704521249224112232556173811812597832480434/14914206870957352995164952860638619614103749215955545079657826115866865029*y^14 - 232061049604110601254305528201264255281843420080772343073067082474369441863544715/14914206870957352995164952860638619614103749215955545079657826115866865029*y^13 + 6434648377558956535135116584647961341795583179185309042306314931311817004954919/14914206870957352995164952860638619614103749215955545079657826115866865029*y^12 + 117292534866332153139886399135633721406837768230809408245366207276164352967060639/14914206870957352995164952860638619614103749215955545079657826115866865029*y^11 + 20296209434351840887121018386614191614269633741829899311170547732974072249585913/14914206870957352995164952860638619614103749215955545079657826115866865029*y^10 - 34255424466677969131695318037703489739479438942081155740919419276400382754756903/14914206870957352995164952860638619614103749215955545079657826115866865029*y^9 - 12128373994126228499909026155219674549475823799246352362620089119992171636986445/14914206870957352995164952860638619614103749215955545079657826115866865029*y^8 + 4755488668455671234859483688224821187104113037483051641537825335044165051055107/14914206870957352995164952860638619614103749215955545079657826115866865029*y^7 + 2889981344880604966913178176183589284721140070820695869100134773940789256582778/14914206870957352995164952860638619614103749215955545079657826115866865029*y^6 - 125253997542426719195061045004574703555241844690050631967996675063870914116823/14914206870957352995164952860638619614103749215955545079657826115866865029*y^5 - 300053553389171256290435481307945976408413227360966317139090585314643552978876/14914206870957352995164952860638619614103749215955545079657826115866865029*y^4 - 23977613567702700992923142170709477087802418989240312010624793661280336913042/14914206870957352995164952860638619614103749215955545079657826115866865029*y^3 + 14109259311416457310072334336341687226331826915228811505301118412653599393601/14914206870957352995164952860638619614103749215955545079657826115866865029*y^2 + 1553200174726786828159043752617364218517526299516471465203321023530693197780/14914206870957352995164952860638619614103749215955545079657826115866865029*y - 311547699954596998386981231302934858143800219750336134074777514159902109729/14914206870957352995164952860638619614103749215955545079657826115866865029

-468734405701479617885063752097847130365786296874125735274870513124331401950/14914206870957352995164952860638619614103749215955545079657826115866865029*y^31 - 2190944579121563003745763186864329878334926330745803608112538844600083922826/14914206870957352995164952860638619614103749215955545079657826115866865029*y^30 + 62692675779273577415703919854467952823516652318214788768480146675043291372826/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 - 112655142658894764675474084257220976100473771274561931265245865614776723724654/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 - 1164748955933931737319844573151363015498595492456949352328483469889355401990763/14914206870957352995164952860638619614103749215955545079657826115866865029*y^27 + 2686353005670411783197637920089890033961990561180103542278871536552014249453986/14914206870957352995164952860638619614103749215955545079657826115866865029*y^26 + 10708507642114836748782487194303770703148267231775356110831168089851225700630282/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 - 23082124126316885097882504305431907352653061902177506199988988160764040854070960/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 - 62825002374039226613740981764860282006442114150842960652112626038908617298320624/14914206870957352995164952860638619614103749215955545079657826115866865029*y^23 + 103508995516829072904933038903223496703656314929339378808556496673960097303056591/14914206870957352995164952860638619614103749215955545079657826115866865029*y^22 + 245016351869381299700228028478160737330873257286806686425204388697849576477214169/14914206870957352995164952860638619614103749215955545079657826115866865029*y^21 - 270360572865319306347452191368819919047609744930866616654918259363935020024827834/14914206870957352995164952860638619614103749215955545079657826115866865029*y^20 - 625777845665194668188388633173809098104834924574188577059385612761120748604538596/14914206870957352995164952860638619614103749215955545079657826115866865029*y^19 + 415226169378091411834442736008522733486448122379542850491101857962825332188769113/14914206870957352995164952860638619614103749215955545079657826115866865029*y^18 + 1042144965772053547604709173899819774456248373225047029251402813321766929597883886/14914206870957352995164952860638619614103749215955545079657826115866865029*y^17 - 332929156362179399878044107544189445414957043009849079251738496711888505277489939/14914206870957352995164952860638619614103749215955545079657826115866865029*y^16 - 1138277310443371863250927061143722178396215417670036681251802873687965311010672616/14914206870957352995164952860638619614103749215955545079657826115866865029*y^15 + 54763489330393244200994433599552430440685880877816220276779904548678467691896617/14914206870957352995164952860638619614103749215955545079657826115866865029*y^14 + 807820110106759015914614459890293946193448964995085824079529687391549639006662313/14914206870957352995164952860638619614103749215955545079657826115866865029*y^13 + 126212243521453734362818484532221679306227077798477716829968214782364377170024448/14914206870957352995164952860638619614103749215955545079657826115866865029*y^12 - 352534273317797031418044653605978636703714660486796483145901457926913670726314415/14914206870957352995164952860638619614103749215955545079657826115866865029*y^11 - 112721376967319554960683879534996705009184531984655698873803067811341493516321988/14914206870957352995164952860638619614103749215955545079657826115866865029*y^10 + 85758123620634321021552199813768900397649636369286461544379831662431720383444690/14914206870957352995164952860638619614103749215955545079657826115866865029*y^9 + 42528391155069700378362756931560221819449779676526513153225236129472224088091665/14914206870957352995164952860638619614103749215955545079657826115866865029*y^8 - 9349123997115766729409165023753696007573783992781772851877416890252437374065775/14914206870957352995164952860638619614103749215955545079657826115866865029*y^7 - 8092611547415412014327812927600373669702596538056832806229648975632082355332312/14914206870957352995164952860638619614103749215955545079657826115866865029*y^6 - 1311813191380461297764960396588002191413998460627173722925274942694659029198/14914206870957352995164952860638619614103749215955545079657826115866865029*y^5 + 766848195198935868688924875509847279522802774634073487322803201142333992516567/14914206870957352995164952860638619614103749215955545079657826115866865029*y^4 + 70774591007750069043539193992750468838634503428283968490622365510128339018847/14914206870957352995164952860638619614103749215955545079657826115866865029*y^3 - 36283986443822449364658208170007762216969546391339974885143649552232046627056/14914206870957352995164952860638619614103749215955545079657826115866865029*y^2 - 3954268325979083932950876419924333827040828228604249466844053643614832835534/14914206870957352995164952860638619614103749215955545079657826115866865029*y + 880321170783173012318192097438989275264916570127095116855086084415571089827/14914206870957352995164952860638619614103749215955545079657826115866865029

-1570755389837294028940125258693979159629333833743434955621164283223674798508/74571034354786764975824764303193098070518746079777725398289130579334325145*y^31 - 6668646775730174798969776229052321088073470726500690015300914252260093810399/74571034354786764975824764303193098070518746079777725398289130579334325145*y^30 + 42717029242835383536837702100077180887495856940465855701071618152560904596052/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 - 93150859962779448996613348798130795646683585756701515418378593530572319584791/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 - 3787364509517912004812957546158232703161144678502041874540920214901379685097628/74571034354786764975824764303193098070518746079777725398289130579334325145*y^27 + 10736747727733214083670378050250472730109399743785507320209819764068227853516973/74571034354786764975824764303193098070518746079777725398289130579334325145*y^26 + 6585534527547410697528611556401477149938655708298585786663499267457789137055984/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 - 18858393661046943185855700638289708845048703591333310720079010894324926586756051/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 - 186145794075061027298762671614092186627203832897512052471337654020615580970166401/74571034354786764975824764303193098070518746079777725398289130579334325145*y^23 + 449960674886175947852183829777956750565984918332787666965994681428615602755349323/74571034354786764975824764303193098070518746079777725398289130579334325145*y^22 + 725598127290331389884802202267783311016250854626438616795798778171536942015644268/74571034354786764975824764303193098070518746079777725398289130579334325145*y^21 - 1308384047046134448321876509033500247168446472078153406609728685130891718675901136/74571034354786764975824764303193098070518746079777725398289130579334325145*y^20 - 1915898383083781697840969795748322736255280849938603435342510592975614501865141326/74571034354786764975824764303193098070518746079777725398289130579334325145*y^19 + 2387050941148534340152506460695891771959744402696938328240337658758804101266607343/74571034354786764975824764303193098070518746079777725398289130579334325145*y^18 + 3407250441664102434743245623261119810339531331400871051205668553026757636169267667/74571034354786764975824764303193098070518746079777725398289130579334325145*y^17 - 2662457903875587537761620502567101985574462560911848980560195600694836593867869799/74571034354786764975824764303193098070518746079777725398289130579334325145*y^16 - 4127863880402703856917962823673706344930481532173353058653891942980355308295400056/74571034354786764975824764303193098070518746079777725398289130579334325145*y^15 + 1664410564662375245503020226625097839484033716394737909187446400370927637926759518/74571034354786764975824764303193098070518746079777725398289130579334325145*y^14 + 3382334941021004466022914021774940844078245600243675165385244187242414898368082742/74571034354786764975824764303193098070518746079777725398289130579334325145*y^13 - 396805827795145492077320012455077833882412670943243839746686181162139471068212951/74571034354786764975824764303193098070518746079777725398289130579334325145*y^12 - 1776110874219042735701349880162783531072037195332062659718799133186285707811673426/74571034354786764975824764303193098070518746079777725398289130579334325145*y^11 - 171268898834951904737234091574249854463678062819226495597496415600795603706517816/74571034354786764975824764303193098070518746079777725398289130579334325145*y^10 + 550546487573741779030893393901990275903740269217060855239060800522898629129893374/74571034354786764975824764303193098070518746079777725398289130579334325145*y^9 + 150829864616992341652181082266346823258364838055943278370289916507567514136342393/74571034354786764975824764303193098070518746079777725398289130579334325145*y^8 - 86824894537542101995326245628536223167385771163094235575757443098594752363245067/74571034354786764975824764303193098070518746079777725398289130579334325145*y^7 - 40786524966502569361243463908401122549132788781281108443144389746739317830322778/74571034354786764975824764303193098070518746079777725398289130579334325145*y^6 + 4618701018687125343006324968443706829670481184740855228982604641552313377866937/74571034354786764975824764303193098070518746079777725398289130579334325145*y^5 + 4705229310993551190627120353801171657684564689008047288011086867915116715576211/74571034354786764975824764303193098070518746079777725398289130579334325145*y^4 + 175193141917675269234243049926384360598611819340730221190778126515212497166016/74571034354786764975824764303193098070518746079777725398289130579334325145*y^3 - 244229498118480394347121774692900880038496046602075967422605257864631176584021/74571034354786764975824764303193098070518746079777725398289130579334325145*y^2 - 19366583424688521130534824173288764646757723055548787613057075793437351467631/74571034354786764975824764303193098070518746079777725398289130579334325145*y + 5700063451838935790619051246268739686460860494058438908895397995224978537992/74571034354786764975824764303193098070518746079777725398289130579334325145

-17101362569718834900182398153581176085204148447286137461751982863218143755336/372855171773933824879123821515965490352593730398888626991445652896671625725*y^31 - 73410034210190352215309323966351521346634262991235496438257623731452841516358/372855171773933824879123821515965490352593730398888626991445652896671625725*y^30 + 464220797804681421570391576340500777632347438289590241750697043576464715602378/74571034354786764975824764303193098070518746079777725398289130579334325145*y^29 - 993123338274417192257416534262609689533749851568690370967993697865889147231474/74571034354786764975824764303193098070518746079777725398289130579334325145*y^28 - 41362053131266232265120532971242300700166040622762516459145686963719863917040826/372855171773933824879123821515965490352593730398888626991445652896671625725*y^27 + 114803198271657233576189983013899496300203603914607137231188862817990649240429701/372855171773933824879123821515965490352593730398888626991445652896671625725*y^26 + 72365047102586780627198183008515003272302130385814410217045237878673321323088349/74571034354786764975824764303193098070518746079777725398289130579334325145*y^25 - 201187645408519087688775523037746223398773289313230234468744538720284990764202016/74571034354786764975824764303193098070518746079777725398289130579334325145*y^24 - 2053830252231133218500097130408375735229857094640135501430203739341879897671682362/372855171773933824879123821515965490352593730398888626991445652896671625725*y^23 + 4772483402596579554274062091583170536099084819812699656216912282724158983554418196/372855171773933824879123821515965490352593730398888626991445652896671625725*y^22 + 8002391684288855067943265270985333265704357466186059757438064009274242482636656676/372855171773933824879123821515965490352593730398888626991445652896671625725*y^21 - 13751652371299259041787461347607209559662892416153131973841612486985268548464666142/372855171773933824879123821515965490352593730398888626991445652896671625725*y^20 - 21032195195031616056355198986169488301983245645763643924196229239793298391952327702/372855171773933824879123821515965490352593730398888626991445652896671625725*y^19 + 24774279516544870294060171546424315272610179806037175627716278366014314000703792826/372855171773933824879123821515965490352593730398888626991445652896671625725*y^18 + 37096392820674752240344255719830896026145278200707604903459911350873298792197179654/372855171773933824879123821515965490352593730398888626991445652896671625725*y^17 - 27117152041964616414511334635522041160124544185504865184069598534754057275891572338/372855171773933824879123821515965490352593730398888626991445652896671625725*y^16 - 44420883661404073193214266771446422615113754203004635199295201577684375196418961077/372855171773933824879123821515965490352593730398888626991445652896671625725*y^15 + 16358044335819480980119200024826266210150794791162757297645717502935309856684948071/372855171773933824879123821515965490352593730398888626991445652896671625725*y^14 + 35887774427931853989695309540334059393792354391300199471770553313979168999926041924/372855171773933824879123821515965490352593730398888626991445652896671625725*y^13 - 3372464712971406916719916214795667846701277752166357080544680707487240750566790182/372855171773933824879123821515965490352593730398888626991445652896671625725*y^12 - 18556308001605559671527696509901711505619165115814547984788938065097251991100074487/372855171773933824879123821515965490352593730398888626991445652896671625725*y^11 - 2083762087098500556988723825983071541155242168833121519103599892957236158215260257/372855171773933824879123821515965490352593730398888626991445652896671625725*y^10 + 5658174943128209780907443769714601425427927975083840571907334749117917917236257138/372855171773933824879123821515965490352593730398888626991445652896671625725*y^9 + 1620933884241144832443583799320871043625368155592575341150297962343614354206926891/372855171773933824879123821515965490352593730398888626991445652896671625725*y^8 - 875969410218826601321504817157942863975957404949979044925017876547726499368340504/372855171773933824879123821515965490352593730398888626991445652896671625725*y^7 - 425231058722280807594853910473414801284527687064631317754881753139958527554688946/372855171773933824879123821515965490352593730398888626991445652896671625725*y^6 + 44689440896321264696445340395144995605553481720289755011167433885167974928303994/372855171773933824879123821515965490352593730398888626991445652896671625725*y^5 + 48393449068684939307093816742133481511072402022283483483179502180099663605649887/372855171773933824879123821515965490352593730398888626991445652896671625725*y^4 + 1958799405828651965624853426117761530888118852786323325948748661422644806479212/372855171773933824879123821515965490352593730398888626991445652896671625725*y^3 - 2498645148464778144729253906467069728211358522657783265935636867379117453515347/372855171773933824879123821515965490352593730398888626991445652896671625725*y^2 - 201770711263046529120520488378563605684798247685554730385604203541520207107687/372855171773933824879123821515965490352593730398888626991445652896671625725*y + 57637292558290427468975967575597138369438144340925454897516521874825877249864/372855171773933824879123821515965490352593730398888626991445652896671625725

309660793796351044911344064188906090942385550186215350344531895704792440716/14914206870957352995164952860638619614103749215955545079657826115866865029*y^31 + 1319770453882719465744287424619763755957785655694924618987103830077283374150/14914206870957352995164952860638619614103749215955545079657826115866865029*y^30 - 42074175789586460129975112334663893957950346895521783165694106214948798160372/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 + 91182331628108363519979685693025204913739993504384518525893961884133228663501/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 + 746779176330966682247378949333094064673681821834745470275521762432624752118313/14914206870957352995164952860638619614103749215955545079657826115866865029*y^27 - 2102770203869488434334922712745310316420704232756177825278341674787404126031292/14914206870957352995164952860638619614103749215955545079657826115866865029*y^26 - 6498668908940760131435894454657796922145481678586394319670282064440202236464004/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 + 18440120763515578138861435343243737144916940146711236908189350745185531316269359/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 + 36728886876089568646485894187446817151542628173157093053181643728080150291412144/14914206870957352995164952860638619614103749215955545079657826115866865029*y^23 - 87764920433730049193007143992784395869709329847853144419567100038194812517296578/14914206870957352995164952860638619614103749215955545079657826115866865029*y^22 - 142822517861414342238534283913457918282877373455401658397737836638287294629098402/14914206870957352995164952860638619614103749215955545079657826115866865029*y^21 + 254370051567701225132293349656226144614378820664013906833796460715304707726301025/14914206870957352995164952860638619614103749215955545079657826115866865029*y^20 + 375398990440302746045611955599206100420575516509375740328865933991934611022845850/14914206870957352995164952860638619614103749215955545079657826115866865029*y^19 - 462659198315058716975265638791378529612738443385519949610101631656893946032876923/14914206870957352995164952860638619614103749215955545079657826115866865029*y^18 - 663496007640315527833738877013923329428022174585645415093401289944982783911935465/14914206870957352995164952860638619614103749215955545079657826115866865029*y^17 + 515279866628242032547412789819103306712806039180687663519115590131473841917940071/14914206870957352995164952860638619614103749215955545079657826115866865029*y^16 + 798419800595776894549675719163177657472239938648054740503860536514810612445570760/14914206870957352995164952860638619614103749215955545079657826115866865029*y^15 - 323857291008093792965397848851108326900120792375930624383447147068151428111163873/14914206870957352995164952860638619614103749215955545079657826115866865029*y^14 - 650765560483827452757765130134118818999883258426427397761096973897164761682916653/14914206870957352995164952860638619614103749215955545079657826115866865029*y^13 + 81559800061827708667388847231315902124749377650960131450451837606402874218998210/14914206870957352995164952860638619614103749215955545079657826115866865029*y^12 + 341410472121755705940267588783699156627264904494829096793893671144504878897953078/14914206870957352995164952860638619614103749215955545079657826115866865029*y^11 + 28586424484854577653868981312262359124767058578414505258005811202062687638308081/14914206870957352995164952860638619614103749215955545079657826115866865029*y^10 - 106898918756374954697718743470572595999082804060915607062507584419589437156936261/14914206870957352995164952860638619614103749215955545079657826115866865029*y^9 - 27371003914843800162963990161268209598295676095004798517129982521788601920129403/14914206870957352995164952860638619614103749215955545079657826115866865029*y^8 + 17556275329160831379220906509699294312486450224916191035147904471494172478775121/14914206870957352995164952860638619614103749215955545079657826115866865029*y^7 + 7689701128819760795506247840457445022960098175833271972865326823274702180124957/14914206870957352995164952860638619614103749215955545079657826115866865029*y^6 - 1099004908859333575904028323355462431091886435214439228122957108447905217225738/14914206870957352995164952860638619614103749215955545079657826115866865029*y^5 - 936850751230911245893075238828949913959099936985244394857566279963147559310621/14914206870957352995164952860638619614103749215955545079657826115866865029*y^4 - 19674353317994218529546411931298005559099305870736591352691318340853768231123/14914206870957352995164952860638619614103749215955545079657826115866865029*y^3 + 51584117385561067637195825716039255127871622731060917412592820148042367771217/14914206870957352995164952860638619614103749215955545079657826115866865029*y^2 + 3615081108189486061177096738676162867728797094001834370850181714986087308556/14914206870957352995164952860638619614103749215955545079657826115866865029*y - 1206342465482435713986463027426014593187739646742088413729438869431188358202/14914206870957352995164952860638619614103749215955545079657826115866865029

309660793796351044911344064188906090942385550186215350344531895704792440716/14914206870957352995164952860638619614103749215955545079657826115866865029*y^31 + 1319770453882719465744287424619763755957785655694924618987103830077283374150/14914206870957352995164952860638619614103749215955545079657826115866865029*y^30 - 42074175789586460129975112334663893957950346895521783165694106214948798160372/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 + 91182331628108363519979685693025204913739993504384518525893961884133228663501/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 + 746779176330966682247378949333094064673681821834745470275521762432624752118313/14914206870957352995164952860638619614103749215955545079657826115866865029*y^27 - 2102770203869488434334922712745310316420704232756177825278341674787404126031292/14914206870957352995164952860638619614103749215955545079657826115866865029*y^26 - 6498668908940760131435894454657796922145481678586394319670282064440202236464004/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 + 18440120763515578138861435343243737144916940146711236908189350745185531316269359/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 + 36728886876089568646485894187446817151542628173157093053181643728080150291412144/14914206870957352995164952860638619614103749215955545079657826115866865029*y^23 - 87764920433730049193007143992784395869709329847853144419567100038194812517296578/14914206870957352995164952860638619614103749215955545079657826115866865029*y^22 - 142822517861414342238534283913457918282877373455401658397737836638287294629098402/14914206870957352995164952860638619614103749215955545079657826115866865029*y^21 + 254370051567701225132293349656226144614378820664013906833796460715304707726301025/14914206870957352995164952860638619614103749215955545079657826115866865029*y^20 + 375398990440302746045611955599206100420575516509375740328865933991934611022845850/14914206870957352995164952860638619614103749215955545079657826115866865029*y^19 - 462659198315058716975265638791378529612738443385519949610101631656893946032876923/14914206870957352995164952860638619614103749215955545079657826115866865029*y^18 - 663496007640315527833738877013923329428022174585645415093401289944982783911935465/14914206870957352995164952860638619614103749215955545079657826115866865029*y^17 + 515279866628242032547412789819103306712806039180687663519115590131473841917940071/14914206870957352995164952860638619614103749215955545079657826115866865029*y^16 + 798419800595776894549675719163177657472239938648054740503860536514810612445570760/14914206870957352995164952860638619614103749215955545079657826115866865029*y^15 - 323857291008093792965397848851108326900120792375930624383447147068151428111163873/14914206870957352995164952860638619614103749215955545079657826115866865029*y^14 - 650765560483827452757765130134118818999883258426427397761096973897164761682916653/14914206870957352995164952860638619614103749215955545079657826115866865029*y^13 + 81559800061827708667388847231315902124749377650960131450451837606402874218998210/14914206870957352995164952860638619614103749215955545079657826115866865029*y^12 + 341410472121755705940267588783699156627264904494829096793893671144504878897953078/14914206870957352995164952860638619614103749215955545079657826115866865029*y^11 + 28586424484854577653868981312262359124767058578414505258005811202062687638308081/14914206870957352995164952860638619614103749215955545079657826115866865029*y^10 - 106898918756374954697718743470572595999082804060915607062507584419589437156936261/14914206870957352995164952860638619614103749215955545079657826115866865029*y^9 - 27371003914843800162963990161268209598295676095004798517129982521788601920129403/14914206870957352995164952860638619614103749215955545079657826115866865029*y^8 + 17556275329160831379220906509699294312486450224916191035147904471494172478775121/14914206870957352995164952860638619614103749215955545079657826115866865029*y^7 + 7689701128819760795506247840457445022960098175833271972865326823274702180124957/14914206870957352995164952860638619614103749215955545079657826115866865029*y^6 - 1099004908859333575904028323355462431091886435214439228122957108447905217225738/14914206870957352995164952860638619614103749215955545079657826115866865029*y^5 - 936850751230911245893075238828949913959099936985244394857566279963147559310621/14914206870957352995164952860638619614103749215955545079657826115866865029*y^4 - 19674353317994218529546411931298005559099305870736591352691318340853768231123/14914206870957352995164952860638619614103749215955545079657826115866865029*y^3 + 51584117385561067637195825716039255127871622731060917412592820148042367771217/14914206870957352995164952860638619614103749215955545079657826115866865029*y^2 + 3615081108189486061177096738676162867728797094001834370850181714986087308556/14914206870957352995164952860638619614103749215955545079657826115866865029*y - 1206342465482435713986463027426014593187739646742088413729438869431188358202/14914206870957352995164952860638619614103749215955545079657826115866865029

3984543965371462731966069172033432869642212051270651662138673945162094439269/14914206870957352995164952860638619614103749215955545079657826115866865029*y^31 + 17086572427361958328069354677902719018381257591622519910473174867048777328811/14914206870957352995164952860638619614103749215955545079657826115866865029*y^30 - 540968370852478063208525063651492098616009583776399631471105261560158973363758/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 + 1158941935963739712860474890180101334726594094740156793696251186019362715329028/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 + 9643331060933055167827492309997110163781574962683012400881023178715568851804142/14914206870957352995164952860638619614103749215955545079657826115866865029*y^27 - 26809107939344358068787274791674486113065095240578378748061763389978755943558182/14914206870957352995164952860638619614103749215955545079657826115866865029*y^26 - 84397706826084966487023277392265974765981527906332250633449749587850205887831007/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 + 235180829043951537171388066108709502242309438939802393205394327166470032178403953/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 + 479476201255716407648548411236201875220430811193269853013490112769244545193650199/14914206870957352995164952860638619614103749215955545079657826115866865029*y^23 - 1117628622107356007223639387342938704821496600095063347704661269199857224258821063/14914206870957352995164952860638619614103749215955545079657826115866865029*y^22 - 1871207418592278034338606759377311619933040084014128702107751691187212809534743688/14914206870957352995164952860638619614103749215955545079657826115866865029*y^21 + 3226959681119717210565295339182707282968008087841250377610741070076093441076117198/14914206870957352995164952860638619614103749215955545079657826115866865029*y^20 + 4930277946111107148565671079317802210693716454884582577566606177212997772607446875/14914206870957352995164952860638619614103749215955545079657826115866865029*y^19 - 5826998265805344592690804669277886540002722347788971453494210726923374769877472333/14914206870957352995164952860638619614103749215955545079657826115866865029*y^18 - 8724078134108592425765277587472039734455426287228767232020315732252803591272381183/14914206870957352995164952860638619614103749215955545079657826115866865029*y^17 + 6394404836662763346346870069640640213907885520189583995075577065611132900615143120/14914206870957352995164952860638619614103749215955545079657826115866865029*y^16 + 10483834566083357580457428324447108475970146709610337863309312147483962117925761865/14914206870957352995164952860638619614103749215955545079657826115866865029*y^15 - 3865911263005322115909668610637622852454227143084220024124577431077156137350849499/14914206870957352995164952860638619614103749215955545079657826115866865029*y^14 - 8499788485143665099955605209029108011193705050416470287410397080727204230817713766/14914206870957352995164952860638619614103749215955545079657826115866865029*y^13 + 793269027481088660730898834364346732224282657277069360379030160967422090289068498/14914206870957352995164952860638619614103749215955545079657826115866865029*y^12 + 4410585117050785337428603800337569705916268713525191638903384703513628335460978070/14914206870957352995164952860638619614103749215955545079657826115866865029*y^11 + 501384529783942016481292701317475168665446267652569880393899067923122165993087888/14914206870957352995164952860638619614103749215955545079657826115866865029*y^10 - 1349123114206072628734733952883581388325296654455865970796025841504357206080734455/14914206870957352995164952860638619614103749215955545079657826115866865029*y^9 - 389025345620664201367629289675667571606302259769886271203465744131882178741556048/14914206870957352995164952860638619614103749215955545079657826115866865029*y^8 + 209221465428723899585300726855795181137542888373677147104142429603229125349573623/14914206870957352995164952860638619614103749215955545079657826115866865029*y^7 + 102215664655201588274617223930563475690346583213970009861454735573429468407261034/14914206870957352995164952860638619614103749215955545079657826115866865029*y^6 - 10627217150462986874855259542882522460276388001364718995227337016075389524750942/14914206870957352995164952860638619614103749215955545079657826115866865029*y^5 - 11659517026601346579305065443516305863932921454060510661439988290706513076190103/14914206870957352995164952860638619614103749215955545079657826115866865029*y^4 - 482819476177668013329555964605030133816199226506265225420185470929975056359810/14914206870957352995164952860638619614103749215955545079657826115866865029*y^3 + 603779040789872038277714741055393576193802674208573862582961506234035683399771/14914206870957352995164952860638619614103749215955545079657826115866865029*y^2 + 49328911283395820402296729219027337677428743731039929579364484027700011914685/14914206870957352995164952860638619614103749215955545079657826115866865029*y - 13988279973304192063789921871408352286529625921831777491496740608236492958400/14914206870957352995164952860638619614103749215955545079657826115866865029

3905780333601436586054067892851123259008468794414215648986316775496302718882/14914206870957352995164952860638619614103749215955545079657826115866865029*y^31 + 16772717278625028091854358620041577358601149632331211252459637955800425321904/14914206870957352995164952860638619614103749215955545079657826115866865029*y^30 - 530155054919136961928880949707270554672369518053605692578492253229978304543289/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 + 1132866186707648169065879383603593083637032125262888164888416361520953086546535/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 + 9457325988432044981447019052423521179970777110473839388080293868308199100224009/14914206870957352995164952860638619614103749215955545079657826115866865029*y^27 - 26216770800381705963858539212259774411645889186314532314604602778453805224816470/14914206870957352995164952860638619614103749215955545079657826115866865029*y^26 - 82847749030376327398601838408608253336012215333377665688977393161574084269757562/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 + 229919236295913838007822674850735712036992741284608394612526660314641939714015821/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 + 471028123794961615808592330774722854524166399830946690490191845788006755416788205/14914206870957352995164952860638619614103749215955545079657826115866865029*y^23 - 1091741644717672134826947953430100073706872029893741920413998755190486521664917806/14914206870957352995164952860638619614103749215955545079657826115866865029*y^22 - 1838726623788254928485579158491554201453557633045431652578111202503075385284703036/14914206870957352995164952860638619614103749215955545079657826115866865029*y^21 + 3147746270685641301480877084204217385971191970637180681271627621250280267932413326/14914206870957352995164952860638619614103749215955545079657826115866865029*y^20 + 4843656038109067486687067324388333778305383902996760172685691338283049774437009522/14914206870957352995164952860638619614103749215955545079657826115866865029*y^19 - 5670840532758408252996299249726081191860482745005828343702647451540503429686470188/14914206870957352995164952860638619614103749215955545079657826115866865029*y^18 - 8564725008974945981827701400980502325828152545049161646378655450621485627269974303/14914206870957352995164952860638619614103749215955545079657826115866865029*y^17 + 6196965547726871044692309261469443868004799217686535033855984940515045546938982526/14914206870957352995164952860638619614103749215955545079657826115866865029*y^16 + 10278089332126855435657913918613752395262608865735525973461200374245409344846430048/14914206870957352995164952860638619614103749215955545079657826115866865029*y^15 - 3709285249393020228518474146112319970445670116571392510182499048972713927479071235/14914206870957352995164952860638619614103749215955545079657826115866865029*y^14 - 8313744432578222468831687632517751616766489131254059510561061800411126606102292275/14914206870957352995164952860638619614103749215955545079657826115866865029*y^13 + 719995962456949419813002404680590297658769028650723391770915574777553788015017922/14914206870957352995164952860638619614103749215955545079657826115866865029*y^12 + 4297946611022751339123220917956654703034732788452591470650705427582335739783133996/14914206870957352995164952860638619614103749215955545079657826115866865029*y^11 + 515673156138849827482127503895447835192257412030255910907628072888394607900474745/14914206870957352995164952860638619614103749215955545079657826115866865029*y^10 - 1305864550784171967267424276815218890926370555138037750135739631052212100642261606/14914206870957352995164952860638619614103749215955545079657826115866865029*y^9 - 385843590593340485390643976176379974182049087945478751341442604756972338457668529/14914206870957352995164952860638619614103749215955545079657826115866865029*y^8 + 199458306769016672022285401775834203815068471971799336517660836028537084165639269/14914206870957352995164952860638619614103749215955545079657826115866865029*y^7 + 99913339232222653878599712713575654800095728853258307508429048447402942459338782/14914206870957352995164952860638619614103749215955545079657826115866865029*y^6 - 9510631658321989670867351742075926253537677802076242749702286692361038304682319/14914206870957352995164952860638619614103749215955545079657826115866865029*y^5 - 11211807405457128328309550673787773379611727031182424388027122631275701002324782/14914206870957352995164952860638619614103749215955545079657826115866865029*y^4 - 525299094536719317495485661030386845328185157251252309032488321304717317113659/14914206870957352995164952860638619614103749215955545079657826115866865029*y^3 + 569627722865220603917626783264761480980396846360412379297042700025839871936537/14914206870957352995164952860638619614103749215955545079657826115866865029*y^2 + 48974962719092173721548071484629816527398919553739200001384829491319158130647/14914206870957352995164952860638619614103749215955545079657826115866865029*y - 12881154104825566264242319871417652406652615633416325950471313008482939549625/14914206870957352995164952860638619614103749215955545079657826115866865029


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

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

# nu Gluing Vector
{4, 3, 2, 6, 2, 2, 1, 2}

# f Combinatorial flattening
{-12, 25, 15, 20, -21, -9, -1, 20}

# f' Combinatorial flattening
{0, 0, 14, 0, 12, 0, 0, 0}

# 1 Loop Invariant
-6262690697162096140979370804103571960469359723646764454804541492318192926605/14914206870957352995164952860638619614103749215955545079657826115866865029*y^31 - 27183438772828885057323232927689709676240952527035310775739138895839328505472/14914206870957352995164952860638619614103749215955545079657826115866865029*y^30 + 849211934389624659805937405714379337009817624850359128892120537916482213777821/14914206870957352995164952860638619614103749215955545079657826115866865029*y^29 - 1775478865678039402479311188633014410280810626016915669784118869723879455172812/14914206870957352995164952860638619614103749215955545079657826115866865029*y^28 - 15299462233512561105557559828601116886714773695785711369382694930371111646262303/14914206870957352995164952860638619614103749215955545079657826115866865029*y^27 + 41436121273692275201744384471393020635629015617792625733709586623783448589886960/14914206870957352995164952860638619614103749215955545079657826115866865029*y^26 + 135708547796733663954576442458015037239436705033904751230958246596916073748579325/14914206870957352995164952860638619614103749215955545079657826115866865029*y^25 - 364834443092633227625283325502604513314406945435296383792762002069686142542448362/14914206870957352995164952860638619614103749215955545079657826115866865029*y^24 - 780503559052867161381645557807458599499576052621434245616279029208755882885537122/14914206870957352995164952860638619614103749215955545079657826115866865029*y^23 + 1735299175874158827262594575258506373173805296814331575161974361599676278671109208/14914206870957352995164952860638619614103749215955545079657826115866865029*y^22 + 3075777513844634135306820988938001852329409274254447514475974695988537057283159234/14914206870957352995164952860638619614103749215955545079657826115866865029*y^21 - 4999159576873011292325621640635126045740970531895436704437056780808242596348212576/14914206870957352995164952860638619614103749215955545079657826115866865029*y^20 - 8176438873367817465983652278376773172877744384312046635130618488682678948856056900/14914206870957352995164952860638619614103749215955545079657826115866865029*y^19 + 8967526927999541445876619017374490385083780729973122937161558948524683069566242493/14914206870957352995164952860638619614103749215955545079657826115866865029*y^18 + 14590635522253175013722885939001150505018810320639809244407964393265451192320366036/14914206870957352995164952860638619614103749215955545079657826115866865029*y^17 - 9675089109043865173347987806942010198861909482727368279314255632769650175632155577/14914206870957352995164952860638619614103749215955545079657826115866865029*y^16 - 17640563110859599795444121793560668149462476483524858549581011400263009937834876695/14914206870957352995164952860638619614103749215955545079657826115866865029*y^15 + 5525202002180692353507973771595193372130454924191536316789889015821628295014357497/14914206870957352995164952860638619614103749215955545079657826115866865029*y^14 + 14338716959740030083217640815587951476686677536792849640708228058742927437451121049/14914206870957352995164952860638619614103749215955545079657826115866865029*y^13 - 680722596708972777245170523441209557070708206326259638079422632241151253365301296/14914206870957352995164952860638619614103749215955545079657826115866865029*y^12 - 7441558489542943700722911328235387912753095070248623863585640264888409314859630332/14914206870957352995164952860638619614103749215955545079657826115866865029*y^11 - 1150104437595297869412858542038311935166752146105345908977542987213617747702457876/14914206870957352995164952860638619614103749215955545079657826115866865029*y^10 + 2260410821710064786571988295486479303778410295296191280918811501029000792927190195/14914206870957352995164952860638619614103749215955545079657826115866865029*y^9 + 745845671069210305609977916571213791857890004538888005983002252715636057116728327/14914206870957352995164952860638619614103749215955545079657826115866865029*y^8 - 339146527777756391240279967238547117984281628397998770594809987838642337473084846/14914206870957352995164952860638619614103749215955545079657826115866865029*y^7 - 187234975482621713465061946931562453989259720402915353313138759343860325371860354/14914206870957352995164952860638619614103749215955545079657826115866865029*y^6 + 14130296102753504805299687399626776133461749807714589072610778316414841313341159/14914206870957352995164952860638619614103749215955545079657826115866865029*y^5 + 20891560083013663808621398132488477673387486910863313942193487004771474769657990/14914206870957352995164952860638619614103749215955545079657826115866865029*y^4 + 1184619899508755108510710045572294402997096586575828297638122255489293506620375/14914206870957352995164952860638619614103749215955545079657826115866865029*y^3 - 1071994864050257792370278067387338415460989168852390694559576783147305144442534/14914206870957352995164952860638619614103749215955545079657826115866865029*y^2 - 98411748249775378231778693707712000094438383482161467461812687649363356919808/14914206870957352995164952860638619614103749215955545079657826115866865029*y + 26316104658468101363705239139409807392312814431789936833359964675839955307638/14914206870957352995164952860638619614103749215955545079657826115866865029

# 2 Loop Invariant
8229999692232711130607756116633627144211814759077423345128528018204900584938614876580593890120472125798493938594987583957720323953866786898068655259530725073540929048738822783969496952809/2157151939031077714717531070357936493817698173736007256136820376145048744555213138412975754377839348722141729546504608795291483330844145516957695914774994247924486346437393150012669353722*y^31 + 212016799129093005088471700464249697392366319369937738226828667342640161319854865632200684658095950847778917910937424014519863738968343822795150880461251048902395785455665837978881959849667/12942911634186466288305186422147618962906189042416043536820922256870292467331278830477854526267036092332850377279027652771748899985064873101746175488649965487546918078624358900076016122332*y^30 - 26811596511963009189877069123068935683024319563937951018018597123738686484068427101191567475788611760358110660460058020299838251430637583419100469374097561157630251791916160746926091694120735/51771646536745865153220745688590475851624756169664174147283689027481169869325115321911418105068144369331401509116110611086995599940259492406984701954599861950187672314497435600304064489328*y^29 + 2387861944170505553245454242084337867137245434590958175857014007533744762053363435819816495799797490604307058665072057826940755633793022061469004683520605300889002886461482894507166452901063/2157151939031077714717531070357936493817698173736007256136820376145048744555213138412975754377839348722141729546504608795291483330844145516957695914774994247924486346437393150012669353722*y^28 + 159424973777316941114147129653584455578410417342364312833960280937963223463520889140090778541004807201761928293964781650678319812901397746743057130031810211007839597165803896874563903457082277/17257215512248621717740248562863491950541585389888058049094563009160389956441705107303806035022714789777133836372036870362331866646753164135661567318199953983395890771499145200101354829776*y^27 - 1326239400642492958090314016757231505435284500293717856712871913192710819230767120803975101272502384408787379289549319624418371572231954034056864937129378663265004053568240293663804917238524361/51771646536745865153220745688590475851624756169664174147283689027481169869325115321911418105068144369331401509116110611086995599940259492406984701954599861950187672314497435600304064489328*y^26 - 1396570173986485741417694784342007978882356888859887290570380136033871355052511358796763978120744486184575289363735821261925728737053189979789057746271509814472890723654721023763784222139692187/17257215512248621717740248562863491950541585389888058049094563009160389956441705107303806035022714789777133836372036870362331866646753164135661567318199953983395890771499145200101354829776*y^25 + 969348079557634123241610343865776983337366012551977167462495088461667371627882004144899315717065328306790672660577911480785623493254511260649559782541187232576376889831892996232864497536542029/4314303878062155429435062140715872987635396347472014512273640752290097489110426276825951508755678697444283459093009217590582966661688291033915391829549988495848972692874786300025338707444*y^24 + 2977708328057724973810993781383698164494594270152765964197698053477792938395155814050637556856556974219121304936685307058663624112977816467027277917629743638779774311641214835113970434912772643/6471455817093233144152593211073809481453094521208021768410461128435146233665639415238927263133518046166425188639513826385874449992532436550873087744324982743773459039312179450038008061166*y^23 - 55243627162246757826824456759705490533913124364446911435291424615958141280916163709583809074215864882799383263897319019956477401969668598160729404745981474221730855503178277162121573030067590257/51771646536745865153220745688590475851624756169664174147283689027481169869325115321911418105068144369331401509116110611086995599940259492406984701954599861950187672314497435600304064489328*y^22 - 93006966097541670599390181789700122522616111870406169444919774282719726615703615658149920014449989422474286527356609224149505095785364685475964934301346175501964989017867445578420619527005189379/51771646536745865153220745688590475851624756169664174147283689027481169869325115321911418105068144369331401509116110611086995599940259492406984701954599861950187672314497435600304064489328*y^21 + 79659793043660697641914702212325899264701921775277705357123190152233551299679914046103151967839278997948898915245017103476749053519328210518672890793367608752411861144993202846703431041636307807/25885823268372932576610372844295237925812378084832087073641844513740584934662557660955709052534072184665700754558055305543497799970129746203492350977299930975093836157248717800152032244664*y^20 + 61269681235139511923113444389336583438489007782816795119880501137327514275796309247033704607596634729174781566975208622190589356966969223266564710257039844363048155970828403673568602315412030183/12942911634186466288305186422147618962906189042416043536820922256870292467331278830477854526267036092332850377279027652771748899985064873101746175488649965487546918078624358900076016122332*y^19 - 17944654243121002861776302461077413535038851045932647567394723469020738068877484037183102677768135136489507472913982547088949278787068986185200391955239357639822753263533954965531538442721239111/3235727908546616572076296605536904740726547260604010884205230564217573116832819707619463631566759023083212594319756913192937224996266218275436543872162491371886729519656089725019004030583*y^18 - 108390039851270922320947112623623729196769802479723355976916621229828939661711019625346520253949530775262653289016600256809380870501499253779434354940729060354877107478793838427230315207813750887/12942911634186466288305186422147618962906189042416043536820922256870292467331278830477854526267036092332850377279027652771748899985064873101746175488649965487546918078624358900076016122332*y^17 + 52314333394426387713521934877322268484708884189442241618839631088635050241854915839905377460608402426791864455533507224968355832750935612400937553379638987482256613430521281798760867622704524571/8628607756124310858870124281431745975270792694944029024547281504580194978220852553651903017511357394888566918186018435181165933323376582067830783659099976991697945385749572600050677414888*y^16 + 173543202289359477974682843391182868442779004577982677343746395409463979919432370756527775909310400551215350471646818534560893666579305787751780353251072688105441975626495590671196406130458587719/17257215512248621717740248562863491950541585389888058049094563009160389956441705107303806035022714789777133836372036870362331866646753164135661567318199953983395890771499145200101354829776*y^15 - 11749707935522400292243260265692594908282687970839949824880778076471074036168855694510277671003754602102928755286597616766015914353334257141905724187183008237256785967317867672853156724422749184/3235727908546616572076296605536904740726547260604010884205230564217573116832819707619463631566759023083212594319756913192937224996266218275436543872162491371886729519656089725019004030583*y^14 - 105371142552713817266898375160001314158305819668518153515651181594118879611271793185075676475207546131283548784597069231184883295113963102855729492551719485985571164201065018253933713464564029749/12942911634186466288305186422147618962906189042416043536820922256870292467331278830477854526267036092332850377279027652771748899985064873101746175488649965487546918078624358900076016122332*y^13 + 18261667928700756911013019923557980318521569118299294629543346288765688601830878096219887437349495436169054739764770951284118926415251983089526702004175510306978383612333459200468360685520847551/25885823268372932576610372844295237925812378084832087073641844513740584934662557660955709052534072184665700754558055305543497799970129746203492350977299930975093836157248717800152032244664*y^12 + 109079712006555195487485905975220564525908234998700398264286179700275596230159640824063618239671737972722782565252040672547237601385686847240440054317737332251325495013615283365985094033747753889/25885823268372932576610372844295237925812378084832087073641844513740584934662557660955709052534072184665700754558055305543497799970129746203492350977299930975093836157248717800152032244664*y^11 + 3272790516545271422032494599493689025204217431709785189330450406963676048580734982433238609497525252094650856758110463856862580923974632657331448323644399817040809778616900009612578605890986499/6471455817093233144152593211073809481453094521208021768410461128435146233665639415238927263133518046166425188639513826385874449992532436550873087744324982743773459039312179450038008061166*y^10 - 16605525720403703632755543554270627335983492508927597744667520257355720322123458144555817125381013334132000822669932072889713489086817356620886612177176590854069578297366659626880675744301306827/12942911634186466288305186422147618962906189042416043536820922256870292467331278830477854526267036092332850377279027652771748899985064873101746175488649965487546918078624358900076016122332*y^9 - 3270143206682340858807653423088517458010550485382005514549325916342024770160615240549412210503334349411239155083710183113765822953994854426330265798263494656127010873904772633660388585410932277/8628607756124310858870124281431745975270792694944029024547281504580194978220852553651903017511357394888566918186018435181165933323376582067830783659099976991697945385749572600050677414888*y^8 + 1273918098818186308517013118770671026556759606451722969654107496446926918688411006057820585915867516038041806638542284426959795679797605356111426924075653609023322520319617432573015494508902679/6471455817093233144152593211073809481453094521208021768410461128435146233665639415238927263133518046166425188639513826385874449992532436550873087744324982743773459039312179450038008061166*y^7 + 1698036565871338498270862981715113124041957049972219109939078718843065117800138897153836797659992681403460855040010124079935761554835296413850515655562131379069207467785125956792851969667503475/17257215512248621717740248562863491950541585389888058049094563009160389956441705107303806035022714789777133836372036870362331866646753164135661567318199953983395890771499145200101354829776*y^6 - 247556273141111290503442293866937977152445833646001666303423157824707459213162764020729799558705598813391219362985352644582783124481532862552802418553733945213654838869860870325227066103123635/25885823268372932576610372844295237925812378084832087073641844513740584934662557660955709052534072184665700754558055305543497799970129746203492350977299930975093836157248717800152032244664*y^5 - 191552440535824979206619152428615281116860549348161159818242146124929235445503685627178781827818433095523886512188486177817195833666892118623422571464166403360768105063084914518414509487752959/17257215512248621717740248562863491950541585389888058049094563009160389956441705107303806035022714789777133836372036870362331866646753164135661567318199953983395890771499145200101354829776*y^4 - 25878843838052264086453600129487695294588715772028657853117461704787824018730660598069206886509477918336860294167980419704793475736400181984194787366252521908601087051796497906571348043321261/51771646536745865153220745688590475851624756169664174147283689027481169869325115321911418105068144369331401509116110611086995599940259492406984701954599861950187672314497435600304064489328*y^3 + 29495821965581492945608809950115546600468880606288717318273979024957783841325648827721935554396224593401587410843429386540963453337941533228277128872709007936518506322679762972446685157973289/51771646536745865153220745688590475851624756169664174147283689027481169869325115321911418105068144369331401509116110611086995599940259492406984701954599861950187672314497435600304064489328*y^2 + 1231034404797426863988051193268576428312814858427332841839767003808309484146234947127914205053815423253381362990235362387076205617774625318049528243173903532618459757184889532608929737677697/25885823268372932576610372844295237925812378084832087073641844513740584934662557660955709052534072184665700754558055305543497799970129746203492350977299930975093836157248717800152032244664*y - 26782338190558016851137121113113802635474205168637945984647332530026450206227895239811331752419202222880687185210662768090847882078944857399743578537080970059670938558693717470297672020351/6471455817093233144152593211073809481453094521208021768410461128435146233665639415238927263133518046166425188639513826385874449992532436550873087744324982743773459039312179450038008061166

# 3 Loop Invariant
-133480928135174019206625265171218416268382594668552465591554569627391847918509861869675444736695905065151777710955862994149802501529827390765157147716985955565208370158404012814494079785963474308091633449354908316018172130750024755533477367341/1160208438874046229406136025955352547746626165821525476837184400941355481059061378156363572923566318916155712732310965093467394437431560865275500436253786756528232745900459591951419656302111861963062187246542741343689424706043849015942464208068*y^31 - 1152421813468837423514035090945057536093209506219151315245629979883332031274709177829494956215357775060883837972057325148892161556809850225656491860594850264071371107418286319875044800688734532123428261213749216382946049108495402176352244199677/2320416877748092458812272051910705095493252331643050953674368801882710962118122756312727145847132637832311425464621930186934788874863121730551000872507573513056465491800919183902839312604223723926124374493085482687378849412087698031884928416136*y^30 + 144836913196815603910290465551824008900625816391028711911362917572913995870992999706657346620781084327451279032424940508236984831862712576407593992205143522459175893312311074662147321501353678785728707465538214457745820203363762637928875232907323/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y^29 - 76625973707989160844609947478285033088848814324679437306847588262467886227151381133506419426953341854359376892683845715197996540381225709208201994604881408427597083415460728953660525902844410091476065114853724309739996854688097238804515793761493/2320416877748092458812272051910705095493252331643050953674368801882710962118122756312727145847132637832311425464621930186934788874863121730551000872507573513056465491800919183902839312604223723926124374493085482687378849412087698031884928416136*y^28 - 647981973463853868376805408902971490324813285866007738501900277646175817241313268662522043053710948793221844540935378472847757088780279627498167599258156171816307160518159003536397410964851618262907801658838710112074160027847820637984699223536477/2320416877748092458812272051910705095493252331643050953674368801882710962118122756312727145847132637832311425464621930186934788874863121730551000872507573513056465491800919183902839312604223723926124374493085482687378849412087698031884928416136*y^27 + 14218787142077583003120337838993279997393914928493033794185947610035676406750052845853011946047337489799497223046814731274304739791886095645527283977129992814857328841968102512447038119975778302468145276156564495333055930440615372098938398466629263/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^26 + 45593191132389404369424730376434316141307273928450151608741282560661923242762706187521163994021977198574101853068910071660918321247612815015044761275396569781723346263864700038183633429843807465859153959765880914542996704191687309213085186107034207/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^25 - 62340756066981399396617316571709858193755185610185857461872644924992792074373674686897464753140998774127295294383004300106090786077228668598969831740258827796805924660554568709541381234067015874106199174494911305690519559507759181201977214070667287/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y^24 - 130026122920960967882951349139565086946308430941365594198063984451608828853811628104099371074302649179165580641324063395761720719474170887273926948822301140992890531606385591271733836196695649056136969610240980676069261186151784278737475503854081903/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y^23 + 295514421464751590489255585272307613330625883660035491728964387233567842835778238918003172801813687454978228327273026960905586367662554778649257816827139143038091747987817384491967644978767702734319468293511247783057622007607126269383580240919432025/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y^22 + 1016664254665900366331991377826279895725071967320854323526218971323694224873080406007366537273048199121595363531017831870215619039537729670890983316840252406039038620416589056554341569569705878535872854173873210409308149248550063666385271310323191329/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^21 - 1698471310418475926141260336768728155674522769584277171644557408093279456317400866960940088440586873120702515748416996793628870876953526427392098892637538225021111096316112392593729640633374251301363951999091935534817848535087876754160386459484506119/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^20 - 2678460523803534385348744476962612750753541260486540340455419745072549707621065143830397953064250507187823037016918798136384422702508788678503550865150468417524846667710661465802062251603385441513408536916280535034611527354852249740947762472416390649/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^19 + 3043836236359791228510172397668568393075874997052859239148321986501685836088875207257456174346483499674960028633836743970736973227980523271058915145388531056663151165091980530164014980230086560584114640300336472006820663065932602960625094203649967625/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^18 + 4731138125176070450648786030605001174341632850888621772904990110639701892140031425531630008822353139182826731880578095763552871441519119593144276916000233773394243629157599662098932195758226005123572959257934163805993279139512035653554775967787920301/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^17 - 3295624836716571651303303841123150472298527549820064390688671946303255684970129429312496596275009601377078443415635729706099377895405226266302144066147093990975126637566326398986436282384809938367566906692287851564057211923819613031894362946869187375/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^16 - 1415796494658716290750088783947458529540906983668428038545088202764941013414447553920991250131813146360858680568237595193866223454472383643980342439601287511479981322846558019508181589993220128482200832752930117381258812641780463005843898191018015781/4640833755496184917624544103821410190986504663286101907348737603765421924236245512625454291694265275664622850929243860373869577749726243461102001745015147026112930983601838367805678625208447447852248748986170965374757698824175396063769856832272*y^15 + 964631054583958311333116888226727842824792800244035572844007171818723371909305688869558002078242688903488925684783467572936296097447659702315789449418890878817374030751165176429535336780779469566813846283907281443041002194782136984184588549182589511/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y^14 + 4562650595638139983435928342342005389311669897139044327100764838464209978416661277594901408067673027582452803819357646884359727879074324540151506073467601233315219874439838433813569426787688213290209963837808954784090924579373972550113581153834689567/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^13 - 40686782589744282785424265802490423390574836979606119459789628291627379606917654536151925796248810516109995943138489759026045639899676229340245866541562978593386255209309736722898379215638898409220167873380055393919496288261592421926240194573891349/2320416877748092458812272051910705095493252331643050953674368801882710962118122756312727145847132637832311425464621930186934788874863121730551000872507573513056465491800919183902839312604223723926124374493085482687378849412087698031884928416136*y^12 - 1173648335779055239758750701715693080785425137716827145300123938223182277472857388940596536213684571799320653165571093995171316140330664322945883947320415825456532961833912385960470378701081306949576588597908942355487747348271093678249771667994566233/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y^11 - 310453452980514630941072287926141679105507871189115897568977416247625719779584636984036620530990964182843328955304703713242268466156821207541694507447528141184192518699061873383145253006269502326523724292891856464389212633831293320542648843448400219/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^10 + 708705961753811093560714608729182866799359879416607817408845821027108714413613423600542832177105872215200027013710475049036396386379710044954115096182018164860411943585834118636541027962580907586106329923509705999298614959879973253228246787401390375/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^9 + 27205024192306893218351328156970812666968098752782240392862192535182587445168579372391126613791005190417004264391982461256017539270605590981058350876755539909959523087463622160292005271784039862673042692384808652696609193535370140853233410343984309/2320416877748092458812272051910705095493252331643050953674368801882710962118122756312727145847132637832311425464621930186934788874863121730551000872507573513056465491800919183902839312604223723926124374493085482687378849412087698031884928416136*y^8 - 13383714024726093118188007793323292838337280365028398141455829549544699448578258748734479141170624798957954157985829917438546312002737154217627228824627988798506765421019343553671869098027056460445966971111138634974569511888812653579344393495143945/2320416877748092458812272051910705095493252331643050953674368801882710962118122756312727145847132637832311425464621930186934788874863121730551000872507573513056465491800919183902839312604223723926124374493085482687378849412087698031884928416136*y^7 - 55465918114993572477652231892787692304717053603244109810628351067456786659866484410536856778859455711258418218508684564293205876036134757306277405304817761118760858963699934008195720858797604104180409353232203941092625771506426046613752378712512283/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^6 + 2436346217455078851486350357324820660109940848085942304700358273910425746627718793378772763693898389598068928286858009856219973372911288586124889369088149155808747666057774838496492907311620823526034903634490634256236224341877422123462485107933861/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y^5 + 6191462872954632045635436422333876628069329925607085866176857280989170197135240248255819813917896717661061578374346126042421274243828795973005366517915676254367934131429135733829868963563894929299256912602879148845328847613078768920415197176048093/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088*y^4 + 78197283163786020267036128901497266094504298231001138496448680013260943084996112376282431711644449990749825256458953302227315848016410579001692488454589782256467797016538155783770409283214891110280762457367251689697496134321675047140349619867925/4640833755496184917624544103821410190986504663286101907348737603765421924236245512625454291694265275664622850929243860373869577749726243461102001745015147026112930983601838367805678625208447447852248748986170965374757698824175396063769856832272*y^3 - 78901888846526951972314192286478421616787734873977273921049145576965074888289895869284126595267691997997786869046042178336249029857709994209630427246214646605857389528342177293094171435297805644424542083945352970426992010245534302430320188509207/4640833755496184917624544103821410190986504663286101907348737603765421924236245512625454291694265275664622850929243860373869577749726243461102001745015147026112930983601838367805678625208447447852248748986170965374757698824175396063769856832272*y^2 - 13793668432800589590667043845568098006253724112263870963158350688319445639657265283044144369355394040824908483768710112966491622883722344336270684791201876069754319579218522782520543276847526701444800553628877988143758522639863732549687210365995/9281667510992369835249088207642820381973009326572203814697475207530843848472491025250908583388530551329245701858487720747739155499452486922204003490030294052225861967203676735611357250416894895704497497972341930749515397648350792127539713664544*y + 7597042728677629336121296821497994033707447342775341233126057531577845996016027262852692106157127572165244342217200763986018875960749325432210376579085057858350116965787739375611205163162758128122320949743604799479590905747437273855195160769519/18563335021984739670498176415285640763946018653144407629394950415061687696944982050501817166777061102658491403716975441495478310998904973844408006980060588104451723934407353471222714500833789791408994995944683861499030795296701584255079427329088

# 4 Loop Invariant
-274796880831164063062657363088569369443876575979555581038161346769629793665725509148276385458017942098074446733551918141226380017045455678033808263131237518387155053994043843304183525631505631836057572919674546333281880025755532183628745468791509765970027892457972645649653287278660278831370364945734184597182011367606790091421328532544533968251958820250645909/322194276778091500667164554208026209691445113690661689598358024997765105996563552263236194737055650771522481166337920772825363811586053211933097769290780980386074948710921678409339963650934004224701332097430993081985216204472992472480873167283187983640922302608346796552038127710635647089064216884244515654530478166954661316018088904134709427316406305509678080*y^31 - 117625757278210550094514796214527151278064727102691768667132050345384730031423320381609671540799826085533292756658361676419483290984475246220201145210673573194886606396121751562305845690993499922130181012455852408372361154805179746072520736348768565420842387054270859751676805882556399309916181420442976775448879884470675958655447285019937924770693475435210901/32219427677809150066716455420802620969144511369066168959835802499776510599656355226323619473705565077152248116633792077282536381158605321193309776929078098038607494871092167840933996365093400422470133209743099308198521620447299247248087316728318798364092230260834679655203812771063564708906421688424451565453047816695466131601808890413470942731640630550967808*y^30 + 55976487504181937547672568797329644773836492790523230414430864843613000422482172069659022701573075677740484462831294940700216708560687833944585951136410564152972839579027614497096286522614243685502071824893135127727727912251996772421705130336962924633780800210619129718406493878446175392345079570049862627686016076182176241324227855908810593994995443350049055711/483291415167137251000746831312039314537167670535992534397537037496647658994845328394854292105583476157283721749506881159238045717379079817899646653936171470579112423066382517614009945476401006337051998146146489622977824306709488708721309750924781975461383453912520194828057191565953470633596325326366773481795717250431991974027133356202064140974609458264517120*y^29 - 120321336362119581312481340028064244871295462338939343475627701714002063581109499761628895257920797274200180360932145001881095079773566550813959573470898989670684143414317718347649829891869859313041149844587091360388044415610950451510449940061697463878545836563355133955159005226328690657285813058401488951122780667998889123027986270412181571331398815197371277991/483291415167137251000746831312039314537167670535992534397537037496647658994845328394854292105583476157283721749506881159238045717379079817899646653936171470579112423066382517614009945476401006337051998146146489622977824306709488708721309750924781975461383453912520194828057191565953470633596325326366773481795717250431991974027133356202064140974609458264517120*y^28 - 664469569360274055925741222363776248360708164835178092635997303487434696305280987976739201570456027557573339886584583002175089006122687932745501765828911896021449881370442902959266043627875718875864532221675291141030140391315396981591579100287196304994829985358944763663161264633636061526561884489506509259131914686580948214792082195866657505525910014228098165957/322194276778091500667164554208026209691445113690661689598358024997765105996563552263236194737055650771522481166337920772825363811586053211933097769290780980386074948710921678409339963650934004224701332097430993081985216204472992472480873167283187983640922302608346796552038127710635647089064216884244515654530478166954661316018088904134709427316406305509678080*y^27 + 5561989989503092245623969914666511381936245341631992193017593812414049065131669279167545400032125382472650662687257703242536021206820601547565962190135901407941914117363756596923978037090990496228936233702901361481299907246487431617633481252806462887949107282253092689978979117246317373498374591478993079611224902106050718694447928572123746596844545152317118795621/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^26 + 1742120464912632687068135259934617253781314523437019879641172738011153476385639642259868228537416243495273828523119736268816129697050457423632677073489700558867255169113237022553495959381119167554800358344593602387261477490782662391250811793623118539634646185708495718276919470161844668923334072425017856939241790514887845067071369407391166891880181869285930590577/96658283033427450200149366262407862907433534107198506879507407499329531798969065678970858421116695231456744349901376231847609143475815963579929330787234294115822484613276503522801989095280201267410399629229297924595564861341897741744261950184956395092276690782504038965611438313190694126719265065273354696359143450086398394805426671240412828194921891652903424*y^25 - 6098837818786882964879543015422405294488254610589172289922156222294589698475837190084872729052138560281269156402596942760194146436835621061606772427068519886260396740965515054717326118575964916910571697899874708435019734669067722676296496052788118838711417552957785091010839629816693036760475386896252177852960338698935340335876656011568511136678644948136929735977/120822853791784312750186707828009828634291917633998133599384259374161914748711332098713573026395869039320930437376720289809511429344769954474911663484042867644778105766595629403502486369100251584262999536536622405744456076677372177180327437731195493865345863478130048707014297891488367658399081331591693370448929312607997993506783339050516035243652364566129280*y^24 - 8238151874513881007459940064021499178737896622907085613934251357636424122473502357552715461687881499806291505834969316211579797770474577129843769490678344237273793331192269764753356331757726258985045992284446634027357522325040137275992576978927776467731124453636426886550595024694344847203845403265302157854896889081400419336644529406085682307734260427243963940831/80548569194522875166791138552006552422861278422665422399589506249441276499140888065809048684263912692880620291584480193206340952896513302983274442322695245096518737177730419602334990912733501056175333024357748270496304051118248118120218291820796995910230575652086699138009531927658911772266054221061128913632619541738665329004522226033677356829101576377419520*y^23 + 115986385132802863975289393329777379835666994966612969456292975746041545349038810135217350369723472935808614207567503783830845004972029460381989718546708561045819583930666520359410029367707075210767396704876238771477907097971906305872960217411425242395441667659749111550744509021914208158157036490817873386210797071984219797258085195355556692039909183894424105475569/483291415167137251000746831312039314537167670535992534397537037496647658994845328394854292105583476157283721749506881159238045717379079817899646653936171470579112423066382517614009945476401006337051998146146489622977824306709488708721309750924781975461383453912520194828057191565953470633596325326366773481795717250431991974027133356202064140974609458264517120*y^22 + 77116765073566228571927488082067710079850142574558075409455074741551537358430779848598700471650710618780710657267508910185723009732366170773425852338270510652482516782292061131887003884794107508093360601609469839064847080424605761170435021089744657010028042503049318758994471997301729045093148993340418158005211657935630682959338129669383928129162726390913919060407/193316566066854900400298732524815725814867068214397013759014814998659063597938131357941716842233390462913488699802752463695218286951631927159858661574468588231644969226553007045603978190560402534820799258458595849191129722683795483488523900369912790184553381565008077931222876626381388253438530130546709392718286900172796789610853342480825656389843783305806848*y^21 - 670417354561370266198094997942688888468774006256089853333262149745681924271055017882388856555005535048858407157644682159557535547982143331689057577732355895125475637975869610667368254761384080021626460647338697351186241497853116424224092599659639083546079249007386885596232225422075365992415621965111906652153100851238701028894192115207935293913888388288142114881267/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^20 - 1015811767584597991023668951556647665232336457458040798809445443802382617209643943882465053081833514164315514435614194951766651606238722575166002722242228421473990216493283831300023622266812210113766968084277889035783563435616275243817357402135119532143018906600628469366076141506250428018734885350752415704769521502759205060516326651938132083970052891651906103234957/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^19 + 101033360024917742209769583278022631691032386214808560106940223379681516254989922975686752151012977350848194528150822785903936403696417831822275925350998083853869926731569879831687785325217109970147437254772989718681817204985581821256117938894605511611650685893948090916010765644321048990614869755638908202093105366957575600084096358358737179049175623929098821273159/80548569194522875166791138552006552422861278422665422399589506249441276499140888065809048684263912692880620291584480193206340952896513302983274442322695245096518737177730419602334990912733501056175333024357748270496304051118248118120218291820796995910230575652086699138009531927658911772266054221061128913632619541738665329004522226033677356829101576377419520*y^18 + 199763897386539170599195422295835416795197028473340710236571779210028095187626136515275140693049248172229530002326333033762538736045773228280028192768004189749673268769943886057952356203529790809480941518619408378016973196096952974031236791924415158263789923965414508358157270219955595716544045025278670611556494102675880112720073618051058689149344668180184822931527/107398092259363833555721518069342069897148371230220563199452674999255035332187850754412064912351883590507493722112640257608454603862017737311032589763593660128691649570307226136446654550311334741567110699143664360661738734824330824160291055761062661213640767536115598850679375903545215696354738961414838551510159388984887105339362968044903142438802101836559360*y^17 - 41684224473800940591632033447328119356062229950289030675591982854644137912752307389492341126044820752331837331927468085221201341734606769454667539044457069279219529004511131481827901477838255355509863860534448398083386149765978000890079933629569513782524324778876109705070870181395253983763606721024869472267456853780426726920853158107192085904834456598788106253409/30205713447946078187546676957002457158572979408499533399846064843540478687177833024678393256598967259830232609344180072452377857336192488618727915871010716911194526441648907350875621592275062896065749884134155601436114019169343044295081859432798873466336465869532512176753574472872091914599770332897923342612232328151999498376695834762629008810913091141532320*y^16 - 180164611697172401633232022470753434057993098614752935716722974937904372510249353339123166471774651355682013438105964004741520285231015981249355420000634561571802003812207487402935920036223534254548661480359303828075877586623826013313258441622232922996952433693405199257730091673274698039411029383979578127274131452903431615181420575402515200456613978503466222045043/80548569194522875166791138552006552422861278422665422399589506249441276499140888065809048684263912692880620291584480193206340952896513302983274442322695245096518737177730419602334990912733501056175333024357748270496304051118248118120218291820796995910230575652086699138009531927658911772266054221061128913632619541738665329004522226033677356829101576377419520*y^15 + 811386071678702777655670105043936739252638340609498766092463954284805971942444871704193808066381897829587683744382214344750832926841437251385623427932015451262712916406943452650809691294754346736912133214903823703978092968374337200510894811545636846149801302996481790059482785512677400941763824057355460122638174091276837658675992506761088233000913076865566483540323/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^14 + 350939963970259581210927423580768516288982120469714476273494305777368115394805261011077925838545652377850679062749954344059826754877100934761805891518031151907904318015183414901132550773152208474940984613571827099403041659326957836609829754733375379678011773492034863624212371149896580600944197359121960829266638875306718040561571890512072228444186611241461175317239/193316566066854900400298732524815725814867068214397013759014814998659063597938131357941716842233390462913488699802752463695218286951631927159858661574468588231644969226553007045603978190560402534820799258458595849191129722683795483488523900369912790184553381565008077931222876626381388253438530130546709392718286900172796789610853342480825656389843783305806848*y^13 - 9564852947451433833568230023270146559087188455094567860560624996718663519047802516834617645110673523912876047497233617293646386665710054835125355709792921531449446841145955483131632455958259600933884428169464359798938211044562442149008801803002584030876455216899989964999410064725771436339227331525776650672031173087388640029378208235512141586640265078639426418121/53699046129681916777860759034671034948574185615110281599726337499627517666093925377206032456175941795253746861056320128804227301931008868655516294881796830064345824785153613068223327275155667370783555349571832180330869367412165412080145527880531330606820383768057799425339687951772607848177369480707419275755079694492443552669681484022451571219401050918279680*y^12 - 911640227719314565327885182311200150861802744449388106752798823397649622200501672011362766973183953689784795290212352302232623669950509569301772440884087312942740416001015799883584011950437756771503321343222693187006202757705750254192339538789015661317777750193193143678769645139834228430868453440647073144362213580622218443593859019632111697713295943942466232918277/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^11 - 50134343162191368789787290016902334212108873451791030478870873177251575599883641916758069020018048665197374748421456832401825283239368979702817890270910501468992019487055054259875811448688168374842853106630617274861207752423700244811347910282697068912228728162733563041094105222659436446583756758000530755822424459964116575500393692463301835838636012521231450148723/483291415167137251000746831312039314537167670535992534397537037496647658994845328394854292105583476157283721749506881159238045717379079817899646653936171470579112423066382517614009945476401006337051998146146489622977824306709488708721309750924781975461383453912520194828057191565953470633596325326366773481795717250431991974027133356202064140974609458264517120*y^10 + 279287460580994187470557120096541554813731234697761380834368585138125911298106268350440034492539006189580885133246125618831489689124740494750435939483834979060388543868519498969976139423224043937626102857821533550957689061085888973467651136177445870616763709813958421372074801887838573445985856256724454000506439639699796619027775785946265742382698035491261136139383/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^9 + 79630519439855082515445437500271613044776411877179564094635505968602957781329807996042551690357504847047331858111064789245945307744579509846087876532836416887648169422824893165843267956998111779958962654681636098910397834162271643326141698532850969048735223715818656190628950684595673075522922529743082031947907452479494674693640166334437662099224713911940786963071/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^8 - 43432208706862942985787272086915666400418952995850219092583186471909530127057908508603663047970589458526410820896940888771808691329730759899704873396702079663688596601864994112986021801717466000671084512691073705264125889859086889401110602143515309273112369434291813299264056650897752143959721641982919504081999076248682819909762010304918953503360549118349733222549/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240*y^7 - 10517165053002273636495040206839014602094794332776296700492254928383314167320971665999730938347095624927807423736606090559708841077474605977819098322770626376914658002489404872343771793247081531181890212717249468750302278739418399546742752982213486169560054452552182268619859554174991170522841991910856347607419107396114186735549423453098933425584190817465085475069/483291415167137251000746831312039314537167670535992534397537037496647658994845328394854292105583476157283721749506881159238045717379079817899646653936171470579112423066382517614009945476401006337051998146146489622977824306709488708721309750924781975461383453912520194828057191565953470633596325326366773481795717250431991974027133356202064140974609458264517120*y^6 + 1114853264180816293446333964825129497803065750951439294080632616537556198531623968691604805359445293715697978208690608182774710473275457222839490751674701030276863205558082620481175002941370347121182897270162930765962016661741703561206041151127002138051405729481136749357695864083335942268568641749856902176249212004676882722886344749299641783584123980195213174519/483291415167137251000746831312039314537167670535992534397537037496647658994845328394854292105583476157283721749506881159238045717379079817899646653936171470579112423066382517614009945476401006337051998146146489622977824306709488708721309750924781975461383453912520194828057191565953470633596325326366773481795717250431991974027133356202064140974609458264517120*y^5 + 480871062019837587839350106459719804736826055359840220053632428960174240469059051257991319037311208141615773663544240119996412890929174278595637685190839580872597534011905654395364401971769333572450277846832217968867529321210837030924070528066075288630946859430122992188504071398374505711175154810176113065883938461897361792323208745742018290090132218338570003953/193316566066854900400298732524815725814867068214397013759014814998659063597938131357941716842233390462913488699802752463695218286951631927159858661574468588231644969226553007045603978190560402534820799258458595849191129722683795483488523900369912790184553381565008077931222876626381388253438530130546709392718286900172796789610853342480825656389843783305806848*y^4 + 32431102317578271617848613637343808850536839335109378815295700840677620606844784704345488934824157298070783506474036968644244925634569661772524250615570635888537057707559949470404551167025226687654080789429445198014311683387802251414885982249540050468817724322576379484173914986723758331774045732969689914822972664932899509135070049666079634322283105071714124257/322194276778091500667164554208026209691445113690661689598358024997765105996563552263236194737055650771522481166337920772825363811586053211933097769290780980386074948710921678409339963650934004224701332097430993081985216204472992472480873167283187983640922302608346796552038127710635647089064216884244515654530478166954661316018088904134709427316406305509678080*y^3 - 13833858887392866995906811455007253716126095327208475262169537620995527545614442172667075035608916208062341466761342254249645703381971926714522835985262956796774801681709875536052390775400917945253881781023585000116525178436783082548144971051579124160335901656420138843762442575753716403888524648063424006636491020424532586447702974490053688659327963449947584163/107398092259363833555721518069342069897148371230220563199452674999255035332187850754412064912351883590507493722112640257608454603862017737311032589763593660128691649570307226136446654550311334741567110699143664360661738734824330824160291055761062661213640767536115598850679375903545215696354738961414838551510159388984887105339362968044903142438802101836559360*y^2 - 3365977504886489138364190550625752325176441929907392103643414598552195483958357373716411772793507646186720518860369255950940009087893039802583013645913205078622810085611495410872290683973034691153307066027766196869150008164152732741446543469770086681551597219348494763448501719549378719397370819578768023689343688128091525383587077163870355197824586089364731509/322194276778091500667164554208026209691445113690661689598358024997765105996563552263236194737055650771522481166337920772825363811586053211933097769290780980386074948710921678409339963650934004224701332097430993081985216204472992472480873167283187983640922302608346796552038127710635647089064216884244515654530478166954661316018088904134709427316406305509678080*y + 2872624320654886349503372511899925634029974413894316184166367187695671018541936285451628337561794418834303691715271061195720904991835263979855749890904867305563401718758000000796108139334017029521919739788266889617178234637464812682458327155643500547518269267397000667401949095385509949077679240666915869479427999026097634061024562069046510704117421121397448037/966582830334274502001493662624078629074335341071985068795074074993295317989690656789708584211166952314567443499013762318476091434758159635799293307872342941158224846132765035228019890952802012674103996292292979245955648613418977417442619501849563950922766907825040389656114383131906941267192650652733546963591434500863983948054266712404128281949218916529034240