# Manifold: Census Knot K8_219

# Number of Tetrahedra: 8

# Number Field
x^38 - 3*x^37 - 9*x^36 - 73*x^35 + 155*x^34 + 701*x^33 + 1985*x^32 - 10716*x^31 - 6001*x^30 + 48478*x^29 + 108847*x^28 + 232712*x^27 - 102730*x^26 + 8195*x^25 - 1203635*x^24 - 3495215*x^23 + 2657521*x^22 + 10423876*x^21 + 976801*x^20 - 18120173*x^19 - 3673521*x^18 + 14779275*x^17 + 3525797*x^16 - 2884172*x^15 - 5371720*x^14 - 413399*x^13 + 3026543*x^12 + 88690*x^11 - 695655*x^10 + 64117*x^9 + 74227*x^8 - 43655*x^7 - 7112*x^6 + 10266*x^5 + 1803*x^4 - 802*x^3 - 216*x^2 - 7*x + 1 

# Approximate Field Generator
-0.246755069465497 + 0.722237929062781*I

# Shape Parameters
-128573737625981402279642250062333184335777717829274215727692725421318523297742532572149334999659673999166158988206569071088706067262825575140/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 + 309342610922389509675266463042865438476005983815015423029060664679862424743066223137362571307934877123721809584573130901496496937213858092230/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 + 1337317856489872749059550459329505564781042039674383848319074223698320177711765893996210714279350762804904672642659572420089893605990213877517/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 + 10190330841209447791733212007177621802180932542859714998879256462610495332588996026193084085235334190817450018064405392819240036523470637481606/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 - 13841557391676476296262027290509759179257623506994034414809405171796190740457633695818553453417628605467275427336415641957141162045643390250167/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 - 98079295759932184040558438516593946233595147610585910376002080504951268408413966500974467124861748791167744656385845672269071394470694081734532/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 - 313972426604838921356366083170155156894113974934323370700446337175718271990029027455855861642732862097202045877212754001813298324819718328151191/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 + 1188708974229652359882192370069948784457482753176308407510799195687487450506670824791473868220438431951554404776841234762605143434258729976855385/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 + 1469864066870686048790166231953212803561264043687254488536724503747686356530146841517811004802745706535361518066278681014347662709408510570506822/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 - 5323536701215215555236609511011265923682908222898121497974961765009940530483941629410751303117930862521865155300030864549154009448932220289829911/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 - 17129438001182626601062054921017860851633481351918910465331463191791859625990515366552955104589107429652057331189674857795876909482162445656179567/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 - 40256436622577053477863450797333079305095503892964083879302150063685077547680134215055262501346119060178546116497917890870956013921479748515447048/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 - 11127217238514769182441865736529709629040978463148923677627337075237151586063128512538340755169698784219715934447540634939017636692074641054166202/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 - 8635971415671722556591531450062976710047284265837294795415545820980605890414991651475928462056970496969704832542691333249551044228576631183656148/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 + 149675544456523127576651044804034040310646710773563088089549248048273155932019780600056671944581515705194138710023636832896305034268969341248179889/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 + 538048652770048212182037777954112339553017025383429480698295400681911126698364248235334725495230713069274427350093186555031623671148459984518594466/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 - 17777675579485898140341583831477002859918297808431697863880399919658152540101306841523385109778927538630941732716464076127854276537398209418281093/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 - 1337286752486481632845780477640046494928931944097466238893452390904715314872517819534674303194063244859589458505888522017701994158634603235985695680/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 - 925544470831094110260035958062906635103171202471226409323727632569146611903909162013238757176556593881730283728164552854864682610256229447559608676/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 + 1744409625001138299897030846896755099464774984835252674185178751249850966838503797874575282807198974529187634819182359591839526820338830963262868345/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 + 1495960004420766293215114812576373417502754034438693677034066276338756771139837415344558979508658645211614639504707209557812431146683724850474100617/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 - 957596396629364995755903807339962777718940596490749085083887435283526828606458113152018803371692029332474370005744806110344768960166239441636154444/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 - 1000385150073560040952237637101766652499903381613134480801753732599978295652431550740559746963389817249820061595516284354643658812488624525457191514/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 - 259133950487397027712538824914784989317349317443293030122388332322257578376625452487553120703345930497881317255561991999178091273052529500224437524/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 + 521994069531269200442661857135247764574640951250602242978379749115599432869690337352461059444844364914501752912046920805176154893116399016804596334/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 + 362098546633457919935611878019706534599919929672519528939997639446487933455274999171637130754605676983520153499091019778648996292919461099930852509/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 - 158914016710002031195675154764694614986016961029920469468404882883933197200458292086891543326039940955814592907818331720605010249591042262128290639/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 - 101417554618694343508792187308241603048009800326858465959775499674270449565188643051361860133187537260071714119355340365125391762945281874757186737/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 + 22862045767213032340600828916995669164514247606213051386960414462078612741253003574021878833430776666846437419889219428951968035370150852545297803/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 + 4857295414836203934522620671034055559246540395154748554735062177493205819607576152460575502576929821283410079378962101131634033140710894835067766/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 - 5712142012483307089705761533857969532337846095541625686012642001524229326080970863504127670857960214727548739367526219554013898470719014505706566/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 + 1999994849302138546281580900905527398935751002555342193875351441503200516815242776938901436663467862939116692107783390342842923762342806862016662/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 + 2006079291993009046625872390011227774749930565351015894700496428341017989932313861399250375526403240243884703844551212439766626778570429897641836/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 - 32575409312187724250078309793036257351988561315560797276325739852798791216463297118244207696745925897314288289234426672838333404031343571625559/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 - 230418140443405402104039494385278353579513536155772306502341883089832623679346686437992810908182168945985610800614721491142424717907197588942961/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 - 44426688954177782715280041182756899035169300506038484788484431902803525721100030149227947259770291778336233254553672180947947545832418751684511/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 - 1253241373730824048953336943974384090031681202198361585854179331953024973749164806050132968147805141660744234330733893939946996385097911474776/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y + 202632931510586011344405703395730280555543159108942772114467100740405181939731192265358119252242198673979233893996339357541271754098560681089/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

-86638658428511366642020468491646806076944704729739404970046419353029970626647671878108451668117883709609067823586533450305160845074519438207/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 + 332646587739755656445515101416419828144679120445812935818204942886036124660211133770693396158404091398745399537145983809817482345300154318742/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 + 554421715149072366329774647438822275825498245384471219019417732079934620423679415398393643950915094022041261640713453349722964905395958232382/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 + 5706848068573210679587226131696238368086969434395198782280127712357897340924345074849206355078202446378605417777401039310066224733906109491425/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 - 18718169264420130982212820658726003933868658683927375643411205228590714115374651025111753225641698362130738411897773819915004105585371022597904/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 - 49080639216014009774779302632917561101403127580270959443986716960453996481501668755907636885891423113229510428666533498463140070780904377949193/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 - 123253358704056134556671326738126377702399305234694933600490261098743208771864564615584493101358331076441093268579958401959728813482774178108956/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 + 1069979850854806608008753562836443856513377776598286808540223681598164325176776123684474689469485859634380492071533221170215967401969788586857717/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 - 262808022578732275942160847382095786181986452994185274735852841263280790497971382373994384839541773048928280144512281219761766050933809605821129/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 - 4527503086868683910518936729614068946721744963205194106638975070201441259108940072075901138576955575437223804145531390602523281657243837252085097/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 - 6019515675409934536902656434508529391325459202342454010918979541108630428541434482751408944248256143965695309024664712789145552436605526028078010/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 - 12697410633931517073407813280677395112589914287199993686430366778743063422964450112594191884348430925799549677500160183507736717482700989101044069/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 + 25743553925102052767269698828028441795134848598066735790188367238891175147662106522578572613621194699955101779195021423589456949042396512443515183/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 - 8098901441577336655614440646601135247158291411864598779557492871697365287215816278928957334220168715347913877683092124497483452682254712860939802/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 + 109600944230270105905385364914474517534244644692374344266859273754260566577568949019512375826101071795595546124574089538093298540422558661425923231/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 + 214634222287735034505884217627734671016586290079223435936162819509032374312744704268963425666479774843545449640004560518699100887840149675946221234/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 - 474808630488484061150175020531772064541301252462061948515010574272846798600958464559579586243733813913573716435428185248900258837211315968221120904/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 - 703309788513135113776340635317464128321047208829100509402576483902209439572235985153901883805622535223109279700980710045098965791553210122674864607/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 + 598413536591715189537143095229595053354936913106850066952101205543816175257474099683427613216951854768535504355963454956216289670365474517842715058/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 + 1595264807288670714217318999434200222995535611401322451868225005309727910005287789421707016171771477307528030733337905296274740514208016090642730445/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 - 856144722917084284045680330715505356285969144877978064546125017472017768161541249736583577660919631477869283893495550285454620581617484957429832313/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 - 1376973585985974033625919485871886443867064311786324967337083300395295899791995157757603407750383732913475921268317860186766589040660580493694168706/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 + 559359761608983835621509769374962556347880425422579621789734398296612694468554169213544159218191339381179971890019584405211523949739674194106688385/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 + 325465843672018063310187817171575034309063808678323572838374703820383118808516409875956085967775223482284193200322040187458559861818633538288243084/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 + 391937731357299043085343149514796039520290595867645430647510948384962237391309253777600187091615028710398478684606624290467729133640177491138908801/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 - 281857468408414258300490989630931561365069091359495630284920465338917175365859150239762894890675444104906565006019090626027668224600506696500092821/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 - 254664492294163245152645424229594650321218042061363014669524901056221462933562872704961063783466046255616957873319247118069156732412621793470530412/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 + 149257313812005322350563793223295631622719175047600838138073985458994956511130385624834789031019453232260501199631036201880940737774170300985871033/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 + 31200748671875449359512980349060014372498114077565177585096671083238358087636611464146410079070471384199380831702824975914849034687071043761769979/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 - 27944408325937104954210180880576996842677365603672391415584621660992245339300137750744047695043875637108270001544356380857769442724840890845949506/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 + 3472303419045518580219641452606142610847695553109296795294810845433907422756075329468676160183607697499482350625175692448585582576154471804697665/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 + 4470423997935505298497698359842554136322118680558056949943256334202027357590494745761080795870711607059595020169696204470476000872454536972865434/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 - 1918596805730242884968662640103008577538043134138175159559892728812974658029824477198448098936168558365966736063730453088609813407227122238698807/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 - 734379485210311490495090731893442279082443162044867839804794106893892675046978297125213227264591282029237636241412104161382543035511005601754554/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 + 197573113791005732905589503267851803276314767926272297034121294271156100613477224354661447929943359269383173799780608242367746292001542119192263/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 + 63212297024095776078656490880903255942375951602088973637675434816339000628642797665187520738554018418373736683806243575829428837771172824545558/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 + 1008190962781671780029631094023578143346569544701334942313703807066198544491829778438259184488583520433267173915805064602866884302079209787803/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y - 233427504439973530370816662361219509560379042218128111880122862171444228802723811237245444721200369787651077089978193950817867907021926660129/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

66927431575407404618658508524895267198515848981570613983896614750383054232296634271610167380935820332034668910120550719610559560809630834379/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 - 185498414832868835284101059827992156427742694512332173282952108435333553476977541035135173607325069881076492663263747358342741732395912891892/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 - 629710806109443938371345647956741833951689942095944931831654328458095126200983172377535541206580477775412588213510216133182518432927221923163/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 - 5070410244569052462234800692973438470324566053567451319669295680054953153686106863099335657725795593994496901097409860932897896380210093379907/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 + 9072922335648632883102574005101412295929986007917064844291295285071695415569626943583878251622969283775498315474490270289916585703811617427502/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 + 47845554103966170833331667542408685283091299898876734297342629756650492733347995134760185007423051846213005587397332665768761486399737573966699/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 + 145759853709590504715970147127539353598000729089452797899819233040540639686604192909662447438711816059350229546668186899261238795817965087338620/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 - 673098117367120103626365450235334561990069591309599065466053110796640681783959265393680220502789226559559266752710711599029871000696250892477741/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 - 522203116655082146282395756038072251002355109665583401907383435440977131119555068365010459100346393805276527415721396196027103720783833792294103/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 + 2975883605289591631810084449895685823063816820566305738967677635593386371080584826256747824801389550947001119750616731770990072468279968856758468/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 + 7840790135821011057481369140045976473019876674659243079459817912010034914783982686162813266936606896439474234398227930263382472813924603485364496/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 + 18026815480789868423516628293724598688653849308903540801149246587540110126664512996984253655179405478105622830490216924836766258201685437482162734/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 - 972347432312913990032238633422352659889313163135851747122466207524088010596682083038517024757483792626391301912968437982163453352229287940421741/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 + 4444682685476952378571132207792495929789821116629399729832512233786194429628200123385037665596609501762786149619437322616793001172846772262731266/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 - 79578130522157846411179068017278541494623159473893806834354610042963896882653818481564086413013313259434220151308360683163688924489905170264233954/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 - 251107063737172723814857245065151430440191930463697128909510991982899691277492594189537180472707416699256253446791575182466351208096981345473862010/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 + 102726760465717554312227305906723710502169373397554958156134807479926322073719976399107214954753514212722655708284483664835394561666163582906374453/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 + 664046509680896059520065990697688570126552748285623465095786188802145192839632280160311163075056844588069758915897632791430963822924839001392518147/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 + 237522367526577357061161375583163061589573129743776340197451879334835622690657752425718094979062048142344866322210378684877272085078179480498440076/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 - 1008747190679422011263131231497494134152713630968633124329372165213244973629667602519066558654076408134450950306355120601475496069924728340017719443/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 - 416355808269761389985023019329136543114537407602764463834994883266967297461739166523023463835099212516333612158326243973215372695296189654931407289/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 + 670563597484646000529407726985897191747119604811111514872613223771003735306520416039902593951062409902603609697517366978042064948401314302769577199/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 + 285823213247097623409263845896732390405852234149252897935060606553979186365719259599133694440339970263860061286447691254299535682185847577773528606/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 + 18051893430953996297908668738250572962706288020334956943443117722283577131465243153280539586038428269273745644579567952745061311312527747396907586/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 - 284725930335456463647089575214909599193664572261947120294601687026079714306896073483360873608242256125151643536287301325436919971502848507532655326/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 - 85605505211192812760187748333128708822179405914395705538493031747817146463081010902436304026871385107194392511798750347477448364093290296665993692/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 + 119408850373691378235993379223351555896118263382394664115423907327763694994186419789161977690230068470939577810574904448842498028258473119355481543/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 + 11217920510404581103719741365777331245222741478671969485713268667070016179183443188219476170668634673226362372764893357324500241323881890284206173/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 - 18184037768613374216052404003817570014839337843872545434689014141785047650997353788730636564789817477546954210287758258414043760078608081941021100/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 + 3838890943019499445890459519627282055812875852587810975205289240600854409586035363224844022544507887935478926030618042137595335715875830990040424/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 + 1911934794387180329373054373648658045685268674017429029476230819067641050624791682194394482875727347610172542000934822282908923995907049521634148/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 - 1813367502108041935839602554724679082461135423392325230033201711715388711234860670565974546722246026008367519141418873806088613904369046074424071/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 - 423561563378523091414342512836438864162876947630157258502323914696543263849860038600299869260266583407928684019675906125203918612002616500401909/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 + 203883917533651265028799853708447660414443986373076139770413395359703791668233310055350556365724344217713279070446127674672361901067596083871963/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 + 54395659037392545953282998332242491316704849023596411395564373563556035033487446562188988309758368762097438343639091491652644359739412524014811/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 - 87397568696404310572101392056856530196316195769968918799456210970647915442437168408181322609840877926581057849735909879918447185825046455660/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 - 361812665812287418195056401210308968850967787298469450857458852720045742662194949689800676195691147526564733249103280196919092034965910410475/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y + 40646921067883432155588512450902136013919384531464517726728829195904847894508073484097087999832166278590574477452232073628174867241175434173/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

94388337894624262152212808402427085219632476492382829685193571013119420111661263884938584964496658632050623975607709653294867637618453764557/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 - 222385604446659072512154424732709574149775767558084765987619623240986622445430516432639769220386578331083201733314805148481945736268077194725/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 - 1001814909052840543700047351987439541271709819251000341381465029985806479544716200047850025524795882483822388832180714527550488454988937134388/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 - 7503949383810960201826686903482595818244475199514234935364408552899757700365262469732904977869123883436281285659495693251813502201623417333032/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 + 9865554292324771883570921087166605327015204200707371798714123434356177385755784083647914556718689149529334970494990112641673737976292595082255/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 + 73154852988216296766002537856578241872657820036405281980075803360750750285968895094254519375966171938737688003956811739716052926643847924718158/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 + 232770025134706673087424607884242011172449132075160243432099207664494569443141127897300287050488144196856310784681877920149273518176345418781275/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 - 867166735875453256388266787528907667213471334632397220245220881122140647748220038703365681656454679654817183218941012235665737568050203119165098/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 - 1140413373661090545220780919487045143935071845541820627084574003612108036161074908642359007969174709829975457780814401113082427554728059234868963/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 + 3945876402287287440213841035608969471611105193046791263609434074535767302198605387692627752864228275378185350770360678596952903834732091727001142/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 + 12820955347007974410685544339224791483237260620372415338851396947901573327759460729493909483462559413152644405952003324317181859715219504468153482/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 + 29779552033232346333846671464714886351000372102848934916837420131735702605796124367030583326531286911587711548413083466796162551933655986058130552/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 + 8693812364015878122829955729608226426034694257062745618085319480755225486631646832155883080317441009335966251791832375579858345634212570547686464/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 + 4590235494026675794707738172365215460284842037748337424124949023516236743626136459004122792927482264915563380669008473266814890612717372896885483/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 - 108970079498885797907818150876368099315382766931545697539075662496554921026947271153542994026294241264246305772197341212244195382663825990884895712/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 - 401059905940999767873285032915593214357414402558917713561276398995133764886516511938561636409111677602686236346540855666517022381374695342367565966/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 + 3930479032837121460919748480916508690675539637814401153407143651160478434206992915192474897368177633160720664628459998540618803850920162440507616/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 + 1013140237305481345718647469805862226468218053728784629756543668861441756711571761093969484613999681350154344293116217388733475977487293690308369509/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 + 708681638179698157665188318684798082370702573233762596601489495885225433261142841888041312393636508023674891674675924377544889768105926053123388747/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 - 1330842283503646340026593205138332650542828937762848415782466612192245626738818133974490560281490081131993735930306953319562484257044735128243953304/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 - 1177174564530473932098670366275536837237228793676918514871221694857278803997605636865236450737975769257895883855737346738809918345297809165344126351/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 + 785466715371542941366013706609271714954824620520946782879976739782689488944590293083427592016541903993872313062788640231710059640082718697089443697/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 + 800075159972584979090367506738074516997610684138153029036572697452721827758811598222774560367403073059128607804433890800350367030139939902283786018/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 + 131087526391937343665723419885351507682879274766952978508957025733201159130983669616968682124766020404666537252799948577410827119106485960538285419/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 - 396367263516730296555844893957266371744614919556598306526818044717872215767902717572536759216439697208243904683117732319609091601073696802036751305/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 - 282682247172469589721123884527136393837198695643980107819473477790942618986940385875797467400637280704050779540648975049468499801876144330958081917/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 + 142138220944245662434030922991860264900094653766801395572056803817858510151216784590941537332230077930343026733729781693512953374198998831555190659/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 + 85229230298299595948175508176436494320034266363798473994442953635993691205688190198475076795501700846284785589694190451097248570485909706405130470/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 - 29978736997780089622323712694052735322278478713365609368246265243900507494450795511252920699495145587033258091956430165240498963057682733411995590/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 - 3405678517398443782103022746161869889424319955228261999279282873387201887400916140277206039005983093691456618098731637347792468653711291886303086/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 + 6165464504587310631448443742770332449856053420439427041982098420718244525789017574309583247913041178448111229686944665490127931083164403904692917/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 - 2032782772382864001980948693569448622385301814567294494330606419750185170485548266528587155837062547607007824628301578171136964665067833977728290/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 - 1651932235445287996172514879429620735167199906616423746152810345164965942997853283412012610691725942212935440643959243182303942172949857836481261/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 + 209020229077387383192502821570218396139818071034859338965818618845686308324834318380503683563099910172172975362118610470105807288771932503670644/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 + 189987568525806520583707309209469259682822610777880857382658897433852541971771890518334182868947666020814906642368342728891345628410649336658001/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 + 11675955043019606733736544167916478359932376505292400992638924698365563829467106587736520774211170140627988335766287316166299662160790384124011/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 - 1461644246994419652328802368699934033390718961129339463782765348764243694949161400580070939180662099392383089254494226286729836679205905711883/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y + 49441150303893533796176820846413076472081551746579699367926296996028083387514667759479344797809689362275675961581393953215400739884903234196/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

29091827663177153225925252578334626469058255472287374647954428510820003918103098366512046270091284012259545578511466453223835161786522602928/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 - 82473228259712805687756790021046642512808682786568581771366422669395912294952035793732467930028129575932712064857254756862451919980585152045/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 - 268194029854323343857323370276992188187153928020922548338925299846302671107717329297985212407518060741395694471693572532088005279844096416969/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 - 2187791275411974543690663089804229707351955273189541866630476154889146191028190880622000596910107145804107838776935243215693012535968970489058/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 + 4079273501961281712845716352415302251520997084858734187455762537753454710584850566244835340393290301237429825397610280636237380665058029650121/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 + 20514965827168860996973503621671262727495312383875520681070992111489658028680829445359353806626045587527619814668841208598222454534732393808417/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 + 62094702689867489651666232677148037633879600000785814548254280518570263658799977379957935935218258242955995734546953934626231446881313452177524/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 - 296289717789789899504568902221043179553764745923681165731888456701514142713916338729184942143818051001120166840486410613486446567160846174202379/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 - 207503843318941692345961490967781420582438879683589419696564964252949496648382500298093735076300975714209962634859401470976816124245851239987525/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 + 1303844642123000223900263756090636162755974607135061988335344221651786454534962198864095494448420019421904542555354217865814480522578569343232811/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 + 3322810844828122428694728496615010483075595468971737440088769871904251318802737924786048338466572915087940537463576541994538370849707192201661308/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 + 7637647596917458602737625403382941071634741423731077603596267504413938404822324346082619927365611516807767037792296024932155336774307263250089641/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 - 868051538847626754115258212893626024780812584266133119625421516463140773759501514953131392932326450925007528703082568946159231794045577102021479/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 + 2082623215880759308386461571961313814149798584722124010883498518862522794185074517658546580418788844802634160189520956049534742855903272207042575/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 - 34691544592398012946306215748937077068044935750479773142344543130005000388023110046366955107291652041976482535731980581708620491172721574029633566/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 - 106897395650822300098115144973612084787470955599779975216789314984914939464433910766443242247854935928849956352826327693956355050663096845637133701/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 + 51079507193683975123358370908802858516622501435563854834339318365927684469653249925290789720453639510637612037408083821624670554329372352131429056/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 + 284192354255388939430835729841558375010848746622606511255036988201118109799397045155857872420579068416697617186084755282718814507909412864962560590/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 + 85325607468934110741140673113065134923499576337130638442209607948427685405499865314677419206898378463693010053054378595787667647924231615075479397/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 - 441191538296688097958637811732545566910456174993119166280823428852211395079437381288528374858535363374377169421514127669285002724373095959368196130/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 - 151310865956485605322740996026085687912110745722046075942377237422182785930440133739205292607608176406368389652081782316217409761740370841861268516/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 + 297689657055860456565203582522466850446892494996158659856222679721016392242454247991702319028634515739573006971902404448090128145649560985536212844/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 + 103263616385623522612870102379071169859931170619450624015420415149936679610931374968670639336066906643572638669682122540347228119140480639154164497/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 + 2861448899124354786383913041338112861904834996205550687137591738913706293895369377418759459882233373038636078580032889652550453786520069674403490/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 - 123044379276405268331782570392715012771831812489319178221001482146629135738254176114888886090941450152307750932549534076188705845218822172941357644/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 - 28672448652273256839183181292840311448073636642952565655448729874521661132626502982942684980609678234023479900679262476867072233073324274589496165/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 + 52977335920180388971271667539260365514286205935685596671155757517728181929838196149164060798901489082472007430881408647494987364966149726517839200/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 + 1183416629757410356282975758451411559696999469067785130289272855442896924279985309934562351497520877856300391910397155801066933321970732295007571/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 - 7732476606629965720897328611199320212109494636182590761193678987010299003037205788027865116596779182883511630567538577340380308046319078356071129/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 + 2123299119258845104860006452862532054882647160677972095475691102111584974094523382670669400585810889522237350362193114830864460781502255816865508/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 + 676304902895800783193143693835635943957425830807825974650736637772279593124324405884402709586975036080164654417090230879525891739221378617255510/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 - 811833928563468605797913251149288314909613873796258177260529759031047397726263873906183381990680003825197775236238317853514119835383498328135562/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 - 128542865093625636780841789717465114033332160669180175356248100260968262850370175159813689395441988607760893616042856225064025769922339121695323/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 + 94420163014097495911154488668793474772483154820559505297639101642434590535297484888364630526129487520161827955225512103503198475574740266777459/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 + 17366595110614124246055716452921412657031061811814230544372560523304868293644633886767781110226660993906499983716519676031167685830640186833023/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 - 1083708024985775598935410103321579611002668537513201263053533308867748540270373523801665958136467404539966927090465133250940261642111354444848/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 - 150726612526310184268969117496529929721120630314497627228489057533011854150488007421557210275265253716623352013945140473018109523787992848937/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y + 27632269437500387249927667049453375412342726767458631139616620467680750191503639084510369325994844418911691190199146244238518575914994607064/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

327020293546692039107704092815555817089551183433984829352932197053803880381595611988716467462716011257430406507275263804894490217758326200562/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 - 878009221103213132222881134052536065571905943332211179319572113755260725791982707530999614963790882536414562487587292620752368495322954682321/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 - 3168242244806506979528469593186247855981130795828647117461235841528450567618788439122531650871533188757579083824186655071250250615912436475647/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 - 25003160645987776461636704477277068984119066242363624338455431142772651998365110055646258385577691495372806411172175623215486351291653018480971/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 + 42292528624241712426042198437287905900005453320096874629257299526388813771098542142394595628748213614653039554692307746033214685977919996560759/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 + 238559426295240217742622514693103082357962820051828989996604125849843715408641630037657544300388815385726689809259910685074560589523525025992404/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 + 730499689381509633696727222051759923213365178258931617855985960607802036212306300199586600151941714051537353862071380006201270577410472861656570/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 - 3235718846085928078908382484618113236424145175966351157963631793775035981576962060941281966243602998968817448404118152984324624265336602959146213/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 - 2862131496744583821449756173484537210301229849856882295209057168907193588828981014517806133627902673719164637826295865981964185429989234399393668/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 + 14455061449864988427039135603874933390989302245413923393510373695012993353311950547747394858947571920394520236828553235020670694132715551384129716/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 + 39637333604424521665775921144024166732927536495725940079900999268893272459054540252838933588923190049885852175024817753479353339844690109780175820/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 + 90814079962366821032196271687542704364701484101740207545108867107992037591452216642295938451386926792619363432194066152065796241275735251078977819/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 + 1552780273402362570264689489282930922510296669445852387349519329936233609426218080723799293831638214718683262870829889951962656553751171402551368/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 + 18290093405401008924455379596751452242737034778337114280020462884973077404388176145260918882336112200071820562263317258287965450762264231585089183/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 - 385787313607924000566677095383481677272994545465788537784434070348996616435374931558624333018667266238393812390359214247280050483262565234589425000/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 - 1261506103028306010154952426026520734816376331652892372040034860456747107117567978102032852747037218730178666555899090384380968257898983250156115634/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 + 411022750917525615520049558406065780431537074924558972703187827532939946399471317935904472391250116801319862197597042431066506551112697463678307604/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 + 3331797289115607467820821684370320517523217776991503429818456103864306436162100269362712422016629177518949076016769396826519266675310893085064513699/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 + 1409339407226680787930210659253664610347011378180623330896806171967980537776970995787320504214086518622051087736077952223284867398093353296055737198/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 - 4949770604275773679070964434795976604729133044724230369583649602916612088566589170980899811288270625086143461827004934760370084697696912939967873148/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 - 2474214887609814477489510827262709604736358780534557127344864525773508278054896679719147296132516773596963498675210945646152510585367443149133080733/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 + 3304586004104775231064917937458352154024890800038107290382908483876693297658546718967446339449759750209337529646266861873258403757972615950560079222/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 + 1711694525412792746191316440589974971015679331119422443457793732188376016962370458782053470454176847168993663137605637072975619766621271469445946789/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 + 62924303746010894784681250225870887164050006836491796303160944694692838795087718426055322922115882509872052763144619877423940503714701992792607292/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 - 1408495617757836903203237886673296420377363053036404045672414524649304345836040831307832897413805662451546054701651739743051659207928625135466187032/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 - 531659357306132047151732885695153045390081190288504573989386352556277099067201330862526364303947094171225641453254878896930408339634752628342948014/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 + 604869398603685186840009870301705284382076126246551854064415307913636683446325725353023145858301935381879670213334056164531505287780712336038620480/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 + 109044644562086961617443320833548574664372459854901051461162573505245165978200594657023152502644267759410011913293768155959143888533459046174466249/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 - 110024639722250740169052990747385855731714110689640299051511735774832412131186303417041812881473137614677123336086006804787669349482346608947781570/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 + 13861216716745319176578404994159871910436328038520268546090465126049308195121096998719597614277582073709061247647571538222146223694041218692240176/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 + 14191398082388545982526309316389532045245399313431341031418659521838799918448438341667410082055533691446613625462266580623094018764005276217291098/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 - 9363875923595721162367240694708165252463264845519765829160384313302919823707729141023458257589318094727478674831853617646200498517984403554419920/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 - 2932978361188067112480432260625001148690182730589118684242479123628193546642582693877131910904965754557704517921911893264424737542601697249311423/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 + 1221182566940022806069507295871331126623066626782400008348004017258128435320161372440341431230801586837601778415130433173082283587633239214648269/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 + 360058636482121185012633641979522643854362601748392977143309346235551429265414995634870711490690404464622917461725871329227252278657242082566588/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 - 24650303916929672988708830717570825059188841705111550855929407990491569017909810734495460331127717205333843454324633142342773246542828880121662/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 - 5696498251140732856828468806289463463693013638942184881797734281445753778961458389774618424548350071690544112688598697930032295151371568292076/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y + 388278046033179090491271812824870812172009750678933586737395721545371631284219184268481673799876799771773424172857302089576061010057577221987/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

-49123275007996761240734821273899554804733338484206155159967736880832894751176598365024991098237624936926252682089437285835227343094483428163/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 + 116956996081007685582185311508480937252898466056101507275993974055138173549802381292156655064861089975203399941313653014154604843819232256629/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 + 523945912295144329807877428907488892832352656795997869219874412624806562014768437163414481649263187991296418972029173574929107858478729432954/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 + 3887577303129177450301683558505937064668766655336547616800069384521936075557740386735400402614429570801203107744919294541964236774776545806712/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 - 5304474310932583311857603311679070822232508214616896927113434971609980110663379872430604759610706394130989327494829098852635642984354539921904/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 - 38466132093612268151822246087438205049626335156149625028984201175154645487978607410783436939492456390090927175396539162009509914606576932854643/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 - 120306650521210560774343977736980177604130693731572932679744810832744655735212232699761170875565437829969125714129448935508733905695101314083797/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 + 459050764159078285782490215557376893755171749075670419778952073091022305253169212135430644980377442730244765872661972918955821435868612200738905/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 + 601933023291402651942744999279481108301947687715923153652713608873310529573656206325603209701341462527605798684163835982645484316390626546461410/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 - 2095741246708456703033344315222934716030382391291716706556078728282781598253104013627106807677372998492354987330362554674675959069351188619503616/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 - 6749326497168467390407541423781510482532905174649714612788472391825087649075470362523862820018203885421575665140621800207514019131484232360648989/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 - 15221965017301368222783836682482759553937711332923952533055167605937154321600832029402288272366991054627409139671366009271109766614761279220982839/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 - 3137055916895158364389772929919672658508342128034119846574370845961225947718006454049038113509546128628425669752239641299174983683995701928164637/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 + 605293038362041137601827028233996180614277970023055794284607628757937267919761259314479585862136726894013018441799786948476844566391437850691870/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 + 60367808172592017310376158663356317265971692166001484769100379248907653043498619864940684675042059087342639887832338518807621850146388912488209379/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 + 209940194920685356011758390505762220721075098352690472970821646092429661041069148967798634809315028689864199072248028723054564849367784868110465919/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 - 11297400349656195426062843227128201658154404373431325020301869681206789800344842927098013480258439213236164548472021785315410893477107404767543049/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 - 558153742662643861474879059324291250914596266540517771462829260036413037031348079161402116607202586183067242932934017416352184700711225780124439675/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 - 392195069095160547299998359379576951453855668966961769174535686211834808852499880839009388761506691967342058603324402019364842773592219645472053437/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 + 742564639284594770648802127277647974031726663287869228856381269890709613186084762416439465260383801889472537953948587779481689604552631090553085557/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 + 704430938935363755574335359668112439609389745646361582821758477238897943853086309036508168311597527929182821323770721658512861073832695266097939409/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 - 414291544093685642880887543569624765588547092671318203441963345240755019882061077042010497140222781429534622546601046897334529858312015201492484348/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 - 529518572070526516711852156473063530011182654230195935828993917254448826120230060190412411569407505773430182539097065977430939949384078057620408320/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 - 116083133550359995134043243617222418541063515301191710088854908345212137587754591989707118191681098535079428498912844860127265339650393328583584260/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 + 254967385163246251478726949761382988220722780388440089722366862592332381297307894198189054875010261478326355487189541977253799140911533072607095873/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 + 193624387638828972913217828080622155804803362458748282814054953635996493310834310571315346495255380489325248139509857562663407817702146986382336698/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 - 63616055846808306947056796097816420740539480008601880742498635318918817058046850036016030045685929408136342842379144457702806842870615583718725199/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 - 66072784714779734394105233382019703756352010357384992856239438106466609851434666766933104545614198609139389747814178142428054988909832197440636564/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 + 5631039494679083038390219676232332905209107920840530469630425353127990702645676252042937440899719336848801820785908900183851649392437211503242721/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 + 5853086678705711741296034983968088076082294158054724129736232791631740245085068778047361900899211106658467118041601320345276778715143561427355906/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 - 2305288874314452865870019850163663334973851993656900178641766193816669845799581846651912682916341963985169145031505392338661004385072861519421786/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 + 680673157011670509711326095004583003952280523398399373075264444533073602835276556426827634945229734093252915382048970361677880773618023415550071/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 + 1224152222934887428043886088071125930820056362778677782238293979028443460782176744129099729183375742240084089895570068869182870249242110068683082/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 + 81691092803294086551365063039753115967181846445045915449869784882312977771575362913787190070136176120059426700093198611610344806117966331660636/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 - 152771995869732720211894041856645947141067651203706183627449201039051277487147983882368810184746564071193296280234052822186259039076884890388040/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 - 40271278030609779063764400337604730136484701654555643075445844571016571678943096426581375846369390027189815331280122970332626907678108370343303/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 - 1714956588472608008588094178897392873269581186618784048037710606648140289856148681989285463571707373403357422253594376529460662956486844033610/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y + 242963371943499782176626533931946588836927583096571741059943556842643986775762360257750866640088683876159786840279659239066754200198342201589/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

84312512453550741151315566839307516467860600791886651171929434930038608260440051766610469811326086842092464093199027663412022529747905133879361/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^37 - 200060040532129035926128709361957745465873346616842808127209321679395834125470866439606400086123076580317989356405459752547672521822040827212574/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^36 - 884406324241129218670583398423745453885429465705804062484458021513496537269540611098769495811612046990155957933803873198407437603633902944759824/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^35 - 6709081071201741678388845445547569876280770773122064456158963207774767604754549612400651759853405202761496912658384823992696187668779895670296268/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^34 + 8861821111370597538679126273670962513409621566666079420222259911859842059391850336642502631006729241059279495515220583991589064982574196983145689/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^33 + 64669661429061330609774549090816774913367680386291726885787683261267376205603085943615418438154221598248875398759418009054993673069544333985696427/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^32 + 207897330330565843736573371330404785149763295587121664482981770772043662530352190483571881795490833088021642792481328534786406676137751675656602900/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^31 - 773192223740291909804142210599782824697904331008984086220964390466147075250403466622473803004982422119252607620897210093536238643528628783918337628/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^30 - 991103687571189006488198432467798529775996886622450203397418044593860273687127559817760703154358021191535220128754747993181129509031499898157308803/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^29 + 3467112689912757615581755576608402473600276748970947719696176767295542825979372235777439637673807280649929339406058398683610598201190998443662196558/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^28 + 11352127328501873729847160939801626835089570408749700522915515625026609197131333866507361937396155875906477271935239201967850613778080262994087205254/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^27 + 26733908310844463137635537455940011303110658338694051756855436975076418548167640646217994613900191752932180319832740063873827318674462974808660428677/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^26 + 8092406284327357573775187347404681688077828213223238967486152634430913181638834856586123643253799847298456285523753883363274387287590763788097920256/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^25 + 5740417774628909034426682181345228764175484529019384118481619726045085566948789098777524970161554681301809848117518421212059551646208044096147378313/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^24 - 97859760867558981557763305011086696042028014342496478687041503110529360995638506752140464016018682667465794122977912730778094337186840723429942280453/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^23 - 356059515275364327312597885688940942942293333112455933401016986087801613899474695551654748305250174022061067147220487381350002489599629423457379759890/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^22 + 915519426997289843914044979215136663903166321992754078658892170944873457248353647825874437640941479392128482896081174950249831043665912170330500315/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^21 + 879846725126959690658528700253467228149513230405341532325866082262780361329786425505967244719769997106949684524536750289419661295846847222893063050412/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^20 + 633731384018430859260154213045047805426538433438450443554263174527244588323806341578297310969778606439045248375848055604458539037295140360275246835732/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^19 - 102874449648401643607039490854583762775035715478476470018597071215498665906627187307841171192373375192936962145251625254539386780734486298970481841566/335977260031094259822849942364674630319963799432926844012133242078008210190172359496089596252633971638994150765032859368103001510669882282193*y^18 - 1019394529422460035542150420515168586299092510794861156950643342642905817002265854464880340126189624102108887239059722660297328224757186209839669024610/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^17 + 609143020610658896355687182215666654527017538580613139040359794517095839383499976265071035925538527311388426655855439935065675814290150099922979213135/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^16 + 679621230443958767154326648411901200693199977165907289121516454189936364886513250839350127737444452085622098245816890355039061559834382317656372745890/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^15 + 181170220841142824736736972098907976053363621468005362799917339605933720087249395146301738017752187491950153141891080661442117739596805625643753612271/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^14 - 339723579642914720001483550032737780374334198370415911885592086901254079334051709132158781561044328167623765282991382570333679837998625558256147956816/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^13 - 247656155795211050307691052470185026525377418921835773061825982161346267183370952327003014180179572553387554768161335820644813634395304411178467558307/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^12 + 100604597450747896724696954642742069124956623744502068313802259473813669036186942532891609074145245315246876632888343840967530255696649691654695469177/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^11 + 70654345416998546219411670491393514654881502107247685048440989343839797875695429907958582304495561066799809791545852685116861680883372897452694368559/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^10 - 14685375087483243715260385714278127982325794862344768756227583255897119962813290477485452504179198633422084964629635457413671867125921904315526167948/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^9 - 3816302275250537929201516035190705391051874831455218344597959913500057109803563033623903234269645128594403225709729945775147353620878517904917126043/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^8 + 3914587805506419135384420082171576422547857811294820712411820574953850800138053212835341979376080748300739748217220228206365567172905094604840490083/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^7 - 1235399612145474622591816860344105184720045441116809884803532108513165977571075206694698613933078099172066668221194226989388052810219734538671946259/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^6 - 1377019452522145291453115237471125733868082141784225023991514856835809518937554223270940745830892493484668712239731491426823472426473534399041452499/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^5 + 7416278418296075558220853808300401277198666655041721965792643321406300165944826661377166785083848549523041884585793734963192684923065490058722817/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^4 + 157513664672177996549121006441015038016448128606085032302394981459561622348938762627272366945123262482150429074680740838318001108783497002476567723/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^3 + 30472465644943465906398839543067346471906377754021119230230367393922747886883062167073285731829936589610634213864373076327824080469890301402174238/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y^2 + 730377467563630682195966635891223081987250300971479817127529802679671686388720140497863842970901597071149400228911141405836652565410401800612066/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123*y - 132748661294184383797415916792472433398995191699167244207711857143283656996087058136462060311783781492169567871823578996770367691323670888481952/3695749860342036858051349366011420933519601793762195284133465662858090312091895954456985558778973688028935658415361453049133016617368705104123


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

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

# nu Gluing Vector
{1, 0, 1, 0, 1, 3, 3, 2}

# f Combinatorial flattening
{17, 18, 26, 4, 0, 5, -8, -25}

# f' Combinatorial flattening
{0, 0, -8, -8, 0, 0, 0, 0}

# 1 Loop Invariant
22732833272717655141553324332364360665726112319612960165417764096932155629789777837089631371683929545366538561012112842696457069866250951741562/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^37 - 53504300286234541572127584999924356594965836334249644342271493221902170688105882637731223663609827163722790869346133641378032643053744329716806/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^36 - 239523706410290675601232067838925557987039928854448295415377331165759615103722276044453320974061726315856379764742854692219282610863100299441796/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^35 - 1813699844292252402744940340832190224087550503984631483307569771788684862339822631249333141892160674585071630189709557131860515984514968214857747/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^34 + 2355457173096847593737309747656695700749874884370482561637310376659092538156480432951434285400447781971629001337236568976361571616285652465704114/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^33 + 17487209485980566262087449719849542066338363765887351584477870059242283983485640532946771401717918154828235917789342622385125132618666670335076289/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^32 + 56406022349157713243315231596836016593284199100505958358064732914996094085306530283845233144772359828544074145100191202369986206012629632205243351/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^31 - 207440630533888688511525378256782212749695288695480115599844946997996416854501652105228671546439387382188478311127205108335018186210129181257147600/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^30 - 271481896560907418642577028355344911045966016307218667412354853268817480697604026805006290521747356332459447420884496710399642718457907073996878236/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^29 + 929343869229932691545500122832149477952758872598887100655492221746652637428226634505142384803886727522093302016430381450046114729755330084395899177/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^28 + 3081268663373922186387446518723327430773534065842874702464651794060522708247099835309957393467958237186551561481891944593019146926085880877906105914/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^27 + 7268490781685246398556071959554781252901913397338125928816907151819642453522248438288269468791734241479291187143139241716274471324926887633923184401/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^26 + 2307491953458130961656547646849002723192321433451703884663683992679956419490415995191652633962370153790260191108862862218044656104676125571755011104/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^25 + 1549532714026318197695136208810490360767456739370999436380230169857192842053594988220632364985730592762312646350079469856436600091459993347285995137/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^24 - 26436964928218293873408018156044725324741800677947164443852303996681165661565802276270590167600394797368050070785040779207231434532759779333770320079/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^23 - 96545038551236150501668064837338788294484476977195361016411053070872821252687760235918938620160916795960302360267940488833934541086989383738337093640/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^22 - 1608282021932756981632280624738320768602827101656997713431230981382082570623060295686109649802582717115089263604289057973111736838629991018205809385/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^21 + 237613790705185825493633056528713962352868328705975153522593229575117633609146771718832525772681089322655882172603078586682937705789723414138332017984/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^20 + 176427994085930615754295171734859898375987923137176422226903824968201756939742242756051146419579727115878630489125547774878825148116821219910054170438/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^19 - 302046224797069304538970845956180564557652555043395296616550669845235295183479961980306948373592689452302977998306211261000382869104267554047232669448/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^18 - 283120924396770716941211742655440303025413526019036773237585655777373163249884705397335415398702718421484958458018754199352591652940540275228681095870/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^17 + 157621134494313645850163643920922568807028281390483317910130620075364701929802241920468605522968751364514864654407803993644162667526207833710362678473/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^16 + 189325697680139706008857811083345481679724181875653638620988272166682201758703098290040309299063754462409279078807895191464183775872566279691754758449/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^15 + 54416596824747272032067856815403236502678399896472542857168220909905194835559954866642945632303718955904078240106211554838186764243723662279701726623/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^14 - 92000287234793394816558781548231566888693162092130561457106485188988894564791886385310551318104145928170713490389701620630631035408857306794047458696/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^13 - 69702937067318251595979664503242022637118369830559395613917158520526610483967480979555930779232621980769312709847228030270379375649487457688299514637/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^12 + 25293387716885193687044514859141324603781954600426019938523789298845280008946297690456592616245591965075759731225360788515625765790071441281728551549/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^11 + 20234442532621891160675802603891518973811641566418983052775578994279073871638057140211279422789501283314773006234186799131868359632109467464734536870/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^10 - 3196368306741768662433293970567573755024965183965333952186621900272697766272018390025723156675087239531276939746153867246781217428746316721836227771/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^9 - 1301716747363689177645963386072061239304895672674852668598431969070100638736625365519824223310782021385645722411985777256580186008076108113028960282/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^8 + 999077868239747025885272757806508411589963078069547884074826569080313598841090609229613558497412872344627242524837274915868764383279752122801656542/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^7 - 287002883525743228359911939243619093251575659343574141609475102972708039662015733256683614036284295219902655603947465076609953775792573824520925882/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^6 - 389561843722954014151229935023136549554163081941334847398073242660400332182105233039433348866286852939072486608568422679371247832306519976857745521/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^5 - 11912757597131965485624468240203600815211366674620325800474550442317604659644058154259492991867958426273155165626326320258778166350941206816353400/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^4 + 45107721409166499610760891329410830618199032881995119802162738957943156995939949926191526902347612123141920508055062157828015310762305956508819268/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^3 + 10244158983167198885670866616045614746984096602478289443405769599538775733522900539649567066737774814028996870745631588987240121406295965197513080/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y^2 + 326632690133213184542510583029600045159453629057189111438573747796484626453468448882301001992645334216896172191051829132938194447796920053009843/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563*y - 47195904076402579874985063794701906168999626609819670771689744662950678573866163790909540267982206317963009487340825735784261066555778326641941/30543387275554023620259085669515875483633072675720622182921203825273473653652032681462690568421270148999468251366623578918454682788171116563

# 2 Loop Invariant
-15138775843283052975585254181861044414498646184174888019790963754923248376452679661323858710503443123466977140216823690463436240746516710887719298562870894992331316270171394909940050832814567930089584275422713820159453897196132218379110268284984312585947569539538673538685225/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^37 + 11100434703090020983545868218662007180163251308603039120857454693088068700228235957855890025564562803991186325577101900293800532257996743917285950297108671478229371292460905199341722131665926136735148222210381838923190561827017296118365590076437126942046242105593370776236553/30036099825027827571378203083240285996281658070814357615571080254817492575533280197941210551749459717728145340249347668346686942875448318116808821300701655049485572944492171966978200198530700847481512231830061282812372390650888462031553698470260364284654924389730584722466992*y^36 + 7550090155965997062626910261703557802930129364622307356255732629419847774164384424811488622082259880255323051161589630713802156212794852865717546696674339164432422511849779309955891368132485275791629604389741295470433257342066807818800082473562434484260979017348685113933991/4095831794321976487006118602260038999492953373292866947577874580202385351209083663355619620693108143326565273670365591138184583119379316106837566541004771143111669037885296177315209117981459206474751667976826538565323507816030244822484595245944595129725671507690534280336408*y^35 + 614617507630056773553400416505696562361497869281615483205991533132720712536912760825562074440914817884313637212958177138395198436068856932888759874499204544282370211206044054257743599873858368931002906151979237298670227767769759379860536350765699328758878624043133977560553285/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^34 - 116083312831984057153668186333329721102212951821859265934565005597524554791587861357579523132919681141429585075112414414318772154142209551488172953087802158136014620213181413544145728679390546473265696857844274570651079001840121625510517375857818967633425662217975105427982315/7509024956256956892844550770810071499070414517703589403892770063704373143883320049485302637937364929432036335062336917086671735718862079529202205325175413762371393236123042991744550049632675211870378057957515320703093097662722115507888424617565091071163731097432646180616748*y^33 - 498772664393982978360215322550822790195489418457079124983696242640020532815975663113803374841487499140175844543652028819622197422093700294734607477438976564662939774540444109022512564057799756101457519803215470948775288520303204158950011062717684316483675537605313356133144653/3754512478128478446422275385405035749535207258851794701946385031852186571941660024742651318968682464716018167531168458543335867859431039764601102662587706881185696618061521495872275024816337605935189028978757660351546548831361057753944212308782545535581865548716323090308374*y^32 - 4900116068189099813713059201088615375802465415668000425267158883139373314735083366582660063058759901022321944305896215675485088237530749942923425678464998406217364191139678396780189852817230414642678983444012472325098088653202277206809102698191830301164222198900404498406619775/11263537434385435339266826156215107248605621776555384105839155095556559715824980074227953956906047394148054502593505375630007603578293119293803307987763120643557089854184564487616825074449012817805567086936272981054639646494083173261832636926347636606745596646148969270925122*y^31 + 44382277223006585342532734545351828956453190474260397940405141612289654090601510371457887212776649831205589244044926764661295340753119581088273557887444776388903183845357371486121340955182852514677275051882849856459213905139554863910084943880245980063383959702153440575498456139/30036099825027827571378203083240285996281658070814357615571080254817492575533280197941210551749459717728145340249347668346686942875448318116808821300701655049485572944492171966978200198530700847481512231830061282812372390650888462031553698470260364284654924389730584722466992*y^30 + 34072014799684638408686313690760689825241622337744706642711086593519335475509536116947764766365648441704096416775728464604422533535134621317444167762126784386782721428893704294050788120775623275836561925096310358522267868555839445729707627628430214001404273615278404232130596265/15018049912513913785689101541620142998140829035407178807785540127408746287766640098970605275874729858864072670124673834173343471437724159058404410650350827524742786472246085983489100099265350423740756115915030641406186195325444231015776849235130182142327462194865292361233496*y^29 - 1140770359964600233095964914906644103950080781126585328646469667694315121893298034342634708486906153149131944006556724645400864926994987775068342676748720211247280488720530312073352832101001507723353794979910590535613985824564300023514230892453042479609972122320003673005492744/170659658096749020291921608427501624978873057220536122815744774175099389633711819306484150862212839305273553069598566297424357629974138171118231939208532130962986209911887340721467046582560800269781319499034439106888479492334593534270191468581024797071902979487105595014017*y^28 - 538803398948894216824380815609910212177965227223134620350415923721494330651655784747619528823663756313906120308462443793412016034847924042464230275879199428986009633165851807195668670872597897207251723977095053936724544377058804863383297453429362857949641660285140907436949330141/22527074868770870678533652312430214497211243553110768211678310191113119431649960148455907913812094788296109005187010751260015207156586238587606615975526241287114179708369128975233650148898025635611134173872545962109279292988166346523665273852695273213491193292297938541850244*y^27 - 5106731938366656453413433310953444495722314430785422854797936873565980908185737879252178829045713276199935031012749359983866228590907080013609144396832203917909280150196676418341506953062499852123078130967014959137945889632236844817672081419417357387163719051805626158248289161719/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^26 - 179511968238468635725722767228611347614356635275426832145800762738488704262243586553633215473151021509013069244402762210530041411972285097366899319496812073910786235452772520724545368593323595684582440648565957983419995875535019534602374481044647541604181400722390559985434512467/7509024956256956892844550770810071499070414517703589403892770063704373143883320049485302637937364929432036335062336917086671735718862079529202205325175413762371393236123042991744550049632675211870378057957515320703093097662722115507888424617565091071163731097432646180616748*y^25 - 487111591501543461043519943606103325266239335684253423327153024401818637750330994915302301851577065742155753784649122647669410363345628763732522408743349772410196385927348148071982311053549700688935361763672214165368622517652482393087928761507477584960519750395728869802466801503/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^24 + 8710107124312507454081169791443228664592068842317201457663400638589249043671637241536431552504972460467246517030834834200013214401821298449428009821564187233862942375175643653979911169111329324245578863039404912245579393341887922003120656945407076184124529773774358093639197151339/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^23 + 16771930206692793164842783089264088486945731483932697042022660146662501219539115555707359272359629664714621559688430500549470167650564398308035888024594303607403223012261990983403565146812392621171230377589656903822124470084470091339134059009469070725895382899428484032339952553935/22527074868770870678533652312430214497211243553110768211678310191113119431649960148455907913812094788296109005187010751260015207156586238587606615975526241287114179708369128975233650148898025635611134173872545962109279292988166346523665273852695273213491193292297938541850244*y^22 + 9642359979442809905770572083049139324881465762068070222491826147641607386591510056345432217639694919615900830422992552486713630058221317879220791718505530397069571290918414151883480518649177218556862999343264098020296401754946762933503979781816817982679195545995472517224519721355/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^21 - 54055318655006064966395015353993962587815827010423813264053357965779220304898793457703798296137647509012067685750586878388048712903906022103376750090711215372642253639416646687167720701465224467766042991770759014636236005794998205312120551964523133408293871350255241056503731968043/30036099825027827571378203083240285996281658070814357615571080254817492575533280197941210551749459717728145340249347668346686942875448318116808821300701655049485572944492171966978200198530700847481512231830061282812372390650888462031553698470260364284654924389730584722466992*y^20 - 139974091067979240826797742401632902208393600074120409453304784567553759672829016444777955834809785813365700208896497805327765252788155891925448898739988287425227733420213317334187254669441595337489076382670623642461676612576581875557895760657901586678309394435948821665042112515885/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^19 + 193857695025476816807810481972386910243100264334419373532839633030337217269355178923541305985403838837167817500557154465957904942395781953554613686595169018871953643456658025428596682019848186331946001225790149342970566615061000403989421962239429715898789043308157505207425541470583/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^18 + 74310727507284533778171331897349813229284658668358859810473540593758393947373643592836602953614016606552059386563960196288622557017278225451775224088979248578781797396541911127467939008740162666579221235274593181168577486017166454825093619072201703222711318350424268762902097513987/30036099825027827571378203083240285996281658070814357615571080254817492575533280197941210551749459717728145340249347668346686942875448318116808821300701655049485572944492171966978200198530700847481512231830061282812372390650888462031553698470260364284654924389730584722466992*y^17 - 23139253268978687344647193847791236777221654493598433940380490410724668756242989361399303200672217549215307046360279507347504856232148276428832599357925933992101042396261897603195353695284421904519887333685939912261722612907839489693570456172507090101989013907472345308733862660739/22527074868770870678533652312430214497211243553110768211678310191113119431649960148455907913812094788296109005187010751260015207156586238587606615975526241287114179708369128975233650148898025635611134173872545962109279292988166346523665273852695273213491193292297938541850244*y^16 - 74089394035522342895062728125578084246310426738730626626069199610359865378860509865630536961963737875888830537930748506602127555821351323052760457725636281311440690934814020235981304006472053398265349476034906143098877841420992622075875696395437459975470235526791349476974107849675/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^15 - 14876698780459452669832512701044126010515151295424685608438285812430869558453195137361150152568600772775676561958406412651030088903225842036094246769034312006890715126581926674592622997995437927991542867320665789977311755812270368049667596927034848081150644871047627356570812324869/30036099825027827571378203083240285996281658070814357615571080254817492575533280197941210551749459717728145340249347668346686942875448318116808821300701655049485572944492171966978200198530700847481512231830061282812372390650888462031553698470260364284654924389730584722466992*y^14 + 29861605034634518451922099390292859670472372586268356323677481621095776872308442687086438281584033760429857344371312280009252660352942307307912191827716368027515871754304484438104798850250014565148185548439512115188748141046175030810507754128836254984601374586323611131273392344053/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^13 + 28081670369413520891523412327261175042574368428126879753649609440338323665650285965819988460306595304173003134198932347384449280130770162101650236905529183424043250366310947234532960819029743199905574633304255926316566489472602610741298412102379154035616248061239528071430440268227/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^12 - 1306969873846788709749305169060465451752351966243964576807430189963553240378717031241728156599297898266743122379472171862359292557524341068056116699631542530938799919550346167599732404188129843884156217124164957598128468556204691218037658594428968975678751757345955569475545597053/8191663588643952974012237204520077998985906746585733895155749160404770702418167326711239241386216286653130547340731182276369166238758632213675133082009542286223338075770592354630418235962918412949503335953653077130647015632060489644969190491889190259451343015381068560672816*y^11 - 5733484970403225393896598794826837099314453992474721366515809291621889418201483473307696385846231690358297755231841245872029814786132170124304546057268010245078111382422951045213632250243295226025876445408850940160745351036581827221577947443968994387958365162626502637521836633377/30036099825027827571378203083240285996281658070814357615571080254817492575533280197941210551749459717728145340249347668346686942875448318116808821300701655049485572944492171966978200198530700847481512231830061282812372390650888462031553698470260364284654924389730584722466992*y^10 + 249598007064708488154051523617177084885933115518698499263277816817668508497090653056138922948881371703110695041628308101084482957310529005193590916986508441872599378431416846501750872440683429625476968670521333244833134711966959939625339410701611046020888391928876701005323662089/11263537434385435339266826156215107248605621776555384105839155095556559715824980074227953956906047394148054502593505375630007603578293119293803307987763120643557089854184564487616825074449012817805567086936272981054639646494083173261832636926347636606745596646148969270925122*y^9 + 422413799180236983060698131595266773617076781838340172552400133547448881634265260129642972557981151929497921710152495657430862151626242618433848136132506331023816417779538321428097509151435455204524894771091225851160654670052904714019845375574697176916967526508814085713624476089/30036099825027827571378203083240285996281658070814357615571080254817492575533280197941210551749459717728145340249347668346686942875448318116808821300701655049485572944492171966978200198530700847481512231830061282812372390650888462031553698470260364284654924389730584722466992*y^8 - 66692105842751769552063760892437505719660961871875558862986049757706312060664807548448522421337369974743291469652443245764866695049098688646191546486291515728469611175726903627523422110960449265944675739560796569463723630478498635509963181762373995019792330389251034167524103361/7509024956256956892844550770810071499070414517703589403892770063704373143883320049485302637937364929432036335062336917086671735718862079529202205325175413762371393236123042991744550049632675211870378057957515320703093097662722115507888424617565091071163731097432646180616748*y^7 + 156417604428179809827675604776064416236053674045853952371174391558295377992257933006647160549665087621618689614025294149484581101609837772177980571049175240696346637771584568093340303865590437733582980827359192485001013080917599074454866892072625152232676771890457337649489170043/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^6 + 156682737159258776214303948674690310043597260897543172690607044947602280740827140724287484252544402961102873444466055977524058246692037259347103603217287310357115136880284794157966933690025524901105804696808255226993030351951182141380488896079518258153322332774893563359393670311/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^5 + 9598707077559992027996142501282968909161898890077230208819184751567305069288696636257160279150592139458120048519052270973223630436499973902404554265380296383250013299189490202271947315835537120784079293821631278615679907376222016635314203220904209190528806695296791651954105035/45054149737541741357067304624860428994422487106221536423356620382226238863299920296911815827624189576592218010374021502520030414313172477175213231951052482574228359416738257950467300297796051271222268347745091924218558585976332693047330547705390546426982386584595877083700488*y^4 - 34182663282932941627344652671816086135483158382111536676286454794933586566633377340037806246560361110195777611908140182616712701754923302379055152596369401598896108327514049008359526881142150351654486586047981346111760077320032708060321893631875252873051608283092502909984981995/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^3 - 8223452130451794131967355725957616970598829822470861708817045730747819581148994758147677765972496177304582208567591418846916957758005266000618120326403447822864882819313284636071419385504340607000625675422309592734071965305080869157486720450823929675936603844960156204309430405/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y^2 - 495376082449025164709329398473299834030997260146698945366989322163727066257211544985987609030286554197561412398836420306918119327226483980785679219282738654709097611653197321961630755535186424281344030205983370048938281787531933809025513999008476141283906169111520471511414165/90108299475083482714134609249720857988844974212443072846713240764452477726599840593823631655248379153184436020748043005040060828626344954350426463902104965148456718833476515900934600595592102542444536695490183848437117171952665386094661095410781092853964773169191754167400976*y + 181364098181434559404367480272611726174060961947922142713518543993973821452631420481948799360872103102942403821446509348312533353897418536292464127343115556581492904335707109785739453720306277931088525855955351943143206820087828444464146457642568480896467868450991148601846669/5631768717192717669633413078107553624302810888277692052919577547778279857912490037113976978453023697074027251296752687815003801789146559646901653993881560321778544927092282243808412537224506408902783543468136490527319823247041586630916318463173818303372798323074484635462561

# 3 Loop Invariant
-4668329085815471766919787910389996714618338526114609038856360990834562726792544063316874772115575435093336783605090521849708013345299676521587016695205045500539936561620963749637427789283137476060111174619451990119917648563837800941084413360914260278302261083813631660253096375969227538090684438855214185394904751006710486317768209930162587/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^37 + 11991814185944273900259727502432128201435480426862810098344374585848764512207022179119498452914333292733385117378382425197557123036811188814418907376671669178737747598710402884150601103342929108487593929915089468543450039847766637989486319587743900863107643721477065111208730435445850873007947673190240373301299841361469676837860227410112257/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^36 + 44850997615193668100446830396404069609400820970800114071710964576167630865744254491216781659865984115299230990205594840384690615543971496564708837570409914026326580868987194671466070729264202821099810245382149685170320445087345786042234525484515221326839777217802452615353751623767000010593107360777437239722253540568931807982332588953919683/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^35 + 367526324638854222487181769349441296183370333263346358666433152290070222485116467198964017459582901338354184761283368484465442636028378737619564716799319933529685562655705247778746637037967311196045523349189751194935110957727724188784235143956855565003021103455206205446566503700832878647976413084634633846192992927913471150907347209476240177/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^34 - 545807851965404218647552987497683739981403443571417752918058868056927562369721967796365597801804264061442791451053190743744388386604725144066850222411451425383214844333463840988841080227869889877963943643582544367063214233367001881589059185060422317430806542815887691627460493203217813293551604219156788997658055179479344345968703444452023903/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^33 - 3339300705475301027120272043112002464877046756106232417931092700964673884344173612840368131229947146030892949964923500519764544917932466172199593921048480656335630967461460830472208259927594445265591824230130466653658624197795514393721603688495883027104453080199997309720525881639973563277481832569578275454440626835596241778482283586616497177/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^32 - 11092156411514557883092305949221430050129931705304000185795433342239102048975143764162916174297453176176844689056715269512256035260278116425670135025027615630699579340189003610562652906022692209061807557008727868720350700285693174097637301475813927047949133041906483818036413512835935567023865961872879741499401109396635885230815997005680625783/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^31 + 43707259151583177773604284721760893726235672115436693096981465773723441003108000915580389064210576872907938367352064656917907764720826229593116695107436668762127629822740004243446800638145966790070072905757956090008541968987912852831364922575741632511102977356628059508851036310746679740030931638278777749420420748772556196629788584271918191945/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^30 + 662820231407717738593576948394852018147522973285699968275087408067874628347130335946064518580854035230717151342640129315641834985358676728420956595748151055260014645487281283815039197729312420789952434186934917064189344097231743189368048040469628489174475169326380036784882739313360210063088397947279505278592371681773294153559641868628360725/14717252301121759009094600321383168327306183169267271689106930688679292438352051499202821741563495512999539844521219007542121428416378503315175954591776310522124929545054342823548518673911277854965133230013510004990957512146794960691662474941188514967344393703581466970278539571221309925008196377321124855050794188771756346890872697211736591*y^29 - 182603755515192332951212309559053126869820745982449940112885688633867786271103776976286841885202158333390830814591949397540169631463730800060504938810231758761747885779854272973188731045984967671653659273290090933882532558628779770394630639566070140042883717933686953994595576454837477924280731848850470061546290807709267623503884695663476735891/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^28 - 578208120789128562148371626495878992800280701253356638941364625371461407946734587400607895330379079083733256159254769785288159759016648114101076239685092378799427496443069848908341709641681246595965377208839332959364373921727109122746940655093252969555352305335091104922138155368679152109446573352616363372286382412630662087632044928808297150413/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^27 - 180692223796468992634623847608538673792492383670263976486993875145529553033209133369273785468775831942184735197822839829478997630634689048162098906163653043295492731509565190007767520307538909605455341135217906132164412042966757152881253981079793262810202886688320452413875789334153723294607511388284406242886636202835389140455515835071961215959/117738018408974072072756802571065346618449465354138173512855445509434339506816411993622573932507964103996318756169752060336971427331028026521407636734210484176999436360434742588388149391290222839721065840108080039927660097174359685533299799529508119738755149628651735762228316569770479400065571018568998840406353510174050775126981577693892728*y^26 - 375447364485045127626873011409211730966436335237486705429697667848289915981779536742689134145586713586778789568100095164289991690891735810324054464148689841476963542963620672460876975970753038584288572043311434454755197992020431630629404282553839022711860949297906001340388753603387059289475483266287733127143084518223530785794286461175412960573/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^25 - 363181854981266390333654761181674460252847698939900780382789364484170011061172147884603710972132343481125657464003792923778262326016001163269873257536289647878035873000009701478600677683533506382140986476602165319620077521824288140091736767166623007600977677821755834691724516704836634925740177779835772175732950706057388048705934945348499821817/470952073635896288291027210284261386473797861416552694051421782037737358027265647974490295730031856415985275024679008241347885709324112106085630546936841936707997745441738970353552597565160891358884263360432320159710640388697438742133199198118032478955020598514606943048913266279081917600262284074275995361625414040696203100507926310775570912*y^24 + 2787400791587929383588358782265036067851142870732627641756068821857145439542581345766517333889904465534819049362073179142635076268661240478462006115601925653054923094397481169641414483390248792092568179689932172997469156168015848002396072145325466362119812579222445308109748386843034188235860578739679633824591387961047529355186767041207384235699/470952073635896288291027210284261386473797861416552694051421782037737358027265647974490295730031856415985275024679008241347885709324112106085630546936841936707997745441738970353552597565160891358884263360432320159710640388697438742133199198118032478955020598514606943048913266279081917600262284074275995361625414040696203100507926310775570912*y^23 + 2315122919014384133383692561906866499159940695597767804871395174923412990825048488522586679706099423634583373473103013437774414036672584337601649916726114737818304819661418971049567133783919580786952371259880049628435644921636482168148672596006414231395763983002318038512235584713631121480487659433264880412047380168995147641230784572489003507175/117738018408974072072756802571065346618449465354138173512855445509434339506816411993622573932507964103996318756169752060336971427331028026521407636734210484176999436360434742588388149391290222839721065840108080039927660097174359685533299799529508119738755149628651735762228316569770479400065571018568998840406353510174050775126981577693892728*y^22 - 1576732152673466695372331237834548898951171058949621547316656038338707947256034013666859724509992351662704435376498306062666012058503917661762498057024965142099930158862219709754600645462010846788638650190920739222446407449244512264264199492684178163897316863485920817986372148723369181499075368108577454585719866823618990127620503338849403397087/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^21 - 41686619997460386695373887980127842489128988241055419917707330166522423907290620086514544781375405585337101596071719924408260548079172418965673660064230134001413371636729794019593455815772441456743910333129197416307888903918490746893985484322057338315143796913313719390206073829891737144260293833686438481553033202405397604152332185090874438588141/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^20 - 2676744012799310417439487851217155978141516340197500153482253251211330125550791372432880053538298132465932188244073924154613985119506028178061237731966006008788453192341267139903720972687398622222017283528414027393743433295926217875606532435578002884073415123872198055185636702907616496698575521170375014663291225984108514852850232037282999181465/85627649751981143325641310960774797540690520257555035282076687643224974186775572358998235587278519348360959095396183316608706492604384019288296463079425806674181408262134358246100472284574707519797138792805876392674661888854079771296945308748733177991821927002655807827075139323469439563684051649868362793022802552853855109183259329231921984*y^19 + 50582865122207404980568975706985176617045735964685165710337310329527678588767440234530013713136171574382382193369984217707063616032938342294049901864446956945652256801769471611000534939746436259259713451985449559653273220341138600861399083805704305242173786085861385133423878305362685833310414911471983650830600732972642815735342072065811277751397/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^18 + 19811783765565746457239200373776397548507044977151773857513623583886276569163799577996623210723946035297713732762182056102939669591246201936963558440940152908084055386133826787398846448012092870254539523561002719971159040834963465977092632193264525423683341624324338905823453309030995936865886374884649271473278208238589634344361469359016051525495/470952073635896288291027210284261386473797861416552694051421782037737358027265647974490295730031856415985275024679008241347885709324112106085630546936841936707997745441738970353552597565160891358884263360432320159710640388697438742133199198118032478955020598514606943048913266279081917600262284074275995361625414040696203100507926310775570912*y^17 - 7308445398729677185202058484449770170661045352571119183910613386773698727176785152655591707532090103038624056065053886501938061505382140553513905622696305748252269589796639460793145663528388926924073045604833004106547578492514066539398344349736915283717506921429831764154720259716636574169163612710027907948369937904715691003197574148051470382571/470952073635896288291027210284261386473797861416552694051421782037737358027265647974490295730031856415985275024679008241347885709324112106085630546936841936707997745441738970353552597565160891358884263360432320159710640388697438742133199198118032478955020598514606943048913266279081917600262284074275995361625414040696203100507926310775570912*y^16 - 22503196255830559331437576841613099824154447269484265044951404133589043197632217488028065121944750482924005760807142138239665619246004445767716283532245200534640674262079020291374782913837033354175963187716346869590989787291247300957121898950725955209124673428254749272507273294953886073660404763800245596770370201267632954872592413477455747450487/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^15 - 23524889420133253331599520387067728871853344416115397107117658404425562250553907411193775421839655010060484048798997079287558720009404018932604441110826143942224676582236127733411285289555569595464871804506709654863433147523127815611199910510288236901286699462417160339525143404635892128011950313711726652349845313783355001029434542157213985479085/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^14 + 14840409757094496035530901791467649484195054315917551354681137107565001794054579514082224223807470309061427286982100672506568487701650845478958656726457137167406154913103313343197690799348716416427179902873159712003311935229383078609356756508542107748519704046727322480684981611953935307756836302592456597745347943985235820272705549466472106478823/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^13 + 1295837611658818311500282350339381542907668577722217929451575084671216728350820005964248632825264690810943274064879659419232483251609756398657046414545230442523041673224992324645653401945235355176302847901351571433028476093492898093659533391993661816772347899800562779707760548320572918619705260342739678920702960676259369770154516940868775663757/117738018408974072072756802571065346618449465354138173512855445509434339506816411993622573932507964103996318756169752060336971427331028026521407636734210484176999436360434742588388149391290222839721065840108080039927660097174359685533299799529508119738755149628651735762228316569770479400065571018568998840406353510174050775126981577693892728*y^12 + 21451999148264569185187453057572538348715610542356707131867004946930320988419370106148814540250082889419640557402092024355616192065366960990296098795675681192299049064220275928292726350273658061387809434072059352470384703477247378097948874816979645586514449775413583440525311111312978885630841577975776912322469596708649898619455208353691687979/235476036817948144145513605142130693236898930708276347025710891018868679013632823987245147865015928207992637512339504120673942854662056053042815273468420968353998872720869485176776298782580445679442131680216160079855320194348719371066599599059016239477510299257303471524456633139540958800131142037137997680812707020348101550253963155387785456*y^11 - 324723975238506766668076352984113816501343262264534593018470022088625000758120916157246093443483201120880313875274779978875677693807299813729221744334075288288379605283140864492808863452545442622226758849027284271026970532322538660751734854282253490651446757655807868656407728007958978342145061019679102346200221008523042950749583850300186512581/235476036817948144145513605142130693236898930708276347025710891018868679013632823987245147865015928207992637512339504120673942854662056053042815273468420968353998872720869485176776298782580445679442131680216160079855320194348719371066599599059016239477510299257303471524456633139540958800131142037137997680812707020348101550253963155387785456*y^10 - 2139982530038344546801694927049187355312866431224511903302196608124544095180885595017404635537116991095511293351928602649187175100859525105168844115948044688872535297111294083768851876673447028447283275670774547591318363178477388861491884166226072209352735019559796049730436107951492140611660069622982401047645542640829893971224444293662977068935/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^9 + 36454660163364660934019999650691097379908169054179632658213170852926686470113559515567158940197172504748227213942851221312254168918674783485206288782045588973796228626053449685741640383949051156875028614132158795546465029667759524864498400916708502229474061766182149872199141815597680910935958380894126868924033840990783370975404550089591863439/235476036817948144145513605142130693236898930708276347025710891018868679013632823987245147865015928207992637512339504120673942854662056053042815273468420968353998872720869485176776298782580445679442131680216160079855320194348719371066599599059016239477510299257303471524456633139540958800131142037137997680812707020348101550253963155387785456*y^8 + 280236662097940142170236425218256062858781253591074097095017212030304934142184257937521219586235809455945249648627412324620359467716674607767018434375133074509815537651467454962469339176071879126313477873928265831946865657808525911148670912383196489702356800826174334897239924328731103886690123229929816647213792136851926588209934651851018285625/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^7 - 70422998924994323959921586443928797600949872016697043485359020100288084577419574591629568375397728431791303198267689587147692258830739590379879657703861272030277760991785304947854872858296923760294113938158927481880412787860637122279254820331066908957990391294483717267566850772669689670487123443610856952757658549782201383858498247057510884555/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^6 + 28717971752984862331549443873802597963431641016492367251687034562776400884304364285309737390034630978007631051241928810856001346029779494538659927596230391888972053768405250676455034694157980662677606989826043963295616298715756481607016783581643023987308995298623564146854294614015311413597195955004820990238231583636891385313436253706816431445/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^5 + 10983194705367049975482714858477265049848704540903066084386247494030421392162606164027233117023608630359840421033953734042537055093832142055754712176729250709107548485811797223703731390519227937908565570058167704954938653216010292857048160030094523619388744712931141562408497602486194942458941776179927526773941837655240863393892820480318091925/235476036817948144145513605142130693236898930708276347025710891018868679013632823987245147865015928207992637512339504120673942854662056053042815273468420968353998872720869485176776298782580445679442131680216160079855320194348719371066599599059016239477510299257303471524456633139540958800131142037137997680812707020348101550253963155387785456*y^4 - 3734847724734911906857438316087256586916001969956228423624420934451009822605687577783667679116340447495838487260253409317019006264293975633894677147418345884908194098328799240197458154544864503165690975914595878037066037933221515048895908965669986249957925382515402535959724656304253935115364797548057562986268525221462536634572950067625687491/941904147271792576582054420568522772947595722833105388102843564075474716054531295948980591460063712831970550049358016482695771418648224212171261093873683873415995490883477940707105195130321782717768526720864640319421280777394877484266398396236064957910041197029213886097826532558163835200524568148551990723250828081392406201015852621551141824*y^3 - 148425694367760307414423753901068361987004758248820903383754150256727901515021138271010988227489898883940624879423578905952911969753251588625364824132070188731913356674542535976064825369723510240331219349026834984159605330748477820806047642476745182063225132134400985716299523034109402049692747495036455698870128135052368207482806548370226161/21406912437995285831410327740193699385172630064388758820519171910806243546693893089749558896819629837090239773849045829152176623151096004822074115769856451668545352065533589561525118071143676879949284698201469098168665472213519942824236327187183294497955481750663951956768784830867359890921012912467090698255700638213463777295814832307980496*y^2 - 127806800111040038980291358735468867109248910399405613000418749596245295107008885452229245508779064800194880450006111191416100223484707385156629392229395537208374947373275218785278607039751513337988748655060142295203079985551527500199720083973705303684772957666462527175056141829693856209539759702660627482035456275602255455574898841693635911/235476036817948144145513605142130693236898930708276347025710891018868679013632823987245147865015928207992637512339504120673942854662056053042815273468420968353998872720869485176776298782580445679442131680216160079855320194348719371066599599059016239477510299257303471524456633139540958800131142037137997680812707020348101550253963155387785456*y + 23611719926431806489693870574104655108243786992381282074101040503987319795553836914609729244433192810952828092744565815348527347382848044615485596459364239317919935342556111684194044521156476572205925983002488893354958158008633248287783049728738966610659370275836339240169424180167952501436320697119365713721885668297820498608710032200734251/235476036817948144145513605142130693236898930708276347025710891018868679013632823987245147865015928207992637512339504120673942854662056053042815273468420968353998872720869485176776298782580445679442131680216160079855320194348719371066599599059016239477510299257303471524456633139540958800131142037137997680812707020348101550253963155387785456

# 4 Loop Invariant
1437585808994757318938238451869183299021387406078508450859276584258234099466363977070543641010252841831904365021693068999635527407449416023221190582052620975093441258003308347737668960262448925867279894802208412345573111974412213671135924359943778227535665910070642263201186387125643144775068665665180323595645223194355670409847316668739176650983472839837606626700993094470608981581853596344589137049013969550855206812574214386561422205462381643604036540410666930420779991303/8336342680019629110534361099414108743331603172821168278077465571091291962421334153759262935144848226954664938906557471564361467543526359396357977135258320696556065438908064818084589053694326703074001462960890456369168074849776082867794444019576039043437541645383015104498029353419234860896715955948898938207753302159660829818309144800170613181393992989528364039528531732656744428681360958811093242940676544293872918175826844623619021500549545829367982143174612226897740175801344*y^37 + 57788072060461560551679598770812951725881269522607604972539349884735551404113149406498775192270460537712471316106183525839299944598044765162227305856751000822761862150392394819570130158515068086447812934002666398409873896042360538312307500875499519649816134118817915490187392267696709836657135111529555454364041770233740016196055499497717077425410761876388907883789966130997896747915790179531704731007257981109571157557206519759966639120072750406938671062280499694680661597889/8336342680019629110534361099414108743331603172821168278077465571091291962421334153759262935144848226954664938906557471564361467543526359396357977135258320696556065438908064818084589053694326703074001462960890456369168074849776082867794444019576039043437541645383015104498029353419234860896715955948898938207753302159660829818309144800170613181393992989528364039528531732656744428681360958811093242940676544293872918175826844623619021500549545829367982143174612226897740175801344*y^36 - 1173424867075970576754295877623597341308445416406493645493682869644776598882555698782133152468979598723881882098414402880376788599593853579117878596537256760381800948872667900806187696942945714856677335259632555312442768702273602401095213180937614251077219092064725250974402625307088235797828993876828554131097043152786111857721289073974542551946558723076152886679358534241871742081429872372130672800904357048778966604116525520178895361707153492605847005021280098884947759459/63154111212269917504048190147076581388875781612281577864223224023418878503191925407267143448067032022383825294746647511851223238966108783305742251024684247701182313931121703167307492831017626538439405022430988305827030870074061233846927606208909386692708648828659205337106282980448748946187242090521961653089040167876218407714463218183110705919651462041881545754004028277702609308192128475841615476823307153741461501332021550178931981064769286586121076842231910809831364968192*y^35 - 641310403818764974318530708083142322674425795796682332496430480483086602756323247542905329476693604567938413991902799773217854160602709694893573291597530556168497425709800963023017424902840067510238880214745179264651073440959048245557176912500132279343521511307584476970363492741838431371521468759697742943179213240003417680651974456389809032360975396494124778625090708640293296833315887925002077242166398054726344445114649546170955388229840646156689888814069813881697530075813/6946952233349690925445300916178423952776335977350973565064554642576076635351111794799385779287373522462220782422131226303634556286271966163631647612715267247130054532423387348403824211411938919228334552467408713640973395708146735723162036682980032536197951371152512587081691127849362384080596629957415781839794418466384024848590954000142177651161660824606970032940443110547287023901134132342577702450563786911560765146522370519682517917124621524473318452645510189081450146501120*y^34 - 5968634650764888118165020210529157171099768574888832523247999562335286699200211522506408069709240048976379860338355051471687989963678429428160643058993059211017419124208494852014964961259463117188811642795320183958814084874847925686803873111500702201606997343251663865026878732358877365527748557171351334716772765489758613313549972381334319302839356029199404563957122273921851413901524484043214619548773644675814482558507957494224417316889992668112843513373367599977992107210799/10420428350024536388167951374267635929164503966026460347596831963864114953026667692199078668931060283693331173633196839455451834429407949245447471419072900870695081798635081022605736317117908378842501828701113070461460093562220103584743055024470048804296927056728768880622536691774043576120894944936123672759691627699576037272886431000213266476742491236910455049410664665820930535851701198513866553675845680367341147719783555779523776875686932286709977678968265283622175219751680*y^33 + 8887674813608807373308579294308219110140299697970981622662588752523057050898048980485638702200690787261827029494865663965026028018603146494397100362330236235760951769733659162701190026701896528149092843545015789595328821971680184519003144462082137740139151636523842100218769752893158589860099457147000825557511954778972057149730912896230830929939690410685917317842069177747341159020398699927162881246052596936883472168170456675395109484742133951894773798734752879751395590713377/10420428350024536388167951374267635929164503966026460347596831963864114953026667692199078668931060283693331173633196839455451834429407949245447471419072900870695081798635081022605736317117908378842501828701113070461460093562220103584743055024470048804296927056728768880622536691774043576120894944936123672759691627699576037272886431000213266476742491236910455049410664665820930535851701198513866553675845680367341147719783555779523776875686932286709977678968265283622175219751680*y^32 + 17030035542643744829541537774072531622024331365059087313601036340719580185865200610398519499620531966166044431766385185040180918007444580663528741635141882598063797790156347823143844077294680056532934030800694196493965414938953549112309256643612749918177061612506590168117797845276376355386955361111131233512747951814321011321072103741779537823183743236700280289863907638007812416753337848700718423824164148609945549651705514566747921400657180155679112012488055887522681881063691/2778780893339876370178120366471369581110534390940389426025821857030430654140444717919754311714949408984888312968852490521453822514508786465452659045086106898852021812969354939361529684564775567691333820986963485456389358283258694289264814673192013014479180548461005034832676451139744953632238651982966312735917767386553609939436381600056871060464664329842788013176177244218914809560453652937031080980225514764624306058608948207873007166849848609789327381058204075632580058600448*y^31 + 118215682742557751608221202872987637330490899296831458075099331605773257324339089482132971630428083600164942498328747082449284142233738657116434054806491347028332427190309995055612763539517143971841273348890958414709626331263063654241081329182253652218739192409933772859180278583344068713621913199137539688183954552969329910733078629811328051904589253013418969253329187649864312684274799244186900900608825188697545549208153926990936599072029099737027040731484787515463793504215671/6946952233349690925445300916178423952776335977350973565064554642576076635351111794799385779287373522462220782422131226303634556286271966163631647612715267247130054532423387348403824211411938919228334552467408713640973395708146735723162036682980032536197951371152512587081691127849362384080596629957415781839794418466384024848590954000142177651161660824606970032940443110547287023901134132342577702450563786911560765146522370519682517917124621524473318452645510189081450146501120*y^30 - 706424430184302539544138876551427051411510317779870821049168437082723592463853453988672736607688034558920116953717558863297177539771814585000711924257686104717294336781663765352939088143718319863743052469003779360377611176594812438331790152966915570685374464376009635134048725354748069374427342573511377716337021676012589300735796296438059808440772759870273429202453802877662299759809478514842445957497258217071574899429201396136198498465377190254017203924267501923117690975805831/10420428350024536388167951374267635929164503966026460347596831963864114953026667692199078668931060283693331173633196839455451834429407949245447471419072900870695081798635081022605736317117908378842501828701113070461460093562220103584743055024470048804296927056728768880622536691774043576120894944936123672759691627699576037272886431000213266476742491236910455049410664665820930535851701198513866553675845680367341147719783555779523776875686932286709977678968265283622175219751680*y^29 - 64648265462103264456247714128727806506822269354083093401380062929718750981451922720804412371016619602592545233540909226070020179421122255157695613194701524689652423861957673051823163972626175347422878425651809717790899116351301363316322113989808208850400736461408877694505603162354531722688431637545341998131515360957608012795949128661189935604524821716984149763913911916129547161911901406195983847465763241108615421101177636919401593074850042576419747270191192035536642319047995/757849334547239010048578281764918976666509379347378934370678688281026542038303104887205721376804384268605903536959770142214678867593305399668907012296210972414187767173460438007689913972211518461272860269171859669924370440888734806163131274506912640312503785943910464045275395765384987354246905086263539837068482014514620892573558618197328471035817544502578549048048339332431311698305541710099385721879685844897538015984258602147183772777231439033452922106782929717976379618304*y^28 + 13245966384951579821222043307306291145737851032692036657567985587004022428500224940020494269395950266798670019788699514997092969495517112038592560565761498919981826020285566918534158276175086271593393644641744679233077837735000765592852138999376351249218042434176930667420306869442221769841126714500002077333744034653440413272505438387621713003696597625723359274484113510967539930398673043505002835472470440252112225052734306806218228232184485307535398346232116574803255083590260119/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^27 + 22314875032021592294766240719153998423934977142234029579319486973479300513142316862587800910818990001746455800550119879128771825206720588812593840230047983805295749084756408774861588382679796824927575426108231948236725305981529177973727138638801948263893653791678088858426716253793326846524484019817579839633056322772250626401795324201647098022886340658525529821612256904734563221698956468512593101422347198057544592361651330143459206483282267322554995760192003222504574099126973119/20840856700049072776335902748535271858329007932052920695193663927728229906053335384398157337862120567386662347266393678910903668858815898490894942838145801741390163597270162045211472634235816757685003657402226140922920187124440207169486110048940097608593854113457537761245073383548087152241789889872247345519383255399152074545772862000426532953484982473820910098821329331641861071703402397027733107351691360734682295439567111559047553751373864573419955357936530567244350439503360*y^26 + 20259666480972498445361062227900920370023908231369214455151449217403361513867943467631433525845347162510728851598802646590643301818048688556202177760532994298457831183037369273022103364000909806537361315970557556016394489905670449716483238702915296095493296672160927441656748154593724329742814872863010742632904539839087359711453958299240246200686181571313176267182393760338585960734985074484913469993302908105799359886388809437135105328331778584098621724587930713673204834592808229/8336342680019629110534361099414108743331603172821168278077465571091291962421334153759262935144848226954664938906557471564361467543526359396357977135258320696556065438908064818084589053694326703074001462960890456369168074849776082867794444019576039043437541645383015104498029353419234860896715955948898938207753302159660829818309144800170613181393992989528364039528531732656744428681360958811093242940676544293872918175826844623619021500549545829367982143174612226897740175801344*y^25 + 19048006306795604169077424356863791356298883617497820312725979014199364688447476393541860886414188922793937029595933795053865985656649950200024404206478021121097156632097338647145688801240391676176189950708564255320185182811021527440042322046790359951159622841476356529950260889165785443075694245596796569912907452548152321934170843622415203858032353957940376777681756466298500168543741480725510624571923746785535631909160070693880150163219497070439179458742828173738183805577140657/20840856700049072776335902748535271858329007932052920695193663927728229906053335384398157337862120567386662347266393678910903668858815898490894942838145801741390163597270162045211472634235816757685003657402226140922920187124440207169486110048940097608593854113457537761245073383548087152241789889872247345519383255399152074545772862000426532953484982473820910098821329331641861071703402397027733107351691360734682295439567111559047553751373864573419955357936530567244350439503360*y^24 + 14160530979270449009388717117316799195317283812524505735740589673192855507174855979132428176404704129239355800206966771646189159308522614529634378480751914359293266723812935390235667990395430367764338036273438857060347521242268450319483517136570171780711918535977351303667875704839762134157685448192184082913837067055507756479258217362164248475058998621356330690534886148649797940072932938390728000845134779719314359762079786281657021558624568993215440841777076189775021860717154901/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^23 - 384679415788876403894822758217534255475426723907031480146013535719451962490786214222074296501093092463881946997806356103413208564341865328078974649185081566143006236670324184428603157294773228759573975528750272396876094461145282182562497490269082026662897180683539033688041156587502495797831690728511086382379175039126373474219249792688956056603553906070813144019113385245212139881344060755914943213517957413394277778490298615967498707498989598896187697241972373510222199680164434477/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^22 - 662153526476888337205586041836760646961723132628080668965272942875956737545029960658268536579129729471906691066493381742647475447712607870470323604337083202836631603358411712950242154003595641830220769586515888001203422580265354264901431343396562383230343992918335001829327831038904355606763064334783344890064719714068473053595393413459041331469830783085602311430689474725582541099074426614829840838249996981014523306128600800441707242552583398878201388887372937886441510126297378649/20840856700049072776335902748535271858329007932052920695193663927728229906053335384398157337862120567386662347266393678910903668858815898490894942838145801741390163597270162045211472634235816757685003657402226140922920187124440207169486110048940097608593854113457537761245073383548087152241789889872247345519383255399152074545772862000426532953484982473820910098821329331641861071703402397027733107351691360734682295439567111559047553751373864573419955357936530567244350439503360*y^21 - 2278583639796725492921105250865039928727592790333923666837574079156578959122063273427780002132907176165752724713409392167106723158718813970943204689447761155536833224600981368429438008797054748337323543476796059823229239550149497258825910396278377468187557014310946607535540169312178888807192491646338074826127122634634549499697527470873874931903010382191009655356855155464528150935434285503177423389773897793166590636839439281286948151462729625869651519275050039334707878695139223/2778780893339876370178120366471369581110534390940389426025821857030430654140444717919754311714949408984888312968852490521453822514508786465452659045086106898852021812969354939361529684564775567691333820986963485456389358283258694289264814673192013014479180548461005034832676451139744953632238651982966312735917767386553609939436381600056871060464664329842788013176177244218914809560453652937031080980225514764624306058608948207873007166849848609789327381058204075632580058600448*y^20 + 3258071336650898955534438508307378097516559266864027920696961587890343987763667100492151280794799992080452326832373759535399915429536208732988541239170505553945414371371778030845319298713666813009938296429882283949181628939344919186148243044964901233539812658208422111091766257384852622032054035799822194458813464018685260511876294349021863200458450082014796158421710583729144642484793353991086616590750303240216936312781802357078517848476578296338653704681478314028423425382907173021/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^19 + 2494628819284169155416643898867598428184109261353635086557692710886836680965553653415597056317947146786424751854195781098596620941064111820555925743519210374000073117424284380117433311522807377042082747156346699883154799964678258368747263700311838106880420610621377900826507964721268637016743020014812057404985017565310701479664313196530820216201004873231289092365818635291243352562360590533479322443273241991204385795693782959863538918881793796125673523763187671246728991589259616841/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^18 - 445193974228621802390580940401276347391712405023455808947703526296776477909621245410189705760380456324818626095750586134417701854918608566102386072717815251651567812634429526282598053087412899258136937612080733038945733568344451533512955302400267339341317900797241380077860263904436812571065224860342517598090350862487257583708972259260867566602689948561448969805418774742240355709448807200891654782213997893301307491570635771337001198596152035890715478477835385384213301798791817337/4631301488899793950296867277452282635184223984900649043376369761717384423567407863199590519524915681641480521614754150869089704190847977442421098408476844831420036354948924898935882807607959279485556368311605809093982263805431157148774691121986688357465300914101675058054460751899574922720397753304943854559862945644256016565727302666761451767441107216404646688626962073698191349267422754895051801633709191274373843431014913679788345278083081016315545635097006792720966764334080*y^17 - 673385523032079928219926909131069664463689288718474376416175976523639154916911208731024855016400647042351655094044151827301783815964984591413033407865969505619543002011400995794218938676209498216005688639465813393341214497874893972374097761057761572614744195857316233375514698737436035376724252231087704937925427468032087464742803644344056379554351858585752429675651818101217021850659278678353847582421681573579606729063916422775285706543691361565286121295232440253485165490595794689/6946952233349690925445300916178423952776335977350973565064554642576076635351111794799385779287373522462220782422131226303634556286271966163631647612715267247130054532423387348403824211411938919228334552467408713640973395708146735723162036682980032536197951371152512587081691127849362384080596629957415781839794418466384024848590954000142177651161660824606970032940443110547287023901134132342577702450563786911560765146522370519682517917124621524473318452645510189081450146501120*y^16 + 108121560429456599949849921381938693759989986114200260847712212835098059572435257724617090195952490596216761561386837310731577064135738476332027620276795258307582286146877308662466392384233856411853260021006627906164574198875333533381938235936169031745635025100879881345901419072248331767716871028016036969328055894383403343290290739303478008006953162173423055697382725393538990408598473604162710684025251233015470434284956573129882458623524411463742846437113349267234792195981022873/2315650744449896975148433638726141317592111992450324521688184880858692211783703931599795259762457840820740260807377075434544852095423988721210549204238422415710018177474462449467941403803979639742778184155802904546991131902715578574387345560993344178732650457050837529027230375949787461360198876652471927279931472822128008282863651333380725883720553608202323344313481036849095674633711377447525900816854595637186921715507456839894172639041540508157772817548503396360483382167040*y^15 + 677448836761803912230440746079201148608167366223452997955317641477072292418129365034520256240797654937611109535836586656431844344820763782842004091524442868200391350207797550929024052284780439011868794579608096675244058924644252002110754294052758915978634437449558978060659933822705521085356928774815283631272032833542688425534146809461574565302937703973360836039942313004805678762276277333899244606318919701878398966811571265380216293677882293905362787559285344065434203016900869537/10420428350024536388167951374267635929164503966026460347596831963864114953026667692199078668931060283693331173633196839455451834429407949245447471419072900870695081798635081022605736317117908378842501828701113070461460093562220103584743055024470048804296927056728768880622536691774043576120894944936123672759691627699576037272886431000213266476742491236910455049410664665820930535851701198513866553675845680367341147719783555779523776875686932286709977678968265283622175219751680*y^14 + 23771364503182219651702584065952996100235537788473828538045964940284034090290825441713651268061219500609948988582892137170685598366006601898654741569134079254626716664826395360584965450350039763289559223117258315127391674600850138860557911876986637930372136154359657106905030801130503135433009640108130463746612623044432093573835938981511092173458391723787074104761918784350372668805091389681673852645842030388948078127140211476884270023459552179307333125415249651767186130529963901/1157825372224948487574216819363070658796055996225162260844092440429346105891851965799897629881228920410370130403688537717272426047711994360605274602119211207855009088737231224733970701901989819871389092077901452273495565951357789287193672780496672089366325228525418764513615187974893730680099438326235963639965736411064004141431825666690362941860276804101161672156740518424547837316855688723762950408427297818593460857753728419947086319520770254078886408774251698180241691083520*y^13 - 15038559233357378405325550297047430515064484561735522266263599071059011169138347836215339502225979841483301468585476013730823350539180635657030656267662650016190022216017693228837497997670370221164648634363320846830215445026248904389924126367582266509896945950168215579291515558467115200800697625420127331708482120746961915444823135576877518036039306615014164689408362318110607167093308932825421067783520970696472333119894607163985795692209628151904113769825878274439265824131029615/521021417501226819408397568713381796458225198301323017379841598193205747651333384609953933446553014184666558681659841972772591721470397462272373570953645043534754089931754051130286815855895418942125091435055653523073004678111005179237152751223502440214846352836438444031126834588702178806044747246806183637984581384978801863644321550010663323837124561845522752470533233291046526792585059925693327683792284018367057385989177788976188843784346614335498883948413264181108760987584*y^12 - 23007179359772295447803986405822869402266791936687128542240484353167053375842704795904976707736347112647477344298440642829556722287451173118594409696538312813529854873311832256791552192462572306647736570279695300778603780254423128543325708704980740350249600033781070060914020772229955287444629125334352391632518196026920173781325544051044763503115041236415790589838353992350644344573320832417255853336934680858990998236532621532406799137750157381759995162219291742537272233127701873/947311668184048762560722852206148720833136724184223667963348360351283177547878881109007151721005480335757379421199712677768348584491631749586133765370263715517734708966825547509612392465264398076591075336464824587405463051110918507703914093133640800390629732429888080056594244706731234192808631357829424796335602518143276115716948272746660588794771930628223186310060424165539139622881927137624232152349607306121922519980323252683979715971539298791816152633478662147470474522880*y^11 + 285137689862981253629693252826655752321971755225211581294256659073554776623668826473088793548145367312619667446347096376122468941263682197800257408536724026866766327062924482775821629566805793099105781106323141789256955873885259217362849786521079132608848826231130426652960583792668629265480371243969783186354989683492619313290645655883275372975093372203625895659620824704997038124543436635978055579652388280263149397696231698167321665131312731253201103247559595457037383824748191009/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^10 + 16357003809692923206391903086260117528117506165887304614251833863429534059676037705041779728745705527643471699026584576037953068108060923888338412818931454702544158385742933730621076402395224776364340024201232337580472164035524513377616717963360796092661524933719787396315686472452363663110011757591973924204885208178395514663610402053749475852911326822525727686801303566529796020286904950129894452024087308338820648299667256111639308986805213788080129625901050217463063415019889259/2315650744449896975148433638726141317592111992450324521688184880858692211783703931599795259762457840820740260807377075434544852095423988721210549204238422415710018177474462449467941403803979639742778184155802904546991131902715578574387345560993344178732650457050837529027230375949787461360198876652471927279931472822128008282863651333380725883720553608202323344313481036849095674633711377447525900816854595637186921715507456839894172639041540508157772817548503396360483382167040*y^9 - 15042658044885360800984146367480111416208824956465092446732772537669863913944045855280200956427937871425500470684583362495877615552170443041694745303567906262195425518496110748685182368445268932065694933858680190456099851570516634360331958952278858588945407290499773499881620287939206350308555973743336829755191963026478592863474423278190598442511634800235205578850016134794970545300923581799755788168072144580014869895918985309758023710961283873765048405563900791410646552801398813/20840856700049072776335902748535271858329007932052920695193663927728229906053335384398157337862120567386662347266393678910903668858815898490894942838145801741390163597270162045211472634235816757685003657402226140922920187124440207169486110048940097608593854113457537761245073383548087152241789889872247345519383255399152074545772862000426532953484982473820910098821329331641861071703402397027733107351691360734682295439567111559047553751373864573419955357936530567244350439503360*y^8 - 8538524356530770530137857669798677070244193856837879622055433936565053025751076730103143868549576575117662836938437398569028068054935415122691179100982847191338150492119201558133156914660392665392001672950888647525029897293847619722574316232556568959377883929802871924226487953377281822703289630119556238414657906886704060433833508889278794744623879174467030156599794876822400074137161616351590162751189951973393083386373134404099760950395907673257951581127103871924467584114698173/20840856700049072776335902748535271858329007932052920695193663927728229906053335384398157337862120567386662347266393678910903668858815898490894942838145801741390163597270162045211472634235816757685003657402226140922920187124440207169486110048940097608593854113457537761245073383548087152241789889872247345519383255399152074545772862000426532953484982473820910098821329331641861071703402397027733107351691360734682295439567111559047553751373864573419955357936530567244350439503360*y^7 + 12693267460741573853266924923935301796565023101890114610970501414044013642795927489792719816059775942841582816258786013986853915079409792781932429100049624919180114576316079197981117778933235835366429248744536490125156877680285409908060636992251131094596139460987461279875556598137591424740840167064719456539143572436925072002881842109863804243159546423507742313793269360571488207840919821166708806486577483658394509173400196489440325872722131615843851842370859120186487555901009839/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^6 - 1942041943642867755001631837283612632134344964816005591337097613035577533809608082777089866160732839048964493413004164342902632470775071639753519101111117148762153520689517900427487374989732519959854454050569222758824294510534414798607117220256352402217895980255121973683860914925635752792148300574634685420677369372522209814999285892200509721283496089204576479741685562424140268252886227452046837786750852921883092643023886915761028489842870385004802128489687660278007220893800803/20840856700049072776335902748535271858329007932052920695193663927728229906053335384398157337862120567386662347266393678910903668858815898490894942838145801741390163597270162045211472634235816757685003657402226140922920187124440207169486110048940097608593854113457537761245073383548087152241789889872247345519383255399152074545772862000426532953484982473820910098821329331641861071703402397027733107351691360734682295439567111559047553751373864573419955357936530567244350439503360*y^5 - 878187018518109370864723161212405361144592463555531828238003854143069382672954282663769781848370533351217526918586092221379776231779583006633883557093882742267092920702390806211650005098993206930289334181807284343527105089718651805031511829465478967841711465086731640068684580494733516927758084384833001938597694310918225798360516754197332372771523687995859870083167094976182974519799206182792000969446133438371647657365254150889927171890399512530069091268517687166354916196130497/6946952233349690925445300916178423952776335977350973565064554642576076635351111794799385779287373522462220782422131226303634556286271966163631647612715267247130054532423387348403824211411938919228334552467408713640973395708146735723162036682980032536197951371152512587081691127849362384080596629957415781839794418466384024848590954000142177651161660824606970032940443110547287023901134132342577702450563786911560765146522370519682517917124621524473318452645510189081450146501120*y^4 - 158502457859323766731306690969061797743658841818441223776572208899229828581733412713612536212055733264561972166935176330983063796299173941300361254714251519502693230427604883906629809142658275732995162293158874449990872972560434589122155966910150449999625669763952419031681711149271072877151168210945952519722776231068830788420358840285916850893085520386895047471586367294888997381708598048822399954840516749470160121190114599693442051272807711472234364478053443252698188887818113/13893904466699381850890601832356847905552671954701947130129109285152153270702223589598771558574747044924441564844262452607269112572543932327263295225430534494260109064846774696807648422823877838456669104934817427281946791416293471446324073365960065072395902742305025174163382255698724768161193259914831563679588836932768049697181908000284355302323321649213940065880886221094574047802268264685155404901127573823121530293044741039365035834249243048946636905291020378162900293002240*y^3 + 549138449309126654825110978764019117412835406540159396045113932095021395603510743853776233925444962185028140167378103560919025518312820549417508670720613152512631788031674884534585346326858026300420639291497566027029261277441739594016386733552879609516602280734368519473475097410179045367155372042116361791388437218606821906823883809747209672860457851402078219880745866906809540510716027289609586838225030858404546365884758731998799374390304621145119283813511093351326744888715579/41681713400098145552671805497070543716658015864105841390387327855456459812106670768796314675724241134773324694532787357821807337717631796981789885676291603482780327194540324090422945268471633515370007314804452281845840374248880414338972220097880195217187708226915075522490146767096174304483579779744494691038766510798304149091545724000853065906969964947641820197642658663283722143406804794055466214703382721469364590879134223118095107502747729146839910715873061134488700879006720*y^2 + 14993734255110074966474883037602698789770621115506197463561192159124895480489579430744679603100914005029689893795651417798528472881372495544758887634726206471765543970434233127504669984403862770684846617815485688276247962079243432482040858581856472415732165591441564589923319214328764127529563948350058486983332293593012966989491217067524880057818677335712268809897035951980155322421845028320567277833651539192976297513969601913977206074274316769379401170724731072842222152368643/3473476116674845462722650458089211976388167988675486782532277321288038317675555897399692889643686761231110391211065613151817278143135983081815823806357633623565027266211693674201912105705969459614167276233704356820486697854073367861581018341490016268098975685576256293540845563924681192040298314978707890919897209233192012424295477000071088825580830412303485016470221555273643511950567066171288851225281893455780382573261185259841258958562310762236659226322755094540725073250560*y + 4056598737498425402105398261118063116366413666191792975187334419820803064755174369564020682758452705894517338144756798032032029468871409260477133324990256902660298241866257981496709355675391290728648133503703571046472980295738409161395219256924921555788760606765677600928484698557613528937931478097210543886792006276042984321879780889797194469226068682270565011491926129147087552748251325517416448810285522196339677399428247226901858251890706912811444382930207688117192240312607/10420428350024536388167951374267635929164503966026460347596831963864114953026667692199078668931060283693331173633196839455451834429407949245447471419072900870695081798635081022605736317117908378842501828701113070461460093562220103584743055024470048804296927056728768880622536691774043576120894944936123672759691627699576037272886431000213266476742491236910455049410664665820930535851701198513866553675845680367341147719783555779523776875686932286709977678968265283622175219751680