# Manifold: Census Knot K8_38

# Number of Tetrahedra: 8

# Number Field
x^34 + 10*x^33 - 197*x^32 - 182*x^31 + 9823*x^30 - 7840*x^29 - 186909*x^28 + 266383*x^27 + 1687191*x^26 - 3165970*x^25 - 7890143*x^24 + 18759985*x^23 + 19477928*x^22 - 63365253*x^21 - 21256163*x^20 + 131057331*x^19 - 12151984*x^18 - 164415851*x^17 + 65892025*x^16 + 117387325*x^15 - 79644608*x^14 - 43855170*x^13 + 45016044*x^12 + 10881008*x^11 - 12523750*x^10 - 5647499*x^9 + 1869557*x^8 + 2598101*x^7 - 414858*x^6 - 459613*x^5 + 78350*x^4 + 24286*x^3 - 3448*x^2 - 367*x + 9 

# Approximate Field Generator
1.84441746782787 - 0.553122012085166*I

# Shape Parameters
549866921235578141153194603072217262851955027015457943775270756839211892161280491806201086033150713057859020920990017100270993132972867158573/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^33 + 5689798396934445113180612933206001351143945464845589314280999038563924220998997782790421792067161648499329202754980817464144080968247214428581/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^32 - 17726611893786816624694425007172467128191447314021566410295742741692709331877764818808052792283246855902389411287118188133259821355887468987629/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^31 - 34296080467776263836535690349597902511208373576130716618995050659456083095287760608919401840081620666747186736639840129953377340766000776434926/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^30 + 5356313286646558025718699182700287314700045241415915042088181441622213015222566924803280140605923471561458879192529267422380105807859614057479311/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^29 - 2446154606636207084820176019320021980847617736967626559386790104815881317587914002498646909572975299379196100750332092903684516707531969083302411/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^28 - 51879211316884324398082765494182211522603785004456692381793875594089502182960073238231389146882260811705075612633705286124837132859251867859239349/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^27 + 110490498613611064802006195164566457248405814554307803452109641370649829564471509425372237121567672969417230776198279427930798632348546471943833357/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^26 + 484346527716413066936741219835402906156298885950254540084944015719904584208712104141796137494253968443008852229361436162577853214310880239578399441/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^25 - 351819655595905009818287771720945334643375112847260167512500820833083771068055164025937115567901309527960369204777566092731569637926243140446710003/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^24 - 4851199114503847260032234855081265250451166671684765495529232562334303635477121965049891746358197132928589738544213429088269213653457641142356561063/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^23 + 722308192382370835332807647365093552743237772703809962551334465025759017834510499531079244908043264107210624642885866924133490820365061957741351852/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^22 + 3459342996565212687755552235999296861011358001592075492992901055307284327219640933280620590167499760016128711656096764886154321338805564917523215372/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^21 - 30264839158104035036188362926321201181436601572395777235208296140213509492816025962479278104273456532776591818319666933104394561735463930336145315873/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^20 - 3752527983200000156873258370799770323835962241978163317924165541829547659492932190921566518719523427946427175740690723162651482045340117975486202865/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^19 + 21678237629320284361525185220253405167401931604864874235019885255393916623777569001541366606315807926230211794231862154288441754499781321990002067391/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^18 + 16359491137235168454220719000233986081061914968520184695780831735962783641236488728884326033578740683496708800285134726152641272664571940203146915251/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^17 - 14399742119401119131080071605240450523069700754066991758683911351747578025582254203739450634444487287479996661208197894545687885203243636851411110839/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^16 + 6052175039371432207113637789714019367910505051687164046196741462174651789147112035778109568703651302752439556351811294127597509220531110501751014083/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^15 + 34407385172817940798134611348424310736229112556845227374135914925335442484325647629095511342448101752036603272412890132327574900132854607661260275907/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^14 - 3392779740033345965048977185453692361867110600310102935275375482539752029188376147341869578310380213799532541881418338029207235472874854614815324205/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^13 - 911708752910214629276195918519939692959186466772204511733293083845266685500424079593652451689517059533706761189305228491104146001739678288097727396/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^12 + 1174998303093954950219588586716750999568573040003828046377976056655496641257282182065352790129021794911974487529627920233762612382907073684394296943/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^11 + 2895186587885761027731416321432578109589746650137593161631892210434304928386307851091642977386544694293357884529579230787473952033436912420148952749/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^10 - 1658851546219215706108910094193307403945064399290397755094650239012305342968185492611710073587212526318888573630290997637152008164515088137604804681/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^9 - 4474756802211447008475373200641726680427152487997559435289496976516733508057558732425124186229724832337756993414277636179913616144049003377189980977/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^8 - 206097158915296220347847183245166644794635348375878341197872168418034097213758465542491279956608472220297957386721530342321434163717974843896276117/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^7 + 459472151756961846173898249149094642482405256469507235707923498146410632357672184186792231043462498583777906281405887522018711595752687188326087305/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^6 + 3049001893490486695999923115817664190668050593481283091557560085731609844518301133309283784601773180905528534253847619518498887092278460725749835/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^5 - 50095903030832441556970288749816598170266054626462510805205230575558795287198780631065606357990276055331444862354037658748720055721753363009412727/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^4 - 13757318901004346266647448350803435746392337441784230296334853813489886236907148289650865572877554537548567947023261994401734300941102119647112237/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^3 + 2219775392490199093359453775706405299523786419799594065871646730463161633930235182870559670459186357553565504771857423243778253683121623953322723/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^2 + 272149167982911409401965516457249118833227788369327981422694656099681133983231863788159091715686471022836276607984196151000747687251717682318269/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y - 2718727043016014768213252571478348136869124342216280479567108063778520666951428443577755065355667747879139346321442768012462890153993010036655/397838098834067523950789073210845890430639665964861478568873389181897489570108747546986443865867461091442108205315071538140059488555309511252

-47643785123283278535936738000051216086890598149024100351530439337356173606779324335681773645752728102166795184266358457177853356530936958332/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^33 - 992792003215936815414458111870890330647533174969276551478569197962311660482686835941066629864061742146204306210504935877286224213804353330075/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^32 + 3060168813118428731945961073302716656984641147801641817989331773869647997658355952006775357806312398149413680505640869446884093731143258668438/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^31 + 12543652756496136160457372306503840987238906382701299229638036716865464482622377302905127285135027838456627073585857373506573431766219747780381/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^30 - 463261748160900586636879447866438771941405504313759580735092104502116975598586391712592300940636118003155555378436164394091494705355598240786870/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^29 + 357778918841047171909376422094463293508768230159154913286149311146813789985436028703674351174286187688382751661057273395945830616449136920054091/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^28 + 9005626643363511993463858595012537839993188448990446127125809131087569965356182151200116926881394722150292521187917519480419814956959414751899859/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^27 - 8934608773648782650625487782552314433045740563649461643954880424604491985203796961142748063163402206672886781158954504876206987726923732181606057/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^26 - 169238802433503285528713027284594289988529884617715111945468666484455370802252363035384327088852905696082456984238314108960617809953483543908015975/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^25 + 231988022246088932667037895036784854296479361064050416173131910353190966377857075388205456075809878240223906400981335935820388196178928427357654283/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^24 + 858068280548336984992488399424053712098480591884257038316365351936770419444472048157885460236294665876217801869249446858257549550194887016403619255/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^23 - 240493043931053997711962005149299202832128925093283655783231878562248485174108507710968330081728645403844004938811986081749182164926261761957483228/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^22 - 1252230376920367098563321236038163065915056817553166202263687546187934656930571081434484251230645903533828440014772465319477369460083278739294318961/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^21 + 2539103566983432618206320219472876320035329188589723884190345296973033365938954760088736414179006358243493223995767210496846592445825673773002828530/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^20 + 1423653450566026771060019159445548142950375967131351537728824285935853382800545188580243563627953058155866159948083506283552432896306743852694470663/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^19 - 3668570381411301048033207306160089434501151859634312996886359713197956352382452294405277082993923120319044558995443482704398910603558464717721929561/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^18 - 1809996952950477552824125109378285203017799230571755942530574754241022457043805011854391697022335551037627990761393986312519194790218951645709285451/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^17 + 4931957165925842891550479597543217654916271005690504944292197031078109465773894172992981532755471878345557376569752983111225076780949647909682289283/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^16 - 23751485756638779833488721672323777340317122473111590876439169116696422123564795158510184416485134015794805649306404554757616679071077661919703529/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^15 - 6013508218677879407970216768110806830142468448351554254188469297281833515096672330110705673889104028246735998142411887999410165810250984026446868078/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^14 + 456007700431885704945088384977074822146638103093899403946089129324934808826185023494368760692047591782879833105832520625528847940492151271050475951/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^13 + 330612007261970214289214664805130062054874020130862802437323552365844828738959625365896361404224609426888743531789039203449126675917811846757159619/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^12 - 347646661846606437568613363327335677908447738393778742623910598221231016433858426691588537925711153598654216001932573658345023032531941746777822518/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^11 - 1088822683231705586947748607237238576732639919621427205589389052720568933049070049789604818161712723578946038914886271958538556679354024455993272318/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^10 + 227693470773377283020851257387640274585235502137452915494193965581601628017143074559395024186285526446413378510918259230132196945684106124693378622/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^9 + 405999849976836049400177127570711188167416059911900307561322674010018176867468720523805836882235912434850659108230743463915598003993133454332952446/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^8 + 118369967558254539236267788090242843203867940980020759025954946532224092095378892418743687748111349934125566179772969279782994131015365465236630931/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^7 - 77959362304998490528521392693432646805196146422046556610994866853088751122171167855269625143211574473054581466784238172523061482761558232157482273/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^6 - 39144114069392005264014623053289569958032916455038379871400057731469422940190249689291367043972087275162335159750778946429342246822344156551483/1227895366771813345527126769169277439600739709768090983237263546857708301142310949219093962548973645343957124090478615858456973730108979973*y^5 + 32741971162560112486937699118163438135736038117381244447316579142087490616255765367395696647495832458178659621744268480211963886909606289374534873/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^4 + 6657945851311809494433504153001834156101933383889805988334930866462412208839456262286153854451607086822870759226282564943917833807441366291997703/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^3 - 1447865724855021854459608820248909207214901057392900062221306199221907730921551604630480510463706027688887533929600110222920161875225836037777321/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^2 - 250591073623606892408696892739111699571244534862957261785409171053043852120149954442441830995318882902007806323436776181128582434621103245504669/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y + 394059814883938067935174267222046347241846446789921539155342571292594366219454646344584724718744782002960108733535803788641538063515563294747/198919049417033761975394536605422945215319832982430739284436694590948744785054373773493221932933730545721054102657535769070029744277654755626

-9391205446742996087302585398771694392652976146221084962756031186927098035460924332703646842837433485721145976938295647349765833093370885774/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^33 - 97043287448073432098284110187260558057129285181277184468729489672793629706328482237405673371385285002022482674286060430459215140843155206798/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^32 + 605885441405456141436516948172851810524068261237619218429222794354492990248804907929846398240937778921776929181571059737172804548554700613770/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^31 + 2314653566052914404773731145550606636680770394562087492347756488661186020231242031062125570313677592527309685438031518747321170485999962122868/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^30 - 91467728466610504232827550219058752037941919184610332899499289074258067806052214704246397327215361213700578728717289488471428906302916656412855/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^29 + 43148098105281903205318643299539204916327309629549465241359747581739456173153839269246948777642302969804836052631909573066700393697384955922138/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^28 + 1769162201769640437712749039642187089365905716684686590860432517078114223872256620051928296219186592868475430975686729309511642862450729266153449/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^27 - 1911775908804857225925008326302184459608855797319480598072777136025197962822252795789052959771107597410163938398705908350843866958454882358401229/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^26 - 16471855732853175928167182226739421197592433564624143883797258997672087184953832177534433135953084412373965970954654216585611303768862226377619633/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^25 + 24233886873535614486993064669388370808118814919150513824194348290196950822754545067283988095039266063058619040285947507660765292917803642141505819/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^24 + 82078921256312490897733450838901915103935789450114283992112468324343185859086337785803207565044039170571544143361823967487886154609244638180363830/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^23 - 49572223669060261956305564437751045273378904417358059614408686821606545550082199623818705611997102682001569957319501528246427055885413581120337161/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^22 - 231982902645826375909451880153862902702970334497435306781238847230006434389003052120622690190244488806479305902823543028676512614831467070864765081/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^21 + 517100843597759646829945833362519312175831509215189485538480085636804311953600447125755815672916840440214399485724805283712092178070063371786925618/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^20 + 123463729751070871496842412452518582619430274426556516995922215336185674578425917730282874056810112806592505519326560551225794585230867739237492527/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^19 - 368338836869721454315798837616323204429627867900769188269093618320777620979824200670397228224538883190542140565873425375606519382628173071289481634/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^18 - 251131671541725317549901651823287728279243752771624415302850469424577467145241676039356920087465114237831708266996400618739188774876613692584455970/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^17 + 485101917678566281356360783962964453304125064433242589712002783942537809939234576243717494359472969047724905713462675797109822032336188055560368558/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^16 - 137231219991706149542863070323491937199275941067812021924065626999188201730057483059498315848961877081017152487654940144341710916943769221266039527/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^15 - 1141302274827191177223651533681123825491564777417555472768214457633414949783766447817520225219441654877743525606871705502161455655876138870368708683/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^14 + 123164418026706116635193301550337692265465936896145696605133267196161855136778817010709529124919867686678697112357608422438711728269800473966895125/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^13 + 58819315679980227253972810848199881282849791279726168036419456670223178392716465755477226588128719545692760282491076304840885217453979271343193870/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271*y^12 - 82113569544924661924230329021942851380170178547512398286163177835738762686191903253972061628491818801308761671181325395540451906749943814611648073/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^11 - 181444156347226381519869124271533053721563275912032832340983826071670004169126496443452440451165142873687530236264896437320986949257500086869242828/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^10 + 56769921819162950472248687165164118554355055018658034997794899632749923336272093574223896491012581746411752916451911548837082537422002116977625540/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^9 + 70936705958342913830266414962986361116898523476507269163983330162297110473358823920434113599480785301235024711389599354066506465977063380187748582/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^8 + 6016289582951293377436612916493508940995488220720290109836775578247990104524174593372884810389031360101290796545669228327953690494610340280406793/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^7 - 7369231378721570916974407794691457844537292829381166354330772392257906667113590228010878772412075764323322956567058358305479702720260444455760164/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^6 - 122978686572581722767857812281998577272012689106018074344230721537518908607170145186260582027625684334358294326946843453471369242671268080284825/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^5 + 3173256761228038541172895140603526362272260386797380828512400691112145855733043516697763926679725465669763536751931722489792752677469381325647010/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^4 + 293644388477355167226863809979022679705662570168585812140406411540981329378527147930642757591790394149801897371917043754888516986029331116719977/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^3 - 127488142842916916977604468367350069649173293163258353559695070406927503000493990962241745291601385827288586796053233233721806501605385669091806/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^2 - 10942733906738514092846201553959544136736126586264342761182707452920401458908890969018338909801202897416664793890628370315801387734981741637585/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y - 62396876001643785847035374108226342535968255715152331840273786307442629912054373822120539454635752326356453802901066316732203783076443691710/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271

8130367101041350697522702137317193979622243229948082425693688131243019671008546747429615488261109822751109184467776095038540798604588162263/88408466407570560877953127380187975651253259103302550793082975373754997682246388343774765303526102464764912934514460341808902108567846558056*y^33 + 250748927204347618240022443924149115415448032322291265128967906885517699559969869180313408982991859356907185226122812492693815641280262853515/265225399222711682633859382140563926953759777309907652379248926121264993046739165031324295910578307394294738803543381025426706325703539674168*y^32 - 87679496312772641231354801042847584914895983319360684228984056834227655983241606641827525058850133506194899454803624703625984350685801656947/4911581467087253382108507076677109758402958839072363932949054187430833204569243796876375850195894581375828496361914463433827894920435919892*y^31 - 160165219980320409198065463168478799151020804224001237756157296567523191120196367646221351638431946285878862132615836421408489611538810259649/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^30 + 237965873309542938310179406131689033889293415211459421946454632701652411443731029691846202561197968113715050796766514729689497612640716053840695/265225399222711682633859382140563926953759777309907652379248926121264993046739165031324295910578307394294738803543381025426706325703539674168*y^29 - 41507989781340278073162494673868695549158408116255056082157546689487566112976974119321980994657454972687703016112003180296003383828520153368359/88408466407570560877953127380187975651253259103302550793082975373754997682246388343774765303526102464764912934514460341808902108567846558056*y^28 - 2296627146776747754702863757015189544300319052234373241569851973381568749562870708634977415257833963064253853081609476872919266617589746351148299/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^27 + 5209205316313444536693514902144529729258946967677985212572021063609644322008824589850978620241899594549633524705572282816482615665081760669164957/265225399222711682633859382140563926953759777309907652379248926121264993046739165031324295910578307394294738803543381025426706325703539674168*y^26 + 5325241369908988910477742197136704384466959795240373491484939600772386628440784692442474748336389758092584944398633989565585665323705176546878649/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271*y^25 - 10877062440751414695194232364996415582256290136108833484513807657623899124452973525088992239785512592777695573733667993304759436228212793160679363/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^24 - 210646795498077239277217637248881058077575675530722437176074316603425285787112914865125806361676627943979551951119672601968389070242412236882664369/265225399222711682633859382140563926953759777309907652379248926121264993046739165031324295910578307394294738803543381025426706325703539674168*y^23 + 16597266710492128312668870714846861565185400606635780130177780838174372353551520790934739271236129391078498573696827084887907410314298200664952409/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^22 + 2714342274384277247763266393056189147958549939352410775123958917407839490597824376095720772375729511558592364574229239525064391967007920499620475/1227895366771813345527126769169277439600739709768090983237263546857708301142310949219093962548973645343957124090478615858456973730108979973*y^21 - 1380062450595025872522143723087454100918057368089136737306847057173959158890150330906493387892517776150160587131523750437393200465050339974205212577/265225399222711682633859382140563926953759777309907652379248926121264993046739165031324295910578307394294738803543381025426706325703539674168*y^20 - 226053865750153993752868718408155435022311948571240404439922274639209563526156920371066130634635561519676437262504548357148852024149856872588224061/66306349805677920658464845535140981738439944327476913094812231530316248261684791257831073977644576848573684700885845256356676581425884918542*y^19 + 2939334737310008235526919607019947911915816040654794864739071039858957056992995032242996670414253019722883288564297943663618772918327992703807453059/265225399222711682633859382140563926953759777309907652379248926121264993046739165031324295910578307394294738803543381025426706325703539674168*y^18 + 526394644642056198948843392979090080214632600748776897417233874228568186810362986176752298167809863762882574285321320363365814470946632694857593075/265225399222711682633859382140563926953759777309907652379248926121264993046739165031324295910578307394294738803543381025426706325703539674168*y^17 - 321230910359629975717925018794783589336999887670778816321076954953608073628864717657408860137700081239729160707824147180679861797441916882580243707/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^16 + 175245183337565210802929144737523965156444957478558208323053358883412636821770268361590718722834070623619323355639293978634245082588205299886590051/88408466407570560877953127380187975651253259103302550793082975373754997682246388343774765303526102464764912934514460341808902108567846558056*y^15 + 1500245919115534421306492785390320286981292065497989844503451435820781810260959652913460109717541389847979131059526754756247762528437784065124051343/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^14 - 182900907072937863254307540624725079258100587455760382311195192316264396944220242344451441573724677037931580859329391713338219416407340579924937725/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^13 - 19027050738460437880387282574111189317146656149052136393265617589589525025154675907367159173272595350806807080529763931037708490426547623088111222/3683686100315440036581380307507832318802219129304272949711790640573124903426932847657281887646920936031871372271435847575370921190326939919*y^12 + 19694285581479823672350160469488454494561282748605797826177463521241019949372928368034275551766708619333662396398647203141819653699967243600821247/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^11 + 6407071102973464820679627849439014221643010734154303247040428350410527328606802720872671212986525785863269098725765230718961950537024874118029381/3683686100315440036581380307507832318802219129304272949711790640573124903426932847657281887646920936031871372271435847575370921190326939919*y^10 - 86643487413972269024717901021315260796233911396839890290144791127747134989053708232219146376522549216017687889737544457884802025238862951112131581/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^9 - 61872701302723689105685841391597427153232912993062970043768735294095359043259549870327362817878050502886559180429680770760220050991550387011318495/88408466407570560877953127380187975651253259103302550793082975373754997682246388343774765303526102464764912934514460341808902108567846558056*y^8 - 906172636573670611829487880905617655277506774753217168962650604589693364021392706000957009892529010158821225896127604675649113703807201412011738/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271*y^7 + 2258423449310666865158867594135127912383776501130920059726124466816658181503098101441208779037559627235335326363047565113936885160058531559764991/9823162934174506764217014153354219516805917678144727865898108374861666409138487593752751700391789162751656992723828926867655789840871839784*y^6 + 2362616398270167546615598455988906448736657181409280899363234494470042397342450125397753682203817022811084190407253238022048796108074727049800401/88408466407570560877953127380187975651253259103302550793082975373754997682246388343774765303526102464764912934514460341808902108567846558056*y^5 - 1507899746535762991123537916131810750701690031121705637856496105967577925692572513874705711654337805087312901085952791458003652399006575069756661/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^4 - 161244747089140446133299262157352560437395303035701468370603289651928907593214659735253915807174670591901497256805404527588754236428261477203711/66306349805677920658464845535140981738439944327476913094812231530316248261684791257831073977644576848573684700885845256356676581425884918542*y^3 + 63455593179710993749542015269998991123523492114137753586167053063170166698875283589568149600154962422496443640191186449728335584272355300528297/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^2 + 13570108684432962558430950869403532948117897762809220380102542347427069004947558975590982747949290345905991293115747628126444328876959972060955/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y - 65904362342510903570603242567366490689119128286316887275345819817092004386142225211305321861994800441885740995098788777317323444368717296553/29469488802523520292651042460062658550417753034434183597694325124584999227415462781258255101175367488254970978171486780602967369522615519352

1267488182953643443296070836976916019244176438807776163615929141047748616023099418864935296099411791080478039267422827536810094035418016903/14734744401261760146325521230031329275208876517217091798847162562292499613707731390629127550587683744127485489085743390301483684761307759676*y^33 + 4337831633794982963909474374825272092329351035748550611630575126630494135129932774801286401593657234499911887119143675407485810855901205747/4911581467087253382108507076677109758402958839072363932949054187430833204569243796876375850195894581375828496361914463433827894920435919892*y^32 - 369325762897225638675634712626390964460932600949402536463240348505416089745134777588847365058382812373496205538390357623734248767005893604693/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^31 - 222336195713206544289068213380548607658665148319002625343580868339882643800798007999627284460700388279741103223139335408708898244009427309509/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^30 + 37113129926574070235336995582271623542909378964699009894384610104688471708697987356976318982296517775090594699891474806487423076225388677935039/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^29 - 19896156070812054928307930317982897556417560949224543640270436019226349367519909054103044929747061576807784834575681166356106510856919889857789/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^28 - 357993592406005402358350907516918104202905478105000346211941729559880825206777228221147322949507526002841685087644643822373022446668720334488075/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^27 + 273849194610877824822791771906223511860893413430600350980624642524594719929337058465139809360205167175331710272196697162782373089932881865915959/14734744401261760146325521230031329275208876517217091798847162562292499613707731390629127550587683744127485489085743390301483684761307759676*y^26 + 1658547251506460642464778980710800016452561200190844328554721592262635373719217925809058598305901320135060094598788076641826805360069275374618545/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^25 - 1710664514124122938388972635741608389435030842066533705486709115792089243405470162392686663350360873882380981839217342292480746232598431891843149/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^24 - 3637536276677556000146439469461913933698597233669700743523362998884611429149282309307168536397556832533301874573986136288668023199484085065020641/4911581467087253382108507076677109758402958839072363932949054187430833204569243796876375850195894581375828496361914463433827894920435919892*y^23 + 15641268097110888772681468115593822868261627514408440212307294148724196690524716189763811921637998146800440191998992596902029013971230489128827948/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^22 + 22689322940775690568949513070769388897934928532011201998143826631904443313490377246227277649401582489006033814129631681804259317191373685761108013/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^21 - 216569183174955262709189026391531260951460780518615547202463969174665891342166017405236802657822637245221623933085465321794663591398238216477662421/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^20 - 11556303581709518775744691099508187406450692008416798739827935300664612371897158006091231217738948007205577135338944408028656183879466932074340720/3683686100315440036581380307507832318802219129304272949711790640573124903426932847657281887646920936031871372271435847575370921190326939919*y^19 + 460878409965532113657846449026151359727427843180919259928040929643986065049669130612505143835070653505933451428896324109627716959790649611358102815/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^18 + 77089690411824181345428217222895251952566303256205020320655727674075778193339781612271121384980184033680293299980362046349149845869115028236307727/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^17 - 50314674821555068158008259587268754737252072054482150012569508717252120902073309257506389858468838003613248942321508367890964227833922229737095121/3683686100315440036581380307507832318802219129304272949711790640573124903426932847657281887646920936031871372271435847575370921190326939919*y^16 + 9848958348162461461727058062998941124228594302920289296003996024770609951756538556864014338884862789149143976164401514555465567956115911114977969/4911581467087253382108507076677109758402958839072363932949054187430833204569243796876375850195894581375828496361914463433827894920435919892*y^15 + 78182659488456062862577755464355062757340597701622432607839358742751670221052022103454936710373516754920726252487923625811065131237762090444184931/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^14 - 88256123201115819433632511057875828959620141142914329142901962575207277099588139302332322664880057264804040862118099058691074027939529488656371777/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^13 - 53336093304086127637053667635518784119925413288209324342843362288261588211305875196504288599658189082910063496887437504026379056984155235954745501/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^12 + 28315749426393377725951730490049029406200329748963067687934629106239702783172700290724442197430848328244741412530337615468753159223296564386996276/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^11 + 17881077668411533595800516029131833427093808246778049550400057923081267700840856717211781006466861258613171700690962048738005020925078520553418084/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^10 - 14023767760457779983502157141969687190892840380486091768735431545177339966007328679043910204670166999016656145681504853501097309922398157041769271/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^9 - 9662031030074361135797660230870191307414761374836442214906693367568898137269036284358883002751359683102101487470476000772249331431527051718242187/14734744401261760146325521230031329275208876517217091798847162562292499613707731390629127550587683744127485489085743390301483684761307759676*y^8 - 65653693603591762495183211349326544932576854575038160096033763828488628748231997595503605819544204068699202877013556859878528258565122126337444/3683686100315440036581380307507832318802219129304272949711790640573124903426932847657281887646920936031871372271435847575370921190326939919*y^7 + 9646996056627828691757156501391277923717422845986322561665929625054150454120584760497573673179698347018154663161135131648440341048851166875517165/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^6 + 1041949441826906149131458595274338609852709762705681612616614588309905308819348684951784387980706552279921077787498666539108649618664450056742591/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^5 - 722987995575099764119285076027491666157617699018110540595375614239763556888632586048436878168441318684443114065974803848309545424974416019283395/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^4 - 24272807254799166881721720487346495145478745841988096647761456346579862984185521058838582099238978947530206639714319631209251244388832206422422/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^3 + 30806997364129638464706673293232242550035966414654972186687781290184744982719276407640158906993235199051158631513285443874488225683870406794397/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^2 + 2133398536764881863987327814403908120208301908690367363930897103435544525619649969586081305102125112155051426635949329512539079756632155283033/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y - 2625955010174034227317497214503983734471715554572910004935219089501350162614746413467263398844912787060754679149849246177645941777813157409/4911581467087253382108507076677109758402958839072363932949054187430833204569243796876375850195894581375828496361914463433827894920435919892

9372704196203894517033927149496710710328954105333246219416456933785447726904554325433130927459589559148094084441143345268885523113948194661/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^33 + 290053925105874852416871651642335159848065390403738966035188482401430283342175275524730646078143837729355326266418799884567573131450189293889/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^32 - 907997506398755332368310338002706214575934836742454147878634058673664561236176425149082835290838264211021573435965550297008697445686051877885/22102116601892640219488281845046993912813314775825637698270743843438749420561597085943691325881525616191228233628615085452225527141961639514*y^31 - 569934530709663451174037869574917966972777053237493325757867701846271210180608836309718014977246242551860161380696728002294686846081361413186/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^30 + 274092899127308748968955990559154458633862456694649013816481920438271629699090359712124184801580213366605429010599321729777927832406376268483161/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^29 - 44628056822489239969687390264186544620345994238320212789312968633609130225296886573931459233307329475063632279690465261387988292016227185853613/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^28 - 2650073843966160758844863612953050444175838519389904635291691348250089051374062803281876184230868866405772749297627531807990549439918660839530187/66306349805677920658464845535140981738439944327476913094812231530316248261684791257831073977644576848573684700885845256356676581425884918542*y^27 + 5818311711619082373981534100422877733513162690132106033428469079624178244563209535512631023237309043090527458022298109922158792771599271356094191/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^26 + 12330755981200813372493732429718365157989361865437310553878458693448285128964020597358724439200308448346455860580814324935191950722787684393741790/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271*y^25 - 4083163136549632362254483863776131797544720090203025750538747271003273645803402976458790949712704546818248046563756274536902185991692596194306581/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^24 - 245489324367773562535596186283980332763232079837179090847653112478200261300904611789037642977478225030492478449042110734700954807799067518375062051/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^23 + 4171951395659552972646942129016239800016838927368104739164274968076601109676789778417145877240224446832544571636868647581552612538256389662353929/1227895366771813345527126769169277439600739709768090983237263546857708301142310949219093962548973645343957124090478615858456973730108979973*y^22 + 57678955209429848342558700650061735748852840696155267406046358048435710270187479308582189291831788558361528822542574040257743708896485641548778922/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^21 - 1566734306509876417598362053168273540050818158499599025815346033693082658844388453344326197649849907916630624804533129409244321666454630239598107583/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^20 - 274750521555490660408624695808763887078179836833310074425713397873716443881822908267589762695487136494681261811511654747233492932437466863353895792/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271*y^19 + 3350570802893669607939545585132777959828035611741505225301009405003219006585169683053139489328329461505556085535582304347091880604759684959645170161/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^18 + 728275638021458066866461881873249490199387556984644542241943764729706677582698739966297019188581788869711973646428986088146724255086278865705048657/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^17 - 122786864362758370666796247809541657397340379662833937705810964457079136456147961115505441170484458081168112172273630376593709621685063673026887764/3683686100315440036581380307507832318802219129304272949711790640573124903426932847657281887646920936031871372271435847575370921190326939919*y^16 + 16481576571155312270370024239358544930111655068725148435931930662651333905039138642477650551178028803964749660952752750951265013351067023945135049/4911581467087253382108507076677109758402958839072363932949054187430833204569243796876375850195894581375828496361914463433827894920435919892*y^15 + 1739184589798603261486007508430457900661593744823076285990591068419816070696332960043584647506526885709282723250778567446003446233115097009408711947/66306349805677920658464845535140981738439944327476913094812231530316248261684791257831073977644576848573684700885845256356676581425884918542*y^14 - 63180216026808810288956073998383110071042882713514548887666285997186597772856656479552422390702287044783380642920969771937394217329462652497663663/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^13 - 15031274987677238480150449791037514913372750357000864535666195960618729861812743707547372166308303738008960096809889476624988875068435305236728187/1227895366771813345527126769169277439600739709768090983237263546857708301142310949219093962548973645343957124090478615858456973730108979973*y^12 + 21027189765327196441541014090951171098718331656874066786149283368727046044608365866326275763365006151104155616063531163821866292908263648842341159/3683686100315440036581380307507832318802219129304272949711790640573124903426932847657281887646920936031871372271435847575370921190326939919*y^11 + 46775029226506581408377825008702970817552385853691388086232185623456724246748537465606128496412274357581603344240983093173340405721745301588373057/11051058300946320109744140922523496956406657387912818849135371921719374710280798542971845662940762808095614116814307542726112763570980819757*y^10 - 89394771660408242424013180175608754933043743653449647883268732956890504570577505525271449458582027255433870769875499888115642357399736571396047193/66306349805677920658464845535140981738439944327476913094812231530316248261684791257831073977644576848573684700885845256356676581425884918542*y^9 - 73854914663043536254566782600707673309976072495774878549720869318819250031509421681033746199101212603912104048213901749323376316324128902413559681/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^8 - 4179822985785927989126922503890883753479917817847925199757623790774000842662372655142373045623348308116056473757947404238648498906396024824960199/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271*y^7 + 23341535057237098414909761173161607335874152470236850970941275561761784331872924101301545346041733542809229888071102309964824052672660547043843121/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^6 + 3649262397849895735362593796804944900864992618439812673924291392047965766551119990474601811269863394885778805501954909565971286510746970421379543/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028*y^5 - 558215394401738102000618276155370742592148668955888613295883530181278042951054477664787014118482134726495337364074182650714890260876074194461909/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^4 - 294121451919784497420218811338410061992372677554559527918791252549598038413801207847240082555412837260953034884722378917352355247121827200290100/33153174902838960329232422767570490869219972163738456547406115765158124130842395628915536988822288424286842350442922628178338290712942459271*y^3 + 21518322200587974990869199788380162459989935420637167028148397978577150439324657726350178125636674774822342778190826653973435308375387916488277/7367372200630880073162760615015664637604438258608545899423581281146249806853865695314563775293841872063742744542871695150741842380653879838*y^2 + 25481401054756937649228578477717997605896657778280537951518007011135921692928366772908773376856043731120385544943228566858991923134606763822437/66306349805677920658464845535140981738439944327476913094812231530316248261684791257831073977644576848573684700885845256356676581425884918542*y + 852160293388761117262349114385536169600124220301170307275896472664856181588988904786342950035759511444139237478877334922875593349286098457719/44204233203785280438976563690093987825626629551651275396541487686877498841123194171887382651763051232382456467257230170904451054283923279028

383244132962701982323273552885818556722389799926365517976198317775197197423699342610380314502277275717495095002827487906670706384456613539025/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^33 + 3942118600467002778501275234940557118872412260092394015102219544374934236494092086576724920518598908358244062426963747366285448289733210213395/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^32 - 12394875678037578485817296855446286075019528388616996847813838571007566498131982866266212649297160077434531363112103508670220475825731896276617/795676197668135047901578146421691780861279331929722957137746778363794979140217495093972887731734922182884216410630143076280118977110619022504*y^31 - 11377053099031687816847793848095783972086605373694957201385191656773569038336985797734886644378693395530074559404302095711934348976827873912751/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^30 + 3738232022849600484565898216285650344196748355279275799484103887593967430252205126122683244647904496525357923786770978102882259526355768760991487/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^29 - 1935184495103719662553144593421496085645232847628193974689083495842553425313287963532974970010984546421717452747623100475910381993810828364083045/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^28 - 36084581421378250856632653259315828998158176347108375590935683994909693622940961959733073248433889447657665022557686592957937935062922277560004131/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^27 + 81425938819287871655434767040324198471972495074105496835731415760433664755288727883744221620767512626356552511847626808482782628525934749207113901/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^26 + 83699168890779766810780146966402649425704236650242191853218928999786130063172325359404106203218328871740606790355249870469138868944432778876824419/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^25 - 510660985878162709861769282476430746402885585480175107711210529440467097179783654363339135905847736444846712789599286667085075980007860429550632263/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^24 - 3313241592961470358536546011544423136507022166450766063297288449644004382185724455139579657974609450172872214255408705583677250513042008099102866185/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^23 + 259860904757545879396081815527447091062256903559624354468349925684992749489957480063652710802259200576949671591267330529173892179695038596823962917/198919049417033761975394536605422945215319832982430739284436694590948744785054373773493221932933730545721054102657535769070029744277654755626*y^22 + 1154452904203456885410182661047781182538234899337339983723066273893978549112712260468981717566949152499726194034752779768058857418915260398277621317/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^21 - 21612354242142193767863254944699782109130944176361084020836749473592716671369710470747560516764098135486599437793939654126967674730791778265789701525/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^20 - 297793913750602956984351774354126841975609240216567052246207389853664745366678281880810601650512074302839056696882387806144068503412163099903525544/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^19 + 15345717681748528153791424944705666570285454471284969640339142002374501041965949865066917332868129599264623622675952351881767158257828726863482529101/1591352395336270095803156292843383561722558663859445914275493556727589958280434990187945775463469844365768432821260286152560237954221238045008*y^18 + 8466451717959945403527349868791873749377430006980027785327269068368795745378532970541839370741312878191075105770719212290450763484909206753455616103/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^17 - 2515854071095668654511473180913139568402564746300974776410129436995217457224525992535544406559061569592947274427840136827252277381083626632604196321/198919049417033761975394536605422945215319832982430739284436694590948744785054373773493221932933730545721054102657535769070029744277654755626*y^16 + 7985740608431264817258964131777630199523948676393487904035205536840773463236665153915139398706027752935609465371077016382117358282608764397552755233/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^15 + 23503490049090657765867888534195438033942615252125333005817525530438677046244530538319378833843285345805519230281969593944646901676492152649003946893/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^14 - 2833921557769086293377235279986621355619095444994100497498123210459191314857109859448181225075165020616757515445534488497439968979654404167319024655/795676197668135047901578146421691780861279331929722957137746778363794979140217495093972887731734922182884216410630143076280118977110619022504*y^13 - 596544279272639737687291008348388497200903057776939279806185883149168717808714407365272866346820637848866861778887708744305387226594688889928374789/132612699611355841316929691070281963476879888654953826189624463060632496523369582515662147955289153697147369401771690512713353162851769837084*y^12 + 917203104646842280883914268357131668523995070387604355335800758228069425083994021422399922538128528428874646557075488779281773761547210382220828211/397838098834067523950789073210845890430639665964861478568873389181897489570108747546986443865867461091442108205315071538140059488555309511252*y^11 + 1809747102055363573874235179688165109442946554373250303004583518464327653779799059630138061635061874522834777521739960686297238971594039766838778637/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^10 - 1334355330489773818873074275900432918122999911948949650031707300791689772912763984049933192874356816185078118427878384481083348982591165191902334181/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^9 - 2904905630756158339151005814915123104168904893163296750854831447651851225162297403177806934077599223150360718892217985832258028547314477703535211873/4774057186008810287409468878530150685167675991578337742826480670182769874841304970563837326390409533097305298463780858457680713862663714135024*y^8 - 16199608343039682565218569575345445312595963245514665331116730651268739756769530867166638768803986384594443070381109698536629220296428666701503253/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^7 + 316128383188068707901757133128434278509003481775325437050378645673839357432284733983565041289089101499237550489574535020828038061378808624160969015/1591352395336270095803156292843383561722558663859445914275493556727589958280434990187945775463469844365768432821260286152560237954221238045008*y^6 + 4188624704041360212552605345895054492071929967935426232405887488844265116709748456047776122340579377281826704398426224764560705416459326655505937/176816932815141121755906254760375951302506518206605101586165950747509995364492776687549530607052204929529825869028920683617804217135693116112*y^5 - 69960269344366040301428002945457374975547820616709241957310255703164551219892752178231448006194652606433327932773657651264001169498882121790735713/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^4 - 2526920992905553012623500726596440894399511096143010861939729093818122458043018035320879026151341030672407937872950674368723153625766248798550397/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^3 + 2922235528540687003258749471381921170726930522626092588041933776310867399271592172565840628415059188740578390870487668658965011304870578473985323/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^2 + 209970732833392716240976733250184899215267719458540403329353618938772814883453501484427845209447854675084487546590632472891385538958666000622261/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y - 724827900483923362584783785567519516127637750785502533946534844503827850682785088221858201505214537348854292195785072653807389375667437152585/530450798445423365267718764281127853907519554619815304758497852242529986093478330062648591821156614788589477607086762050853412651407079348336

-279911733853517664106745476459853032785589094720774378284153131876194729813767323987882607705738672052535698008544576811562915553915518243759/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^33 - 2913740862968365297999184811664708576392925841828438027262863572396048739538339932924017797233424747220916825049178544495331029822999673198779/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^32 + 8993335346079885037237759517119198571562788701687319394797371183876333543907244947239838542301051695584224983475739064758256004548205965145641/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^31 + 18287597785839666571921616465583132900868649043535524746766508598079790409052159073788772373108039924237516928700102553513472080841669349430753/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^30 - 2721658375527522482874385936759223591803379630781682903387539915389553793387745712385132748232184350640205587952195168418435574237709584484437277/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^29 + 1077260504785412244194863934352199044410878489744893195026326423171753120011488276161888878170935484284102728356126296135275006051047917885909205/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^28 + 26431027994949692200647736145820590978007447045481650603186358554071444920339055066665753373358535574963910917056936707669313889184504970580799355/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^27 - 52959124455194920124667654596273203090447235371044000411078655332115639541137047032866155667386396199503134004538573224588562444251536550606821159/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^26 - 247974700134801198658862865361528936090885892131090201259556772939746961650580307357608433106508083113739522225698458347600833789453391951125899939/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^25 + 171283967795733020038444718182360861006575937474492623492136104338820001786108310069014087461436812702430525033360186193337690648107307667682451260/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^24 + 2507844711760687904239071807527180221128793867880674612267298360032235340289844763082183644021461682282938062141765479784925183601434150285254120957/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^23 - 354200794061854765860164576045370533593329808664001904701892532520558081269363226638478198905678709989308334774134800940418818903925001699952341367/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^22 - 1821823169785587894719482717390258160102259124155976202642846752704293008042167298426156661633647295493585099930255155348085390722185144714090336322/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^21 + 14915152845658980248780468770657131494236908449409539234267766341200070327006907907679018264496640603814236961148817448971145869326166987228185124327/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^20 + 2055327801704350942956439168981886946097830594370985367475097725726635010662442526493350077140150024941463542252649020609015689077875577445351388573/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^19 - 10735180229896909178362413866220982366596942366330612305297549522880436930484828344218666014855890631941473577424050740190755912512070122830522946245/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^18 - 10248259421500684389671763377672966670631356588202146931214213445898677633499533927579658617438947098715145117230513651130242929410669767491937543909/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^17 + 7176684352432866951160576508886213366954285090725808174796027986879311526005865464252109903119234199014657831570766356723850355070692430320428916423/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^16 - 435364443050566707276689270748566996018593742700653012658741860294345774587062024196895272908402710003358112061936154464576859741358098279853031149/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^15 - 17346096806733367388356252524071001266649010974297371584094102073753014531822284774334995279427008012638371850224559710981616846213898971992665014607/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^14 + 1353945232032867654294683426886917597206801467837685092427583391453143699271434913505234466161567342763658204345042516365056035659884724151327621137/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^13 + 470637164543712851091820087499604960734663175968720704552265582857473382528656995024457799155216378738174839698425091975025791163363462411209992490/99459524708516880987697268302711472607659916491215369642218347295474372392527186886746610966466865272860527051328767884535014872138827377813*y^12 - 499353210817494715601862754142226081522699520106892083087130496797036405390111619459949795818124861693114975095911511892719588631192907578788689692/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^11 - 1539711754457021410774987883517233447261791008131770037183723344876815383667786395029703002951974787402212764887712688170603735481571715144314410902/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^10 + 613677280523224687635593053516541243068481032755601489500707783613740953359867450926855686785361045209006352264357056935865565700636310809341783855/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^9 + 2323769988757786978089196901910282228724439271365833277082302932459027425047878027657119216223048565546577714616043153502388410544251903362588541763/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^8 + 186539860047340608880669124867843486384908374071999866484040918218140834477469130816607586836376855702182223113810768426234558375659505541471933389/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^7 - 221769566338528789581265235611621070076775196790872303511969581933354233889374932803036414612606561729501398203766145353063897071334697365265572903/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^6 - 690851097979110731227962691881430236501438780832752031190225942100859849954163273844114381070065258553412078955575777685747234859265164832431679/14734744401261760146325521230031329275208876517217091798847162562292499613707731390629127550587683744127485489085743390301483684761307759676*y^5 + 21673752397799336373306132203795399541885564351229863028976979996060263773709290050225124240145049925225681130249026104294334755698357897969196712/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^4 + 9846994947287740949857224853322183580534481548888200845855844497328997459601854275772974858892081463274029353206313137630787482008957263989257813/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^3 - 636222445633577416639114309641775650209332916271468818861807512678255244852938618860027145760443932271452512553824971534936798505582690429380343/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^2 - 208589126901461140825095599668276245216403459260329135109507968822352420961862012267290113256372807397509692738114606466592540926442667028621012/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y - 8045905305546976924106788022045108102691895334801914410780615433909542475607865725169542564606179733705462215809747566419348083781759095171203/397838098834067523950789073210845890430639665964861478568873389181897489570108747546986443865867461091442108205315071538140059488555309511252


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

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

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

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

# f' Combinatorial flattening
{1, 0, 0, 0, 0, 0, 0, 0}

# 1 Loop Invariant
-152013513533653545019355948210556438115879950117776432767054045905080713003892707302651831820809174239167243917152548407345182799544616828268973/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^33 - 1560342244752726164933007571385783655068344281913148858094099178942868764523874167624383082808635859293142748960689462268571629009039122177955475/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^32 + 4922001536208462766847448283939553913917654888531278758693050210906979103321013327391293643583411455408052945028584545863074925508059129494610029/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^31 + 8864493961348235292888750726040416262247069751878503056813994078413711785126419871707665220954369835706019409122738555684408898841306541291014563/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^30 - 1483468111267693759586721384015838321623779494099819126932290298564735491948452251950033151457965140472205697104553872196699326170486748711583633027/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^29 + 799793538612685881999391288923764924429215205817567087358742310799588235421990081760474140088576070585599204283463359141130814755076563829565798645/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^28 + 14302578419602073129389526290876236838549666704719989206754677492797526961713880771601643764181754454431266875443581253324613955959807134023935165629/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^27 - 32913902522551009838650342826894115659937786319977212069817551075244320942607738230463527559133261334521587346044014851861916525191109827682971302209/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^26 - 33102193585861586253870605039020674984919048697999015291051455344610205454935869150866606656987435252604381608964968241643165309128485001950881045717/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^25 + 205367288402146093878607087108541095400539003824724841794026721752548360184628077736320015323401545505656619559291610457570402328273012924134105464433/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^24 + 1304745881035453330263451105898404579539163091120603774264806810608533204134523444863113985693105285774324761379084160964032383463229936169998851376037/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^23 - 104198541013200244624817481579954155873831744112229244615703800432375736296774158855339622657194637261587046629807033606548013371657749270069382022034/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^22 - 450843764834126897823774989614675203967168114167408304100037564952834712155586948832042944580227508174751903587238313626244076876343140705352633648210/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^21 + 8643291848030581336679333920183083478295180452971924335129690984312852864379012176186174989265042678481361960996691066739860831025120129873331826109265/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^20 + 456482365171973012163173358448787532980633570573906167760441250787325352816212995832874928636042956369088670865272372250160342286898374101332603222283/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^19 - 6118312211118939598882211094658879536152845598006498942185598492739272544013044281118524893401719475192998320278358070412994913145634314172019403449797/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^18 - 2959964392439692623171684901243817801772180621306974227964568747034152658749326841861055683847009876353798289580828521687611480917356583818978970020151/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^17 + 998548355056911544548818081848228692265833812689324535694704604344518297746793562283295106019786001685718676918504573883681055968903165833016480775349/298378574125550642963091804908134417822979749473646108926655041886423117177581560660239832899400595818581581153986303653605044616416482133439*y^16 - 3668717981172799737724548651294882626243789587272708711006934407489116239431752515107082356868340154340161621957509446938521667783955793568733196183041/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^15 - 9253764812340085657341932222368330790728000213527064568344403781565535564127986152923941737407572290332869500824197972172500965277780777326545225796525/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^14 + 1184251192405430657215900606639509239215715407554954020498207231388724909215668467490779501686628791599950909668803932871978300063038948523214847535885/1193514296502202571852367219632537671291918997894584435706620167545692468710326242640959331597602383274326324615945214614420178465665928533756*y^13 + 231306901759585856379888995495966501498198443777855425953100342046679491573940306233160524014301268439555314889823502199645803013085020700390454438911/198919049417033761975394536605422945215319832982430739284436694590948744785054373773493221932933730545721054102657535769070029744277654755626*y^12 - 375544336669395177164776781904280558971986312140978463619357998509625907715399532115642249964311130914857816779884760258472965614629216381966074066835/596757148251101285926183609816268835645959498947292217853310083772846234355163121320479665798801191637163162307972607307210089232832964266878*y^11 - 345468413948457816360527171892886541979063638283123352806584935034635625502218881905159592023966561026523310655906991078115122713819525702712354437374/895135722376651928889275414724403253468939248420938326779965125659269351532744681980719498698201787455744743461958910960815133849249446400317*y^10 + 549155822535976705487522766712343572922657586482748554529327958350963010732617805484093340176858592859686345007241731601267566394599618433385038560783/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^9 + 1127512479290541452735826345535314922603044533043852001147752285506492637945259590054150885441432985484513677628872289946509304470426846411288289420601/7161085779013215431114203317795226027751513987367506614239721005274154812261957455845755989585614299645957947695671287686521070793995571202536*y^8 + 8150615464716415298972751952039783787901028327104822909914752808593685816514856853155545399908904627620175319748282140554732404133894562903707925157/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^7 - 125110725724670065264007858819623740807167663156165951068088944000066037467535485493733127418907200507332940405151509535874888253979830570203904790211/2387028593004405143704734439265075342583837995789168871413240335091384937420652485281918663195204766548652649231890429228840356931331857067512*y^6 - 468414307727940442206699840118217927905682505110744254346278274274688944714677186639482777380291643844481200381823109381937321968337782489406762107/88408466407570560877953127380187975651253259103302550793082975373754997682246388343774765303526102464764912934514460341808902108567846558056*y^5 + 27636269832644354064706937914798233145113006045550628130687841151747281552128400887056086923215369348199042044012972948760507512147739445002330338177/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^4 + 772586269058753579264326618850448939069259672197059524150920065460201100275960234719729047552772212981500084575828341586849190401735388636717419411/1790271444753303857778550829448806506937878496841876653559930251318538703065489363961438997396403574911489486923917821921630267698498892800634*y^3 - 1108759064493998082232282034528546034193761818428379077905397262542625753753887986986214498582664454920875345383340845548222950276583055332233371971/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y^2 - 75394982792657970837023260877692222080751687573544744530370866527998661878044533199712073407654519512351345004443882562701092526638966538375840019/3580542889506607715557101658897613013875756993683753307119860502637077406130978727922877994792807149822978973847835643843260535396997785601268*y + 482003692335342721964535888958720609364731263950552375421555672742195788988027867908160160733460058088347310943625734761744312918365440194320317/795676197668135047901578146421691780861279331929722957137746778363794979140217495093972887731734922182884216410630143076280118977110619022504

# 2 Loop Invariant
1571425219021119258955515302675277434836740632872492290199882816719708379963085347315276121544172837344356511322565421268162951205221492081873768710229893338661541237568110562236233306447231310240661131727929838148275288416719675721510899369136135294108514916131855/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^33 + 16111382125023311419950904007102842962229854768754198521941974170260849260692973214177823904299152534019171690662490065815925048354213132542271509967164487263792887702988760166631073083178834149714091730352398311402874899484752672798782728650183751342342925538328157/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^32 - 50916067884338750668321973233267465923040626607428656956133720567365995298828132308946455970359753985624179116519676143084086332659143316930480862944639587910283529742805539593573796173626873867529749582122239116969786908751565881787997870113635298761504304385682917/53627777006722971954547208545345839994437575319043635011006258734404120408329570408123202167117185634174655778672056632213580356061891948792405072878682779479411964720084037678198363655886712303376764658830564997854202126677494662540044618220548376504920684848432496*y^31 - 22698801689906188562121131076050489632075005093006890952030184163466033772134998456843556656787654767685617201346684453094866946472756300096729660952094033799783417097567255800159547118681794317817670991928673043983207231435187490052522602119871385766843102526794641/20110416377521114482955203204504689997914090744641363129127347025401545153123588903046200812668944612815495917002021237080092633523209480797151902329506042304779486770031514129324386370957517113766286747061461874195325797504060498452516731832705641189345256818162186*y^30 + 15343758490978977234811767672106477330147308980562042669590179911489906921947390809087278990380422583861374586508340767613957159198463586097294970342410535813771080665887616295083451212621467991280735254162522185898883022599859170068095191576953832336326495793217791513/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^29 - 8442126570939607994784472307664815688129965843174185420610240402003318870285549104761769184457029472267730941793688245609678815391966973302008716221534412195694871434670452813857198185638197728439125242789980155355993072527414374730493958248345495040100692966696853519/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^28 - 6430858985352070246629413892857368652452285454040479286612628978250624536483579333101780395627108360747190109637781484685191326509988607456685063432759751569558773091878345594476457976040934425702239818256163928470760953453724145291235302905714978062602955365949599431/6994927435659518081027896766784239999274466345962213262305164182748363531521248314103026369623980734892346405913746517245249611660246775929444139940697753845140691050445744044982395259463484213483925825064856304067939407827499303809571037159201962152815741501969456*y^27 + 343786629745392941920750679754764272052922531852870519276114326267832341988893516279855560550382885806438840632121546997625578055127001278433194642520116648052770381016394921021178719986601436453766250298490442553137665075551858454419738964562960326934066189229115239995/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^26 + 1368840769227041089676282018673812589859126433769383206446451821419682803542546207988084082705030911054285228658073483491091590989664372844496232426071141623190342730303592728548024869070753971687002434974231021657270211882420248579654017942636218910654448596155687841761/160883331020168915863641625636037519983312725957130905033018776203212361224988711224369606501351556902523967336016169896640741068185675846377215218636048338438235894160252113034595090967660136910130293976491694993562606380032483987620133854661645129514762054545297488*y^25 - 1070461298736940641966563273617007447792647126232242991515988475404746522901679315368979547501419995182034430352189443245176954400994206401233824927358940423043100701981338881947554323756346471724729549621467766345827703752054263165761366912446076570941945488431416441477/80441665510084457931820812818018759991656362978565452516509388101606180612494355612184803250675778451261983668008084948320370534092837923188607609318024169219117947080126056517297545483830068455065146988245847496781303190016241993810066927330822564757381027272648744*y^24 - 13476908247777084292938915782455167361032517689519141232451919443490142220531562980811065453468512207321423569640976820822445429461598649796312878729119038326295369287129035952791096666176524564940682377670799336134671580101007882042594008234958810116427129337149946766983/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^23 + 1085806524744748400550294859961811575480238526396447107880778153428254264856557481912467828281774661147094607913136333634685540506833513095441222528099054570791985481318070369978956811622944551687291827442794775802013976225220320258826220120532517484813993860275632018571/13406944251680742988636802136336459998609393829760908752751564683601030102082392602030800541779296408543663944668014158053395089015472987198101268219670694869852991180021009419549590913971678075844191164707641249463550531669373665635011154555137094126230171212108124*y^22 + 18590129940485024090795141699312668428204317783209232847502973148493136834494471500729688991919573094002962839827092491895444389779008846927036525243395369745177703930129928689881985160382574062508340000655631030137032976895860697390259272475946724629913536202920674214051/160883331020168915863641625636037519983312725957130905033018776203212361224988711224369606501351556902523967336016169896640741068185675846377215218636048338438235894160252113034595090967660136910130293976491694993562606380032483987620133854661645129514762054545297488*y^21 - 90095946897964945470169104389483811845327550942665341976795306318619348838397985381753627371081614056023046570094159773761271570148447877020493590508866163045595087703377032182628485200607600461214407605774651071948458185633721983319668822013484028939724575268726186016109/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^20 - 9361128749657495601305508597422280792796534362383807353158731464265533572825884499516581271092671559665558090039779680920829731930021690141062196589024328127876777002421530567732803522021444081105708991424123893270466116271480882121252375029342610065273469694769228798939/53627777006722971954547208545345839994437575319043635011006258734404120408329570408123202167117185634174655778672056632213580356061891948792405072878682779479411964720084037678198363655886712303376764658830564997854202126677494662540044618220548376504920684848432496*y^19 + 63830266309407363049181155050822309855526698580680155981111415300861654888016677865640915792283707117162217756770747417686801024954979633745659501992320068130510175882044249606864494875965621466835599969122420311603212244396924157698847337440564776089462084223351326917197/107255554013445943909094417090691679988875150638087270022012517468808240816659140816246404334234371268349311557344113264427160712123783897584810145757365558958823929440168075356396727311773424606753529317661129995708404253354989325080089236441096753009841369696864992*y^18 + 29405613820558161479542562039686351692103745595273062025114476887985939212053316073183297827560831105662745663626542227750551514110701691683079722210448761312280433845363675393055311743941632146702604999050571865335872922258118961463019994474383356735128517676607058531467/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^17 - 20868787438398350336064100907797752286543829050541395946226700809842742245618445581927290707222320221422831944049290027701309479873453399702775682621463245760480986503362856823878783433198001820868496062025016998791424471255028059541540792554679886285498205201646397359681/26813888503361485977273604272672919997218787659521817505503129367202060204164785204061601083558592817087327889336028316106790178030945974396202536439341389739705982360042018839099181827943356151688382329415282498927101063338747331270022309110274188252460342424216248*y^16 + 39875622351930964638423043773158449913161180271865240898204209062294721577350640473079822319299553914092255915036583961282113335697008089435950768541823341898575071803487405014987099103256694823714596125544156263859198502101179090778175936566258884070938074128863507198591/321766662040337831727283251272075039966625451914261810066037552406424722449977422448739213002703113805047934672032339793281482136371351692754430437272096676876471788320504226069190181935320273820260587952983389987125212760064967975240267709323290259029524109090594976*y^15 + 12122225890041498708059921936719052846915691736467881871981943873363510251134928366547671943189435543484656913399697819084193738887475491466698979467262627712131941534110621672241266827900892208116928148843526632429615569728440182792845727965218316405086432726638343123723/20110416377521114482955203204504689997914090744641363129127347025401545153123588903046200812668944612815495917002021237080092633523209480797151902329506042304779486770031514129324386370957517113766286747061461874195325797504060498452516731832705641189345256818162186*y^14 - 786594876769841417904269825710026124909098188636938080434530786122820796997435009907135625823703529580378965542909707360193038020209102840236554748914526578571663397826979594762511255120456534553944289996677653982068225412798376660878132683221979396122633369269751603728/3351736062920185747159200534084114999652348457440227188187891170900257525520598150507700135444824102135915986167003539513348772253868246799525317054917673717463247795005252354887397728492919518961047791176910312365887632917343416408752788638784273531557542803027031*y^13 - 4869460739393365929530359562789220544743786300927911429600387941689865068913966436578195088781936311924190843409953038829689370247188904012397375234033537367864622611389679266037830874852281189359890582710175363500102339888546748025389978078996056395027694600833242389443/17875925668907657318182402848448613331479191773014545003668752911468040136109856802707734055705728544724885259557352210737860118687297316264135024292894259826470654906694679226066121218628904101125588219610188332618067375559164887513348206073516125501640228282810832*y^12 + 8005512399023934468689487425826539410216242403870336470975892240698966008524987808646127288146820232100600246027803120806140753445220398537468850168808239005228130679434665905022889776807000599094802776089846470030973838780639691456651510280888348945221557666256770209071/53627777006722971954547208545345839994437575319043635011006258734404120408329570408123202167117185634174655778672056632213580356061891948792405072878682779479411964720084037678198363655886712303376764658830564997854202126677494662540044618220548376504920684848432496*y^11 + 7292753442147774990102385987565446467082421556293095297294475951065284439761854610877247129830658064839957240267103042199053994308010175345529481143763371236550781577522846993442379789180813822432652551066856514240938107880837035093930666870414926107323650734042364547501/80441665510084457931820812818018759991656362978565452516509388101606180612494355612184803250675778451261983668008084948320370534092837923188607609318024169219117947080126056517297545483830068455065146988245847496781303190016241993810066927330822564757381027272648744*y^10 - 3007648771023175659971250679653789674296149181934712076280418962319806744131944927683984514388795654905133097662435826624027843144148803339829838141863628210052637380643092744568596897043550804418043729071993706758470848524629201663685345622043474352702338963712572292191/80441665510084457931820812818018759991656362978565452516509388101606180612494355612184803250675778451261983668008084948320370534092837923188607609318024169219117947080126056517297545483830068455065146988245847496781303190016241993810066927330822564757381027272648744*y^9 - 518361561310002563048826005787500080158568322962620099082229699247001172169279728925559526947057415740810811224260984248519263293752937356286441833642490675992340616705886574107792087763045821511910465529610705544264565932166011725368699792353284663010362872116458944887/13989854871319036162055793533568479998548932691924426524610328365496727063042496628206052739247961469784692811827493034490499223320493551858888279881395507690281382100891488089964790518926968426967851650129712608135878815654998607619142074318403924305631483003938912*y^8 - 10356661774313148632681399864359437187978863600221674669550648770681954997126153439369762329375419380172206455369618834027782078148376561177158403813723282341742911883151601091809447586486221961347962191895584159487541158977478915413957127450003772001105728222927722567/20110416377521114482955203204504689997914090744641363129127347025401545153123588903046200812668944612815495917002021237080092633523209480797151902329506042304779486770031514129324386370957517113766286747061461874195325797504060498452516731832705641189345256818162186*y^7 + 1341552995530782811944568703966720498277875745867931710210666621685273261561403832011102169864592143279292809191240943182200873983837158935015652357683743644810204882663904813483732770099023225161359613738332647520943001010768074417172859557831584203331712096317453497917/107255554013445943909094417090691679988875150638087270022012517468808240816659140816246404334234371268349311557344113264427160712123783897584810145757365558958823929440168075356396727311773424606753529317661129995708404253354989325080089236441096753009841369696864992*y^6 + 14457382569956686626635485811064493577856600317633769903136944043579207034721506205644383793673589821770196491620227647585467772651306665361760915797529969235425549795856584695193278626550144758322687606295584707174033593974736234930075295133859443762417837850199806905/11917283779271771545454935232299075554319461182009696669112501940978693424073237868471822703803819029816590173038234807158573412458198210842756682861929506550980436604463119484044080812419269400750392146406792221745378250372776591675565470715677417001093485521873888*y^5 - 13237938493331552753962909639380095647877299017172796418801906377228750799763287939831865179868401428172770814186435647721275145967455448157153019999118755919827841317367935920411178483805495994031946134157592518061875887368263438762832552867382165016340064031823641031/6994927435659518081027896766784239999274466345962213262305164182748363531521248314103026369623980734892346405913746517245249611660246775929444139940697753845140691050445744044982395259463484213483925825064856304067939407827499303809571037159201962152815741501969456*y^4 - 17815456379268651283189690009356086019274268811649042752596916521325504254916401317519618347721612500740138320737437884969642710011029575652248663406795881619343079805220397720101220583036707461810467006952146388297647722513228112444921994949693065410627056446587283477/160883331020168915863641625636037519983312725957130905033018776203212361224988711224369606501351556902523967336016169896640741068185675846377215218636048338438235894160252113034595090967660136910130293976491694993562606380032483987620133854661645129514762054545297488*y^3 + 6574913994421909662807691444179794249174658847256646881692642445079357408656140419184165142556325505166169589230909360646825130018075643756592156920520254969284154790623225429828444972904137759931293729536101191702695168411164001257741168339951476587460973114657520343/80441665510084457931820812818018759991656362978565452516509388101606180612494355612184803250675778451261983668008084948320370534092837923188607609318024169219117947080126056517297545483830068455065146988245847496781303190016241993810066927330822564757381027272648744*y^2 + 202825468231996936009174038915422104599823932467732747396245221553192792362975123206934274214037404427317579752730997566535263639518079389635719569912211816949586267651046320872892394138874738440570582641611902718310856258161214018037502726196762894966253625749089815/40220832755042228965910406409009379995828181489282726258254694050803090306247177806092401625337889225630991834004042474160185267046418961594303804659012084609558973540063028258648772741915034227532573494122923748390651595008120996905033463665411282378690513636324372*y - 7623646116673547630609622717224318616087100660660153833407030711364608362870912565311703142997526028837540376580140835718900845606070575040480390249170947218244247488641721969665557596603846379794775812535275964482313722354784389378223300222303080429058624565743273/35751851337815314636364805696897226662958383546029090007337505822936080272219713605415468111411457089449770519114704421475720237374594632528270048585788519652941309813389358452132242437257808202251176439220376665236134751118329775026696412147032251003280456565621664

# 3 Loop Invariant
11067992580082641717710141239497832855439859342052295791043262456451074277515495623709475580691974298140867196152904707018553156866589999187728588720604475132346355395372118498467802387137950642395855845304571049598324403132397440710166832810882589893358017196146156101006354069551118796663874313503013776556520299066061465241/17051482298981531371257253205426517182354218546278986448868275271201387204411345820927368021269619275200045528390452106170337120229376027545352256365202328629142692531346311501758161134246755892161955300755478283710488217120152286112830358165888356498500672599062142684411150334408316261686098178635187813256760701750006105032176*y^33 + 113894253451703361843887799754260994896240293008886168884737293642331775987412971357839266817972521773701522649181066245868424966572563832070946431686111989821581498330424260243616791711407973968686675842923124672040137952279696162650789131449958809742614059316885733158482958840712591610065258609478706856553275247389053181193/17051482298981531371257253205426517182354218546278986448868275271201387204411345820927368021269619275200045528390452106170337120229376027545352256365202328629142692531346311501758161134246755892161955300755478283710488217120152286112830358165888356498500672599062142684411150334408316261686098178635187813256760701750006105032176*y^32 - 178939280445114080079825553672880306518836521009995895971387649741052850637190201269296792577982636961387822818714383405873488395585585505459572289590528036420130151966316361604585251885678612564834459756442740021864195131845643689563048578740077915185840129499256840123097942418023977260822197396258689136865868604081337344263/1420956858248460947604771100452209765196184878856582204072356272600115600367612151743947335105801606266670460699204342180861426685781335628779354697100194052428557710945525958479846761187229657680162941729623190309207351426679357176069196513824029708208389383255178557034262527867359688473841514886265651104730058479167175419348*y^31 - 5274977289784684936906808291740113077170539063617867063705272668830334655128287907529648181732938984735713523110815008427488227909885981699940349062886114460781612130205882385485869282027635817404444499505678271147419853961331044805467761011479370770694245072947672522609382280761077241523976255411187164935349834905028955948965/34102964597963062742514506410853034364708437092557972897736550542402774408822691641854736042539238550400091056780904212340674240458752055090704512730404657258285385062692623003516322268493511784323910601510956567420976434240304572225660716331776712997001345198124285368822300668816632523372196357270375626513521403500012210064352*y^30 + 431784181534276222452997587796757227606273047590113307309882123998256573563534602026675209382274222174611469913020092546925499891613816127104124678402370364361376827961485331753698646259132334375851115015581012433039837411191065886356379693469032530499587168141308464361452163948795928336849442898873656330660066337106587533275919/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^29 - 221747825457023891372916746692640738907174611930789726912343513717201334789980338969610481190796460542017188418938747388875396689611077683890335753831923550140495465079560500152628894591777458277129700465399925643237417202443199345508858022138800030603338388226615558929193950169874796959545934394491714545440203252697399137204593/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^28 - 8337435925558791383458200267730667800104912599775164520024262940209688008001109216438027121382600195209914709927241446535071314605899151340795559092865247127674651330915976146015091767159498125072150810713640063604817988083835802566535147178119423940874667369911368540826568320505073383013284609119284382304714812109513760477465035/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^27 + 9371481281464900755785897189178360918623109857888749973981894963048231809101344822128506102813812137508160135206864575384331309173115874865460491902263549879712581100245126357222398320370511806384009178176453155301775301802120089144438131898908230109919175828609918517826473121522178611838009332399432626824266573670437446387409407/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^26 + 77382034134380433451047517712479328145845762865341256178056840543234669113002574868388575480666635842921847934984079470437487337798953292618436853263761517581010905016594747400940337464700304133080742834644138930980569935371323665239123340723525460820695872761245021909664419684650462860297687519237014347476242208993607045868562423/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^25 - 58830074946425446083146208318548444989359944820099003180816588474801823079927285242420430986252147936169895909431870626823325741742656218319462708665773898198078507016851895547185891149137271906662346143677248992830199591869261692486778097794350433340514053271097213608861062603692726988944857680605438915899850720057523797248054755/34102964597963062742514506410853034364708437092557972897736550542402774408822691641854736042539238550400091056780904212340674240458752055090704512730404657258285385062692623003516322268493511784323910601510956567420976434240304572225660716331776712997001345198124285368822300668816632523372196357270375626513521403500012210064352*y^24 - 191577318622475036498528196801004498533843164091277726416968528004255720589365389563751283924517353614549517429489260698723390146140869500721613638186119928400723760257450628295163307125452049614862597932194117526817774715712332403903603986107480894767240344379777602588404451054520299760190678230934250031955333388864239162309761085/34102964597963062742514506410853034364708437092557972897736550542402774408822691641854736042539238550400091056780904212340674240458752055090704512730404657258285385062692623003516322268493511784323910601510956567420976434240304572225660716331776712997001345198124285368822300668816632523372196357270375626513521403500012210064352*y^23 + 239619654734593037853666764865577953590119449396448453863442981287627529912563950367976619048832910505810842996795601866235629113405248939146274498208683390135382201927592046410983895557473488172353683091944852447587028382560256061781487770880357427233366024121879905499267134878584232529819143236859670600357432260680991263659223347/22735309731975375161676337607235356243138958061705315265157700361601849605881794427903157361692825700266727371187269474893782826972501370060469675153603104838856923375128415335677548178995674522882607067673971044947317622826869714817107144221184475331334230132082856912548200445877755015581464238180250417675680935666674806709568*y^22 + 534712321868825986030957602752233575744240269211188406190103376789229647133933497821642413809204310984970368306188522017121221539790191994195818082024736301895400359168705046030841940959353056840212326006808894464316788988595790441357087360142450513756424908621870775106495158032098757611248505402195025959344913767435625522329428387/34102964597963062742514506410853034364708437092557972897736550542402774408822691641854736042539238550400091056780904212340674240458752055090704512730404657258285385062692623003516322268493511784323910601510956567420976434240304572225660716331776712997001345198124285368822300668816632523372196357270375626513521403500012210064352*y^21 - 2492175766355439658890714614698645786682214673461237302133317280081517827047845193899000772785733245496421957968087890881372548281521406890061707848512662535289492963142249815975461682647160640316763915154010599264861542216820848377033816726179382583341176927903372777413501967333309725196805255662097434363673704548766688372454242015/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^20 - 276648937981270609530111505960574112031314786872768737076754460431613729472220529504745753553340326073124118217239949317164422555813354722994404691589922066001661050542780798938850622044959544441532179424285098051378087320347192475185955262599901044596472350422211763266199785259644871245447996575092995731776637091476348767867426549/11367654865987687580838168803617678121569479030852657632578850180800924802940897213951578680846412850133363685593634737446891413486250685030234837576801552419428461687564207667838774089497837261441303533836985522473658811413434857408553572110592237665667115066041428456274100222938877507790732119090125208837840467833337403354784*y^19 + 1770394392252158145063115888673816333557398336706844979894099150222462655595111122991478684207101424086606197480525071097634077961867226059166321981946903117526459208810692867528057953252128173211013177624416735547372787221526645610680200121243218843231707022443947313072308332409023695955854468083779138783445826828694440242872871305/22735309731975375161676337607235356243138958061705315265157700361601849605881794427903157361692825700266727371187269474893782826972501370060469675153603104838856923375128415335677548178995674522882607067673971044947317622826869714817107144221184475331334230132082856912548200445877755015581464238180250417675680935666674806709568*y^18 + 21648583965547086360006553727667908087331420967513609500760686826216156361092236459190426820007107000722680752895605657761187895247667761045392825956011516812800744858373087426886855621177763313938521758020357919205640753993620167652675639823841554278533373293197932549296174349055691363158649900637942002563931410322302333619822953/1482737591215785336631065496124044972378627699676433604249415240974033669948812680080640697501706023930438741599169748362638010454728350221334978814365419880795016741856201000152883576891022251492343939196128546409607671053926285748941770275294639695521797617309751537774882637774636196668356363359581548978848756673913574350624*y^17 - 2323577498872496113779157633241151863632721140858982296220400992884336676037494963908313785994549201415168471085270333806270638843929950032272871305858729629741727967754755229757685981949372142342942633760203077553223189430509005312810389616926594814408298617747677724083825908980597054759832110244076065528872377037648552382522368085/22735309731975375161676337607235356243138958061705315265157700361601849605881794427903157361692825700266727371187269474893782826972501370060469675153603104838856923375128415335677548178995674522882607067673971044947317622826869714817107144221184475331334230132082856912548200445877755015581464238180250417675680935666674806709568*y^16 + 900750736545445168484814259119250557015043250742674028978826753714940100857902956173439588476114734612347872772308329409602125607442870579819908110359774229935160108285871292597083369331099434885505883734515251594065854346588213015079729392835542876962245529434096458165677661648012678458292556974985144877419475357028513088359924683/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^15 + 5433549719505757877673924004054146913938332693574759408721640396158532329520311249283620531930644154961040542752547310044599907029544562127058752161738777393713788956678034131041971519301101371734429168813785101656072994923371114481041499514827371584820493756332258328610778775507838370640677984793012035251319396762807979507906506001/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^14 - 324954989795226275099944592921035893059824872198584369188082443056856867056353915656431003614111389786326991091616485146751056530408211962884152559225700867930630792900957805683696385781467013486013076094980751158715913605499270391778897722323503799094923112233568643361997551832091610617287660852583915868853622198337170518871838503/11367654865987687580838168803617678121569479030852657632578850180800924802940897213951578680846412850133363685593634737446891413486250685030234837576801552419428461687564207667838774089497837261441303533836985522473658811413434857408553572110592237665667115066041428456274100222938877507790732119090125208837840467833337403354784*y^13 - 276478900666315377926116079043653391399634619454367743158397048574772455307368987804922126885614128440714110948357035730825986091235544702747992329574448876938372405615162429892214422518807247685625561942678893085077183212265020969174925690928922800384098534573738757297914490410141401276062338448790879469000989838138726103072422555/7578436577325125053892112535745118747712986020568438421719233453867283201960598142634385787230941900088909123729089824964594275657500456686823225051201034946285641125042805111892516059665224840960869022557990348315772540942289904939035714740394825110444743377360952304182733481959251671860488079393416805891893645222224935569856*y^12 + 422347171865026570436835278935769989924439190621353156307883062943176333304105660515249557315951304217747254538750364997644112232345705385936285897390504623100424992685844927569575091577404507928382954637019459139550077129211706838612644363760272901724697858431605402668396244744899916995973977733275027830890035566967121388238651565/22735309731975375161676337607235356243138958061705315265157700361601849605881794427903157361692825700266727371187269474893782826972501370060469675153603104838856923375128415335677548178995674522882607067673971044947317622826869714817107144221184475331334230132082856912548200445877755015581464238180250417675680935666674806709568*y^11 + 840618273222358437400698634366634668654197843334139309052327665641191694351223117247098538454085183541791739316094760861749804083465081173870470788681284869784782425518896262479454723902948414242383438871685896784629156213306076231691309087353051074667550431373349652273100675166236758828818019229780888560330346602537822814398421473/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^10 - 153936363062566196549516692424953542624511510965736726377881998468904690192410245441000805020417176009097218311132436363090837688380742136907202168577592224283525950857521389638656686952140011188723738653505191045088195746086671089424589974635437813158578401967998360791220585868457283701407982253765828794497538991920582296184849017/34102964597963062742514506410853034364708437092557972897736550542402774408822691641854736042539238550400091056780904212340674240458752055090704512730404657258285385062692623003516322268493511784323910601510956567420976434240304572225660716331776712997001345198124285368822300668816632523372196357270375626513521403500012210064352*y^9 - 336219987783001792321098884558175146743849295642608800049256424279217227752628076286597133020234065158841597908387205628718648116057690473302583115637938834352693633760865517022337194272210289711600768853716242898495617465296875872304847125910620277121830922000923708068022651601353338830422906399084661429390367713820085851242033367/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^8 - 14989704666082962220245210840267195440337013393955276076235295907348177709220027229195626441643715133746006541157774362559874910987093343155732912370082030307849267465230721053015706609598236694773765890812148069192810866346678104327833148993962826038119264905861125784141586523521001333395870835842772471890828937264002663069720811/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^7 + 18251781056956864480789867663443505420268081691864083895624199614663924119538386626911331042130009454415706505749136614881392516703316102243962596567529760920033859119034164052846676465751067896119756395868090535713263952198592939073007290644507894056614695175125231074945541927823737841373323261711409755604654120017109066831284897/11367654865987687580838168803617678121569479030852657632578850180800924802940897213951578680846412850133363685593634737446891413486250685030234837576801552419428461687564207667838774089497837261441303533836985522473658811413434857408553572110592237665667115066041428456274100222938877507790732119090125208837840467833337403354784*y^6 + 161233862160665140510691593217512600028519295909275123315808836273935042992582205183586249585862516879737145218308313791768227845533786393443846974694986268846301706730852165932368346222172566637812580211498250496279172213678258195805993615887037184110885394741547419131393472935799608718257805966596733438103858129864762435548127/842048508591680561543568059527235416412554002285382046857692605985253689106733126959376198581215766676545458192121091662732697295277828520758136116800114994031737902782533901321390673296136093440096558061998927590641393438032211659892857193377202790049415930817883589353637053551027963540054231043712978432432627246913881729984*y^5 - 16304302705345891164186216110413358981458310982088978913936466330246602183694847090001239936873666335390606554425982892237656577776464422655451795211884575879205219367977628162238631671196698562320288065743937306056838803942638912894082693890118526791793439628274897622838055855817660648279792462315672637358825386638495290191997037/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y^4 - 587920419513113935751202008087514606592779356953688732328189690515170414226911578754092047316257654750167939926397234138698528771018243145728285830107452900213878609376985941589413368287546777521003186806118624382884568507333960312282314771059415549934144663207147243549234617571777376662169301082190271542416641819178959488898955/34102964597963062742514506410853034364708437092557972897736550542402774408822691641854736042539238550400091056780904212340674240458752055090704512730404657258285385062692623003516322268493511784323910601510956567420976434240304572225660716331776712997001345198124285368822300668816632523372196357270375626513521403500012210064352*y^3 + 44592642929231659360554684239559491748040539007511554203896473245830574390690435294701576235449335035956105908825710743332140222984050799651099343430741585617620835422012576852246599979785190157337647036383710681330882356715458687296940366868557162704973131577440112567158664948034368790067450438162987345142242506348947442551277/4262870574745382842814313301356629295588554636569746612217068817800346801102836455231842005317404818800011382097613026542584280057344006886338064091300582157285673132836577875439540283561688973040488825188869570927622054280038071528207589541472089124625168149765535671102787583602079065421524544658796953314190175437501526258044*y^2 + 48194256802061614584370820644561760998977593058057193915813753403951326386904435723533881564590400658636466387123312576879455505384341499465521112875237914625415643065842876004668047984321208065869389135823859817479938039211201529322674931220544866787991179241018084735997831034288012102255308859525746901985581448665767388464527/68205929195926125485029012821706068729416874185115945795473101084805548817645383283709472085078477100800182113561808424681348480917504110181409025460809314516570770125385246007032644536987023568647821203021913134841952868480609144451321432663553425994002690396248570737644601337633265046744392714540751253027042807000024420128704*y - 100848084115519789280162753750021243194584336963446272282523183343068542281172723867930131130005096957123230682834944434400539253152523481833505027859855450628056620328669155011671249817635361947896992777731777625059135957962392806586140739090058576859862845482233108523636798404278129940964271049679037971380785977948914873215/7578436577325125053892112535745118747712986020568438421719233453867283201960598142634385787230941900088909123729089824964594275657500456686823225051201034946285641125042805111892516059665224840960869022557990348315772540942289904939035714740394825110444743377360952304182733481959251671860488079393416805891893645222224935569856

# 4 Loop Invariant
122233474477509930178277509752039987594894330005730112655438470901559538196022961986018034244989632083348132668718193910715248414296857310570940045348102846564743295950944845802723885077476653181950674409131984234136046456579302343997678474057188128818044786152993082064829782426020793272774549843426434108836538407649170376734460462673397521068638053922150222926841603822900712689311311720198119755257331341659874578120607878857761601822170287864918339/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^33 + 1257089456891968452005919044565088889848584260864552339888534248937948777576151650655723942736504964966779594950694297465153847906021339788237378690191013633660095601848951258946892271034062540361801572708017604867224920411447079173689950301933116316055110616344230314587949379680573651043572926519348671121394927257321952601746385683662400489364657606198390680930387435594976662548111788466548328758801210667704541732065145009303652948799005262009340359/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^32 - 7907552808646233651036215124598519678948335346217493824699274972715197771057970370407339585194570595478317795922994640162974193782909121221565073767488365566981954467902723416110912873040158972699869720725695237995625032528118430673458162640059404838947894302113198087700834170632405004261140616384332780952173344445827010929221501000810539893673160832721592192425745873770910640774433471521833930196553766897745875807329525165641913996956076171756925181/61293482150571154891520408143676031881670158214311787616152608635423189835516761554504371018927997477238999540315172279102602440818937428347135527438170487450820543672571752194738726551851948425240731378759069475677017213900906961153057912846141738306196157386631408653888171506231204437455557952135599171119269744863955068020210111768972575856029460429978128155358648697984884326505884173712062696393948189046933101359951097827891351586285878887826017280*y^31 - 14496270400757761721318824996188917956066612656819475622498748188717384566524601997067581064102444235838018498438358890958897854759042654524704267276231135855498371325691653183559121127351883342760854154017843359560737588436992121992699558926983199354322472859685063895922610588284455109392466008699453029451914206315687928708429321594563808873520086523095927908823711545080828045073938837584041959318316487430014713085561920776925729038484617460162931417/91940223225856732337280612215514047822505237321467681424228912953134784753275142331756556528391996215858499310472758418653903661228406142520703291157255731176230815508857628292108089827777922637861097068138604213515525820851360441729586869269212607459294236079947112980832257259346806656183336928203398756678904617295932602030315167653458863784044190644967192233037973046977326489758826260568094044590922283570399652039926646741837027379428818331739025920*y^30 + 1192473805213714179890000598488705183733211562916508714449245873691900798228182049629442145671249682316436685274790739803346714402161936783894148471353955189499738295625165101801512807371567133802575614178717784544993549796663164982457114054064996604217027400093945670146664520463212960196026366709156510158147818596109106819450492311488769818797498146996524445761217739908819194570107259434753477956559616005759144165947738086455279687941658639916124775569/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^29 - 123845725284969607128059843231036044091960028829950380755005724996728433580632544526177532787466552357254358753532948364011632508977643783250779607219442517760680047624127178279448820305199208865587234576905532026647816577726158770836917352859780140762288364076975389440650883957919214335050170646268649851147751814396959234599158138889867491842434345345755832494169909353677544206219354230808161404434430736061904423139661918766102058044601050629617756629/36776089290342692934912244886205619129002094928587072569691565181253913901310056932702622611356798486343399724189103367461561464491362457008281316462902292470492326203543051316843235931111169055144438827255441685406210328340544176691834747707685042983717694431978845192332902903738722662473334771281359502671561846918373040812126067061383545513617676257986876893215189218790930595903530504227237617836368913428159860815970658696734810951771527332695610368*y^28 - 250255459850631502002224551061300456719552971877674144964976598544601814719179469813525944271196088925733410802767490468404446122849189384766543229993586674786272140751986233554138821400863835680711240374636707711185790219692548695858210069862074756313412118235214396494883126277230529188184910476942474471851615788575873619703139195371291396415270117213642526388660940653959467894323257497741064178449510619091346010418491676644980919829902708329149662019/1998700504909928963853926352511174952663157333075384378787585064198582277245111789820794707138956439475184767618973009101171818722356655272189201981679472416874582945844731049828436735386476579083936892785621830728598387409812183515860584114548100162158570349564067673496353418681452318612681237569639103406063143854259404391963373209857801386609656318368852005066042892325594054125191875229741174882411353990660862000867970581344283203900626485472587520*y^27 + 13007474899607580557491992528266296437833887041763550603662319941646888406195515082409867862065305272890137412200486633186502718509028531861621441324195794146927164106973402321110447035234730100470951117991222110613295963576112352034687129246883327159205812054737707590705213068342000080833308758787286343510111452659847489972641554787299405827923694844474608623115734666124196269401538875944607102248399281744529898800771849604380270733284236552492897709381/91940223225856732337280612215514047822505237321467681424228912953134784753275142331756556528391996215858499310472758418653903661228406142520703291157255731176230815508857628292108089827777922637861097068138604213515525820851360441729586869269212607459294236079947112980832257259346806656183336928203398756678904617295932602030315167653458863784044190644967192233037973046977326489758826260568094044590922283570399652039926646741837027379428818331739025920*y^26 + 213645529140043585933442942235981477065291477082707400974811695161326920770462948925281645160929493380931391924575735313148839210741398202737067647071838208524906564169191001415169768302350909148616070196645467076939215122960074719576546553351963373176353925609242513249143920991801764859981063630427015540569755564974606502193768387382070550656141292229845307679951719499188400991363173136041589945206911849178865514615148205561698659508262522158518536499797/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^25 - 16312912376725452596527716697721828255651782838103442104126786133824903646919703813105817073891296093256336270820603744610495264536711448383200774707288337509746533935430567623326052228384199349900906452225726792385500927036576132296854485073227205310150744500383529278019540274263156863404600126595403310119190883293712664393017174019284883642467025892656316548565575491999573347951124592066519115019703738814575407464932945930923921089146827436064455666745/9194022322585673233728061221551404782250523732146768142422891295313478475327514233175655652839199621585849931047275841865390366122840614252070329115725573117623081550885762829210808982777792263786109706813860421351552582085136044172958686926921260745929423607994711298083225725934680665618333692820339875667890461729593260203031516765345886378404419064496719223303797304697732648975882626056809404459092228357039965203992664674183702737942881833173902592*y^24 - 66085520892738830636840757545418675836219737867770451083690004621322243305657594114043443671663649671871459544891910949128351936927229866314784546448817373875166080709738950172124493196534145231371555370144552592638176470964456059941933216390026212678164616320144280334963323860850854425296012712661054983834024634305059399411894463415905804312866569456268230461736346799693585892349047218548634185356557478657634605336216978840878263609374162134591874546189/11492527903232091542160076526939255977813154665183460178028614119141848094159392791469569566048999526982312413809094802331737957653550767815087911394656966397028851938607203536513511228472240329732637133517325526689440727606420055216198358658651575932411779509993389122604032157418350832022917116025424844584863077161991575253789395956682357973005523830620899029129746630872165811219853282571011755573865285446299956504990830842729628422428602291467378240*y^23 + 166056145831968853752069294485538200321091139259479614069018897301833813581417012718910149291546818212628381305476644415844820307156116478975922779645629613739899166581284544423677606982530173856492778175328804015074255510174449248656519331093825247085114539888287559956736918684406075453358808135689425058300505195349853932042796538917489679820323576829002271082803047014448684525679985485229911942805859676638898726098644801810576644261442436392201961299467/15323370537642788722880102035919007970417539553577946904038152158855797458879190388626092754731999369309749885078793069775650610204734357086783881859542621862705135918142938048684681637962987106310182844689767368919254303475226740288264478211535434576549039346657852163472042876557801109363889488033899792779817436215988767005052527942243143964007365107494532038839662174496221081626471043428015674098487047261733275339987774456972837896571469721956504320*y^22 + 1474128829017891223755070858820542876969463126497694038992230508415939996226772995682780278855783841234784533217979323841011480715208911031765994994543452166276285750081611083446853793836767147809818462199271790923452980575662644712298381073567493289023449324724897658902172504389384653498385162893189013239142736970761671388421946657678093530631524749410034111583486794930997249438051556337220796937397506802803567305245026578413313421305345195699743886500691/91940223225856732337280612215514047822505237321467681424228912953134784753275142331756556528391996215858499310472758418653903661228406142520703291157255731176230815508857628292108089827777922637861097068138604213515525820851360441729586869269212607459294236079947112980832257259346806656183336928203398756678904617295932602030315167653458863784044190644967192233037973046977326489758826260568094044590922283570399652039926646741837027379428818331739025920*y^21 - 6908423248847528944861087275855880805574399389513590831908627416728403367680459886534621017441824987696073572709357264694497233872880005244100295992543880641017292454964732210410939705523468322466621682482504241445331694301245759569357910974657317667983028158187548802149254983374809796840843798715130697761653099957472407685621497047173455285539779432897968799570380915554020151846599629438200051726461233644111884658861248558032641879152278740587571753068621/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^20 - 760813025697077013802480962122139060185929780055845419589331896367466547823406024706008820833769778520478057524418250522054647609324527151702503486911493418216296362904471761371732830507015872360895226165404330505651198523862455360445122146507794994835660769573976833466929798503441244572796323375637527149748477964901027392049157016380811755685035652644570966631554524998483449360353565816206828946358975395861603819577481474585781012047665816411659440688531/30646741075285577445760204071838015940835079107155893808076304317711594917758380777252185509463998738619499770157586139551301220409468714173567763719085243725410271836285876097369363275925974212620365689379534737838508606950453480576528956423070869153098078693315704326944085753115602218727778976067799585559634872431977534010105055884486287928014730214989064077679324348992442163252942086856031348196974094523466550679975548913945675793142939443913008640*y^19 + 2454390855421995776155301253071132705312068228951909033443137666154724504343459050413708046332805285803239621958489307939238740174992908681889807696908406699470738632670815987127531869440589316344103571218533970400178547494316993246214949008861069984827743348339436306461940049900947702058638755342678935506329936656991893726407989253859834143043792995081017285938063417147321458720545805296406101441176502715911102058610984995628899849915923651020771374839451/30646741075285577445760204071838015940835079107155893808076304317711594917758380777252185509463998738619499770157586139551301220409468714173567763719085243725410271836285876097369363275925974212620365689379534737838508606950453480576528956423070869153098078693315704326944085753115602218727778976067799585559634872431977534010105055884486287928014730214989064077679324348992442163252942086856031348196974094523466550679975548913945675793142939443913008640*y^18 + 1352897771857490829456673008988964225538566094624177907463988897428047696468763006118403270003266140221940756739602552017813342250048848792583409456227637532970924428929045149493905125819421317485127135611371115768107753068904209172067956536509527911248482568710683176103908366487099372070862590185517345012433883683985793027407553588015635307744023147850147718472177992265967159977016964136080365835564555167253570706495792462804142253419716316466283958097457/91940223225856732337280612215514047822505237321467681424228912953134784753275142331756556528391996215858499310472758418653903661228406142520703291157255731176230815508857628292108089827777922637861097068138604213515525820851360441729586869269212607459294236079947112980832257259346806656183336928203398756678904617295932602030315167653458863784044190644967192233037973046977326489758826260568094044590922283570399652039926646741837027379428818331739025920*y^17 - 6445909828069211454094198456257471508335837223617297052263913800569439157113984189442294089194701209245515106709768929648185208041715894912045790614926896252437876703176066359997250253004006203141896980120131923373037262593942397407129283348647295161270875591353649821719597429225639691879366340979570069290685724233357312085459671331611544124100413333974758291966444272357061767319021869844287228494419282605640037117087757177708661531354579934269403442434569/61293482150571154891520408143676031881670158214311787616152608635423189835516761554504371018927997477238999540315172279102602440818937428347135527438170487450820543672571752194738726551851948425240731378759069475677017213900906961153057912846141738306196157386631408653888171506231204437455557952135599171119269744863955068020210111768972575856029460429978128155358648697984884326505884173712062696393948189046933101359951097827891351586285878887826017280*y^16 + 638134747560799094570519774865051637847692206930661407911667071406472467346584442860586033063957012522253012878801094594711046560820119169642265087184504579239624119187837550160249931865612121129622907970008974501790784731639944413179951942036667158594820611384441899706688563707185176224761399336246169183716628393171100598712942331625254775952014312129623112096780654766049119495585746908916914012006107377672203730425179540482527822905191894397028801881819/45970111612928366168640306107757023911252618660733840712114456476567392376637571165878278264195998107929249655236379209326951830614203071260351645578627865588115407754428814146054044913888961318930548534069302106757762910425680220864793434634606303729647118039973556490416128629673403328091668464101699378339452308647966301015157583826729431892022095322483596116518986523488663244879413130284047022295461141785199826019963323370918513689714409165869512960*y^15 + 235739775260090446136137016042947110626430132631370481870104768437221572426590211775150830616182742538935795579464341505409515855160503648547048357704795225526281144216508339699375129777870314403910241813104340827820907696872361841271935799136573188502794962134425463683938214766774383951538499136742091777403616249017263374429979893981453330910789962413718405441456147765129318314476357159032363569876398743878453154458716136689492683947149441427644369365239/2873131975808022885540019131734813994453288666295865044507153529785462023539848197867392391512249881745578103452273700582934489413387691953771977848664241599257212984651800884128377807118060082433159283379331381672360181901605013804049589664662893983102944877498347280651008039354587708005729279006356211146215769290497893813447348989170589493251380957655224757282436657718041452804963320642752938893466321361574989126247707710682407105607150572866844560*y^14 - 1815133194959390453246108848304320843722475930601011607473876435701239090346745202135377443977261919190449467569933731304476218393797643526164956092754388761165485177655608238536632945395623370400455120546067279148710468592612818012191968851781163202170750586146450043887470709798660399322953927503579080781261778484455502314235736164610016145379357321758758450246380810399878493328407903527747906450831272611265482255682324752832011048093588398819002602184981/61293482150571154891520408143676031881670158214311787616152608635423189835516761554504371018927997477238999540315172279102602440818937428347135527438170487450820543672571752194738726551851948425240731378759069475677017213900906961153057912846141738306196157386631408653888171506231204437455557952135599171119269744863955068020210111768972575856029460429978128155358648697984884326505884173712062696393948189046933101359951097827891351586285878887826017280*y^13 - 76875185475498774706145607203323651725893598523191191340039613750052238934073678221383372497696999839004914543818603412044691393776764116336829294314543089940883648760915139191099312978465219390512502777066304340512905233880890330015889713118394731131606546413620604712911167672416343785503016951543906170906431174604387829467229177190416176842526607009482150601845294992414678851339520106823538109496197237527321586319394921509790237977825890811790445423663/2043116071685705163050680271455867729389005273810392920538420287847439661183892051816812367297599915907966651343839075970086748027297914278237850914605682915027351455752391739824624218395064947508024379291968982522567240463363565371768597094871391276873205246221046955129605716874373481248518598404519972370642324828798502267340337058965752528534315347665937605178621623266162810883529472457068756546464939634897770045331703260929711719542862629594200576*y^12 + 589570910633222000289589016170204603712628914374114084764956559969772271827767644367094454444822228708839984647128253408620054154744742578613360394301977878195679097285691246146727902050375625875518566443073836367153894558960459354309970723825903950288649418870862037064856458942416726595109797050038853004940081075078457264981649314008770274998317321231231247936554144896571486681337111906323605905061736215437849552205935110028384167330311668320525933493593/30646741075285577445760204071838015940835079107155893808076304317711594917758380777252185509463998738619499770157586139551301220409468714173567763719085243725410271836285876097369363275925974212620365689379534737838508606950453480576528956423070869153098078693315704326944085753115602218727778976067799585559634872431977534010105055884486287928014730214989064077679324348992442163252942086856031348196974094523466550679975548913945675793142939443913008640*y^11 + 2340365854414778408884577086351257294443721206442200093958590678512898524784823209284186119543117076150215681669609810525469203535165527459578566576862545915125141604055518556534736500148359876894578579296171077657037366422307080595966082342924369671526281815364257280395342449229075593146582417903412771353545374049651691082045090386568438379331460698256370711683708116633494953680676367748642651140543177942595238048065808086015710969197319887758811769492153/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^10 - 866822215539142857128899705380530640192063366813304353996406874851560507504719033221054806663965552295102062443596986637276966857697791038602886892669630878690565913869878915858480840333101627485586511342026066487555766372651732470924250505081583009297301825146201794747699939795188440300357978379507354280625730094618532400927325333808248743564670994275384269407100313841113951903247504770023977491660468732095974263384208683331602453756109925077057197556883/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^9 - 8160273261068642576946013362290485570323624268747957702016847010164934813596877939390875686088718204404394624091127217751074041623619687839587402108563428844222738400764584494550076665347405911123290767708800284084606515223176857806718232554040973987380742700505326396681712114524401206963112035113149245519074329579387784276578423662914347104564487497891487366675113749444322433534202721968629562857205573077418588108033944105416712142280425469132099070635/1598960403927943171083141082008939962130525866460307503030068051358865821796089431856635765711165151580147814095178407280937454977885324217751361585343577933499666356675784839862749388309181263267149514228497464582878709927849746812688467291638480129726856279651254138797082734945161854890144990055711282724850515083407523513570698567886241109287725054695081604052834313860475243300153500183792939905929083192528689600694376465075426563120501188378070016*y^8 - 38112875027037615133410579610411348422108201717693622227639826714280146106341389806775461525604398360060112720880707851475353526488581926142653369785876994517830088570991468220921972912801602837710508445130721937307849188045618783679253198482087554881420683552903285805137741290198518445152424316532709600121910365002705449492292306664372252887213626646437329870563318563440161393041320560265887321168975307478952476694748027681870147107771717778637367329513/183880446451713464674561224431028095645010474642935362848457825906269569506550284663513113056783992431716998620945516837307807322456812285041406582314511462352461631017715256584216179655555845275722194136277208427031051641702720883459173738538425214918588472159894225961664514518693613312366673856406797513357809234591865204060630335306917727568088381289934384466075946093954652979517652521136188089181844567140799304079853293483674054758857636663478051840*y^7 + 2561072272151099048941564749596830530162085291170820427402682677892838167316166114156024078442712813990978731238780634340268738589834735188593703286772043906622455556166936149781121302708675066321396411949869558288595229834024908721422669058135118314955725564777226928890999207522880093478013025652476787948712450808110966638202934628918699925334523835543004647900951406160789309988414696185238839452937967466952393685635213393617815994846348128035413641109/1532337053764278872288010203591900797041753955357794690403815215885579745887919038862609275473199936930974988507879306977565061020473435708678388185954262186270513591814293804868468163796298710631018284468976736891925430347522674028826447821153543457654903934665785216347204287655780110936388948803389979277981743621598876700505252794224314396400736510749453203883966217449622108162647104342801567409848704726173327533998777445697283789657146972195650432*y^6 + 1363295632045573417225608256917932301180375394594726744391270815933223130866415939328633007386357611451083826434352523619953867184410218449134143795915933028002824604648945789591850514404377756947827955535722236493890179592957939418602218130527834734301882873340022991386717652341909000284557211325303883961774813624418939525501851355568045239710816911884346444194770282706486672159937416239234291543545397798494042406064913561044880159516779668788003081721/6810386905619017210168934238186225764630017579367976401794734292824798870612973506056041224325333053026555504479463586566955826757659714260792836382018943050091171519174639132748747394650216491693414597639896608408557468211211884572561990316237970922910684154070156517098685722914578270828395328015066574568807749429328340891134456863219175095114384492219792017262072077553876036278431574856895855154883132116325900151105677536432372398476208765314001920*y^5 - 996422402686717702455419080905776808511206465018903841706693060123727021031153384105728584951727094172864041469884367027543299994475583348179771369543080694800018448990309274688551097619750824869801826642426424987165014296041642977000735198106576575792413098125529193015528443658634899797766015763869315042531359590762953429280566472092928843165707957805427766736153201784089182536172793218470123894179063200270755273806927484330382541803980664001640877507/3997401009819857927707852705022349905326314666150768757575170128397164554490223579641589414277912878950369535237946018202343637444713310544378403963358944833749165891689462099656873470772953158167873785571243661457196774819624367031721168229096200324317140699128135346992706837362904637225362475139278206812126287708518808783926746419715602773219312636737704010132085784651188108250383750459482349764822707981321724001735941162688566407801252970945175040*y^4 - 218681585072119850588720024219794445220221372522809950362813547156992727851914649194719774815588867358568225149090469081459927339253540521732005184349363136399952747610285644319274366036657478715788269405241178408443858876231376264513638326849721883059719454145638896478030865016309532291147775544536752602305754013584237326455232303666917163681781221593209473251368175663891459735921696528257618626255993625187231898654085414595512770276520960112776405347/11492527903232091542160076526939255977813154665183460178028614119141848094159392791469569566048999526982312413809094802331737957653550767815087911394656966397028851938607203536513511228472240329732637133517325526689440727606420055216198358658651575932411779509993389122604032157418350832022917116025424844584863077161991575253789395956682357973005523830620899029129746630872165811219853282571011755573865285446299956504990830842729628422428602291467378240*y^3 + 49736603976558164307017565514670391461716369489873115337614799044277325101690444345701185432313816504307334406935126083915215877423236074863878695124990177894621030329090670916334684386595249844027555823506869273800408629398300989126376733026588291112536338440037075508896271482157884741448350626180077416486922374323663381263007022193598910491626969102420266031668498534974435192680121873673944621245871524167359661330739999491236649045400138083643615001/4597011161292836616864030610775702391125261866073384071211445647656739237663757116587827826419599810792924965523637920932695183061420307126035164557862786558811540775442881414605404491388896131893054853406930210675776291042568022086479343463460630372964711803997355649041612862967340332809166846410169937833945230864796630101515758382672943189202209532248359611651898652348866324487941313028404702229546114178519982601996332337091851368971440916586951296*y^2 + 73861939573697123728023099327998618249879866098117312521050745346695140280694159529067901868380665996691094736056552528087567945066248531021305987581947821265184297947445758145512220875623230536839103784122869822562014385249997099806429377983016593032567834615523240577472723327575051555810030461946530995207287446063153984388720821016132360340053530394628558391321381139518525534669734692922093012622551493795052251835536623788912667481026939936541563083/91940223225856732337280612215514047822505237321467681424228912953134784753275142331756556528391996215858499310472758418653903661228406142520703291157255731176230815508857628292108089827777922637861097068138604213515525820851360441729586869269212607459294236079947112980832257259346806656183336928203398756678904617295932602030315167653458863784044190644967192233037973046977326489758826260568094044590922283570399652039926646741837027379428818331739025920*y - 102062264763261991221664164675807416500727615765946448996049170282737301592931509826608214282133147048568240847108931174929664249248761624169334818088280070923477489795103248684704896377072026618145060777489037959820174854514155884379755502664366383645881936496078877817341596364180921681241739517430499457977506702265492480232282120067423014458389748821363807644591669696950126916256199664728997287595355636007338450879933982898636843579391876663361179/5107790179214262907626700678639669323472513184525982301346050719618599152959730129542030918243999789769916628359597689925216870068244785695594627286514207287568378639380979349561560545987662368770060948229922456306418101158408913429421492737178478192183013115552617387824014292185933703121296496011299930926605812071996255668350842647414381321335788369164844012946554058165407027208823681142671891366162349087244425113329258152324279298857156573985501440