# Manifold: Census Knot K8_41

# Number of Tetrahedra: 8

# Number Field
x^37 - x^36 - 156*x^35 + 946*x^34 + 2248*x^33 - 23128*x^32 - 8301*x^31 + 246020*x^30 - 45816*x^29 - 1507876*x^28 + 524892*x^27 + 5928489*x^26 - 2144676*x^25 - 15647620*x^24 + 5182463*x^23 + 27844255*x^22 - 9113693*x^21 - 33194551*x^20 + 12907127*x^19 + 26677298*x^18 - 13522516*x^17 - 14784574*x^16 + 9000397*x^15 + 6135518*x^14 - 3128606*x^13 - 2324990*x^12 + 248250*x^11 + 790890*x^10 + 162832*x^9 - 130287*x^8 - 65484*x^7 - 3121*x^6 + 8028*x^5 + 2776*x^4 + 264*x^3 - 47*x^2 - 14*x - 1 

# Approximate Field Generator
1.89524564822169 - 0.595299418228666*I

# Shape Parameters
-15770647276898472799182904647683074021513105022265673696037650395012084319064546319730017143206084469506756560257966754553/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^36 + 20148404523606880005135802095715685875278874630011751274342156343133648722630886463996100196324859469718788118762661615505/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^35 + 2455728205911080061695681986774520051751766774346842563189622321874460605748477618164796883335156942084386527144239530557521/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^34 - 15601457432541473633547474424037284453272011566917686010316856603517813261397985156756490073975012839752463324334160841050669/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^33 - 31293164082432102961984241248213071381924488077958477544016013192225832891483154056671426517189542753700257668775179319439129/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^32 + 2693632982609638140866237393648396900371797626243172019363985324752009966062664823261280953889174907870042539958955383789001/68609151261727969828063554503846878749869174092466903563491395018844498051863390641075591576579639661373099087490064314*y^31 + 14860291453470938605119073906230193466989976152824445118433733016028378601048921246570058643453286939430253311237262467881527/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^30 - 3912412744143319391120590361405241488048947187666936258023698947209863130782532593057241737151534944188606446812272387404743827/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^29 + 896229430292692328898624338905777190589477245083826289711285442207359063930644949987604189984544503779255873530120159142386877/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^28 + 23540905069633155067341816107108191896679567462050610261163545126434437076901275946493377102122453096752853527316653593758176321/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^27 - 7392778491981369597812872426497892478566670567049321904621719856966748416078440495432042560310720237758549911591562628286672211/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^26 - 45482592170671893999216484428517664575435703595887238538256421210265399813223099358050626447958170583512117366188096314879036728/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^25 + 29583123292197237617356129881636172997538872713073248307656723988393893464686169046414287931788101030548978431603371311447872443/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^24 + 118214617247126948030524752696076990296544048176987854211823985961884449719662957130004172851544430355850152463086903059875134909/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^23 - 147829056045741294207266790518288240367583018648837558736475046911583713460894232198020543735588906706994445163526342346377896447/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^22 - 413615631456987663831428311670585631850306317231589529128161218398724718066018015788822953451334979661855913054163811507086562431/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^21 + 129749283419599220861907540895802166537799653017320945643322432014968087698019458605559117694935684374728476451394375267389289799/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^20 + 238852763129080717482174151537086942721323447468654887736635920560471716419459219777803831970404694298460639867399298579810259995/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^19 - 338512856720030025734763459217395306600680052454734947625641690818185330522638553237898855837106492499713640173626967536387217399/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^18 - 178048458064047701301483211112796733281605452320268537847580033380699894460943197630508891827222644541849487851430934913000316226/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^17 + 318018909103977360095641980948561515054747381720227147268321986716645836963663707183674246899144097006625694510300405382009980985/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^16 + 83612589911412680222680260413463457448630422751459441959119253276471223446472150186309343028021595014444068595377202662170560786/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^15 - 98213480963836719589692780909749140319461057298940698851386476619540009553372899296366835140579074024072487293717969932364059196/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^14 - 27035452137072364360938915992955033144352543797910354207952404891547641307875371222409292820667269227168764406866476681937742042/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^13 + 34860651422497446130015581267490587654510392229401599628679012371517486466349915998761000468353025646670092373084579405737446349/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^12 + 10869556003012900600726852926588134450177068748213623386237678843166349636430233056884083043889090361503484573140776146010950627/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^11 - 5652575086929019681330706324326331016554037770954581092975104709272862038876764226950464456390447966228880193944313305968127903/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^10 - 5321278491973411228897832526565401063733017189362733315551094858777141528226493512986628972803058763251342190201966823950844056/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^9 + 107702615462183065516088354192182547283852199157491164074350467194778480034732963737727651909039686635491817556370234733570067/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^8 + 2325606610286404877085501249434961342120379638081169583079102870188658839517694773792505643427789549937777011643010859922809745/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^7 + 251169262539323137482242183751149589066063736517865364279000738009909450388190816118315279679867844933996929131901570206047230/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^6 - 57234717961525470463403706322370993993977714397009629008192992250255592065911522400517979843274964164684195088478036007847571/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^5 - 55701633527940297371465415994961064640792540555038849544944598507214951492429438559836253939349287694189345314027873414016594/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^4 - 8461483734700289973111539624221041809563184442369179586340173723979981451874818609397819479432337371028035321509921595366522/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^3 + 502402273972027831447161171573003126947634291181643694671915231308340196126068587274108371635923883599005227561431586451465/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^2 + 448938334326133143103526234115664995881465458101626467857369917772325810666893746347839551495525385172627327434553932214115/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y + 20915318613979073449369864521452072634293893903449504512076777781511132209571820061335773838432699610083246375653433235327/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823

80171991020137020943108631245152720932238838420757912610820519971185249939209384097545341099523043065200311003752762196851/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^36 - 97050525720941110417019425819287927501930624258219216803539188057780099491434594283363253229667396622510019508521874786637/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^35 - 12489320325691748850570652299826925721410711128720326240017352716018067186614132902266327730259792311569340630447257002275201/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^34 + 78473422011767949884471925015130217345136440586139648412181436466375882408210795137364321537538367779081762503248848787866947/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^33 + 164161732757688221534202965126734810661624936575926706993742001945299138386075605098397390239353416091909416043524149366495435/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^32 - 13606457223841677724247416348564365706208815170879589937306717261583299398115920130229602132754350740908347273851696388127725/68609151261727969828063554503846878749869174092466903563491395018844498051863390641075591576579639661373099087490064314*y^31 - 137590141567688842984534249823510712251259543759280482025969812343301758247143893151113820039491306499875177865955366131716746/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^30 + 19844799145976876504233150778358112807284377699102491926857981496918914561427465930607446385360236613471010929131213794617535007/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^29 - 3897153839796844052256187558721591437732811512686998248999535562106128434233547623266751139078436636457842012826940314403229204/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^28 - 119926586367265974490024845113030581084370946462985027287603373124726063897164014689885358176307509366147724594010392722811880621/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^27 + 33554469384790662667260603910401657903307819645696418259566947641100710704288736077358379915522941577972890221527055802726512566/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^26 + 232673565870745584848424949300108217121593276988911115568702529940816467333146640938871852070866179095767467858173917387923474094/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^25 - 134620542955054108405218834868103776371194058758192617705335210045106583794418772180383931363811621749287549428393135526550423882/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^24 - 607049439420688547497685588331350568663848150504895104058257744244593541000933758828767135502538022563050382790163664670432184370/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^23 + 668736398291887082399076344902828367768587677931910147669197423533303961846166487870057237027343319063347836594156358798267219289/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^22 + 2133342352871943398104225929803101991707789043282590368026671497186366826233427554231133938862025782944013099222393163699801356681/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^21 - 586457220360474934647676291354486133036742167795960499097389421873261480258694305173621488750420215227291614001301462050550426063/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^20 - 1242594389779157696452584836724953500205253328377491122945931779966907761385810612087603428754685541139856278185912793772878775827/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^19 + 1547799590393858603125090979364858415795204068246260735994743859769369652986733744366177818025616660868537219203521179172423613835/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^18 + 946438022015379851086217381834350831930908401681936423952806185865865539280754837516624750977421452424456591590446016564274324203/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^17 - 1479233403537547793401954852905437241359111100764276781923636885646330727418695687924816860596064628028667509979526100455751436711/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^16 - 468475769657374557153259077886553885200171164215180575767965682600910295736925737555738402569214021015465148181128160468963235705/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^15 + 462612068125377822148800560814766465365171935237242310964193724082476522487630391619986663918178456397044203063949326967345868605/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^14 + 166702648742102844932277814052296682367337307860292253350766698833315321773090696155774779308584052683129590511250144152952667191/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^13 - 163468124788013645103347220600579195961853088247255857477426071358019491647125277294652670243674513443288839178809572916006749097/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^12 - 66344475503461290419498287440326588134236015196071144328452438886162691128534086918103814902374925086197532731359324197996217561/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^11 + 23989459964149560325395214942667188925938931340481239952561644921973217124891895049356158971578188205787857751348893643008877089/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^10 + 28830230206185311278909481197942962114119435081946827715071700317815696726398390211455300059218161929880740513746138564003472430/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^9 + 1260148443322968225342714587596087633452896461653617559579686929261003354673841679315869242588212711506839344569483468130023949/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^8 - 11695694866684780081865319526209078252047020874832908563510743870618727293743628678218820749179031815538460308230205038985156895/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^7 - 1689661798144429498625749149502400182888258508903561533743829566327081136753053622641783757945679693804053529290132489331392987/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^6 + 202032010838783193409715089460254717380845432964377699830864782670648181034472347755515474651957164156116069458371325166796966/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^5 + 309834679213343069543892046150327054454048211468554890667041686456812301118949642057173401368330645843223782043481695182254996/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^4 + 62196324878994504594893659624405306704715796598972906257669320473132141091197101166545123745304536696555458774355231925173270/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^3 - 198816097970219168220149816770800703580344582356744978821850459631858207035441487268504323693649671343684716219200511932153/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^2 - 3875862148710592366536763385183625997899426239469800563354079593742279645180378669689665321251152077152222420736880986956447/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y - 231050037088725226122768478433249860567281857761925954268619691828394831021656353183408825294678365843488369658557976417863/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823

-2365975796722679702675218894591541056223477248427593320220099155106829494947748942711467075902163752696102815986051665409/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^36 - 605172683564899332452324994824325355367928072994503432704449068110060261626158398193297593933801892417209205973877778292/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^35 + 370102745264953160020111546455507869592510250643672396712035718832952209750679159781001214992010068494844488391566619093327/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^34 - 1774262226220518885560577336394984834408843644776205541285913184099006608739886738863460353295278727482179991843994425454464/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^33 - 7823148076758369538984104539531410801219062338768110454520451812192413281936814971705265668223862799868035455422052871903750/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^32 + 333971718924756179586513998599510439737763052522090760116525566564140881208877741359180774713690213371871107546777318153397/34304575630863984914031777251923439374934587046233451781745697509422249025931695320537795788289819830686549543745032157*y^31 + 82692770672082354920123283010168132995637727306207078670797221620361649424647909845451853028024065935680232207204418074579692/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^30 - 516369827559986946309055778635222759684798196597044125396861672703897349785340999765021739643686309740316831808110142690907983/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^29 - 574522570085344235418443170659118990387693151684309953352683872644629504800449196617380256410125999949585742198133177727976642/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^28 + 3256902684040858563629514507951215295612277805765812477143405998641994249681357896870183483638697750281657257016937722694334999/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^27 + 2982944580588766760818339250403573065477326314552595892740891203755481822930282522146348044223662246841929757784575903017328465/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^26 - 12810773193739421826672088987525272627681772624635997017298800158717548506591239978710776297859955806352641003197115686292014738/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^25 - 11428778970090325742943127932642271893400053580716803670576404557185747661342433013202063378599171277125042679584481792150272196/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^24 + 32530143105506778284625188444315305623875251101352027899374852137608724071292256508369756066841514778688500506792257273845850380/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^23 + 30061768731494297502464609506450598601693183403726570407852416694412479322900445943987792965712459071172571027248530513565953281/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^22 - 53431568959158753076717699671915977875655646006190661968936943741692464642568929220329254989689729087855404978471288725588959001/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^21 - 49857183413823058619043372337096788617782367746558666244908179216177391767005462280811346006456411828062531174418032900641475610/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^20 + 58764149669451789972212634167561039171798399507385144895383195917890786283120459285912294016170154133511423377731865346343252929/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^19 + 49776685755536216976580753428109019683999962542368560115681014324904279576726432821467800498427643621484973439921706582868956719/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^18 - 48835650075562370011002702604721939434083513188340976059558627289943348212603296532531071818961323381139925999880446222735887354/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^17 - 31894255499388727214849812984806451887548631456131650473578279084585476414304566346449249519164132563727145769752998429115835997/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^16 + 32821005723890353441172373257899773903678474899784391432590560623789009618653534390138644956898021379224384569346046248587441120/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^15 + 16550884765751111717519479290976012740781458415402925488637309687646015140190864639065204654984668500015939693982048330700523629/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^14 - 15478303027932999737858304011543067119164505706979716483887734524163360212876869672098148522455522760497885443615429363195139796/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^13 - 8834875240607488688144648634728828181406120797961181961715014606709672205099409756766964188418869063031491169754787358974102550/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^12 + 3456138525227373365044879257866015374413527599949968796290961586408460119419369785879563245273709783397293975633484474777534457/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^11 + 3897535958986929334580206762695018858040359166893673681144558790330238551160052946907541002588133805618197359614538472411648248/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^10 + 435754826272892541621745993071431879430168977476778737296482333224776083796048540708202856658490588128514012500652129534996209/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^9 - 896901291204757500377453042156936138321871624558947878366101826166978611972993502279593250819371866436706129684290039454450705/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^8 - 414874327058558990235251080357543578626165115415773112956522477100323563264399986714425140768242126185040595777217993161301406/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^7 + 5305434430564681761010154527246611407369761213531035072758589056928836315316496983976291439169254754080465757230302991541057/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^6 + 63232659150909698040555442925672199485534849054593621138298824370107361588278343228772922852327689604535622652108454092476972/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^5 + 25253229406864900586820873157628496395416441644866688103903896924167870924108923549768713618389078998914666064937491959952226/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^4 + 3283372121753724101393959959865493339303174592280123212097351788634867898796290597454596985648707025170683164156320320684474/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^3 - 206107616829186854744862606676151161760106417336890851861792683437864407293111130497761369458320368298803941546800116240139/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^2 - 147099720616471868526201100822633789410429019432866542123411093495192042760215688096605341344776372482358100937651339407989/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y - 14527648881341718851134474621355205219942363220997062062666704116974279432772087525264291893468739170581040308792385675747/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823

15735570582417133862024256603473916634977589603032760404311439746809868331077391972433496441829454100345846052947365846025/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^36 - 40688222492699825526882595064780291854047379053271823382727264602645580084076890608934067050255860061713279252697847087947/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^35 - 4902080869666878380712157486385692848046221471011020973093311213914817475032309830221410055988377747784857262159128134852789/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^34 + 31209215397340815089530852032254225332881464888161781473054971548417361370759745343072377694904796338489457825149454401392659/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^33 + 62309320320049280073312559893892239698886336629155469004979461698878439307854999168971112447268389446696167398313254938931863/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^32 - 5395335994788814054797318528846916840210117594553653119650578394474288463328584592938036074305595365830198289092815530251845/137218302523455939656127109007693757499738348184933807126982790037688996103726781282151183153159279322746198174980128628*y^31 - 53932079903510658360004147304967046438490258341235192760540780382992481958049185758333390215542216663821017206174225907322129/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^30 + 1963672004985764765628517787569065619217811585721770268399502868145765528578205187135957729266186763066067171904697100340995677/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^29 - 3648785028824097987651427243812865758248884450715831350749923125435904267853144927275133398805348388399859888528626446370768319/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^28 - 11857031473655997630646937603836814845319752473991299885087458980337229930917507720565250816131601908763853176997769678483031815/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^27 + 30003803189688254651850572288370360178994257885734920578175001791071614317445833593800623577822582342128420486281026870162382947/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^26 + 92116881620205269695598967650869527773828410899870808548417333240498496448476282342913835877951176395138736349896088555076128877/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^25 - 30002950046469821367678208259427883439185547568863839783946122864654817615852785609269476156589659692392586785640020269808471113/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^24 - 241254778503606124482573048015765400317714350252032589418661994881507399197152100833545024822982574104326596756333918536056409759/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^23 + 149578455695848378281602257934382698778889241830886615059934000300271457765416764530237225189089395440682524707505849565809227271/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^22 + 853574770830275545976774416565034935023839237929097217778075358107781473790621177298179987646678048667071834758988553661006962957/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^21 - 521835514411236284780921819548207241641017699858862104908079158911274540878797844199129906838470653413324598002016257818406457183/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^20 - 501037439508484595493979633731134237687460877642818505851847241675379916492761778416506042762347018925373394868454956209547638719/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^19 + 169014751738658127976141546816016374148512756187510756814691533414387959339683387762696765228509824666998399444109664685632246089/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^18 + 766391368597193549177779988322156549651751213761694254028974556289762980361691252193789559283001547206841687426625303565282904891/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^17 - 317640671412254769791328839947924890377587304787281914703262460873433258319549218532193019237338949517247247842311056034639814175/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^16 - 378589919544057885540296806935204509474311217223332241704965139375903886259550612048029416795024687032413352979429278684759118695/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^15 + 198184235540991481615201167573236114644522551164602200612359074569038864071621084590287170004439300071204159802687367381419175843/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^14 + 67722138225207242171115406008206453395847025932004025871124813789382393506202220126947207268777243879730523724627838589266841735/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^13 - 35734018740969424358383056491128302945784859230497178548516612209760392012011306404135134940276164420852988595532394376965090411/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^12 - 14086035743722899242979220075797871507624566200670141790033920447550239485912023159556362994659358206635246731085379594272147053/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^11 + 11311956220053958556302482215012061104519437928450598603902728152563465632147178437054809710577546336429978427695201616285622993/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^10 + 12720164846677202108710004376259476170620410629229485309742126054680635810486154242054971675987497176415172868467393833499265979/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^9 + 209651520346717880666654744547999997693755759065181996670704648461980439219201470323809906595980915808371222761316478411979775/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^8 - 1339958705306716657980110291256207569475408587383792689376448628745332914764224029479376900274160631153890621437857573807128962/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^7 - 1574836413587431820994895477443547620282057318700707122954143566119997413729462503317247097827637373462670931920648232649618901/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^6 + 98834324766281110801001651248476420801802875652246281832096617253033123502652321240005301586897270224797677291803841955534743/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^5 + 148421986053748954139512802972774725686612600731809912822772022639267202177144070633088456451880424403588026845467729846562803/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^4 + 32124218527127125309607142474100719771805034408459118077535085751075149654279056396172455199012395163729871693242379448221401/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^3 + 402418456641023795305323597536889325864536361173562513141133510427245286713142710186689231796079333545623190114673786440643/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^2 - 476864704844791501941324773333247462003891711075751669429509636408606945922532837740471020481780454158903718741239462146172/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y - 251004946419812328153266172861545063125354067891464724452417190069815435295339800985755981332456302433852874758447057089147/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292

14912726578001619622624229621000527398559634410742162955711704894496751741357354618894239523457434501883871024003466563338/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^36 - 15710508585597037186835536650112349084485329486398573577832352140925467888833062205168986252055670520541376823427311174718/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^35 - 2323972914785058459941984398594749662731395284165720142909053262219040551717871664755602915410547211724390346707336466736635/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^34 + 14231034304289356238510441614308823097784879408152980647749463920846757519250943592523902687565224266907812173069825457205769/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^33 + 32517114258055214313285437804846603758729897186314805509315477459284513665148411035993121854418342199862024424230250515969983/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^32 - 2484068773090207417295931934779186720242888337806179655783160261213068027710498207716823477659178190866846734104449260416627/34304575630863984914031777251923439374934587046233451781745697509422249025931695320537795788289819830686549543745032157*y^31 - 101096039790951482597110761638850307794886607195036254569008157373703604970383245860518968252913151593517859845480342185114363/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^30 + 3640347117587002912377654766022944146417597488108211853696324589210638051400952617064069307523800029775486432237570220558515682/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^29 - 908553065286492538190943877247247467899582956437150097644600220388647093802371926755922500062295518249808403622475130146784130/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^28 - 22072685661912955299454603947018315151407698232264957557326493607380807005480216548364826821451763441179680093502205400627164347/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^27 + 9127402623207183937439148491698002105803826015084566163259601584507776402342519914208864137745785894706711407393529903278050285/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^26 + 85670173007258411735084245792874310086786885485406673613223556623319864645982550615022804059857710714491836734231447825493249068/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^25 - 36929010851058252747021215927704150814124796064370175415113847537475618169337187595516415916446182152262829383661299538757815215/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^24 - 222587937741711064029456495094138454358110343288875207531905027707346456839664524570303612227762723877534720606394038109120036993/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^23 + 90472398487545035253007569440765635815496369840898234665152603532685277933678347337935396072281002800847872959446827343306612886/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^22 + 387808460212875941588360176172154815261168301608370428120558141370432179093661624934756403750822263477238406833741685508840711273/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^21 - 160416406583140252504173665514088368065868538038946164248052055593960955220117899317591465630021361768904807309702053458647732702/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^20 - 448096185329306127398683056863015561437458954397610736694483689281730168077952602702373767578112386474022962046637031795123743108/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^19 + 222102416417005357741055798495479802030467820973706261780642137775118428170997713367208148694318632217622877036156016109232069192/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^18 + 342595888572541650783991660797602649486792368508291409040217671982014341347201049760453335718841003531912265802741120372537518720/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^17 - 222075080917244234131773449266176397068382318799935042247330050402341293595593628828340931884120176682279747188170095260599471703/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^16 - 174350018002115274743821819918036206538207921903255665434359876373454387119857312079901705821906157279496674503956952293964151637/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^15 + 140332201049154966403752739538949797679416776806404249650041754196992982433831887222017333774201846407595533193716940569596378171/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^14 + 64223955045302285033694489311270773245129579687602155183292364884144915343307024179786155702671897912774043890436103413754062281/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^13 - 47030100810217720861944613476842664141035048969822174789157718044145347658453507266914269729187855360282322248302916706669271679/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^12 - 23874503583769376624919319942570278439568832760596120046273945279201271613074796578607381805436411008569047657306352818032365065/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^11 + 4972137106437905714232231965768246474434069038814599538338546909535206898654317371750492848630045538538487886441995048780971511/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^10 + 9129411569440228111228019720980671872539450680858357549089908173836150245214349483304552816712952382744705343821509501516976997/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^9 + 1036885869266508196680921372914613681798641294913576394384748226200391388020352115804959377737579583398626563541390463340918240/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^8 - 1604505292118008152290197373113604552299882943045156427915339022520054815117699189442221563876947904264967195578495676417006879/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^7 - 558570869356385546998237340974641564725968339577699517194464190371602267194315685127002995767239289656323614567064522965637422/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^6 + 17158362264858807599852862912987288389869930043669716771864686667079608365634650270027275598752878035993356865104892196179190/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^5 + 84405987147970415706239800722367311551264604654616694300834552970327108528607939419763785497470381427419884700516419049073998/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^4 + 18265472442725368797934552799382330096304816023385207155693747553887494416899532503975812936264211496455959667097212032473208/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^3 + 291281338496476543934025817652112151947978493924358787796413167776116526426668167393294302990667489662175499198254845372958/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^2 - 572108556585496193714575504603186045044023510432476958175536918591972072949735816565853385261825743625775249141400508449928/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y - 66202656886239028707249842370024404264081551350191357825514290363055712480193390199970418400344298708605204806751259175928/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823

-1534896578238320381338871272208132594622282592636264564228408296255927281846784577240582336045594607136765420197702092875056/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^36 + 1596412991915887750699864376756301185032076089003240892408723773696376416368579423012153276103511363473683874468353569060645/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^35 + 239283090113915784203290366756595539426465572349842046534653365674135594477444957712939634272041236039023748909734168644855388/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^34 - 1461575380245891102257213587630923789611687233450515724624942210882205676667824571302545027454049623532679616486491371906534927/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^33 - 3376753672626374639914898448488877710471104181798020074670325935501017249925985755890919075235729086792859478779002574876090059/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^32 + 255782550752648900441663848991964835434847208846966749394377587120442297222919903709577727959724211856992093857284787051074769/12383951802741898553965471587944361614351385923690276093210196800901431898361342010714144279572624958877844385291956608677*y^31 + 11040914590731931090826672762452796671068812955545755701974518946805779272037280422213487404428813401774245950201779132531137271/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^30 - 376021012492674672103180636762447986785089305540763435823171966808710328676667795673134240448694980026885534438393143439296704727/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^29 + 87660323948357844896427865671092286635539216149344493281413981559602902237977128024566571083578691972852265637142352903802377478/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^28 + 2288818137244332202329097380136892671908314303501822906847739300255507028663726204456257309361180267160405858354138893744084870591/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^27 - 908890201500242376860838196718066297903908196568815567435686213299139151438117937978561719976680158121222250813412438145481118111/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^26 - 8926301436497118606587191250152564235129408717100180185668052077661817840161672368752499923458456304923810089888569955820125731241/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^25 + 3697828644703403410939960404473053228112544479097333522470956387778238944283690003984228260053233657785535947773830789806751402579/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^24 + 23334669849325044298126675966210183562018510126459666344059670317462012083041901294729045004892901245214924215250308030695563043346/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^23 - 9069989554118806591306906370092119208463911863193234612283520909830022332099947075641864400610748229993960576224052938189062353081/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^22 - 41006250572524146626974242696332451939920612684126794903268856508059250105992528072628153898727993547795112527161464080950581001060/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^21 + 848708199553569422370022116102361814623557941687057602903550896511919223699748931385269888388656444137847713675679181728358111119/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^20 + 48003441594889230488822810312296379535547788850453162605366478270779632894282319344040026076389844216497283998075788804102179303457/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^19 - 22530991621652290259482747959811742416547929604829972544524378117143933651537741015391121202129131721496442792733292944897533596708/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^18 - 37463212946609276915673684082328745408318090909708215855660559247254899856749487024378986281773326148680202486198579012084999352147/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^17 + 22902190919233689765183515059900314355001949327297593622925607519537068715271607010443788228760957899881251889236840035656506202227/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^16 + 19708946665674196898916122848774341725673935398861797720994878940190146260736230432650777103896443980334973127576349491223413321245/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^15 - 14830728232999334423864216342367195462955101963645776719799561854306557272414047781718273646096129480520502368319154227222299124062/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^14 - 7575084906653517022683112780533736490004319938778333319005597922419002951064414152734707117259476366671125305283566408881829242892/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^13 + 5174303247246672315687041705762169720095024834034651638693540837755775447733123971051592623994286657360309629490751703379240741523/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^12 + 2810950312300522946970316320202917828976939911554012911198528711057913832139066165283880655572653665462541181997800745519930276043/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^11 - 605088168171219791315461656821616546260733156249012425373799578838089458104406304560241756253327312481191958274279345807155785003/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^10 - 1033700313814541071248412442559546687620105018592707854501959207651930399097144921177183801855910738474255430732451222490027076489/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^9 - 119846584035493983344898835729243729871016074116594589322838079157794192788539676771941236084001200675130188276352690210410123236/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^8 + 186826030733323329992962438955063292892276243807995264340549837321260899551003704672504138620788648099832218113573677883208776494/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^7 + 66476451808460411050244264046510088454559830932586262818459367944235204113540726919297366385777625288262430891704985582061720246/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^6 - 3183207559205541023358126348559722687242205881928677893596883342966578188653251746755467028251786731484554749402869012291838056/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^5 - 9849221876118480147113237009180122274737719354366357182924576532083621280402437000740969988859104406417170104496537680474897877/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^4 - 2235375086084481110271106801231351066616823841690562075724267646999975433468905438111718372157738340810827422880790483551098432/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^3 - 49404981813899895240451663680787711481360522781947476423863784088573263820284831538457941937151002230717422143764955719206830/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y^2 + 57263195191447561876779878881651002993486590412221744386151763181879551437061512389750228818834568501431255919717217874713331/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103*y + 7433891974956789272952141001393647901921328265973049418558885001129008634461841523999974346958877721331760681354582451750161/1721369300581123899001200550724266264394842643392948376956217355325299033872226539489266054860594869284020369555581968606103

6540765276188077064369526237976668599050723911106486417971673749453172159223285354194644181113996103594375560692508850345/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^36 - 7665790161491178868703695824125907155610975107531890871148014356396462497291568427657665165053880690694368146540195514419/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^35 - 2041213772239426818808436895592076594535803201042235033568501623868402299866497556549811883929988236623752205608482571755805/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^34 + 11528852042261552851781906689721838005542464855395609883879586664611961367162039543283551278476283119342647006383194677036593/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^33 + 33762050758582185172862858991782869239059085238775490821964821926416764811378544021621269377794627730501030226029108213640633/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^32 - 2059473093083314070356241900007711624191838780978721221065220593819584115215025000591153536447193251544461682956692189042297/137218302523455939656127109007693757499738348184933807126982790037688996103726781282151183153159279322746198174980128628*y^31 - 219880246366789382714174291387071270101904689595211233028519090716953352227196451299097771711067610028812999755749272396335309/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^30 + 1534796302005660711613227277219702630340526099444290755457661830446229541773334879570456884242198608703573356854509452676854295/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^29 + 618732261293297545494096577584535876265860191244686758476739143312929036586235844417267521171187806088046630424467933807113295/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^28 - 9423395918309491859469888647690515267794981781568283671397196407204520791316520811297224453840743489350465207667231035296080935/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^27 - 726877133711420977539142728664511993550264462397288884030308750670195476202682326448282553737395311216135702793565260709217793/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^26 + 18353205250849730599357126871540608444595588737642365378822089812184613672482639079235987481169298218186897036428442725445150093/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^25 + 841078356356014582009674900475459408945331468433372231754910476983297933743992435342422623186193179977092989751828159311853943/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^24 - 47250431715537193484169271133257959414762496275547062476601383092800343900413018219157588829341436618396661275586232751489751221/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^23 - 2035555618978790176126301925011569064637596127840672530211937874973138943921479404382626456434269369673373512018804128764751422/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^22 + 322284126060336710798843548592077373837579928084787797112014554662125311730357720465139031423582052660171253564015154937518073871/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^21 + 7505481338497067949682656871488560578119769534573060268105270669147462898936479255467864497261712563479566219950025676126295483/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^20 - 182762492647062785015774738817213521038560405269727279857936880459740248507363854420915917608039237952616829926816342746070297327/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^19 + 6889268311655353054115383429364737752556178980781176596299170775661268545901594038104148941665759505491011266094173588079998168/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^18 + 286028667373471064916971476749448815490596593669768243637251293719564003946957941416850209459813448609018596597255344284919745511/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^17 - 31178362673790728801546589623612395759155500060396276336343466298544163880938851105768492445866952595067443995736301079395591677/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^16 - 160229319911559343984669558598747655139898131246212074262961112072081220432527951341954735313999463559099939667236772008424467969/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^15 + 22990089324618460293915188733479804722317121849216264557434744000266331534873799903390880720990337378907506660976739195060815393/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^14 + 32543548014625781822061797977572444563882722831241937248598849910763414282829024531407626572304466957798111405391135320464768819/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^13 - 2154613027225404528900147730895739315194472682982338196781982151047643378750685399212167058351839478022707816310577521098851808/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^12 - 4905307086026473214375381309873005150132363953748133326004807621373045270089024062573774013797098091694090923159819845765100932/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^11 - 2520304344942084674099523556145614881069987153172266764705950570150078857867029736203407453782291537481882374901727109503514297/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^10 + 2060497967977396266515880574246035776332699142890416285518532605567454016108284369941071475890385396657429702541658278004313063/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^9 + 589193914930568942528470859617462044917678681915604969800695705488167193837250071790537986512761250653093285500750215319584442/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^8 - 13935279252630122114732316028951097602858396279872499661984818182053897242592354707375866764231047875144863986810020501817264/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^7 - 319970196458597515229175157200423689668203917568923049810550073134526742472156990447260923812498467508496274990457980071893069/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292*y^6 - 59202670871829655569259105378358912310057968244975784803172213979383420005847653946737215138197981997435335789744718192997915/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^5 - 737530078343062559185312348910431769657124803655218184923589527663102853857300049646350893142824447465523355062057497738935/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^4 + 2136514344035953369924129028869441541640992659211779279715267203956224461747463363709946273907564093469939224671505704941235/9536672025380187806100834076034716146231815198852899595325303907619385229209011299109507229144569912930860773161118939646*y^3 + 159063736502603660750770915145217951737320511006991233826165034221426910939725969898821342673170206452614238773951953802593/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^2 - 15349408586038890934030463091166807670789701633613881569089422043176307587785456371169513728802127938848979788532414608665/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y - 16992610712938408651170827959624512974888674306452758386019060437919172836271469372611588635182445135162699816228217091517/19073344050760375612201668152069432292463630397705799190650607815238770458418022598219014458289139825861721546322237879292

77724071682949255707423933555664634186437910435619663808399239420077369768588075502995447281286046619014900495538068256917/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^36 - 59691949433510145928900634548431660172599171015983386764543128382321377448932549886441621294381563097334621364449258630809/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^35 - 12124753076537337933704424006335195632324792145780886855391982646523770368734665222607517326758187082542330101043841327725267/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^34 + 70709042619907333405717839840361631844236363865650204747859601164838429764091753862464441757840554071505513299890368736423419/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^33 + 188933868348514322915858754989122734346804300044479842643326388757890762110497109170108361498060437510093798853927008457226449/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^32 - 12531628668370334322259676729611525920930651715186193013512875494710301708767016326396443153391286934324586131106867426030165/1303573873972831426733207535573090696247514307756871167706336505358045462985404422180436239955013153566088882662311221966*y^31 - 505074978170645052340947565776455678233286731054149896709325804551711375004908044547521727423180750715970732536300160133254506/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^30 + 18588200995354065752707591063165269232564194902707765677641330522936174984209092638591500249251564400109606388359697436609773417/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^29 + 221721908320882037487527126976270298573866198262186090894777953937429717213009452876779059037368151069266633800170857420802705/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^28 - 113851258445685717995544227768449672285742578619780248206823117416634313107011259975161051903600872990063566459073553254068470537/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^27 + 7909106622356219972580282251687916535897563990914993850124514060099979091806317954882151182393172724553145870937533157963916243/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^26 + 222172473390426247724666620382167428879199390358720174854303424097227289662292195334628765551644562723568595159388052940561924699/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^25 - 34559131093867070622475671422398609332495382551220949284324973415546782792323938630065040885134943997276422240261536429804196109/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^24 - 576709912510128770019660337685560229908782618885013443575205717873986132411902053278878892350332048416911358604204530513945184550/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^23 + 155476734271961156159802836792243979917452291063511182922286335479686791353846294722042300785025131954372739307941654300566723433/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^22 + 1997099105192454316735713068272420031918631128704660393944715524678854774861198176242780996200663891757267393613205475637681618031/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^21 - 7932272411529269628865065127150623792511231224994269895014225964171226632391809244862326746612771736250679851174677012730908259/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^20 - 1152202785931269221065016160714056160851479114823311232611947200381923779416228362993031315769068937270273902495463898361960620758/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^19 + 558211194726523306840841719969071062689729955870082336671103295265284955217604776190668586581379729533631266321303038370731182735/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^18 + 904932918479282472931301406568595554208697313701256798054300572898463992015631181313111706421386576930860536708073077454097103005/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^17 - 694402056373435986810002533970521367597894756433733344084764179880375427451908021370544217725812925903917917298333412580006015187/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^16 - 496646071001986789533552758617999668564581848350728469081415617729476980336664353444767570117431778393927675244565260880869121924/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^15 + 237394807275641564049881576547176718170189525641202098250800837816271874615770478816105984865608287282527391742093617250118260114/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^14 + 198352270520383580591803391856368707855554855936982242187398990397498901455813236635592820476287859138156231091798040355568726956/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^13 - 71111437095841785672877640028878796784912865570559247682872723024814554584219638703866187930016912139379434161004292428224649451/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^12 - 65204809219061959350963488770470157814142374814227037766061286125367631134817522754404620885945964909025220566347172487091540741/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^11 - 1979191445760037624297087087690881952469782613322626848222739061728935188328328911545787971227515666475761613226406298906640757/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^10 + 18198132119610007440434971265189155484866276905117875294466293481752462761105061292759127762889798105288846124801503139052120463/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^9 + 5434814415194120269549403406851249222518596247452688678279257132250085592296793797573298371833770941440304520968165951366422813/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^8 - 4145383977795223530451554205173926080128364679000448436719331041420980101606160258362774198644422441721222067944254102728373671/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y^7 - 1263982297173529678540982155507369527915781509385540852255322118898658686285712441421006800558862873845761913292869758063545296/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^6 - 182216534418440786829779690238515052002106311417535548203658557918903112583136033228026371084536997263534185437951769271108847/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^5 + 92509100625194848868641720142803047152972429748255602732321166889483096258395902060794742795856015306906665099432807415660682/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^4 + 32328216753827450595100813744650119449094199113468908723507285719456225553424743202732438149419404544366411926613394931242230/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^3 + 2823597812941468154126686456868586529509328228613214033752789588848600734189034695265873674479316303160712530166161093627545/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637*y^2 - 858411811634310620560644171584220920181554218549732849343086611924317625775364832278650360844735935043480820907344812456999/181196768482223568315915847444659606778404488778205092311180774244768319354971214683080637353746828345686354690061259853274*y - 83559040322492722631036901171293894007391787167253017158266167040131898026430702358239656126136681245086399503242026200349/90598384241111784157957923722329803389202244389102546155590387122384159677485607341540318676873414172843177345030629926637


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

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

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

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

# f' Combinatorial flattening
{3, -4, 0, 0, 0, 0, -4, 6}

# 1 Loop Invariant
1359252300752727567425966692831922505505806487314590501364708138925171783040335264594529619564068092001697040198697291252772/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^36 - 588543543366178896463729503986087619170903147533967931131218214804223842960775471092859465661230703246909686165756382566403/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^35 - 212199063578027748809939047708930186210708619910504088474050487165376654957197762669522975037200378671235529196771852415407657/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^34 + 1165455160628214887010012624396352731704953748736811410762284799505220747680529229668490762410103764367453897058283561338099003/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^33 + 3688631795712911011980449646694240181251102936217143529987941519972017572696677065423579247725104422227921265041439013689416401/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^32 - 210017438581062392290267249502800812334976046461331561970486483273832298646493230704328190001774270091952325927456478474371318/34304575630863984914031777251923439374934587046233451781745697509422249025931695320537795788289819830686549543745032157*y^31 - 27353390764845219907266322806107187743016534982530647898012975488114964285249650873499681332648219447912627216548178947660584160/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^30 + 315063958945725825613978327106651537447979403818055605382597141144026350386111927878619818532875874585886286384089550275730052582/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^29 + 112812466546055744467667229422990429036966989526774854520861992957970410459511922384746390661708946495774490860843019097570376790/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^28 - 1944265978880949308712125022552525264510606111307730231820440022360156353324555356907179374299883182547177937886700882942855506959/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^27 - 374481923317108473685733449104208382121289815567813349542422941580033433967083660380954410248167210697242820122153391976494810655/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^26 + 7590573342242942527546342249400007738867615655052246010767653201857972818536759104945322257696065787656130621649758405957719706013/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^25 + 1341641965617103930530841646255016803712120758438458692490363987827150930564524695014835607923179139484856917987580044327452072112/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^24 - 19509776831830726310993442197417318741439724867283195832648304032780033139388198681273414690805257068833492730617558992365656377069/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^23 - 3849592291247234701311774874134175628875375972168357105142948388461028592022095452797585901797257240039047787503525215868461914178/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^22 + 33092055639384945810302869429447658747023157005370173533201870394744981901790717098322628113499680226104495259631645976893362440671/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^21 + 5888667537074939257766440486815364659914714966521260032461988837880771691395685542738344267795021470509588698225884414478755972439/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^20 - 37401337787362172665730696438255760949369108046537020789920039156645763090794908567218416494821176781920077870676891173883635983492/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^19 - 2914943865492532571592854226650890374357856900856564763304494053784978385091186668923170189530135122250956537293685210164912035091/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^18 + 29633240931831671482857104236684414086974454274458156081208341655687356121670700666921638443577903692576195113120945709114596750373/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^17 - 1940935774331581916344898034726923847009417159488824801839028280135518452489524460953988881524791711896356606512092194859256880133/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^16 - 17232276893876906590166262199012585096988587581843886105381181300809497939757379744994720280563292559759982324549656617135121041979/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^15 + 2193888045580335089711744746678904022312482337878060635328416795120013228762255911390384470334445455134489382792471627631275208846/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^14 + 7263734334593215934413335293505487392207011377776598613721486591047144388532391181395178565129760396290117427932804224934770958356/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^13 + 167531839960369399045403326981193136769161761428400958021200471465884040273448624521372372888511984009509889226794719097001856880/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^12 - 2076170501239434931062145191295517731337195222364452686496593526381732067275368813656871362086940598360242615512103544950955262491/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^11 - 825955177064288220227083158899036808205306896313434712913063367988401741466172046250120144526458229825010875529230999431718147071/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^10 + 316604465579918422979975666501636549874133884674713443820190954438508587257869529447242367346414621132045380217046788259839167741/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^9 + 293130326749988495171001522743804249853510269722312936923094489087820944394213311790580122689914852469167418560520783819091456062/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^8 + 36567742200066890585256490053183257880426905626213275935470638060689056832968650378217147769477920880259769086663508984895387741/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^7 - 28166123854449567268882713809552775637189714949817168704954196972484045156804134778794403307791074785947575408526337812106928081/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^6 - 16333476765459597676390165948501333935275975350533198344555269861366808233611359470610611199956326823635873656505051707081310775/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^5 - 2743756431257989129871531815466420230664592409249251632421471343963379789148758011236241450380257841787722204414133186044315257/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^4 - 17062533209216377685690353857699235722087876529943111022310329165473876286253706907467514372218787939998754169247099426730445/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^3 + 51655391255668206578518866965853637108018102637184288633166224560885854479029715886603361882608832495840801022440603779877558/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y^2 + 2593133667180509554355752539534916358144142299750226573601448217734867079681500448208628463230395370819835023032131761474435/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823*y - 595827249464469743938025978700509749144356469230556833984340957567433480307956475566866050925684408619979021316121214484057/4768336012690093903050417038017358073115907599426449797662651953809692614604505649554753614572284956465430386580559469823

# 2 Loop Invariant
14507824675745366449772987520409878399782949807319349253326206792701322843510800081217589378823991787399315502850443800329145971499430551673263729463651889242322614154617790971493662444421587911270209814336026807336428382133439000867214663212995053007/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^36 - 3037646074687073904470284554725402659975018296144762435082085648997931161578971531225782465202640501867924010908425837002588909379468756796960896767266464906670144834634127164320287751986907730252528629826396205315974358580702779987375667657652994057/6463605202772623975818739648953841016248311219742138256355139334950291630611775870050228162056422209672564431532997969152965907015662145221550189613140692901431259936920086308999133997472637707838010948543813913072106344436332031682046983140274752384*y^35 - 188307404618684993139153903180406208369604486188627026505931306090704155791930284573029796022804196107572781545561062868843975123998239052047453880884957529156977982415541220278764981943509925354148254557232696806189518481457961602355664255405651758365/3231802601386311987909369824476920508124155609871069128177569667475145815305887935025114081028211104836282215766498984576482953507831072610775094806570346450715629968460043154499566998736318853919005474271906956536053172218166015841023491570137376192*y^34 + 3575996077970968987574553510715810388633191530525956762882873599706913463009958228687438072050468858298509955301130995389379012596234960563355616119240246010490676504929557367205241629047074465659366422787270777704128240717757132800653594640804207872621/9695407804158935963728109473430761524372466829613207384532709002425437445917663805075342243084633314508846647299496953729448860523493217832325284419711039352146889905380129463498700996208956561757016422815720869608159516654498047523070474710412128576*y^33 + 4854271496119167939397071246376370980544485533862112276795202837507894010349856090860809463057223847541068021265272757528287793635167876552260250163308239224479335446224664289926353607141666792690047934081774569603035903641157953126080697186106264736609/6463605202772623975818739648953841016248311219742138256355139334950291630611775870050228162056422209672564431532997969152965907015662145221550189613140692901431259936920086308999133997472637707838010948543813913072106344436332031682046983140274752384*y^32 - 309329609534015920228133545324474064010995332737089019926659001618814629190536416216539828197507370995319411653816920150420194128033840378866448710182996482367096614518620767689715495312240250818693945895844814438813541220676942153758625196107465804995/34875567640859481883914062854067487497742686437457580519901830943976393690351308651350151953541846455067793695321931488235427555839903661267357138200399422130024783832302623969419787756147325761715886413006190178446616966383086501881548470181338592*y^31 - 35387450829231681206892013625378138323298354140723207091072351202689617070001605335635906539370073444999600941326882436775205257640476614544811345226961998463260202401281913332746856717675731418885571919061575294650106798895548168401466276549994873141921/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^30 + 3602695509654763129779259752202304892322277046968109035930003176760813510630437276473403865730810746638188245239957990245794039118352998781508032149397556287060269323155910143813615337637100530400641190529774811511522015573000350544476032144639817677026819/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^29 - 1564561640767848264261151377810554604371598079151395759612279050135664133601177429177388928146971286803322869928261214995431729307300891397213055311474821333819817898883370303535409983253394691448618273831195412361498354891620064314140838567253940511678179/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^28 - 21738801657357328402499958636301156399811861825838778173041204238282617511814476827109555429176912646262946462455387461494996270920927166780110980701831891831124003935209660446132492198753504746614280850798090359470669738373950065766119730840781369409246887/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^27 + 13086304842802280042741144044802218743465055416060598012560901879051471984277076968341423017150161510133458963862626544282384574868632066750973811889028680652749092233384438635327360784595421527650222649272994511887445973759576762001480241833555531092480791/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^26 + 42142586107481293270104550924824562994687537997188376484507943438464848229517696018980639471753084193606210241546110900779538341740517098483336102709715578340916911923462316166268367726464702775213060035311260265413190886198536581576559686218574348637763531/19390815608317871927456218946861523048744933659226414769065418004850874891835327610150684486169266629017693294598993907458897721046986435664650568839422078704293779810760258926997401992417913123514032845631441739216319033308996095046140949420824257152*y^25 - 26183900948690018410842889603991363175031115114833919593164978002735662783193632340400539785622362132277647504197794509530514607665173974096027012643443165028905703677892880804356048899520629262494433534940043842597722094629586600992444808486800753912730801/19390815608317871927456218946861523048744933659226414769065418004850874891835327610150684486169266629017693294598993907458897721046986435664650568839422078704293779810760258926997401992417913123514032845631441739216319033308996095046140949420824257152*y^24 - 109979565872071460185367104477392734367167987487690761378138206837429461318533444383100315233526618950028515470537743197778057341685321553948486749442256458163280611449281013632373900934100909588974294805455967743263328542581159551263302932003553086359738035/19390815608317871927456218946861523048744933659226414769065418004850874891835327610150684486169266629017693294598993907458897721046986435664650568839422078704293779810760258926997401992417913123514032845631441739216319033308996095046140949420824257152*y^23 + 43433241161155689203586555867011548180930937779916573083611674514093846654003424857171087280169646858431571478558292349002354309938455633357317179740952348916681977992557189700396832518362329499515549348578447633611511408832128824963334321569376877214009861/12927210405545247951637479297907682032496622439484276512710278669900583261223551740100456324112844419345128863065995938305931814031324290443100379226281385802862519873840172617998267994945275415676021897087627826144212688872664063364093966280549504768*y^22 + 64490150261248236502198533494984006746009763951378546343895782496821028895332529282856281177356358082894370693107137603031419185795276323462583957775343917776365703161005755732036254063614477433046943868841133167745325555363571917001993536495355280566508593/6463605202772623975818739648953841016248311219742138256355139334950291630611775870050228162056422209672564431532997969152965907015662145221550189613140692901431259936920086308999133997472637707838010948543813913072106344436332031682046983140274752384*y^21 - 227803971714969103349766158683670289102028223567754589104155343719028932106934937614066538430864668985221236067938306426070761185432250501351365362050074187736144641180918383037859946747957841698177799476501904280198213117812628871170875469225238605136262931/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^20 - 28186613961615846380347261797524910844363255490379083245863126067897219510568438350107555895979430347357425610263472429864840240352718188670178999389305064195983325538294949491985669439106916016410983446827776268693376526578346149514953252274670258869212087/2423851951039733990932027368357690381093116707403301846133177250606359361479415951268835560771158328627211661824874238432362215130873304458081321104927759838036722476345032365874675249052239140439254105703930217402039879163624511880767618677603032144*y^19 + 297261111457120170858498745215948905995020509817920255510399416941851588762529724397242273311100352587135035031157439654837496068732836718798640096334504889457149550962659464023201912048569406822822253555510403353245780331708200322479769170022967851479585589/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^18 + 114095364993917606599538589273861974325423604321201432040449535995923895237991923522500220434863193280322233187431451580758543133432094550263444577497723953971370803326575613663770700499752072642558569947216699724366967858708299592977168845326017581635459031/12927210405545247951637479297907682032496622439484276512710278669900583261223551740100456324112844419345128863065995938305931814031324290443100379226281385802862519873840172617998267994945275415676021897087627826144212688872664063364093966280549504768*y^17 - 93563728367919322608853049957983613585610031833795626995484386741343419813062060041371829386966093409387367741275515041981358869283052436686305690023464312267787522873406681793629304113340196348677616575217759354699077719668780971705763133981158671982093285/12927210405545247951637479297907682032496622439484276512710278669900583261223551740100456324112844419345128863065995938305931814031324290443100379226281385802862519873840172617998267994945275415676021897087627826144212688872664063364093966280549504768*y^16 - 167551808552441941253903300828601458508843472371210939187349002288761013602266632875515709122020150973275513779571959552917935367963577590572044939059161133928022779270343383463169933971074991395726514329966844439684632877633110423849552704818320109444100847/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^15 + 10906608941873203716529289736044288809828278034647978322054472654923255084942978277485129953426600616360062594276375899986313067699435923483984793178005781315883132013075326540235177278462222817457580066256348162375527203183001996902658636383089133393033505/2423851951039733990932027368357690381093116707403301846133177250606359361479415951268835560771158328627211661824874238432362215130873304458081321104927759838036722476345032365874675249052239140439254105703930217402039879163624511880767618677603032144*y^14 + 9822928534359486235344628151554356257583512582429005189234591615329108361024845765563155368491623401540544747996187742736607689466671674038289273461208542193309644367896513146379537784197504864539852143780900772230046123626034605794784943843241779700840789/6463605202772623975818739648953841016248311219742138256355139334950291630611775870050228162056422209672564431532997969152965907015662145221550189613140692901431259936920086308999133997472637707838010948543813913072106344436332031682046983140274752384*y^13 - 231183601732560573230236720441979986735997464545690474940905846455378958127476529499939671353600283334413967819595983278353974841030966261345648414431716360482627858362251647928199566204381546778228060656666300208562834411327258911993415314846473862838241/144707579166551283040718051842250172005559206412137423649741925409334887252502444851870779747531840515057412646261148563126102395873033101975004245070314020181296864259404917365652253674760545697865916758443595068778500248574597724224932458364360128*y^12 - 12045665277896258538031785815022864285921655020264665397254404407617036156014127597202591620351363960815362515536580378878446976001879401229117189283888605247760953065503142385740874666019227530469474681190397428064647146763986681907687072808851382977375943/19390815608317871927456218946861523048744933659226414769065418004850874891835327610150684486169266629017693294598993907458897721046986435664650568839422078704293779810760258926997401992417913123514032845631441739216319033308996095046140949420824257152*y^11 + 789137216492102596373854853740059693515724029161120706512713666585555312579807820218696049678388957554646915584821226802838939724003501757408422894073174750512351994695660198794812868300245628720457124434290779613893287360566183128327920151219191003629983/3231802601386311987909369824476920508124155609871069128177569667475145815305887935025114081028211104836282215766498984576482953507831072610775094806570346450715629968460043154499566998736318853919005474271906956536053172218166015841023491570137376192*y^10 + 5419326693007881741198018194647751649836670922180947408189210182550030162908834522721950075529493120587702179807458475303233317210828997375477892780423953021564592694022625625009728810783971724456224716451736468132475830373466430193728630150201127054279271/19390815608317871927456218946861523048744933659226414769065418004850874891835327610150684486169266629017693294598993907458897721046986435664650568839422078704293779810760258926997401992417913123514032845631441739216319033308996095046140949420824257152*y^9 + 168037301870275515807572371869808353868916941572606779361094147475590896246838970457590954688690827634943189800672297392151312043419615996778588053997117766847552091360863569047153818415126409111849403253584865467080653172565702197834836743057012887727727/19390815608317871927456218946861523048744933659226414769065418004850874891835327610150684486169266629017693294598993907458897721046986435664650568839422078704293779810760258926997401992417913123514032845631441739216319033308996095046140949420824257152*y^8 - 2240979660703814238823739108353461378417657574447250662503467979909639805437878845042273699300136183177548328358596187264201830142010312448860526812510788997679080270701771777099755684912024895638408076669508420350381405221815182491560506669159007037679263/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^7 - 637926448158354031756199931568485374976632345832260927358834171912730219361207238941928006437705074417803000915401678564359995710628986241783198156053760323060752666265074432658729177065495082037140755467018775755438181436145078724718951689498773196050937/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304*y^6 + 20560319102740463667946922360873273046124379924241267962589385074106305878407341750225988655556496695451590198225731045258988482604260123172424711595913159992341736753413443815612361142480944333404561554180162191363082227936432838143831423373152436084411/9695407804158935963728109473430761524372466829613207384532709002425437445917663805075342243084633314508846647299496953729448860523493217832325284419711039352146889905380129463498700996208956561757016422815720869608159516654498047523070474710412128576*y^5 + 15130603626933507869003977518104989879984090843333761170568517008354514241781506448364493458568406065048922796203833929277404660369178922341048136246026030344077642048423520585857073696979860691440378671935176763326360122863621075641997209819080962751979/4847703902079467981864054736715380762186233414806603692266354501212718722958831902537671121542316657254423323649748476864724430261746608916162642209855519676073444952690064731749350498104478280878508211407860434804079758327249023761535237355206064288*y^4 + 6096731953341522596311527207859017445400895648498458763338346321206836425422854672656806377738493371593028958813731259374849102573423994865026192419343495299225287030529608130060322740531672725186332405055099292297636174628304012287227401707755180518845/9695407804158935963728109473430761524372466829613207384532709002425437445917663805075342243084633314508846647299496953729448860523493217832325284419711039352146889905380129463498700996208956561757016422815720869608159516654498047523070474710412128576*y^3 + 7212766884460288778555256030895020012375808597219527136319754887164587185922776697568639020440757092275499029297025782372478788191812717530017612918106297937095712227195231587340152550669625925545491661571998247225605688573941930051882162566512234499/3231802601386311987909369824476920508124155609871069128177569667475145815305887935025114081028211104836282215766498984576482953507831072610775094806570346450715629968460043154499566998736318853919005474271906956536053172218166015841023491570137376192*y^2 - 262877854414963057261404139328371766854762268251728426773602356950892931791581755211105509173550893607125947579668075518412847704305412447507286061176471879451848908923410765690148813082045398226454474107924270284405210488264979211114241210832652542379/12927210405545247951637479297907682032496622439484276512710278669900583261223551740100456324112844419345128863065995938305931814031324290443100379226281385802862519873840172617998267994945275415676021897087627826144212688872664063364093966280549504768*y - 88526808085556503720503685948180249037297935884238962569845269132444397001910769187126294492755671672549351623630560470127249736469905355313878275192215709932380877744465359818363083277532951375442147766221711008042895626681158787229597393623081235489/38781631216635743854912437893723046097489867318452829538130836009701749783670655220301368972338533258035386589197987814917795442093972871329301137678844157408587559621520517853994803984835826247028065691262883478432638066617992190092281898841648514304

# 3 Loop Invariant
46578671964977077955821181928732030264323821891696949302139665932115542089814471104476712846207798390794059150269445076898280811960074913398153810424282738817937253163520880192332026290359473757981411794253405125535570347102692669479811552022183580894114109611124888159022399145749481847830016858371364825553853411/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^36 - 15298940799046210558643916252404624800720719625292320714300390182401934569734284698592363072524941693974804140387019876972412665277222908517506273443858175875889616447076768987463144115249476171275118881822242897709021570957388243509854743281666506621562846055216631070997465352281857260578986240194724204562389021/168272756575847548718260381943862890721936889810887334224233049025211416408159525880116906541405270030352695299619944559892704257578567606178481870102656092295183282989210628785936146868066304366128601890837054243243662521316863284890381719477281653004927869897794148491729095506686020237066222117363901519376493568*y^35 - 3626510913545376449233614109383296248133864439767233474218553998802020901135755105473408037674907655621294338598028228478735910696117236520217503958218513036122011563933903201923341092752626860605290739125389182625736532498350060617374535327392783200751826851256635768930566018620976168115952355297645979114970579453/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^34 + 5792808983265262701293530979131285844384315611207709757620863752115253818219254800729911803078445061364837542667374871853214221885395929577770184919465171009824999050118639183473211116642930923604709898083573990544120450113577454345446658235530585912873272724064932837234779115962682590018150530137377092942328155279/84136378287923774359130190971931445360968444905443667112116524512605708204079762940058453270702635015176347649809972279946352128789283803089240935051328046147591641494605314392968073434033152183064300945418527121621831260658431642445190859738640826502463934948897074245864547753343010118533111058681950759688246784*y^33 + 45547589711730673633394592192717797476112195562832663311237718069568320260334764609427538323821661335081277809264869895600102433465865050459821959603718054008556609333047289921875452843968399813698808058746670487257938724435299635246757410248039558241050455956669601718839514982217172592032699801092907340780822790049/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^32 - 3996473022546029899644925768984533266919933245453556883026214785471169402258683882646946559922871189436533995551869169272580216222339116103661355078258665857962393911913628245667752783987947554117786688659439533713343785539572282494702127590765567037575925737052335197376166884030171885954471938332973152375542726249/2421190742098525880838278876890113535567437263466004808981770489571387286448338501872185705631730504033851730929783374962484953346454210160841465756872749529427097596967059406991887005295918048433505063177511571845232554263551989710652974380968081338200401005723656812830634467722101010605269382983653259271604224*y^31 - 53850889244004780449654350878681810672318383210773980047548052899757169942553397720443325554865778273769361111733147016522307438770156252041614791487470157743010976237413121905196851298618191254222481072958337932838297271107235422907747476976115025831402880621466050172706427118893048158445951423371847712990105757603/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^30 + 11605073206240921647149290489450477067041827706743379056073643584998980729519825109344401193163401426753387038870593786905017324680663254902379830470144710628055149700378647675432192962777719861417022251663284467248242021750461973704549434546615831990885139925114983224887218559857311259897038120601202214628478167148673/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^29 - 5663607361674034887061607869552592152436881515149845306711129195162834373883715381781456507329002079864267024990277082105680237164720353099195267536317752411814871371203023179006497014645012351466615822170774564370499922654320406368799095652169350268955122326731392693755414223928842718101837285740792356640753598269799/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^28 - 69846048157437910391560787088499302451227335082279711430982832538065633453085989507300037694943038241314988231538039153358385197846801140215764154832684963889607284738615375103841205524551158647845500047346840504911144055406376071157244690000495822587958442417440551378530715687451269111907997749836514559193643224820673/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^27 + 45954140106764588662548863849044308247479116311769716110579094909441438298574606643980856649397493693723786887016857082752751627568499188258392884258380642697248428939894678012497857114326229291670485473816217802803804985993737881348500315620747187118219542082132543941098031725589679217374034088028157346798411878573965/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^26 + 16892493726341392488563909331428473407343120042518225231841077698866615812451282061832827646942921231350583337840043029669414952501241549947093766600999990990202638957951694503590475499117816156174789541809500027392202177647263487928056496081442806477029407828030550024385043444912713701576449634960153290036971731782949/42068189143961887179565095485965722680484222452721833556058262256302854102039881470029226635351317507588173824904986139973176064394641901544620467525664023073795820747302657196484036717016576091532150472709263560810915630329215821222595429869320413251231967474448537122932273876671505059266555529340975379844123392*y^25 - 11472915337395094268570174122115274457343774344273157747387015193348878675719789832767034941559305876008888969675673931972671246913704699357351702111936030339527567568403624021491079666466458286087818903950789218341274860075999520240114567372079436969312517660504124123888855433576920159259994466435070806676573046311843/42068189143961887179565095485965722680484222452721833556058262256302854102039881470029226635351317507588173824904986139973176064394641901544620467525664023073795820747302657196484036717016576091532150472709263560810915630329215821222595429869320413251231967474448537122932273876671505059266555529340975379844123392*y^24 - 88083883800459859330734621088292858262392284395422636635065119955769573375087220504536233692605714736453879837825528577149973080597292064411252095804968364980467144326745124237917899757997245925755083186146984005376488532109269362705480054227170543245080323086931534696217513269962569018488382482990250848457132546564199/84136378287923774359130190971931445360968444905443667112116524512605708204079762940058453270702635015176347649809972279946352128789283803089240935051328046147591641494605314392968073434033152183064300945418527121621831260658431642445190859738640826502463934948897074245864547753343010118533111058681950759688246784*y^23 + 458536833906711006189147637455491800765485422574774320045257633082534965284948062327208226391596231823164631347787247763244686823260145082913746888782551110183549509788291712885510625136409165245937358113392757605561778422795212122853749737244779821051968839483579810152351337917022985247957484530609380203465598001182085/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^22 + 619587291268582178028913504044583557778689412379966630527860964238640267439854023773984958696391563646885866261134931773630224348808323194946643990088853377254162185774248764445403677502447134730586131851784771289421932654554938918872369362860342542306058377960168129658447036592312701786807561689815527523816786796847703/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^21 - 801195849976160626159907705795187757075643777752846922122533754991780643046114197161786509830602943188680780645707404442964811359889485016871982883897806145320867709341482905835947649486445362513124877655580225592940861713945416197542152328356004439306235778978820841735266725788858294376102210605210306426382684624538587/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^20 - 180173584678225866630146572769967919459428074006727541054588024035086325824663797061418768946188309585637228864705029865266849733347621161262233475620543314212150879411888982357023288921916380124836854574654620436477176803113986021444176373092029797754720464092368242670491796336702841420586899418156349689347397852136485/84136378287923774359130190971931445360968444905443667112116524512605708204079762940058453270702635015176347649809972279946352128789283803089240935051328046147591641494605314392968073434033152183064300945418527121621831260658431642445190859738640826502463934948897074245864547753343010118533111058681950759688246784*y^19 + 1035282383607308407582254762920785279925894524299207528531823250828634516769198827071531118501766471535120176522989082578624754840315211220503202610634536003177451525795535661983602511114483211337096056693172000505940846675656828643449467382949911560500304072155397613689841662609157007971175843184641112344625932662978249/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^18 + 1083972182948633505821001040476464293975410618741503865356673973278223588034135234468557220295286851358443565368951351100614555711647420594739663335714557233157740988199385904883502017221879887441593043163643245801857425548924660676936569521884055852491150080566488445708278265926829729320081121297388505604646273165702179/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^17 - 965317217948442431991767767603591855305692516187354582809800410860542754247551477708807001283429802601786152924400468455550544544136288716448072805997166203264601709319492849999494671977386372182117877406365782618319951976510859089720210365325599757913144127077649690750144943554461969753750782271707279683289837708632447/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^16 - 516967216782099097043115865465995514959256985750515968142372632877720417614845214602854869256644608728416914121776039845810336136913396196409437829485133128194333807434830099388617692220898693954575443786908130405731007042316460805004859082221196911828233192699148483433793430127494343794356930122137537253514306227752627/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^15 + 149031757467424946931808024952687047897082082512810526194036019485625333913671323926258187579052228362598147601873039394849087729588914058204521099042252875255350450947224885424676916834164472548519351100449534875071012775065221615007449532721027751408089377603726352161622427269933844731451979063287071824043137579889697/168272756575847548718260381943862890721936889810887334224233049025211416408159525880116906541405270030352695299619944559892704257578567606178481870102656092295183282989210628785936146868066304366128601890837054243243662521316863284890381719477281653004927869897794148491729095506686020237066222117363901519376493568*y^14 + 87098302563466539723292093771729684249560818499815892808902488297941547952607389638357611663908407244005578598492722208129718332632376189810588065057320916281152601846667071570903137220390939969051778597393330323747257158017858308791156308528226579290357231445539038194878717610819316940597263312904313836865152151892877/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^13 - 833865785229225886879853435973456929857105072227955845941856901782635003860746388701949672285177055388400463494666009304386225204163680728952722481908711788210982506710118852648029615880851339060835578466925757068508995977103519287427970316651778782554834196104894585012599992478352527390326760623924382092096794498927/2629261821497617948722818467872857667530263903295114597253641391018928381377492591876826664709457344224260864056561633748323504024665118846538779220354001442112238796706416074780252294813536005720759404544328972550682226895575988826412214366832525828201997967153033570183267117291969066204159720583810961240257712*y^12 - 36463963421405799878426770959500873828443445092401092824451795642568543967004575468220630511664564983213952626228972840103546790144512165121191558264335343408654150162034956348154321020541366374120850629725636455822765622042127321254139708354049743729671799551302789264202852683528290508236128350726246668942528167255845/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^11 + 8753194368346412234170161792358613354799900053758627670253505726049107597166814137494768121483716778100840259488055118565484024882744634413205209045910099349667493098288976153856251741165512749527817577203536301301286619486471430909481926251307571392689161165493868036396693567854400601205124055199776213746074427871869/168272756575847548718260381943862890721936889810887334224233049025211416408159525880116906541405270030352695299619944559892704257578567606178481870102656092295183282989210628785936146868066304366128601890837054243243662521316863284890381719477281653004927869897794148491729095506686020237066222117363901519376493568*y^10 + 17559223658596865486569933033993420475158118294052960372189702589999774791760448819378235596769947614249126219365085344870679905546047962280738936583746122536786450379587933211932729999150198463320047208520517596070478771676663394139595139823198056156094609305695513098578593042082687039150885664042599705039366928029675/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^9 - 42758392419044252532522598886640216717036051053217172038327994359339836207874278429976231262015133492675183759806533090633437713001856874667953714510433376368120669978436271290393680061053642053892390842691069619519223011664534619480094124578541538644933070672904687377540248101959061913090107204380367263389710536201/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^8 - 7615064291414700693203237512417424357898924548273683402176817024799373507839009953942262291108815872399933717629003588709635666604622819921112792925572015874540916198185813096881023224936740984105296622632421147612814354337138335525586311272178217511652477665113792940975223767869077387823842993010173583757213959904383/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^7 - 1932890837640036625367674487326549960214972705926395331153928052264361999827747225386126313649306765374637533033584065188971910907216416717626310533260464496839757337244900713191379243360593673141386677785944043170275854856154889588167992481394761297154477179915736976196218320428779688904762229145699635304046325648123/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y^6 + 21455776909189588634565081160064839349381636323216274155286130719041780947633480925276424454341467318436055481537921358137504034173075240364620396442397943941237446051085333056706097987396483855506379654155667158609837372531610393543272534479449275995112132172354406065755727237040835887880365153515501642662574241029/42068189143961887179565095485965722680484222452721833556058262256302854102039881470029226635351317507588173824904986139973176064394641901544620467525664023073795820747302657196484036717016576091532150472709263560810915630329215821222595429869320413251231967474448537122932273876671505059266555529340975379844123392*y^5 + 200916458659359087027570900910017565636461952528398763816205742482081468225658546785541205737105192808036243853723111714058632485057412115714638363937915291724701992947706862077101369820967219485214574369841570399716834628507277329499017184313375298974620843843581519029308234708135683075031729942470472635493526703983/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^4 + 18742718525448156173681176654376182328649387876449038066792445624811036312688615701694511717287785658678117862366513174225919320146077339615249569200015856677547431125102466261070740234946913889225217987139557563385882251482000616320370093315760405541817584788661117760909722685600946198286003517076813253252275219459/168272756575847548718260381943862890721936889810887334224233049025211416408159525880116906541405270030352695299619944559892704257578567606178481870102656092295183282989210628785936146868066304366128601890837054243243662521316863284890381719477281653004927869897794148491729095506686020237066222117363901519376493568*y^3 - 519053784970763603171969657905492926679705191570044094551273133406725612674450393497727954006474433729845453581467249373260949849699548231948313957456744056648813223406649299410522497137826872536795802264539472276458092454916067362392601762305743201840059059606132859653730730261303411177303594858317685906436821793/336545513151695097436520763887725781443873779621774668448466098050422832816319051760233813082810540060705390599239889119785408515157135212356963740205312184590366565978421257571872293736132608732257203781674108486487325042633726569780763438954563306009855739795588296983458191013372040474132444234727803038752987136*y^2 - 2447357516628171591801566500211417702393958915505977046948480357760524511604691600185685152495689787834693480289979767574183287845709077747968787976328331902686371514883979806164146195596476112635161390536241089385442989041479012316355744858882556718679435078636972605338705215702478333111205031556467980167405762401/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272*y - 283582056300823523114868516370535974220439803112912207228575253525710661798664281225608048625250488975887512344719802320129274814537603534445442347500290237841553486510478935403094291643353220948386131495142271082590494182180025943736175213538322996687977626307608306014515885296436422079291349058896687083487577261/673091026303390194873041527775451562887747559243549336896932196100845665632638103520467626165621080121410781198479778239570817030314270424713927480410624369180733131956842515143744587472265217464514407563348216972974650085267453139561526877909126612019711479591176593966916382026744080948264888469455606077505974272

# 4 Loop Invariant
-25935385985182474860146908178189757865685372435206487763155847284348190675306394556221817209596747652889493048106777569264967504022983294127293573862439468982824656874302694457775023087571760344383921585983639502007369319001571592282469770365588339680944805698211859912341606425592550437372514125612827581089555876584126844668708614768156786646751745752127483565511706910075637127649242851148569034729469004793713433211443718615443280842417179/8211533715699205695140025481722440983482179661179291368358260533500053906047889561782702388959329823858217357642866880950278617701753169069381405035560604354886264104660520198666745909603656751071515687854024034441109130570654906914836923634393430107407602820672524383940965341659034639641527539593149429379928345275787763257597882821159529090951623586363996984447008778948522936493346607049279840729718772877473929710230776151870747702220816384*y^36 - 16592552711575306908949370756853115895200388603345932315677042908764268458941806570098776610717535372224058671176080624020966284210525809443949291718684713349038362682268675249727648721239619954525329149069341772139159045121787994074889982625000088667784590186244790041853313654178839972479883223497461451848586579131868222520135367939138060316016779700873909535624313892951844771904793194198635272277989752452330166255390507231198710507629851/20528834289248014237850063704306102458705449152948228420895651333750134765119723904456755972398324559645543394107167202375696544254382922673453512588901510887215660261651300496666864774009141877678789219635060086102772826426637267287092309085983575268519007051681310959852413354147586599103818848982873573449820863189469408143994707052898822727379058965909992461117521947371307341233366517623199601824296932193684824275576940379676869255552040960*y^35 + 844790302042874180400107655598200100355616359929735425314019775004331055456404217271487691602169101348770862485805631495942174869610407375005894046040979914533380896162604397846344769896318190469246777868947328039510833158644917849618358856560922078873141963000023086479603913126346491706833001495997592366666354876084250997489973058168598509770386454905989201326412595635284544699074201051541711560195269101815457003301043596817030604872680307/1710736190770667853154171975358841871558787429412352368407970944479177897093310325371396331033193713303795282842263933531308045354531910222787792715741792573934638355137608374722238731167428489806565768302921673841897735535553105607257692423831964605709917254306775913321034446178965549925318237415239464454151738599122450678666225587741568560614921580492499371759793495614275611769447209801933300152024744349473735356298078364973072437962670080*y^34 - 270057210528535906736091349192055926669338069488494661672516220112798820026128496466260779226884356547117739521405883630480367986443785496935087054489078916215830805395335343645977030351670912859048032175625624733187705743117867203970575482778866410218374795725479683633155510196390743803204240931653199611156966251420273000997065035874756155261973398878172202623608947041814705197380812347103399908523074228928489138276834217114694524323590313/114049079384711190210278131690589458103919161960823491227198062965278526472887355024759755402212914220253018856150928902087203023635460681519186181049452838262309223675840558314815915411161899320437717886861444922793182369036873707150512828255464307047327816953785060888068963078597703328354549161015964296943449239941496711911081705849437904040994772032833291450652899707618374117963147320128886676801649623298249023753205224331538162530844672*y^33 - 213613380180330507420968105067024005174528901927339319866437855990866598574984239802986993608538533381721383620760129252619814153452990247042407123086369679428077500236935102520818380520619763196682113443851225510553238125783410416444087580431055450373279472815079956166032990168119638473378458858610539202705688335738601886624502023463698621121583576417623804626287475209030819727547080049617473099869965848204333655611514387166532717279677099917/20528834289248014237850063704306102458705449152948228420895651333750134765119723904456755972398324559645543394107167202375696544254382922673453512588901510887215660261651300496666864774009141877678789219635060086102772826426637267287092309085983575268519007051681310959852413354147586599103818848982873573449820863189469408143994707052898822727379058965909992461117521947371307341233366517623199601824296932193684824275576940379676869255552040960*y^32 + 303701654533724336912020113677366472062550633844919564972435232129249977043336083497262311513518137841333094220454212803125415021475370642133917590853174422558142718874944942539394130944066264170990696971689161757523345560924289992959701133204320471811383642739248458220128435727324625266053578842496626542569525568587518076000235818946647454573688219141090892941765461478892591752864581396998110482149144498333042663135608524630185324820663435/4922981843944367922745818634126163659161978214136265808368261710731447185880029713298982247577535865622432468610831463399447612531027079777806597743141849133624858575935563668265435197604110762033282786483227838393950318087922606064050913449876157138733574832537484642650458837925080719209548884648171120731371909637762447996161800252493722476589702389906473012258398548530289530271790531804124604754028041293449598147620369395605963850252288*y^31 + 4519633249865607346418012950208439378189004284906683238040302946904238817840797897571079721085905081874172672480659826079029221112712928303321521569061087187419037849123837392927200676958469028553042566811055601107481433284998180864726058247305359869243420962537183500301558762265167185992307501333589102156154987034102829562435336965772731062934287443521664445954073037344189354614199870660424862641325037986906324143284246746493860307163837290557/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^30 - 9343349245354561382633800502590998957408575505758856257979492983123803646824855726544068794173054240381246037241220466167004118972721240023983578923299326593972354342800161560509300251736639438855719732694482253019864157332398154853418095485962574584991282754686184916022433304991936308876636815051017229057702438127939919484185993051258184266708417857730092554720384595127360493389284119872910015871315014644362529229529889870979472039730439213281/13685889526165342825233375802870734972470299435298818947263767555833423176746482602971170648265549706430362262738111468250464362836255281782302341725934340591477106841100866997777909849339427918452526146423373390735181884284424844858061539390655716845679338034454207306568275569431724399402545899321915715633213908792979605429329804701932548484919372643939994974078347964914204894155577678415466401216197954795789882850384626919784579503701360640*y^29 - 31651565420482588308205597252748706189705272442543787616348001480142570791625039039319196789290509425300267375390570236388521279616623781142310094108399713914314148350885246647949181813956139826896548656448942876676355319911957764992750143102513772360084829397155286973370563053170089003891261491773957720478560101182134653759931673376929769456122011336324302152070141714343741304155637083303990039626274755749046486558591558051396193254010927111897/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^28 + 175645403457475111164331830919718432422536526570885300877692626478619632911453138490269249760091183790278672383711252933956642715677561206098953031455953913726419855344961519857426610108304056263266348453935654622234856786119131493325761278430835550161849823845987575597415706248679328705390141781453512721145387248821111051395866253503683589975240514278203561979702560712771465125934241316261305792744530903341276761972450490902445761329320487305703/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^27 + 166575516944243518833842885253055064349568734874279425945261281218276698633612595803539081871343870051235316369127732820888291544184988910235608995053842977046636868983425206039593416461861645386725891935529258857813350771749449113854781473863034912906353433314972200547937743403844073318249918082951694970183147307040285378757659913165789493674251092143321656822090827819537335196222640997054699945803999666618403466412899136255411101246219539543109/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^26 - 342224699817277625318528760592816569783072175383682524684227887819127124038430025899615135627496585246592689087557966758382620348004603482418862921252450570444168329228493014843745784351154361543254858761631681848817794716076376570267130242776087425902176606111775190338743266489792339881899558135606145731463577491102518535730265053124088380131805132901403955143324924761732134864700811123363268030366782428918569608946157587858967069085590483394999/20528834289248014237850063704306102458705449152948228420895651333750134765119723904456755972398324559645543394107167202375696544254382922673453512588901510887215660261651300496666864774009141877678789219635060086102772826426637267287092309085983575268519007051681310959852413354147586599103818848982873573449820863189469408143994707052898822727379058965909992461117521947371307341233366517623199601824296932193684824275576940379676869255552040960*y^25 - 323731389675512519918510739561970671565199033176155809607217636295430938939100317843241141666195669106866171105022556987676221289805669504994190075626567198152922138953180062678755894762419729184411496833793151681997623290774796406204674893311718703269227680491776682088001984896918996510856271165236455313354812638047062229276165744912272285675655755567061135870611945397580898969915165939238690327151989523590550610337256745716670002706677763746719/20528834289248014237850063704306102458705449152948228420895651333750134765119723904456755972398324559645543394107167202375696544254382922673453512588901510887215660261651300496666864774009141877678789219635060086102772826426637267287092309085983575268519007051681310959852413354147586599103818848982873573449820863189469408143994707052898822727379058965909992461117521947371307341233366517623199601824296932193684824275576940379676869255552040960*y^24 + 171083088059611437776449137682283726211864378117649472315199218564686269243289670339401218669602553921324549195806405706388690800704016973073835162810621234528244486270679408010622350229817881580611804330748613297677255080939434554192444530108651337518694178084053736638460322490736258224236129725485291341636958612448346522355987248436751584814262160564332920452088011060168513588697348021273216148512157367730927232294127075323454127059131706937371/4105766857849602847570012740861220491741089830589645684179130266750026953023944780891351194479664911929108678821433440475139308850876584534690702517780302177443132052330260099333372954801828375535757843927012017220554565285327453457418461817196715053703801410336262191970482670829517319820763769796574714689964172637893881628798941410579764545475811793181998492223504389474261468246673303524639920364859386438736964855115388075935373851110408192*y^23 + 345560508546652104734487226988814289293775960560379099006593338688187150445575687743093219692364329812578014655206039081258598442096031725732208321385192951786214003584559056820771618411024402833059685253707148255353158042116467412569167510499877193131776942595582475271922168147021677641082177238526994223890211904763422701229760339053596778496919513939232084650264023797630777213261984900290771283217169176745850950347041775856441264950491576256581/8211533715699205695140025481722440983482179661179291368358260533500053906047889561782702388959329823858217357642866880950278617701753169069381405035560604354886264104660520198666745909603656751071515687854024034441109130570654906914836923634393430107407602820672524383940965341659034639641527539593149429379928345275787763257597882821159529090951623586363996984447008778948522936493346607049279840729718772877473929710230776151870747702220816384*y^22 - 30286825153238396977749731260878367751989434608393587800980023337151870755032815919960229904883775663370018162997663084257832141267946927237005592070324752915707831326417159245249904270701375118081667333791310115164168223708331294244111746053130824131836005904823895102104828515237870498036434094065794338759522087317476320603121478543469394939605036102534329899258066974343583116868144353760704331088324452486789062505836007339949970805047130428869/456196317538844760841112526762357832415676647843293964908792251861114105891549420099039021608851656881012075424603715608348812094541842726076744724197811353049236894703362233259263661644647597281750871547445779691172729476147494828602051313021857228189311267815140243552275852314390813313418196644063857187773796959765986847644326823397751616163979088131333165802611598830473496471852589280515546707206598493192996095012820897326152650123378688*y^21 - 2922535540598504135468456562657894738683452683759739089570525340339554203285434141771778040073238171059869638414298207295821478328920008665774569279171659244503919894124035718405110156358505060242296634913792136035664899093621834117844264922808416614169093854724704947798526110618585375582064735260153370991278746106838850748406258008839508448309411020073426160010950417062034999800859171475190302497346074356594507251975665567882986025959885268758953/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^20 + 353940929189544541842209380719148117335973096102166348951577836782844223326237650990754516724046332023842402248935626525304848456759307785275679973523810922891600720611971998070585987922102790450154295971094978948015883567379351103088524150782184280169318956883070939489366166160709707896503641403364961109060192561522768125335979284828719277742343167399183730083453475239286086269466497423429693984617603149508838451318834564126486328422307259588663/5132208572312003559462515926076525614676362288237057105223912833437533691279930976114188993099581139911385848526791800593924136063595730668363378147225377721803915065412825124166716193502285469419697304908765021525693206606659316821773077271495893817129751762920327739963103338536896649775954712245718393362455215797367352035998676763224705681844764741477498115279380486842826835308341629405799900456074233048421206068894235094919217313888010240*y^19 + 3023641503885038388250521217025407235659668034943116707838629054952328119694696329990041283090425969848758782553683518786134510722149703682086797357464022199113292494730490234440478398021817242728805529693448591413823962777506614605905261093819984979896263600832212017897944690186976374021714658906610545587337565553465940470181592606041834274616381781242101209798246623064557505420587841394162507341768086111236851381291567215063000066609838288466507/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^18 - 730181058792436013849413130495862192189619825493514070707252832861148553326058922797093374368811655726699172519500812176070043025658947359914508702037187861461917395940106143646846084064320366155882967938697739186106751064375328338161881079008624224265437550060526977697068721549085690221848060681409589051047256822111870317229733971090439309570299687027272570890077896726779311089047648380141936028025788966030637184999880102921981697747547298525971/13685889526165342825233375802870734972470299435298818947263767555833423176746482602971170648265549706430362262738111468250464362836255281782302341725934340591477106841100866997777909849339427918452526146423373390735181884284424844858061539390655716845679338034454207306568275569431724399402545899321915715633213908792979605429329804701932548484919372643939994974078347964914204894155577678415466401216197954795789882850384626919784579503701360640*y^17 - 2077339998950017317571645156692996882501305495862923328478608598749257222919102583892313904128800641365486809852394337448964714892459960411520888739623796811011243437898525380825084847837120148058555654056490018213546381998014216587753787889094079254573268791080073407358383489179180045562914579435706937023601234918983340245362734460257965339178898069721408761538216153160241265736758885598155248829097132673752499434613020948245746584916944876740457/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^16 + 1421891913311492951200801247062151921765521662657267786004347507332029729404555207219547145708781976106146388041709729092131396469752170139542371037994291865024836912726438785195099378736487976632828784163484201057038297797976541548042747512337678004879239944761015348794309317193692709915860613863176033039412064177055372335369602399563675204445313092097250629775713888659724760540495699152248108433610772423553194490227702058204106858655717645536067/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^15 + 29940657541661445556293663934032096404822173327405611169669199058946485427067086001364320246583172050803394157105056441223007942353358964442821393926729409258665852319315943298832344660698775151310296043833856024906962401190227574432582704133972918872363007777118667027378639881901346367097768577099595541114281118948322369732165105767116801232577275372038464867847457115523105761811783250017874291072933857661263889642011570834491981286961262477391/1026441714462400711892503185215305122935272457647411421044782566687506738255986195222837798619916227982277169705358360118784827212719146133672675629445075544360783013082565024833343238700457093883939460981753004305138641321331863364354615454299178763425950352584065547992620667707379329955190942449143678672491043159473470407199735352644941136368952948295499623055876097368565367061668325881159980091214846609684241213778847018983843462777602048*y^14 - 328100966560164140537160223306218095448840114180492935939367559518513085870554706141970507463486865078388809038773563148143211188334447073903265341580732541834555239601747147373013335206093394046488366470964634809693383115932999464091503800586631679715302097700894476383191254886948303975986301380325018596463992165777641865614615663675662298166906428904862256079508873150755573868804875894822563910186624782905985373654614557798466323361249381118499/20528834289248014237850063704306102458705449152948228420895651333750134765119723904456755972398324559645543394107167202375696544254382922673453512588901510887215660261651300496666864774009141877678789219635060086102772826426637267287092309085983575268519007051681310959852413354147586599103818848982873573449820863189469408143994707052898822727379058965909992461117521947371307341233366517623199601824296932193684824275576940379676869255552040960*y^13 - 497183485344854468630781850066676426698752439337863215798281465497805959269094791869785903292997229870599066312925373192238992247710976099187130514732285838950151465249528641250947742576639104113000252103321495938810186903318084190868783627662643887817428624750151967286052529936613245738416398091482380571633025327349628569213017416056399920323829708948131969145039373791768333896316576928047814433258657016858643264923256956141978781242228063063/30640051177982110802761289110904630535381267392460042419247240796641992186745856573816053690146753074097825961353980899068203797394601377124557481475972404309277104868136269398010245931356928175639983909903074755377272875263637712368794491173109813833610458286091508895302109483802368058363908729825184437984807258491745385289544338884923616011013520844641779792712719324434787076467711220333133734066114824169678842202353642357726670530674688*y^12 + 54629059817902298687895903096511471007539211557502179614306944073069766367852433529617548726428319739782455132367652221844852538893732627585756031134846171172504585295987688506447535065989898825747749875032556584263384466712341776075511075933962506747563992520782406450819502128884179997238044747420469099556598839109264869993171318388083211851321268073255968757178299751603272925972452714574771165235844507996298697376615145876672675313957948095631/20528834289248014237850063704306102458705449152948228420895651333750134765119723904456755972398324559645543394107167202375696544254382922673453512588901510887215660261651300496666864774009141877678789219635060086102772826426637267287092309085983575268519007051681310959852413354147586599103818848982873573449820863189469408143994707052898822727379058965909992461117521947371307341233366517623199601824296932193684824275576940379676869255552040960*y^11 + 68864998445867499673279867087874890222932422999046353223121866113472780911425041483184474995263079527445519451447795718253184901631902702080905078303889985932680937359988769403273148619570042049348584792169879013331729840257662869324897511843824907863372312672407995637500898883508625319621179860814975742613145477762581667963618952427884758208827035749564777073988091290441424040866875029503524543917790385161932185274762466774224759150894714452273/10264417144624007118925031852153051229352724576474114210447825666875067382559861952228377986199162279822771697053583601187848272127191461336726756294450755443607830130825650248333432387004570938839394609817530043051386413213318633643546154542991787634259503525840655479926206677073793299551909424491436786724910431594734704071997353526449411363689529482954996230558760973685653670616683258811599800912148466096842412137788470189838434627776020480*y^10 + 5861852311208752495729815720446889353862967118978634165935046610222371418732333959066502272064299459477584980809670989352761693697726874140019168460236040754949761266619930755133914984624302374965106759986581080194271570499394125452212763304410177078751457352575808653483150613459476312079192346706712865144766112591779944438416539370872523756177285148628139388475516139776614638074513281924576098478600654124712205554932000303390605167337076248753/4105766857849602847570012740861220491741089830589645684179130266750026953023944780891351194479664911929108678821433440475139308850876584534690702517780302177443132052330260099333372954801828375535757843927012017220554565285327453457418461817196715053703801410336262191970482670829517319820763769796574714689964172637893881628798941410579764545475811793181998492223504389474261468246673303524639920364859386438736964855115388075935373851110408192*y^9 - 26982517214496131923523290821683941451154091868892509886542682315595609815183891069183933236820086192812670512977712237219856692519091805315522033686722836009489399668770433418194018373751219216725459028479645618660817362388054093674198066048399720673454676422567087379725504511161993231146603528226746062725087262377391484408079182746280244607810728637505373042959409840368241705386729886883668023235801389884572981257611371667856162526902588186919/20528834289248014237850063704306102458705449152948228420895651333750134765119723904456755972398324559645543394107167202375696544254382922673453512588901510887215660261651300496666864774009141877678789219635060086102772826426637267287092309085983575268519007051681310959852413354147586599103818848982873573449820863189469408143994707052898822727379058965909992461117521947371307341233366517623199601824296932193684824275576940379676869255552040960*y^8 - 34684834038112873705835732130895904529921369183904533791180906466991409429104304461592794345670410452053138854162132501655112912881663966357114059341963826403413143008963401848186748692179535870146726510378193258860953892813158007159922492117472071595467323501660132545183456423106909729875963024923083959032227563704168019657763538622715975061033877923920821725865376716259338686640336847341859093097085747936330256018335260206819703948220512104369/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^7 - 2379877666787255324360836896699578682231973036963227986349688996215835059353627276018904174073364998535905905054998403340438324949594342172430794671368494835122156263543195070579106106182140761750967593731082268089180019292590963175327179841647806419914968492448492380810684849974722994270557447340376064679444350579044627838026504168847659387850117084677348456142438254474963493268619283109350587406441568998957575141105651787513338050096380371963/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920*y^6 + 1214492501758702533699095774023622558448279147556669040731850621275133836318018436035929570914812553774248921605198732334143982078521960536065645378223777725417813883818545128640544934565759674936542943691463729330407594217795906086532749752114171647797370047005689105303080997477477533563100654316723476105649255103061670867498082320094219086195988523464907188459437142779467828037153811090288621057548692730362452298167466751682519947124037303671/10264417144624007118925031852153051229352724576474114210447825666875067382559861952228377986199162279822771697053583601187848272127191461336726756294450755443607830130825650248333432387004570938839394609817530043051386413213318633643546154542991787634259503525840655479926206677073793299551909424491436786724910431594734704071997353526449411363689529482954996230558760973685653670616683258811599800912148466096842412137788470189838434627776020480*y^5 + 133778900721198741353822774024887043058816235208570532865221586109714026707947815561247486264172185713118251522663500453335654800329241500354879084985524407204114044671711498067286006613077047521668893827232660225286897854885473139681488797755426623285587141872308997051211027470887227266330852493356267205104976870769490974674007027058767704453817001474210318075851520895203304188323570023740623581989242605250102811382588897890851170618908147291/2566104286156001779731257963038262807338181144118528552611956416718766845639965488057094496549790569955692924263395900296962068031797865334181689073612688860901957532706412562083358096751142734709848652454382510762846603303329658410886538635747946908564875881460163869981551669268448324887977356122859196681227607898683676017999338381612352840922382370738749057639690243421413417654170814702899950228037116524210603034447117547459608656944005120*y^4 + 27007350124625989349038516040000402557207963365302881108755972542944061183466225247242681146268674073239185419133774950435874944022768514006023374195960628176112816393951223255744007542060017155493686541055855439616591555623074977537429725083894267684289280207238126251010910011182688788224221266067085918267425177449554177630321670719571567487591392920422012916195405212529799473104640849671009308229921437803065297179274956472641121194359404851/3421472381541335706308343950717683743117574858824704736815941888958355794186620650742792662066387426607590565684527867062616090709063820445575585431483585147869276710275216749444477462334856979613131536605843347683795471071106211214515384847663929211419834508613551826642068892357931099850636474830478928908303477198244901357332451175483137121229843160984998743519586991228551223538894419603866600304049488698947470712596156729946144875925340160*y^3 - 7887286182101691047566458649006078681323321403164215140205408712298348860069879395074985856367835608561368360726290212218167415304513333522294056034502462912340355537184377194030538709784614892420624810830281169106756888267558801997113267110557544321014795380435630561509191872322891313886030722629109097253054538238534967269058497657491366840671807224387150308512043226256608276652958685088042861979773651310635603884926190859530962764178135659/10264417144624007118925031852153051229352724576474114210447825666875067382559861952228377986199162279822771697053583601187848272127191461336726756294450755443607830130825650248333432387004570938839394609817530043051386413213318633643546154542991787634259503525840655479926206677073793299551909424491436786724910431594734704071997353526449411363689529482954996230558760973685653670616683258811599800912148466096842412137788470189838434627776020480*y^2 - 2769632307478965226278826198241397610732168645334885326419418446318790900896099736272776985533128134976987186531827009058053055277252623770488606702850666001487322188499203892409423163698473681256287984591068759058652069091941577393270418023025634185849741483942554286885979389103207694785592724676601005522498271650769416874922326904748132857723554021816468489842253961064165169813469749507643335032639279794067086995726719072679583562822124947/8211533715699205695140025481722440983482179661179291368358260533500053906047889561782702388959329823858217357642866880950278617701753169069381405035560604354886264104660520198666745909603656751071515687854024034441109130570654906914836923634393430107407602820672524383940965341659034639641527539593149429379928345275787763257597882821159529090951623586363996984447008778948522936493346607049279840729718772877473929710230776151870747702220816384*y - 927181496852549096260690619882079493049232531282722527784121228178520484419468506723243268163843739375755725992661955289863647043414202052703595018613512525549708573565786041660684114721935209059701328453556942562532163523988939360345887798888116560256201900274687730351938117118186969566629323109252225791712110367743219015072790828550375215462090149280513767022625579035710674041379651263136233434154063132285696650458306188530378525140207243/41057668578496028475700127408612204917410898305896456841791302667500269530239447808913511944796649119291086788214334404751393088508765845346907025177803021774431320523302600993333729548018283755357578439270120172205545652853274534574184618171967150537038014103362621919704826708295173198207637697965747146899641726378938816287989414105797645454758117931819984922235043894742614682466733035246399203648593864387369648551153880759353738511104081920