# Manifold: Census Knot K8_94 # Number of Tetrahedra: 8 # Number Field x^25 + x^24 + 141*x^23 + 145*x^22 + 6851*x^21 + 4524*x^20 + 162045*x^19 + 22830*x^18 + 2163357*x^17 - 1127342*x^16 + 17860188*x^15 - 22966092*x^14 + 101738173*x^13 - 194223817*x^12 + 454643918*x^11 - 886913581*x^10 + 1592281322*x^9 - 2375374552*x^8 + 3396539965*x^7 - 3647630495*x^6 + 2958942346*x^5 - 1521173028*x^4 + 547673723*x^3 - 7110701*x^2 - 35266106*x + 31847201 # Approximate Field Generator 0.121177620127629 + 0.548564637544626*I # Shape Parameters 268124547634059131328566407427146741824609161579626547468924494161632003515478443669423098318960/77375534647517441508544821880100487108985405075445481785812829704813627399669352687278753100600909205193*y^24 + 5340018326835220779175934724522086855992782263121342508303820253597856496397265981983093943417/2116655963001996880172958653255028522738202570452915915113420873383959412149009647980269841657775631753*y^23 + 7230528090333698329560226318514482764478801230490462960314641453481843315904282510733417972709311/14816591741013978161210710572785199659167417993170411405793946113687715885043067535861888891604429422271*y^22 + 257180139080970590060442817105780032101264578237686775261835662700360651532208755497397945821017081/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^21 + 16470764373744355479516492210240571887545100280010360454981358047281002346035129952968690898446599172/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^20 + 6396430046979030427736045545445049118975619202348753387057437052523324482487171287856091683338060314/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^19 + 389666080766351559729418777290731662598952250904527078312223068083360059854199538341364750705935011525/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^18 - 52929316823075098683473581747226733776391451504404552104472996017367393596486640718303840857666496615/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^17 + 5243266563894182624158559115030601752972227165887124101438176604774594374630530753300000915337628891561/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^16 - 4196050739295588846361500412627635720703542861568334053745341557729947874190341245459226338442133361056/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^15 + 2112725376728476038533233068213873126140051949041655957593248936083393344158284043266145064912252360918/33160943420364617789376352234328780189565173603762349336776927016348697457001151151690894185971818230797*y^14 - 68166231449411802896829738642197295573103237170219270348595027243966554664961407586788376748677166736118/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^13 + 12644070101762208777944098365715497824672439496466863184129985404021894905273617378252616040725454789027/33160943420364617789376352234328780189565173603762349336776927016348697457001151151690894185971818230797*y^12 - 546645424921043248189142766335522409957795493501738477434177717670563184924598485098221749272908516685500/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^11 + 419503286698187108301130648082839629224445793310252587063173891891867277055519208259130502399803639766472/232126603942552324525634465640301461326956215226336445357438489114440882199008058061836259301802727615579*y^10 - 2515440881354551545618933853474969699787718377587314519329882758587284653264969732415019509933902170966313/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^9 + 1532547364285943228848940591544955115134317382000580740532239800346057845435752754932833699233019357519993/232126603942552324525634465640301461326956215226336445357438489114440882199008058061836259301802727615579*y^8 - 7118803793066882369799496958554089101974673294978258249616385383926342895339408825961819026561243029660390/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^7 + 1152066889316515389346018837218510592368726048494436932502669757070749888759280573416413331868386255626025/77375534647517441508544821880100487108985405075445481785812829704813627399669352687278753100600909205193*y^6 - 1331686044738298216929687516315548662467664701546358854623597360270655358575834298434606144991867818087709/77375534647517441508544821880100487108985405075445481785812829704813627399669352687278753100600909205193*y^5 + 1545233519299876822205162745366330175016026921277308587253551771889656531172521628579630679717935218966650/99482830261093853368129056702986340568695520811287048010330781049046092371003453455072682557915454692391*y^4 - 6950351535549796004078461905265579220205946354232863104547807083734195427610999163025791199239068199056046/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^3 + 3355965432695085222679145071357362565256017591260500943480036059076140324304044771550945843226349971043383/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737*y^2 - 92694710551981368490161769021362033382424603712218869425179355102199143771909823036595905889490499658671/77375534647517441508544821880100487108985405075445481785812829704813627399669352687278753100600909205193*y + 79948015130230951278587080960627276520975088958740000012020582722253693402689324696153687698646723032410/696379811827656973576903396920904383980868645679009336072315467343322646597024174185508777905408182846737 9907511919639405693319755177689750946785116593805582607838878367374905499248638168482067282802/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^24 + 20359912690514158312621939896252504651878154498572166585342429095230608977557855676592921746723/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^23 + 472577396445498110952484064599940344793450367598301921154482741027324829025404843662878055614634/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^22 + 2930742824475696066268390455698720202601511258394709317545212316416491739987626535126338558907853/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^21 + 23622380223995033952136766652406593395231377306825163951855934235752784114567283653525520318190527/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^20 + 39788062974605970890775482847034591808880162728111653689185798274471672365471445360260749716565909/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^19 + 575445022860313503457268230931415509262567472046783946582253161864395424212637548481750373157686224/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^18 + 679467337634584128858914466931210602931843353076161755307200252426801407509670252642698897015182680/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^17 + 7820415540808883560222511905856717399663529035455134023635493581233190058203314301402405817070489761/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^16 + 13427100024089353353065447413965079764863511474413046203649757726664480007810133721125213257544091794/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^15 + 189465361779001120563462234328008558478786380809016739609625434250702820669325791919984434125030862469/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^14 - 28681690017134072273221486701753982337517638138360193838503499205088790953133029717057254651345504968/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^13 + 321562340930076057664854186524925764621259653996317941900914337316409834545866782383249047092777147626/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^12 - 904549621799068403011314853619010714275707435025524224770103308334048296710175352703401238682965456769/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^11 + 3485969790610050594864231452353117119089376055320500020048710293584185475781682037489118898884423633410/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^10 - 1681376757813019157962750669162197858341978430198178041583636611545127097264629103511492772189699573496/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^9 + 3408307189291551138420107634197516939899365435235026898598837234002229805655684487380680399042320668100/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^8 - 12392263481971153270684328389666803556341095910106510846551067800168467659049772847940237579515422877130/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^7 + 6623187778587253363459987567281461593621336583156949546657407420178314861888166460124987982867236138390/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^6 - 14296863896434992987970412929975647353722861405362072058731615310356630817741830923008818186143359520390/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^5 + 12777323069155019559377846767595384352797490807237256269153525160595240419943909553223905212899245880676/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251*y^4 - 93319602132828119328885575059880591829436234757008638914186809191990076268260962732068809580788200368/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^3 + 1282299440803490820282384321073426726158761089079965575306548346549084382908422756446966225209965948741/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y^2 + 1455001165450805156172150945201869917873176539586221686537652945832527092659993559272904709108894373477/235183995889110764463662072583892058082022507828101768345935652598217712461001071997807760184197292417*y + 1928986824523045297131874475087022593334169780524992180512069871084389756885832336228652969537375182993/705551987667332293390986217751676174246067523484305305037806957794653137383003215993423280552591877251 -79948015130230951278587080960627276520975088958740000012020582722253693402689324696153687698646723032410/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^24 - 9412972268715352178817076559286201308584123165134962165381963974937098075313031111817729491752559130/67409567901573158044241128994902197624376607639930674184716052352254505574551352210166897681513353757339773353*y^23 - 238653592931704019045524694629138687859629445537239978060299176637971666844998537549410317296014982316511/471866975311012106309687902964315383370636253479514719293012366465781539021859465471168283770593476301378413471*y^22 - 256558122240108629992098196081193219001987292257625395057933414321423362860257844192343065130378522079811/7392582613205856332185110479774274339473301304512397268923860407963910778009131625714969779072631128721595144379*y^21 - 539533384074692621552856567115883456501084909079011903575547504251173465059987353283063427065879658492000629/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^20 + 162862923185110787987285155968587952276706902733306471437861644749249876241885831747915162601021656598494732/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^19 - 12751467718389693875121417716833903910094518831482362880730826330871041875456801696462442512213512676016797336/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^18 + 10584560811625059541676162355221045972879153443030871472677678902538400761165326108851461139886699518144071225/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^17 - 174641748759748194171057730241833604035737333135255414362190936279503882273275192347467560157547396107889124985/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^16 + 85704039809954065946196668343692390115189321568863817887999102391008329990100800772879277682836414736584508327/7392582613205856332185110479774274339473301304512397268923860407963910778009131625714969779072631128721595144379*y^15 - 223074150250473498522548351804365572792089517577757507597066080384525928790750507795582579670854066708732671048/3168249691373938428079333062760403288345700559076741686681654460555961762003913553877844191031127626594969347591*y^14 + 1083021885012732827863810841373848969153482060912535304032259662004350787496282693650173207917392810326442980866/7392582613205856332185110479774274339473301304512397268923860407963910778009131625714969779072631128721595144379*y^13 - 490698508033713955703008694650134685761087177004063061909904667847454100618298989802372890116749542233813194888/1056083230457979476026444354253467762781900186358913895560551486851987254001304517959281397010375875531656449197*y^12 + 23984051741934349309126364646812028689003787075371736927868924219948344579449660613127720371778074916030149640937/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^11 - 53757005558322353388936455689306204365095838223044153089065306869864202492063284115852044897127070842810695667880/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^10 + 110986996867908687876552825425390232793524435639657863161513913966998453919384689151105571668635000607113212694826/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^9 - 69136494191651898868457694467143512768708966626235743740245770289121400049120544536538727971920940304704725995311/7392582613205856332185110479774274339473301304512397268923860407963910778009131625714969779072631128721595144379*y^8 + 336328512480565534001131243597811004867973563525626004894410650004114628680416561963257690997463410676869220999099/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^7 - 55362289309957501663561086505935764575010551972477280798929954203787508432654138434547505657233635196812217481560/2464194204401952110728370159924758113157767101504132422974620135987970259336377208571656593024210376240531714793*y^6 + 621831770109322178293496761153175637968869202844280544161270255215842773534429937105536749168119980821872180397175/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^5 - 88322260809795606844369486813794132332937801669699992027365081645850455774391898704294387879157927941052545258063/3168249691373938428079333062760403288345700559076741686681654460555961762003913553877844191031127626594969347591*y^4 + 466094301625807125519832349832311893017509094667243256104034694920867423362050977266883184409122730741357865764030/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^3 - 265134669466146913787458992877245016754914949498760521291621383597032907572759840824412474428294804852955741589676/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137*y^2 + 11938510235025211017142232447872342420152109197160335376058202514469936363583143926265368748068501219586230993377/2464194204401952110728370159924758113157767101504132422974620135987970259336377208571656593024210376240531714793*y - 23749148531199615782779747897461946377809057285337069948324053302446237753156450183285127793085818180967528073379/22177747839617568996555331439322823018419903913537191806771581223891732334027394877144909337217893386164785433137 66669320450727032947368105695911095328832364745173942244146589461743125174678165194734434235124358550005625802211627823/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^24 + 8105372517845853672254725511564334264463668232134778952127094082549979653364152772016107837573896909589635595409915990/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^23 + 9544427931693497437323230239949665387126294840362656704600145828278547971670462627386106185656409478919240119885491269844/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^22 + 6593644378312469312258633333676903415810832141765670013297218652775861571886811574940103590325867229482448485050368093092/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^21 + 159098460184222864487881238009436672004521676424839139569236250407591026275616730989028408916546335079745879220647442968593/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^20 + 89011911035001405871794447276690153068056724421718699250850371156887444526335504400246527475726563527828763986491716935778/860741011335029703623751076469577548869873921666660831220041079029781231105100461515314785085630054931818856821980313649488067*y^19 + 3872447227440675358500934854959184939725962839021359105709009829800712412151209783970119571492780636869132977161290023256240/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^18 + 4481513309632742271420354587401557904047172317034399078557836546408959151580897583722721691236123234545387534391379749924549/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^17 + 52418805096078411306873426910012389876957854903392489638876783790344413187557996143069079421040575384559745034793163191131553/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^16 + 81582775512900666853504936036555033885640232939064295106027607085362991340125500523423601129486364314990998865510980167482809/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^15 + 418950538621016697145849827408083011935790251312335662038214779037214420149781676387245001335334143873375970116675292574530023/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^14 - 331898346287474031731394547164150630774229993418719555971785006182440431550107508983262247426613135652165914679128217067816178/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^13 + 6272233836025205205030585389630867760491513600961388437635400858733233601910931899928624834792562894763687152150845201063892973/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^12 - 47784645762051879490233043709970911897752566030965503231517493046068151636835901342847635775447943386171905869186622901171753/50631824196178217860220651557033973462933760098038872424708298766457719476770615383253810887390003231283462165998841979381651*y^11 + 22226258344858499477631357266943759709283519775058265821640209340715814171135929823982374410988036939418068790485775837279325521/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^10 - 2363030657972614424774464694637217638905658542525340965057997054499930201444366314776150436262097526627073397895468693866318749/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^9 + 66379531322313290670119615355056124872903731991860915468902061994891401728249130043457180914517033721213480168355131499534927495/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^8 - 2006072406860779746218958864370293819505890207555696989728247104130963670156751346741609149804882143508734240804360547085061443/151895472588534653580661954671101920388801280294116617274124896299373158430311846149761432662170009693850386497996525938144953*y^7 + 15217665260588711414689110930897573754053772895483544113644385094270849982225485942711606274951887866922567466153200711030384230/860741011335029703623751076469577548869873921666660831220041079029781231105100461515314785085630054931818856821980313649488067*y^6 - 2554626713470958467204103412165372308007385719855302794313476806684428264554482357708575901747845618620730504150655554924997686/146163567962552213822901126192947130940167269716980141150573013420151529810300078370525152184352273478988107762223072129158351*y^5 + 95509738272983735194214843444564432628417511693451215195280278247425338104054307518508716221857833673888457154268205667408784956/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^4 - 57477741900730060080812480296053976969885534633726155178440230734105254660478808025313483379716585501106534665213392997977849761/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^3 + 12457295309566734261320495861413434994454212661500198664587188466957653187023612471259745506959123530790582542394978265168886558/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^2 + 20335450692792273014820583821311761423842152857521509226340593110458759316777154577926161554068779425525017007554919532233014343/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y + 17397495459651928926331950185892385906346103836304197330138518086202249201054577412354845422407077200253227633910048281160368/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201 66669320450727032947368105695911095328832364745173942244146589461743125174678165194734434235124358550005625802211627823/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^24 + 8105372517845853672254725511564334264463668232134778952127094082549979653364152772016107837573896909589635595409915990/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^23 + 9544427931693497437323230239949665387126294840362656704600145828278547971670462627386106185656409478919240119885491269844/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^22 + 6593644378312469312258633333676903415810832141765670013297218652775861571886811574940103590325867229482448485050368093092/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^21 + 159098460184222864487881238009436672004521676424839139569236250407591026275616730989028408916546335079745879220647442968593/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^20 + 89011911035001405871794447276690153068056724421718699250850371156887444526335504400246527475726563527828763986491716935778/860741011335029703623751076469577548869873921666660831220041079029781231105100461515314785085630054931818856821980313649488067*y^19 + 3872447227440675358500934854959184939725962839021359105709009829800712412151209783970119571492780636869132977161290023256240/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^18 + 4481513309632742271420354587401557904047172317034399078557836546408959151580897583722721691236123234545387534391379749924549/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^17 + 52418805096078411306873426910012389876957854903392489638876783790344413187557996143069079421040575384559745034793163191131553/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^16 + 81582775512900666853504936036555033885640232939064295106027607085362991340125500523423601129486364314990998865510980167482809/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^15 + 418950538621016697145849827408083011935790251312335662038214779037214420149781676387245001335334143873375970116675292574530023/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201*y^14 - 331898346287474031731394547164150630774229993418719555971785006182440431550107508983262247426613135652165914679128217067816178/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^13 + 6272233836025205205030585389630867760491513600961388437635400858733233601910931899928624834792562894763687152150845201063892973/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^12 - 47784645762051879490233043709970911897752566030965503231517493046068151636835901342847635775447943386171905869186622901171753/50631824196178217860220651557033973462933760098038872424708298766457719476770615383253810887390003231283462165998841979381651*y^11 + 22226258344858499477631357266943759709283519775058265821640209340715814171135929823982374410988036939418068790485775837279325521/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^10 - 2363030657972614424774464694637217638905658542525340965057997054499930201444366314776150436262097526627073397895468693866318749/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^9 + 66379531322313290670119615355056124872903731991860915468902061994891401728249130043457180914517033721213480168355131499534927495/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^8 - 2006072406860779746218958864370293819505890207555696989728247104130963670156751346741609149804882143508734240804360547085061443/151895472588534653580661954671101920388801280294116617274124896299373158430311846149761432662170009693850386497996525938144953*y^7 + 15217665260588711414689110930897573754053772895483544113644385094270849982225485942711606274951887866922567466153200711030384230/860741011335029703623751076469577548869873921666660831220041079029781231105100461515314785085630054931818856821980313649488067*y^6 - 2554626713470958467204103412165372308007385719855302794313476806684428264554482357708575901747845618620730504150655554924997686/146163567962552213822901126192947130940167269716980141150573013420151529810300078370525152184352273478988107762223072129158351*y^5 + 95509738272983735194214843444564432628417511693451215195280278247425338104054307518508716221857833673888457154268205667408784956/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^4 - 57477741900730060080812480296053976969885534633726155178440230734105254660478808025313483379716585501106534665213392997977849761/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^3 + 12457295309566734261320495861413434994454212661500198664587188466957653187023612471259745506959123530790582542394978265168886558/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y^2 + 20335450692792273014820583821311761423842152857521509226340593110458759316777154577926161554068779425525017007554919532233014343/7746669102015267332613759688226197939828865294999947480980369711268031079945904153637833065770670494386369711397822822845392603*y + 17397495459651928926331950185892385906346103836304197330138518086202249201054577412354845422407077200253227633910048281160368/2582223034005089110871253229408732646609621764999982493660123237089343693315301384545944355256890164795456570465940940948464201 336575832801607081514247781135500084617261696887570054768690765942951645331906200201569729157689364578819802422271211204203127/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^24 + 26616933021399787519191081038501972348867548455913878866323200529374851783775953774615898218153624330073800910820350883843324/1367169073723493392780496410633144490187652625972702201781413258994382872666351730812619171475344836161662132311406784931557855801019*y^23 + 47621688594317073655564591654299780887237359607724544513792584617105953970039190199839136334423130532780802636321901890807904496/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^22 + 21735281848705880101054087217629913901700059855041987489793955073983677143907640356181884181628100216282462319561003774157928214/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^21 + 776510554368681785043243732496855462934420460021020585600467784156638707426934249097156877785068416368747733875987531928288829817/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^20 + 775075521090690230723399618158896322618950786116501194066104083914540312571493832572667373394482656647936558962908200968250566260/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^19 + 18465561453158732970632489309005399550924106452529138650265218231374939309231524671848069674174583976985409529857036939969468280803/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^18 + 8917135194175365821576043395140063734517476272228342004254554579045495681910280286171339281249038985538822658596430253300296119931/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^17 + 246191877246011987538500379076225065175621323331057431375623377009022373891458937978701008787607851460424256447265760341357029125180/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^16 - 126133747893885837389026377171714560942500828826279434051916152356102669669063210437132680314081354764426380815040795245808307928430/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^15 + 1994318634160736802460522276895812310788609138038936901595610337121065320921763849753880636929710244928307241106719991047590324893636/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^14 - 5696364093645047861702698905244515032170077085429826189707473880407271565497364818123805149596865646917250273886799525145042815130804/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^13 + 32395541837150094501544316381805215559702902397567915822248868795910616908861414517933026850146143216708512754077920937294790720543245/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^12 - 1069532780248071838573573605157898978454168367935029545558076637325149983542019693263066626852685850891308555580642164528494191082682/455723024574497797593498803544381496729217541990900733927137752998127624222117243604206390491781612053887377437135594977185951933673*y^11 + 134884325651182736851046444004670747632835777245352587749597462186961403512683216236781349218156544744073190753378811820316665976047619/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^10 - 14958322235137610737053978730963022933426400157414227104307680718362607567121990117263048074555999410088445901917099755127949825078510/1367169073723493392780496410633144490187652625972702201781413258994382872666351730812619171475344836161662132311406784931557855801019*y^9 + 451576437768166772775607345065022412271349057332212157931758477063326035770459576322242242467167186205120206027649917690940049837496566/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^8 - 4265802697157373268103090730603117331744342575624590780079453103291374252830637740233173385437544491839662413786043464788850187433160/151907674858165932531166267848127165576405847330300244642379250999375874740705747868068796830593870684629125812378531659061983977891*y^7 + 310314648501476751880883145257724309484883134126443033529743349650874156295269103082147445732695373982616426380341333302924667216561196/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441*y^6 - 17507418516369692378438762556281829061230109273451407255810940777350229033355473061321617432623992785566966005352591703879935291072325/438525929307535616552234697750253893079058389462942215665736328356688845949584517430462753114733249334872759420639912147858180162591*y^5 + 702553566469438568925223877553910367256561429996728177692986106683744504056079142295691188505586123489297282420430319726701973153195308/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^4 - 300005243595215518053156490305210182890107177083348196021666688453301811756698712374138865643745980083211232052167599617121550189737577/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^3 + 100235967542882391969507634127481402516826656894662651802598794993807413015437903770902370994592133014797080268202035370285845785023231/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y^2 + 17036764510717743238792791189103341174422426192905539977883959335257036020436231804464090185392413670042027050956973088362827271100871/23241874253299387677268438980763456333190094641535937430284025402904508835327979423814525915080862214748256249293915343836483548617323*y + 6298584814928445370255561529253346148416493359218912227181273862455033843721501011193738465539864178093061822170507521089133866269759/7747291417766462559089479660254485444396698213845312476761341800968169611775993141271508638360287404916085416431305114612161182872441 -115062259845482250233353223691257391662858571327404070816073856291986957945722005019348850729622859120244977949016466620984/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^24 + 75102456106478667297566447299478729301703486004397019793030931695710353427692874248943009077202542253454878780479915681821/6617572703853698232624775627173011970052192233357142308849695857113944118378913621084170243556899309017786214404078603083195465563*y^23 - 14528145129175295413520226127980290400490137132040868465186672489112674024040528996801655621890237242533238689107153592119031/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^22 + 59802474470103583666438627905972419196263661378803669313353982067771101677084189838292227037926325297864151208237040746681226/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^21 - 181580375714896591801588246316057616506408111701099861759343577820682521428896768702029299013721807837640272379823837278245200/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^20 + 2997869956329213974082461208054225832170093814261014791783940356362373279549084828781306030740557149042419420090427057999978319/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^19 - 3474631468468713870676994482046781638417160915062246678591813852423103164490278105944795303062801739495383515968083981110069444/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^18 + 73681924001278798723259106818588093788689750106960671865739663080098664739786003593352117317937874744533897815205848697601818496/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^17 - 58112124758512305496814293093628875788351498197805377651875100279917223032362143104705472925824894224470002763437941751191884919/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^16 + 3070098896885218434860143450216571673966881088251055286564757626429064138991699585079574665550464397436240672561325853010803261446/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^15 - 1026181904123367464243864403819662184884822103583058460892065691700639896770414662511148027545833220372403785238546584289509816436/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^14 + 26143425445689521353217047436214262237441428088576615219318956263317374381547840473697924356877055379923932488257074167903751927901/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^13 - 39039877034063482161310372443470532809910175155939190694271522194186375236004184614552403828346681766269786302830819675476934854664/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^12 + 2929430431234896375124960196341587763452693036768740937313615213930753539308116931833348811825342876228851580254556120587512711432/2205857567951232744208258542391003990017397411119047436283231952371314706126304540361390081185633103005928738134692867694398488521*y^11 - 291479349860862999893657337275005568750579052193770892975956995573306724733345271836019468960375866236568906427601246233058094010225/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^10 + 37810819204073199556142627803757979174770729972327428726111879297872473514231958768828778905618751227967636572906031371027010227267/6617572703853698232624775627173011970052192233357142308849695857113944118378913621084170243556899309017786214404078603083195465563*y^9 - 1244986630259089375345468121697193254804115966935370411644021764942248875900503993581885240175423882206635785916123229793223595115333/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^8 + 41652130749429660862304201050622206768470512166044737261756382677991145450297707674582969290833243280250913813517090469037184484576/2205857567951232744208258542391003990017397411119047436283231952371314706126304540361390081185633103005928738134692867694398488521*y^7 - 1012606011304297895077633309239453878917369505142053365608378080294307662260081385295517968661955522615951403222384354265799649586786/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857*y^6 + 78750272132699890225962910314394506610449106673816623167264777521004177901917610748048646977246379822260357595492637681299063875162/2122617659726657923672097842678135914922401282397573948121600557942208490800783614310016870574854495345327653676779929290836281407*y^5 - 4092923621834042878522506108942327271906182314408651864250925173054801973303176218308836151476642944937768573601093131627763801288646/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^4 + 2760895230418316741907421128997089396706344765875030201388477791039656088274804914023179921061955364232952817484260229645485977464925/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^3 - 1179678357307378575297162125191573141155420585992623396856322609709725586831830050028222255117469420141111621749291568724822973362546/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y^2 + 456686192809825380639797552876501672023278040446759392418468408978130294486315578051761189505129257000759707305654682680271417664300/112498735965512869954621185661941203490887267967071419250444829570937050012441531558430894140467288253302365644869336252414322914571*y + 1079774924886343427817491634339703402837809212643594181717229351939115272826877546933861680949602344275014079387070990258582175009/37499578655170956651540395220647067830295755989023806416814943190312350004147177186143631380155762751100788548289778750804774304857 -320029891158191073255132016904567238042813317753358250158730713407584312989996139163821383647554601173870590451318786/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^24 - 29312023777092092913385168959193764381966044742404542057246341044499164083664187881883819279296069263941476400944333/623374032511086129605999813971690507751578441699521001124999574416032113941088287892317781103296893408414718870026782235889*y^23 - 45278829751019881089051467320971208592462194651518912673308277950999182839471723390068123956789975253841972520009620444/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^22 - 23815362298703358138609953185230434809914029455204532353430881961390919914595259372309329510547274746650468716221379735/3532452850896154734433998945839579543925611169630619006374997588357515312332833631389800759585349062647683406930151766003371*y^21 - 738316079867648577270378056064430132599533965063409470281393768308285118108945964379021862906547048864586513371091432536/3532452850896154734433998945839579543925611169630619006374997588357515312332833631389800759585349062647683406930151766003371*y^20 - 2655653173677893609269089075799915692360812056489352555809266876263065477632720487527053583026036749222165452547884380162/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^19 - 52490587556522353427160656099558723514816074576215964288042015441159971735845713160269341658714144871918713904431364101102/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^18 - 35593965129011768310423513820489568971798003872151795178042465124095937554258324150415289373351831658338297692215895517471/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^17 - 692114425039238502513004162254977054818061912604664952776825328123276369902387258246241872428565272214927745336236611735659/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^16 - 12587387714996482554921271024126444507982980042159665986516933869372016285827856309259895255515659784590498541867496458154/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^15 - 5458606515602602132697976684938620787114536484106211578534780390913271005583557133304547170642561458705212250034397517441315/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^14 + 4296518809694618500133758748885566689204107545866447719069874401858181955815053535899832670481951803557018282025605524921663/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^13 - 3119525811036316500376392163334518574645043170280847576200226794661835833841093713917881599943357072690587452816994785510727/1177484283632051578144666315279859847975203723210206335458332529452505104110944543796600253195116354215894468976717255334457*y^12 + 2632947559257415684382373950396490059143602695760573468078342720166307958098205846367863421317804608644414183561499297077181/623374032511086129605999813971690507751578441699521001124999574416032113941088287892317781103296893408414718870026782235889*y^11 - 109709588818194162880035950676888475573160491336131698230493539716132444402165914731575348810346321208624456615753688446463905/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^10 + 12070419203717480394290970766322975065095031469670199720287676580655924808007387035403348056447689772677015881635089784480780/623374032511086129605999813971690507751578441699521001124999574416032113941088287892317781103296893408414718870026782235889*y^9 - 39150819500366842675929455912851499851867003015935996738880824883263152001765626128970379931772366558084024303387106558349730/1177484283632051578144666315279859847975203723210206335458332529452505104110944543796600253195116354215894468976717255334457*y^8 + 28499091497249610752354166280349735156285243190186211155520830121355800645726334688879416441661956488357434281428744663176751/623374032511086129605999813971690507751578441699521001124999574416032113941088287892317781103296893408414718870026782235889*y^7 - 75530203029705854514094262030561015079452571036484957012536132208607714303609266353573694804031624417246166548911092972640494/1177484283632051578144666315279859847975203723210206335458332529452505104110944543796600253195116354215894468976717255334457*y^6 + 1260532665198306644138494688972699292876690110070133793430649631893563647557332669293890247121609829466415490117969876341383/22216684596831161851786156892072827320286862702079364819968538291556700077564991392388684022549365173884801301447495383669*y^5 - 352915592831685859155146032239805511017235704752837072810799396378924169011087131591651308750337366310086443821426729088477222/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^4 + 62861820240512718910350102598308525057107916876271639025585605812125999859632830211698359832234266356807621395046020180575446/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^3 - 17152966420109421300497762507058207888446477945422267830379563829103587600506412737930356974582837190566322820814633122462965/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y^2 - 5686822403931268633832545269571355685147519740192524586153274622961446350290012864887640814051549319281288001420288795420609/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113*y - 6986112438538022196013048212941965725717576488676752532628496354039811857823458110069664953755175561530627547316212605474892/10597358552688464203301996837518738631776833508891857019124992765072545936998500894169402278756047187943050220790455298010113 # A Gluing Matrix {{2,1,0,0,0,0,0,0},{2,1,-4,-2,-2,2,0,-1},{0,-2,-4,-2,-2,2,0,-1},{0,-1,-2,-1,0,1,0,0},{0,-1,-2,0,-1,1,0,0},{0,1,2,1,1,0,0,0},{0,-1,-2,0,0,0,2,1},{0,-1,-2,0,0,0,2,0}} # B Gluing Matrix {{1,0,0,0,0,0,0,0},{0,2,0,0,0,0,0,1},{0,0,1,0,0,0,0,1},{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,1},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {2, -1, -3, -1, -1, 2, 1, 0} # f Combinatorial flattening {0, 0, 0, 0, 2, 1, 0, -1} # f' Combinatorial flattening {2, 0, -2, -2, 0, 0, 2, 0} # 1 Loop Invariant -14866516623803357498756748700036182004710334796920499350185264937830732760067911449779222399740249268427843481491168257/101263648392356435720441303114067946925867520196077744849416597532915438953541230766507621774780006462566924331997683958763302*y^24 + 2984104369903447011779303617469862673047167003988366224589427253537719177167315614680445782096482838266117246886999285/911372835531207921483971728026611522332807681764699703644749377796238950581871076898568595973020058163102318987979155628869718*y^23 - 18455789456143879147758386830147986556457149971882735636729174749563697564027289984778424970105877000669508491132260196523/911372835531207921483971728026611522332807681764699703644749377796238950581871076898568595973020058163102318987979155628869718*y^22 + 291747687278454061275336495765911869604968588239781418917264188770838605834967582341015458204067942200151654873879444351/911372835531207921483971728026611522332807681764699703644749377796238950581871076898568595973020058163102318987979155628869718*y^21 - 143039702327359752189150316350284196948423391560928274340100655609969528552522061106707404457489166361474021865078883239851/151895472588534653580661954671101920388801280294116617274124896299373158430311846149761432662170009693850386497996525938144953*y^20 + 130009470738403239840417182199970177887407458841320746036274795061128915356559720656415437519343751045343792624398703595385/303790945177069307161323909342203840777602560588233234548249792598746316860623692299522865324340019387700772995993051876289906*y^19 - 2131094988057799301073999631634769519162928908554474589885818489223957892018948317879138316124158110605749626250496779599791/101263648392356435720441303114067946925867520196077744849416597532915438953541230766507621774780006462566924331997683958763302*y^18 + 3539841968979019267541846853699052334663541576717812246124779026836784232530221584787281755598977120862102153902094170661495/151895472588534653580661954671101920388801280294116617274124896299373158430311846149761432662170009693850386497996525938144953*y^17 - 40309632413050164580401935186099448029999899471512124653140468285206780713270985634811872767410963224600372136942029769266012/151895472588534653580661954671101920388801280294116617274124896299373158430311846149761432662170009693850386497996525938144953*y^16 + 78957301676448935734269200111533578122999557457721514772598917049161113605227811945889017104886994171721763700503109262264773/151895472588534653580661954671101920388801280294116617274124896299373158430311846149761432662170009693850386497996525938144953*y^15 - 979822716267816405461405115165230529776019404868453560944630213481486566724866034011627854889237461368117135124600553876294672/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^14 + 304473960103386476549060100673039820866027810238695571781181955887687063085201082253935809206394544526800971538346886996206343/50631824196178217860220651557033973462933760098038872424708298766457719476770615383253810887390003231283462165998841979381651*y^13 - 12159729627056568433162457825444456706744701196633170209545026014650769566878401883735775142805193766550454584624950872017421145/911372835531207921483971728026611522332807681764699703644749377796238950581871076898568595973020058163102318987979155628869718*y^12 + 17938264765200982848360675365470873946467613708443825588313109458844582073070482841583254768367991720341308314960657028930128007/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^11 - 21240929148210236211230811776272798793565834959813437125749089573715615022370645167353592633950761730161985801463505944226388305/303790945177069307161323909342203840777602560588233234548249792598746316860623692299522865324340019387700772995993051876289906*y^10 + 70541949310404756799432678015437238664348202207522444341433367866662978150732493061776017051959597325072476595912405637130973525/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^9 - 120406011652459238620983196510447649099456440016544263864445541340973044438432132581064901749173987668775184992084911561235727147/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^8 + 178427919379531836906981862709211904785008056342505179937458778477607104953678914691566650937503021580094164592048132872572452493/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y^7 - 26441684305751389418228589039805466876361388013974872362886064706084347480418179763743129120977816774582670816730274059596634975/50631824196178217860220651557033973462933760098038872424708298766457719476770615383253810887390003231283462165998841979381651*y^6 + 1118152934701358132628744978887628124092267125369708526075467330308210426681653953976532603542240432267742584957663415393419425/1910634875327479919253609492718263149544670192378825374517294293073876206670589259745426825939245404954092911924484602995534*y^5 - 9210557715351981794343403623014449129882643195934211185641886042874859367315402590377345225489886323444065880625630961446693342/26805083397976703573057992000782691833317872993079403048374981699889380899466796379369664587441766416561832911411151636143227*y^4 + 89065050934487986554813528945951237974140626174812286152219809981577157919147403565677685523903143383479955752520612162374453591/911372835531207921483971728026611522332807681764699703644749377796238950581871076898568595973020058163102318987979155628869718*y^3 + 204054482012200756251853248940760802484930441909152601425644618543564934685678194207824519959237292221766351412475262531402705/26805083397976703573057992000782691833317872993079403048374981699889380899466796379369664587441766416561832911411151636143227*y^2 + 14604737101381072201213007108730580681352805519893802018924995811346171624236100585291690923445246785249868624561609691023837352/455686417765603960741985864013305761166403840882349851822374688898119475290935538449284297986510029081551159493989577814434859*y + 3795559981374391532761987130123931957342147762012988420563980062738226658085632554793151349897405420600698132984585829565982931/911372835531207921483971728026611522332807681764699703644749377796238950581871076898568595973020058163102318987979155628869718 # 2 Loop Invariant -1629630909934623669077441346824614337428175910702057284071420185126138737312650609756545687939387405132841130531681463217430658585623348905019158992582846519756801801262837319459792809305089/2373246025883377309836248996678295554582117286283947634845467565649518610895215652059723520511061090204409011417295511179788937627502385784483048619345251832383656989259916601879040132348722059416728*y^24 + 1400149088226540527496026711444213809917413543934337386877653477107854298921376909167134054816037070573208161918731861699998613574926241112368834256555877216246721662333346057098288554438/1113851388868919263064572432733868376681219001697722607092678769860537520758079936824025432029596882135986707486215039665107448823921645393217951479667671385661916609477432698003304192278811980327*y^23 - 581467760882000618623664111809695635312454480702575258314501576999821894751299284484604091735607400315015270356618477298899494176370496307620403844093311589489512352760426287089470782399612/6311824536923875824032577118825254134526907676287094773525179695876379284295786308669477448167715665437258009088551891435608876668889323894901725051450137852084194120372118622018723756246601221853*y^22 + 59484930974589737360936996932311912906616713646206387191634828799147073425574592482518818510697005114327157846320070319329271874972209007026220880067785205365346713285878045201245668691806199/331150608262796833930639394885343565755644272504736879280762916137142131752820788659496305187589919563405908569855187606482177343372425923416239342234221185913998649664174409564517227769589124569776*y^21 - 19132169021604163597672289908991013050538084694644709316400236104493882120131448908791244497595125999292071081373174205078929747808882155961282546725349221216183399493745143792301166095783847817/4746492051766754619672497993356591109164234572567895269690935131299037221790431304119447041022122180408818022834591022359577875255004771568966097238690503664767313978519833203758080264697444118833456*y^20 + 155873714300090743864111072480144503090093893211996836218576186033547745551355557081142174715870074844961404730452293138172249033168354466062078553835567107795731968008828237725294066121406877501/14239476155300263859017493980069773327492703717703685809072805393897111665371293912358341123066366541226454068503773067078733625765014314706898291716071510994301941935559499611274240794092332356500368*y^19 - 1183379132704875552645626602186489681108236516765221114154867120641290649039146770456099010432791070918601041313905913863974326640392148967334784005212282285389262920534041956905268533201790853275/14239476155300263859017493980069773327492703717703685809072805393897111665371293912358341123066366541226454068503773067078733625765014314706898291716071510994301941935559499611274240794092332356500368*y^18 + 259709304201435401030851184971219321679723552852442135072904255436242478898238487186636600694004617925100334292350743588012450673555800415113674877595614638261189628130237137450338182788799870667/791082008627792436612082998892765184860705762094649211615155855216506203631738550686574506837020363401469670472431837059929645875834128594827682873115083944127885663086638867293013377449574019805576*y^17 - 6950164245010037391146498416924092162696687842381835242878192973762347543087393433230931145038968614409921757807998963566541516530594122580194203579398034097071423186761515808894314509920003061001/7119738077650131929508746990034886663746351858851842904536402696948555832685646956179170561533183270613227034251886533539366812882507157353449145858035755497150970967779749805637120397046166178250184*y^16 + 38699928252287434864872765937910003291218329829394413972723834930470953566843700240607654718329275895552646356147264530719066544360114839235633088515555954782380569592356182784406620563368185498081/7119738077650131929508746990034886663746351858851842904536402696948555832685646956179170561533183270613227034251886533539366812882507157353449145858035755497150970967779749805637120397046166178250184*y^15 - 58785669745720273402519971413802458906900222185789293212259630753822733953767773303125059588954350388020330074367887125510032214859493284712423831148327021346058763010964567060225096985244859758997/7119738077650131929508746990034886663746351858851842904536402696948555832685646956179170561533183270613227034251886533539366812882507157353449145858035755497150970967779749805637120397046166178250184*y^14 + 83224091859927455925921322683668039940640909244273620035281454538571085386461338417929117890378917954558267609553071860918111033649927545932099643525342700629274340825352626370423044348924980107485/1582164017255584873224165997785530369721411524189298423230311710433012407263477101373149013674040726802939340944863674119859291751668257189655365746230167888255771326173277734586026754899148039611152*y^13 - 466915087622169471092662037974530908056217109731448828242702157502714251063467574958914127233357182930313102177932084158374472518602020993659259429527381316171890218306138062571286878208746662159247/7119738077650131929508746990034886663746351858851842904536402696948555832685646956179170561533183270613227034251886533539366812882507157353449145858035755497150970967779749805637120397046166178250184*y^12 + 9598095479833192267782165215648497653847052848685726158470779716775654331331380107066234263793650683401451997152030798520223967153279015223746735872690309832338339431181841097955261361961266309719/31022823867756566141650313682069222935713951454692125945692386479078674652225041203395078699490994643194889038134581845487437093169965827248144426396669958593250418160260347736980916762728392933552*y^11 - 792928047630968539789946632602437983641830030771417756281918839098027512874248433357013215160040436403087767325596794604144083248810362482125920658226894595455390440255880922264247025434282445212721/1779934519412532982377186747508721665936587964712960726134100674237138958171411739044792640383295817653306758562971633384841703220626789338362286464508938874287742741944937451409280099261541544562546*y^10 + 491534606255040924424733985216310879651441300762434125918170829420330447233535871604580985339070312842758017834848524188860675525368670042311955062990474927965524059538361533950954034881596033861027/418808122214713642912279234707934509632138344638343700266847217467562107805038056245833562443128427683131002014816854914080400757794538667849949756355044441008880645163514694449242376296833304602952*y^9 - 2290680325772146820779019416778779286362808504622471857092440168049653510849283045994875944138532668824066740221263524327843897404976785422051828379849436464362271182540709209635084231019915767921463/1186623012941688654918124498339147777291058643141973817422733782824759305447607826029861760255530545102204505708647755589894468813751192892241524309672625916191828494629958300939520066174361029708364*y^8 + 2627580247043474561301872997808803144133643175107908455999978542337431202765720450903037155075451293136276878929040506659865556681667874983134347722885976707547904612831786362064646543708894391952115/837616244429427285824558469415869019264276689276687400533694434935124215610076112491667124886256855366262004029633709828160801515589077335699899512710088882017761290327029388898484752593666609205904*y^7 - 15170679041152502095079546933610635787211917141148296534009039383175306638877207156137578729059836917285290715829189425355358654213744256146072951503791280131364150151717739105424290357626784062699733/3559869038825065964754373495017443331873175929425921452268201348474277916342823478089585280766591635306613517125943266769683406441253578676724572929017877748575485483889874902818560198523083089125092*y^6 + 1438960949122034784658455553766633109254471500435856026958060750731636711891285805747658349868110305629975632724632380629737841737937184133068447661691200955046295163554640938523354341263159634402033/268669361420759695453160263774901383537598183352899732246656705545228521988137620987893228737101255494838756009505152209032709920094609711450911164454179452722678149727537728514608316869666648235856*y^5 - 55669494264411256192521498369017826021350775443041646829156552282318841554821794612645406986903943182752730741316493753355571574283558094259343846037912180375449145537269790264957970440150089177528739/14239476155300263859017493980069773327492703717703685809072805393897111665371293912358341123066366541226454068503773067078733625765014314706898291716071510994301941935559499611274240794092332356500368*y^4 + 34250751558144286150152806180525254603555224510595566996923531824335193422893362587195268119080271255231827118657431207555099866320430340269412153813751026800898629247825896736431938399753973533483511/14239476155300263859017493980069773327492703717703685809072805393897111665371293912358341123066366541226454068503773067078733625765014314706898291716071510994301941935559499611274240794092332356500368*y^3 - 1435698873639079584157874117437577620659019792876194917833052138864322597595706068266491092334659522338109093099907634969665602256644765570480785583276499746117600570684914728522841531976364482351877/2373246025883377309836248996678295554582117286283947634845467565649518610895215652059723520511061090204409011417295511179788937627502385784483048619345251832383656989259916601879040132348722059416728*y^2 + 6019246110554138531506814469875274374558628044227661701435476826580678523657308558730313693648063460783336758100021631959742857274335155366555396482058212822128225649477210591338738366649198098943037/14239476155300263859017493980069773327492703717703685809072805393897111665371293912358341123066366541226454068503773067078733625765014314706898291716071510994301941935559499611274240794092332356500368*y - 1866421222108882373347652717175557820867843669398654127083230528188148119263321365987976239352735102633096915574012086054471625915627845497628143558824499704708739990609560992019055981773402944686745/14239476155300263859017493980069773327492703717703685809072805393897111665371293912358341123066366541226454068503773067078733625765014314706898291716071510994301941935559499611274240794092332356500368 # 3 Loop Invariant -89398417468968388462154980789576781569162957415224499615494552274565728689284124222122501473743328403064915176479566895074311625081086993645467267471281040933479006499163333079368191840065990853400807271969289217042416024910399637/67333612455297268482747397543090372658726064827997297725189397019950485960657751192032137012571462769448908239542817445140514727233538445618075220625127889235103897180157214644251032246313630977939215443017955398867057318874167623297690432*y^24 - 313617330806562089635585014954053373186002306155373388056722418997460615405398435197114258518827731789768663995340550243770445369729807489562212976563478012313212141658399232374914908259593226373674340107882283834624699878931849105/202000837365891805448242192629271117976178194483991893175568191059851457881973253576096411037714388308346724718628452335421544181700615336854225661875383667705311691540471643932753096738940892933817646329053866196601171956622502869893071296*y^23 - 9504257211880324804145391199631458600406213081785948953544455199210788411117631893618242594612818353788185719890796164598779728812968003181318856594871455344284644522437555458831260466806074537490846892984130708401789651151409789957/50500209341472951362060548157317779494044548620997973293892047764962864470493313394024102759428597077086681179657113083855386045425153834213556415468845916926327922885117910983188274184735223233454411582263466549150292989155625717473267824*y^22 - 5684335886038768212871527144615946754425250853198250141951769724900716389497786137557100733392288669725897999330434086666649558025836262008042468644107359362400984535036916318224033446173497697928891004040403822201035321698240942267/25250104670736475681030274078658889747022274310498986646946023882481432235246656697012051379714298538543340589828556541927693022712576917106778207734422958463163961442558955491594137092367611616727205791131733274575146494577812858736633912*y^21 - 207314864002924058643689343935259953346492046169993454171730207480166420042235126186309882185096819442605183612578925931721258264453903634468418209852772028835440283541367353414320318361677508442006641511532244444921228405364026359561/22444537485099089494249132514363457552908688275999099241729799006650161986885917064010712337523820923149636079847605815046838242411179481872691740208375963078367965726719071548083677415437876992646405147672651799622352439624722541099230144*y^20 - 48442300541182749528621752882446018394007906270783785528156144211289445055472566821742934846533264987248610829134248180240031206291483428444704332013460868473038869668011167720907199417362326055394301354989687040244495530536096104751/6312526167684118920257568519664722436755568577624746661736505970620358058811664174253012844928574634635835147457139135481923255678144229276694551933605739615790990360639738872898534273091902904181801447782933318643786623644453214684158478*y^19 - 44710292385693562919386939326609168480306879378240575258584113498513175532715312382960969725911765042674972222636690167251303926721801498605507432554086862209237180141823827141419483169701092131951863141076311065420840383299044866847251/202000837365891805448242192629271117976178194483991893175568191059851457881973253576096411037714388308346724718628452335421544181700615336854225661875383667705311691540471643932753096738940892933817646329053866196601171956622502869893071296*y^18 - 264394339224700609361863225459752429521338489563399076139865502089678221958403183629459910851264230510197555606312403905305325361971322671727049697450512823890721237790844048301277497992947914401285460029808088970955394761749536671447/3740756247516514915708188752393909592151448045999849873621633167775026997814319510668452056253970153858272679974600969174473040401863246978781956701395993846394660954453178591347279569239646165441067524612108633270392073270787090183205024*y^17 - 37824541242443732581031301425873626102669690781056472487520472827181456083051443106226468689460486786887399803427014673950095495627849933373730735129618016920959295376580708630818402187118282295610160826482409313195560088742496420741203/12625052335368237840515137039329444873511137155249493323473011941240716117623328348506025689857149269271670294914278270963846511356288458553389103867211479231581980721279477745797068546183805808363602895565866637287573247288906429368316956*y^16 + 50073337665211282021322094603904811100115625275490107538612116235832763023250345970743465771178686743938427279332021873156651920358681915977259388968244473985495708947960608278854725087308351704025421946576147429733755181031265072887403/50500209341472951362060548157317779494044548620997973293892047764962864470493313394024102759428597077086681179657113083855386045425153834213556415468845916926327922885117910983188274184735223233454411582263466549150292989155625717473267824*y^15 - 629992725912381925279862422905086884194974233242551399022332019506833552746364915562398995925353107871422675314810788885680667707668104094210457205139825438408778345694540867246374663657066703914728500066916358259755843867436110212607155/25250104670736475681030274078658889747022274310498986646946023882481432235246656697012051379714298538543340589828556541927693022712576917106778207734422958463163961442558955491594137092367611616727205791131733274575146494577812858736633912*y^14 + 2774338462817259807069046026460489055051787933933481505358034603544373395787762073584239079962180301813099593979214340549868278583797767136526930494162133227354878318003265758946945829503036704873520853357752984636427291762158323189373869/101000418682945902724121096314635558988089097241995946587784095529925728940986626788048205518857194154173362359314226167710772090850307668427112830937691833852655845770235821966376548369470446466908823164526933098300585978311251434946535648*y^13 - 14238025554312223063384697181997162265913813807747327430732264472659578224201974101120257698278841621764347859967612776553474931586451566151255800624162298028974765397223883162868096542019498279687262767315185068491474562936280038009767599/101000418682945902724121096314635558988089097241995946587784095529925728940986626788048205518857194154173362359314226167710772090850307668427112830937691833852655845770235821966376548369470446466908823164526933098300585978311251434946535648*y^12 + 2856371759391120385548733064511645136182898946777847411364408677822017766549521610395756408622941960175957798148482788846541341413959280223153390904333676136384264376773956973045415635684107716263467624442364998511813033914201424731838157/11222268742549544747124566257181728776454344137999549620864899503325080993442958532005356168761910461574818039923802907523419121205589740936345870104187981539183982863359535774041838707718938496323202573836325899811176219812361270549615072*y^11 - 62055203356017967573142123821060803417897249442531174649486545788529535489722475477381342246671016294927846177516870503598732318429199115148554416212317455293461250577792021576632723467679319585830150263115310666866428321721084172465399121/101000418682945902724121096314635558988089097241995946587784095529925728940986626788048205518857194154173362359314226167710772090850307668427112830937691833852655845770235821966376548369470446466908823164526933098300585978311251434946535648*y^10 + 82929740272385827602175151041496582665826987491377054279618360108611508573154527596668242894135219208573510894881525527738613960006351773539163542297486147135467748205236540823332853115619990063982079209152633723450323260442792234718665367/67333612455297268482747397543090372658726064827997297725189397019950485960657751192032137012571462769448908239542817445140514727233538445618075220625127889235103897180157214644251032246313630977939215443017955398867057318874167623297690432*y^9 - 25442409030508046211008237891364894074201227743462251965397586077246479453445633159153429194690713319888438346329143249965687197232775443648288530379291978183071744930828961300787685133421961421988007266227620464492574219070818244550497323/11882402197993635614602481919368889292716364381411287833856952415285379875410191386829200649277316959314513218742850137377737893041212666873777980110316686335606570090615979054867829219937699584342214489944345070388304232742500168817239488*y^8 + 77141844440098176039205025759668236690608774974951943897108252181982340382190105345908125962634769186709460031533021602630886614463943412484240229788568005272269376419086151314039649559998264100616293679121010457965154317229745540087878239/22444537485099089494249132514363457552908688275999099241729799006650161986885917064010712337523820923149636079847605815046838242411179481872691740208375963078367965726719071548083677415437876992646405147672651799622352439624722541099230144*y^7 - 57297774714470173250095921972778495764467012071883272987448872018093997327073763415291841209842735356477664150590642186482508288094780160052379367850141605337079416073488681176108496478588805691025738746552733188247189686262548475297255269/11882402197993635614602481919368889292716364381411287833856952415285379875410191386829200649277316959314513218742850137377737893041212666873777980110316686335606570090615979054867829219937699584342214489944345070388304232742500168817239488*y^6 + 10502575024538999569263929841382764771080035484386552885290813809180174170246648237708006648454068559522668657445250472258209307667971404054787568680733618376994154862433823947491909548274619195306016930594190651516378730653274778504773397/1905668277036715145738133892728972811096020702679168803543096142074070357377106165812230292808626304795723818100268418258693813034911465442020996810145128940616148033400675886158048082442838612583185342726923266005671433553042479904651616*y^5 - 21239710438869373484386612542624359756324876573938679398082347368295452369144209915153713064987566226517129264489529492907316616151492682573141490519606551850666180835534785191005515919063109137891851145790880143606459003958730174631247721/4297890156721102243579621119771725914386770095404082833522727469358541657063260714385030022079029538475462228055924517774926471951076922060728205571816673780964078543414290296441555249764699849655694602745826940353216424608989422763682368*y^4 + 322399834207946562903538836586101529540885998746066273947451068657011946430031722769270092295292179441056152857468884083089831693164840389430032365748783235677903099977069721064579632377179724958082369977028828631775161753146797146773375039/101000418682945902724121096314635558988089097241995946587784095529925728940986626788048205518857194154173362359314226167710772090850307668427112830937691833852655845770235821966376548369470446466908823164526933098300585978311251434946535648*y^3 - 301085188639075391378417363612386303584103238502857433838469927647171026019630611940300551833314920459112783701722310898723113959042643129868764059509015159017647182872512578148413614764213485715097008583667855977432081361563954668651431849/202000837365891805448242192629271117976178194483991893175568191059851457881973253576096411037714388308346724718628452335421544181700615336854225661875383667705311691540471643932753096738940892933817646329053866196601171956622502869893071296*y^2 + 31540440656773889228138024401028666359472568661589668886639952818893901996634987751541032893295813333344740962403561555687018845448372753931660569423076155363425624419160277748259446665120718650118606662243821501910817944026294997824731019/67333612455297268482747397543090372658726064827997297725189397019950485960657751192032137012571462769448908239542817445140514727233538445618075220625127889235103897180157214644251032246313630977939215443017955398867057318874167623297690432*y - 15794602502626889346976282235172624015639305371097142444559371230309897851148215977843668790997797976545009130978650719784939048448712165361237916362649131843659458579173343699044289900338725170968665789246789510172319795836357694290244975/202000837365891805448242192629271117976178194483991893175568191059851457881973253576096411037714388308346724718628452335421544181700615336854225661875383667705311691540471643932753096738940892933817646329053866196601171956622502869893071296 # 4 Loop Invariant -368730542324938102277388837931745755998549660053140416178599026182086164595651725540526096145671058445598668110994579409002566382110301829316355226231531782281654512060255848550525144253315957490841721540559659977023939438563108493290544107305762218685374659411284594779546393605292353221955300085944465193/284049227209101600729563066333671588820039157848753362218522049733335571710236334726930454345324015637896517917138422984865696388017077638146948861796752407552813938866986897580786812976928838417985915902318154562870283001014033238650404740270022409511500235027129265278728052442178739104679496507759099282975728640*y^24 - 403268369135508777268976693271608648688181795418690557110683976806867712545031773675022151197243430961061524446547558743096067912073294067607095540114243807490951435979518824449157232318612349264639827841860329903128599423314394898646185384998527582900849735394651051424544827421784578481738831873748011/118501972135628535973952051036158359958297521004903363462045077068558853446072730382532521629254908484729460958338933243581850808517762886168939867249375222174724213127654108294028707958668685197324120109436026100488228202342108151293452123600343099504171979569098567074980414035118372592690653528476887477253120*y^23 - 382658635949357154032760063870089321554938754992533886542508568927326612215822330105051278093803838120980767020588969459324483974369186098817083861125338643832305794862292265761653153690831163036812172680559341503205966857711649594703110991927137429026876717120125521272041464903003734560912858054976368743/2014533526305685111557184867614692119291057857083357178854766310165500508583236416503052867697333444240400836291761865140891463744801969064871977743239378776970311623170119840998488035297367648354510041860412443708299879439815838571988686101205832691570923652674675640274667038597012334075741109984107087113303040*y^22 - 28214632603666221527459851497772956761040974870195834106343927650472494937897075129873887888890578327011352277745749564568245865302943437802575953905359261272812486406400048026828923003200353865624500253530634657234414362540369395352370563416462647215172930448265747793305474087222334855463171132824311389187/56809845441820320145912613266734317764007831569750672443704409946667114342047266945386090869064803127579303583427684596973139277603415527629389772359350481510562787773397379516157362595385767683597183180463630912574056600202806647730080948054004481902300047005425853055745610488435747820935899301551819856595145728*y^21 - 1404753711045538869990388899689801257436241904090968700876827302038198225246047073192095638016709537459755432544514801589834306484830916839027264542179058019219633219969668224991575834951196000529173925811673208362965929405639637330877461597543729314714956632699159625138205249260521934900973747276426136259029/142024613604550800364781533166835794410019578924376681109261024866667785855118167363465227172662007818948258958569211492432848194008538819073474430898376203776406969433493448790393406488464419208992957951159077281435141500507016619325202370135011204755750117513564632639364026221089369552339748253879549641487864320*y^20 - 3119544254545302726099579793933940386992381756810420964254400821831627019440515446104353182438704059673355116834225996265395802191381115712043026566815234571739254890774831237150966750945592123757979369625779407944029017478498271043544731529808133097314077188187583900867563746783189087416580859841392275410291/142024613604550800364781533166835794410019578924376681109261024866667785855118167363465227172662007818948258958569211492432848194008538819073474430898376203776406969433493448790393406488464419208992957951159077281435141500507016619325202370135011204755750117513564632639364026221089369552339748253879549641487864320*y^19 - 36196233293387059966198992723007428005952957249056744186929506029745431358001600533045510553558746252847409818115255583406923810211806804359458266445986480046686216225210086527968398951796424870392461837457006021888985338574576541082571055249746607321514552104055614517491483982870627740648615482324640646320029/142024613604550800364781533166835794410019578924376681109261024866667785855118167363465227172662007818948258958569211492432848194008538819073474430898376203776406969433493448790393406488464419208992957951159077281435141500507016619325202370135011204755750117513564632639364026221089369552339748253879549641487864320*y^18 - 62630484076873208852180605579817651169440806442387987551437809747795106715021299230509101473924683144464276796475009498868342772216544089223714827168544279108656762972055895397758493917576017807751474266447411315937360205229822595414041130311368861067556194187702834299358168738362430877805203999830899663412341/142024613604550800364781533166835794410019578924376681109261024866667785855118167363465227172662007818948258958569211492432848194008538819073474430898376203776406969433493448790393406488464419208992957951159077281435141500507016619325202370135011204755750117513564632639364026221089369552339748253879549641487864320*y^17 - 528014491369456184879668918805366805580091354239547310324731600117768025319798534594495222064876879345836830597131403674404184717304995915781997599353270745566560363852795387178656390590096353162372969914407937984330235434730305174752402451558551288253251301759547882663790538643219386876172613239554099024500697/142024613604550800364781533166835794410019578924376681109261024866667785855118167363465227172662007818948258958569211492432848194008538819073474430898376203776406969433493448790393406488464419208992957951159077281435141500507016619325202370135011204755750117513564632639364026221089369552339748253879549641487864320*y^16 - 413957548859645162316368497314448887010347527467881700500331024078373891220420302421658729286740844665473802073223579656661033463807093340450716815419983920797277101201859523994030498747970533669616473115111679233455905033398942476832018959886439099563184630291648824672845648512380179512709630439189024112388941/94683075736367200243187688777890529606679719282917787406174016577778523903412111575643484781774671879298839305712807661621898796005692546048982953932250802517604646288995632526928937658976279472661971967439384854290094333671344412883468246756674136503833411675709755092909350814059579701559832169253033094325242880*y^15 - 1028385433505117527292776899748707086657615645516861722485176215884787123452846214148492782213670079946490242269353589057808101162171746917768048463515868983610898169302893186799879727070129960231993042528002109202460278606964774261198552045509410642131915903617108402190636369492458558327327150918189680993825189/31561025245455733414395896259296843202226573094305929135391338859259507967804037191881161593924890626432946435237602553873966265335230848682994317977416934172534882096331877508976312552992093157553990655813128284763364777890448137627822748918891378834611137225236585030969783604686526567186610723084344364775080960*y^14 - 3952626179677745567149063251904103767982663701760641446806431821101716097994780965392629146009257955570724461536156939895800598027736529005764979899272528907344112194376807056822820908981816596845139532599309036564451302239909900542184342789783336792489196928107796255764505549678079131146403687827782840537527/219173786426775926488860390689561411126573424266013396773550964300413249776416924943619177735589518239117683578038906624124765731494658671409682763732062042864825570113415816034557726062445091371902712887591168644190033179794778733526546867492301241907021786286365173826179052810323101161018130021419058088715840*y^13 - 50490707919720550590284786320538437501738246255776857093142075635670767365454662203472573951251720572005025847192671999822636288070135448482364442505980424888638309447217922036210619268112120189798653890927337252909037671640418316901529864921158238544237213276809736749903370370886605621675853023939400255194743521/284049227209101600729563066333671588820039157848753362218522049733335571710236334726930454345324015637896517917138422984865696388017077638146948861796752407552813938866986897580786812976928838417985915902318154562870283001014033238650404740270022409511500235027129265278728052442178739104679496507759099282975728640*y^12 + 215279178770299606365190157870068598923759590956946832445666252080164163280207561452525257465333364551036798310733634607856593679315430364263253108521252108407929282254905799624407329491424106154102576974229825363592216589653062369722216893011545560194468553251223023161697156260775431544682603406784508952401897/8354389035561811786163619598049164377059975230845687124074177933333399167948127491968542774862471048173426997562894793672520482000502283474910260641080953163318057025499614634729023911086142306411350467715239840084420088265118624666188374713824188515044124559621448978786119189475845267784691073757620567146344960*y^11 - 180395846445750622730079388951018138953942488134962945638226898381263390274893432122140556083151739003459148338178359028717950204283477385857042377824713380830756375595912055323503954762630588281168406193211581833097683625580191839148402189590736465929411423634467892602988659572304396216594033752721725265540079617/284049227209101600729563066333671588820039157848753362218522049733335571710236334726930454345324015637896517917138422984865696388017077638146948861796752407552813938866986897580786812976928838417985915902318154562870283001014033238650404740270022409511500235027129265278728052442178739104679496507759099282975728640*y^10 + 2250228387836353700614512915263326132153549279465124790529539939236700675999233223220308979775965255524435535099118223610388086365755703588512028069749763813794750091810235069016756204124735325149590864430128806885609811877157159114460641797509137183593946761947482506043316148559580851327018156912006593969246209/4177194517780905893081809799024582188529987615422843562037088966666699583974063745984271387431235524086713498781447396836260241000251141737455130320540476581659028512749807317364511955543071153205675233857619920042210044132559312333094187356912094257522062279810724489393059594737922633892345536878810283573172480*y^9 - 93514146085851425321119228902071147738999095480927205786511394628683239581459259610046839617682648484566521951182840571345978468929732008147904900533120806588758658156370394756621142037195492118686207713080328631247397809649419674004031049455714074532736034250195552498873458081260810132303769313494330233920220873/56809845441820320145912613266734317764007831569750672443704409946667114342047266945386090869064803127579303583427684596973139277603415527629389772359350481510562787773397379516157362595385767683597183180463630912574056600202806647730080948054004481902300047005425853055745610488435747820935899301551819856595145728*y^8 + 1684048831128191708735428424962922774037371326606924538538833062443738023515513033668448939136351910470854436078414757605360428344998847571455620370718288454463816096391991032304935330323811619430999472493715951718625128063662515013842988278793472989680128109949756175850534445876672893255995406453579433543147109/835438903556181178616361959804916437705997523084568712407417793333339916794812749196854277486247104817342699756289479367252048200050228347491026064108095316331805702549961463472902391108614230641135046771523984008442008826511862466618837471382418851504412455962144897878611918947584526778469107375762056714634496*y^7 - 74290992872570608031833669882570206467873780473810808186104555547108635003919315817846544995220283757839366859892145926446551427060487110204877460785472134089912239129877665667034730994495595394269443679195178794741540470155437715345891797241348143261457512683797487152314971501300241767903988552727684203834481083/23670768934091800060796922194472632401669929820729446851543504144444630975853027893910871195443667969824709826428201915405474699001423136512245738483062700629401161572248908131732234414744069868165492991859846213572523583417836103220867061689168534125958352918927438773227337703514894925389958042313258273581310720*y^6 + 17772037198990011321088749682371446819008272346769013731249141637095376624532085358038472671334587274579867570498655077904351221492735856700619036566010272642907656978708001860216145727442313656028823079429925222222428498734050047555849129286704118448512776288285507232458302592363454486922726498557380669011659941/5359419381303803787350246534597577147547908638655723815443812259119539088872383674093027440477811615809368262587517414808786724302209012040508469090504762406656866771075224482656354961828846007886526715138078387978684584924793079974535938495660800179462268585417533307145812310229787530276971632221869797791994880*y^5 - 29845126983143072848261273754958190997080295630806165359179245886686236495899376060279019538286126353288052971241848231085401176096413098753471457164999203347465294633108655755076635847835059890118344463515172027762747971673851703092260422192440511313982694619333812920669854651818689088443082684976044326463076585/9468307573636720024318768877789052960667971928291778740617401657777852390341211157564348478177467187929883930571280766162189879600569254604898295393225080251760464628899563252692893765897627947266197196743938485429009433367134441288346824675667413650383341167570975509290935081405957970155983216925303309432524288*y^4 + 194510038306750135657228590218434966578824736021087619998828605899487063013089890210136933950069814759195622473757333298443569575191856736222138150341335339087507286732141949078293674825577299734738072741307804446945366492996105058383958881483547519117283957596980853392547098898101754320728551872297032445361809243/94683075736367200243187688777890529606679719282917787406174016577778523903412111575643484781774671879298839305712807661621898796005692546048982953932250802517604646288995632526928937658976279472661971967439384854290094333671344412883468246756674136503833411675709755092909350814059579701559832169253033094325242880*y^3 - 76223805626583030680822257113687767368375688965478550392970993164632978353171469560176221008328991949902827326612849573080265409702400302020366881933662934816486406456671149928009048346867607461242250791944199306996375084443921950649770868006133551269842262865760676250612122550025420578861203682809094686001240063/71012306802275400182390766583417897205009789462188340554630512433333892927559083681732613586331003909474129479284605746216424097004269409536737215449188101888203484716746724395196703244232209604496478975579538640717570750253508309662601185067505602377875058756782316319682013110544684776169874126939774820743932160*y^2 + 24741037087717072956599063982025731532979492060685347798401039410111730452686349982992945645188614116445733549029179039231540691560440264630239564382125629246366789107671643913053341432008450216820389128478180973957127539251978046073661562372105736513615765953574111015179003552126548394194622728772732757046515387/71012306802275400182390766583417897205009789462188340554630512433333892927559083681732613586331003909474129479284605746216424097004269409536737215449188101888203484716746724395196703244232209604496478975579538640717570750253508309662601185067505602377875058756782316319682013110544684776169874126939774820743932160*y - 24337088880342327413802064737040884500225534115719102939398989299554932090739156459609060539369825219736855053316202538380437178724792014451180997427525107403311573443109085238887477145986765952991482724489644752703855477734348314504159177981490058015033334610601653351876619157744174941694886887557790633860103219/284049227209101600729563066333671588820039157848753362218522049733335571710236334726930454345324015637896517917138422984865696388017077638146948861796752407552813938866986897580786812976928838417985915902318154562870283001014033238650404740270022409511500235027129265278728052442178739104679496507759099282975728640