# Manifold: Census Knot K8_196

# Number of Tetrahedra: 8

# Number Field
x^30 + 11*x^29 + 51*x^28 - 6*x^27 - 1150*x^26 - 4873*x^25 - 3770*x^24 + 32692*x^23 + 100164*x^22 + 10331*x^21 - 378579*x^20 - 405574*x^19 + 675605*x^18 + 1276526*x^17 - 633534*x^16 - 2220454*x^15 + 147128*x^14 + 2581033*x^13 + 409934*x^12 - 2138697*x^11 - 605443*x^10 + 1286529*x^9 + 433453*x^8 - 556235*x^7 - 182742*x^6 + 167382*x^5 + 42347*x^4 - 31930*x^3 - 3827*x^2 + 2944*x - 128 

# Approximate Field Generator
-0.773416426974065 + 0.722889679773770*I

# Shape Parameters
131138618536711089906411729380801325118239205615952072425097980217431/1846592328193813903809808377978928664615452007992386909207590229178883*y^29 + 1541022414656541224394752464354239691395100067844793196896526986592941/1846592328193813903809808377978928664615452007992386909207590229178883*y^28 + 7841541175758026591678040919612015365059308662941294694625328988693468/1846592328193813903809808377978928664615452007992386909207590229178883*y^27 + 5053562283364944509334145433588483087956429976590201756381756430269033/1846592328193813903809808377978928664615452007992386909207590229178883*y^26 - 147281315567608950173348128047001051139972644159090581423800052695533049/1846592328193813903809808377978928664615452007992386909207590229178883*y^25 - 57689401905689432152746674386315348710740820727552574543495817038221562/142045563707216454139216029075302204970419385230183608400583863782991*y^24 - 81022784320886719160189642700868326045458322312484032399270795365720076/142045563707216454139216029075302204970419385230183608400583863782991*y^23 + 3521648128950271898789957804849994230657287820436051361912314081163821984/1846592328193813903809808377978928664615452007992386909207590229178883*y^22 + 15826482450183042363793213053882139573150178151219150810272929633851034363/1846592328193813903809808377978928664615452007992386909207590229178883*y^21 + 13154195515230806700210369771701750881339130879688876170215358212648452687/1846592328193813903809808377978928664615452007992386909207590229178883*y^20 - 3100998005278588796234971830528004876837230801347281003442772891085813511/142045563707216454139216029075302204970419385230183608400583863782991*y^19 - 6473373441135187166204671227221721707493390206275806396190886743588318242/142045563707216454139216029075302204970419385230183608400583863782991*y^18 + 26378847052359788989661445729155497176687781237167314320744847762837383330/1846592328193813903809808377978928664615452007992386909207590229178883*y^17 + 190478650876978109370882560918850651899663650141344262772131426504034814183/1846592328193813903809808377978928664615452007992386909207590229178883*y^16 + 60637918927722737290544787734845217859798099695393058619960399286195940241/1846592328193813903809808377978928664615452007992386909207590229178883*y^15 - 251848391646314272872103169028461410194105694662182349951271825762905441743/1846592328193813903809808377978928664615452007992386909207590229178883*y^14 - 174824500991334838415638424256366744985668877565371987177352298359500893099/1846592328193813903809808377978928664615452007992386909207590229178883*y^13 + 213759997965619816089606894772690784918090769049126874517927198926411051676/1846592328193813903809808377978928664615452007992386909207590229178883*y^12 + 17189011802468999104284714706913790444673780920125439289637404500614980060/142045563707216454139216029075302204970419385230183608400583863782991*y^11 - 116316302645694158613506086064957624524541311412293115114586605717303518546/1846592328193813903809808377978928664615452007992386909207590229178883*y^10 - 176462791575324350121118311525809326932392548436467448341261177392551816468/1846592328193813903809808377978928664615452007992386909207590229178883*y^9 + 36369769432563234798186424206083264116723924789648718983355146549403368641/1846592328193813903809808377978928664615452007992386909207590229178883*y^8 + 90788164005441633259672186026779841173734222269033183924128681276854371450/1846592328193813903809808377978928664615452007992386909207590229178883*y^7 - 3457297897315400934984737825525081940368290932815117152864088728946393285/1846592328193813903809808377978928664615452007992386909207590229178883*y^6 - 29479784140366596857755874036407977882998222510099940990653609991378962505/1846592328193813903809808377978928664615452007992386909207590229178883*y^5 - 1166871180369922416829815062666367316859513841256908884498178850096876782/1846592328193813903809808377978928664615452007992386909207590229178883*y^4 + 5441766667394301818635370842954873300503159290319280281211244029848084784/1846592328193813903809808377978928664615452007992386909207590229178883*y^3 + 211940978088070048376007515567224656257653447421383283354872753321669164/1846592328193813903809808377978928664615452007992386909207590229178883*y^2 - 441042203424162284582108906961109855644259764995543050553239055805569908/1846592328193813903809808377978928664615452007992386909207590229178883*y + 19896235162636285788422582043636519465362811470309312998050222556944542/1846592328193813903809808377978928664615452007992386909207590229178883

17093010445110787755910176336125156628306473386519662355408271884518515/59090954502202044921913868095325717267694464255756381094642887333724256*y^29 + 183972352269656500819811198375457057377338230388135151114582230205056971/59090954502202044921913868095325717267694464255756381094642887333724256*y^28 + 822988708015291611227205663261081024765483742633399831064222364972372839/59090954502202044921913868095325717267694464255756381094642887333724256*y^27 - 89614918473586108742832736073497388032540965633197307743371320408766649/14772738625550511230478467023831429316923616063939095273660721833431064*y^26 - 9941793376871144891629597824019998310515072205265123165089035315843301531/29545477251101022460956934047662858633847232127878190547321443666862128*y^25 - 6061352067042004445336009955354238795724163629126376623074126961206433427/4545458038630926532454912930409670559053420327365875468818683641055712*y^24 - 384502701929488037010778963730512276008592151902474602103242243093984655/568182254828865816556864116301208819881677540920734433602335455131964*y^23 + 74759357970808504654833112013618493077445966518807943863738438939312187319/7386369312775255615239233511915714658461808031969547636830360916715532*y^22 + 403345561178498884569130789649750926628498545686288589732513399210325591957/14772738625550511230478467023831429316923616063939095273660721833431064*y^21 - 341845436944941796952257671795452200804878128261559797384712282948992982839/59090954502202044921913868095325717267694464255756381094642887333724256*y^20 - 539950051415420614991232332574992784781579751770145906487926485771730229655/4545458038630926532454912930409670559053420327365875468818683641055712*y^19 - 13990099063344881671378952502718882798949402589847805644368947772683273848/142045563707216454139216029075302204970419385230183608400583863782991*y^18 + 14481022493470290004041988425963732901931173524130140546368124690254888019507/59090954502202044921913868095325717267694464255756381094642887333724256*y^17 + 5443970029662300042065510036844300571825612559522850348900243851683923141923/14772738625550511230478467023831429316923616063939095273660721833431064*y^16 - 8422015098821612326111292717484256927254251066902236752070379842991247426807/29545477251101022460956934047662858633847232127878190547321443666862128*y^15 - 20741632196547447147163755091508308006150405448611068056633098948487135061535/29545477251101022460956934047662858633847232127878190547321443666862128*y^14 + 2392244778070399197420146521922046021650398808701368021770528097665255066571/14772738625550511230478467023831429316923616063939095273660721833431064*y^13 + 51580791957136850448057516899057489963347920333433873686501840512857231666939/59090954502202044921913868095325717267694464255756381094642887333724256*y^12 + 41273810792406488147889554346895878932843337888116303357105099442342518313/1136364509657731633113728232602417639763355081841468867204670910263928*y^11 - 45057635421384074896244867725327785393896348659496771216114403057159765986783/59090954502202044921913868095325717267694464255756381094642887333724256*y^10 - 8836118555605692779291626346583137110856323510116424437467629219054064464387/59090954502202044921913868095325717267694464255756381094642887333724256*y^9 + 28165281196513826294923380433784413676565348475896287367741764700595101533349/59090954502202044921913868095325717267694464255756381094642887333724256*y^8 + 7844402395686590563192205100100370598011975667447891787299966580708675424145/59090954502202044921913868095325717267694464255756381094642887333724256*y^7 - 12427378499549472427888909437129285733604412737869357017985471776955747441919/59090954502202044921913868095325717267694464255756381094642887333724256*y^6 - 117989256667148821012876970239848535368957618327949547221189431598536516170/1846592328193813903809808377978928664615452007992386909207590229178883*y^5 + 1855970135470424885130621308280173553935616848118530803977907459847874408899/29545477251101022460956934047662858633847232127878190547321443666862128*y^4 + 989166055851609411012025722525389843577329615442208749223971455081419419757/59090954502202044921913868095325717267694464255756381094642887333724256*y^3 - 42498599417973619724120227572905285835750982722088878116515355000424354859/3693184656387627807619616755957857329230904015984773818415180458357766*y^2 - 110210633663926730606440441404011999530957019686282082831470541905222130573/59090954502202044921913868095325717267694464255756381094642887333724256*y + 29520990011720660564250277837193916056116774894677311883540925424775996425/29545477251101022460956934047662858633847232127878190547321443666862128

893565753909701141158629571263708759293939003431731632101862100217710/1846592328193813903809808377978928664615452007992386909207590229178883*y^29 + 10353909522022574729728491375160761052771957027457180035424095995781473/1846592328193813903809808377978928664615452007992386909207590229178883*y^28 + 51644738657443172535838940608688026432562679423322790080434308236237659/1846592328193813903809808377978928664615452007992386909207590229178883*y^27 + 24887479785277418835636348016203807457558511397883065627967196764839817/1846592328193813903809808377978928664615452007992386909207590229178883*y^26 - 1013354066071674740196754610128715501620877805038298439150690186827022913/1846592328193813903809808377978928664615452007992386909207590229178883*y^25 - 380727483712721348421463536404783063961182518890887974225601159747426424/142045563707216454139216029075302204970419385230183608400583863782991*y^24 - 482107346484629638731448334182476294617113968536234138669519752672572318/142045563707216454139216029075302204970419385230183608400583863782991*y^23 + 25567164464150089070689519423077282956038117271906934653896966642604762333/1846592328193813903809808377978928664615452007992386909207590229178883*y^22 + 104553420082616197209162834719799613927827220607243008605940023625681538604/1846592328193813903809808377978928664615452007992386909207590229178883*y^21 + 70427503709446531804775807863495239770294547930886246844068350635868505099/1846592328193813903809808377978928664615452007992386909207590229178883*y^20 - 22895465338420161622345870265046947269491389725381430474610274022289034668/142045563707216454139216029075302204970419385230183608400583863782991*y^19 - 41347031672507397159924012540487108817759177039368383148049196126918249679/142045563707216454139216029075302204970419385230183608400583863782991*y^18 + 290241285121724235825240615920967030282346607303427977103477765481937623850/1846592328193813903809808377978928664615452007992386909207590229178883*y^17 + 1314208043430877738274550851097070290966393780862299839754348254197426955355/1846592328193813903809808377978928664615452007992386909207590229178883*y^16 + 202714256267385821377086365597876767872583090227848039306472520089929190452/1846592328193813903809808377978928664615452007992386909207590229178883*y^15 - 1873039100234568138815154296832092512317592640560905365027763747700049596550/1846592328193813903809808377978928664615452007992386909207590229178883*y^14 - 967181530456652625982100378795032585364670622512549887302742065644416596162/1846592328193813903809808377978928664615452007992386909207590229178883*y^13 + 1750244117817012530327676326010920846551412443858537512211502796793272078596/1846592328193813903809808377978928664615452007992386909207590229178883*y^12 + 107401593505949522672812549081061903022529782522618527440268151722970240128/142045563707216454139216029075302204970419385230183608400583863782991*y^11 - 1103083565201177377469323171017519801696990507117170732974474767234904979982/1846592328193813903809808377978928664615452007992386909207590229178883*y^10 - 1193135600056966411336455187985473938227186960689013425776236764312229824665/1846592328193813903809808377978928664615452007992386909207590229178883*y^9 + 457447951991092490378186041371088585785974832090667095620450850153270719909/1846592328193813903809808377978928664615452007992386909207590229178883*y^8 + 659900705423860729475729162926137826250639523637938166561970103514736527767/1846592328193813903809808377978928664615452007992386909207590229178883*y^7 - 113861094837246169578553560941645824383856046727499856832242726169704898834/1846592328193813903809808377978928664615452007992386909207590229178883*y^6 - 232256564448469071689355344846126150760264890898785174826810013543027496114/1846592328193813903809808377978928664615452007992386909207590229178883*y^5 + 14742932504778450612034613988178018784569191910859094641759256251537873448/1846592328193813903809808377978928664615452007992386909207590229178883*y^4 + 47143942485610696590475589496960716567026141906900028699951736223682051807/1846592328193813903809808377978928664615452007992386909207590229178883*y^3 - 1227854588619080676572368360662065660442897351817286481317919569806624638/1846592328193813903809808377978928664615452007992386909207590229178883*y^2 - 4228011344053409657017587825038049570730890028954853017713382293647996757/1846592328193813903809808377978928664615452007992386909207590229178883*y + 198375923972286236580721800590997291871415930072933306250247816489905536/1846592328193813903809808377978928664615452007992386909207590229178883

2517943052595551111059312285608676422212026525790975126207670370210989364264405/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^29 + 28921007062418130471174479686865346842478697904314867732145472398200163577476033/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^28 + 35637521652029234123259351319525043249160440779112530236669188367179953986394790/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^27 + 54995314077199015500385605468254296395964001266086263423807427772028624398515687/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^26 - 2865354083609449969315308601321448126123615766929935144746243434043481670796823285/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^25 - 262789493588319788776291632193448433402019230838843534633755443681277289345202275/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^24 - 623953782733383923956195253069992541985199693369793614284891715528977662954061373/183986578609266013592300754798095296225347469268030090586483009241453494213338*y^23 + 37050883923294209555570636938252085654308641078373107562740830047589916036528803389/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^22 + 72028113183901483802506535261049977694507348229871475143980933452290080369904979790/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^21 + 168616224353103436019294475029154251889713789044268170742485648809673683473754217897/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^20 - 66541975520710574678551021223587807671340012615031015834767736731228021410945134845/367973157218532027184601509596190592450694938536060181172966018482906988426676*y^19 - 111087866770671500090605304556304083952299056631879414606379093147149343550451958091/367973157218532027184601509596190592450694938536060181172966018482906988426676*y^18 + 243171931803001959095231460322861101730699470520604965860719678542128992624552563412/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^17 + 917802348012754921328075167625659372343404936255833686922815097737788714722995856692/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^16 + 122213693388634555612281370142969875810441112963115685340523508960272113085007672711/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^15 - 1352879489295420254785057567937850720077213864345856197740736763363051355280065409638/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^14 - 582526133681077092028315255692331327918915311784437724160055336852417764292295432236/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^13 + 5255481393908825801922062320901969451040247778702769263385670961419886143743170919541/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^12 + 70064128205866111331518561486275455783495536446439661176234865002713219972028401119/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^11 - 1742024406023553507432550947992884045007615018693294722244004424166117469213495839261/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^10 - 3245302350799276018846378091706796984185254159625765686926555622296077581123442520045/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^9 + 778251525613587414507374179306731506641226590430624840848764705833408246311208553461/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^8 + 1853565431397935821727273629255056269804288281384290291605318289791538790027753959023/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^7 - 440421688612722655997042809478814628730100963940851529666653317746788804188750471619/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^6 - 672586633962481678551638977757178632083849344105957714036336294864978072547815239565/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^5 + 72229170990343854433559716397176692277990435555318784765875700722589861232746449237/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^4 + 140632686473090756347466251593037145649847759830867971104983632617826593718197657925/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^3 - 6963785173473877494614405543260035408520577678645983341057440517345820790498794293/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^2 - 3227121420056067714223755175345861552831548879836990158955366501329323526465719925/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y + 153371355676219934475108048241332723567928181108296765964106225848277570285592672/1195912760960229088349954906187619425464758550242195588812139560069447712386697

-2248692526052181607808813973627723198473914778660513639059416813226068253748325/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^29 - 12941193993491504641879185667482828591322550619677293079853399106512545178078294/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^28 - 256209565648014011779060346543027365658101432184470928278324845238833500679345057/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^27 - 54169071757714450958785239363887810982773712168932262989138704931800423670216493/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^26 + 5096173948934260285171227762655732138906909802714101901185883939885870935076182729/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^25 + 471633140324535863669441661741119755096524172219182782278555088862177882041180783/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^24 + 1152135676804995524697668050386091341254508253195473747246115665277179873859459507/183986578609266013592300754798095296225347469268030090586483009241453494213338*y^23 - 32457564908060492418844775066803195798155433847657584834246956764196276553596316064/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^22 - 128921257110935793003502226494423513775774694726606874396419447676192770006698824873/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^21 - 80829758063818228444147844678860324171926549621723580908923423459285925910115450565/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^20 + 57724809395899844625887653514297119436885083190683591111871669308726060528184072977/183986578609266013592300754798095296225347469268030090586483009241453494213338*y^19 + 199622228220839002593506769926970935328774445679923691672458971602074284836100322065/367973157218532027184601509596190592450694938536060181172966018482906988426676*y^18 - 785983384626616796263844129624046948322313989295547202286746220981651455243465552229/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^17 - 3215639035845069376870390884141803628037147399239338883077477275234732550616525925937/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^16 - 350222412007855156266636841545730482057176948250908727735133760051365670891639941471/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^15 + 2316325333892642111144228593942746100812583972299454983332300088756938372583879614532/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^14 + 1091200051684153918177807360721214611689863523162367178392130502200539042536100267386/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^13 - 4383641966060771688402659029958238877881725100424438138537865006803076213949263384645/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^12 - 250260658313822313061061650720367497268450446604267971656795887894745720120058450525/183986578609266013592300754798095296225347469268030090586483009241453494213338*y^11 + 5622317552759964030767374080460832322429011631889878171347988444483465693738697765497/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^10 + 5632111487364969382856637656600229736980543690598421091048632146412617997489072219341/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^9 - 1197759577687623343199439619753963546465073135612595963954295980327108258547851104121/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^8 - 784105694748334982284906789168244958899378463916706902092027555034850608986912735756/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^7 + 156880242247522219091844446027304007405454159802424536745311157861804969014145259102/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^6 + 1107662998095721769513264550239615604319198201572364791050589440388164262424113114129/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^5 - 22587816435777511619990390803741535695846369860048914781475053583586342576002325049/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^4 - 56192926523607738774189843791923584575526810749186337636552180203920757429869279918/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^3 + 8014112264731044581556291402065844194719690929105052708820304501121900414687842133/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^2 + 10016395944449683265773420808893254897791540422243980670673299436809592888362497995/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y - 236741307501459176934616602032694730351454477384201679591325910171006432290103229/1195912760960229088349954906187619425464758550242195588812139560069447712386697

-175212976680986976812096367960874053302119368989370382159500311813496850181204485/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^29 - 2043637716884618268170753871139113470872640832261974937859928156524937422474992151/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^28 - 10286306418828698071092953597859129021774778838450695835001604457701052474552532511/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^27 - 2857886894823600475301143664047546528992370513439013732988982239006549005576461473/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^26 + 98975379649018873214446279912181484714261280358517248797422654069584708441859568187/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^25 + 75763931142273257885906748056189595075858946427321593471397661097210436079434424481/23550282061986049739814496614156197916844476066307851595069825182906047259307264*y^24 + 50293403260564627995701837836208982152564178624247867211874279797806718104958959717/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^23 - 1220816516100624515554101911420487136330554738611553641385040773170816988382632634513/76538416701454661654397113996007643229744547215500517683976931844444653592748608*y^22 - 5198118004446049834798376652128462540252095509460754080312101279995398701649394455317/76538416701454661654397113996007643229744547215500517683976931844444653592748608*y^21 - 15411964256644998569410691673909413194259505639340182721393587108694399299222203539271/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^20 + 4348302852504331750930559754171097072195001710032488516895419611073306575035346889275/23550282061986049739814496614156197916844476066307851595069825182906047259307264*y^19 + 4163923313284922848847933745391316938364540339646238807833610436735147396830928681211/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^18 - 48537992916695513011157022645459441908605443721435666976102409751632556778836959494761/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^17 - 128318715944579850385847710000627668782558837889899729653340519560880817088437462158627/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^16 - 27357089188138471217352958501746638979597997511596887372946739665171572586956803115077/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^15 + 178324405429877088546942780251513565902933461984028020872084835562511978416058672708543/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^14 + 25552889095457386158465568927458411440581771581765628653541035766615234575970957303397/38269208350727330827198556998003821614872273607750258841988465922222326796374304*y^13 - 324387453886659599991484859624242760976655373918418998202605136331191392325890514226893/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^12 - 10809492313456482280738052811359144939181868497057724393263109151536795082113901569471/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^11 + 197943197014533602624919657860239077760425159559622604464994287270744363281739945476269/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^10 + 233623371359289225649620835392069629906227177305882831730132758754280631750934962488751/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^9 - 78603468917010006162404148873852774970867693907774051079390434054059995354674011224805/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^8 - 126489142019103750265967641640015229470148177669344171437087428704064879492522019094913/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^7 + 18288903841247610628313795257624845228302168689185823323741290686313258251975209727383/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^6 + 21856703814357303446424178488159986040547506779317792715632191532654336738749843591015/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^5 - 1080701930216010631568718490517750623842302693757051559896411595687613238320198950487/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^4 - 8759998738520150284783598075702848734725613319081929173608865674774957408069875800087/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y^3 + 102888300595998794357912678374167422211645504121558355628129769176771194859930712321/153076833402909323308794227992015286459489094431001035367953863688889307185497216*y^2 + 781660595959545091740009132844182631240609988885391847502371378501300940083645033919/306153666805818646617588455984030572918978188862002070735907727377778614370994432*y - 1282351720668958762798482478421372623532540041154828750824639521993348086480755997/9567302087681832706799639249500955403718068401937564710497116480555581699093576

4498006748042908842090923838401704188081241651759947498592653090044176410168631/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^29 + 52148254619642641817600449177601072330007288008670977657027387707281877174147701/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^28 + 260100985895515789355504148294434174898395821131546089428132896752074751495141981/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^27 + 62412771574919524297432153417428399543020648719928555440088748351764188796996895/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^26 - 2554768055386780608509016921314190676541411404868263959058025744468608742406617089/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^25 - 24942183971328312027849838525596120137606388811291060403389926840080728768403910975/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^24 - 15740947982627834349282086605545070939767896414297457797232551325843653386052165415/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^23 + 32343440098942168973477992721787967196991116012326513880614974574960834754856037807/2943785257748256217476812076769524739605559508288481449383728147863255907413408*y^22 + 131885757397267365826675203175316028866620249706714857912486223903060405981597428447/2943785257748256217476812076769524739605559508288481449383728147863255907413408*y^21 + 351380491114482536215238255295116940513038867529856679118042377253657114634069941293/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^20 - 1513077776882194332251183109466823184122532907473571331312705501883254280525600463885/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^19 - 1355981454404223412295712685965845006562088595580575976059985966875981816622775534201/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^18 + 1512602731500279284617942070943283870160927106982186899165062017266739099063707262131/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^17 + 3339781740611375985589687958849651194100961442321771453260721232630989430862383619981/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^16 + 466692729783677529719848082207241462354990918157790706421216436568352888860822127071/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^15 - 4802750191565294072421511142438997323567697068061569073878015810431989951271806303357/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^14 - 599220998295863259909254647874643436561777316354081502046534883300016956210786252241/1471892628874128108738406038384762369802779754144240724691864073931627953706704*y^13 + 9089755225915105741210546075660677187785395915978620964039509194441335345776934742799/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^12 + 3509304981772398413157367772885544701019507240726750336579209346710438518176897005325/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^11 - 5845309098536844534336474437306366694681347284352370972913298746187534221518509509375/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^10 - 6058733754102740001197243312616908249445196721865494738426298435012200767370428086429/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^9 + 2513551430223396292812210235435515858233799708325681429107775997614291521054454264943/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^8 + 3385677830168515721191661947534707001241318045422291734124293349101593848067977545283/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^7 - 676300513055068656474126200585014380335981526765935734088790628096083173256930934757/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^6 - 603534117088421764418940237893125093875277280309897645542019277448252696538803276625/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^5 + 53324099830491685386235132809302935769993203667054378892905015878975054875695888213/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^4 + 249163757540248858625269555315672625858043357606736955604473788077894355719779672909/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y^3 - 5931345552516977679624229658346014001163481954833201603222176773701816022485523975/5887570515496512434953624153539049479211119016576962898767456295726511814826816*y^2 - 22774051289501721374214514488311784701468267919817022245692011389946779203483581157/11775141030993024869907248307078098958422238033153925797534912591453023629653632*y + 176481255447351137842686324522064505175219834218785177110622443718952018491870095/1471892628874128108738406038384762369802779754144240724691864073931627953706704

1197356112961031768284276140092200754662751478993948821995171737670521265456641/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^29 + 3422057045495398639020561054931479725051133828712222205194940666748723235328305/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^28 + 67158934685105557287083522462290728013573378404031455271997149952764511875774139/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^27 + 5928794885843873590869546133015196910378257631046446857543440342284008788458086/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^26 - 339606328051844568668519360104092494549793400124706194681781373050282632913208602/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^25 - 247151250242986658536405636517395567678425617784226434487052575667331458802205559/183986578609266013592300754798095296225347469268030090586483009241453494213338*y^24 - 144036863135113080768080409820055455387543135216117533955441887141715216487430853/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^23 + 17567053556522205781293795061299100657190556419832088947641383296084239132427571851/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^22 + 67360782862473711381941228699240978793660708003227992021229404297668862471716089197/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^21 + 76197362716890677767770891488187893364916579725731640108529356759018701495610894101/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^20 - 7799120428989937976195360738899774829676990991293617019352834707664633760350123776/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^19 - 12758086544543112512331317312208966130071134788537435558048658723064602757681674898/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^18 + 116115152691075418852204895104694096374984958664648076296427019846506303699179950211/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^17 + 421287804905191487703956001236950555399231928561439361675562442182157777931285802479/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^16 + 19900177520493532792797827650945624280082345245635759685477747659223813915898800433/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^15 - 619782251336653380022587558505511728061681933455884135224245024903134356780340804663/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^14 - 254936173201416573164848874649454114225053688905776025746964290744550849789552383232/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^13 + 2403160387182188280356842441960040668903198467840175462606878741084863359048059554413/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^12 + 123959515700198975133766295700343306414639558736888179113810030759742185149560757555/367973157218532027184601509596190592450694938536060181172966018482906988426676*y^11 - 795565644490619612122773602153643213663738027353693614041363098580206928318288207429/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^10 - 717100557747266633091462100770249150914173457711355504633334260039081064867135485297/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^9 + 355354312681976662368688382309663926659172603428852864640454887456672940390416409809/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^8 + 815411205786382425091349445742091145539787075749901945349809236973144346702576457893/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^7 - 50448813797139016673991439512919284314488405647227890813870705010472152619806588534/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^6 - 146831342373468053808638505928050113899154796527239060668361130387666070943034075565/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^5 + 33533293547856429947328468827149031949589815915568355512938920157731578347868117203/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^4 + 15210160107855593226883541540947004672016524582455387652078481699760998563099465528/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^3 - 1650880260349625433457765415268550230627564960914220612483746589529956142169776773/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^2 - 2768867127035203817020489420233530288755895495452226021536020658006624168038011469/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y + 68813319672178111065652347226384212772117892443851198456690644303929760868293747/1195912760960229088349954906187619425464758550242195588812139560069447712386697


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

# B Gluing Matrix
{{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,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}}

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

# f Combinatorial flattening
{4, -2, -1, -1, 0, 2, 2, 2}

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

# 1 Loop Invariant
-113813758228803083661378952198115303650553364962225146507704325030638825021945495/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^29 - 5253765278422125812627098441832868575755672029663826254661765066866436378526333929/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^28 - 13033138707382042855771982453911548943855420714704412250353049104744034502199199297/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^27 - 11454219064125325617168857820876404963143093737076925994049725813134961801591713687/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^26 + 129225471137460221865682659061158166499982289863401275417155451764321735290821781460/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^25 + 48037689673941257491226967881415198971837639384135950404412380968348509419976747185/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^24 + 59169170360007758237650360777399405977367905615417151916638449950058696750831717839/91993289304633006796150377399047648112673734634015045293241504620726747106669*y^23 - 3294644958469177496784537710966008471901900172364384881837404929746234308232710426630/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^22 - 26349449669242338431083367631896678372934451766811837289825982633952625196332073244461/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^21 - 16741384029466417459981153771568575079258321182597820853981488488651301895448453368513/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^20 + 11803766122769869362258124496782137422001689071720548325512842886587411672826583201087/367973157218532027184601509596190592450694938536060181172966018482906988426676*y^19 + 10295677423940887842846149993639117293605926975282993540907435148927535113837363286055/183986578609266013592300754798095296225347469268030090586483009241453494213338*y^18 - 39942899429132104067402172710625673900614753041793115896271345248982831025211984081224/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^17 - 332525634111685218530556758429637394772145364514444011232952523963537531922846607468149/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^16 - 19237771921972060162592021134418041531551587881198911187108030180052838283377234547323/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^15 + 240325159269813605836222615118388796265244289083419654846446131244036358545618343282591/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^14 + 114817095227619045980023366262942604455448488835943824129853781780047242238337789689007/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^13 - 228317591070286357928057873172296207265239897091510966830169948713752399952900492400493/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^12 - 52660633011828966932235689788779849234670571142254398410097894426939697579584730049333/367973157218532027184601509596190592450694938536060181172966018482906988426676*y^11 + 588647616839426180379185470428876489496364030651073846973861430149510212693213992943735/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^10 + 148714916366168806373493147541944770002709654113837010790019656769152780206596974888029/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^9 - 63162891141757191791064252687383477904046094232235861544268871205618976054647607564012/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^8 - 83307199943461949780309170133604403887061023024292913885204696178372844403370605055007/1195912760960229088349954906187619425464758550242195588812139560069447712386697*y^7 + 66966714517027399977991341148559324331461215174218594299436467731851650095592783933271/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^6 + 59340512193767348822797908274363735708435204876462888368859358365616124834437597574825/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^5 - 4925233981843731997237216791033712776215735897473434731050388321791286625890161543453/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^4 - 24354311509298960450694161992582821594097812939341977825094436957181810315650009837681/4783651043840916353399819624750477701859034200968782355248558240277790849546788*y^3 + 447445430098970730511963917801316826239460471252939413750088607112308421441331550871/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y^2 + 1099488537372721702287212213045085966171606539047761111926459201780842353495402218181/2391825521920458176699909812375238850929517100484391177624279120138895424773394*y - 25993878793628542259854607701180800782565350383172354488046404107899958422382826958/1195912760960229088349954906187619425464758550242195588812139560069447712386697

# 2 Loop Invariant
5222415659829182112077597277325130088427049271300359036562568236280187758319279981033270824845082857210623537491137605229000247826382190476636343165870662522566489157962084191867/65525658160548840416974496895245012128753999131027873667905991271362792675512716902249433667495543548714870857099053546100674673638110912139694721655340512970509945041715611560192*y^29 + 182366407421807202432467857590213538066537138517996050803424010611058773601354710885031367582286321097848523202165693288349038637702861074263295178015298403374619051773788863901535/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^28 + 914084169785506831426885673471582249648000348587279111451980206233916623744386637054993650632019818557748029996541455540145946351512294468553665922253613022899006611320758261241859/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^27 + 78931143465322012690699073906424831341012878849015773623574994715554445474239589663339140709382429669096029541044065188286895871559132529122006492060317286462296512017805995370143/32762829080274420208487248447622506064376999565513936833952995635681396337756358451124716833747771774357435428549526773050337336819055456069847360827670256485254972520857805780096*y^26 - 8895592010466098151555240505393187457456113269702756104883064090420936090525454004674709522182390574621885374685440113076467193435770423546041719044795938202168986855348363158119107/98288487240823260625461745342867518193130998696541810501858986907044189013269075353374150501243315323072306285648580319151012010457166368209542082483010769455764917562573417340288*y^25 - 2248601706382692926899073652418753689521890602863387524650019136712202122760360355929451086612801917951908366673507747332001714801709661259041067024338794173620588847542747573254067/5040435243119141570536499761172693240673384548540605666761999328566368667347132069403802589807349503747297758238388734315436513356777762472284209358103116382346918849362739350784*y^24 - 4359599188113716532384375525891144041513561629319426113629008231764374627845680240912535776270599697834947718771306599687962415878172466502869004218808701404478132202861837288243333/7560652864678712355804749641759039861010076822810908500142998992849553001020698104105703884711024255620946637357583101473154770035166643708426314037154674573520378274044109026176*y^23 + 111710764245032004657960806368435739818288836097086897114237849193986884330857563261506914549086534733353518809755267255816283369243939663881077897900135684757246883566722970873477967/49144243620411630312730872671433759096565499348270905250929493453522094506634537676687075250621657661536153142824290159575506005228583184104771041241505384727882458781286708670144*y^22 + 464776897928366115330139440731745861104488022863258509170616400790989559718169358646148094360249007184658147292754382487417238064725877536708936840083879011146986508013263251794605999/49144243620411630312730872671433759096565499348270905250929493453522094506634537676687075250621657661536153142824290159575506005228583184104771041241505384727882458781286708670144*y^21 + 1300023408614150634054343075030214109037456400132060786688728511849746600214475962959255658372405541426580970470721486793737546122527029053114011521124534576205817866195766520075788995/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^20 - 402886461960296325795025498810759627596739202693944368640726701330786932021458179311370852712437896248719511825660982410751979684242397589474619885112621798264264252604441286187060067/15121305729357424711609499283518079722020153645621817000285997985699106002041396208211407769422048511241893274715166202946309540070333287416852628074309349147040756548088218052352*y^19 - 372579040757991783557792005288561149393857491457901744921022673214924638888974649447365985927955615599826803886169956669912249560077827308858472777095540256973697209476022411879692403/7560652864678712355804749641759039861010076822810908500142998992849553001020698104105703884711024255620946637357583101473154770035166643708426314037154674573520378274044109026176*y^18 + 4918501846428087089263580905190968904251275137314830183627736668105941976463542033416385910787216583932440185780872209025918936625015240825931709922730023835889164153730839233365597033/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^17 + 3928240936683002783426188974980997841047861286568550585000883655918596043503546898303472505796768754483853299844746510194465575581367935636634049326417181394535054341642200681956575505/32762829080274420208487248447622506064376999565513936833952995635681396337756358451124716833747771774357435428549526773050337336819055456069847360827670256485254972520857805780096*y^16 + 692986634426054187887195559810949324860131842649141248944544298254995925587361533403449884309888181715714153091047911773013204347569012806991505141139846326433940967790980160714209247/32762829080274420208487248447622506064376999565513936833952995635681396337756358451124716833747771774357435428549526773050337336819055456069847360827670256485254972520857805780096*y^15 - 5582365737216951954720673225329462425232586905625825937709680903949041965716397904314305391606249809125631780522906181647445209423663419734134602526586303432936508642787309804561428749/32762829080274420208487248447622506064376999565513936833952995635681396337756358451124716833747771774357435428549526773050337336819055456069847360827670256485254972520857805780096*y^14 - 2252702614832197805954599445079730219299933412613156654065706262528759121361040756419315758498647372003838327358975928047588077968442641430221138267077151809844323719370319306316419179/24572121810205815156365436335716879548282749674135452625464746726761047253317268838343537625310828830768076571412145079787753002614291592052385520620752692363941229390643354335072*y^13 + 31206651121836879445045904417842550923967375796596146966423938905594851419087068140733836427108847809091843820660197768080572725441950379504701242952516595964031741887754502088175397737/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^12 + 988409447504082681210349799619308286126460516268630510173345202813440322754242160852425251241515545684086301005427926295122602737037837320235056440285687512770530350904778455537717189/7560652864678712355804749641759039861010076822810908500142998992849553001020698104105703884711024255620946637357583101473154770035166643708426314037154674573520378274044109026176*y^11 - 19595588020116551602321355875684351408741491061206614145803958329941854473527015070896545432487716389106691468976875157305689478360891105803562543216339372741530422120916269182405400045/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^10 - 21888570183810005254052297013141583852235211025050685401414279753990443347675558650974546872954307531995258372617874106780473772880647089986577131445520223005870565612190507923414787847/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^9 + 8084326058725157465691556546186680817389404675023861267567242003070663979618965502100760079423520580920573074670178135414244574162310506542053851256205478992256375918878413432598287181/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^8 + 12105470516635164249288131335691680600976690817435352513405395447789437135250988676657622052980065835737246804755420280616450413863735989691681871581428265563980784638111488757691474077/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^7 - 1993639748270778691391144229497899029523902275453337680711321098988899020413494087546973520601673460254439786692537159153991491968983795667120109533045231895072512257165812753386473119/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^6 - 711866103047541993044962866102285036407865390377749016714250169187637051487073822855540708136535202147968548209750227510010947962871774498506161290164332154592229641300597379652432681/32762829080274420208487248447622506064376999565513936833952995635681396337756358451124716833747771774357435428549526773050337336819055456069847360827670256485254972520857805780096*y^5 + 127048471709783543883073810266187111347115216224665470084207855692809220944248799197898539113197066288150855321162678547440703879695161821862745920165105401853801521262438529198428633/98288487240823260625461745342867518193130998696541810501858986907044189013269075353374150501243315323072306285648580319151012010457166368209542082483010769455764917562573417340288*y^4 + 871079986009566111837395620096349417028575379006307926853832356010680714466665170873651237240535585507105418179122412747985148899753154976097223615580307095810429084360077307228664431/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y^3 - 3598604698598624934778654223889198162904598495295212407017024416621074861663702201057542512451158284164947370233524628277826876566374713475651095988498599834299230507873787589106103/32762829080274420208487248447622506064376999565513936833952995635681396337756358451124716833747771774357435428549526773050337336819055456069847360827670256485254972520857805780096*y^2 - 78566199076890485110549126592669043515749470597986838680993238350160229073106802675621091609414586798581901943250068500390708880910459128822229704461605765312067805921707228984571991/196576974481646521250923490685735036386261997393083621003717973814088378026538150706748301002486630646144612571297160638302024020914332736419084164966021538911529835125146834680576*y + 267481482343580586994163984028435337818935921149250932946436329622482226752638375839208844489066578551406894526680969805895956767602681655223652311400440269284427114490488675249025/12286060905102907578182718167858439774141374837067726312732373363380523626658634419171768812655414415384038285706072539893876501307145796026192760310376346181970614695321677167536

# 3 Loop Invariant
262795163713551166112344783309137105930268382862718018738101646219787696496922184387945798880759760666801692851745541581828341259592825671178743946194295265768680643537850875109513550681558246982610379545799771821906841584377939/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^29 + 3017596058867624845072963110195402306288936373878147176904692239694892656680695200109607853475684505887002728841890997925179852263629430800000618353849837877095697580371182593636555493441808779930691437272224694077550917666674833/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^28 + 14860672791143364683663638118307463574385331791147391567496979577126705421403479270786017777183998788885346620312120563483362680303599251165156233439799435529670448048158402094210000074847573665336247367602556246921755412865363705/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^27 + 2805349800266259741923689740427173763232307901320731856088191025277951703108000066754165177399837108620837011564075641902210328069253975261125970212138094856010804469602037536630995512600316034234572490842368550711507548143344159/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^26 - 149727692438887894957465125932417127948180256287199699054892307313505782673536439689783082597981104557760049206190145949891946018462894228543027900455403401451024150011580495231161313873483530639489545887916248674255380808116065509/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^25 - 109636822189367042704125705046521875048824727675819084221311573868681826626579545594749727896756505732205805375532970091169480145602873672533712814366209862167781766790196300729796396740728816135062148573540774477035630178919782407/1179842362144824271298015414715280138945797064129988366912008754661092407983394907023007389826610333093822902658414826375104931320851753589777529787956311468478303271576164282773745986862776408448925274777115525625804072193634304*y^24 - 64631720977085683485409000642554834174326523175498404918590096495466232023175064393967522102146907594295544023634793665554582437419221684258600981381857369054488669029809743016492924012337046701681701134170636520160809481603985971/589921181072412135649007707357640069472898532064994183456004377330546203991697453511503694913305166546911451329207413187552465660425876794888764893978155734239151635788082141386872993431388204224462637388557762812902036096817152*y^23 + 1943899560197869724134110693424470150473539941776979320297058383189418313752700941357447673061900334547305386811117360675441332837819567559254752017001468760904147971014412298838039278316944692726787951434018479132825987781001250751/3834487676970678881718550097824660451573840458422462192464028452648550325946033447824774016936483582554924433639848185719091026792768199166776971810858012272554485632622533919014674457304023327459007143025625458283863234629311488*y^22 + 7520375828913698978396480842298674319086462832195168805541462116038527010166315665502295884716383643633704712686019854003885795938896906157224972818732968420502882898689030474704506176694751643499892174385436970089479328781077765011/3834487676970678881718550097824660451573840458422462192464028452648550325946033447824774016936483582554924433639848185719091026792768199166776971810858012272554485632622533919014674457304023327459007143025625458283863234629311488*y^21 + 17291527173807556931405905524911689495809926808491729094488172086423436031878202382545557336125493858444422624868987998964826058432226342042686331091312893726520413231460624954625513645755833913460329376388350172877567478395935330209/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^20 - 7005376048899908620528193026754734989909887256646363061241661105358020554467349857241831039372069489028719861820274221182603404516319469768876938492674502050950943611455018820280287303036691205329452888987788849217379730873717763021/1179842362144824271298015414715280138945797064129988366912008754661092407983394907023007389826610333093822902658414826375104931320851753589777529787956311468478303271576164282773745986862776408448925274777115525625804072193634304*y^19 - 5797821732929850999469971921093952390937804101464711947545873134653693551077147206936361025249885933556035357854166283266515692875599575791139418888242224645019058392731225374727139231560984515397055393583520321251840868543382749557/589921181072412135649007707357640069472898532064994183456004377330546203991697453511503694913305166546911451329207413187552465660425876794888764893978155734239151635788082141386872993431388204224462637388557762812902036096817152*y^18 + 104232408366385120177855210608403295529993147594247158081805017208834913007064888719599364265566339268238640991683381570443170851746359537613110657552673713753054851021332965446781627393425145329998227228065767787289324633919835356671/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^17 + 192989752336913299380913054574314569677169039096380113035521585201677002851191023781462113840883031930725359051315847334662425719242373700068213987246893688387878119938350906783537629741459271025204038501705427469098358338506208789813/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^16 + 10742298015069154937319822580907340694874267605135630028101859891050079356514969719587877072539876493445801269601045932868608707318277198579521720621676962145557417003079314332836004970545745491478516207501244067898457655214989937907/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^15 - 286366408313683518176486840917283913553939911456709715794354168865075831947037779820146578943742662178631694174779791045329489848817135103032154345341713365268899526578425026804068247862391758623444803107962055239727159868958868105529/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^14 - 30092461531982375381551063709061640069800715746510012892924279799721869354452759653915409410496350954350307377612649170240592304433706972968685627378296001585218463358013271651459647151020982519585340012486429393859827309030992532219/1917243838485339440859275048912330225786920229211231096232014226324275162973016723912387008468241791277462216819924092859545513396384099583388485905429006136277242816311266959507337228652011663729503571512812729141931617314655744*y^13 + 560417516020244197764740571802863803311981980238772912620899483251718038423507103116789612631007103675601594486620413121411317443251781063549349955857621944007443696815670552417243767581184367350330667505777645082719685695614652166795/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^12 + 14680606370308714989628816584742205826178342377991383916189253839953209463069226541313390412750212568748538294922606712640388671771007755097829564288741838749646122883833261849373680461602126773058737601653888804076462809202276708249/589921181072412135649007707357640069472898532064994183456004377330546203991697453511503694913305166546911451329207413187552465660425876794888764893978155734239151635788082141386872993431388204224462637388557762812902036096817152*y^11 - 375075618105832272163972979927325189413820854317874107298070327285242641271566919965671760932329707269597182892686864479027425490784185163951867124437371716490747681618690491442231149128226955439125880810061043162310221058556313783355/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^10 - 342968189611664714738447619526212835185354006409714299171266895955882224243273780303271280721464504862658323330166924289079682126818033762453328315005014296168776773623748879412120512877475650060068443948671382997859264724399132722553/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^9 + 169804157706045264827452722663322811512184568316259075875808004501361165156698491296911394635117231754620804354565104894593202643599489309894062889261791658000331401873832763064575785348385719901356912788351814434083301320040020019651/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^8 + 197478569014765933525171711979562033496231839996120123032134555865496122221870216752668508746903709751908751518774021775841721955433266745951241046540794648729935514626212629957233162196272975928780091008675023406286253955676711654615/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^7 - 49046733827188017117577058736659727903347240081675666838395531072054731139988357061605885947578521568600920035539054396169191986646035461625952347967624736882904366407442624556851211278349785381142607106601963667551739899038455150513/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^6 - 36158019702367587291668090548569664468212155967985770452924636898672108484946730724233055089491976738543063201086413806739741793581374645758321164478647766235751523403965706993756675394492440788384172619872472966608776934944898539033/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^5 + 4154562870726369130365271871549044867724998073929419885174906656619174184904173070321093182459018871850122436444187172337795213591885356902028790289645545085978939030326876967982789460686366047202853850385830655130731459002568339145/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^4 + 15288767925478096899087233871453595890040779667865983305902813934450623548131986033970899493082980136176314643739276565865742570332130978556116934743936225510975008407631296910915707128342582394201493186629916265897686881703056760785/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y^3 - 410214059968607915067270170084088663974466671915444544013485064212788833969023513958276348238798301090954697138410955164953452462665271876376363945750833271539691284445150168306409856365294092073233587034171186161853193193020954031/7668975353941357763437100195649320903147680916844924384928056905297100651892066895649548033872967165109848867279696371438182053585536398333553943621716024545108971265245067838029348914608046654918014286051250916567726469258622976*y^2 - 1421625141010635014813310053359998512138195230518343946853367769927725237251729557217400840018127093677254184739328013683852690284109704808258265607137802460461932541138888147952943628862392190311768348882738462125904692399873245273/15337950707882715526874200391298641806295361833689848769856113810594201303784133791299096067745934330219697734559392742876364107171072796667107887243432049090217942530490135676058697829216093309836028572102501833135452938517245952*y + 2124177963520701605294422270395104529022022769189726015710224820699867374195469128061554479554572152915390389772463328298194403183631613245503344956150277492636349126587333682509342188835363707118121306154791139674827867428237917/479310959621334860214818762228082556446730057302807774058003556581068790743254180978096752117060447819365554204981023214886378349096024895847121476357251534069310704077816739876834307163002915932375892878203182285482904328663936

# 4 Loop Invariant
12920089289205276503423064143859106129823966637910312497754801854792870935436695610367459021320962407876534037786739723580951800352707684949026452412591535091942639981130824319330477020778046372714381342568621024126412387401317894284794581758025850240984060364545133791710869642093036953048344761874294676073057080176668495435835/1890870331429937147357011950600267637363708905540994520651490561546600015081485761685503061711942579642254001186780847023415454228771476232301292967541057609761694254036217042781492377597217155056986846228313314074166263617925876687057368654937190441952236316859883960771506943876001852812077011518589184714005647636749947141619712*y^29 + 753424187824514331878659272419491741019178167763608212836513265280215531499898674274358678133801208128319135308857521842412800814132776407839907998763152414969862920951697167201661639920635175379030759678023667708665767928456593703790315066100653821229707032103242290331465006028539295462862954598139430707912606733605947933192621/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y^28 + 3776724081210074340033794664090951686714033055599646422153624316830740842840802944314575973204448851351236527918117619426429172943822091879675209226896011328042316924047900715470943591091038417519743151597251925478727231401934687211883541999121630484131845510355861748961435836177838401059259378403510147712544518694320748946323717/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y^27 + 322542628107000745869575094181319822708588657196594767234820340185530321759173818889087988115467242196508009415843609513387882144339254363250010586522884227753167736264782938874391041464785912596097846837403357323246524386057187346704954164064768188910800948741144662505567313238494085928223769503138849452494765199538078527010553/1575725276191614289464176625500223031136424087950828767209575467955500012567904801404585884759952149701878334322317372519512878523976230193584410806284214674801411878363514202317910314664347629214155705190261095061805219681604897239214473879114325368293530264049903300642922453230001544010064176265490987261671373030624955951349760*y^26 - 819971719186458388311855644665422457872870106550683112889544729710248658067116197359642786780029364979566858625822159515089402700455641182531693894489831637381803256824163545795688907441944141299682851669753346844294325194019871863182712749049640982929829932009296049371755821037794759144494239022190306581134817607470156606560861/105048351746107619297611775033348202075761605863388584480638364530366667504526986760305725650663476646791888954821158167967525234931748679572294053752280978320094125224234280154527354310956508614277047012684073004120347978773659815947631591940955024552902017603326886709528163548666769600670945084366065817444758202041663730089984*y^25 - 5588664859647356808448713465455281517067252372408600609201629900572617955996749258471801898954694509730612203039920982764816253193705572429936066915140274427429152896466449922087184287753669196100706627473365627965745765573373958781530903978765125759304604701922740661075660223119786832334080913109321577366069006614207458211528927/145451563956149011335154765430789818258746838887768809280883889349738462698575827821961773977841736895558000091290834386416573402213190479407791766733927508443207250310478234060114798276709011927460526632947178005705097201378913591312105281149014649380941255143067996982423611067384757908621308578353014208769665202826919010893824*y^24 - 17889402859567068207172896458336902163056257675161222347347493853359867073355614982201540472508595274864609566703156415953131835668772483660133695128226655456441879991493101174112682017835233480880131496642530938770474591028936900058784048331376303671070836198927299986513484630210825414533605296869482912746093146994231219708884727/363628909890372528337886913576974545646867097219422023202209723374346156746439569554904434944604342238895000228227085966041433505532976198519479416834818771108018125776195585150286995691772529818651316582367945014262743003447283978280263202872536623452353137857669992456059027668461894771553271445882535521924163007067297527234560*y^23 + 156442842606656355885569075810736919375940090797523531748408618499976139854995281667739167559444122220051959638952896510327390050373091728067542735401508381736557058525772812049211264926102494747393605070251559849666160692453129252289018756349631515218381099106981647735269996212303210640387810573287931474898086446369719827246006889/787862638095807144732088312750111515568212043975414383604787733977750006283952400702292942379976074850939167161158686259756439261988115096792205403142107337400705939181757101158955157332173814607077852595130547530902609840802448619607236939557162684146765132024951650321461226615000772005032088132745493630835686515312477975674880*y^22 + 215254097988646262997060578612738625119747102596148518940433224760096162290350002586971151170765076345939460500058097212578984367441182787134570773547884772422546391969925545600895740424473124592634456394977155908495356956739157172093358158492125114336041508686102438173432676788247524254324287520230073023701422021579225846522611647/262620879365269048244029437583370505189404014658471461201595911325916668761317466900764314126658691616979722387052895419918813087329371698930735134380702445800235313060585700386318385777391271535692617531710182510300869946934149539869078979852387561382255044008317216773820408871666924001677362710915164543611895505104159325224960*y^21 + 5259433729723615532319667471395934581761755911156823525434991042296074769659910835116845977020306079445335028973930065190762855986435523547373244906546146326024645128101689792021543427885317425031961617390309080755988673763707276838478656669710224299346191513130733939100685637760604419657827361728891845991842150899923863301038492509/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y^20 - 1721317158592591103546048690839429457469876761016173253756957599358098321941668858317645857625894040087441907343064248982823203823205007128234110891782790857055171005528008730048486415932580266185253714490367672625892549520886771756403788101886372230973980057533801046645380401010618011189611168155500789377002654510986305533488265081/727257819780745056675773827153949091293734194438844046404419446748692313492879139109808869889208684477790000456454171932082867011065952397038958833669637542216036251552391170300573991383545059637302633164735890028525486006894567956560526405745073246904706275715339984912118055336923789543106542891765071043848326014134595054469120*y^19 - 1566007574554475582237158737441927835034065424238529142045740359551553127821732618341285766657383217639619195831955789401425805312300798701535286238292367423461252179227381863470661964190278807068250210238182716058673178917925383165250181054587052780881376701699931303497770042784850025140562409625284688746297082331049569325743275977/363628909890372528337886913576974545646867097219422023202209723374346156746439569554904434944604342238895000228227085966041433505532976198519479416834818771108018125776195585150286995691772529818651316582367945014262743003447283978280263202872536623452353137857669992456059027668461894771553271445882535521924163007067297527234560*y^18 + 22256356393211706271926646432370848560347421894344540428562362707784830213508154383117133952257157726900066087943365605409584755420902986857523503541918743840689838807614010673513838979016127446401341632173812983541183896858507212468277335502919340403758583910090015361752837625533911558360049466190719697735958412873014474161718332531/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y^17 + 50625040770235642347038592232142340463257372882500301522060384243143665819466405191188888637004268815118644427806214805135978637395665430719178491861608776602105918363745119173342197031603742172213973599959059463491889001032082026216643563691389414127563793077546364213529723251377805894480035706511353111202764879968020779481258115649/4727175828574842868392529876500669093409272263852486301628726403866500037703714404213757654279856449105635002966952117558538635571928690580753232418852644024404235635090542606953730943993042887642467115570783285185415659044814691717643421637342976104880590792149709901928767359690004632030192528796472961785014119091874867854049280*y^16 + 7647124834196635598584418033058155651292327214310518447204253632655406327086963439981453306200181426427720341342720023104158232433239601634595098853024899947598863610227931994888957979590941216695168535498351137988652091801314239444469289557057610567164803003506576788504945683116848110943515539041375880076453445570770131355946240583/4727175828574842868392529876500669093409272263852486301628726403866500037703714404213757654279856449105635002966952117558538635571928690580753232418852644024404235635090542606953730943993042887642467115570783285185415659044814691717643421637342976104880590792149709901928767359690004632030192528796472961785014119091874867854049280*y^15 - 73519961933394060357158762173790634489579951783927206543430825682154264228137072177780063127757714700448540395592002543570736134594985564460536724473473844511866170333529398241497662613251935265887623184323637784354020210906864814712707561733713383489654640305226175449854782064011780857368525509762487785799698803624838343519848705573/4727175828574842868392529876500669093409272263852486301628726403866500037703714404213757654279856449105635002966952117558538635571928690580753232418852644024404235635090542606953730943993042887642467115570783285185415659044814691717643421637342976104880590792149709901928767359690004632030192528796472961785014119091874867854049280*y^14 - 3134688180838784289122782772244670181472946367078213513621832138363389867887023438009185238277834920169360956740361526278933837245372711121216125835014848210655349296857106167936147486608533341552581197524049766735240904247847331496996234962794220905425512831728304582494754411549291007521366478260111621443660290743957683665562255397/393931319047903572366044156375055757784106021987707191802393866988875003141976200351146471189988037425469583580579343129878219630994057548396102701571053668700352969590878550579477578666086907303538926297565273765451304920401224309803618469778581342073382566012475825160730613307500386002516044066372746815417843257656238987837440*y^13 + 15619274322239926885782974058815129392005464173094145401864465345856993004816259458488041845061782676231488637865273977248878440603734127036038370995970680732057639376572024029310339932910842869203395633758795321257762138502188166614606957891737534961456094189485053729192037447428110153321581929543555353669149816480366834939391174919/1050483517461076192976117750333482020757616058633885844806383645303666675045269867603057256506634766467918889548211581679675252349317486795722940537522809783200941252242342801545273543109565086142770470126840730041203479787736598159476315919409550245529020176033268867095281635486667696006709450843660658174447582020416637300899840*y^12 + 1419696111982241085935528143011307019102751483591350612296847055609787153671743012246803699371389457826321019533683613329266950076337807673449418888090676413178990317963498334988488450312883105912066697828009210703676806775033320541094244466218497260835675975712516224723557608505034540109847347060849520060442303503599836606864696231/121209636630124176112628971192324848548955699073140674400736574458115385582146523184968144981534780746298333409409028655347144501844325399506493138944939590369339375258731861716762331897257509939550438860789315004754247667815761326093421067624178874484117712619223330818686342556153964923851090481960845173974721002355765842411520*y^11 - 91361713258525504118853363734001272686796059721647932015189908473582801006172044202915526670855198396402667290827191017069585851421922708041887238721404416122892601064302707310546880867251520197894015307104482572105897433682434000105914029325234478710374538104697038390543030287077180065276741645935433088574364192464982369389809530079/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y^10 - 96657156961259873138925194416464992371094558686550338489736720833784119854015303661724310289484052098580285057245097232902519485606116324302792447654171751460785431809429850806987370287025955052599743333395242367425592118141873407236738679897714642444350836468555189129693290220515173559389685922330394499412585284265809503566140615669/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y^9 + 2647650605261155819511378828003088566223913048453597240778888764907848946221973684955666688109897470304869235349714903859451293886097527323685720603924356806277486722898564445284444107351553947261976433221413231695899794792767361605182224597056744443284912527760571687815653665962434312951524533270564652063653728658908083270421645929/630290110476645715785670650200089212454569635180331506883830187182200005027161920561834353903980859880751333728926949007805151409590492077433764322513685869920564751345405680927164125865739051685662282076104438024722087872641958895685789551645730147317412105619961320257168981292000617604025670506196394904668549212249982380539904*y^8 + 6086694018813994944806077600711814718930542691655531227939729844576401184412046962386873370783107887538757144819498160568374094921520235481539570781278148957167796579077588660460083294896023456037106472209897900054778520346384865024962518999969081309180721277139985482910228857643605585704031074218261247431162930382441881978549928067/1050483517461076192976117750333482020757616058633885844806383645303666675045269867603057256506634766467918889548211581679675252349317486795722940537522809783200941252242342801545273543109565086142770470126840730041203479787736598159476315919409550245529020176033268867095281635486667696006709450843660658174447582020416637300899840*y^7 - 3584690748888078825334128885082270504871156219746391989053027459329507295965121133719316326249085232748175878854114153270297579610334305682027733537746273941828179590492927921589550166511539984101827548393011886399830900958536159769847088451593238197767602915608593656628822552054124924860280980985338593007786253013096134723723924559/3151450552383228578928353251000446062272848175901657534419150935911000025135809602809171769519904299403756668644634745039025757047952460387168821612568429349602823756727028404635820629328695258428311410380522190123610439363209794478428947758228650736587060528099806601285844906460003088020128352530981974523342746061249911902699520*y^6 - 9940087355630603400585475947673463953056258993452891826019812512791833874869098998843260366950961207033792321752958295142749006572064136115706409519205033700874834507513009666398596776599610166348193796609912513416932549248515001480735418907102242256926438730805585952881466241705022795861032213032954532083579128293764019759961760109/4727175828574842868392529876500669093409272263852486301628726403866500037703714404213757654279856449105635002966952117558538635571928690580753232418852644024404235635090542606953730943993042887642467115570783285185415659044814691717643421637342976104880590792149709901928767359690004632030192528796472961785014119091874867854049280*y^5 + 165405181022081776801922187722573480974661635102796127980162363908368494875658591735423358853157188921622694855448448585919527711693372313513826201573553307171736708859811512340151718171511049566485994638047554432173806505711323677133569828682230117498493044502245034665804302102363674848163062715028646710276367397646941714243934857/945435165714968573678505975300133818681854452770497260325745280773300007540742880842751530855971289821127000593390423511707727114385738116150646483770528804880847127018108521390746188798608577528493423114156657037083131808962938343528684327468595220976118158429941980385753471938000926406038505759294592357002823818374973570809856*y^4 + 4187183606096464859334475062893183504669296826253221697060277185760831227300563679837580517294053821110393271543474537037993681634759100872228062719049734733502781094613087074249035211778969195899028826447920055477551027381294567080976521441460245862309739580198294255469395290991504103328929161906326246069950750083330177804869531277/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y^3 - 80982064049948538192386305023333912282938088890026841512044810540204894761144270687719553288226012806217405722187274599349927356552988739560539557223067199229653517141379290751310504458366572700818930019909467396290075763272672765987812815245771956210720452499528055448436890837138104372012102293321046340787847028263187355079416523/4727175828574842868392529876500669093409272263852486301628726403866500037703714404213757654279856449105635002966952117558538635571928690580753232418852644024404235635090542606953730943993042887642467115570783285185415659044814691717643421637342976104880590792149709901928767359690004632030192528796472961785014119091874867854049280*y^2 - 389683519415749099723180023949170478138311634727876817979908260057659160332617047378000687942897141672691013672246515548519343118152732989474901468881490718415504052091935480773997308955800843517691215231523719262482112491686522989416246846189178441724074087977210895977156275270032019379868302868493380520746903941463732760719863109/9454351657149685736785059753001338186818544527704972603257452807733000075407428808427515308559712898211270005933904235117077271143857381161506464837705288048808471270181085213907461887986085775284934231141566570370831318089629383435286843274685952209761181584299419803857534719380009264060385057592945923570028238183749735708098560*y + 288455554792466812499331644881647760591925008576333753306989942946326076746136772844184215225887612255389660857819397793229645821044750142031109708593406211748976989121576804361156593208206212559671246907173501783272802365619394797435265657388203679855473084011841675479287798445383024814905977382533566086043777795383647020468299/147724244642963839637266558640645909169039758245390196925897700120828126178241075131679926696245514034551093842717253673704332361622771580648538513089145125762632363596579456467304091999782590238827097361586977662044239345150459116176356926166968003277518462254678434435273979990312644750943516524889780055781691221621089620439040