# Manifold: Census Knot K8_161

# Number of Tetrahedra: 8

# Number Field
x^36 - 18*x^35 + 29*x^34 - 444*x^33 - 6174*x^32 + 56774*x^31 + 350408*x^30 - 606837*x^29 - 6271094*x^28 + 1232481*x^27 + 45631057*x^26 + 15715088*x^25 - 214541091*x^24 - 40403130*x^23 + 783086778*x^22 - 481580588*x^21 - 1826811382*x^20 + 2739679092*x^19 + 2093714544*x^18 - 5735310045*x^17 - 532348321*x^16 + 6072680880*x^15 - 1287852335*x^14 - 3512624673*x^13 + 1583948319*x^12 + 1083050139*x^11 - 858132099*x^10 - 135758410*x^9 + 263013456*x^8 - 12369368*x^7 - 48473024*x^6 + 5785376*x^5 + 5385344*x^4 - 596352*x^3 - 330496*x^2 + 18944*x + 8192 

# Approximate Field Generator
0.293842300012070 + 0.506909039195593*I

# Shape Parameters
5721244774633257051934613813200165251214526930357973228009905906672526917425926575879570158955167892153902372799420587895800938308602926087985579402490906814601803367589118589218657/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^35 - 52210909955001314526781319199648685441674279326594920493313591080873417307508411295726598945990017663844163389542752635668286302180263686431139387187584505402576171348587120568266329/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^34 + 195503971740868110233480775323296986345365278683805685230640027129657515069759060182288934059352181186754855041572665709127929296904232811789532502626649141552181148468103971372756097/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^33 - 662127739347340265431947762202339104197454888523792094368182221236619220453155039657795411554549309114576924455029036658547719172598542983486776734022961000503273026035187376625685687/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^32 - 17284992450513595581716539264575875433702318372579293744693896563047154644005480670948182641166977952594386636267317405057018129647752274956849894479168992277534247178770881178559671733/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^31 + 166018783285670613671527088044407894973367756303638508940847132221469025917421643151072034919223795295693386943543055036793662333640526669115766499988913906744703106365965411338588897167/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^30 + 14847813631265545313349628355262077837192699580407614073713993279272907090761256670078119491216074039697215091409876504054998471106906191027827130255435641249382736737584842105145317675/15203373576191475922769742183657190206555307641398649026204288330688712583417162811913109370532975089320520624199190109876285437779655416041161346424551140528482355815829135255636372*y^29 - 3766026547405960087960373737544621197976936490850228619432611392848670414448551798414396209600166435050323855522089089310937113106649540255123669307725721985839359868093331836659554821357/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^28 - 16871482027419051854082329180827088405147704077339029452341873717532339629770195832849752761578352134003339455851074880725214446086049322547527144230185157845130985977212475729844404046483/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^27 + 13809775733316050333619357079597614235178395735065513242612689647015197599112975055809960795398639026738339772554512582073405322584723578813751403523635968423407253021867342762825283212173/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^26 + 236908296699536281260845811709146180144820472404256781533470401174731831107979319321637351293210080802177395250515283542806270502731652696059709972244364325768865115497879708610882294182481/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^25 + 7506245463228044762030967913421227423386279257179541777747049749115360123612414285041001705802013716515285736760848204850591949608375655138495662532663489619393431414226066000749342226253/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^24 - 1091150025751345130713352847281999078490632554832831140252490288194994718717624355233110490083429711209355595956787404180059486767271675517179598882168296844533287711843435763196522884173207/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^23 + 60689593847524173311169559979215280399888644570667177724417131147496767031238661724203333026431996365940514625770147517704037752319643726946319405658438427127629945779227067904657789445247/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^22 + 1901987300393698546647592264531164884512261373149560797437371450603174610796351743845040611378842132809581770384744570907619994479221668652824014871426627269807174416595062534870616428031007/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^21 - 983682562382843147624314387265241272987709759946404999052667628433478641659802421197661520958163953464045799747223035013698999076623365246674190462917952450703059083178452078683479500822155/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^20 - 3568201708460711311052245989448661176580821746699922549566168493668130859273727405788241722915649906131893780168674235905365873857643703908227756514786438338394458044102924060907932741270055/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^19 + 4052902379884290163188504023623088134729318075422609984993288523398459487695875822693374901237342561583825527919392453933413453700591588857763326370503387535554469290243283993214214813246989/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^18 + 305836411137629458148976755456917040604063464437860269823258035704945990802860787482837764872938860668538688319576255404429345551865429095799356622467636406360406612637442359371831242843731/243253977219063614764315874938515043304884922262378384419268613291019401334674604990609749928527601429128329987187041758020567004474486656658581542792818248455717693053266164090181952*y^17 - 25772065151139909084098026495568053304400926864401304663951671735853183000582087629598643998959526990776391450877754150034484395230144713729389538888786920969797264459115834155971529174678749/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^16 + 9807156695145928785520527078992845446192176014448377937290087077600183415868562891547503978548262131998250209797066156480191116702885685101637515608850496711382165316397136987455021184127583/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^15 + 4282824613647471498218763338297189600996313659547469927898955520748927279356509360703536939456029205347769796527809210010089666446707584639918258577285873332038038218548461222289362168475975/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^14 - 13865075161012748271555319552332200142017318597131884014036824529347515693916711379690404973741718277905944597832670689749584780892000918225438025762054546701182841355747980501481750845786107/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^13 - 2271949037043511843546994616300315197299255739128304885118578086052087188807414878190067472727253151990866970874317452771920041926555961144548183199692535780805517356192759551787781655595449/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^12 + 7100739812572483847025041938264539923173854878869929781047692655838817400834879185365739074493437840088068116775830849915013391003202137513607916273561761538540065551923120468638398821652051/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^11 - 2556343532772061168536979902935044640828362499101496474627666818694860966006635194468564810839311467935839256351263755824190551798876372630117194380123387931005381038412527520163782685240545/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^10 - 1116618786027171267161069748359958045011158009150020904060534457007350392131766808235511921830416405313223945989756808447962322914878805208103707716497359863146023261212986554959949082954367/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^9 + 573162982344670741613067102349213108226581211865479893490610494352664505101051042999212825491504343137005283942736899104668407957517750781894493386211409484842405150405837736932418911131253/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^8 - 57682779000133977415630964285194664093792293411083756147640144588694401010744987599978341382288736137879424104718005299033307901312858200418744393823647360269384101017177567621640730026397/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^7 - 14641687574297133173461216011354170887118597256070316577424265597546915268129275817934123648631136304792232962223625063139327696744014841316212741564753362549832245306879311787920863557549/243253977219063614764315874938515043304884922262378384419268613291019401334674604990609749928527601429128329987187041758020567004474486656658581542792818248455717693053266164090181952*y^6 + 706742593386853798680773782335020756584869774270511302222003674223346198135787876337924372999812170210347433987075504021598328756028979455502140820473760922103676141362888974916328058721/15203373576191475922769742183657190206555307641398649026204288330688712583417162811913109370532975089320520624199190109876285437779655416041161346424551140528482355815829135255636372*y^5 - 435544805509683633974044814222256529819001913275398370123279492216587038077628598831869050449660157656486712907936968447191975225535009706364663230649643950596812380569816846636835919449/60813494304765903691078968734628760826221230565594596104817153322754850333668651247652437482131900357282082496796760439505141751118621664164645385698204562113929423263316541022545488*y^4 - 16931794427330467252356625878285429660806132914532093610565674274183242416517833510337298737716415861587639423166701593614834775865508081137563020175118161331104776440620505430564650813/3800843394047868980692435545914297551638826910349662256551072082672178145854290702978277342633243772330130156049797527469071359444913854010290336606137785132120588953957283813909093*y^3 + 5321274559523765509059073480113342894509668344666478827835449447231713734174646000672186684136710919934136256313755407659217822943877694279424436592926195810321823998911209527054730599/3800843394047868980692435545914297551638826910349662256551072082672178145854290702978277342633243772330130156049797527469071359444913854010290336606137785132120588953957283813909093*y^2 + 1033011872081026812745771050214320045983058430045061538619275198301015191936016325361198181235540495788351254433702252398976595202108406467700246129773579726907768755669446370184802985/7601686788095737961384871091828595103277653820699324513102144165344356291708581405956554685266487544660260312099595054938142718889827708020580673212275570264241177907914567627818186*y - 198498015188682744614654055577526552520910235808835232022879399144152813342779601577830781023832427926123633391396736084470289530238515692988196198540365893370638621151565780528922139/3800843394047868980692435545914297551638826910349662256551072082672178145854290702978277342633243772330130156049797527469071359444913854010290336606137785132120588953957283813909093

-5186586089754179886143116621403646879987957839949194389825618029071337661856181245954361508881699004549210498530779800110380594929180971936802758617312774855324328529646762849214931461/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^35 + 47247545496594238888526108815119066427918104646045244700974228386544028997814616746891481079082896514123959006422502808111147716421641206259874046185660950726407978106414662848121633509/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^34 - 171024884684200086802292249977512341445116383804824938448492891133467143678731013076343959850797378415843743345993730668298797666834448102789724028686837994064872315256340643723957025025/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^33 + 584644110677561401028301227955323298004711972518471728362430533462782080744344680535945150977531790626727102787930146683452007331200575489622885392773907303576732162226169310522101780097/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^32 + 15756780452885880756122219655789177401730294961335244253650622105866820618512214803658123996369683394994033548953852714823445262904522087153528149398775054125774986807017833824663020003619/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^31 - 150706439739483332751621325377240192448520120352200788271243427842512024010999686547171704514098551140295010047612727794313158715875661056608210854847366830591235002198561436345543178374331/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^30 - 19908095298094498525677006050528332340235122981992853800923722931053336047901325178657365817326787473694220036530323766137418062227228230709398240693577266399481591579601310768065182056805/14351984655924753271094636621372387554988210413480324680736848184170144678745801694445975245783128484318571469244035463723213453263994712742856311024776276658887343890142703681320735168*y^29 + 321546728471994976191268192606096549833792577437327442862997541601650524943638966197542886030515472744620265134193496555041142270516543819319749827478599321697242807853423404573578259526475/114815877247398026168757092970979100439905683307842597445894785473361157429966413555567801966265027874548571753952283709785707626111957701942850488198210213271098751121141629450565881344*y^28 + 269311282595666042326414663710123598455606314892432604535793201506272398907861760823475770539832936883338229510015086892793140632581585442069317879617643906179138134297120053555842960028981/10703174997638799049629898497294661905414936579544648914447818984804853658725682619586828996855214462881646519436229837352904948196877412892977587882884002932051578494343711219968005888*y^27 - 13435510104983346888716537067692343790268211980427825806405344368963502773552899452997398939878989262716062037891892909461470002053381395841345216395335772299337376669513619323310127750442261/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^26 - 21295662067869796389765968169384621853959073929370085365527597041315376253219175023386770489297879312237982817065570179527014299442252033357607053479437503786709637949573486230196785484328551/114815877247398026168757092970979100439905683307842597445894785473361157429966413555567801966265027874548571753952283709785707626111957701942850488198210213271098751121141629450565881344*y^25 - 1852393461612758846051295103715724709264793357748261288266498425129509095419990487561329267901205447316674663846783763652081432669896936772197798117232513643278245632350132830708725073066771/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^24 + 1123162860046483413826817645539722301913697070993266883431037422311567358925943502301136093839950376486690730378724209779909339267197214960341043248355823294740816458048602057521625339716982215/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^23 - 19109666909168996961462669283980754760611417046985014190926255755949030369878837701278094681352148502816468486088121588774094284957915168687875424534482061877994836773716556607762587347474283/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^22 - 2036306623652958821758597968841798098019039174514148118324715827388945898931031083629781441876858775340245877983527679945593314668384799029885311846746609556587762386552209397431318168762751297/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^21 + 850381439072152224532308376007351545244339704550319018348617678005331892565400727000795482338895492869238782255049271585726955291689183073439690718963558678551302718909129221708748878819615185/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^20 + 4398607302789963569077423494230120316195378791076294218225775200301488976530138634343441919712172381742431512510893780541852676767784171003447572127317972241864455953116849324537056947470894103/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^19 - 4058830459301540566463044433885111984107082906102587195327150626813591648656819871645574431172853344111385026847571555150203044855250531427362640528724320425656941495419879489471764239935737597/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^18 - 463014496733829107975272408801906278106130649737644116589358719261156480389557467473936341127053049172278540397094267506347433115844021416093977527206487226663599710093789472134153821968289669/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^17 + 31721310520932920706721895161582599590948851074019234252879255259268281676268600273360536888879874239200567134432579030866798366403909442111473526707986969649531580239362907557314243182880149281/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^16 - 385784648730368160703198520960150922430346956334654712344448785958762802305230788695234607134954116576636100394587756827512533707126072000314437148436086986071226582508773209277919626758009153/114815877247398026168757092970979100439905683307842597445894785473361157429966413555567801966265027874548571753952283709785707626111957701942850488198210213271098751121141629450565881344*y^15 - 1944678017534228109889582810505044355845038337753851183207430448068618039188348083325345189421154566525724273725823510251009787104983100290473333106485613142695121500370124547323648450274447565/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^14 + 13865088622264650052244713577906256376636965510678437358213858141435593183351800770184748604864775483450315248535217728931830816287836265803547720182700063100374074523208294106919005423645644819/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^13 + 15554470175136809735128825105455080750125720226292019650767998587471444189442925677349225102659105093811273152106918523037364923967852339618224301838129746876207391046184399678690799123480732157/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^12 - 12069241766393012744674689054436406703926204796867803351261001438741799110372178890331320749116423013420726966901086090498669812292283287203212101235172195420856081225140562756339895728717822699/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^11 - 3024885220484902241244034903513656785917363024052031030199763039889175152602473580568834624866381902040136540750086508350502383321083347013278779455825403634012979463382017780849307849650310879/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^10 + 5355641664860487545449221387615908525115865779463552250123086393443975588155165399427616810489835428010625780729902166253741450982643083763725613804737810153827165637635720200076415191095466935/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^9 - 269080158906408518838810076077864340156621848394851576209381235519194009443102275544502863099985301167231916704175858667707730464038078771527117050034573325270973050923682182400355726688723827/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^8 - 163169160756125536969626584308156121565364467368201983317709460800839893246469996794022864723222629427930995186157032052007259388235302110251938535983824915667508309478566313803814056793295063/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^7 + 24312877101069798839052109918614503061358198818838334673759050742509766057878569916662592994642080537857406552407330380906980561739304396092273231517019908654427309426845418923871470213820123/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^6 + 661443183761968436008833583948151043163562590958020684763169307415699016513475558376150962208822812691052710940003273618897118592821814815078057399363864228950554846129455693377819112433775/4933494725474133936938781338596758222027197329633861609003291563308487233318869332465803990737950416484508942552637190654854624559498182505356856914766845101492524462236554390454002714*y^5 - 1173512146565021432476181613290419450241056906451824915233075915374000310246193975651136697690528164378787371638191876857519157181238324388080873040348765752207217166487445403348550283015485/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^4 - 163479559331562056095961705013902519911656105827343792291046057687152456572087535336757153820019774104975471709601027083342859799588501802781980588516798617482117761759197369177845581063715/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^3 + 47382556693507701421828362287021405765887250621045607044682432111506758827232478995160400412597680542933416637078103261187534507009495090042574153194867886393931836622925785649233519561651/9866989450948267873877562677193516444054394659267723218006583126616974466637738664931607981475900832969017885105274381309709249118996365010713713829533690202985048924473108780908005428*y^2 + 962161781801332212433550705987433931038422660111336774843900300261839541334742813505150412575164796444921856825555099873818888452395845261747022987988283738022700410052410921060429378967/4933494725474133936938781338596758222027197329633861609003291563308487233318869332465803990737950416484508942552637190654854624559498182505356856914766845101492524462236554390454002714*y - 333384490377236522637839979185446898875089325171060351588026175051417312968101988382933399261434262780459080584679440247624114373212443479647413736580913016455613627530433734816126464859/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357

267901877538463207721604473277514315688683227500200395924032449889348604039415781161261388924781996918624708417581563956162038379670610068431073984342240526783531657165211106146372579/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^35 - 1225038601081546999351330241770771489164511888673563239888494093013667320545306289065115570545371555000453250298148242556007009664234608098243975085178294820964701359527702645433181983/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^34 + 9193364153741878037638627785206223400304979204495623789299076345785296103306558082633093296825408115632239911114991004891996464522520984420069488850282143126953180732268799460186364895/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^33 - 60802041558384923020174895479242470855678541560764742249461348236993888095559531884294213116001103596126744801989451468882483976007446329553527815202702762211487749487264099133846452981/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^32 - 809342122721670271180744023196377939059174688122503152882163589311904597784986406980169394909080350247311961906150562697785095986170216857362796509157997536391070554572809820043002033067/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^31 + 7840560406005532462160909883722806216299040252613787877002300231978908063208919068678160444084365236046907470274720753404684459411227475573337608955565261035552142808830795720847076066003/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^30 + 22330104413450350692223626192306070636036830370937010528412834707221300421388751153517398130575136966378246934642723724518010205832911445242809008770983789875393204846074100254009479773287/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^29 - 188609087914383388744157970758585878686244023798910618843255579174384641059293152483344305091206395923212228252073301058164108270804000974886741507632961361023796706433238065162468826161799/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^28 - 406386445126433294029545048217074138826330676581968432650493863296814766605599011283763155217414357763470608562839198931871039935658175117575095757257836530311443513380944211335022608867409/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^27 + 803526778683263145147560687165536306238649557640480610616135685838524994730378831041588216792479495615251378646485079366007499873148746650952164210496918198049426497487551352854834051531579/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^26 + 11997321153787398727236433439490128796526677731302530704829405369642622500026135692759204867233729301388098009260924093215317294124807892884340679410425695631839926659346353342412827035817397/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^25 + 360274974900125603532662521108289460058196708276059634276651836835262731881364456850040484581951575626877692384507693323665731758893619415563210139033128780665799931991302966693047088252507/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^24 - 57730093426063921635650283936165057435451177970128840518750524786743591440884862946775569814662914641957694907440942586014454684606709789058374386755945231748041332682091829793679002963055805/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^23 + 1485965213560084241085836962713885481677039921423416464184041433223640701920238244885269969457887507662664348850159697507753733791816024069271112996049806521499576348947747525189405054954705/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^22 + 104131202200025438310802913134959573600256845842717000851508993378189460189555726055409973757659808693125781618287861995434977781117055328829394319889329545045041052921836707958060944082514483/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^21 - 23690674312577823220240840607530963013213709856810342732493602564726354178279184279408171788182938947765465501097352224586617150068182976846094426810483639180080245611599059870295404914204221/243253977219063614764315874938515043304884922262378384419268613291019401334674604990609749928527601429128329987187041758020567004474486656658581542792818248455717693053266164090181952*y^20 - 217502267316808610104435628158433205662280582507102998713825270630231939333721034199153269662214826575602206976608546719819277982001420041969534129521362405614158217840993654872055630586589689/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^19 + 53805603395861564614534453855731170514315115143199876372335530438889874866927132576302273559735514426096835285151432523582012742701650929571015421102416503873509097648418078422116360356943579/121626988609531807382157937469257521652442461131189192209634306645509700667337302495304874964263800714564164993593520879010283502237243328329290771396409124227858846526633082045090976*y^18 + 19512583203876579860352754621006887305256931463133254412423521049057405378793240475824891482519970705234807473612679640767433358383272937265628929247414271072356519910383883208407671292062673/121626988609531807382157937469257521652442461131189192209634306645509700667337302495304874964263800714564164993593520879010283502237243328329290771396409124227858846526633082045090976*y^17 - 1629703268754934885522954899824830073778024441117289447970214083317160966411849427974328719429882074349397005092845513319141971794692306223220455436156160578792648692425400620024956508315267335/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^16 + 329443116591197438318298853202642553991250178899918079342807557707505995590116241309405628379909307078708863368175787448793920568562434288715424642696465956849643685462679095896297398288808523/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^15 + 767896897256142992667884907414969580956908913561821231592355611755317813059972687290368499357497692301816289690849997221619813133366324527628180333063370283916633153900779072149151815804434245/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^14 - 791062836435557137217662994609882666576324389708554098607053980448437859727961805590463884873460898983555455182346427121184991962295064217537290745522786896369292435285536310489261733561561721/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^13 - 715450432385439900547259179932704809661522274957889755890503839320150760607267228231657915506158406315645448315296657000991859941204321700625105329639064917605679330506741548486675752500395721/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^12 + 633222692678321659450823397654573696398081959811777377669130809820216046665324398190141089768742410582260224805031862336989672895474170674808864089421821841341526455216796623354656565981321199/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^11 + 108193953927214477066714235920816252149409843285702866773449596244017577744769989904357609290423896852375701604452489678162230772060276585061972441816404851958556937767266255704341176923264651/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^10 - 262338285828590223939389014462953400370374750243830036657329459669323582371678917528034093646167816923846398914780685650463400907287905790200879660230000857080420890802215652348217750138971655/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^9 + 4922971379036802120335739061275282641485438589858206661461593617133066199910955603778433329352711175455122132558892031303512890489107042936904296252634223841779131137411988361716753519748129/243253977219063614764315874938515043304884922262378384419268613291019401334674604990609749928527601429128329987187041758020567004474486656658581542792818248455717693053266164090181952*y^8 + 7433204932264486115757739314313284170550994356186284325006778052495022316201847581065312052706700511299195126970670059293677349261821768364114532396634930933621795425658919974887318845710703/243253977219063614764315874938515043304884922262378384419268613291019401334674604990609749928527601429128329987187041758020567004474486656658581542792818248455717693053266164090181952*y^7 - 642619957903831730955391697538004354539693518895953447874205120448242556134141528906618958390501771508719649732386857390007021682327388246957336345938721741070272259523491120316984834193033/60813494304765903691078968734628760826221230565594596104817153322754850333668651247652437482131900357282082496796760439505141751118621664164645385698204562113929423263316541022545488*y^6 - 111217437486382323245798361885083872146711266775478217630056771624684035863592923027619517669425076558478471845300065518416759011425306280170702481410716374154732500719927110502006355415263/30406747152382951845539484367314380413110615282797298052408576661377425166834325623826218741065950178641041248398380219752570875559310832082322692849102281056964711631658270511272744*y^5 + 14164163384441158533035711376839820126680990446281797956104775007579921566282431251264008824239338451304726073936291070545454474523626421061892763961665325611397785415963461104158474061907/7601686788095737961384871091828595103277653820699324513102144165344356291708581405956554685266487544660260312099595054938142718889827708020580673212275570264241177907914567627818186*y^4 + 6305879217030802212185798002038644938146373326660869025527119551508644247516566102329777939764864344309054588781212689578937528403083741632601346983853085240174651507879490795022157779175/30406747152382951845539484367314380413110615282797298052408576661377425166834325623826218741065950178641041248398380219752570875559310832082322692849102281056964711631658270511272744*y^3 - 2174879015076858229219043780902986117991288413749475518733364041956254738842431760491031726304280284839452898884123640757802021975226982813002126098696698907995844805484855489838194755261/15203373576191475922769742183657190206555307641398649026204288330688712583417162811913109370532975089320520624199190109876285437779655416041161346424551140528482355815829135255636372*y^2 - 16965010152675169874320781050659289736023532839685266457118917128925440103902878114587611174209595091482241960370900408161687103781870916355799837778571482042352718692815480289126126251/3800843394047868980692435545914297551638826910349662256551072082672178145854290702978277342633243772330130156049797527469071359444913854010290336606137785132120588953957283813909093*y + 14950787542060326877564386999237097046510377458882029879837908275768746890193412107438262016950313984137583847138322611923357891538171644360278747153290368822422763185179960683459607669/3800843394047868980692435545914297551638826910349662256551072082672178145854290702978277342633243772330130156049797527469071359444913854010290336606137785132120588953957283813909093

17515593613808263367399489533984169663523810669394107807627851617853843011807631076054715156059452612616594011445569679893144841768633778073795953283480080459062046705078000870969982283/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^35 - 40192055696923054201216215591382158953526480555130628348941064100702188001867401589809223067211347776804103340801649568286750953067249587700278195615098530687344893056245808975156140171/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^34 + 623088390822099543603520842814898385705516914901805334481728736233669655117800291471063795649959252186969404865165231171616041320342098470401358680588478827885081424356056011096738039731/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^33 - 4002471491134611154155225511413026733269425412071453454894972710745164681398090346707174104162649365518604840879981210916817905227918634369640404467786236772692471715559176546293783556839/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^32 - 52635749522673252393233580475356520873775170473635679180167181433076506762456572794889667195271855915133691726220510649677534522859176693141198380771372255790052588009269095836506384939273/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^31 + 515945489765341940285823536532627662176875809660665419206451047431442345423599430745720203949513804473340609788047261600468697452490936140804794774486690934165815159306402064189933802851559/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^30 + 131074381247088610968563210435065446523070258301268679286134883810713268824025075866269202313334728935496528176236939585535761654141757978044022780025165384272937915144285005252056905421373/57407938623699013084378546485489550219952841653921298722947392736680578714983206777783900983132513937274285876976141854892853813055978850971425244099105106635549375560570814725282940672*y^29 - 1151938916292535426123026431907823185652389491254082886263234154179999288891950841834834271410581232903267876666467728371105806216002594420172895661702849702906272612793897626724284280697861/229631754494796052337514185941958200879811366615685194891789570946722314859932827111135603932530055749097143507904567419571415252223915403885700976396420426542197502242283258901131762688*y^28 - 222921232393240518994830651145311095107195782368958780657154835469345975769986549187659841955918490141482176772674687468828802205763539723968623522166659381618760566538378432946550836617953/5351587498819399524814949248647330952707468289772324457223909492402426829362841309793414498427607231440823259718114918676452474098438706446488793941442001466025789247171855609984002944*y^27 + 58951959639368295397787615768241958935777298091857555272096315124551448943680971762715472965583127459006516183372896196891815151146152041619135313956545234897195772179529404910350105462073703/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^26 + 70584564313896116066023772417265200324263457334381781814678705693191785226069895115177466408058791216999293782361473989490029433161473935048584868857355522973658554614426703465918030696478955/229631754494796052337514185941958200879811366615685194891789570946722314859932827111135603932530055749097143507904567419571415252223915403885700976396420426542197502242283258901131762688*y^25 - 518568268471278362405721545613875990102574240994439170019576536489653122015855410677360846480705045802186545264459235256893965537728867277162314113096069693906012086828464797738176121459793/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^24 - 3744548776969159092206923649232113021365921303651665939066362654281926516541747754349882699498369237559058348550859290891248643274982484966467425884789500012750589673081288001031112659959876545/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^23 + 78690677156265538247044636389740448652359190484629131768422990701450629589222162890307107622207173962916826364691157563138561989952459397364691984106730215426590255703447906629883554556724467/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^22 + 6714911899702930448996904101721003724525168394321187808915689325303543049675645346648353943202304634028127098472128919999023875205951339350967554844546926235226642976245921022499329964640388393/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^21 - 1652421333633273588091126485274857499577096017081245786029345192738044981428045336402973917758284442006283036016403931935564292571959678618038679330556650143670721442577864128175273411235402913/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^20 - 13529130113652930816728101005937729845253367584572630407467577270904773905216105369357149986237383722703726261911608123366014264924970236876170678533542710021622842355075424416663178371270689477/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^19 + 7177754032818418385568942805512202594443268007309957749022489244365257549148661385120961725179790969024958809536974787402208856218117242454122396069251978603332595269497285239949253617814399597/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^18 + 1968150240385507485715499737261485076449908251126473856133375238468370372032851565638283916429142092645994192975917407302339066677757160250880170375797146459003581663109393349947704082195674557/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^17 - 105128135009212714147063112910809820395657256956865316643446881112202730870263747097808044588937353683855771546091851745328844765889265398463194951069203229834044120145086882945920042835343668351/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^16 + 2581405832704792668549768088057686902427278004795392608397647751846109733436714739620543642463895077551841941658110206430644470809079718594109935674457718945714066189580814544439017930990381277/229631754494796052337514185941958200879811366615685194891789570946722314859932827111135603932530055749097143507904567419571415252223915403885700976396420426542197502242283258901131762688*y^15 + 47291314002232338801665489807444241449602658942698636046340793225740567407278675330763956263029404715941790487473576268923676737544287099590908444878177807928824660069246527464359116531407128985/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^14 - 55772487516745008442105071151866935286354808715435916263300262809805409587702282333713793917324391128316443410695753207712855446227863642336643842251271022333993619715811452528403463344850223109/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^13 - 40277709788505737367906658829717421513382073614117114774955647269951684075195011064151531555492847865849095580359880167848796178721220543320797872398248903661964420443386412087379526041675775613/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^12 + 41214935748685083809660393996743578504534966032069387181164355114107377300171791779444018106998983283726469137462343756542751827504935872733317488306559562418509087439341025676824718101996642375/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^11 + 3812129962893348237409463560518538229215730351485645380638576141071566622708268603839755338143873172920793443088486161471167190114756715350548436575169616937122613508648626356689080251319641755/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^10 - 15808062363231223945713913467238559731925332900187324789189371665151486938111749744545129412477563933226438948064473641774173787340271473177215325863853441331217219970687850335840987107144570807/2525949299442756575712656045361540209677925032772537143809685280413945463459261098222491643257830613240068578586950241615285567774463069442742710740360624691964172524665115847912449389568*y^9 + 404379277070148247931662503628298798043866907007510958455081694775862638087390934473006410906560371759444432887671323799792250836720767658586201608844777894726759292617795476176658159070648603/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^8 + 817594049055429187537394094323142168751626641017465467339008847280985863256200432686566471776829155937272139128783889584507674657787177397527286389968025505187535732694856596023465086561226773/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^7 - 165339944061550602244722221015298257309476467784511125585711612707750165197791953734714797056346495106141552076623343743932478215050201687865129450915144295560680624055668842340425236253568005/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^6 - 10983576392134151074825012170594303169752439609917576161115312370584857725939953314306402372315461193609736789276338678503127133314599377390239561651176680589185501505640663257626521817404179/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^5 + 6599005518315976606353866273593444238389325303050639094256302855336808959221974576695180267457265830426815425620775365727778170313068019019886188894053779902960212473017208500298103292161095/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^4 + 17525304713869128607030356558502542348645126478898486872274066976849044551272257814902465386172999573546894530412245230708728336874552049898578031953405539639794730116223691413781440525327/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357*y^3 - 59855880907332934502316139184011092389650627144407374762570700664235833053324431846956455396483385156348442156274992635336592879788573540767070549119057217281107144905189942245166388215283/9866989450948267873877562677193516444054394659267723218006583126616974466637738664931607981475900832969017885105274381309709249118996365010713713829533690202985048924473108780908005428*y^2 - 348401676832559699254916280146580437557813304660647382525135001738229428020803916002071360420347741914652833740311964792727312840163211926638232625229475905479764806815787617755370213632/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357*y + 796767624458723824504283341143908115699185358497432184661465168631020660550112891644283930342212303642149852944257436584074795549440427103652354323610697892130976546605646222636132947973/4933494725474133936938781338596758222027197329633861609003291563308487233318869332465803990737950416484508942552637190654854624559498182505356856914766845101492524462236554390454002714

-3978991014026690148919649189948775803577484618910016106361522494581892347348942687244790086046652209484254143737881576012260469046869028058741936386423527594813323958663050821339510989/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^35 + 18525286697786904604519224483992168507462600668346420351927955707258525381382880027345052787930100785303275007575832336648030304749361889092286851959455084963390076592600294514972130713/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^34 - 161499001226989818654250031504676855290357563086224580827169103289926853129706535827674358554253788418213684657919617933700465277889959528577038005880593276689575762863606236283885280421/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^33 + 932973697256947459975560662690875687439052024098833314826426729179318228705330943948144277306778962537015339092959517869007063948827066695701668266744223961570668631117344210976033762711/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^32 + 11704574963019644791364228471876206301955563461300814104205245662084015159679399578350084191849057198507439107394076263887937733574378236633537239554343574189330645356982249975026000746531/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^31 - 120262552857639247861962055271506451520052393098839881362430989824735997856141107665446177243535609320921529668564484030676872739608201375914477929016784849799907847535994936433014948451565/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^30 - 28288708804752440811312465615182382710421691162691806452324017342034799495962876916253492753637753574269288832523346278108882885189852730426413656921733719259624175290109285059351406173009/28703969311849506542189273242744775109976420826960649361473696368340289357491603388891950491566256968637142938488070927446426906527989425485712622049552553317774687780285407362641470336*y^29 + 290455970052186501926284505744226439064899881167726537515730380576156643874196249374683655442667608132392478650010941927734661271249009278465872491259792536781078516798621101321455175183123/114815877247398026168757092970979100439905683307842597445894785473361157429966413555567801966265027874548571753952283709785707626111957701942850488198210213271098751121141629450565881344*y^28 + 97341212525728460310840406787998821862871941595982619072533664920155307246493203034323207174419659095212747832814162184315574141595968830913267606714791769363741985239663054868076478538965/5351587498819399524814949248647330952707468289772324457223909492402426829362841309793414498427607231440823259718114918676452474098438706446488793941442001466025789247171855609984002944*y^27 - 19322747454971719784981907109823541335928471597826114933163843953491382882291514780846107836218246531782754797756671237809926416860963274389802971633084567872912979084515631987835138852872977/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^26 - 15435007651889717551591340008513875324439447852371483592727718334900614086153030695415189091111955048782043028873339295291640311114610645441090515083143275537112307632472835193910698299972409/114815877247398026168757092970979100439905683307842597445894785473361157429966413555567801966265027874548571753952283709785707626111957701942850488198210213271098751121141629450565881344*y^25 + 22265717772043238045448405913346629672889220335378521249372647133641851814895910544101757697513925686024999416489972343529612798914133640065944036663248699258909196316560104406870530618047729/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^24 + 828184833683307596535444537780050175764525221708596166766639487053107543272349467823379385790794374787309139114297355520129906177861308587671867654533193017144503722536085469338108659222796463/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^23 - 90732009686281943803094831868151306245730073327428880937826310589613147557476984270470185582839322143346057035454280027643872158631232302052648232679014179801160306581571022338233014225813875/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^22 - 1451788426429034065112535796884160429637596171474726696900969333084064688432181933843461838656083337384643140363526201259483251389682688014016830607102902752556824883635588171702055983933538639/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^21 + 235256556810035327155394951668574872805821435822821864375512183873502127851718114625335384840149276895454363155061240701294012705771181159028060664679074082948711987080067017379175167926903357/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^20 + 2483119983636679902319249750831976060900964015068337847038485154543938386641865086005662285400001577609372180663471584743257766526939939439825664732477199356258094797398061398010581051518400979/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^19 - 55362863526106519786777135275900699040532570678732997440305428918124568781374156028837624060012937870818080845607518872777564117778281167716337823614000620974073147640730288739660485684724429/4933494725474133936938781338596758222027197329633861609003291563308487233318869332465803990737950416484508942552637190654854624559498182505356856914766845101492524462236554390454002714*y^18 + 66725299261632385654254144577616034463685115393994012288904584008602085632890919311129583335968478284384283269126281303572049487855670574845220945293491858026590417765906032367295759902758081/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^17 + 22947950465220554948122863901020957999229662745386106109597399873102761933521940660441272619164302756859257642302006935403002943462857559108104197064710057132713563431525411625278421981127435449/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^16 - 1152720258270908968110317443762870206401721750769261813789295289927635591867086845713299916801729811317438917665852590858010130725778087411089283798692278017553348333393290409096965627362984815/114815877247398026168757092970979100439905683307842597445894785473361157429966413555567801966265027874548571753952283709785707626111957701942850488198210213271098751121141629450565881344*y^15 - 8379431881983574411553773862411495508568086117664643451055449596889719141343532853742582896817900946613870505285964166080017034036596705020357306698153736685137229466882221033007805000781779545/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^14 + 16632915322959297436620756779196019975168837768474210865619531664559051735365714539627380615039472078733949352598346279813080070915249692063601846216434847295283714244052226152005543446487364667/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^13 + 3643382556102281591034052099067946296228421336896159813243972896900169212318417086141006684209399565658313081020245828738049506240526224897419261042354428821992096113173993192215912197905320599/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^12 - 9555802902639842926464406956340185575629014741940044794934139776433907168962993737948445215895087722327659248996400294654222871817598341482181821978057746319411611868329315306061786623058838869/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^11 + 2018857643670654857170839643755671507140042286900499165208010780589266299826451670920004911828235468395806665900107612272948703363120555520982313482714590915286929997413268813494795274291878079/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^10 + 2565377557244607269928974275470813754396925777438786040774756371777134493633546601555714539557527785142770433312961212240294435688921975239358792352882933312132466659561985711267399421614565901/1262974649721378287856328022680770104838962516386268571904842640206972731729630549111245821628915306620034289293475120807642783887231534721371355370180312345982086262332557923956224694784*y^9 - 344788615036955462146976945448150127966252701014565498481093119045537673690479440826192625795602396997258204713329971733238193828575788966725660704173488263474082948646412231270063685817989073/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^8 - 56907103699893850935762980450144391974026951090798272983041761029848075771364386995915987854479039492529060563761689881125286608036137622211957113842612580068078119665645218713512005287489751/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^7 + 38324018881923432225853426873689974780081860551099353190168064589053650712488680011298303373145853994345022759074140467831243883284688332482406424799754344917222406292851072122076360231886783/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^6 - 166024582469323308618137447458257366516660520909019905369422805565645722072972328262652417292735532895686026630372913833420134921552078954338331989816384566469826242051152732899360153713083/9866989450948267873877562677193516444054394659267723218006583126616974466637738664931607981475900832969017885105274381309709249118996365010713713829533690202985048924473108780908005428*y^5 - 903012023077497050225604648627617696285251823965731845706225250883170433902591021702549636820770862827810196563683041028063206143245417917547152242853540341608474052021316274624182383925821/39467957803793071495510250708774065776217578637070892872026332506467897866550954659726431925903603331876071540421097525238836996475985460042854855318134760811940195697892435123632021712*y^4 + 32004556503946153017791333357481844995543972824507747019029104318958798147614189228022850387222451910512018711192469410680870677245823917556232749837822502820691191409617465187451044374633/9866989450948267873877562677193516444054394659267723218006583126616974466637738664931607981475900832969017885105274381309709249118996365010713713829533690202985048924473108780908005428*y^3 + 2157762641005466548152842468623355468194864674394733935871552685280781130202681838365764568254835814612016127466943570319681021650580472824342242545672321835582254704154380193413236542214/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357*y^2 - 288610883394731462175655505036992452635286804023617298668843095062036408351496824952944833739726171372356211990126068471363027583462646194519896110478505787427160100072577074283055061831/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357*y - 18166224540610816969439086028433800485579022546127170909994714669077239238124483869951284859674947199784440785305546882459025129919196567199966544380220320161423003331321821888219590955/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357

1968535164089511945655675468893985363812346076026909723647467330336637368558810437359910831095856981297314681646667238035115688100382404186703422030794051208911023264140079819492075417/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^35 - 2249227738090507228968328334370774443523501136362726109853861840917685351374383182284714687625981349077290906497104365232289651015489119868834728701641775324860412668395900227645640159/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^34 + 67210251735172308005174585056748820519192492331343441144618782389771673407459949889355099198898208267469686302326811605762944832077463007202730396369183850670642992981245972256602198813/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^33 - 446424404302310256920607810053441281309166528261503655408201797048460542498676573996022489029890414262309466541449404029503544737905148885785265098837075160423231894087534003442421732085/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^32 - 5951300150802263735201645948666826654477485169641482380959945356050739950940577702074777658538221582970176637620187062867927930288912583205045061894197478194552896433396245993187747092197/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^31 + 57556888928391236896666417355475272636312760005430085210694759530126265777672793032796735159723029561311538411904987893209766869697799832889950416406708021259297697372482766249580636139269/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^30 + 14941527934924511386564128005609050336953107582681284109387237032306217837145543267132427211227089838599237505587088495344188445693093800093558431300902077711526854919564591265182327269513/7175992327962376635547318310686193777494105206740162340368424092085072339372900847222987622891564242159285734622017731861606726631997356371428155512388138329443671945071351840660367584*y^29 - 125445597308896361014992530194525195272837047475090004735301203839963177445709355903445166195416365980580762523454751219603709135948580688458473824533268246622082351080814622404598947743359/28703969311849506542189273242744775109976420826960649361473696368340289357491603388891950491566256968637142938488070927446426906527989425485712622049552553317774687780285407362641470336*y^28 - 6333923933961410246724841431569476914530432798388853997518860890559997850659336973991805079986009502957820567356504158764810082588236721105613786058016586997906664817791395744000015073097/167237109338106235150467164020229092272108384055385139288247171637575838417588790931044203075862725982525726866191091208639139815576209576452774810670062545813305913974120487812000092*y^27 + 5794608491899027183629333420470393002414984164841935114376878661237767979808686790555576932214255497115254774061144424957077213661994195512146838630362658451009878086791406983938078568222193/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^26 + 8020866557948109842535202799962692294028114482675794863038989865496698041813768232860896933672179124675021264132461195627623838451479311421411682133469189770140942462339902241966982658955385/28703969311849506542189273242744775109976420826960649361473696368340289357491603388891950491566256968637142938488070927446426906527989425485712622049552553317774687780285407362641470336*y^25 + 3052051114869353317521614587226828039823968905128313259432380796661210644952077724183378621941529731621026653771735366014188805051825757584006568346561516864006838462634096779366574024001671/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^24 - 424291378256777482561913672479815050453331841182646769712912685752118728230190663016302119773926224498070423122085790842570502301519870009688202531163396057445188733575951010968671230071028511/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^23 + 1242237530766875076836172494076522019168596769459246061275030404049971265073447623171133104063345874027191599552725476109748278913236674641389496609591340023480719310066176744510978374536979/9866989450948267873877562677193516444054394659267723218006583126616974466637738664931607981475900832969017885105274381309709249118996365010713713829533690202985048924473108780908005428*y^22 + 765727057616562631705119003229898572845044605066039194100163516892492826217623269444306504856732184302234387763722501251124581361919665662858136223600947575062358352862986109945425226643469897/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^21 - 86164443491747539918072260500087009585012640595268450297675422850325458639420200152985974171004007427239766250467720749647036163619862712356102407249450204932947139114011371710003421638139793/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^20 - 1606090371724495704949933269742686244708746220110702028229848307322398199229215856575916452137998134377765557671813029384505274486718168131939898652524400917402868409441470902812041982846717971/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^19 + 787395319693967533869307658694622626202499261909673711134018772944628144386375838749605256361703640544841073212471398329428544639780136039690012048818639684418517503647012583124741016441253699/39467957803793071495510250708774065776217578637070892872026332506467897866550954659726431925903603331876071540421097525238836996475985460042854855318134760811940195697892435123632021712*y^18 + 147403970191981648706207097124880943271146282183147064235756481215613991604636661597852857160741945038713025788028616982535129700292593303968194296112342744976468667144246601558999532427593793/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^17 - 11966885546144364548745544817733063194534301874095471591210851086273245176874849159900352744877228019992706596236584144330271055485035436803971326558673373348914749828494894229663034608838895109/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^16 + 209786069916776342804749237957462221791588486771914113110222637873378703007829985373788499613562918579654792423277058257576325532296306205499531956761635039161813033087539853879393928347019991/28703969311849506542189273242744775109976420826960649361473696368340289357491603388891950491566256968637142938488070927446426906527989425485712622049552553317774687780285407362641470336*y^15 + 5666169931705684180719701515094045824827221864525916155807301083911345153935174999904116594859989063452163448959495191381425947606378560947932494546364972260954799085586914806131265617013446465/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^14 - 5718539273444236605038700993309494675335040924595044220830735289851852474156312782578666952549273422336075623929212443234333708828153610251390013733946022069152721000093796944413192694631061571/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^13 - 5334213226739898107536965515789323863379124184987024494502425753057408721775890881175733401282613866131329941270880374611041544239244757626685321888129567304790022258755850734450331878157985415/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^12 + 4622287691879652031363221881847937001357776228457495866859177070628693970990656761502365582450100156872959125668496989519312885010719296380666121881890302203451159223482992939729751073538621217/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^11 + 847671341756700461657879304230431081413283979273504774788550658778739256701908802726103010259431826733716277843268557833315193757044274835532889680560165219914538692576381048266985795323401765/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^10 - 1933538470800871322185834024726830054168193766454432942380694077187152185671403301618837034500903913633878348899504340322800710975113950912312483557823592581000129789613683669324263794654102897/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^9 + 67940096875205599125252796670994413118050259530645738975728850444254238373270296189552473092318565028649136693657854070626946657198035099874701138222362445284937659947384065854959073975781037/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^8 + 55574997462051738318520593895571524287746268310961627762247397812224547800591171318503138880386364037894651467019593628870617000563175879164990575291848026240795678705504500973467465489835331/39467957803793071495510250708774065776217578637070892872026332506467897866550954659726431925903603331876071540421097525238836996475985460042854855318134760811940195697892435123632021712*y^7 - 9294458777676943928604207036980798115335467701204366478673359805772574232494390854599327214214132409539834572339686684831740310785823854248156879682825134263800753522849533155304077859053669/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^6 - 3411071296395416002156864474774962217241999982942443502265969053425186367750966163799073457415155130629199986761886203414309391380497890873191322003189627025767907912103803871497859930485329/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^5 + 835603496440872584938616372015087099579374437921318279556460362979127411536869774529810406838400961800976210005775996726208109446450105442978357881042838749090367927129980007445856750125891/9866989450948267873877562677193516444054394659267723218006583126616974466637738664931607981475900832969017885105274381309709249118996365010713713829533690202985048924473108780908005428*y^4 + 50722473988015414470690326373730680215112729893978384075376184768442082597731534029967401211637643942241674688998749932856693678646035919809543970419845569049256631370433807424095827778671/4933494725474133936938781338596758222027197329633861609003291563308487233318869332465803990737950416484508942552637190654854624559498182505356856914766845101492524462236554390454002714*y^3 - 16382023623843844555970956219379515940258250334870601966460097177974529303216187473520550772255183073238446575415087500330232667003563978926386591272204732940834197315347560157613882789287/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357*y^2 - 590899349981834456454253864847648497715307176330507897306217401475395320111096806187426242513470749208753042200424132510391315912572752201802978672913638153234805957478262624929412703698/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357*y + 463354780796452919262342105220431913874757712392137118497316392102208322022107067076142828640043332187366958706689483100420148304699476982475292363578330083389420742204978162073321482362/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357

2831230971711762717928569234229726202348470873188226403338229900962700595111723319685140872814686238971540570560509575870210810160117566634120164386940174014302314844927315385831084813/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^35 - 25871180886611088134419953348839758303214342260111218588292383039462885000361792235717958344476893183068277170073796956208837185137311368406913880044473571213533106825556919793009907085/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^34 + 96374191327210246464286235541613124169194691245103494538042251692328054179126978042984520150056315349438487498969183407431898357071143456506699544615575074256466844783732942893221982029/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^33 - 320950044167105666624308402127096480148426818731651379608934698343001070674513276693734967684077186483087908905306019232449165581867743032699418951423428042357218877022924080387015716447/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^32 - 8562986978222276330531384104406503976954833166884467776061077173394765899507431204120236184634956192372773034172843067158942534064574061843740446820119384411255178459350930944364697911977/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^31 + 82727690597068872418597905919610060055786188270052598500620509743100642228383575474543543033543038453586463235931412998476378617045767716665257589921536999664358261140238031379298154921459/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^30 + 5377445087829765576374279099680857808104517100981467049532739792431699747435003235185750089348577000853786165170654915756265623272441255905421924737477919270900790021989669391497023771289/3587996163981188317773659155343096888747052603370081170184212046042536169686450423611493811445782121079642867311008865930803363315998678185714077756194069164721835972535675920330183792*y^29 - 179850278502381740068385902692747982748070710092998164903149479121994967617458584423184975593124080424276173961318890782478154200479631193936563936154992089818432345836009017892216657270651/57407938623699013084378546485489550219952841653921298722947392736680578714983206777783900983132513937274285876976141854892853813055978850971425244099105106635549375560570814725282940672*y^28 - 145815686373987449783625969692400107086545773593491614321172457520616713072381112173258714177865017093101347557127079672868107627107535541644338283761996209940765873667769147217024712357837/5351587498819399524814949248647330952707468289772324457223909492402426829362841309793414498427607231440823259718114918676452474098438706446488793941442001466025789247171855609984002944*y^27 + 8225389108400233439144187488268422795094444917331849940712478263054497071077354909823528700253929469381371144685823629626789939818605992590372493901005016610121640373924072493381326168155977/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^26 + 11533045215106979572145810604450277911855775775653559384897513948152189486330895744159344791129059834758582848479144955843946884120473021960923812620167744177991238566297129652069700880342503/57407938623699013084378546485489550219952841653921298722947392736680578714983206777783900983132513937274285876976141854892853813055978850971425244099105106635549375560570814725282940672*y^25 + 2384736261023636603239056504706360380872692618467707260405886852626839028267936059172720590816775428434676564034642911053990903292275435613188862290976640527243957594798813122916514600145313/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^24 - 609599215129370782711912210766401321894034358606241346724036212110172030174317817230647417305934982389733758474109386000418363945520848170021374052801361382912665508120699243909159540226483019/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^23 + 26897743641709130232236921100880886445593211019133508638218697883689031138617017568667770331547957813617464508240819863121306896050112904152271844027523370300637186903207135097182786902451731/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^22 + 1100107621403822928531946145958624501753696901291152167807032962324753528186485167513833042559646279717273203526856356867521149184294994342759089671520116591210192340579194205507786537066485083/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^21 - 492592672079222614435758497937011677285352020673454454896917442188437056609247505928415354709953828797456179702539684535799977851458414601133738743202900338309720355505639119736895702276477855/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^20 - 2310824321559134047304559088067504402758709344530742223754849443535621360828688428523910946142694803791645925280442210542367700225578812454292709595483953497876636959955739703702214694182708307/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^19 + 2256561121207139616914843841904889720336228697951806986396640427206758770599185037199736729812562394979415929627648590155612625890091700928439537518329399994488184530405865667781154010138203073/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^18 + 427821889055643340860048552420026782372211554527645677268113986376030262414324596083295321239587505310337134970407376372815039281636042196989918476095948178609211371860663284921501791338841147/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^17 - 17156321179707350501979034869428304809145193357548662084503038447003494114621204898882680495132069423512843759421754116302378800243133046069602723884899839652835778699790947200994741209430326233/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^16 + 294770647383389164610226846232483904429601153469237171083730955212479664769153976206044863603956795957891927149574691271164518977058203180511262024359450385756732861918682359912238295119658249/57407938623699013084378546485489550219952841653921298722947392736680578714983206777783900983132513937274285876976141854892853813055978850971425244099105106635549375560570814725282940672*y^15 + 4061800598356506916808227471164140660431421341732581993014034823301366912548610619351226746692886878879816546587407834329488978270544037694705289998641045549967058565004161801706562265642890895/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^14 - 8132707550004382292664755199716468304922903624290764257178894992919473977855658331885872746043912680119095781190278577481220269999999754633740970549526043381049510735692019299372574559919306079/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^13 - 7648737162721931673362372333746089881818577768636428491850985680410939987886515226653795633076496417832731367128056420333290247761857643958318661901688102810406117647594507978681143165569256677/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^12 + 6584991039263316378871549756505822461737423188149679459396753527579347123623085497743055280651747466953486692895977751905638707822230172864235589400470303642646419338539869305921963592391659319/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^11 + 1220151119768600623974392993676242705351318360646062723346192143272937947863542531927674104467190667190867498807759771205427559224850085764699595667821773486375694367878185488557966172158956387/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^10 - 2754265461391565693520801546430212880427816028465403489445919492312871850896294968257033367458210246774077559576747534121338253875446847144303299639838068847542117076335564973638266253456796659/631487324860689143928164011340385052419481258193134285952421320103486365864815274555622910814457653310017144646737560403821391943615767360685677685090156172991043131166278961978112347392*y^9 + 192209551602518637215336875124469815649280074877873462526154868729170648991221243361610303648244086407034114287381259583838521216073605950947937960626617744839684996799642457663416336420183985/315743662430344571964082005670192526209740629096567142976210660051743182932407637277811455407228826655008572323368780201910695971807883680342838842545078086495521565583139480989056173696*y^8 + 158043482829560715026733181354212791237814771719487086128993951876670702540053337571312686439629602070792933414432725336208726022622816370997702336895314357596546091692587684761106678677527187/157871831215172285982041002835096263104870314548283571488105330025871591466203818638905727703614413327504286161684390100955347985903941840171419421272539043247760782791569740494528086848*y^7 - 26330127479105809295017568922880948803355432811888420283078334836257960312674073443310937984743790917738926369415854898723655922739461260698733994326394438266526094790010752487958126574625935/78935915607586142991020501417548131552435157274141785744052665012935795733101909319452863851807206663752143080842195050477673992951970920085709710636269521623880391395784870247264043424*y^6 - 4825532129220612304983833010877408201335081727668768778061065485997067878729910299758865126656093063934080922274057927008188890239811911461210245604062964803528990649637666446228242571285853/39467957803793071495510250708774065776217578637070892872026332506467897866550954659726431925903603331876071540421097525238836996475985460042854855318134760811940195697892435123632021712*y^5 + 1176789754737494608186898068452739071893287863699817065162118076268564439585952228436694501641445560197550194516994168897441263192011089665212802563514442282495133356237986097945246953865855/19733978901896535747755125354387032888108789318535446436013166253233948933275477329863215962951801665938035770210548762619418498237992730021427427659067380405970097848946217561816010856*y^4 + 70762046238868352932653533078040823354479524867738873846469270596866989362329183687307771053331160614403825576492931390637310014950168477125769064625375681840535769598539381649510913019907/9866989450948267873877562677193516444054394659267723218006583126616974466637738664931607981475900832969017885105274381309709249118996365010713713829533690202985048924473108780908005428*y^3 - 22776308377634312294068541808005349572744397125876702957907400937725212186486693223183824715463347380647516750510930494036765502480284637265612881483303107728274240866186061543112149552281/4933494725474133936938781338596758222027197329633861609003291563308487233318869332465803990737950416484508942552637190654854624559498182505356856914766845101492524462236554390454002714*y^2 - 394514887078016404231234200482504830035606237014404166412895697063099944282007850769661312066950905992908837270325865546426337351216317845993382688023819445151883756225889684864382785397/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357*y + 315246619121660088272502149895042401338848623559167895254154061859735099289881340698189816842494024254998453452262406601195622114821753553977095415652147488580132801069346238674591874656/2466747362737066968469390669298379111013598664816930804501645781654243616659434666232901995368975208242254471276318595327427312279749091252678428457383422550746262231118277195227001357

-12479156078012753479806929844436242334850370528550139452609235685429922201958702072206435682223386039475604872390588160555974830929689821073558574116399781648037226355871316719276886825/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^35 + 113947985737229865250085475676922611796770563696686263434219073793199736934581602204567587513552702231955386375204354975756323943293758337950541973424142236934201788861514703671098647385/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^34 - 421637042766720619573574145885446367543501109753297808685562415035821577770033326828259220671091940205519659840869171875816058339122728234152358369739318411315577099961448322390374708805/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^33 + 1412831062791606477858700527451555655990578168065639540183358432068937256119354503491157711660783401860962037804573512583216635800839665068560091072108147428118993658357889765697190918891/124546036336160570759329727968519702172101080198337732822665530005001933483353397755192191963406131931713704953439765380106530306290937168209193749909922943209327458843272276014173159424*y^32 + 37782428389876293041845005727472197096754171217043831191167519772346790959425434342009569807070080477177797314787055418710459787948713932735313490981542704314587380918426522118085740946951/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^31 - 364149033496328058921763552478236431482601734248950255306800402429872133159422218818116311103734023225258970066138512332102360508823121363170493195229641763168108518117514565497041995653259/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^30 - 522733435136566847384927791575151235987206531365567513976657876135300907531781277326775089542534551298619572576757531164404605479760243912416145574968368401286212488572491669711279874930725/62273018168080285379664863984259851086050540099168866411332765002500966741676698877596095981703065965856852476719882690053265153145468584104596874954961471604663729421636138007086579712*y^29 + 8668836238820614917621735805109122749321955213583702945859096534113604274547785774115411242315977648028082152677443486130743519028804120645662338014314435734325978338374106997274731350510141/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^28 + 37992219884414410865555281410878427697657537714016309664906989334783546571360339599986173726913100908549750757390915648348430960361406161381310479941691484240876285894859218586710990484963947/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^27 - 35296637185558652376618054475731411505333843092219443857619692779538660981081229323535825076405864931665961360596924525578231930824667858689611664525085917263414108243101761092932127278337129/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^26 - 560164586672196411467168005014350878442696940781269483443536281309225804161853104422238240967319998843936562789910680809364186619125245513142491820772174530419309035353337494826936030832898601/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^25 - 769872469432467095456415855167721442827057534342983491733446599153279102294742864333899342016815907084776879070343520451792289158539152204688798988635969103713619808217640192382510573964531/7784127271010035672458107998032481385756317512396108301416595625312620842709587359699511997712883245732106559589985336256658144143183573013074609369370183950582966177704517250885822464*y^24 + 2690065184837179089224840583557947264135116275332626008468162499537794047097827082974088689420325306149231334950720120964079542304663670587287717631119784081446567186602579819283072521904705691/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^23 - 100524167125414098469054335569374483361611508742072807309442561726304307495916412514536734997635888012392725059885920886925242554465610746803900306270997312304126263562809732526156094775448531/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^22 - 4859460295998986417333277999345100665374560855616986151641515605660572957148318094942080333880403567166633613413438670194066650722770716040485163147066226098148087642193195939648532003907379061/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^21 + 2139421628634599193931841571521166502369251244875578092372641146075050707958570454779812782616663556485528492347392029347214215467027275924987169344016443453870990036502434062895125074223784075/124546036336160570759329727968519702172101080198337732822665530005001933483353397755192191963406131931713704953439765380106530306290937168209193749909922943209327458843272276014173159424*y^20 + 10275742369770715919568370672480474004166478427807229078369356856057161879065373877377406871037290864573298387426721650795658387098269416405420338023366190820870767756221049989872478979055491923/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^19 - 9893832082783785789197191580621004343043592741810179842238644007383383483779992596103840220133669567176924608235229292500764166943592363781857098525574315447653266686518406640768715439642007261/124546036336160570759329727968519702172101080198337732822665530005001933483353397755192191963406131931713704953439765380106530306290937168209193749909922943209327458843272276014173159424*y^18 - 984240603259562862668422611920668793539262129373984112167468272185093221916953219025155331989242206430847206116120325621436842800312208379276156489463952961808590617686113827899147559988482171/31136509084040142689832431992129925543025270049584433205666382501250483370838349438798047990851532982928426238359941345026632576572734292052298437477480735802331864710818069003543289856*y^17 + 75693148682405706848712573389354510006919657571216598498438929205262229237374071532386296698611055057419397983293551367262130626752049197111528733912384252305511143655437258876710717502850592613/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^16 - 13207134617182671687578983505176996376278363006055346629469177207610407349791844095522316439353848517978735855198364793466182589247216687014364884227622205452678577070388740585807274686188059335/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^15 - 282439426161141058134208271629860639275086251256951716514600196774788385418789509880292333505695024278503678955869877522968943416830243168954761592644837776951526165118205177385109824005725491/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^14 + 35031061816889476281903291263979855565395713195403501944570802562490561547871278305322225701060978736240061295814557208720307556048349133957856775109204507177467076284250579412088251107020448391/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^13 + 34634435849982493839698551288694869945596972784358206980422669170964849596948905178411447477751348358582490751454231779232606176923664771337626767582616292112316300568001478843826135445017529625/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^12 - 28845910014924391947845410264195273955625780423951479100017161334240509358782976869202708479827527194146827358445540531674860679308394141959964999650405007444901035319782195949090749020574640583/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^11 - 5943255580143451273004809076391042347648665248592441411770468052430853068840295609173128717456594136056120456288384618553136080768572056389157167295246340500875948511348564586428068506251972515/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^10 + 12264357417024948868777247495350058357104918585180109286136375346867324986847961960763683452451481623473183338094805171578392183605139284059608380530095389186663358072868046645109792319722615531/498184145344642283037318911874078808688404320793350931290662120020007733933413591020768767853624527726854819813759061520426121225163748672836774999639691772837309835373089104056692637696*y^9 - 762309188787636146373849818338206531227919834198996959685845151734140600413904638934968809247523048661216732585436259667095687183507722524509382685077455723905978921663542108785678456241071563/249092072672321141518659455937039404344202160396675465645331060010003866966706795510384383926812263863427409906879530760213060612581874336418387499819845886418654917686544552028346318848*y^8 - 180043103283171864665883997899108314884883656633193505902660391260214836287488169747829640898909239578615252782669954103931323873510759561279140681492808573570740624303671440718839871379533199/31136509084040142689832431992129925543025270049584433205666382501250483370838349438798047990851532982928426238359941345026632576572734292052298437477480735802331864710818069003543289856*y^7 + 113780578161820879072272518821233749174733560622787780921598753769623522581952727484223104064092142073199406092929422505325388553957785671437742332016541732947060069976145104742151887866957971/62273018168080285379664863984259851086050540099168866411332765002500966741676698877596095981703065965856852476719882690053265153145468584104596874954961471604663729421636138007086579712*y^6 + 5713289121605872850138883793101574403764127303784439696490950078396904258859437149946122835322114897433499857664318546047032117289321537351988457311320396617507659758237707484897604989454745/7784127271010035672458107998032481385756317512396108301416595625312620842709587359699511997712883245732106559589985336256658144143183573013074609369370183950582966177704517250885822464*y^5 - 5253468710186368280744368510667311094091403339264336777381147723754074416373821316848424617834111852385276461300983869765268422749843833593113904123291465975277022797115570173887919797676161/15568254542020071344916215996064962771512635024792216602833191250625241685419174719399023995425766491464213119179970672513316288286367146026149218738740367901165932355409034501771644928*y^4 - 179815160021840910911144308154683032108524389435500153772223462660954690631249997853725997813981297682586580673459240432939314213656026006402282312719175896293310425039004369138191853863725/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^3 + 105275966182086996017136768619207649204504100056067003826062877430155426402127749017591627610081865162875175043175116957503469865869037529979993955563784668668705533413304638597507068527867/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^2 + 2267396485028795168252973937301098648193157760045000306414360749532919044891760938936414469373764052078631238796827350639270943707863332915958115636737243211124067814239721014366365423179/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y - 757943040642768377656659247137231514531203801899382285850622627364488594352224289191324784887406510832708767275732459872893633783271420348972214446321509698476051287700064967591950939877/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808


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

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

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

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

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

# 1 Loop Invariant
-2912136058731398049362394426616647123923725552948351553555167518968580344833003230897321841348428786819722631574597200873757174268540683589937636327048262468254054910849782038035862209/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^35 + 26593523907597971663273771401694556979479405102882094673899663882740505296679569454206023345902676426009567092364424823461151014710244109399349445697910014480875628195386695594874456991/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^34 - 98489508810954866863744700536934461680265631860885046445781289273440586861301628479310231012473792104079262160351717103370958036212066111765530839438944766922101815591767312024374032801/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^33 + 164872717939138158670169422724976773462215653246875585552504341418869769156452052674117755641112141724319616567279613594791796760096959017306080696752788865828054810921558140547141849371/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^32 + 8815702725401438826617805095500319052661476722741386752251081643590907039723567500641662458753583317929164880337973813552927608751322231807449036531222888912556782933335667557717488105305/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^31 - 84993534727865998474144910222629650698324955115387071295270406190115444188004259631850356765201564004629630727008744143622041554682200751272212521656598889530010801030833562373279531965387/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^30 - 121946470232698363756164960890907467608388266863546699422708907075577453471249966994111543344922254644282350533895361698523585006598387775570789972353770831888296647193800485526029776733137/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^29 + 2024676569507507087863523269914219754832674750199304546866198939708970927221536357608464919978286913166425671219014500747959118396996845618374020187389613268636633901653748313021734698884061/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^28 + 8863976987992153772804911653362212151616323010951301258538401666879431759673514824238804319929271137132337663195830760094407990882437659467004406759233660213542158329189439732004927166196133/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^27 - 8268063336601671767340083364822069992147631053440606675434218760353204224705700471627040398654580851508624067428624851715746874866575678954489411259854058749144690007207765368552917138154477/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^26 - 130702547291085735233805722855691990933906079839921615271305973083225422737915879301412414506939224732817537540208462613937731347897911391238159797652274760635906785291972310873832445453934533/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^25 - 704344313608063237907511233846243453089787839720162293837814423667209771125948751978052364556345181609406365980825500027337911921457763482035848512852011920951369361436071690290448944318147/243253977219063614764315874938515043304884922262378384419268613291019401334674604990609749928527601429128329987187041758020567004474486656658581542792818248455717693053266164090181952*y^24 + 627755471968579241240991892727422437483503445161070596266678859471666560738665703252154327398331259350109974871543672933483566913358204042202510078579351058886134860863207128682208090653206943/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^23 - 24005536621924864933730129052180120621939070959880002072628886667830908912753642974279563174932119893323327086622919771054217744440441837001899605668326748120364229678948948455116969218847977/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^22 - 1133914044470505781115957442019285917697860676552533853554039785984314520590358110733669846470897482611084169780558839477838446902740145912605034284078383917401067133322645225544092382570735263/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^21 + 500226233711974019772168355324473496061918299996287998680870290622512914811398057184832381368322581476762389275545681913788862644241237524406649551959004692921227326111998985301955797503356017/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^20 + 2396015374112887970578901582228307025140111692419202269473800898149577289512551104204064074794139843893217300216012081864829929844381736747550473972067143635852067392649162900894634443709680007/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^19 - 2310723305310663176684497547150832291012328182284433467503393298540504526189184312355044531197765667351040542881149299492624432089227370471868936663093522652274451970795002559594551069107246895/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^18 - 457320430279061723508353265412324435534167819098924392567717756669274740232681801324695731215962333621573510903813832826048712513444212302393753520171513113880543043253857297110531476829787551/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^17 + 17667810358746720816226411747916221148739649776452803165453399348068567850559239991277616973124267843286472976048995775457706842588909707913900884305573912101164209083641511583390963494316420733/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^16 - 3110663347510924777200884205979909462456774738090365133398681697669910096130468889889438747562129721073282394114938739745096977178813971533264913365526244772052224588716595817816014675874896603/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^15 - 527053163241397674071462373778966027947377520057188330864621335580409971905220596608082575481060294419521734461283908705029039862311850566029510301685963769133956373309301912582682076617015041/121626988609531807382157937469257521652442461131189192209634306645509700667337302495304874964263800714564164993593520879010283502237243328329290771396409124227858846526633082045090976*y^14 + 8199404134813325367374027228330628131002365722897569446974908836686481299109475711887052031044150434026299939762047119408948953713260699406436233327368425485105303659103132794426790132836926707/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^13 + 8069735097159147027615146901266201630116529975632698313827406736548237963737253498710903638975472821513857666290596786599281112962918304080489736225074603714613976209938942979790569506503012821/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^12 - 6742077186533753408802633642582504400227839062423944228655154733701001300692040951643489085691367573744882252906099916847398270830916025688021441624576688724925133174349634474909497580584771815/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^11 - 1378609735648686504715083768084701281837931699876060711793222102751352476502963034084710121602455775115820784410795435678494338849803592221652729689401158277873430122040263078437595391052310547/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^10 + 2864097552903154734928758236898920780192072719596689096020357536865309298506762008769736769286457084785933578259060482815362331808078100409697574926322248585518141231949236339166149514512307131/3892063635505017836229053999016240692878158756198054150708297812656310421354793679849755998856441622866053279794992668128329072071591786506537304684685091975291483088852258625442911232*y^9 - 179507154666230782852076820024517914197099424271511660325809208977090895230051118027215792961749458980059945848492276099757692167040819122621592214338194636569258626518051145236043246929638315/1946031817752508918114526999508120346439079378099027075354148906328155210677396839924877999428220811433026639897496334064164536035795893253268652342342545987645741544426129312721455616*y^8 - 168058368793155460229071926156730693233120232613712058022087535991961337756320164757501459872280487092821179571609804609506641030797763829114931115608746746484018593203430658681320905229297079/973015908876254459057263499754060173219539689049513537677074453164077605338698419962438999714110405716513319948748167032082268017897946626634326171171272993822870772213064656360727808*y^7 + 26665576045994983011439126922645266901268629790132492856856791382772771416127907075052623540249484034082006709716524132311412998357342193213078537451439686202564980687462396352219108638284713/486507954438127229528631749877030086609769844524756768838537226582038802669349209981219499857055202858256659974374083516041134008948973313317163085585636496911435386106532328180363904*y^6 + 166383750000736561762937180344481039840082971667662473368878581925763449532896387364432546493704199228193978407819439604445630488579760188270518151400915492454794838845533227398250218810559/7601686788095737961384871091828595103277653820699324513102144165344356291708581405956554685266487544660260312099595054938142718889827708020580673212275570264241177907914567627818186*y^5 - 1231011176960242838812669308624594037364885628972187618716566270054240565135229537275766615551377465891638611298916676179127849678840266135488319077593178533145509482291661591081814746544961/121626988609531807382157937469257521652442461131189192209634306645509700667337302495304874964263800714564164993593520879010283502237243328329290771396409124227858846526633082045090976*y^4 - 41613730426252466928126684100818973975210290106745486997187618429195823074836673296182917011779035380135961392090359806548495389268391398225240282680057396393180024918307074971239125205433/30406747152382951845539484367314380413110615282797298052408576661377425166834325623826218741065950178641041248398380219752570875559310832082322692849102281056964711631658270511272744*y^3 + 12321976490312429789522072016803205590835764624244112096141855882095362485505865329371149482298525319481570817891018242692722129568508593628272063212840100625671323571023647799670130349553/15203373576191475922769742183657190206555307641398649026204288330688712583417162811913109370532975089320520624199190109876285437779655416041161346424551140528482355815829135255636372*y^2 + 511745733868289591577878156535946809962810253745618625864836645247822496408114368129130724583374142178439723224644729504292318799776202940111202805251171506869716400398761662362254901297/15203373576191475922769742183657190206555307641398649026204288330688712583417162811913109370532975089320520624199190109876285437779655416041161346424551140528482355815829135255636372*y - 175503272143558819456187043586041329498871344779746781533413896555134552452716346244668113369866306933290908141387323807464874759783968186118780249822749615676957866340357239368670674493/7601686788095737961384871091828595103277653820699324513102144165344356291708581405956554685266487544660260312099595054938142718889827708020580673212275570264241177907914567627818186

# 2 Loop Invariant
-1645152061628510322965070650154447105961492327834899469021253871278327274558826166743543512792803700287133199875375365877882944064473672331630634068860251402487744199712557358177484242511143366452372878822633200734545698557568001225542265052738764069237997626440644776677427269479088702344428737445138504716554788991994970870887/523269736891772102157499481443004839817403684071796517609074297372099962688395016657130055996166373411206306102918417472009035060116318832814545671365165766180552999193248455105636082305091117523223045269700892968574675177876761562770417312235675081412707781500960865864177809467362681501867431298554800454970959596682758808056832*y^35 + 90279462175521192466501464163514927164308390681823095024907777689906357761670107564745565258684820736020168965574096244398519654002210408554120501464183706931684072826708279984373672399929463420274100126951397055694440568130648929230601767447835610449313394835878342849493081472229808659296013814682381335714264442085663729632329/1569809210675316306472498444329014519452211052215389552827222892116299888065185049971390167988499120233618918308755252416027105180348956498443637014095497298541658997579745365316908246915273352569669135809102678905724025533630284688311251936707025244238123344502882597592533428402088044505602293895664401364912878790048276424170496*y^34 - 169500715800996773201269522970417673160200623122444644578629907712304161503148380389279040587458383000865805701188539541875741243925658524762177022197013312976480147582144097296431162786129452320103338421497292426685629873249321992296448914642792787334255664424846460723904891730810018579037464082100890805958747328753459515606763/1569809210675316306472498444329014519452211052215389552827222892116299888065185049971390167988499120233618918308755252416027105180348956498443637014095497298541658997579745365316908246915273352569669135809102678905724025533630284688311251936707025244238123344502882597592533428402088044505602293895664401364912878790048276424170496*y^33 + 2241004463861291299205486962700827395314449875563813660830692272149165626631101865535707888995902618527311041087379003717816999383701209208822800128657553160957697000449386822661535140752991390183651879515900439529653679426363602674182398940501986299530219740894111443225297691088529075432010890717502941840253823663874941152733887/1569809210675316306472498444329014519452211052215389552827222892116299888065185049971390167988499120233618918308755252416027105180348956498443637014095497298541658997579745365316908246915273352569669135809102678905724025533630284688311251936707025244238123344502882597592533428402088044505602293895664401364912878790048276424170496*y^32 + 4969468757273999590785150005614917531572693476456775281995085223997591539225775571696143204894315608910518397810158215173222181064924685468090581094356541906485674691956946236911466271894188811501763656524031648991506234847087028442215488766905595549511834745550690156092694101974013482327596734418639590910172061578590646057628973/261634868445886051078749740721502419908701842035898258804537148686049981344197508328565027998083186705603153051459208736004517530058159416407272835682582883090276499596624227552818041152545558761611522634850446484287337588938380781385208656117837540706353890750480432932088904733681340750933715649277400227485479798341379404028416*y^31 - 36113575265484507371164922099386633146197337701612611019050472319443791865236004616721644497829840434298794798150872787978961446981369206918702261866928075110772429300248093047274677692237505855629767093175661302892864291506892298298804011524287839103603729756986723949734664619211886672965689446887477736631256390488632996321416265/196226151334414538309062305541126814931526381526923694103402861514537486008148131246423770998562390029202364788594406552003388147543619562305454626761937162317707374697468170664613530864409169071208641976137834863215503191703785586038906492088378155529765418062860324699066678550261005563200286736958050170614109848756034553021312*y^30 - 24924249294952164494770259316551914184751654394181779652616162774187083505142484096046428290773969911825107533362705359651774527731587365397315107874337774716849025192591449081395012855788668454746800582817652811722478618441715307471094073422975333039670984620964908614047184228988842162400116404573191505624476846333984901787469079/23784988040535095552613612792863856355336531094172568982230649880549998304017955302596820727098471518691195731950837157818592502732559946946115712334780262099116045417874929777528912832049596251055592966804586044026121598994398252853200786919803412791486717340952766630189900430334667340993974149934309111589589072576489036729856*y^29 + 315897329577663953463563700189647959278259585464051191335528938837432653685169949027895246325517741329866884476189305878173013868890115976263038642468830616506369365275155269241649199627423427652017864971208320053428377538170846569116718588152182894634558460929021782660185346728795843668235825118402668506313177006730483633258381307/142709928243210573315681676757183138132019186565035413893383899283299989824107731815580924362590829112147174391705022946911555016395359681676694274008681572594696272507249578665173476992297577506333557800827516264156729593966389517119204721518820476748920304045716599781139402582008004045963844899605854669537534435458934220379136*y^28 + 169112062983847350519385405141449620082274693813548480101507832931607068797237693220774396071562912673913977822735200555385107459070468883286167189011966398376790710595705875082691403647014001592468212816265816936288312435227637082516442635149864714894283975307534020415506483989243615309350093388140159854509234449037312191365376163/8868978591385967833177957312593302369786503119860957925577530463933897672684661299273390779596040227308581459371498601220492119662988454793466875785850267223399203376156753476366713259408324025817339750333913440145333477591131551911363005292130086125639114940694251963799623889277333584777414089806013567033406094859029810306048*y^27 - 4939399581506458380330540794174245029036798944474760798951610392521274153081522566108254982859618082760485468275651871185890635983946753138042454522760741821624190211078762695815917668041904532913684601567239992601022770591039151343576793407100291980622191361713928955950093195663196793681728776863123916474259259458250336136966862081/523269736891772102157499481443004839817403684071796517609074297372099962688395016657130055996166373411206306102918417472009035060116318832814545671365165766180552999193248455105636082305091117523223045269700892968574675177876761562770417312235675081412707781500960865864177809467362681501867431298554800454970959596682758808056832*y^26 - 10037579880476806514296037360279304188800765074063010397897865649165726952655034732570779858685390257315346034905766400686832568904094892943314282432102270620276627895507842447162915468171379048087873531850429360491258356942138175925412777316886018018153240181578587629452506042382718408041742572429680938887842260994757489222457171713/71354964121605286657840838378591569066009593282517706946691949641649994912053865907790462181295414556073587195852511473455777508197679840838347137004340786297348136253624789332586738496148788753166778900413758132078364796983194758559602360759410238374460152022858299890569701291004002022981922449802927334768767217729467110189568*y^25 - 4363096476912101615458059698419947459805894896591172189362541105809371208100265199479444812119625689911857285632200221784281890485948569848413322919246365257687059871072692216921761058026471868169908685618234797135494957515333020534155036794408923638956016969689230980476261007528936772360424389994960346483421282810218080400430432007/523269736891772102157499481443004839817403684071796517609074297372099962688395016657130055996166373411206306102918417472009035060116318832814545671365165766180552999193248455105636082305091117523223045269700892968574675177876761562770417312235675081412707781500960865864177809467362681501867431298554800454970959596682758808056832*y^24 + 354092098696005092687761288114985842248639856390626953622730150538590220447454438448223537313961463728924761093512617002832954708787999307340419946977632958948343463664460582521408951360411567264612458178290875037923098190614866514115816021363540411455153576853829975381879612540085275399258025908242886270619537582514433571171480474249/523269736891772102157499481443004839817403684071796517609074297372099962688395016657130055996166373411206306102918417472009035060116318832814545671365165766180552999193248455105636082305091117523223045269700892968574675177876761562770417312235675081412707781500960865864177809467362681501867431298554800454970959596682758808056832*y^23 - 110916191349001895023192429145082057214833872897632922972719023434010266289752237377719524540657298867151499162898246926594482111787137403069070376494582845959899985362376583780254161230417890367259535913913651892114698659793441676812149270816604044216515275339017142995916024977804941097325501302015799580201093607370548027303936670091/1569809210675316306472498444329014519452211052215389552827222892116299888065185049971390167988499120233618918308755252416027105180348956498443637014095497298541658997579745365316908246915273352569669135809102678905724025533630284688311251936707025244238123344502882597592533428402088044505602293895664401364912878790048276424170496*y^22 - 957653440053181819008424075130797264174939573416156817011535373617187038426676693869271419194367171536386484398289090868261874339923825546192288161943068566840148061899572539718103342214812084097210121150049332772849181128136937390772423232368248996446048026407209342762749638276965055459897701048732128177656729670353833750286040208747/392452302668829076618124611082253629863052763053847388206805723029074972016296262492847541997124780058404729577188813104006776295087239124610909253523874324635414749394936341329227061728818338142417283952275669726431006383407571172077812984176756311059530836125720649398133357100522011126400573473916100341228219697512069106042624*y^21 + 1747826962506206418772258670089143918006110270942962342683988101711818896508925500222901983977014359080468025627057371678290761132898623232230152425268121275251808157488930002828947682977895204062238260016314177747072267761545104796276714592947430435309706792706707950378601089253152811195833140486820078466038845642435646525044567071401/784904605337658153236249222164507259726105526107694776413611446058149944032592524985695083994249560116809459154377626208013552590174478249221818507047748649270829498789872682658454123457636676284834567904551339452862012766815142344155625968353512622119061672251441298796266714201044022252801146947832200682456439395024138212085248*y^20 + 1331424854971186264837832103478101761756081337806656490582801190408107071423736689499703723245267239314901942857815166012939029956657464226883438351435538141495329388203126939908393734306629406654246812411274171899835164922210870024342349747368886377447716954011077062503001170125084844745144575777246120112058731185870129490756356915927/261634868445886051078749740721502419908701842035898258804537148686049981344197508328565027998083186705603153051459208736004517530058159416407272835682582883090276499596624227552818041152545558761611522634850446484287337588938380781385208656117837540706353890750480432932088904733681340750933715649277400227485479798341379404028416*y^19 - 2641582355114521617935036706082294621327727282737707718702006079732702465024881939602990471608828003798357061578233722717040377912916588798299577162701649717256792812607502274843044136833016016382249415109381869501212451944481333309603761496169547007691164230548515338040963236873785101677397345733090740538988950121396028517589787260509/261634868445886051078749740721502419908701842035898258804537148686049981344197508328565027998083186705603153051459208736004517530058159416407272835682582883090276499596624227552818041152545558761611522634850446484287337588938380781385208656117837540706353890750480432932088904733681340750933715649277400227485479798341379404028416*y^18 - 1422502463231426716879794218733435375982202510100684244610843639058590449084702141950604558053545954836889708520095665005069607185501633454093002671519177216579799220579330750458610581224844425572510247663908144499557691877000282627663528906110897123718824012335500095139112465580365263941240973475889486396400135609863173684139490579595/392452302668829076618124611082253629863052763053847388206805723029074972016296262492847541997124780058404729577188813104006776295087239124610909253523874324635414749394936341329227061728818338142417283952275669726431006383407571172077812984176756311059530836125720649398133357100522011126400573473916100341228219697512069106042624*y^17 + 9980951344291102974828072786776591641290598045750304929721978545178522110005977815131372045333418388673006213355780447106714846946419013912587884844834686626474143471080953857124533625556353092842321501038650749639004783700129356884635925343095186262825872165368432932621401371221801371293186241493347632126006473002462973836349022649659/523269736891772102157499481443004839817403684071796517609074297372099962688395016657130055996166373411206306102918417472009035060116318832814545671365165766180552999193248455105636082305091117523223045269700892968574675177876761562770417312235675081412707781500960865864177809467362681501867431298554800454970959596682758808056832*y^16 - 278685612560144173282546189546008990193934629117571233831636403281701586449222491240411542372882113440737306238741468192424126511664716483218897977181633006346467981450748928003892190202963631607424571648661851074396757002771798581527822641970451053689332642498556782312817943962431420037122022842670232038098682648944466217271687391989/71354964121605286657840838378591569066009593282517706946691949641649994912053865907790462181295414556073587195852511473455777508197679840838347137004340786297348136253624789332586738496148788753166778900413758132078364796983194758559602360759410238374460152022858299890569701291004002022981922449802927334768767217729467110189568*y^15 - 9377446145878109078664173401967796114090844118289222415756283311166858917785366319209236062921519377754035743718204681006147014305712279307888621310938105620277351915815428448693587857185983533561187257103771496322318194043029275076344650692855428779470979044042735979506561323324053701300822391913544351770397939922642010573004108660881/523269736891772102157499481443004839817403684071796517609074297372099962688395016657130055996166373411206306102918417472009035060116318832814545671365165766180552999193248455105636082305091117523223045269700892968574675177876761562770417312235675081412707781500960865864177809467362681501867431298554800454970959596682758808056832*y^14 + 14569928991260543582830630651309494247874219788263959197469749039050928026994102066535574451133539965643961270123554764318086012661622716988751158345724055909544964789282714537185397954084724370119317254139001629532640418779204315565919185652722966004005312078717858486943493377123269210752333831725668074408578142874311896834775594680031/1569809210675316306472498444329014519452211052215389552827222892116299888065185049971390167988499120233618918308755252416027105180348956498443637014095497298541658997579745365316908246915273352569669135809102678905724025533630284688311251936707025244238123344502882597592533428402088044505602293895664401364912878790048276424170496*y^13 + 3258882729518566722351955801059603700675518062233241424071931005384730246386916817862633200896538666064630552200634675142632766560382435224617092151046305991378444185812465123782896854263449583034216256195024100636089167740750100421656025639040893967847792801819980136293893254235497030221938038125801523581865316163612355432057836288797/392452302668829076618124611082253629863052763053847388206805723029074972016296262492847541997124780058404729577188813104006776295087239124610909253523874324635414749394936341329227061728818338142417283952275669726431006383407571172077812984176756311059530836125720649398133357100522011126400573473916100341228219697512069106042624*y^12 - 1934842082232196186134914978530381534032354761587714532763137842486086525591027057543734941852624638491666035934430914515948123093929803986614783552391341019512119051060224576370541121260873135272028414582302770905255283162431988550823730638722197149675904671215467083763779715574186044473432815879129408660906290662377163840494019438981/261634868445886051078749740721502419908701842035898258804537148686049981344197508328565027998083186705603153051459208736004517530058159416407272835682582883090276499596624227552818041152545558761611522634850446484287337588938380781385208656117837540706353890750480432932088904733681340750933715649277400227485479798341379404028416*y^11 - 18238876108072362845799854424293477929420910878687788276958772888287748032436851423131959406603551670189322973490330941669864821168420912119611246637132367644316829414876200028817328846174141450541484878010519729060602374584210668868463379864283735934223868423745695648642454059985784353215030582968692998809112407403911420156929114741/14809520855427512325212249474802023768417085398258392007803989548266980076086651414824435547061312455034140738761842003924784011135367514136260726548070729231525084882827786465253851385993144835562916375557572442506830429562549855550106150346292690983378522117951722618797485173604604193449078244298720767593517724434417702114816*y^10 + 49858378058746086647081971396794596749213830949149901629497697699928612482198684748468031279124880492319576304942724951740700479377637433440821432654406785795449189242324523198967469483470210020155886515386385747745768022174094434892453979309572053209274364443090720225905568588801974376800160691894123812401678081926383543847713449221/16352179277867878192421858795093901244293865127243641175283571792878123834012344270535314249880199169100197065716200546000282345628634963525454552230161430193142281224789014222051127572034097422600720164678152905267958599308648798836575541007364846294147118171905027058255556545855083796933357228079837514217842487396336212751776*y^9 - 732016256937507410639044892619423061490681689406012491628292831077251487705899483331794326802708826038105395983845789033432610673761554863115130730707603284164087234678171180765308226647325032954200248175336961562122461380413248531494948801497193755604923881076590461424704145765668635967966524694491720582502230446639492838528156112191/1569809210675316306472498444329014519452211052215389552827222892116299888065185049971390167988499120233618918308755252416027105180348956498443637014095497298541658997579745365316908246915273352569669135809102678905724025533630284688311251936707025244238123344502882597592533428402088044505602293895664401364912878790048276424170496*y^8 - 539352702981337575085476970018523556395024568542038782059796394566986136907378932741354138045048596820533194051130822090941215925710330813696686037150907395738719173081780323351666645715019553495281466210635212951316549485462034211552414562132218231099424133245094246739513784994172782134832953737790144386127025791068707233098079987409/784904605337658153236249222164507259726105526107694776413611446058149944032592524985695083994249560116809459154377626208013552590174478249221818507047748649270829498789872682658454123457636676284834567904551339452862012766815142344155625968353512622119061672251441298796266714201044022252801146947832200682456439395024138212085248*y^7 + 11744710889806897162002461756627519042810618789612168169202899003304654265236071787450346951572790966938434813161195904980479599787913876811342408702274945821586935668424555330182509302480337186123969273467785189213299619594331675161617335194737028535153960903303700751488873717551650330049192685745231054293002069483415163981393570719/49056537833603634577265576385281703732881595381730923525850715378634371502037032811605942749640597507300591197148601638000847036885904890576363656690484290579426843674367042666153382716102292267802160494034458715803875797925946396509726623022094538882441354515715081174766669637565251390800071684239512542653527462189008638255328*y^6 + 2671579775279551345386006749476055583743585036732060543327103633977660268085636610106096325073602814715684123879350613610154301815002096888274931557831006693246778999690102569539341451130152852387782875292373313959784744657075519147499604846130009395357649423725876821034084805965189182587267901438924269245683270120681998727294384147/32704358555735756384843717590187802488587730254487282350567143585756247668024688541070628499760398338200394131432401092000564691257269927050909104460322860386284562449578028444102255144068194845201440329356305810535917198617297597673151082014729692588294236343810054116511113091710167593866714456159675028435684974792672425503552*y^5 - 342638428962065755364408952960368315876141294580726800714093068328114888830216178961931018783907356474801349286716905199879809638670008025898221293967824929208875095111459523766270873317291044339500106102294158189312353259508092478732219880280874663770578958469319366436479091794399136266633338209864820112166742170563174279420461821/8176089638933939096210929397546950622146932563621820587641785896439061917006172135267657124940099584550098532858100273000141172814317481762727276115080715096571140612394507111025563786017048711300360082339076452633979299654324399418287770503682423147073559085952513529127778272927541898466678614039918757108921243698168106375888*y^4 - 75159077376472985493661281377931523659350339531872956723292943684360732327159894500774751979665234086632069223238100763555298835505199869402635172158717098210258547766298747440421221274220600606951264192277362252340667865025224381441498588617046700686604679448907574733735432393776765804063386640108742935222375591269952819446851067/16352179277867878192421858795093901244293865127243641175283571792878123834012344270535314249880199169100197065716200546000282345628634963525454552230161430193142281224789014222051127572034097422600720164678152905267958599308648798836575541007364846294147118171905027058255556545855083796933357228079837514217842487396336212751776*y^3 + 19619911911264355947197542321587687315991664063403135006886846170437563139038682174542414009770905846016768814862602220344648074526821252942922835816228306166442113814639159774171514693301856444467753880232090427682536523822004241226412354886783614186803912958394905735182650035822051492174084598802334116698848787469490535292575727/6132067229200454322158197048160212966610199422716365440731339422329296437754629101450742843705074688412573899643575204750105879610738111322045457086310536322428355459295880333269172839512786533475270061754307339475484474740743299563715827877761817360305169314464385146845833704695656423850008960529939067831690932773626079781916*y^2 + 200533054757744763085492696313286561509685053098884741516195736719477489171356096464187055272211732592992828920320627842352814522532764396985276072155105488930029416340870627127502790573309168898871941419411538745247286670105969242011796068182980599257574119217218049299292143125753467555171231239331912586275234635279216529803065/2044022409733484774052732349386737655536733140905455146910446474109765479251543033816914281235024896137524633214525068250035293203579370440681819028770178774142785153098626777756390946504262177825090020584769113158494824913581099854571942625920605786768389771488128382281944568231885474616669653509979689277230310924542026593972*y - 1064797681833311949599736455624077026357746176902771604438748207984064983470290135616183391132866206037598895436352416056203633282064781990223596309631214573646316334633764074509352672841715043251828575129854513260664231887641859303488307092840720496062967586236786931662003342589745582561398166091522468659203593007676875577840131/12264134458400908644316394096320425933220398845432730881462678844658592875509258202901485687410149376825147799287150409500211759221476222644090914172621072644856710918591760666538345679025573066950540123508614678950968949481486599127431655755523634720610338628928770293691667409391312847700017921059878135663381865547252159563832

# 3 Loop Invariant
224437303038651155464900402652534842789469009748470556235573734416480587522851615630565699991178927541547274471543313617211961936408295560535272977431777949870052514859760201206692228890154066936258066790231745868240296024258539630689741552546138588056153944441039708406103470190766934459287232948701270438616465035334671359438949062494887511284710131361259565805591387924253419160608323899448038120465/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^35 - 2090550016369606172882160803599433065536357928824836294897476984617600729485184632547761725407265271279797946464793173284505339506840641085252409531978161881623386277479884192613456744622946824991913815490479530272448993868410951160721433857540548101058764878016047986232332197879822699023375405265268830456821117187897707660814883620644329826449764857137133849520632514284689580637571641196168705181651/1968852413033954988958516671107427600477946298675670253891200338042357928806785163626275883758098490284652149852826525775653800604766318692790305893776499591814798612287648414730963628391611490286401666234993919179252609790588953679583511727224998772951825282726613243499838716591404954391222395311709737892909316234781436290804679785555582959040867098856601083241695633677342293751019691260540964678524416*y^34 + 9124281385405162835087817884974641651586599453836594664801058421944035583640364915585598619249712550445787870952175446563734100735683469420075776010319928187736669884945435252880528304822247004817463908309978980401616344804740556177143334033531426676794052089841077176245538879278039420370709290389070093485630955304647549358657734890460914593384660314517474713093217040652282412661977578724269594032565/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^33 - 13138500296287227972898786227840195687630490678137496231483867174555237552650942003487449708829210334525779691365969024558837491372473586804308674570060802945642462519745792100089299848754572113549484082228991515704225256320780313912533109451422882086762473903677437030145682700673734000415488516118439435094080838922010066373532161819810714370468817373369514511543915138724384622086904678589344574336833/492213103258488747239629167776856900119486574668917563472800084510589482201696290906568970939524622571163037463206631443913450151191579673197576473444124897953699653071912103682740907097902872571600416558748479794813152447647238419895877931806249693237956320681653310874959679147851238597805598827927434473227329058695359072701169946388895739760216774714150270810423908419335573437754922815135241169631104*y^32 - 660054779978247360299153425746503500967039416750264281046525547845107885171703781293999279515920774186699037339380199376692769420619139783697711514958872427933686281812365890257726753437088256350564559083901419772189727128728882082785551258393630501618377871559217812907302937827835560180360593668437295417920522320635746004878903100831617623240663715921879921525817525639635451873830053951419110448749023/1968852413033954988958516671107427600477946298675670253891200338042357928806785163626275883758098490284652149852826525775653800604766318692790305893776499591814798612287648414730963628391611490286401666234993919179252609790588953679583511727224998772951825282726613243499838716591404954391222395311709737892909316234781436290804679785555582959040867098856601083241695633677342293751019691260540964678524416*y^31 + 6790010561006538366607860251688237871937578037728727904788350187092782951009767018042168797239021601850170334771605044210186548381979481536259736460725408317323536827138410721122338664583319996090671061367325827908287743041644795569379822048537340997088260446501748601372066895046098014463316232404671470529626470735981869961851245953620849868974585775039616479886919194763096848691491221994646406375104459/1968852413033954988958516671107427600477946298675670253891200338042357928806785163626275883758098490284652149852826525775653800604766318692790305893776499591814798612287648414730963628391611490286401666234993919179252609790588953679583511727224998772951825282726613243499838716591404954391222395311709737892909316234781436290804679785555582959040867098856601083241695633677342293751019691260540964678524416*y^30 + 24925810903922105312423790047696926510025777576761539387720831580613452769716228590164420028612739850112147371428674305712352022685877118557809181720631453582696219172575962567591150080360353429807926430655640726570334908152922892558106375046234936224130160489749391019776685892925348793148874334055569272762448624830937062448290601640066721924003455427371273640605277352127654451044012696001090623788463/1398332679711615759203491953911525284430359587127606714411363876450538301709364462802752758350922223213531356429564293874754119747703351344311296799557173005550283105317932112735059395164496797078410274314626363053446455817179654601976925942631391173971466820118333269531135452124577382380129542124793847935304912098566361001991960074968453806136979473619745087529613376191294242720894667088452389686452*y^29 - 16479781152798269433298796464603567541687576480742568497020121696522170532072291420303412527623505105175029844120775248841082540952903028796886402304444186216032433626360228499906300504898501911452077000272216122663870237495277589136911287470284894349041678491389571483309055880715144360233090513947495711344697732996537948245635421677773310854486074376347413458518467917417082448937870198339367396252946335/357973166006173634356093940201350472814172054304667318889309152371337805237597302477504706137836089142664027245968459231937054655412057944143691980686636289420872474961390620860175205162111180052073030224544348941682292689197991578106093041313636140536695505950293316999970675743891809889313162783947225071438057497232988416509941779191924174371066745246654742407581024304971326136549034774643811759731712*y^28 - 11003136977834957082904130789013614291145553403526185601668925684385293373982273239598536938701095381459592915489350076140311827717957667243442604865337676198294766204152884670732304760419564396645188430125673637263441777805187247975150712305993422683944210222120367559466731251063399605916002581701001632055250027202583190069445678630105385567477122587390214170304167757151756630097972042057413337617806219/33370379881931440490822316459447925431829598282638478879511870136311151335708223112309760741662686276011053387336042809756844078046886757504920438877567789691776247665892346012389214040535787970955960444660913884394112030348965316603110368258050826660200428520790054974573537569345846684596989751045927760896768071775956547301774233653484456932896052522993238699011790401310886334763045614585440079297024*y^27 + 1104993681798919607207881991979594979837754142925871187860090962819634703178642411313344753197282309256538535565520236264403198336753380669838825339449765564113171266930738604230059621791288999139766615841892336348801850009295140521900853124295391435419321880737290589028583894709064441391180428793722300098593918674159291856507779297797645938810725082421163079411678827174402905855857207500844133219502120457/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^26 + 876046775383628824158309121954661940172076508122344041381824325666711371954831841867854555397051958243785363807831189642637073570721121668963334630197764415332679004909782641707974332709422845821762380103279706946525191486237445136977478180017211629872809707985525094593899525469144364480656836282461379730188165628348559108957356755103486720661860863490845824428537040217040195926155032372994161429490620319/357973166006173634356093940201350472814172054304667318889309152371337805237597302477504706137836089142664027245968459231937054655412057944143691980686636289420872474961390620860175205162111180052073030224544348941682292689197991578106093041313636140536695505950293316999970675743891809889313162783947225071438057497232988416509941779191924174371066745246654742407581024304971326136549034774643811759731712*y^25 - 648506677141649018188471262118297966013444840619343502541767818137382426849644971542028699077069758283775553089494694234243990337926277884017828456269596144654715018776472446148657463185412962762211390014252650177994522183870496094631314149603230809480920644443790429132647370901583195184751160241367331430332289143660102257945761028900240763757419638726062205368578756162335438230495332357663506340319871937/984426206516977494479258335553713800238973149337835126945600169021178964403392581813137941879049245142326074926413262887826900302383159346395152946888249795907399306143824207365481814195805745143200833117496959589626304895294476839791755863612499386475912641363306621749919358295702477195611197655854868946454658117390718145402339892777791479520433549428300541620847816838671146875509845630270482339262208*y^24 - 47178808284019298747334952622225120849972419561032362572405528870208971343893472635946146603069941459394282205944664274031956206405840209103405671272079976991635482619091489326132941186301182848520923206347776644454056149930489751229205382375862220154627984797663308855388922064576488413136860901486844298484151820472732738595087884870109652547308792313416223537128174009544044233115110505118680784016365578011/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^23 + 10333188458714613759188459467519057159334374059071997011914402121096316084853689791729522092306914741001861710185533614255728123158502800120142518640994938902896211507643439328102085165583104446319364949367056948322686931941057380347002322367397876884732321518844667784464148776909872933100533459722920247601612045132227348551423892111193456324420629624925720330886096438552624805807609416797659108840886266789/1968852413033954988958516671107427600477946298675670253891200338042357928806785163626275883758098490284652149852826525775653800604766318692790305893776499591814798612287648414730963628391611490286401666234993919179252609790588953679583511727224998772951825282726613243499838716591404954391222395311709737892909316234781436290804679785555582959040867098856601083241695633677342293751019691260540964678524416*y^22 + 82955128211343309217108413805120379591100298115359529162819704251626038523195118800024458177073126260198430585498433317787672996304898289593009513887547388062430977000678773671312680993394851209647369756189442346761356960269687902298696229233312891307678925907307558538880795804274182327755462647545211979913198883135157172969753280716592756761779692917726143773201947352822126791928939155388429068392193088665/1968852413033954988958516671107427600477946298675670253891200338042357928806785163626275883758098490284652149852826525775653800604766318692790305893776499591814798612287648414730963628391611490286401666234993919179252609790588953679583511727224998772951825282726613243499838716591404954391222395311709737892909316234781436290804679785555582959040867098856601083241695633677342293751019691260540964678524416*y^21 - 53326185703600652738813783492981703830941257632434087576653024657139178403602282921698094483212127189366648659133043566405039725459581541199200891199853779523085705411037830624811952246137429099971330293497763689298360455903648367406105122236912749613773773165647038864179136016889953875180934621587554195554419513787875640436232505345334497565603804429216114137029846031735804583195088948403372182269771832155/984426206516977494479258335553713800238973149337835126945600169021178964403392581813137941879049245142326074926413262887826900302383159346395152946888249795907399306143824207365481814195805745143200833117496959589626304895294476839791755863612499386475912641363306621749919358295702477195611197655854868946454658117390718145402339892777791479520433549428300541620847816838671146875509845630270482339262208*y^20 - 143460066083248747382685332625545786629111946024859397447699587802697050892362482687721913966025932067797801148657254941153628955468451251118723302211465421834463992491990200501383957593648807275888703572440735134102479637345398074304460038568794235210873202727626541785044394937085450014019397294307849235260031017158294353616111076537732187463265076884504967675586597360071627532241889546269061613880740233211/1968852413033954988958516671107427600477946298675670253891200338042357928806785163626275883758098490284652149852826525775653800604766318692790305893776499591814798612287648414730963628391611490286401666234993919179252609790588953679583511727224998772951825282726613243499838716591404954391222395311709737892909316234781436290804679785555582959040867098856601083241695633677342293751019691260540964678524416*y^19 + 201970144752894948029569328734276901814394030371725863046017211099241302450364991033367177740822558513497212803208242949929736645482729743192127977645203113948294377689957602961640851103872768618948179730266424787257093229589346795178709455142773098748880424840409302286812649850827635777122708492217296257742400998407726284932999136843371517346941694138032515673375875692684623083982358068249150257239780401951/984426206516977494479258335553713800238973149337835126945600169021178964403392581813137941879049245142326074926413262887826900302383159346395152946888249795907399306143824207365481814195805745143200833117496959589626304895294476839791755863612499386475912641363306621749919358295702477195611197655854868946454658117390718145402339892777791479520433549428300541620847816838671146875509845630270482339262208*y^18 - 1112935983600268885310294606584029648965026411914797883298382297428179355983366773036709556197131766789710444911952978955737270221261764137446091141814042650484858347670149266990256898765965211117879423223613481058004911386507102961325066455693982782404502718617597107004582351749933595275671194919551950400119283746093157902885774936487876430504933092316573229102634720218984017120586194985407918740264712035/246106551629244373619814583888428450059743287334458781736400042255294741100848145453284485469762311285581518731603315721956725075595789836598788236722062448976849826535956051841370453548951436285800208279374239897406576223823619209947938965903124846618978160340826655437479839573925619298902799413963717236613664529347679536350584973194447869880108387357075135405211954209667786718877461407567620584815552*y^17 - 1326082143058567053832850983716952098608907468625781268783035269781297623575415391258525537491465137442273248801777148680622237712145122075911611191613546021013074011615286354359738733658622517735137109576275127099028341229518971840062489810424161442602298904944692005608233907310181564333590212760494501414871553653104488131078982976056122348071096869431339227739902564912399195441617589164530310528780529503757/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^16 + 64489226553463538216019585813525481640896684247177881590422490365197165727815067715404376570453610972861254500454320961813668661386265931741297337225562759954395164706186329784232755509961322838949163303583336494945798254267971869099435759663356403823431260205141724864207876026849253064970138616640859134532305906771069589070461734706602378791400984421083325490459921438790952348513539626079263131177974894857/357973166006173634356093940201350472814172054304667318889309152371337805237597302477504706137836089142664027245968459231937054655412057944143691980686636289420872474961390620860175205162111180052073030224544348941682292689197991578106093041313636140536695505950293316999970675743891809889313162783947225071438057497232988416509941779191924174371066745246654742407581024304971326136549034774643811759731712*y^15 + 250124622927604318739703464148600339885332695416725090100077719837113700388596153699268451972523389813602754344083310606599662777122430570944530979186035006051945585376120283158804713104429605343958968877311130614836116186163816716393795012506882516159906141729917377415186823922411788808190651715375303971682521548843211172672905522121168081020407284325444807571948399587708372684076805327151108333365125222673/984426206516977494479258335553713800238973149337835126945600169021178964403392581813137941879049245142326074926413262887826900302383159346395152946888249795907399306143824207365481814195805745143200833117496959589626304895294476839791755863612499386475912641363306621749919358295702477195611197655854868946454658117390718145402339892777791479520433549428300541620847816838671146875509845630270482339262208*y^14 - 952615935660544670331970796375816029690182540225733137103720088356677616695088382430103802082854394013396821808738120330840392709644845396492631628321472111802085343209301227594963955548782006333953794767818126336059347154549963776775689079710399770652131737194714972454768692241738296016821122726246481636834498223678507170461800243892113937298630234032976106996521315973267165339999389860584674083442379688743/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^13 - 253734572624002270510177813374031330320397529526174769048197848455781102189205702692316475874199135118366328749405933794925547510942610342947415583108907091758992127772438844368017892076079648525488292237584197055437634620278038007603615790675261178178021845778841305922713991756445319131005147849787215897075347865498409276340667498882351514375219221722201829139711103267536187042276504418608659606721333212365/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^12 + 565013060456777459120120815166551646904470632392361957337285274184078067594976672858260084599970443961695271097863421070968256129971564633162974764453545639822786775809389874082780675538050297162710018147952953715747921271023994419477903623486318831842503527507234556365032325611256599836402460960886047403825994079890739331836487523263978288538668659464964815374024783137809085331845318003515648060009804090803/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^11 - 93930756858789786669983043969277709974689335660483320858848327287367438000265563741016762673934271743325213291551065955194454873413539666149738040383722059509488625493055013336469944378979514689091759788892824774076468446342431443578981998494740583981410152951026426979407833559496121439862135828558806786715353115095538156137754539302940485782443377495962534080597803974449637724867725756844742278450027048761/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^10 - 163372836747177049993465957440610853809974851081629897649003270448215012094659248770929524561588096277239405768995975424730221085255060040751769279534716786688218892302009004415885169335348857757148348933474777043555651664298873790582672026597629138533544767150710025757200915621247203133431165057867655416092236084989390440542979886493784279656141427205951144617770539562786230373332422194102518921108312231783/3937704826067909977917033342214855200955892597351340507782400676084715857613570327252551767516196980569304299705653051551307601209532637385580611787552999183629597224575296829461927256783222980572803332469987838358505219581177907359167023454449997545903650565453226486999677433182809908782444790623419475785818632469562872581609359571111165918081734197713202166483391267354684587502039382521081929357048832*y^9 + 716225748660710169171212682949706854605922924782059372280286373033095754490658660216616546929060995560762229433144751040694890050376352224277673591769529321066585573805689606495561358552144972122539661487570158847644010026148805726752166757527698435411554957878333900380075436744537859779748796673474409090604707801220855192578745654402931482569206980122170492820704983299069127137043787883397786807060533705/37148158736489716772802201341649577367508420729729627431909440340421847713335569125024073278454688495936833016091066524068939634052194692316798224410877350788958464382785819145867238271539839439366069174245168286400992637558282144897802108060849033451921231749558740443393183331913301026249479156824712035715270117637385590392541128029350621868695605638803794023428219503346081014170182853972471031670272*y^8 + 153958396701082480556096158517744825294595449347419944693365157947150632868380501522916409389379077609623978967694579641920541699176823944442179149854287865216507594927901446281631209605258394253772085816141646294759394512067914476265064754072108017522076246246281574154283036140246927206788186595121906437193007728869916283401509033474494476237386711452960548987686783774652811405339565354998760348841254925/30763318953655546702476822986053556257467910916807347717050005281911842637606018181660560683720288910697689841450414465244590634449473729574848529590257806122106228316994506480171306693618929535725026034921779987175822027977952401243492370737890605827372270042603331929684979946740702412362849926745464654576708066168459942043823121649305983735013548419634391925651494276208473339859682675945952573101944*y^7 - 1166330250161891135062759030594520087672838017948300710239901660289687504582821873439143148222735021076224617067459598943294368412466791743574423547188851272002986505994808905231010010608032231449375232619381933856501082586067907590571263780707343127420777898404645836287580645668597889595829856889232550653094548419157246055133813767693017818918555978721851000342012827923128248303352577897284146952332133523/246106551629244373619814583888428450059743287334458781736400042255294741100848145453284485469762311285581518731603315721956725075595789836598788236722062448976849826535956051841370453548951436285800208279374239897406576223823619209947938965903124846618978160340826655437479839573925619298902799413963717236613664529347679536350584973194447869880108387357075135405211954209667786718877461407567620584815552*y^6 - 342667725977375032397169917904206324321000487946305216760394156373672437393043768976745190244808406097395452318277437393114183753750265585193528681526759607897473051268997679034230844682319550929407068469008486802070631902324696422796160341881398415649848789378696969578633152186689047062253333244932382412339801415892760840537429512239360305119952508904212347341741767752017673894470375059585911813125519/15381659476827773351238411493026778128733955458403673858525002640955921318803009090830280341860144455348844920725207232622295317224736864787424264795128903061053114158497253240085653346809464767862513017460889993587911013988976200621746185368945302913686135021301665964842489973370351206181424963372732327288354033084229971021911560824652991867506774209817195962825747138104236669929841337972976286550972*y^5 + 33077334591396613577329067345210307436756772887888335166378903591808731881007696349901419102366645512806295638213164609654744126196274643561085332741998378645066899017961118595518833921191454785469115147731289059618915881044817604199656997318935269855174228133749346084527341959014187281394637615758714655206486285081236665651830984370623702351916134164535149137370444572607669471584623385995109978213852793/61526637907311093404953645972107112514935821833614695434100010563823685275212036363321121367440577821395379682900828930489181268898947459149697059180515612244212456633989012960342613387237859071450052069843559974351644055955904802486984741475781211654744540085206663859369959893481404824725699853490929309153416132336919884087646243298611967470027096839268783851302988552416946679719365351891905146203888*y^4 - 946453243101439643147940915493386974819436057451518106374588128656947343553898622511443096876930799996358989648431938563573412594310784302032020834997821693360009704980590966895826092360299652390038690857668937465187625724406919666769368655274148418376110734687904259926363411356427072451242305610624775941542985647083459183666135692665684575353330479549815008554364701057296005929483497454891226895907341/30763318953655546702476822986053556257467910916807347717050005281911842637606018181660560683720288910697689841450414465244590634449473729574848529590257806122106228316994506480171306693618929535725026034921779987175822027977952401243492370737890605827372270042603331929684979946740702412362849926745464654576708066168459942043823121649305983735013548419634391925651494276208473339859682675945952573101944*y^3 - 938673117990032663009760248739956797551919232863613501917153791144538346578216325213426018451644730774006098968896150120690669477170746443403877981214297773210081233649863970621051614055114705523733822092506687152239328772400857391249898209478125689288249104552011751573200781974834564907595273405412147017996390014786060680914134538611976421070462323353654586768914837028022964673396025068583947956144581/30763318953655546702476822986053556257467910916807347717050005281911842637606018181660560683720288910697689841450414465244590634449473729574848529590257806122106228316994506480171306693618929535725026034921779987175822027977952401243492370737890605827372270042603331929684979946740702412362849926745464654576708066168459942043823121649305983735013548419634391925651494276208473339859682675945952573101944*y^2 + 9616320824502849214095714368181825975906965330570310070020078736748919874517916809963251311650451585185090212064821937599757993709570332230791561251284994228307286595459569971200770418568866301657507268389303910313856549067627770497747467221942774570004633231663840057165036108011238085985382053230470505092350746342755630394497976614593549114613935046786930088650441433367326431606933167242097611979831/7690829738413886675619205746513389064366977729201836929262501320477960659401504545415140170930072227674422460362603616311147658612368432393712132397564451530526557079248626620042826673404732383931256508730444996793955506994488100310873092684472651456843067510650832982421244986685175603090712481686366163644177016542114985510955780412326495933753387104908597981412873569052118334964920668986488143275486*y + 5650985943271888372655279744993801220886710886441328703226321752796687450434033835226075981482212032533722168476316060747226563336794423292438349585857539395004012128878898526634762515200204708701402832086023537430809033373221314628698600503171590263103318786190824665197183190240822524983707709580387032597335964118119545745656606239346367334184220714865722725590115405525120600144035198251005618903227/7690829738413886675619205746513389064366977729201836929262501320477960659401504545415140170930072227674422460362603616311147658612368432393712132397564451530526557079248626620042826673404732383931256508730444996793955506994488100310873092684472651456843067510650832982421244986685175603090712481686366163644177016542114985510955780412326495933753387104908597981412873569052118334964920668986488143275486

# 4 Loop Invariant
152065937931385936604849926867711325939353304041569417516506785918343592976340173258553796131075111595731732877617637929076682925103248518103003863915337726898311923767235807138779709196281677568278975673066273356988006421985171273307105604729114725676267949858472163677381698915739631694612336195314994422832995637727356397256222375978846744327826015580578448923545692183425950027993733810851703572568542337642576557758457001657624321831763116453338532427206474783497803141586661375918021729321017199139685958900970413427666288288231755046216322683/2165751741742189630694442761787647898997319427986139458883022258022933986105564720254982684339453837393207642157748300586824267137748658171564458792916143541303766315100775122346482032883060728863671821874610296015442813658263297251028518792426443019898180714235736825437568094306982896959000320711944884211673528804603308944808358228390308952164307557017795438010614912223103467652682523837681388409111186114104577151987868421636922141484900422196159716139827582073081146143670646749240976487555540283531356429895798585564083155062139843264844764759040*y^35 - 3768052327872078572408541614159775636937796974902397058621044725845798500614618343724876388694802253642728752380638600584988277719629882253566232186254282717347309625693678636386041612732080122510968092212781607634734281689926148228479096681966291269175842110461575348156407954727970461209671987370327665191269314931440823454192056814119052408652572515269665534466467775450079131921758980261992585615803256464746002931160211589418563992451420622553646302487236018727623244030281800532537769146577985642346318453413481370730340501936696872893025832791/2887668988989586174259257015716863865329759237314852611844029677363911981474086293673310245785938449857610189543664400782432356183664877562085945057221524721738355086801033496461976043844080971818229095832813728020590418211017729668038025056568590693197574285647649100583424125742643862612000427615926512282231371739471078593077810971187078602885743409357060584014153216297471290203576698450241851212148248152139436202650491228849229521979867229594879621519770109430774861524894195665654635316740720378041808573194398114085444206749519791019793019678720*y^34 + 3028756169745933432658983850396152149586794489752018570734026877750259089674479888451022361533718379964468654355594301025278692649004709691110244219708611771081163264441595131995114986535592632864632215568539619237218779948610393974503388878797421007501057794437760273310831073172558271023375519930070266646227468009919275451963066991545411322817995243128622823962856448021234997253719578084539545267568205790197069250009355733365889923251010105273790808864616286379823352057669926729807827378689565319810195144674737753108417530873289915286109629927/1082875870871094815347221380893823949498659713993069729441511129011466993052782360127491342169726918696603821078874150293412133568874329085782229396458071770651883157550387561173241016441530364431835910937305148007721406829131648625514259396213221509949090357117868412718784047153491448479500160355972442105836764402301654472404179114195154476082153778508897719005307456111551733826341261918840694204555593057052288575993934210818461070742450211098079858069913791036540573071835323374620488243777770141765678214947899292782041577531069921632422382379520*y^33 - 18929862945539795557669674930598082740788995603725395210741506648064915016356156728554882291888332775509446599997232805714932431506579156007926275419558195503819871726454236449810891814674169098887895988444467022744067899036214302590959994981868938640072073293166776813910967098947427826765992416029348539973157424483518782382528798742372841462032316960209154120978754611605786686959983238425448693216394722573205834550812962505624642653798235553767965296992901260914897948774376212575860507869600174338972843926647269379791916057650436571758139049055/577533797797917234851851403143372773065951847462970522368805935472782396294817258734662049157187689971522037908732880156486471236732975512417189011444304944347671017360206699292395208768816194363645819166562745604118083642203545933607605011313718138639514857129529820116684825148528772522400085523185302456446274347894215718615562194237415720577148681871412116802830643259494258040715339690048370242429649630427887240530098245769845904395973445918975924303954021886154972304978839133130927063348144075608361714638879622817088841349903958203958603935744*y^32 - 1795108949432102757510496078242188446571046166436529601582105088027699131652964506737496221727594992202753657621495548410004674327598957501522887044704126268956453156612349986778063135737332230373838654657892004584380352402807380338249502244616596108584306708467365423947090766272989458834991833394159021297212616423079205987371470957298848717471232606793809590771058260854245825569937425910484455465762212316845700038013092541195190866595161266262130510589364348562704394171988639159949353946746045696067623126760291128517575213101566275834254299941527/4331503483484379261388885523575295797994638855972278917766044516045867972211129440509965368678907674786415284315496601173648534275497316343128917585832287082607532630201550244692964065766121457727343643749220592030885627316526594502057037584852886039796361428471473650875136188613965793918000641423889768423347057609206617889616716456780617904328615114035590876021229824446206935305365047675362776818222372228209154303975736843273844282969800844392319432279655164146162292287341293498481952975111080567062712859791597171128166310124279686529689529518080*y^31 + 18319211142517397515108861405189885345799990602767197624157546237586859560694036446404655842316697528391915940534484342878012803349343606654784843852524574048227836979767243940325908674455417997765867404313824666758824657452426067184502616360325472606541683711490649170852194729578472120909554397356479396089146297489169822402197255617401825475212597330338728680839042499720652256926022382371055842714386376323986482999879751361608115518583837026384105340190138407592830246572893961111270895099375078878512156104933715571280163509474307267841346605461027/4331503483484379261388885523575295797994638855972278917766044516045867972211129440509965368678907674786415284315496601173648534275497316343128917585832287082607532630201550244692964065766121457727343643749220592030885627316526594502057037584852886039796361428471473650875136188613965793918000641423889768423347057609206617889616716456780617904328615114035590876021229824446206935305365047675362776818222372228209154303975736843273844282969800844392319432279655164146162292287341293498481952975111080567062712859791597171128166310124279686529689529518080*y^30 + 8718900797768492170600603138044565568243788651968084673340187523358733488027861493848378938631095865862661194992467379804983838528889536347642804578928336861717396845546247764382610601662476892314567369686217690463746558574654825349277788867810148280347856934467740737738917590369573387317246491010605488385480499622808874917026552945616699498054757049874011393710537875442921119621186304338663079876840605561386882749609932663715534467077368895553872249425157658242994967200816499651489051225646075842037896419982607154475479934707038868533361430490411/393773043953125387398989593052299617999512623270207174342367683276897088382829949137269578970809788616946844028681509197604412206863392394829901598712026098418866602745595476790269460524192859793394876704474599275535057028775144954732457962259353276345123766224679422806830562601269617628909149220353615311213368873564237989965156041525510718575328646730508261456475438586018812300487731606851161528929306566200832209452339713024894934815436440399301766570877742195105662935212844863498359361373734597005701169071963379193469664556752698775426320865280*y^29 - 2739304004662554490796181021049253323256446471535870399010957629188111674194778471363830201416179405708198359553684918205997635770892866266228925131679511715672210670257162639555037383240280017137225881002459620481982977212054625283035142150339628048182836752827628429774144177027823304705546189971712381737016941086104282514866978013230334979417721149636217927362177910381694653568752667762893091360186655284976247333309811097480941163421979273944449224394879946735430805675865734557388613105646930922426517764106102007714617288326198569230266408391677/49221630494140673424873699131537452249939077908775896792795960409612136047853743642158697371351223577118355503585188649700551525857924049353737699839003262302358325343199434598783682565524107474174359588059324909441882128596893119341557245282419159543140470778084927850853820325158702203613643652544201913901671109195529748745644505190688839821916080841313532682059429823252351537560966450856395191116163320775104026181542464128111866851929555049912720821359717774388207866901605607937294920171716824625712646133995422399183708069594087346928290108160*y^28 - 3996597199944712857230374243669030319338469796485114991390173388291762742382446904429906159263306931518327033769876549846546155509140265372101248204551339719010397548365867147174228317313283320369259726613541302141865756944583176827224024867351888829790422159155053279648807668639096355477259153280655244956885483423848550013822881937322620556844827083625571597522622008109089501777312367914146686603299836724766297673663290768048698538311226205158010101689530238314797328537486492773462239470737104415540232893485481049748693614839234682329668583043779/9788708437252834489014430561752080899422912668863907158793320940216650784657919639570543206054028643585119286588692884008245275198863991735884559516005168548265610463732316937159240826590104989214335918077334671256238705800060100569620423920571493875246014527619149493503132629636080890210170941070937329770275836404986707095179020241312130857239808167312069776319163445076173865096870164238107970210672027634370970178476241453726201769423278744389422445829729184511101225508115917510693679039799052128955283298964061403679471887286507766168789897216*y^27 + 353768247771058308846729230008315460476848674562594705873428394155453508846504441246866567288438240533377203078876711622508306254532769590887515558956362822538255498942739817523099031583612310953697923360347921534276215857414726417125868910468635087070756997150183737175039382103383173019782583818858136974977859279778245142725169699486702348909672178669980861683902607409421762836694417272565720760079736189358773805738985167920888945845717640514150504194378678684428992594444999567322097652375656086930920951140138154745181862635689568490323753934462909/1082875870871094815347221380893823949498659713993069729441511129011466993052782360127491342169726918696603821078874150293412133568874329085782229396458071770651883157550387561173241016441530364431835910937305148007721406829131648625514259396213221509949090357117868412718784047153491448479500160355972442105836764402301654472404179114195154476082153778508897719005307456111551733826341261918840694204555593057052288575993934210818461070742450211098079858069913791036540573071835323374620488243777770141765678214947899292782041577531069921632422382379520*y^26 + 158679775300528090763828242585030837450552639314738350125157858328244681870800065069451621865491656356631764387223935218709292713988894603539742126972104783546774041599155062462614623698470645435143638788250384097904635624274417322695884206639372749601695619002748951891116744613736628095290545625030223777936605477746365368238189208061803462925537282793841524802655797752456425612818782082269784068726469445571210871727217107456065650410249938407880938390057031589021934644189135677639607963712238469412067520600902877743440276642298462478230046708853283/52503072527083384986531945740306615733268349769360956578982357770252945117710659884969277196107971815592912537157534559680588294248452319310653546494936813122515547032746063572035928069892381305785983560596613236738007603836685993964327728301247103512683168829957256374244075013502615683854553229380482041495115849808565065328687472203401429143377152897401101527530058478135841640065030880913488203857240875493444294593645295069985991308724858719906902209450365626014088391361712648466447914849831279600760155876261783892462621940900359836723509448704*y^25 - 1949149112204707810154412760397551560447253868303238409459709057972976865395032009367438204500694795439193994758765543726977910607745318562515460604835838102951948061513979347216469949057788205835918962061321510009808855013075636827205801733541606206166534300586439294430584419035670982454461164739753027277524556277127940175457999569444979431120414007370907790920685319138865733279896649708194458461460067871206525775175974936175461295354252928616275331856148069858025957018525082236507006189758437566649265738724890251610106038807840757924346665467050093/2887668988989586174259257015716863865329759237314852611844029677363911981474086293673310245785938449857610189543664400782432356183664877562085945057221524721738355086801033496461976043844080971818229095832813728020590418211017729668038025056568590693197574285647649100583424125742643862612000427615926512282231371739471078593077810971187078602885743409357060584014153216297471290203576698450241851212148248152139436202650491228849229521979867229594879621519770109430774861524894195665654635316740720378041808573194398114085444206749519791019793019678720*y^24 - 63842972607972143861867048466218339477114403841407205020786508253439532676695643814189023270824643126361735123447647349260026363540860441387790882253432498443631536159093472054580114571159111450766524050626998815455358313827741243297477810383823291457000820529976610509080438586661574234094808142987200423879645815430263882644568706030271771324947969148190951906917584745287131493811796287690478168456812799479066304253326989848273084895981240280579114791945196409625222708040026116863557492299963435314308331132543206047823968666905093168621305033579108299/4331503483484379261388885523575295797994638855972278917766044516045867972211129440509965368678907674786415284315496601173648534275497316343128917585832287082607532630201550244692964065766121457727343643749220592030885627316526594502057037584852886039796361428471473650875136188613965793918000641423889768423347057609206617889616716456780617904328615114035590876021229824446206935305365047675362776818222372228209154303975736843273844282969800844392319432279655164146162292287341293498481952975111080567062712859791597171128166310124279686529689529518080*y^23 + 50461885471214452049222733333570966507745976815766259500566316137556691346845406526685882931244710295819268469060950421214208288760072081560369550988519866860813509133206838277310640504921882636099714458264936061930535763629825197420873282030491469034311465833954821766736130587668865343658019365702667429933741812632024442736429208739045619267981885611952267339747246756502451539594273553814728807313179338315637302026623112219235923451519350234217712990078176286137018575188671086029509145466616009765866891685287498069719481690986522986488958549948382183/8663006966968758522777771047150591595989277711944557835532089032091735944422258881019930737357815349572830568630993202347297068550994632686257835171664574165215065260403100489385928131532242915454687287498441184061771254633053189004114075169705772079592722856942947301750272377227931587836001282847779536846694115218413235779233432913561235808657230228071181752042459648892413870610730095350725553636444744456418308607951473686547688565939601688784638864559310328292324584574682586996963905950222161134125425719583194342256332620248559373059379059036160*y^22 + 112472688033542989580414745123208428668861441455599153662440225676184918227380354017227218662674250586994881566245739738482868546517701316213549305431002889693596610949463736843665265687902626745247020051011092602314344141335137825176654246068940482834087650608351314208855619868401025411901672348728796175623581587184313011952621845457600277147078441829118894344783975396274815064505183065650366413189777442851772218916465479839963477961212999505933799992058651557761438290936208032274251800420166430327202716933531632800016307717876777135547610592127683257/2165751741742189630694442761787647898997319427986139458883022258022933986105564720254982684339453837393207642157748300586824267137748658171564458792916143541303766315100775122346482032883060728863671821874610296015442813658263297251028518792426443019898180714235736825437568094306982896959000320711944884211673528804603308944808358228390308952164307557017795438010614912223103467652682523837681388409111186114104577151987868421636922141484900422196159716139827582073081146143670646749240976487555540283531356429895798585564083155062139843264844764759040*y^21 - 55839573972063392342770655351347206519279038877920298586102648697596846045276766311927926556382223386105744988421439002129020406934324631605515505792805224978529467580115958249949181939552792073564971410547372848617478218682390852161539037524110313969303576765945441654201094731814399180209572561376953575501775603717087881711073733630311001462194934907803451540924381147959713672889630869884759172457960634735562906456165895065524697792294307122044270293038306780639521990724012783006984754633156228942886033640052586197971268351044676537785414675255889237/866300696696875852277777104715059159598927771194455783553208903209173594442225888101993073735781534957283056863099320234729706855099463268625783517166457416521506526040310048938592813153224291545468728749844118406177125463305318900411407516970577207959272285694294730175027237722793158783600128284777953684669411521841323577923343291356123580865723022807118175204245964889241387061073009535072555363644474445641830860795147368654768856593960168878463886455931032829232458457468258699696390595022216113412542571958319434225633262024855937305937905903616*y^20 - 6213784439183148770887246863456602037153151868597604238978513804144763546026978949506345162432940628208862416937348800763187560461813901809789896691669793627116241197694121775227888614594484750190027819597617643248866705703229275586369727740816367188691320771098425954429186818968626916866289164602927943000988641207038541756851585764182510613866349972181981804181112320553693653623787103013346818566282315663582477846295887771993190162133716317071112788859595097303282920324271409118650811074563076409152147865123303496547434926570379943810259039557011309/67679741929443425959201336305863996843666232124566858090094445563216687065798897507968208885607932418537738817429634393338258348054645567861389337278629485665742697346899222573327563527595647776989744433581571750482587926820728039094641212263326344371818147319866775794924002947093215529968760022248277631614797775143853404525261194637197154755134611156806107437831716006971983364146328869927543387784724566065768035999620888176153816921403138193629991129369611939783785816989707710913780515236110633860354888434243705798877598595691870102026398898720*y^19 + 1074736169173968917221570474235658966226138389306992738465863232728622999971855449760637780892621926917995780926583400551804728646596974368421287898793915308452244168244786092115261728193268046148531352768849488072672018040306163751638740326768536442591382919868353618560592489979723399554040578460969954090021624344268411267273718728713659457371277027464886165354299453877510909387746905460958221194392659298719669472092570893452754645452647138926679136139221425487741960078701540028812199438825049757708743973501232010266694422277662787077812156155092335959/4331503483484379261388885523575295797994638855972278917766044516045867972211129440509965368678907674786415284315496601173648534275497316343128917585832287082607532630201550244692964065766121457727343643749220592030885627316526594502057037584852886039796361428471473650875136188613965793918000641423889768423347057609206617889616716456780617904328615114035590876021229824446206935305365047675362776818222372228209154303975736843273844282969800844392319432279655164146162292287341293498481952975111080567062712859791597171128166310124279686529689529518080*y^18 + 433054698680920190632022284377778332787994759032677635911734977610057522414466042206451866463445002089336176238932339586978009328792515334055273735618624901404436336048370248990868462585446517703368016648599401077460223386956775829690204529532482406709597929389480046927690445197290811487543524922204129406544248039871853850875328215722116083448308313219748371555007911963440322561503540431135340733099565322967190724602018253150913032304530930635932580830511443507876676966181568592797071474725957160733402536889313169459532091057027725009462851474522919/120319541207899423927469042321535994388739968221452192160167903223496332561420262236387926907747435410733757897652683365934681507652703231753581044050896863405764795283376395685915668493503373825759545659700572000857934092125738736168251044023691278883232261901985379190976005239276827608833351150663604678426307155811294941378242123799461608453572642056544191000589717345727970425149029102093410467172843673005809841777103801202051230082494467899786650896657087892948952563537258152735609804864196682418408690549766588086893508614563324625824709153280*y^17 - 891851443714609497767808103625062652828529930563706938282624269195235511045597095182171747006656661318403256976966341463361921046535480963902071616829341293560140383309911368458673472722063671037417833069941894863551065747356461095807167155308105679898967710762898165411611902643511021110956670149467169679319476456533883650896781088761414008810844526846355996631766049099810217133695283087224650080107669634633947229302119514159585195520176815806585328243512463962598528565061779748640407594626443067158671013342474104782391196140925453204894279149702676841/2165751741742189630694442761787647898997319427986139458883022258022933986105564720254982684339453837393207642157748300586824267137748658171564458792916143541303766315100775122346482032883060728863671821874610296015442813658263297251028518792426443019898180714235736825437568094306982896959000320711944884211673528804603308944808358228390308952164307557017795438010614912223103467652682523837681388409111186114104577151987868421636922141484900422196159716139827582073081146143670646749240976487555540283531356429895798585564083155062139843264844764759040*y^16 + 10799754505521696434100158461426277854034255124747456459364471549714747461116122829449756651001502137778941835731930614505432663966332251135076395856469491004419978534483535443382180588087831757653010967218754148177020238299830010410276542477972054412696332185859931450869504599788339466570368097317121190532691509207088103280399739488036423629743774100421174691268156353311354550110107342176450989352820930260959977715054816009608910891197410814193225415815994484716730343274985987297699638632289461935968297453768072487203015338791239874729827571181187597/52503072527083384986531945740306615733268349769360956578982357770252945117710659884969277196107971815592912537157534559680588294248452319310653546494936813122515547032746063572035928069892381305785983560596613236738007603836685993964327728301247103512683168829957256374244075013502615683854553229380482041495115849808565065328687472203401429143377152897401101527530058478135841640065030880913488203857240875493444294593645295069985991308724858719906902209450365626014088391361712648466447914849831279600760155876261783892462621940900359836723509448704*y^15 + 913418861811036567693117516143011460428432535482373540734173282280503030833998359296463930423895473612338758551266000190413354738851666291806752725517578262513903488122461233350562881149667361801025251135170719752697182328204053250711616500895669870525219745288334995487595536051489411451998668543045375002457259898857933714655353113290914537028706474500500824181512135716001467198116402775358812103738916420166162318874679805517827188180573893907189550368330327960053251893125069001121835982713583441156747411296906912478332103467446937417573156872807707797/2887668988989586174259257015716863865329759237314852611844029677363911981474086293673310245785938449857610189543664400782432356183664877562085945057221524721738355086801033496461976043844080971818229095832813728020590418211017729668038025056568590693197574285647649100583424125742643862612000427615926512282231371739471078593077810971187078602885743409357060584014153216297471290203576698450241851212148248152139436202650491228849229521979867229594879621519770109430774861524894195665654635316740720378041808573194398114085444206749519791019793019678720*y^14 - 246379190800639043077793448851854923178065828851353537810059893689661632623450881876028039784954621122694166228342345650986250557939008564414687412401392982571195395845826103548971590742100009618296209882117155029503380707087915186639786083152594011524631683839473546894494800648173570560681296337375464165527310272102120551223079242424698274638739812562383065704445482411714474858413414369760122820631066607910610735120041817146187030463561748476292471917633719308380641111137989754068519536052411045677272344754727551042695487879862360170136890423959267637/866300696696875852277777104715059159598927771194455783553208903209173594442225888101993073735781534957283056863099320234729706855099463268625783517166457416521506526040310048938592813153224291545468728749844118406177125463305318900411407516970577207959272285694294730175027237722793158783600128284777953684669411521841323577923343291356123580865723022807118175204245964889241387061073009535072555363644474445641830860795147368654768856593960168878463886455931032829232458457468258699696390595022216113412542571958319434225633262024855937305937905903616*y^13 - 746902547855381979601290070011059962250340993157319286329157481687376133393966796158503712912787110633903015910744830722951377291876348455378223137047549056613411323406259850188697443747556443484261291911703772817116337912678618380373075359061940258939597025275306878323467826088927455384144733240749656118509276178453455294505981197568818392804098430474058273588385614832021275494495900689835034442802076088625149390758773444099577585216620017491533915538985536052249520329277559464704735489680461591357936692120131796362696177400163913334811033798129381337/8663006966968758522777771047150591595989277711944557835532089032091735944422258881019930737357815349572830568630993202347297068550994632686257835171664574165215065260403100489385928131532242915454687287498441184061771254633053189004114075169705772079592722856942947301750272377227931587836001282847779536846694115218413235779233432913561235808657230228071181752042459648892413870610730095350725553636444744456418308607951473686547688565939601688784638864559310328292324584574682586996963905950222161134125425719583194342256332620248559373059379059036160*y^12 + 1486291558425389304889781443531648212236859515128674586856344691508505407007046166917347780749891149844189582904115695898114458222774243710198296040071460560994859823019077617633321042169069668589136168433489996131515798029993044166903346347868242270426454092982956901217415957147686460949101441190058678649683785772143995152620567020418769120018418305364587632041713805525388911560625538376800682317799190374504882138146300478441087045600047255800435197571329360840054318829736922343211103914386776596642753249026283292011878251997429761693314202271172505799/8663006966968758522777771047150591595989277711944557835532089032091735944422258881019930737357815349572830568630993202347297068550994632686257835171664574165215065260403100489385928131532242915454687287498441184061771254633053189004114075169705772079592722856942947301750272377227931587836001282847779536846694115218413235779233432913561235808657230228071181752042459648892413870610730095350725553636444744456418308607951473686547688565939601688784638864559310328292324584574682586996963905950222161134125425719583194342256332620248559373059379059036160*y^11 - 269933442340042097463513003720484844045265604904220398129791733429490671953756341809849915671689142616948558912179691492462192423416446527010480372574121966479956852288831433977909170054069883750941722111070552250441673243911601485771619242740014067246330284633213221471949654917272028110513148176808618734446443896278762037518135297480635736279504030756763693272465361853201112519592172161543199270530360374587832695831614351391044614178168119781485405969974299716029207537954523871407747729831420298262535754457125348812857904702589003114318881430349119/10896864109394664808525498172516467416338714103074915516392564820241177288581457711974755644475239433424944111485526040688423985598735387026739415310269904610333415421890692439479154882430494233276336210689863124606001578154783885539766132288938078087538016172255279624843109908462807028724529915531798159555590082035739919219161550834668221142965069469271926732128880061499891661145572446982044721555276408121280891330756570674902752913131574451301432534036868337474622118961864889304357114402795171237893617257337351373907336629243470909508652904448*y^10 - 438997398834213864046539821699764650700095105678972410392636342853246376087992742397978676389006943699314223034568942282546742189529361194381626422415355632223258710583781897062262448438671048726792207007185860494997070246177209320674430780818905554317389048655974122485312583573951973673418663887261690803880077107604524248332149397142616431710718745029630322549482167111586664419814795137330810770650091769183449790894594786348028572448165842335969338461905383197022962163143509248187334507121969376665416458599387310659547072746629663544890611336024932513/8663006966968758522777771047150591595989277711944557835532089032091735944422258881019930737357815349572830568630993202347297068550994632686257835171664574165215065260403100489385928131532242915454687287498441184061771254633053189004114075169705772079592722856942947301750272377227931587836001282847779536846694115218413235779233432913561235808657230228071181752042459648892413870610730095350725553636444744456418308607951473686547688565939601688784638864559310328292324584574682586996963905950222161134125425719583194342256332620248559373059379059036160*y^9 + 12841428222552356152697336059079618010974408592913921692206870633015284982002564480782214766987653055389537688732124819381278723651327139564644851060759241132279049686636965911330473302487120093125707769789628039451115896607477974274413586347480128805685895170119920725611953391694940627556456365687394210802102455701094334480253319997393614226576068122932285785272893037764540767378814751133446090428843981409902375791979924150530892941233122424140606746701565902651029091623399323854567679413433604048278652706500727660501035180601259547974293304199648843/577533797797917234851851403143372773065951847462970522368805935472782396294817258734662049157187689971522037908732880156486471236732975512417189011444304944347671017360206699292395208768816194363645819166562745604118083642203545933607605011313718138639514857129529820116684825148528772522400085523185302456446274347894215718615562194237415720577148681871412116802830643259494258040715339690048370242429649630427887240530098245769845904395973445918975924303954021886154972304978839133130927063348144075608361714638879622817088841349903958203958603935744*y^8 + 13894155911577777162504951409173462475127749519951973970182199864725799184713862314242104207325770238921341972450770909635369117839316126916285737450868949960486000493471157761250290307471155683144769429868141831022622668167114395842468870836647805000864997558527787412427203294067723639139461827108215427569766163517837278333281630225325644380438798352644314470386918568470680841452997670589946440590925376473701667959054568586177818289296268824733668484157759625688583325114404407338726000438582139795933504288709675754200442153209504953505355637112489621/2165751741742189630694442761787647898997319427986139458883022258022933986105564720254982684339453837393207642157748300586824267137748658171564458792916143541303766315100775122346482032883060728863671821874610296015442813658263297251028518792426443019898180714235736825437568094306982896959000320711944884211673528804603308944808358228390308952164307557017795438010614912223103467652682523837681388409111186114104577151987868421636922141484900422196159716139827582073081146143670646749240976487555540283531356429895798585564083155062139843264844764759040*y^7 - 1207492102513169965061346973632174840414194052619681243846724527790385537426878804990727510738348940127023983073201588790392017072640875829652709993437538990763293392988812989163077302084062517262130393093470858423514688718072833360257248206458212095608231486593155497601991346172085974494596829434087711559041518176197938620628010633711294358417478826236909355301207966256558372326259895268664920224044422841162106161141541163764825476662944353327256387972901705624249887108240621683447134601327399252372164561817441532075310676654932910876742936502536351/216575174174218963069444276178764789899731942798613945888302225802293398610556472025498268433945383739320764215774830058682426713774865817156445879291614354130376631510077512234648203288306072886367182187461029601544281365826329725102851879242644301989818071423573682543756809430698289695900032071194488421167352880460330894480835822839030895216430755701779543801061491222310346765268252383768138840911118611410457715198786842163692214148490042219615971613982758207308114614367064674924097648755554028353135642989579858556408315506213984326484476475904*y^6 - 16466930831845387858985773653014535202454224360453928667242421335273110132712507447921236740053594293159750025172042853413066695899992219871999247534991015013381618559576706020565308634787238099252640827839207490149736525298883563055558749009403381948496549380343677844587445543468821289595571667576924076874558444695300088411769339837876762122473141499027379210450573158573695316535022081314018446761845231491809277502216580297130401223869144563740666698199310237400664389520914670984193999051628598318439863551430298845143489324023281705013114399010287/180479311811849135891203563482303991583109952332178288240251854835244498842130393354581890361621153116100636846479025048902022261479054847630371566076345295108647192925064593528873502740255060738639318489550858001286901138188608104252376566035536918324848392852978068786464007858915241413250026725995407017639460733716942412067363185699192412680358963084816286500884576018591955637723543653140115700759265509508714762665655701803076845123741701849679976344985631839423428845305887229103414707296295023627613035824649882130340262921844986938737063729920*y^5 + 8543933786703496639391935413675234254247188604757805683329121810285174957979099432605937771047011003317557279429108191085348159554757218898613166682283457268232182694103519342795923219956786236124061998976374491654812176571304927348810703614745532306973783671301702643925678423999550100678643808986182544423355578391768190202238646545022156454009800187362427217804803277306014154957267774810872090075773733795499999111154759775947171182904075736347033428249127216986035705313131562653668071527198459446654974465751826596338212106186547045275445048090129/13535948385888685191840267261172799368733246424913371618018889112643337413159779501593641777121586483707547763485926878667651669610929113572277867455725897133148539469379844514665512705519129555397948886716314350096517585364145607818928242452665268874363629463973355158984800589418643105993752004449655526322959555028770680905052238927439430951026922231361221487566343201394396672829265773985508677556944913213153607199924177635230763384280627638725998225873922387956757163397941542182756103047222126772070977686848741159775519719138374020405279779744*y^4 - 9198664080992514486302078202857668027580630984085200190303590643352316966468564237080107708430944268043178044848192498823468062492337639177566632798687295861481347813632042977627431225018294601640240101152495456223258333721831138878204427846258036000142286033373673174493433366988661120772820206741168942632975413708495670472743848199456008099656276451053061303171255139393448601916648318782324536781463275446348234230114280309315724730733882974841785599150990592618133271094856144009380120162177392443445187627876611431534530403947996302498714670333497/270718967717773703836805345223455987374664928498267432360377782252866748263195590031872835542431729674150955269718537573353033392218582271445557349114517942662970789387596890293310254110382591107958977734326287001930351707282912156378564849053305377487272589279467103179696011788372862119875040088993110526459191100575413618101044778548788619020538444627224429751326864027887933456585315479710173551138898264263072143998483552704615267685612552774519964517478447759135143267958830843655122060944442535441419553736974823195510394382767480408105595594880*y^3 - 128086660567170486576265576172277584334037397268739581483165324975946166963765812939527699168617813031262725012826291619488205648679055157231103889530839325723227893781194456445549503898339429430525997676959073093035918676532018158036741612114137831101050157599600084631913397495497932325927512032753150786648953360938918741804988140308527277653045427306481413778705835800388380146309216915712748808115746940880562918190292845403894339539013729814631591654112486970685916109675942801637612993432012760368261326840048804301862148787284072644582319811017/3759985662746856997733407572547999824648124006920381005005246975734260392544383194887122715867107356585429934301646355185458797114146975992299407626590526981430149852605512365184864640421980432054985801865642875026810440378929335505257845125740352465101008184437043099718000163727400862776042223458237646200822098619102966918070066368733175264174145064267005968768428667053999075785907159440419077099151364781431557555534493787564100940077952121868332840520533996654654767610539317272987806402006146325575271579680205877715422144205103894557022161040*y^2 + 34237571424540969739440207021474178570271733617811946654063218320158493655413940156408148064836370538448339104860933478104448068973681347758554469007658913249149946727329610024273267118871774843764510897096028318561650250654208514169299065715259669261490104799264301519689715478482412595082877016380572832465438120780529423671551172803381064053247106756952233740562616412520002340874596378835135768006412491721826763575017385272892228952934479890093862720150444181110719405524920633677648107019568776378284739526029628947236545050745013394246987671789/22559913976481141986400445435287998947888744041522286030031481854405562355266299169322736295202644139512579605809878131112752782684881855953796445759543161888580899115633074191109187842531882592329914811193857250160862642273576013031547070754442114790606049106622258598308000982364405176656253340749425877204932591714617801508420398212399051585044870385602035812610572002323994454715442956642514462594908188688589345333206962725384605640467712731209997043123203979927928605663235903637926838412036877953451629478081235266292532865230623367342132966240*y + 6002876457435100302347042035582307009717042892592042155004966533227907145436095700834307476795658644072368548102588224162478758459608064969835193703695730450183919217659208975778654484791626113737084607764077374481347171520028260072404258019926887474886507185441821856090385563317963974088904333867708157081701911115424166755537326470157201577939145142016026912242436226058171946820524659490120333710383714181106617517738901406018882001253420450766580878022625838343466117127060381341499168024925254118615600094665649571576128210902000566186893052927/8459967741180428244900167038232999605458279015570857261261805695402085883224862188496026110700991552317217352178704299167282293506830695982673667159828685708217837168362402821665945440949455972123718054197696468810323490852591004886830151532915793046477268414983346974365500368386651941246095002781034703951849721892981675565657649329649644344391826394600763429728964500871497920518291108740942923473090570758221004499952611022019227115175392274203748891171201492472973227123713463864222564404513829232544361054280463224859699824461483762753299862340