# Manifold: Census Knot K8_120

# Number of Tetrahedra: 8

# Number Field
x^35 + 93*x^34 + 3680*x^33 + 82015*x^32 + 1137337*x^31 + 10053996*x^30 + 55298394*x^29 + 169993165*x^28 + 212807379*x^27 + 93906718*x^26 + 3467431784*x^25 + 20972758384*x^24 + 32386858198*x^23 - 74230101459*x^22 - 281606344768*x^21 - 78341687205*x^20 + 667622073618*x^19 + 576970753431*x^18 - 794098834186*x^17 - 981591460665*x^16 + 588160359805*x^15 + 879517546615*x^14 - 325828188183*x^13 - 473678678827*x^12 + 151814357414*x^11 + 155178718964*x^10 - 54776820247*x^9 - 28755627378*x^8 + 12692414448*x^7 + 2308511274*x^6 - 1562380933*x^5 + 34947202*x^4 + 72868409*x^3 - 10594394*x^2 + 191391*x + 20581 

# Approximate Field Generator
0.417901722001709 - 0.191151278545255*I

# Shape Parameters
-4577198966493466502397365290200751894161830534463339552257191569595387880303252071426844829972273547349574504513501792586717698978750284363660174558301208371753796826684120603751883508980560730837151840483744702908860679074035118514179770/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^34 - 425562978769286576809989070905738604363668106967378412329795385928432725420592973066229299944757537164158734800484699562703725926080852085069275915702776301277707534325961941513281069750548619559594533743603924036523646703892779175089859327/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^33 - 16832125690439675506996392439435465855251052915210868825502528525120583363805407068873407595491471920449118980857586333557791447161890862789953006488375202266666693962700609764328143342140937080831282590872740820029444791036266267390610946170/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^32 - 374864858066426091086220574273052096569134061069135630769385768513116504836067699602173048428449264302187307801873753487969758685165501992589955119330459521123783553556552945760116033315466244725855366826774856157829623940260283219250511262675/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^31 - 5192080770540071804079567473819321377855160155755412222723147245249222096076461523514811661834827108857040809202612858624158385923691887526618434401702837764049365534086583322976210436532809710004836675446596468705743812805711197172667728889109/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^30 - 45793034419230066741223213288109369283087821630863008766039367806330151381899869092210200044804481448612145629931438235833924627190935994443563995024520846037735183547936809271294481246886198346439785984384239596365790014081553888033493702921623/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^29 - 250634169563454890499447063530184499516226743936360767551875551648126398678994300193281393806669424636595610209704480774944780565629431831767700872364113371358848112702166233862778811983647128340616395234834591511333396575734803152368454895306011/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^28 - 759986099424244328058438088395575115141469047344029602178552983844677545726067446461719408911736671764635660424920635441527761418846174438102923209296311186608576428000180476481067429003467935902560772429086439748978272477224681976467520229189346/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^27 - 888942174180052458628465597077125903861102989530560820051431209568892872762550739737007235979482671726527388780543781687473634029317295187433107908417039142326562299983586372567074916089069500387845738440544886115120961216661879185704725902499636/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^26 - 196001969033996725570097243923437833184380501963387190216290228754277073511058459661896091195900511518956777885938382643832947137389926608086952350323702879936563750070793952592925850330921526755122014897171707779295466080869162144121568821055019/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^25 - 15558538552655800491541928473278230520291267296136115327290818396731397338711066533827532463483362239103593696512727185962694703867213403954279521923760083272006848367458216334271669489472884813988253590226268511696351302481739496779858937294540448/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^24 - 95370465105334717737576351284941307820069105761660319637088733742560249836120506634576612237393690077566030780200861519695623060366110135258766346416347496880781547354180985414918874478400774367691580431888067815344088520357078383720616387062063566/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^23 - 141762263544552079454443850978830000238221345081917126365700350970505064509255649702444591720225515102417686096279192458265277427150362529962060697291327548815957931367627427212235622228271140320393248432737170309620488628684938519728394901673599378/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^22 + 368152048187437303876599384225685247932125482243407979587428458051831231241200380179956136657240185398602971763858841536837037297177149909501407118855176374177384320291181352911816344082146892868013309698908313133605358685559518825138410521535319703/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^21 + 1323238823681768176994250382595943083883630203343273026936046043295076883983824967407218422966028720755094107498803022943987446577177667901346086075772584250846375694983947566253797206074547204945495393988482355907128894534768786335661868957277179820/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^20 + 257280901015080839333779798929343399747974884896536526998140455767915523408893408546282129779991781259301954076894499585445358692484396798334628080047160532762609517152975006966793744706107358927928766551765565918254136315041053934397752260060820941/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^19 - 3387820009521004971893784844332990196169543124829385019592682329385058053836801984020215529457954391790671277176734499629274162449290905086240453802513597015550853708583825099522556258286000110201940068358823626545554795303277369957453883830089481638/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^18 - 2739709092800315204738317678307291746024382330794491838037857306943777109879369785887006561368892642490593241321787289622154602831916912508860720401512434086859059553454669906556701014492159253837469777031975199922784498253620657407498003093866374322/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^17 + 4340163447672179301212043248639206609054465192077218940694658380545873943261138583055837702630989447313266279720667617767153150655394031866568225927301649167672353970226709193021522560765743814039737822413597519752901170590857984400459314066034465976/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^16 + 5156817518524578747369200621902949008037470632160711788649178942965131898411409490356236191363833382100362173411393646486176753867135464772946251167641251450542013916341766448749191923351669949023838167255692647858035455912030465061596644007366714425/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^15 - 3380037692996309100793187785348189144585377298481368219021723139577849898647917862421810550049967244624278288074311327282972762820262328660950423063069806544935963460613715055970468647624153842637475590548422016660814891177818214182559325665100987572/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^14 - 5031567369524684794915361804594254021082220910138021603832459107382365550203731061161957490352627539055869794332501830089905216202403809372284850515871273914918695662529785525278760781634449328631231296989066124234906607661555997910586805965052451501/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^13 + 1863935271947518402125235941250968430300240509510929249204348539303902653743091635061955450540394299109775126391585969598713627669634711475116823608613611206639475501330714897084889658163265194038420666408495680182803364773772622931964660653251250208/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^12 + 2956677208620006472538884866578264644792059179206389822847778205054205305960126482293159298941599421925076662063821461383853924508403849780326485413370004888015741030474083196535493132706878855402270403929281628609833883734389420197711735739766469019/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^11 - 834665512384367028347758720598234107030378355817391653743657668558779161512355898804879147083131145167920668723435750716010679981886688742786244964769434284209502406436040396935536235075214794278612547060710836829776075288093954359442530754765035522/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^10 - 1075767624615029056360317697505634733420283854376979086399221342887567241832363526175126795677333646519081207689716658694412472686727379529278532770266577209996839690866187832981785690664764113214743065522579158100597343733983434790002330869400833409/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^9 + 301715267052202026375654081644454111794474169396708019043167838861691134366910981860238593444931914032046250890392868684060001501450464107606681034491858703771976723001048235490231078941322812586748894037886848818229258453284422432936251890482302920/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^8 + 232597322794462414683707896002251613999076063925541805219159748861138178057267493344253826872466672859452584854208387522861097095855027663950296416830315500940266101736226061953496064639564065577831880446098554313740386523745913556218604703322184260/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^7 - 1262830706310879986981178076575148661322518303863280116331032790532590487399193768276671936587048407978598849268639747332222358921575896158725509787867991833150031042065372922651954021820674878166163493035319600675206748198582212077320498785245645/10078656238466961441582643680169655350941159251571053941060111765645846274468549198096405581600712777205321487665484728944567980582480499453658918363393096968550174343442016228697244624757144724756896360667989687842312229744027904798934702881*y^6 - 25973556947288106640174910128545033060853277400837518268373793282341943392710455408999140162989645215140919171813113726541108203487288126217576185169236012598357206585476310967918818364224267950849846595943836944725474151446705788598268738493186887/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^5 + 10187218504826833631003574787792989992021110012581036283327274568206400454455121363383247351756939556982156616731456647874723018481980910384534829583563383863376743644268524526584111770314286296240464166841545939945037742882880999304683787758482247/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^4 + 897507192605791239498005973857484203917984132650476795373398201316741842949234306120963711922077127504723535913351548079146520849659199668785739169025268571763690448935131154142554608647820251036881821959729074133730131296349786243665509784459596/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^3 - 559700105058798930666204477102911250499754679055627144911893810501726400382509616683920145660361685609534881628133275157105101256588491645678761599651737650708625981423160924609676444217110873756942181336627116120920313957907801647961919458979810/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^2 + 30130641282733891749544589645280083293025656076895512474853276886494141964138879024858825693908530049840896057862140517428867673317015635575770772504130862652809903480726759767286714579656532105906698770930750206297268504058067101431614533468956/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y + 1578941370828701472098361082206027397088710219506775672188890388887628909912155477686469391345946013804928903845519848446376194448883157271292477898225213764821588187537902641709747399696480130543907540739003700262198764662377499367371816284839/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979

223080941661837758394284521813574089007166750797441628491499350198982832316788142003191679149403870057333361705427314884747972095433817785931351071379822180724946999609857015408373231267886522379442915122119376322041806736593163527678755128/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^34 + 4152470870424803984262843737266453412023664224695612029381450380020357958831227493440133076485154980856136590920556498179987315082178861705294570108783699110968200838400318880514025192499373900839667039932511139828631431890447095971290571254/2973203590347753625266879885650048328527641979213460912612732970865524650968222013438439646572210269275569838861317995038647554271831747338829380917200963605722301431315394787465687164303357693803284426397056957913482107774488231915685737349895*y^33 + 164478812016416490833922543192169624390648941461093074400740607182325497133734100442357231830999321140566895343689029525497451950468425592940230911903503483866669059127304513738181684669056270900028556668992382677654933009891068134884415566371/2973203590347753625266879885650048328527641979213460912612732970865524650968222013438439646572210269275569838861317995038647554271831747338829380917200963605722301431315394787465687164303357693803284426397056957913482107774488231915685737349895*y^32 + 3670548151388283015305909127349355220310517876196139572877677818525938187333453982318011891096095620544646262139618322344723615245356975189066272088155008645582769502518414836138054490768765861246341999553053245400042938976626388349569314016221/2973203590347753625266879885650048328527641979213460912612732970865524650968222013438439646572210269275569838861317995038647554271831747338829380917200963605722301431315394787465687164303357693803284426397056957913482107774488231915685737349895*y^31 + 254956084495204996196417795084282378824129720699068962855099537563640981991030472810064734601125917542142890286392217301240735920661350223595812036202798150018305564548025810852298782212177877453983699556800787037728385834533849785559200754662871/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^30 + 90378872963279403357254154122920988573309466648373096948438401932139883848027081326653995680860525358179930706011208645084108211357548417504030329035923792202748240518703637488011768521513962952104659220715722498326897620908382841590124456437528/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^29 + 12475105798335938699794921910600024694635908642310623093907940393923790639806043516312763508873988878724716087922945875917172185551272801822896540951643598378967529702546496484762328980743991422973730457895361691430927781849790990282750350190459057/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^28 + 38608565070965222522005728374708507517380906857165161709563501367889656365563960632665229702421176763749359810266683150481145837777132342129400398443085128650329150906477519833217542613204522635610451361912789133954260939569787794005476983454566199/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^27 + 9802065796742451665058044474009347089781209805072035923879181612297697655202175792153613903517460898200190211530359131112391317320687497053711563065383506584275563736015906123514082014656419830158478875432387208201848698758299654594953243703484398/2973203590347753625266879885650048328527641979213460912612732970865524650968222013438439646572210269275569838861317995038647554271831747338829380917200963605722301431315394787465687164303357693803284426397056957913482107774488231915685737349895*y^26 + 19973504769150654706758255703902740392828051611572128758797225884346494335907288211766210078387441302713621417155533112612876355163330323934046944062196643648049180719468289220526692785363939494652395275259809464341121370812501539837816979037882209/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^25 + 30631482421896590763539325442771914135263627912504482059337137715636720762432527117467349393631436103900653965275793727248980600906661677110510391261172522592000713632691953539106968400619857256854328739805120564444907398128842166171265772115671606/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^24 + 4721263180519212086290173962913075671556555380545189560870965728953343249683493808608493245501161511399543358865512114766163802959427367051888107384130038046914232544837524221148244672676345873098794746525228504956478430730484356782502235127850046952/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^23 + 7490509212994992112608091879193018950183894957380946156993893077099163114610918773441912851873796780681467589420618715022806661360601736520825585271908488537728500143374664229498440884766209299022947956856805485879322306395064700236602476870756136663/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^22 - 16474436926155488097965652416078213271461600252793021876312350359872768932608787661530723102441010820668086507065511294740705850313391187523561454999619166270382439830817738368521309044932487236296857084981034139265040860887088616610313009737905555216/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^21 - 65130095290071055296512014985657023067068734142697923089338369464327498392693145630632305979080434099514873865286876000183053694517014162479389648462545001006569021583849479554183020971796233360415207168055822328675853372533612098995519718833260645706/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^20 - 22170256306965693266269935302041144836202449100869869178517168283532598933425895381348548029368442733400605459564086865894095529533659972983651745088494508906291374848784085238128137565758699153606947077153741262367959246047712450592120227598348168322/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^19 + 30551402948161729497046978450817941090231712013560883813488339686752469087073284652520321956461862116719939187499401900787099761608902140424579620182870132866937659112245961701722491049792120780417919439946275360019919467060269038173437388706315925274/2973203590347753625266879885650048328527641979213460912612732970865524650968222013438439646572210269275569838861317995038647554271831747338829380917200963605722301431315394787465687164303357693803284426397056957913482107774488231915685737349895*y^18 + 148433431754021884632507750785465894871406092274833136586619785477098584115909204197745741129473412091236685371318376958079178814942669954083249205366268961543184824162649448104563309480558321155863816108161687252133455984031739529919468031808674898408/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^17 - 169112230797930224336814018759931766700143622113629259148583613197610078705740310161328276884517083536996259430072365598205333837329934075954850018560172755788614601774667824786064865242405747053781367768130310402580724412051292189753031182795053915232/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^16 - 249577004216841550185017194952386561831693611871215331740989711419215384474622900311868064251033623972767188188770262346606115662664940984660509398806846158864781102304635036246709688372993888622944658713862863402188571017888903483698029921427106299224/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^15 + 103989288669494729164437463482014746112398329061990439475128575533352021031652554332297230982381564857150052040014992195174033291449468243652084985833669341136266015793735846066157741011321769389766578196115918888342962893363898437970890363503128208787/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^14 + 219130655352576169739651725980702800009458519217923808458372561581264581552014657509817131928088484792346423431028594593342730188857635831315075066850922894597859464040041323427849888802129876856360785862372196075503060200234535900350339354067027007759/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^13 - 42276378691107666767444792888000367939276254791643364184932744586790002054705205094811589176361899520248477366516834337877382508824139096158195704787737854673797795623349078166508934088369978560645802621243337416389514060299024510175024659075471777651/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^12 - 114747571394348177376065229371084086316806541628926241931224220114362893390657296721228606257123739798091607294909181833222977376707601019930205245476858117116005632930854992585483601759005316553911657002326135618896061716153739834902648152673679315903/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^11 + 16101597778013656206155501327507432116914397498498389270958268974246205537398617466404426116369615228190438181059693788744093908049745252833245606842367217705799810264754050791964532766992773172823593568129722648535686814728321501301451514776817090876/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^10 + 36790866940002553849400604333179625566256684140534998087574373732975285276577209110796598467015891633605017529025579170539419722160844295674647158598740590990354435272121708796075661821693917951084397262011556146532530740097607664534857817398718927739/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^9 - 6162799214401491486001980770696460446991129959302990785354982588017152337335662157469139075280625132337690280609878739472741951479499950060261184389469806119901291680261240831100403463523836153064470138287061127649755398643054096275643064368354610408/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^8 - 1378589130539669660349161785468969888895056989793463710322071370853536822635992657830509306875684856950491802451696344811193401974503512442306955054284065073346010516371220940892306671748857802333585440071601527199272662880731792615851035036756061117/2973203590347753625266879885650048328527641979213460912612732970865524650968222013438439646572210269275569838861317995038647554271831747338829380917200963605722301431315394787465687164303357693803284426397056957913482107774488231915685737349895*y^7 + 27081564092134823291454995072964768607403407871991126577445328937142520987683312195438228014498160476626342622193130238649413205443567004440332941991544785613785475205114083576721646828794299732912257046130161742400329822031401355510547355647536186/251966405961674036039566092004241383773528981289276348526502794141146156861713729952410139540017819430133037191637118223614199514562012486341472959084827424213754358586050405717431115618928618118922409016699742196057805743600697619973367572025*y^6 + 24934808846106357543889542054361304877993874528680040758923488337708135509749101509597422900891694497643621390403188520056431727023149746403845175648317447868905109762784576638601759369764864785141833259724076078017845314078632085095147243418726762/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^5 - 210552398092305961891216367355135321470503794919438274973547306773730797757454373405097579360632971476932335081987654459512741207397282145093174111472983740916094713495179564653850130361747066890951448491819724663104361318388712045122423289434301274/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^4 - 7947645112820377164829123444809545807401706909226045429255874425200593050052657898370117410051904193011107781891066073957793602274841887986251377431363413062513479545149011054726589327537220870973366232967390265005869581985339492539671696413378022/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^3 + 9754986122819245132525914168823423052188874958534655543023374875589898818285644932277296885540469249399897370158429185801213016311586884463024690386286887419875466284631461035908292759784971173241764528800265632956245682783475824999669981796041618/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y^2 - 1426583674750066240548232521814794367371690582301629207997272626764265586901353809951111387655866268277761224489123867968046597709872493637162566252212970795692323035688004279793509321888371754538642428399834273019877804422101403153198843224587211/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475*y + 82669884383956675015855924145984269989205783913851375284823025616675843818225620070971268110507591180413673319432011591850032048559818012469396161700744039048465133978172335182766819710764372808370397467964617620620369159078191239618470184496156/14866017951738768126334399428250241642638209896067304563063664854327623254841110067192198232861051346377849194306589975193237771359158736694146904586004818028611507156576973937328435821516788469016422131985284789567410538872441159578428686749475

215496904619477686791437973825303954484187322557193714319163806593234394313258490124536996324227265147355628422486121996484546679469672730913612918837949126290604136358972603072695594193192391689385040461666926321682161387472939175667104142563/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^34 + 4020030351685316396512638923706088344425986436360300450614796099957829151153118751881594539199615056799701456582364348057436246845294244878031698387662869500424146112127411409719669026676798929550076500273684433675471329779669358532614146780529/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^33 + 159705340933361644342841416226308969969461605228391012103198939122767121255587375709728219499054990155586695947279185631190998755414152613897839159336757176810449869645065514177650638366911738194956576890270124262565149158790050923960796336850791/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^32 + 3578487368977632648534377740773420231049727899328293854789530376193036760754373175479813629000426204887395306467022961836645367408154729764463153893855951696549907656846529594850012316991962527444031156900632589550014611831166896672978095076124441/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^31 + 249988621679165158041193086798927930916206735082100905660894064285373841441955302185411327721815045221059477961243207232969237129153265588272303448610954816785350058291809904519045952424146061254754083865680813575134123339605680735251106615223797266/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^30 + 89401331125366355242444884515235142442058348686294489571986702167088187750423066504103204606417763341437173388963497315567818586562796313989245999362980147626128475835820221061574429627043471859078413685633041670674025927430993620386965336344818891/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^29 + 12528746119835975729225745731640604896422008191026283250602683275414202478026087732949719337106656068159291413690509709485332732793763142749048184969806659753685894090521895737381627807565561805668065209311132650860359390647373122425977330970575907997/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^28 + 40067703466133955558304952979915328494685967314699053953808333642676195299299178704807396857533072187315115596859349275296066958110060890160301508495246045131423443072352221716391319301500021195347422589906291303554759900005163378226973774257297676254/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^27 + 11373925608915173618021016947439275370230333118537086561121270724104934078134374514658947860030579482266979100166045298724689582190409146805168857869269646177960858466448404081089804192156796848171324145942687997458621616390477331206113666178176568398/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^26 + 35999767635075182747656291066636012484384442697632570784922927561863147695121975053155247870477720469154363587941902609597571797636125240287802536420578541276643278858316630680108124375994229090593060129569119262525030695692564974335200594290477562189/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^25 + 30302351467661460883379561543706224956081346591974347042489517892923617581491607696108309561650656066858626067941934714224120514588270174633765729410124531272221186376299974224397469794830262146608352278162464989922955963112958099788794785193801912641/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^24 + 4727427932687173321947307340546916101440704415018711701214874858281108816117707090621157875415509290558798889212060588600652785969083939335514467886652984048934574069182705193012177703605520901714739236041615321281454935137938936753805228513046616476567/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^23 + 8274893213657916331529581551726737898201903513356972975764075351881694250256849216316585811879791888202665125864696617203354266026575318920017222369810325172404050631491697671040939762720428689032459859175923625797294532588789622177164779534566483926698/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^22 - 13714184922410427862613314171096175026960365569375538556793344555325931949396974022708627912009723166742101832250276203249037113176799935666369526785177550061693702495931532666696094601189717578975491755541903207065158754536694085624194246248175713290611/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^21 - 64376334076713986311595103993664746298679468615370783335224732416506320794269578495321315753310052896691310728840943473385181882643723333967213134504179414970987835518399188007098851508184863721772778612404114706831459631107861335728928126656798715814101/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^20 - 34451426453351195877237582024978528407087579017476780778826949518105709568224114370584524961602366487078581992492352562756155688078559776354694848792867665732909838077553402947316170458812664865047540159351535681906334783506817727684435780411096021958012/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^19 + 26841665789437253896574169900280611741046554318044516520416188189503352969901509432116854602287280778331688529559843100264340868168527663566221376962479211008488282594507389043194758409366695570667486129020061079701460349996966090823122408661941489319289/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^18 + 160475661969614361726134604338062693082239674461891442767140154534774975289189329837089189461799841378313708544552706656193052468927116066056171333868179574884639969055527237705930695241247266973338938593893423559581431134901540499355946339905956934018843/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^17 - 127306646002104528281208141852705118881868388721794516239145011643567251157662614022825226857980099003394653928112996735103128030791884457551887271332770244328174718491377801328019821097630504848358406691408546719261344162359635327471291098010810313857447/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^16 - 245231021075350077206997722429691648762084312443785888953712853580553427132447960205151175291373987742670789974740197827686521534847218400933256347722050998554379728840109195378325670017471444384156015310200562001458939424380387461340635310633906990886704/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^15 + 60607603010422127342243543270793666195375817335972976813489946923048715249824052975257883436819688439590216201979539977759045811818001689797108181301033488823283666842826698744807623583418029873503788648638347260369090586388113880703199268380715844805602/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^14 + 205196915498497647609783783516818427483608628221588523323201453127721020689989388009910351515987342701460170190068427753035203417513809955087446722988137945593953820031879336572090108921440343358096834025166798878784254646894001134843492094167540279478589/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^13 - 15401604809035873754396042253854112369798328322530856858979794546903230065319957386185826156870584643267767956958277734329583042855870738242184093627171856544666322722851935931586444254050562682606023988809329309357154830061044693535636795706505734515771/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^12 - 105940825913086680280830758015832048817205219334421223564233150708485359619672635914619600740033129495446254704352827598177212308806911740711811041009552372168879441406215226712169631400906806290829020775569767965905981501306422895663958439275206017566213/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^11 + 4638625517374451692905101724989628821190692980601559552326636237628934263719265972779812885779624122009097024295043251515171445112611140212875533763620373284639624677436327814039817303619677286482266887576832578361122744509917070808210501679264546468746/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^10 + 34645709422630192578444448884444300161003450810576303278742732480607083703131275598086899725046774953052368045322540250882535324690793492215919831945232036792219149580705292812112179061060486411426286741209211081823733694796493664812578176071913326141869/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^9 - 2688526423371678728955734179145124617393887153243245996712100867262562051705965563807302954402634414316255939601633301239942862100105577841397874067304161496723094979957316369835029528062518332519103855742812459252787703875523604097193401822373532068293/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^8 - 1383791349845781584899843251307472411217458834344400342219685637595761183506653860909181594919719416906064260961596500004551744725103419055992767617845339698512352137259558259450847240402044380657956465557215893920513548365494192499908304071221579356872/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^7 + 15762201518488942982177152392627267744955950596388834028127150805577410546795143319716921574033889672441126786454745176394063159013548925708849549291715840827926449723775281637918605608849765691098206970908599708949430282704574487045388084413576292531/60723903836763442685535428173022173489420484490715599994887173388016223803673008918530843629144294482662061963184545491891022083009445009208294983139443409235514800419238147777900898864161796966660300573024637869249931184207768126413581584858025*y^6 + 29859711538427916083325118905242596973023701759369381859027825806372591148016856634971604771046317918666015974656138149120459635287466365659822465279788556208392111494939694348278103092162614374618403751947151920460078331412211244854083920248021923176/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^5 - 144547938701863002837941715763663775583419251916061828154349241102394098612940136697280586452017378125031653575731236034214572215751853458007938292588000640709003958385653812368162590034146590777013574425706992463996625510752008958650380975369512761754/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^4 - 30860598979789182275146967205904452869307483861743688897624736614789996389820933661565563650920232417754421894456571465016337860714562466070624116933380659185732603382684976729440934056602541616747669469500133744693526903125201952312149898194825989637/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^3 + 8083053387236179909875617930046997611001284587081300030836487250765247913584620522417298645978518551598590775648923410034130432557455190536435393557555543659176316879611836695643901845538551352658965007183718390772935017332350989849819807233402038428/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y^2 - 173191523985421499207842468656982714296733119403827465847502189280447848261263338718605798196214131260222840297640844449803229471316014030526406156579460096254359121842928532237978826618153214146572499606770944736165029544734100037538345881471936281/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475*y - 22708054119217249527923239224245158872019941924663566967629366226462145701725110718818833395436826859645957866488154039881575915694069921690483440348863764151403089480827137958133155850001274418466745106802607743753432502428997978045042269674942849/3582710326369043118446590262208308235875808584952220399698343229892957204416707526193319774119513374477061655827888184021570302897557255543289404005227161144895373224735050718896153032985546021032957733808453634285745939868258319458401313506623475

17579781039954562325730209930779690389542341905243862009265221171536492985487705929885256960571323818710738221087225908055123547593393039256330965900560800815280049777485561606354247687610967984767186777472893213556590649093120378552019/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^34 + 27528456744032010323257396621639397399967623556616877870459189682096762917216245922585142084496799000986744689461430434618174743180812772049558024194286916171246105475910190685741815568458207967173395344952230518287632222378400726816896/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^33 - 85772443345697727535197460167470735832420135545893878197129111081978463985243246722754351939069385326342865344292342178100593987327000252940345683669964645985402708353193197826335845353471788847856767708753082250459679669102102101482961444/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^32 - 4564734543568580228128091816612795172961606443915677941559795312811287022963293702978652161233080498433804901048134287090610512171335424330826717296362681685634890438996127966399224903181807289623228229661525507814814993027918224768689938896/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^31 - 115467890115193055980054807468128223444271958115685208174421103164599113782811695172640116581960737557794795043846946222781876757483944154910764307352662554824547707356095610010822643481466566865122344736092129301812957198822226522499752145935/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^30 - 1732870361180707923079193223845437474295463297089673297912453038357922780040016973016766264469660190554529848666982895031731226675207983314880254449884057678147712627889736840420946672502407136720459448261027268994901415954103839757190144558218/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^29 - 16328700911257408073688130654674780188057732840898192949708454285612874907336902470708473502713782452232174210971138072082596300943092658725726938772485523314983044648148628378500662826886032585460969092841836821780693219580538530544064137329969/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^28 - 96115519802384979731472303684915336903957081967578748994310016460790768429998909474036950091582571724965118428761070978952314689489706994383955916919138653478544116881298526956596097488346009311123581465676623558214615065109949298310679378255547/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^27 - 327007838445808099300958060291015600348047185675918881780323560545260883509332904453832740037080460561566508978706996604448192914236135819196619135822769789331149357615200918281293228250754730898273509028703324017559443581595944032500003027241348/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^26 - 525764885724233771553450099418688175065918852409710071453774707171377521532844004946843447712375905741099068550518172953908890871636141168402094826361420655032010799237174483628725151929565579260378474065802045945847905111173289171529886104469380/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^25 - 358925879623086006468270514143400890988550313426926005683063382563983275895686688859795493274383137636108341622506595122915265703597970496867564655593747039643141328428483326387484893506530882529036344169457252730956637921237309900062044441567415/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^24 - 5381807675695148288834461249319662641993977039679930071835820312608912345579560765203424828173579767712265455977303423436492473892977554197333295346477516058384318506035008636885154727418301741184585856350870722443903725509886272762262029720610129/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^23 - 36582746948689129683537676224075127384736931432549460895165123891305208176944751306495824585581539694143894893078253653772797229730484489845184448400056333116329302599897293535039990607342189235532831433503773361387650379728721795904232518791039355/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^22 - 75015880096074161356659037837012145589580121922378564826832983668854759056039825062572825925466681180800717411736284021130602713098872764507694388655461813759439427265301141904080935629529592126140844655445405580935692249699415182838445325848046387/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^21 + 75514010942682689514917357897229682206658091450264377792081642546987678911532599155065809486253870604850916330608039837979951534954932199118070113149110285208994497737238720559686808107627044366783966965562365297252807188036757989899609245217769686/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^20 + 511354104838973996452140835415969876068197626251257156853947981877624590800990063652701054402726219108292162421585007071029071481397119929018093168809357170691906799245776497991124370956676852606994596328339534468248616528719698889351609446247165720/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^19 + 434615244628110012112851505938677243155773621455030950991893655430741155708674029863444944921515967834943125291877992549999965036485446305957252198709267117053234077360539202646324761984609333346680004646714291325376357284068362340339350947798519632/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^18 - 885989960113084847520574674229242624182038234453386440839603317940069040339043475568905084193208994119606056287773519905622047836269257973824449554282512746482658426335017436179750027842151421262685956941857951584391192013393215656356601686326397482/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^17 - 1540270866286582344504302074499108852731662965718528170347117185813655099454654669566339724429768663680595758164199876673824988921849187692045980519273264901906484315264103685134603705636280243731508059941795942319584708713373476656836301665515384716/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^16 + 480776928028893412608490375132551591082578444030913146590032110562337632893477648328447142266979614320058758993174388103882018813118067103019969194549231485546917702992642475629104052546151899940288498933520271420742747778539706327429808370875103712/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^15 + 2099778045442768266459495694961932142363689081712385770697683057490821325888526899261496678264343509900974812004417810078789418964438879487262029025316313654667363137604121414776208887582086830084922085255063056114781660655411435592067346317001699147/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^14 + 226419911910624550452460486197349493920346370617101505448587023781106152313244333328867070851171856914235924228770203433080915251426663291869719230675540953649807767275230129759384402227767816162642521926047439334219639783144733083794043143982773861/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^13 - 1580416243485137341543483731328888427735350291073574341494180596630116626113084719482117731598159490667276521596821172741023218081426169163548944249560402492602743051412897751026901256077403428530390201864156384662194499809647796275579492976688063568/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^12 - 416144501183289562241693657360098116055038831358092621649584757301819267735243952399429504896380413272981882582790783999824404380961285180763814283645440339335142280894723287471490795494106634556803868245590243402426388935014753800384522896057489486/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^11 + 735191697656304853150879603046675844173030112236983791920349608793049231274416545709853301586581564489330081377675228974072087099323551022193364851172485107253499656134692645816881860315105381027289903827357282021966693921237153461078295562111600682/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^10 + 216168646677013249142192560811159960638804158844991626374710583088909943245681818982100094231924955351745686254198123109395812942219481344342032500958267102339688474631312107946579252406277237474988497709164790133447117561557785625005963415994669457/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^9 - 221853366892509332662404155390074973693748337011200155024608431049126373753428555136263377414365602032864228238948565856229170645303760752834106672910203814246109960995042501030200867668339380686736271690760179546794680988429136788461038573502554624/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^8 - 53990975845467336496765188689930550128433839601654750581590354062020925356770716877137567988800410218594357010848083504737427823886787608400396923093924543716263739623792602971490081622481789608512686026715258055005471505119425313713860941058773269/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^7 + 730718469938727327459948266920680889158735935025165577320202774805315566341453148948348998940867818185268088472962272368889842040448679816104323691623631570671398164079439040410998122023652017191887183167775978667865688718545502110939487886775749/10078656238466961441582643680169655350941159251571053941060111765645846274468549198096405581600712777205321487665484728944567980582480499453658918363393096968550174343442016228697244624757144724756896360667989687842312229744027904798934702881*y^6 + 6492641111830932706418566979323211911139844620881571517434337993167031343541354302458650317147815930164232500161393595680214712503541264548403235155969616255568165579463633586435682637810912931943743635445106615637822534110866116458166680617104905/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^5 - 4843826588098489360920476312793247702229583187427161869499596021904084878965466775298920056112627557322258391125462300604178219908392350386885350463031788539728894750106966646922569415576118835890352220210398149793100272947774654356863069744295534/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^4 - 244144341609570542469965263825437063517657994505366613706108093963018344139808489913888729726325625968847373804154211176598253566002516672528849459810721522216324049103265356886829072463473740884204352713546183993861472472632164591563132673444777/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^3 + 239675190911444272129657905255989627105746236249124234943394087333113448644276271195054920744712011539478207989137562063783910576136608221635036934202675021176900319404960064385575338987754167416620069211724331202402548313974148860696170573252905/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^2 - 9752299502532196390026836990393545062331631346620307069136780487649575073033039645502168253374593015320826026389383745095636305210345271518186891704592708790522585091518855266565477199592815588112386232017390784342367308711640131139973316848803/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y - 607928668220665800073341904134213562914224229838136919334233012179910219778582150715161110505456883825280999342728394365367308214984911186688763613620934346356678125294853180447621203984150732044333674057773111442741817382418895197483248735121/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979

17579781039954562325730209930779690389542341905243862009265221171536492985487705929885256960571323818710738221087225908055123547593393039256330965900560800815280049777485561606354247687610967984767186777472893213556590649093120378552019/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^34 + 27528456744032010323257396621639397399967623556616877870459189682096762917216245922585142084496799000986744689461430434618174743180812772049558024194286916171246105475910190685741815568458207967173395344952230518287632222378400726816896/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^33 - 85772443345697727535197460167470735832420135545893878197129111081978463985243246722754351939069385326342865344292342178100593987327000252940345683669964645985402708353193197826335845353471788847856767708753082250459679669102102101482961444/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^32 - 4564734543568580228128091816612795172961606443915677941559795312811287022963293702978652161233080498433804901048134287090610512171335424330826717296362681685634890438996127966399224903181807289623228229661525507814814993027918224768689938896/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^31 - 115467890115193055980054807468128223444271958115685208174421103164599113782811695172640116581960737557794795043846946222781876757483944154910764307352662554824547707356095610010822643481466566865122344736092129301812957198822226522499752145935/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^30 - 1732870361180707923079193223845437474295463297089673297912453038357922780040016973016766264469660190554529848666982895031731226675207983314880254449884057678147712627889736840420946672502407136720459448261027268994901415954103839757190144558218/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^29 - 16328700911257408073688130654674780188057732840898192949708454285612874907336902470708473502713782452232174210971138072082596300943092658725726938772485523314983044648148628378500662826886032585460969092841836821780693219580538530544064137329969/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^28 - 96115519802384979731472303684915336903957081967578748994310016460790768429998909474036950091582571724965118428761070978952314689489706994383955916919138653478544116881298526956596097488346009311123581465676623558214615065109949298310679378255547/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^27 - 327007838445808099300958060291015600348047185675918881780323560545260883509332904453832740037080460561566508978706996604448192914236135819196619135822769789331149357615200918281293228250754730898273509028703324017559443581595944032500003027241348/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^26 - 525764885724233771553450099418688175065918852409710071453774707171377521532844004946843447712375905741099068550518172953908890871636141168402094826361420655032010799237174483628725151929565579260378474065802045945847905111173289171529886104469380/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^25 - 358925879623086006468270514143400890988550313426926005683063382563983275895686688859795493274383137636108341622506595122915265703597970496867564655593747039643141328428483326387484893506530882529036344169457252730956637921237309900062044441567415/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^24 - 5381807675695148288834461249319662641993977039679930071835820312608912345579560765203424828173579767712265455977303423436492473892977554197333295346477516058384318506035008636885154727418301741184585856350870722443903725509886272762262029720610129/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^23 - 36582746948689129683537676224075127384736931432549460895165123891305208176944751306495824585581539694143894893078253653772797229730484489845184448400056333116329302599897293535039990607342189235532831433503773361387650379728721795904232518791039355/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^22 - 75015880096074161356659037837012145589580121922378564826832983668854759056039825062572825925466681180800717411736284021130602713098872764507694388655461813759439427265301141904080935629529592126140844655445405580935692249699415182838445325848046387/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^21 + 75514010942682689514917357897229682206658091450264377792081642546987678911532599155065809486253870604850916330608039837979951534954932199118070113149110285208994497737238720559686808107627044366783966965562365297252807188036757989899609245217769686/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^20 + 511354104838973996452140835415969876068197626251257156853947981877624590800990063652701054402726219108292162421585007071029071481397119929018093168809357170691906799245776497991124370956676852606994596328339534468248616528719698889351609446247165720/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^19 + 434615244628110012112851505938677243155773621455030950991893655430741155708674029863444944921515967834943125291877992549999965036485446305957252198709267117053234077360539202646324761984609333346680004646714291325376357284068362340339350947798519632/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^18 - 885989960113084847520574674229242624182038234453386440839603317940069040339043475568905084193208994119606056287773519905622047836269257973824449554282512746482658426335017436179750027842151421262685956941857951584391192013393215656356601686326397482/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^17 - 1540270866286582344504302074499108852731662965718528170347117185813655099454654669566339724429768663680595758164199876673824988921849187692045980519273264901906484315264103685134603705636280243731508059941795942319584708713373476656836301665515384716/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^16 + 480776928028893412608490375132551591082578444030913146590032110562337632893477648328447142266979614320058758993174388103882018813118067103019969194549231485546917702992642475629104052546151899940288498933520271420742747778539706327429808370875103712/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^15 + 2099778045442768266459495694961932142363689081712385770697683057490821325888526899261496678264343509900974812004417810078789418964438879487262029025316313654667363137604121414776208887582086830084922085255063056114781660655411435592067346317001699147/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^14 + 226419911910624550452460486197349493920346370617101505448587023781106152313244333328867070851171856914235924228770203433080915251426663291869719230675540953649807767275230129759384402227767816162642521926047439334219639783144733083794043143982773861/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^13 - 1580416243485137341543483731328888427735350291073574341494180596630116626113084719482117731598159490667276521596821172741023218081426169163548944249560402492602743051412897751026901256077403428530390201864156384662194499809647796275579492976688063568/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^12 - 416144501183289562241693657360098116055038831358092621649584757301819267735243952399429504896380413272981882582790783999824404380961285180763814283645440339335142280894723287471490795494106634556803868245590243402426388935014753800384522896057489486/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^11 + 735191697656304853150879603046675844173030112236983791920349608793049231274416545709853301586581564489330081377675228974072087099323551022193364851172485107253499656134692645816881860315105381027289903827357282021966693921237153461078295562111600682/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^10 + 216168646677013249142192560811159960638804158844991626374710583088909943245681818982100094231924955351745686254198123109395812942219481344342032500958267102339688474631312107946579252406277237474988497709164790133447117561557785625005963415994669457/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^9 - 221853366892509332662404155390074973693748337011200155024608431049126373753428555136263377414365602032864228238948565856229170645303760752834106672910203814246109960995042501030200867668339380686736271690760179546794680988429136788461038573502554624/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^8 - 53990975845467336496765188689930550128433839601654750581590354062020925356770716877137567988800410218594357010848083504737427823886787608400396923093924543716263739623792602971490081622481789608512686026715258055005471505119425313713860941058773269/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^7 + 730718469938727327459948266920680889158735935025165577320202774805315566341453148948348998940867818185268088472962272368889842040448679816104323691623631570671398164079439040410998122023652017191887183167775978667865688718545502110939487886775749/10078656238466961441582643680169655350941159251571053941060111765645846274468549198096405581600712777205321487665484728944567980582480499453658918363393096968550174343442016228697244624757144724756896360667989687842312229744027904798934702881*y^6 + 6492641111830932706418566979323211911139844620881571517434337993167031343541354302458650317147815930164232500161393595680214712503541264548403235155969616255568165579463633586435682637810912931943743635445106615637822534110866116458166680617104905/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^5 - 4843826588098489360920476312793247702229583187427161869499596021904084878965466775298920056112627557322258391125462300604178219908392350386885350463031788539728894750106966646922569415576118835890352220210398149793100272947774654356863069744295534/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^4 - 244144341609570542469965263825437063517657994505366613706108093963018344139808489913888729726325625968847373804154211176598253566002516672528849459810721522216324049103265356886829072463473740884204352713546183993861472472632164591563132673444777/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^3 + 239675190911444272129657905255989627105746236249124234943394087333113448644276271195054920744712011539478207989137562063783910576136608221635036934202675021176900319404960064385575338987754167416620069211724331202402548313974148860696170573252905/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^2 - 9752299502532196390026836990393545062331631346620307069136780487649575073033039645502168253374593015320826026389383745095636305210345271518186891704592708790522585091518855266565477199592815588112386232017390784342367308711640131139973316848803/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y - 607928668220665800073341904134213562914224229838136919334233012179910219778582150715161110505456883825280999342728394365367308214984911186688763613620934346356678125294853180447621203984150732044333674057773111442741817382418895197483248735121/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979

116525114605807912965901082931321793382132737712166030123430043938347447609469576467269242663902739351694119270967147861020078942924360751120318219236077295395570555661274635644096584643528408260587421384333334000396449992486846728859283/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^34 + 11966506256281221825911828503301115264483451614220726803936450990444035710560553977381378806494733797315195752100263161329685079910183668316435886173244541387278359496954057478787970907526408649436182107439686675162507956182968741570607430/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^33 + 534115170535564107899340002762570030548470214875162608987798067249232167003519035899630301726750683688045185801096031029893396576702579495634097068614083485604093183945205556594692673574443613753641370499465651240584653996707025689942573875/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^32 + 13736970414707907357544773241731179195173698819518993622390242939687569543998277645581756551348570664882209037259729651041361679703024640693737549911783661855982487383854352133145497920614289923297087353664280466511065350314682412893948183381/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^31 + 226105681099379500013887750107829457807645915309269238996227205615599985117506020907012168357436907346287040149290732825764771470623449547537945343941269727044002732358032542344540544870323319154015271231967711701083617886078897367595647939297/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^30 + 2477582302093618575924386849261017823380460719623561564626217100837780908839772333796413778000367060518816473237919671221813919270899020586018742469602819858491815215761980827010720538062457294144377078060673665533727346808746001065352612983369/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^29 + 18106439724708994505570124946794184726845547403035064779329905082160209449323532952936009699136970795095871000636319513461917192068854145525680848321788247830348095334809640192426123399443506207159768520320453350483660902619817140907996252082704/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^28 + 85119541040930968371014926836070490564761568350751641651455262257597712533150058759660402526617504555967958290198204904707389703261529523502096686017523703799220836001578594037260979770406590691933020557826916216047355773243681339252245286023194/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^27 + 233827763542396682112978462326432338328640364400250918455772123443694390265196787092500483882063728310859362529400757385102442366216464338071093109753463253688959213961926636021592016315766457277476306910316289620760693410224754852286089841639841/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^26 + 312586625455596287210008131822240338223667938683775618990096594260498617260817257201747530798574897718749899313440386793465821807049672647313981914681687681819154572064642775266881039431760902258755629501165806511469471367393562288414851893269232/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^25 + 626022894427266931801147704627104511317306232792885898152086872965540818241511708906114513074364450151178888167329041976489607931663128971571684478167667795248883826490999897085582240362619992994463169298419518303308474580825004808081007088628114/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^24 + 6478830327303973452162645723708870310977764501853603742778123219701811004933572373106399318635928547259422117035701074659556307931272344975978040388300970492082755026293569319806775752496939607756834055204585107522420302223822807262469761596655082/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^23 + 28386104506597343943025091999798456350406371905030088507409495378366129307831031230289530032148715821942215753341950037746608446193495616161811108794827166059799792077946841951121695148170932159260338573211360196426818047798253805301756864270035273/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^22 + 34270553451675769100678834148833774043464707469200123126456601540175018300458648189380196086418316299363456962671065029826195701080073817055159468716552049719268072995714757282751984315193795567406363534051205200082541661367449754418020749926236460/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^21 - 101304588692999589073179975251687956800262508484608392744497197889089342320471945777708065929767481809854168545545118548590067118546205921088039784114971769670853791114233966712832062584045538272821580728502017484107480627900894357425223638418021909/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^20 - 331980944148470363314234061069345881086480555344261054913500421238717035939719257425271536080742488663219638543445532583969552172716119321166486459616697046965482451788304346972925679247220029828059199541940827767817872274006423992462802646263173778/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^19 - 98799156498985312711149459070835964407130597083037405323643290346224692758116393476348472620662883036278186315363650241227001648844701680754211089760408257170546659527835916366306180930301074233506284261920691177203894922464319649018323939988083452/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^18 + 705415084542353475272452497572807959999924305040183707090959330295708943789852400991290621565685632659082495483347249177619448588075948266169696446677402111027600617937742725503529408682601676345383406068791612889321982328670410805526814199008848756/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^17 + 663878099249928570101722102447221345165893911946644695655175172415271105937302106414672664019045819306552296159741786686884659048576194348136950377269497123877678161477258656751358910526515696150658383906860604740770427568764533403756539058672967375/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^16 - 687910701964437703561438521179696669833619772433974975384245746105813864700220851579785935117570786841268843385995516474656399324958880360373989328110260879438972120156315456587747010035701294437642605188084766944176564051017084644053535147448842722/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^15 - 1005840564145637547300146068716931214300693576689430995171521392601768973500109517094702183045116690217308990358632489331630670961015268250024857326771553845603897412713395406288131633630589234918328135152571148344503409257517760526644650565587472951/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^14 + 372554825741852086942100382832045436281185891072052782656865362150695470310766140026204895962247715051605003849981724659460738900489716903309393845968816180491384367141133013107753382358452681742353145399613313370885679934308738147575787199799592298/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^13 + 788555649443071418755920247750265037963465557109927852268297976658819551865474024988140403099197436975089583245262783888081302027731927935397377518597690220965770684689363849689971372860158058793690762441349985166405133478790419540114695020595739229/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^12 - 139780992530136494456968618579779327158556715101875578277241657160357290486034138126748269111402349140414712494401033387521023640007030281347403671137865055791982512978278299119266322667147468709168126119723703845241054687617636310142994524936720742/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^11 - 365483752551228165442648916883523952094654481533698601458597020461414498764213501887929587321829845802790238588836414479087988277699139344075026968084771162814853217298217665810690155639003509425030231617956781037579579110523543384623995091596675129/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^10 + 50990862029835235873917808576730534743726809481933729777850193140920781927297391294159909383179407934965564984722690807025088944758004308318332873719150791109527442086013148129245042182211027216415277842263547701552179012079646341119684908548499730/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^9 + 100977094879009584669244316028287957715130771446131425852962589265090249943889911136696836155558208660381980895569150805302400191944513346677344593013370216314979819831378642562394513689655944556379388122341096370811876141776917613338782227896441200/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^8 - 16411305378649577099257160671456034856105595202183474004131905351586540110427341115559630963641667858949380559110133729299564160957772919123376191758227242682345385539994918153230398030822011040584740933758183863493307233417975912673141822712176095/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^7 - 261136297115199846983885497088479925252607403924600904615219566039885336485210770563498569605932858028346671339673405985346792758296691666667131462654062759056616668792721940972574721779795987404586476510801062446145570835745759946378959501448473/10078656238466961441582643680169655350941159251571053941060111765645846274468549198096405581600712777205321487665484728944567980582480499453658918363393096968550174343442016228697244624757144724756896360667989687842312229744027904798934702881*y^6 + 3035890113030135698583732468947323490319031969158315179375881347742223905530034069093190885058632447942908725216639006075914536543947893926424134762221879032488635711901348881409720713045923942731953003243885719680484181144176434765734024976156837/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^5 + 1057467489482029645037520182921918500915140245028135084300719831052088921470543877518036086417773825563205680736634806952036646792844779564000012748669481677575461480904220107074233639516632720970715396433786277982716073037807264485474490070963136/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^4 - 226166898693975717741713782614159169368445699481663922912139902017097711806929200713091603010406598101385220657271080512662987999866033615801267262926050853881446266953440310650157262164360201372961688629154849257773964271123269351707195679093880/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^3 - 18362007984690690802655042801031021369971076366439685297542999935277817822618612901153310611680744986558151975308675792941098796437262504584884398875288109513648291097114527452378617556586066617510037664979191771732147621159816113944300536740424/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^2 + 1860335340155301794405319245332829837158708731485556509912399946410954861517630792201236720884727366450597350066599871023611170719758803478171886183672847615155458829730724210689286703503107090618903983361616691113932097336138508351782049174930/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y + 688844049998952759139216152167631340439273030072482173847551853866947608158165633569723822760101415733115560649655979400956747817048009070254366236024589890643525178753064843638954947359000459162016307308407341313263683190920363157277481316349/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979

-2194978479534866508302081589644077916236196954443698353890002675122407357276812705628268632163291719336340573085089492012213264816401860672507799849637289284249470738309004413704996733373321494223119176563789462106516903273225076262940253479243/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^34 - 204434374334484627887415493031358847947393514821179929378670025660260070242471041282163277551120823856800188150576358207596470015913793050784303696954429619934270262430729016709221627213107023425802361205904868421458443037060701155923008149958592/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^33 - 8105626298856425100232221677059261949623546554871250589416898524123342356076074968859132327293701447321137019402867315353718400777145787447041865915524653313380206280504974148394575504486135722439168703928699588772013791697025462808732297185095088/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^32 - 181137452143743748099469947596782057384459512905627919650190340484759023829629712803960357896645665248189192592654510907067923421807436735842784154722367627445599513487727532654276110918633281143372584770423872892518692073251184717919514427174227961/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^31 - 2521434563711837754113607984459237750097475549091412657460380023842058156192506524839285945097408775431788520315328410362876157865222518143418774462257343510053969788302995030163564498067078950469487812160078477653398911205247296959420884912944154354/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^30 - 22417494836938414593329819596057028093975766777762733209641680315149613826313317162980531442582651218777485512187476521762080634548140169266149753731557276773001395496217958338650526769080686111023236835249101430058646213330906347912884277713233342916/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^29 - 124498449065724994579906094032302013083610062725688330105421467772328139522561903305199180248829460815180549231357655420206829385007332663058847817411872244560927356841030624099938636469367222758111697997293190499684397826412222981966994787068344000675/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^28 - 390596661294306268817455027705744679365142169751983961082268372780562350508595297262352591854831119650616756246257441483237101483394762909038040432005944073162240389378549131548545864271746798498827083854743738710391238346458199389883749701741691177304/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^27 - 522807200464959292838783274505248968176732025140422603441059129423079421746663685820357069117506833989562834885731831660773902211463749962294336212577102864876243452242085836301656024884675424941402401385259634103473092904307001706300965396143064117677/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^26 - 284448447831934889644059641938604619143886152437196248383014073801538788964076798234188594788491494224227000919100398744313778803905134648831109013835415074052054005677825460683467234575805352080403642589336777629787409770366795018962921607846756580489/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^25 - 7658973424852708733465270471277551525159171023765817137727500001926125149286450784780389480622377167058692783245580164158391472934527177545904591012085140784391137204892343650524985245288085288628052194450039238629405419928569721239397613532222324169928/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^24 - 47091646134871616479704887883032834320623494426790393946536582107711191331433246666415330891668572574710218829755958401884657446787073109562188842534473051455089573556681128436480976509355624828811513590441168680338764089594897659716636687270517310088204/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^23 - 77680905467212638506963816034394146680945785941715459009692042619214698554881384600739095634379597606786425165770285042391762782243296286703189958634700211301404476130642301386639872499311793689842643943276502925666669259556471499545725341004877362052507/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^22 + 151486021131256121470601092461143915416726786017339610494017380914354086405698075521303060085487171083431067589962188159867346426301497385510982963558659536125260122418853324375189753745984857809164902184608014938568806269781457358473577087663199581173803/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^21 + 637599458503772765183322299601764113213614381152665734044165100651413310078163558543348656532713602856684327441276721804439677584531553735475446226047954860877630433364083568556595891176263031012895132241742584361200089428770035228003683375862423208330336/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^20 + 261912045421944164688220438437415016881175732248862698712172355093595497974519946469993909210965699646556129885838568811764614705810557894574653698193122441241573263511213215447788644659303720623636089786323443162901239449399096585446778682192467187434921/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^19 - 1418874536830380125765743030039152150052380763953421246413670273050348039094927723571860414962315919357413076344486755268568287480330910467815555440512973450099431343080494661716837398099936534492491568031648878267110997534663537707454916812798971174732682/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^18 - 1456342413760502613517321333377191266026253502388601377245292064980012128491342415305371916880854924226297583212056050135561626874031592512489001931515178925153120061390907194173638710016955943035998809194424656796672101551147295838762536350323457850058103/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^17 + 1520267520627976730218520632960501752028325868143694692800486185232081242964815400928591441079018924797845087427867441925016246435428935398817174163903592846643805776211805080246880714801438202781396007915654629163934325523943534229715509967298930214796607/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^16 + 2338260261668747697511097298712850227413196827235901919486420604909102786426713102467678964463856608890796556747143010775438587889519808020918893745652909973107560723335703986947920518917205720150295399692219802407674468197441950383339305147921181948956974/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^15 - 946995212902752769611852465826076547156755456230988363428374359516379833120511535081929546410617422950386458713549629262500363726781157937408858217648098231573629653991230055259343705574436826857179243513393484581741622030467064749083381462574630049527203/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^14 - 2021500591807881995778168135164590058741257067289988245188441592923373374322885237433369500789312493341568486160978408655351911674909887321118664466913757895524799301429680577551080567128727546020946346328268845850249305301609931492283700789075128578441884/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^13 + 425107063829488210395958692385085098561615472821540210119989998303587686437457601633898396616640831677421984588122271949478317221288967169137135243547771991764102162251093930627604870784725082785844476596688297452880620089559927460715996232330637810662674/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^12 + 1065248872625604384951276134491038547612493359797253994178301406146886908512534130092338958397038603050655328692384959316958826464296095470577028689623252627102962139537734255510207142939119949323225687021490829413146164345461110462426988377794735805992239/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^11 - 182558904070411493208978413991391132449025814206109485237762619886508368137622950961221696178350871876615954234794562882347802293162370586908834728889207940149995558414430368372630073707628267724745879549149373136458886072274545792178150036901067348536889/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^10 - 348883869455991079526946417211109067488386499488265995701647464556971325704260339374018286981815145375727298305327459955179637158856717397654931225004783220836205789712428602080013052948193176176587468810377491816232871235234250956866493309960738029473828/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^9 + 70733136536065957099161187934191381627456913288430285210950497322680423846901321628065409424002224841843116602823015165952228163879701255995214979477714788081686288541660424064311150722520793235374471148722018614675645155144545772004159282106505068592939/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^8 + 67486563452814188637193696778926701766497319650979331901240424016045008401194418655436078494509401110058945446159092802419536453556843044519993536193996918551845823616381145341179252886543510440589935176937617606497593238907436829199433322306805105519754/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^7 - 304133632818191211622538840422914372857320393742407334246973173774959176280310217758725573331080018250413048150152968575784505057159406295144682446871982853839813138790243732923426936582148689007622593602414825673760163565952123014747458948104445214940/207428824043888533429212389581571676777719998556583861160958160248757162174837211046022123274924269667662721537643341206408153608368031159255754198836993328709731138162380136002817991622126795580221683998907895765482628000361838308666875119993861*y^6 - 6515987307543993235729233696380284948018431237058927437571172350500038764286216797845385303380808100869542218977934390727853285978519862822548269154874770542203717905427352230362994285151871277864082208506836531946542314237776305160622294985900157307076/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^5 + 2361289812439403174727799263024736802744936155150293092490932198092569709490494507256503542936200686108102482120597288665363653714458826342114239539514272731372215554601346129665096849028915596039508195103052179815526721471732101514514040452052738539225/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^4 + 146462251283689219708356603426537372811517946438702087318192505775397124078713430587647741693173125944401293776300822196133702564761251007851567229548799714643802034148331454127103285035966972028638908260725487275673955500801741924240813612182139688073/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^3 - 116994364491868476018531568333776059450658090612792748093184310953809076969488435227240186772195077373065662807321141890073414266885394621342294782199941196167247449301641284202198156652254938822407406795170107548804427248734597722402944309922221878217/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y^2 + 10704760413556193530419252005558601627831905057480874549059808169315147093643498947222089752876952779609040473720156540302284449979083433243451271321601609468127634692829659562655526708562695972853218899491133439977676153676023929632982552992069294863/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799*y - 70250693754738528357818258334712176254782806069443954240325314155494183539958346766226705752348314174341557513846330393757573278465894071277836397336603189305643337377161526700494478942807714584425317515337218406133248098157298462338155327291652110/12238300618589423472323530985312728929885479914838447808496531454676672568315395451715305273220531910392100570720957131178081062893713838396089497731382606393874137151580428024166261505705480939233079355935565850163475052021348460211345632079637799

-47152627096743285206976076366780161643418258586728222809231242730341974154440353402123216391528726992603526770598581832765738579814304563803369190086922052842305242749433099007967261594427047951836667744537174763219775849320390517563176477402/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^34 - 880210195947240117310412587231160287786437157254021237419370965952108730391018272246285479196433796408056387770761951975465925046284561190406309822367272701144027138864284383531317161862057697250236292722527502716408562362422209893945256370412/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^33 - 35000327178494533506378868647109876408713485954565439502935871898706831807059624055279236111867070160646686774629545326029188254282050054332921667956257152805408044371811729247945788756064122352007794327726458346883078724641186279098318172532978/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^32 - 785213932634221297545229826264035216220940140819603955786419144536986707104568178731442278220917201997760035397087230197610730216390515547881107150043791039036316928511544003863465335229875853781257979462792785452535122810264002982069819110974311/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^31 - 54948565476055019058522785652410485747465799242679947282628149784867275545850206694094038228954908878815943568496710314437092478678557028736411533007037511700328639913081471675099460890180126419486056596960717121019010598730480777717223092510127749/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^30 - 98509483460141900615445883372732756846942168427865303143165255919986483536714689498926821164096615676722667304089965159908051310782710154604741558614430666272339107581606050764698798619740233253098810338116081328167311755097802073417490732740178055/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^29 - 2773051860606888747883351734131673117676409874325270223265995001217801152264214497623080961246556857082648930362109261410009977483004014968337637629451920881102475518349761702138834581964026727295262444238629319964326488202215885948979207780477959708/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^28 - 8947679843783597100246228778500334564340918955934252838106117013281436122372088616273594247401515045146754754378849647932321047261438362581052102907366507049251045771114028820883195238954230807733332342593500340513669069038077139441641366898248806441/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^27 - 2608065836897866702397601659020685785952193228181338414699495069492086315839191388668363519148301773319540932064438476665914584559691407567993431954975449907093547417425243147097095606293006747409096842118397936866156100573596375838333508420045004529/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^26 - 8801169209136063164765022149481852949390353018801562999339628524408942830563409811214307019222308720901923092074459240602065069311477647427698554796058438947127883417406546875992164811868558184280449239134988157554108593952878536861868987506511773261/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^25 - 33286690770277374565572500696198192075803274082929375545875780541979610752226272005122625883103293165477333163392883509514543437473545642889554405407335134500423928373651494085691460666041270287126020469380032737878035335049275678600061672610790462981/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^24 - 1044872018146302439597736113813708096560111236374558048948858932961510117933520343613382955992573190916294197903221811668856203558067241327666375133772890294478371027493977793241215370190187717756572221060918496008176337455898533850528803447029310112703/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^23 - 1878387913423819922649289077122816586341546029111481574413436720263385670047769010350554116971878297874127684550867164814967488432968206873367415862801326830466877918260480834380949020401339642093620359701872958022252203313945110106682415783094875330267/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^22 + 2869607531529873651417617743014907772968592391692615402494353628643234099289020606185517308656444527614133874320103082706856208944141653639691577014068282676203670181788461073878495030362596067702894081060202646284122137295139570756447568191127679366484/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^21 + 14246982377361502735140187685976082207643737692121648823941066921015376210668113388571478688078044399710158427520998884547588223919160739000744470375750954766462484281786725339824342943083363850153874005808250527438065495783068986919560471795167702547019/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^20 + 8485131739551959785951394577934775566848731144305526564417465589686601688321325469990175742832967865869152022160390309101624031767943449168428289994322640000758805223436411189439941040162166941101690546012420991121319637139371368954288668839964941574398/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^19 - 5729627702755535223907658150502412145367934985962020244428788526529066531385763254946808915046107503345777644159087475803486310545541222778396724022336655229023286578635607553313504104496915017417239889777409838659093975983236466261031178003052575765954/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^18 - 36873336372677362574971874987805736330747496550118046096184695177149675194413688164693325818218040174264782746611842760219652463367056805861726610902362058196744139377566253319226258490716929565627176951452853450069175511513978111067707224357259683638222/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^17 + 25075615207220299728643201310244793253378617530465446994961358330001630066650843125347428883229496347562587697537454696022329641744993141990821606631109010159775453877627069444181885985294085945687324085809405403520594986932877754178265784344846445283978/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^16 + 54828451228344151838132040215220081128238101074986749260896280793093137630758209049140631799845444455601371384772252129630524213013980265931265346620739215211171210335004321563486254324916051909207533344451740886364549358087571590384679171673257517936061/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^15 - 9288040985886685166161875717668272301618754860556450028420015906840467860464429302474828420756740829060282985072378615644740016288643930831644269954904230727595834150200595247525049742182816581396197868003542230592412741707505140334632965332574959656538/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^14 - 44762845783634099420981837640131421925485363108107185398825340883322833533862641048628299433790752260210568509090725190031332570581535213386870745804000621294225521227057588884681723281848081676678163213474905490444136071555817612184539446304968588431991/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^13 + 247186938996083696418035107425572195157139885106645054423123011950385734072096248514124352168785243547666947491028419866795227515467752944311834927376995621390135700718100565123973865143652212436180198490387819969043593065198317623161829793344850306929/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^12 + 22567836036222162614598353718740131409472669873853060863834354225559119682344114925344063053808368868858924192855766035434657450706877998059945476193939302162913427049214077467402449795338038417169997954558789196617924599765550852486214599970604241715472/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^11 + 500855427130205307986001529243469589557430690560209918766391563226549163534912576866831275829672111982487647428161944180928422812886122110325215609659578402718535709112428690113813219625575130064730616035157010049771557748316919117285763004454037969361/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^10 - 7236245922838368305972302152598865206159647882280758677167872029494644917453318768174456024893051428269216256170935326964513705268790726036487872448269056851512177496124390276597113572399309506486408935554623124907672321712623507304268119390599872846776/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^9 + 113557545110040004853054994024787272318771529016918170033204062624326493435338051884948550538972462078605019315205558153421932827449789891010479013331833298959618613867278719661022010928000625185145877207736851635620192932324288445489503978508259023712/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^8 + 285763941632129418069118167714696096516288696427489857931229586373614121055162208442771512933143185721239842668083868300884239403180098057445979445820915005345727240107380688121193576340410555213529275646704384954228165632170492745794864381530262206954/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^7 - 1852013230557130238321885759182674226197974761598425591930898052138241428456160719200973041719630361371834568696063048719866493332790297521803209126654861036381108600379068823705332133405070140994935779931470797464984127845376598903496113422314169599/12144780767352688537107085634604434697884096898143119998977434677603244760734601783706168725828858896532412392636909098378204416601889001841658996627888681847102960083847629555580179772832359393332060114604927573849986236841553625282716316971605*y^6 - 30859544764377465591091805430050559414240677351822027512667069063217867043190441032341930124143537088570711516748949889108631199695574708744813298544508245772521574862799960040103307459454851392829475693637439392440342286053085224383257118761959609204/143308413054761724737863610488332329435032343398088815987933729195718288176668301047732790964780534979082466233115527360862812115902290221731576160209086445795814928989402028755846121319421840841318309352338145371429837594730332778336052540264939*y^5 + 21107335433727656989665817980275274950333910277811654820675151236294932343485578909787570917290275456365534873939159882486582027642453832577585035672845948196633706272570054308780263827836114253689897440019188722702201902677615694650898136426056175586/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^4 + 6603625092698094694079764795937341353765097894584656466731466627795749897887612313054750784862155265265526282692028456009003859730144032656893934672963866931250367595160845611511787134673225125640893439086831423639883708554982461117692017786481168778/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^3 - 1274221885228541212481404627549868646029706295691970182733030680073901250699914180783964364226909663537860554612178854731393082934723185443952610559276827560117093701659525502687696267134110880399294090501354792427528007473499216442615698170043137187/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y^2 + 14357360679098586505722077309652904612414888094738325918131860693089823443477391262149648574351829751161945050855288201990151261198500214803000488009085411313986548273561385824214422418108287845923725859805834226252558263892228061988143599682801074/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695*y + 3242651414782657478020770692213113040074324257562247784004822729452255378477509479438639740850177267180640048850402025319672491681317590077711807477636778312242846992241570965018927448297525602394263309589392242469493060224903727955749687034760271/716542065273808623689318052441661647175161716990444079939668645978591440883341505238663954823902674895412331165577636804314060579511451108657880801045432228979074644947010143779230606597109204206591546761690726857149187973651663891680262701324695


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

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

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

# f Combinatorial flattening
{8, -10, -4, -16, 0, -8, 0, 0}

# f' Combinatorial flattening
{-4, 0, 8, 0, 0, 0, -8, 10}

# 1 Loop Invariant
-1569339310443961263202464846705836344261968657591677916620588045155140725502211419451315291704480244355760172555400012947341045289998004520940795708027645131342587430245282378193858195323401439282162705522878608425318637105729668223635920489/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^34 - 145828417980349748167747517776565211046973903604236722744126523889728011110231697690107361404247969220660426768206750253789922866835139615972552044619012089594721066371483090324574561897060206490989016858004917912370349610464088811961226098423/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^33 - 5763858295914042033871839686504547623869473090324120685385652549735249176857179127246771839860960217208140908289159080530360053816578503679132438395216203548080811246656513844439352769912211442802777256118449494687897032957466368882920692603425/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^32 - 128254343488309533679813113061786964045876275703542542494188525310272017122445450772134139674530971575512751679265158228847976764939622035173513396365539680907760317658010841669926527085835076866226855381502460900041371989313661509450346408333215/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^31 - 887248542299543671059827328656809073909610643713438385086946287925011256736016448145098438379168353248024283728110038584220274641491776134019235316728206535588329248269965677270891526816545168884352304385068366127429411100490615511212666879123642/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^30 - 7814881608733861869098454226441741385398142436286223452166873524076535376296063290546061261314839107895912981615335402952864904807875546743016073374618096854564953532110523447721751826755453356744280861908442783581287483350664896428590497927304985/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^29 - 42703769264252699596850533579575127423935017835268215458563013420312996081940954533887036985487612441301204858849557417035819358476432196723683528816172457182545713616681554579597531746220632212015509964803487230991519328023272773531235818487208925/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^28 - 258609027537443205016962848976668041611600946114248354875013642445544304945918178500216813320502957721203790440827134340801224002591096194743077942640248065882753822844233341945400083261896594554947380218094744171035007680325042717814983949879357159/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^27 - 304665957745618931284481044374388902226684773809528243652434235547574795935142600965369821034138413337718917477109942257854207199763536959833029588147911907414101141280402741228948246162761874495832768085424901429824818154367136565411450611353862405/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^26 - 91229072837294943146792562225585851664608929013765200815925246882485288890313950583066703103238222952881458111612485989332254216316190499055914545225084092015057006042228056439858808045925750336728495066965125648843800988219366121123684279598447583/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^25 - 2688786886070001848199469589579363684144581365763763982576381837169209998668373894085174899930257583831517816675893702086279678469363933227724381727268570259293431625980153851031533101289950941411731390791608741002248898251651171924284619700667123232/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^24 - 32448449686024631242114500739000278602133661732132359006963075390209296223026822275375441456149246562436220864885503048186310247647867537875845057569438426077742226767781519223277082454676299729336330859900434913390612428655832794614183434463331181151/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^23 - 47802112250938870574879017332989780690668273129027423887459085570460610853817241852618483959164384477419264675545859717927234113226432730901458169719827371433198493504602701670800188741219615580306656606738502757635959080648673870381887708189501727539/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^22 + 123701559489192707677403588640694767661948120319126268264496995930996018070256565470206093705415033305149657601168312199019824464506499664683314554565688831148411799296882361614395967121224336124028099349242909690290796938194725797922860731434008692449/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^21 + 440178713120340447225886195683044138754751227459625685055555040601227463539264661590800289909551326922833857826810524906086742747474614321405999423472849507384531892605363688751166183729503543091402984809642938805741917922082084855334514316428151868169/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^20 + 83897803526645818001434587570597616759846489083004789729099902712425196512035222769985688910927293575740754406393267553901238966498538208322252276077742508601721226493038353701516277787562067305430307909950014614830339625995437682027305061099693571167/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^19 - 1102667090421200456461668038265394149688515358235648031323981221924696772594230245213180675669970074591038945121600579723672087060180097496567279483574993939090323676704430971633724243766787006918134351780464516922973431352418124271780244464925903686639/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^18 - 872198266249087662541627031468926945964804331759538794235681279072769639383571470069226112675362820783525311921666024461428685568000363433523057279302708208380374709009244739124258598476262698751296109020711769646978725119954574460348134493171222116753/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^17 + 1383232900618257352618258330684375460208493068273942840589169174472196413205390942048636423248029685020569068337982247060583632899500100300876134084470555983648651836895104591648598220639467444606259516171165216913789569098952491147883304723052192437271/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^16 + 1592135780489047089050119989361620814413377473240809745877206957920284001160463610711460735177747470152114818911059644362412598908450431641720667912925686120716291331611694543620625589759663306143996771961996583492001672548956260652735462915215011621465/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^15 - 528107407107173336774027366976827786727859610393402244336677361959093482335158606480899812227858510445865149329068772419518504343230712833893633859150365690528184225763841921124107494093425120734302712980212483803283150471516880485810014570343807989781/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^14 - 1496644663616016111144375649978681222918917780437354913723123904452710359020810568314117800416934034666373952156227627358851715110137772041691300232776770844799664278526979177520207841495832229664078601829511168404812683969955130721504548765500516702973/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^13 + 567338916707542616450781915481781167745755884729658592786667773587255205844002546300185278382533078241218318904817733375964708357926926051554008230581909062536839947687147550005198923896066978925554054660239728863718938700459087798511151614793281486701/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^12 + 418883266389483001258935174519981135206859685323593527576590352991019270059002385971455636268071018518396914188607755472734958723917146969699155694920256182038816613707447694253646376114107849669986497115138113354014024357127249371103416354192872055516/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^11 - 120272841472574516930905963664676927626078966019655157808845089548471373052046333003468245924394369477125603726847968699762270132399568745792629701600844164203393139406396642452105783138238892221217012181983819576101863606602874939018449791299655095926/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^10 - 142940071002560896491461737437599628076645210805593685683857644646092954382546397138105208309481816925503615850354018862349126326518950862342715377505308267912051449130289167691477011013988824545817662135284888599645262218730422306648544540696853624915/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^9 + 79072383966850854597441366822185980527206335854875129967194725616281459350487014672141005046130230419503544891102524416039048539960286379043107937570961581261805260578838323496615845742600757636607375252644822675749324745518788392885124303777683381007/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^8 + 28602140867154776659877379591737721675611131613835692556591157752743500470806091232975668868908684313896157091626661005382575841813114104459737321804217827716126574913925624970113089875400619922891617547233955250128375157471679397933576258682897045121/594640718069550725053375977130009665705528395842692182522546594173104930193644402687687929314442053855113967772263599007729510854366349467765876183440192721144460286263078957493137432860671538760656885279411391582696421554897646383137147469979*y^7 - 292892827836234024175545486522067042157062437986778276916370675208259937481627975209064707671880066270719194648781216389058343775146014978845917368379218148905024606751665364538000151523328728245568956942783623688801727135339256393545806609905086145/20157312476933922883165287360339310701882318503142107882120223531291692548937098396192811163201425554410642975330969457889135961164960998907317836726786193937100348686884032457394489249514289449513792721335979375684624459488055809597869405762*y^6 - 5942679675288419361788376577197163170162151182338030394893534282243764137717824586127714182102597997016377497898543685211806118236715552034540284120897603488042108947889378577137774609435628047937144518370571996742216214586621005235597142443974564875/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^5 + 2057079245013527302632175711691345916840207306801684508149936389911375375052103492467798891678404751124000116598755175309650709334680115299689972802820397704295712445496668740463905088108041770322181613831254936686136051402288241141973312514730852489/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^4 + 213620211621282940339116227064549871246255503773762996867837526073781859534874383203467170998351054492623395602475917466540705084607451797781526972972710614572770197808070087127344358970415239780787514749793355742125650506208321736472148281960174407/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^3 - 98003304026104314155299320278346932877708422817008557662660247808551696283730013923941339251855994908675718483478718044323387018699901907525512428973209158536833204714816729947662000885972203790434936238924163837257048490969536126961657992122992875/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y^2 + 3455259157532470440687568135427654348357425880190131711069703792707340951771829695532509678341296845048042406152784408701437331668634029779561495901838835801310211935597364437762668701618172752325803443834325791445400109372943998349595617666482383/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958*y + 198359350119399009276079249301917675906325013732151707841596470223339742507959073852258424505392540903737633735726415315740749406774691816430017606874134328381439093332022208602762544734244618095168026383165166434818480393693214996927089863894661/1189281436139101450106751954260019331411056791685384365045093188346209860387288805375375858628884107710227935544527198015459021708732698935531752366880385442288920572526157914986274865721343077521313770558822783165392843109795292766274294939958

# 2 Loop Invariant
223744653445470034248972447071353270384342726362853803919941341494582867439971020179552592527413605279255451569596052694771231941902443865446495195982223758899350224776841571843098048456587857051648788440218691760731577740296248983525770669306313248871801162324929354166792475873686631370655528378623019213655312324225290211694551186458101158494499626486515964571579/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^34 + 6948020553427539134718583088444652275768204425279083755720183743753653675693140848709811765737450600115564887292182228946867257244078493979585981278239012757517847128234978326689897385742670156923056807118148641159026871035344728774618636563725174525845518194046380674168249612021132424450801707398616593009270490405684221682904490541776430132082780955015777697335801/67606775065149224452672317694689420545634915183987131911743176701301235634631809749999666220266487165542737318457192472518579196171956604765977657239638020530865534220369161430654623671685892522585974000656678440243080497315136317647080883300278027867705572077413138108166869779558836135783975296238751794652778250268701032296629587556905226369019931895960714144520644016*y^33 + 103337977582872657297972828971527984066965924633115714865378630709061305872664239140218189985266429722239264967430184264399773623040550510749718103161391427192027398089267551334808374081019565931240147864755306469987921381154634076357027951316268941724465409412095644448596177358770484330315963252264164263421676401416539656106087188916459096366974470458287024708839809/25352540649430959169752119135508532704613093193995174466903691262987963362986928656249874832599932687078526494421447177194467198564483726787241621464864257699074575332638435536495483876882209695969740250246254415091155186493176119117655331237604260450389589529029926790562576167334563550918990736089531922994791843850762887111236095333839459888382474460985267804195241506*y^32 + 18481566235219668259135712026546647674907614343712914408760225315506561437272632382873809460865664948969272833261253242451316898920469076955952821239235192761224271562243308286022434765341226474637871976680513254885688941560302882546696489086026120829601871412364153092215069000036097479154418517113406581812229423867974172638603676055343831173933075744583388549199665077/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^31 + 257384955378739751210536731764149650805147038859152583005211033945300490780465823129355785939341914213610567228351907701292375465201907164400154257180800516063123660250810955874699723217934400055702715671237994736877224807067021541683669790530088995900417921516935313972754081374245921649796178979845253946708548508566460001416680674561149675015964081390683968926010521773/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^30 + 572423485549079023083527814289456079869866440544572145281997565956830562463237916567568977677638247992644302922258198437409130237106323528449206340710955779808604888157538111143740724253736375735811041201556252986685497585951540656100499447905386149665999342468283385972864254213269491048616560022283831090295023114558953735717402119325215472993532134566391070040055569471/50705081298861918339504238271017065409226186387990348933807382525975926725973857312499749665199865374157052988842894354388934397128967453574483242929728515398149150665276871072990967753764419391939480500492508830182310372986352238235310662475208520900779179058059853581125152334669127101837981472179063845989583687701525774222472190667678919776764948921970535608390483012*y^29 + 12724888988004327250144279194015621984779128134002243477282405843885726054240994871216287527042330314648718455130749904665146620384305155755145492080996541482614666970309957662325881536275387693009470697560578991545891131412307103079934764105782202682369814803643057744014011677831762063138298367574884911339608127005518454783631847741743221200763753562470145162629114710939/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^28 + 13314904238231347752758841123553761128002437725478076384844548942874565259712001613223928193438589167735943196245478469272883704548014997795861235903974607657416000094460527968804375754609291753922786647852560728806849848265733148243624557760846776417337343153937844031899670211381243863626761929802244939849567868605734095169177462726474767482805412660397608647906726219045/67606775065149224452672317694689420545634915183987131911743176701301235634631809749999666220266487165542737318457192472518579196171956604765977657239638020530865534220369161430654623671685892522585974000656678440243080497315136317647080883300278027867705572077413138108166869779558836135783975296238751794652778250268701032296629587556905226369019931895960714144520644016*y^27 + 53303005340726297382480311528752034592078792894561963645957763400149261936859919654043829068293372165930990381595854054791774383714996137116326944250034792310763232766833758001963793488497590243537482164087714516135812006799113175561936551244090702026059715128601929774803032874609770238929830017080049443559959635460176412568546397970718777528049792749583702893962231089903/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^26 + 3416076174496665838956175161805586720181401032772928010753342051682564081618425207044098604779055122049684097235483814075344460620928108730615284416350349624854537456180529430708508825574147393244825900432716163505639265602261503535712488521482502608374942588212392111781182966510151331619960877630442869432333564129359090794089948902404942202498086503564076314846499172321/25352540649430959169752119135508532704613093193995174466903691262987963362986928656249874832599932687078526494421447177194467198564483726787241621464864257699074575332638435536495483876882209695969740250246254415091155186493176119117655331237604260450389589529029926790562576167334563550918990736089531922994791843850762887111236095333839459888382474460985267804195241506*y^25 + 129530126821559536814760729087979760351545665609816531903550097260366034710353010728467521894780949435789470858739681176993926522577744209566026465086960873022269765827946540078362919299017563461352429160205676519183096068245591007706632239151586852112886284899048609478255973768700546404847345299505930395997133003424958930623931802353014254706048219692694615230405103147179/33803387532574612226336158847344710272817457591993565955871588350650617817315904874999833110133243582771368659228596236259289598085978302382988828619819010265432767110184580715327311835842946261292987000328339220121540248657568158823540441650139013933852786038706569054083434889779418067891987648119375897326389125134350516148314793778452613184509965947980357072260322008*y^24 + 2407513406299024971327557132957054337092511493697524166610111801650880549801914252083989378921960585892947143240189457075099169994044846209880758534528870207393610961159137584976292331588853884926074300602528890976773735502757000375431121598388793324942929586409981313731701577258793299658057615410293180555268569672600576824522180860927256094457176929288487007177496642695945/101410162597723836679008476542034130818452372775980697867614765051951853451947714624999499330399730748314105977685788708777868794257934907148966485859457030796298301330553742145981935507528838783878961000985017660364620745972704476470621324950417041801558358116119707162250304669338254203675962944358127691979167375403051548444944381335357839553529897843941071216780966024*y^23 + 7973124874530887864349402952190645394771361466229973884887870046643966711617292952388745648366156803123511158026253910098662301191447822952640553358126387413200401704721090867708069775334506813591389154222398418522021726214473581864639326065812595849595755515515056168597727961336934738681911389179119474929848850989255580889189789463561502246259994433630893887307217487387103/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^22 - 324962926903821084516967028987018260358465927687202471404382494589112952055024065064865328686421240278412994308895605681371244919278030428504688399339348920661564643526856673856615754123407810441981169836814950316530659998251573862685522189107368115421466180187509231970738914991831647204715844145655437606471752291541441365044985620527885562049978684090490175657803526468675/4225423441571826528292019855918088784102182198999195744483948543831327227164488109374979138766655447846421082403574529532411199760747287797873603577477376283179095888773072589415913979480368282661623375041042402515192531082196019852942555206267376741731598254838321131760429361222427258486498456014921987165798640641793814518539349222306576648063745743497544634032540251*y^21 - 32971489431628414550362510313501061505874571155781839567636832708459179319789231340384770153417064905840221274501263361087066133638931679618260542839585217202356107724472485627737670650850196875128764084104984524136215195659169140059699695272991562704150796724629599767075316912720249607145110799123173365608431522981245807296825740770991121301677223829706439613205367730448295/101410162597723836679008476542034130818452372775980697867614765051951853451947714624999499330399730748314105977685788708777868794257934907148966485859457030796298301330553742145981935507528838783878961000985017660364620745972704476470621324950417041801558358116119707162250304669338254203675962944358127691979167375403051548444944381335357839553529897843941071216780966024*y^20 - 27255569655818182338141186803398178445290982884990949767713236079261995778382817086121414710411057011317389678805088913424189697474313584533775463780461221627823434396246126242705563798322091087376200136601353005019609884887392431290947431969550233137889475883251901749740162623961516480409096210417433068648729064692082219101156921434348693591870385375945720752862108071067385/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^19 + 74263351574002706455917599651002406958992887031480953516203052266879839961421633548237857157091466156656941921255903501591253837408115516925115327252912698394082590579749274172995887369555574401498583121043427531097367553038939583375436404485866091184118168327571989146873197781012963505779242998619991838221917752707679287341382441003543331523010721363282555145432036174061181/101410162597723836679008476542034130818452372775980697867614765051951853451947714624999499330399730748314105977685788708777868794257934907148966485859457030796298301330553742145981935507528838783878961000985017660364620745972704476470621324950417041801558358116119707162250304669338254203675962944358127691979167375403051548444944381335357839553529897843941071216780966024*y^18 + 154406199009560557805688710133078180275594155894958972895936539627596200932624675079822195432372227494176414215207597701245872445423101421327307715436779023688026328902015025521399428051441799095433314055647711423614442281236206725966143455480413086027649523743065885982906625954430096256411101610491189675141887556671548316861784178011055606444471352166366497394560372151051943/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^17 - 80197325637472650858656530858728943617154794623966005988736787337225327655407779697597161938821897647553761706609623767502488222271649962896433368245961124937213869370382616652483802395662209733426951923962142023671427640278611873696732045092550415280609573513579785349590415214049107598686977160098901046648940659246126595025610318490925382951305298259355561180859260142553407/101410162597723836679008476542034130818452372775980697867614765051951853451947714624999499330399730748314105977685788708777868794257934907148966485859457030796298301330553742145981935507528838783878961000985017660364620745972704476470621324950417041801558358116119707162250304669338254203675962944358127691979167375403051548444944381335357839553529897843941071216780966024*y^16 - 84379941839987628784602834552302328993902279527137550701751325784001321091480467440966823903429087462220023990945228679236788848169620517451049398417605026603461678245159459958831196099806723085866076976722972699822959893658689934038372448024669158315659344722548393420724447775204162475792102457441362565551591896266990475395663599903102310075060227534767908830941370212895875/67606775065149224452672317694689420545634915183987131911743176701301235634631809749999666220266487165542737318457192472518579196171956604765977657239638020530865534220369161430654623671685892522585974000656678440243080497315136317647080883300278027867705572077413138108166869779558836135783975296238751794652778250268701032296629587556905226369019931895960714144520644016*y^15 + 98344060480173722250635366424857493827430122967901040080267521222240340780625865382483602674726810236460331384018833634351973696791292659279631960006301206004026448471531822815108920380914027488739869399541836248152708202706376601772355640905619865955691835266110867973564901356938357667818588166822807999769343999666352307125765333933917638812993705856528216485238268053472153/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^14 + 74728149311427223811335643911708788851873471689317433814626381979577732115116874629168077284646354589678495533711663823431821888060003963426757050258585647838597536413089127956944930442705295963905797858193065605203991703686232855370990358804621153844124258070464645777691288995237911684892266964408196814755239168152631078878138072694138532568442384581110248558191911969568291/67606775065149224452672317694689420545634915183987131911743176701301235634631809749999666220266487165542737318457192472518579196171956604765977657239638020530865534220369161430654623671685892522585974000656678440243080497315136317647080883300278027867705572077413138108166869779558836135783975296238751794652778250268701032296629587556905226369019931895960714144520644016*y^13 - 13625406005807603601531549160949431752260554940480929248398560518962335017996892366413734785673513778070242076210895968593017798208837336330643502011466139885246067778211592013570078523293152039714949123041797947495391588263384815016195857301758934606135360073398730749858184908104939189756222333800347788635966402585777683378989248200364808699009519691606011166422523219662365/67606775065149224452672317694689420545634915183987131911743176701301235634631809749999666220266487165542737318457192472518579196171956604765977657239638020530865534220369161430654623671685892522585974000656678440243080497315136317647080883300278027867705572077413138108166869779558836135783975296238751794652778250268701032296629587556905226369019931895960714144520644016*y^12 - 30390874672741007482220503717755918775294442027288365687600907925948060698867593219255274193441409112537436291630422279313340304988702772062947296732233856360943008344181528955918458602713066821946484628235112741529124622857803351767825595345488477740076353429471858972287779768146062005989542939962659993076218592265448416524487732464911187351349584153703295822885991562344053/50705081298861918339504238271017065409226186387990348933807382525975926725973857312499749665199865374157052988842894354388934397128967453574483242929728515398149150665276871072990967753764419391939480500492508830182310372986352238235310662475208520900779179058059853581125152334669127101837981472179063845989583687701525774222472190667678919776764948921970535608390483012*y^11 + 1990656163133022670880873331285222050898482394045242749547794542100006843699829698131633221752354099239741666189588858229736563522945167434161869545278135716385504834461705045454179565002179765281096655294988510077183592621303791279871757319125436657462683453733850601930447109378559827159213459527559702909811751550275516701106707650994182885752868940103544745561001173727795/25352540649430959169752119135508532704613093193995174466903691262987963362986928656249874832599932687078526494421447177194467198564483726787241621464864257699074575332638435536495483876882209695969740250246254415091155186493176119117655331237604260450389589529029926790562576167334563550918990736089531922994791843850762887111236095333839459888382474460985267804195241506*y^10 + 41331006071621224654373716259654837050958720909017412131181528326039396430340749252055996586583133203164869044374415480577408683028911283779022905082547690725194232541896644024398965639374070906896697515036089581825274755740876439025839570097636900175627997067982090550559762167937571692020947502190080278878632583897355766697986904206148525820617316912079944224318663175638283/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^9 - 3100879188754132667658854818882892761346182089139098964844316684514530077761343010036599166756118613748821344084275656548265392671371982345044087728616915926532269715925898267543855813912096701504791055544899823717840379162761586722751750512487287933678534193834910276354350204111443667574312949738898537734596319246925307251475475296357903819666163354121128291851300396282461/101410162597723836679008476542034130818452372775980697867614765051951853451947714624999499330399730748314105977685788708777868794257934907148966485859457030796298301330553742145981935507528838783878961000985017660364620745972704476470621324950417041801558358116119707162250304669338254203675962944358127691979167375403051548444944381335357839553529897843941071216780966024*y^8 - 4237032281101011893243090776024869278591624832890106014269017624397594737120348141699114974342959460236615309384911398670794194570757769231622810153188844474512573768541724966639485301404665440236121990326069740909082596288516451396422088118958023035585196168273290020569421615294343885317274183256216128887127842843269224566676203245633469593146350852560573571627121985570003/101410162597723836679008476542034130818452372775980697867614765051951853451947714624999499330399730748314105977685788708777868794257934907148966485859457030796298301330553742145981935507528838783878961000985017660364620745972704476470621324950417041801558358116119707162250304669338254203675962944358127691979167375403051548444944381335357839553529897843941071216780966024*y^7 + 4763615007061083927737605357893779219988774348047037776596886039980522890328368096804250684510750004288100327273366961023976980270350473340767744655628081087742973355434766926718897759985785031543668181241159925689560882895900618951265873487156559414955891765993143305134474565923570145653166178721846205689562804935499127436557173793410637913811998705174199068160284754971/572938771738552749598917946565164580895211145627009592472399802553400301988405167372878527290393959030023197614044004004394738950609801735304895400335915428227674018816687808734361217556660106123609949158107444408839665231484206081754922739832864642946657390486552017865820930335244374032067587256260608429260832629395771460140928708109366325161185863525090797834920712*y^6 + 307724023899093482588465184878672430075774882900407479384940318001563735012775120528047704009202804218605516279055216909945335844815147205224461053094267873688079498779742496811304810139596776343095385013828971984712894239135096313511824589481396159580601592828390062602505479509610228104034662114011400690423980780591264065297742417774797662983366946446641370555944397767677/67606775065149224452672317694689420545634915183987131911743176701301235634631809749999666220266487165542737318457192472518579196171956604765977657239638020530865534220369161430654623671685892522585974000656678440243080497315136317647080883300278027867705572077413138108166869779558836135783975296238751794652778250268701032296629587556905226369019931895960714144520644016*y^5 - 241023495569966242349738835403071880813522923410061804136223098536771598948196399091137930209537782420268122032782486803387563671811727362226068545016269854158827061826203051343408051365799308522983459118276513109729311703018408877181431132788117236556178605739505303827029323240164615687637092108179890063588827679114355884949957971920151667180451291314713381086504613615777/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y^4 - 11841456537815005017805945250682658724405437140169489944950764920119118445928224374706839472578672770187748419674177114628855691913463164780775849167094740874836880514379107807854686255081767060798936208687585489171053830595363243296302117567278946272508113369475983424328720108359211856407795223584421154474021665916630786472460035840863996560172101380083357368816669988557/67606775065149224452672317694689420545634915183987131911743176701301235634631809749999666220266487165542737318457192472518579196171956604765977657239638020530865534220369161430654623671685892522585974000656678440243080497315136317647080883300278027867705572077413138108166869779558836135783975296238751794652778250268701032296629587556905226369019931895960714144520644016*y^3 + 6734740645138497726398637443124815247977454757838175757248384021665534205966296606431275147043698943760170255212574121254103414977014243918598663118848936638601285239522690527075851801170884654037444088940780795828270856211102021683372703658763782725213778890969449898955596623720368223438307114073201477704706602669368777373165165457146517060024021788992534008816287868939/101410162597723836679008476542034130818452372775980697867614765051951853451947714624999499330399730748314105977685788708777868794257934907148966485859457030796298301330553742145981935507528838783878961000985017660364620745972704476470621324950417041801558358116119707162250304669338254203675962944358127691979167375403051548444944381335357839553529897843941071216780966024*y^2 - 587960372739400710717490064854752914913106320962208113772536571819715345574162542455123810990064510987927002173835597114519830653133166966499337370920353153222146995950350587191174469856043137850306269160046326892703482486845282245643770832346853795219812076204589131211058124402341554114469003771748978651207890545039225682145342871007345795127174468352574108245157625329/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048*y + 1154077305648595406295729026312719097164161023643187254180113677738162674165879530183175820975241924398191605148631696825220603104366508692594542096870846955131218399020916326768185609509107306740034150048911112052343053254744314818186319352450015742606260452965538462514823234546573530420487123006510426091468483910139987149222619668127951356259931287284488755788797213761/202820325195447673358016953084068261636904745551961395735229530103903706903895429249998998660799461496628211955371577417555737588515869814297932971718914061592596602661107484291963871015057677567757922001970035320729241491945408952941242649900834083603116716232239414324500609338676508407351925888716255383958334750806103096889888762670715679107059795687882142433561932048

# 3 Loop Invariant
104165936236522490510773395784397922998536226681831468415781231805855693928788873305778099377062616478362650818250999926575978468638710844111385431991987601138131353095171595909400945182781902261867190710187132580204293311420675191161482689058884985981333886408342299181498013762364884217811707414722353071933897736630008491631157764394381204842270236564368782232657950312165871883561953226350807147028784920031543057422533169309/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^34 + 9748219684629110258468526877687075850952102371894273602516101101236541575476479770647522143051070108460058189941603826483058656547901335760286451840824267879070375465713634258472652240731546018705315501505548215067385495301693928150377419926990915089878784106906181971241746052266553785358528504033366806565500257385052118853319775889775370332185717881196869666218140500139522619793074648938132019662135731348831995852927169708117/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^33 + 48626828597958018861481139393746713879195460760126064721068356033202801670882781490289151750034779264048119062491468406313279393305958805808033061697578656773268453083667223170794288206842309950186970045475535254156821264291858820208720772268572997188983676869038620105214809675652418724997950208642156486811128939456385245776563917853034659226989195868336984846774828403063675369791446597921661855017832581170990769942340377494367/90108969048133052553655119624309143632317225799728400459442153873223718355761332355198132062308254146821200079116330521372847554928890915148934706892308281902388806062399419597313557541302099158703686405438281397312413788786050622384209948221985280684152412124754004599844095154120409024977811143357824964019631232083540263566577783571879820292173000927499862913357816285555503464296477888329892808045885352940581233024473141672736296*y^32 + 8769734405307060873581193401601733293245640890009309385089571995716250278499949607331905070880021582155625183670659068052944096391517350286214126989862620001432643475784067489460574303604982851481342279737554907773016125829678711963989016987161244609046828915418714736859858972397889681109085891182150455958427633687902231885786925938584463122392701150970588370911650330944738467569714932335922752587996562766631517179771770124706587/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^31 + 123571158605475218207370079693874157163776748389175191476991778513003060992638971724801190964665488422227239352145179597730143545971496840343421273370979622187836690383714046784140511522327675086997462469237290634366862965220791457690174075997466412708138980585941004541927364175564138834932209366165355660088291434289067833744824429531289558372722264414248144018128798890498219388789943921989968734106977534949492875335129875833507913/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^30 + 279743011366589310841072146856884665068505189663009973931752053653306103515779346936136214035668878097123939422316688895386141619318228908335756023731093176294959259796679524508106316866040315390211064755557673620545961915601174769735871571774239312667361605056677537102569186466083764273591510332560736732608803987502414266372340603224979226503070729704182843981895009288554825404997399500848444297194870107995301166604521700922556647/180217938096266105107310239248618287264634451599456800918884307746447436711522664710396264124616508293642400158232661042745695109857781830297869413784616563804777612124798839194627115082604198317407372810876562794624827577572101244768419896443970561368304824249508009199688190308240818049955622286715649928039262464167080527133155567143759640584346001854999725826715632571111006928592955776659785616091770705881162466048946283345472592*y^29 + 1601758781409481935821978314440766844485790065030894879512350520667808203540027263806802198292063762711634567190468820097782765843875953211450966052657349426939832249407208980337918272920608781810101199766537135540016139682075303856308003808048046392069380334241129311067869529189855307931125284721713470410430740676600260773714684873697223153793600974584883143573994900582416428539311141567403792026441929925890867393602234635758634911/180217938096266105107310239248618287264634451599456800918884307746447436711522664710396264124616508293642400158232661042745695109857781830297869413784616563804777612124798839194627115082604198317407372810876562794624827577572101244768419896443970561368304824249508009199688190308240818049955622286715649928039262464167080527133155567143759640584346001854999725826715632571111006928592955776659785616091770705881162466048946283345472592*y^28 + 10694032281763444877210394427233891952661269497738984247541536771945279850478831882469962585769316401332411436405299311159254966932126608955699842829662398855657625511209780100198918431938128196598910868631757031666094731934892429184896098340860078415896138127114801919028847146951181314080897848053532922497323326506232778857158615256503352016287231101802839660228775895925002452241166757568845368334935694585621029532937358341541637757/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^27 + 34292789899732135174513258128730762293709622085354781722466166587013366934802925477765205613039383468480375422498054387885667952707262940080993789515366806129647291338059149043938728296923086117974190803531187352422803794248718541866548171100336262391758705175723731426906072803779908342742508343406555122375482418040595301805694708429660925120816225817596513060556848572214127267801589564598038275564831992382783192140751869957879695043/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^26 + 3560112234244976554659025984718294417906394284497231348364489618344322972998838647997559970997692455169957797626437876599292745257601263077637806845503697499259485533173139983149744221253544319528347084705205155520015925660396190127359593103736739189355037490465343319282900194214056805386711900760556906677518414874959953286666247250246888795671579729567226537890253158293399747293916590445825760950874780977712165854576673293617011545/90108969048133052553655119624309143632317225799728400459442153873223718355761332355198132062308254146821200079116330521372847554928890915148934706892308281902388806062399419597313557541302099158703686405438281397312413788786050622384209948221985280684152412124754004599844095154120409024977811143357824964019631232083540263566577783571879820292173000927499862913357816285555503464296477888329892808045885352940581233024473141672736296*y^25 + 187645599297842654163967753952761257414005999728089880847924656451848179238728654246246366131966589746434665693296957885973631673543596245005866256684278522181812538336905460539657946818776971386380744003311229903345098700388102012658917896688027148266949394356561542380237250251985481637886923440785880329301790152454238740832138184323424639542862125897142997594671376626052167295600172804349787444660437418387481683697763404378938254139/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^24 + 2401516495839412279300526150642308900812318664136426823427979675916432036400742280307037238504288611924902040585053825704814035745273292392147101246829064917381254033652216722895309569400552951892267167222649293445747964084969026350358895540310137513031159816209528204136906873550117737992076754801770677654971663372527502406257924744213971644091785515777610331670613910451308794966192531489537217291121286702085987562050971293155171703947/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^23 + 4758078595999240116114766499070172395027439584738736202940770586510262854319400980804551259094379415304038673701132273564155171024001770542253226672079168370063457789455101276627764727211544900259261931433258113612022971994450278700729807718142838529330150500778535557824735762881367868228446223283012992612100453930187448914859665610650243384696265637459275568553515731673698711957058547972683544639544123165674049675469871365029588494149/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^22 - 1272010261643834158425042226135060570504400922381171771780218047486204180110167079816643707580843553641106171076721143596941955507918476442139138305737793054256251121612301318021692518589531070677857094133465801568055865811403286581274702090521821184498422728106496344127790801424147110210332100728531480797910307946597372548224210626707421246708863770107841196489601384088871189943115200575186213526386037011593685255042268243857636490425/180217938096266105107310239248618287264634451599456800918884307746447436711522664710396264124616508293642400158232661042745695109857781830297869413784616563804777612124798839194627115082604198317407372810876562794624827577572101244768419896443970561368304824249508009199688190308240818049955622286715649928039262464167080527133155567143759640584346001854999725826715632571111006928592955776659785616091770705881162466048946283345472592*y^21 - 16324499285121002605186252232902463526333016815728847168267146198484552143271260944351274563170758990724116560453514475197190459861123802891504614538884572743635291191236487804461325925137216306279802372819475619697763072463939539427618883922208911998004786358742605652047787305365707120105301418614723301228269082577804505993489850221493136788805810131743040695791197021541903851785951921931643607870598045595215598391961001653281792151819/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^20 - 27126160503735576502297820311914364792215203771761204514247963954254253965230778278493047092025414201036384672659415620085205756402452662156232192505903728247918416198256724419757892121513623282968807305180050850211699958480061345844974656895123055270910163129892209163452368851410777467541299225909293974850830596123448087691274879586764431951309450661964544952033964542914768448399444373503255634180267606694590292354429281323668497201655/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^19 + 27907074861718913889642397676860096569899547295834622327029025271858551535794319523948245718829290667844665471890615146070292643409037562774277489261928672958519916117236548624368880772355083955319757115441529615958558547542904529499278036065173081617464312993065511524968360307097648704277036036974855297950157903957327448858407040603237318386457729101135869215844106688819958382283985886011423236137966138573461156861841198532533630836341/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^18 + 1492989314766706823956245980290243657981861098793471626349242873051192235392170003913878204370865745553061761050901887939657002771647525564450143564508994717002583232424160050371105039074660745289751278906692245161497829161209812159312736390022666701865347264550155665425561803888874046558658762453725963267764613852993634699601182219820834421605607599083858634918981189462687835200900202333100787728610600404262872846454548894376636852900/11263621131016631569206889953038642954039653224966050057430269234152964794470166544399766507788531768352650009889541315171605944366111364393616838361538535237798600757799927449664194692662762394837960800679785174664051723598256327798026243527748160085519051515594250574980511894265051128122226392919728120502453904010442532945822222946484977536521625115937482864169727035694437933037059736041236601005735669117572654128059142709092037*y^17 - 1868345058409868683285206632643205611037410667507563750471080706220031706065223326630355106597721645471817240185040554543925062447523263285901698832440582185735211160688824298151516672326097378736759080046424943110441517026091815893971070954837089158335850915309552889684950969941148280994085153137400321399795928790504080439188195743709423879481296499886687828744964765813351152809199460502431740993321338467749652008759129046023607283577/45054484524066526276827559812154571816158612899864200229721076936611859177880666177599066031154127073410600039558165260686423777464445457574467353446154140951194403031199709798656778770651049579351843202719140698656206894393025311192104974110992640342076206062377002299922047577060204512488905571678912482009815616041770131783288891785939910146086500463749931456678908142777751732148238944164946404022942676470290616512236570836368148*y^16 - 64362352552409328261936249877597612842782610229293349434758270394013836433996948699021717832624020520806158033568472572302439872184438575215391556599379590874577031011515268396323740977645830634931615546862290252221065087526111261068231322868912245043002718076325813963051788332931463323415287287650616369694816566774283692393709408378609738285742010013392389792065254620547493569785222816504252195072329058417913269645449683637855729207205/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^15 - 1789047723568260593037564587115763715281253872784237115644664942629904596774411544017178199060015349718697640093828323850303190782491944262152414776215205192446782877232038949585796154899104128509019018595158796029196048894739954799608308011140582208120290580062917234195782687211986487904811864779477875652818163586930622130297158826849514314102367825243986304396279481912124101184697795393052416021370609804696398615933855259238439447845/90108969048133052553655119624309143632317225799728400459442153873223718355761332355198132062308254146821200079116330521372847554928890915148934706892308281902388806062399419597313557541302099158703686405438281397312413788786050622384209948221985280684152412124754004599844095154120409024977811143357824964019631232083540263566577783571879820292173000927499862913357816285555503464296477888329892808045885352940581233024473141672736296*y^14 + 95838420489972052168235103419594290466454747592418747755340047866995057624520549815926765216647598262808261930136821511838408712028844498372320501539382118681873352388591526590862817683365049553912182175909799156653045761433331927629366308228902079845417827280180199616126575488294070783167627882006376317365274054846660018136698511563592326728727017925508002576895121941922662492253760620919093150759592074419269570476336053963515543007337/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^13 + 1672261033661941929129778830258866267093974487331730122421419185937464911805160662894652336770476598684912864719472053392482780504371233270306591589164494922135275740434577241098125505347336821049013598464928358370667004149921900001493645139587531560068250407236139129741130157684706892559003362405990609316892621301399809516485471559835196565787102373421160198305437698883149426994048132597835873526096653485292666739371082319372557890051/45054484524066526276827559812154571816158612899864200229721076936611859177880666177599066031154127073410600039558165260686423777464445457574467353446154140951194403031199709798656778770651049579351843202719140698656206894393025311192104974110992640342076206062377002299922047577060204512488905571678912482009815616041770131783288891785939910146086500463749931456678908142777751732148238944164946404022942676470290616512236570836368148*y^12 - 22015989383677187263464590399060455705345314290398433225741948156549608443216730993592085799480642824596986401408062748426584448791349143527515048067743522718521581925947192991473746116580280550924628193927201759233257212459722298809076380395305220394302393778470472009483470301145543364105938207315079173214813308356192685362175190240180994109450829701893472612797633458908009639774437869767204831663007923709936215636340871695377784387401/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^11 - 1864908286927723444771428135965917844421296004151029159436407458283612457994903306849744497005972045511293096341444637502685430044679979455779715211013095578588718905602345601230358994725090531079033092957353082062812187582586517199029166798211648589679789769941774701316260333013199995810595631664160379447234596012505454224629948506524845307551934703514361096693159514799591281302399397726627776561249799040071628363903632007907835582807/90108969048133052553655119624309143632317225799728400459442153873223718355761332355198132062308254146821200079116330521372847554928890915148934706892308281902388806062399419597313557541302099158703686405438281397312413788786050622384209948221985280684152412124754004599844095154120409024977811143357824964019631232083540263566577783571879820292173000927499862913357816285555503464296477888329892808045885352940581233024473141672736296*y^10 + 6527124048946647141378857502184388923179290252756119178033007597829588229095042844088789045921203705880345276728173187372484027697997078983112093324884963141999666925208328963239020066232228680143222105519902708641623965713076107204552388359212145864636573833135326340826024229295778110833199664631186885950025732404519158689748790860887210633335171605450769738793690656486378434550674498166064366900882864761683160722325004951155676908221/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^9 + 275737494347553787639454727124931613954099433597321610661601727716934164905439543796122980161692565616108920768737017451536621567019818561360966379540620498151107773152391311531818090699088536234660634977301937553471815361635521713684267885958801616635114787726110802230190317873845930088311377420856583566154936592817559586479670940779679926593333916656739777143184159325247797034865052782268479869314259621327508260761812235339009700673/45054484524066526276827559812154571816158612899864200229721076936611859177880666177599066031154127073410600039558165260686423777464445457574467353446154140951194403031199709798656778770651049579351843202719140698656206894393025311192104974110992640342076206062377002299922047577060204512488905571678912482009815616041770131783288891785939910146086500463749931456678908142777751732148238944164946404022942676470290616512236570836368148*y^8 - 2517914834426516301657410906015775149184166820217906111054997747579934615182776982884557187772347454757031225230202190553870340505488934109404614807067090087315147793915535309494914619665411693840653891802175328315754555958618182754531947357304939675339216600109932181143716255697566047210598782426087308817830545444355209602886396824210635993110137755685339991651076510766775765016778493164357818425805342510268919279576985559622154150395/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^7 - 12956409483461653366218119739556494503396457246847749597044661616562478642881565598880526860041179438633884349107014995116136509811267837652286277280594469221251128872867174262323360304836486678124597740515443457120142176840646717725207133769196770364906044371459691743304725331958014826795412311581318437621142629054087067757636035209730609933490806380045925325337553513137760666515548677554646290921769377664908774843925835914379336831/12218165294662108820834592491431748289127759430471647519924359847216775370272723031213306042346881918213044078524248206287843736261544530867652163646414682291849329635579582318279804412379945648637787987178072053872869666276074660662265755691116648228359649101661559945741572224287513088132584561811230503595882200960480035737841055399576924785379389956271167852658686953973627588379183442485409194311306488534316099393148900565794752*y^6 + 304338631495898101640195401318186732786320449621921294935531978779458595881274458863382662714876893330734886502439762894969725622539920840442010085737470950949972364291836055692290124844861249982374814409028755072172472992889295090830094484985641401282647848044204398244273936884228268509973347375182057478332228615484348859689661347407694938262767997163744955307858637854824245485982015638082709171480126624960473269347978070117808666285/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^5 + 37610359797683364197319995075401135590015138076467635906417273305765276073844755532681084881677015820323297456072629307337812472416328075642426828710851735061390806281697379068389442655301945049521094029669761410725505622887513540596341398460529383564856939303468780956022753103656983848742242572394152855829767739498251596208565627066160408730814602402542307007262839119273308638003697337954980867858611310024778780434613943378717207677/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y^4 - 20368880256994210187524467212623302154472480588455989311596885916201322445363400987205786033857044750815226638129860535498038161953367487820196282970907974829672178497390625126266664438683495107422239913920108587622859775973299597142639902893590133737465742360166445831394937968559479603378304587920763895439224406725787469053526459048578279736689627692723215210848891835277544331396727677463752213194214320304366485581462531499758956611/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^3 - 3431034307422010429506639073353110216874139752052266128810091787702393368452423393805949550659327828016591822427159390537416708217465668766736063973171234258834372837912728369512056768081321363463842240111445320450763771450981255036623777362082931504731923240526626432318937675216120144807082580420315410537483958491919874442715358708300625875835809317669834023104291176833251752519139077723703275246756805290860254573991850052321941967/720871752385064420429240956994473149058537806397827203675537230985789746846090658841585056498466033174569600632930644170982780439431127321191477655138466255219110448499195356778508460330416793269629491243506251178499310310288404979073679585775882245473219296998032036798752761232963272199822489146862599712157049856668322108532622268575038562337384007419998903306862530284444027714371823106639142464367082823524649864195785133381890368*y^2 + 258780552097084995516086550071112220919082121691699570475024580754671854368153309016492160039080099731212762757545051292214985983435840462437930890479493524723773271669526349136817620423800684935823918785201952368707025227015428601732360396103846570230894402822917287727312420421361465031660076326012189896061981749478083080722694378368175006887500511026876311638829467548657792643304377774333880043461404880658816752356855999965401201/360435876192532210214620478497236574529268903198913601837768615492894873423045329420792528249233016587284800316465322085491390219715563660595738827569233127609555224249597678389254230165208396634814745621753125589249655155144202489536839792887941122736609648499016018399376380616481636099911244573431299856078524928334161054266311134287519281168692003709999451653431265142222013857185911553319571232183541411762324932097892566690945184*y + 16027516827099280476963733093174618489185401756240400342589189700169541035263821878697615458464787337378345484040538635823897061911832956993507349986026647828013457628512744729086206240079549928464521368468300889421067948574237609631026679813330214494431884587310904442801791334411115843908188929841354555216578534018519761414969971003317778627177834696885704291993625315952354149641434236498324887888053469259979750867025659083145487/180217938096266105107310239248618287264634451599456800918884307746447436711522664710396264124616508293642400158232661042745695109857781830297869413784616563804777612124798839194627115082604198317407372810876562794624827577572101244768419896443970561368304824249508009199688190308240818049955622286715649928039262464167080527133155567143759640584346001854999725826715632571111006928592955776659785616091770705881162466048946283345472592

# 4 Loop Invariant
-274491355555941711310617007338290899071151665293793777734110444362710346975192112366314242315932113652134554901357590090038524938183703725975928430471166867385881153659811672057079101021888947066518372875090274056609353273138099104541950918655441295497910094618663754337091400398437735552006905180441589083710202357722420389893489963480330120492486421342677606205972883503327429122103235297594146254643049662273239755274399063866544930064593309961642815608741378493689272980834814528418495222403522694483801890167177154882524846002803002187378800167303137021/1844064476247111724547484073749112587888539371200701497017727115853466039264778718957153283198216002669102026855020861783387031083035555792002430809856518789190227564051700924510712163601337461809041729209401087526174263249484378331016084907606785290320181356456147884819759514597116252815239086019450048400951209747989808735309707759412677486784230323836619370497583501786041576610305765728457913036405157684190432726413280969902996240212083182974436730447157029716785324150217208059212469751863121646093803392856301101982857067006029543355495582526546082920645120*y^34 - 10258257688152306093444504663406955408752011314536292105568382508173477882777438898681887171876412337365277263787131871133694623980642323333461710068750926096105091921993475110028462844827326758775933546984513702485121379696323773544013274227161907176805113633065464722837666256623311036728471595951445825840418411206094578700562563652050207088195229343214560425569090322469309711462960166893564221627928810280201902907300890233800451320031236166978455675235925040424095993560805120790588533497886921623197610660400331571193511602771883836065145312716177866633/737625790498844689818993629499645035155415748480280598807090846341386415705911487582861313279286401067640810742008344713354812433214222316800972323942607515676091025620680369804284865440534984723616691683760435010469705299793751332406433963042714116128072542582459153927903805838846501126095634407780019360380483899195923494123883103765070994713692129534647748199033400714416630644122306291383165214562063073676173090565312387961198496084833273189774692178862811886714129660086883223684987900745248658437521357142520440793142826802411817342198233010618433168258048*y^33 - 68075527177251158565668706771833054649082989662296972979734679598645787172077281117612527611135002546031054022046319818951184682623833433432804576142386653925278248152500436599355202437722145165741716973102352388476758425955676738533309297427750604765798585403357310597148537066922534330342062854074813080431842579630694072965374953195044397503743196237030846976114191929618332347532018478728913270988296426365092972824937924800122674165932546467612098782378018569635978565345864590331581813542050757117968145911291318773633918551298388159272098122996004322873/122937631749807448303165604916607505859235958080046766467848474390231069284318581263810218879881066844606801790334724118892468738869037052800162053990434585946015170936780061634047477573422497453936115280626739168411617549965625222067738993840452352688012090430409858987983967639807750187682605734630003226730080649865987249020647183960845165785615354922441291366505566785736105107353717715230527535760343845612695515094218731326866416014138878864962448696477135314452354943347813870614164650124208109739586892857086740132190471133735302890366372168436405528043008*y^32 - 3059968941662337728517855075767197659848205900543382573143921628655099198243098750486246447889347723483960212231386061155024998788250099445179253267827135972328235624835313497284420632667676937959784682941006741431891077381772229164194110929179664586732561213538498500077404544774602203195478553809282552427544802683000159504469602385529682400271271946128077117757609462907413867016561219033367421793983161567214939528536707831423856946857881595075740747926255038669579046459154291428761906476451243804676294443970713928503532967590978475790813932688972343165089/245875263499614896606331209833215011718471916160093532935696948780462138568637162527620437759762133689213603580669448237784937477738074105600324107980869171892030341873560123268094955146844994907872230561253478336823235099931250444135477987680904705376024180860819717975967935279615500375365211469260006453460161299731974498041294367921690331571230709844882582733011133571472210214707435430461055071520687691225391030188437462653732832028277757729924897392954270628904709886695627741228329300248416219479173785714173480264380942267470605780732744336872811056086016*y^31 - 107331284832620168983593993472360128909268320515442428340787781712825953628956284690127381540176755261731944206350998963298626001394302162463712786444601099935967572196087302838897621055409073064469404143533721818166736149598654152173366127949118523373824663258327686756556682510961970989494791129868595444125563829755392364580032486901766483984374815936238642632985809220990857051924639313919318775525149545313893014333110203813547480386901799198524573274657504136945387149543507117822250832277100425886312282385303498951473594656467912388831620815031223928092411/614688158749037241515828024583037529296179790400233832339242371951155346421592906319051094399405334223034008951673620594462343694345185264000810269952172929730075854683900308170237387867112487269680576403133695842058087749828126110338694969202261763440060452152049294939919838199038750938413028673150016133650403249329936245103235919804225828928076774612206456832527833928680525536768588576152637678801719228063477575471093656634332080070694394324812243482385676572261774716739069353070823250621040548697934464285433700660952355668676514451831860842182027640215040*y^30 - 1448405597802839995378197967184014134883940709367963897010615881312331489807131633829370159383086737226651137464710177408331752207734746555737724793226528435900379809388548816459499262404056199840676680880653742382927699813781223748591163167697579010553480805648271908492842227994844426088035427489973582669559245930421415028866546021023249434724996417293832319680617413662760315574970610396913400658363885886436009673076221665692813472235147293494717334929080542924979403181534993952682625151375656821969690458146356252958937004560788684825684261665355926332398159/922032238123555862273742036874556293944269685600350748508863557926733019632389359478576641599108001334551013427510430891693515541517777896001215404928259394595113782025850462255356081800668730904520864604700543763087131624742189165508042453803392645160090678228073942409879757298558126407619543009725024200475604873994904367654853879706338743392115161918309685248791750893020788305152882864228956518202578842095216363206640484951498120106041591487218365223578514858392662075108604029606234875931560823046901696428150550991428533503014771677747791263273041460322560*y^29 - 8202760755340791461804070620653887559080405329770097551490140326374430879767881004712605386389704847678976707901917270286060170427712595822394117267153521401134777565677063446112811518855339069221958436573097218363273924491443565479939248018612894618875110307445688574802069250925495577270565667634427196274782839644875044187938938924290566976678960585259029555991978220017626026187224671700434929229550145058682172911044530390693528552330308066887112096239138917828126519590895160758595569646522981808561362215433526199953099032571774535130016133693150067677170007/922032238123555862273742036874556293944269685600350748508863557926733019632389359478576641599108001334551013427510430891693515541517777896001215404928259394595113782025850462255356081800668730904520864604700543763087131624742189165508042453803392645160090678228073942409879757298558126407619543009725024200475604873994904367654853879706338743392115161918309685248791750893020788305152882864228956518202578842095216363206640484951498120106041591487218365223578514858392662075108604029606234875931560823046901696428150550991428533503014771677747791263273041460322560*y^28 - 107091253970115446264201649633062786428693333489500351958669432587051487763655264964998086601081238556973612899469290107463331312699818588712414044053918947394831557467076941419703476061443247881827853412152574837426393611539966727326371791281260453434229311888643277866010883038093837451801183387651657409808479110312504037554531221694525482997636787674980873423461116607170939963430972194263016997353315019196558506851817116450412958543405718224518946435238342233917878691636096460397294094876157500282625472715157996741132179820989047008773956104273049391357205629/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^27 - 160931931696729629712029434380331754125037399139774050509488540301380383737062928689753243318787683766935255918014619896469463479407632466351846594621276084310981072630363073658300070194814759416508531045534647422999083126228664050848544365664221282711057110840165927713473119786563604339739655309512291196181807602621967854839639537792873714213952886811246661941512156706662213398573296390487476078644986328695277954343374751286137570424421681243648856227320218808572593392250238392310047437908649527843839066906319350328889104399177067238384738925076678924619776469/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^26 - 634477998120831760472953091605097590437435177220536476640675588007201722174904754988851113547618465371988820348907079837723734297495267790343239669243631806670287899148266217911780744457867100299751058127913575778545371343365966857130633723827980953248817588125202461871008290564802629078042417225327767198778671092582801380447775399761812757483691827205974592186792660518231713872948512367496652732743615364747764927858838093122543584856963180109371141467395403680906232499552078592770346673170029447936685318059233230052266737045240549408294738195662939560696247/20489605291634574717194267486101250976539326346674461077974745731705178214053096877301703146646844474101133631722454019815411456478172842133360342331739097657669195156130010272341246262237082908989352546771123194735269591660937537011289832306742058781335348405068309831330661273301291697947100955771667204455013441644331208170107863993474194297602559153740215227750927797622684184558952952538421255960057307602115919182369788554477736002356479810827074782746189219075392490557968978435694108354034684956597815476181123355365078522289217148394395361406067588007168*y^25 - 1941739698571885860198270320726882903127513258941072147988798180393747975136884278278473508627132645734357261317128981998108781527741039906354108105921015315312111260535060510641499759652249992282914452327257372208401729464134594988887347541638441030546158167225800442655071065718038851515487062221841091959227808007805380672935238007815868012300757578199419393322401397139305050926312919591037174506398878810802576277490938159127873338010251138098951825578909128996304632335997227325893823696318799179315010811213261763992692255393025096349343078290128575633074902131/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^24 - 12338248479829938841944130149319851792094534197172534626909116305004754825251984893781166066975432852190228427622046077477628272803134735784546885807273587618468584095957977284567707897770173968255870981923677289089760603241887672818027092477718370912829128300024131162922886486334780419088178182022515054927174913835172109227767257015940130300245521285824948819605907573649436947185046240761050397029190502324991563910974028841536410147469492814307642110307876703617464199958731546950179987991221443024426400164389033267355903193318435414225913066919150972295021061997/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^23 - 765688013392264390114634544091523534659372444017945761510347273762940058135788762528703608903141541389571612072442494758577247228269100144122100297571938561175239298135838295916155329862710233647893908031417648974220548424702196327068824639900007793316820885717279622632114054445899605244419930528042799442865735324180361743100319211234943959010216734324428002532004029835546085627011430697081743733679367835908004539503543918251033545721500059574921051887538811060965635019294085524661768627966445853956345386475179220518106741186446921987281536091743887835114469809/122937631749807448303165604916607505859235958080046766467848474390231069284318581263810218879881066844606801790334724118892468738869037052800162053990434585946015170936780061634047477573422497453936115280626739168411617549965625222067738993840452352688012090430409858987983967639807750187682605734630003226730080649865987249020647183960845165785615354922441291366505566785736105107353717715230527535760343845612695515094218731326866416014138878864962448696477135314452354943347813870614164650124208109739586892857086740132190471133735302890366372168436405528043008*y^22 + 10532480658989555778065544625654518765080026319698960737388843493260290896535654104582396403918543281857704754331016570078693411736007705219966972968405677076147949525055332590170188221734506483999043637495039320242302804302304482614601813872001293644688075121639977030544660422213310483559579977113242745707463248459388768623153006990910549395989844114005305931970155015852145673936881381913363436729922429370694845068459988575523746704007942268882958504163660648279598235842014845288981025465643091750569182508491266286987418242552053069591376270134441115011906584327/1229376317498074483031656049166075058592359580800467664678484743902310692843185812638102188798810668446068017903347241188924687388690370528001620539904345859460151709367800616340474775734224974539361152806267391684116175499656252220677389938404523526880120904304098589879839676398077501876826057346300032267300806498659872490206471839608451657856153549224412913665055667857361051073537177152305275357603438456126955150942187313268664160141388788649624486964771353144523549433478138706141646501242081097395868928570867401321904711337353028903663721684364055280430080*y^21 + 169663159597705072891057588947969776313964866481583223612770240000942574151101726662089083947052852285891240832820199207894321710622976851584888357909352749443223498264595959469771005814943664554740040061066033129542856204291763980351414496331086260947920176790471320150188019027219564731750237613625803690283144458019862269471616011356162322751888341082881145865115509657659104519476556135654423664671458750045065526373997589749204886193721204954022825460861326051907270010997192930344029026713202964579741767915402288397964264532059543032258552496537945641817158333469/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^20 + 22925433216332980514796558374509632019924370196878731260203076514959983412157845401769935581895473293692133254427610409331172499765486509017534960792622432628372365813479089375483149840106070352491719956560468366464470213349363541921529173676180801950661743874117688425046341317794049731984295279113973056310093807090262559261666128077631409156071752423806520090090967687624279485174566348540917808949176467065978266355892610853406744236833497255491942459159522067882475472073228220317860562562813231375615405636942209044078053570498142471554285117406395966405010366083/737625790498844689818993629499645035155415748480280598807090846341386415705911487582861313279286401067640810742008344713354812433214222316800972323942607515676091025620680369804284865440534984723616691683760435010469705299793751332406433963042714116128072542582459153927903805838846501126095634407780019360380483899195923494123883103765070994713692129534647748199033400714416630644122306291383165214562063073676173090565312387961198496084833273189774692178862811886714129660086883223684987900745248658437521357142520440793142826802411817342198233010618433168258048*y^19 - 340571635511078431372959812960970994718418284232286237621770492786305245998680410366180893147905596675456838044053229495507207563993553000504562677368301650765479284478944372381508655181413529439877835648237484313808194698838025797590845344932121277775314935798745786406039395866276137356174187522487504716530410866431497111663454116416162459758839048892997613098919251320585214512161416828178315928792833135135423867933647612902190426929242975278705159885478952263298651706222738748388719531190341885928752230216247489251508812603198865874339423396908156292077427109/3841800992181482759473925153643984558101123690001461452120264824694720915134955664494069339996283338893962555947960128715389648089657407900005064187201080810812974091774376926063983674169453045435503602519585599012863048436425788189616843557514136021500377825950308093374498988743992193365081429207187600835315020308312101531895224498776411430800479841326290355203298962054253284604803678600953985492510745175396734846694335353964575500441839964530076521764910478576636091979619183456692645316381503429362090401783960629130952222929228215323949130263637672751344*y^18 - 93256419385282986968883390610534172571977668799710209475793424283848617614143790135758455610047773929678890051124884948864311871272459834835556872233116006587403241280513817657315213159235713290599094000024899954335136212591850828415321230490614910747936758033849854019923442064019929464099304678507486022403329987169931925899171943558610261619477497246265397809143052726869610509058236760574514772365302242637139957089785392777221603500383518793014883936379862648439305576423983891805676100902796031219738684125943039769453475991939777849693841008579092108738106878323/737625790498844689818993629499645035155415748480280598807090846341386415705911487582861313279286401067640810742008344713354812433214222316800972323942607515676091025620680369804284865440534984723616691683760435010469705299793751332406433963042714116128072542582459153927903805838846501126095634407780019360380483899195923494123883103765070994713692129534647748199033400714416630644122306291383165214562063073676173090565312387961198496084833273189774692178862811886714129660086883223684987900745248658437521357142520440793142826802411817342198233010618433168258048*y^17 + 83644860162946076924024763398514328777384614453383251531085375291953019509248149015662661863386654287007592292388962779448350251140542401167231338695027629518401302091054093526774103773408597000143935798162200033934106254400776369756964355758872669781896518192284152320161031144050141469842290657601457927261449528214406656323969591783178518886909739813366070509472040775232998323170998109753588270016590836573351265887200227601920444501105838923381766609496301021628819320123100029752035328969431081723252461308051129819175506757130448142411238879341495255155787631837/1229376317498074483031656049166075058592359580800467664678484743902310692843185812638102188798810668446068017903347241188924687388690370528001620539904345859460151709367800616340474775734224974539361152806267391684116175499656252220677389938404523526880120904304098589879839676398077501876826057346300032267300806498659872490206471839608451657856153549224412913665055667857361051073537177152305275357603438456126955150942187313268664160141388788649624486964771353144523549433478138706141646501242081097395868928570867401321904711337353028903663721684364055280430080*y^16 + 675944846408658170782816737845304703687205438424722222516502274307147724032327729874669237817975954535490607116797695450278689378078865043453054071543469922335761596372889046026484644230343510059506535201929512167551621296416456386869905041225272767438912196583580246006384448195840345035152553975095632748629336570497094051310109232371509567030121743314458763317858754114567103582974678748067982086003651131267135608263078573152740693272889020642230630319962679427388456529720426073918790490721372998329032525816012099521361481295708298877027352514494106347890981439759/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^15 - 434908523377672531281955124988165679328731665783028054377800330044670383729196766087627945108676157827459199860986090384510382367652849920182663352291687118699626082631227338492337750257527422451933158946716978460636257398609347372190757437362145706514275781946505371286271355685345281909850875068045133006270156832228092670226264199590748813590076488348187021397823537963255421981053338311146359905518697201012967458146610459881566708695072946680711483412489321675456816538161370013644802141746170285908512185047503014110625946391676625380911181956128060832333369551/40979210583269149434388534972202501953078652693348922155949491463410356428106193754603406293293688948202267263444908039630822912956345684266720684663478195315338390312260020544682492524474165817978705093542246389470539183321875074022579664613484117562670696810136619662661322546602583395894201911543334408910026883288662416340215727986948388595205118307480430455501855595245368369117905905076842511920114615204231838364739577108955472004712959621654149565492378438150784981115937956871388216708069369913195630952362246710730157044578434296788790722812135176014336*y^14 - 22404563343210293515819691682576108599834020146427056757204224414742809160879320470948193314987029092643440462771141372540023338975095038568081834485816099726320140545722174835687170086425483124656688049199894497098857849795181700004416191783654428571654828637754075952899844053031106775534568357739609008351261606353497094810859632862018102505964731412884444564298066759968290516196254565024490878149942069905935646605891139904973808040896384034167877360103310889686318158122046293779627602421665610681255215968500800758959978951822772465095899853299031312197704939161/153672039687259310378957006145759382324044947600058458084810592987788836605398226579762773599851333555758502237918405148615585923586296316000202567488043232432518963670975077042559346966778121817420144100783423960514521937457031527584673742300565440860015113038012323734979959549759687734603257168287504033412600812332484061275808979951056457232019193653051614208131958482170131384192147144038159419700429807015869393867773414158583020017673598581203060870596419143065443679184767338267705812655260137174483616071358425165238088917169128612957965210545506910053760*y^13 - 57443052715565225859139956789184311527223941159198218447514381772356318734745134248330493914126128943340918822989035597731133355497864163436708996554369424759895975612890767044512903640977237471099180889461517684956774327622730753178032583468916197155672005483969815294995260248548322962478343949571867973349011246907178717324793059842594775310560311351751164079233197137731760726117801540146109811944771318429348898881542731009719053258182834624480118950763990738553708261512334912107985208445052061135346174566307779504786142145289970057591251115036894520658568585761/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^12 + 14646270999647707297721290062799580201480362968447998701348605873041422437224516992997339059559588235206026360472839015281656430254565983086820176302105758803587598309601750751494203574483201655618257859316784272673569413841711515716387374673006054259893720921370430100020691890417982122067231857820975550321978968086383794157375246116172902484003372304036411409648299925998986591394912514099575613108335852114115406895132570766405327993943340159452351148245244070867133605405109585100399353598604951952706629326823338792576035595839733626229864401150519599835911519907/204896052916345747171942674861012509765393263466744610779747457317051782140530968773017031466468444741011336317224540198154114564781728421333603423317390976576691951561300102723412462622370829089893525467711231947352695916609375370112898323067420587813353484050683098313306612733012916979471009557716672044550134416443312081701078639934741942976025591537402152277509277976226841845589529525384212559600573076021159191823697885544777360023564798108270747827461892190753924905579689784356941083540346849565978154761811233553650785222892171483943953614060675880071680*y^11 + 6209043035306980770566172108918766300060764842704915244000605933239775269183725241598952090895926518377880244036420037237505134425143249937368703589976212858949669837058058844393695736930591571227604915406904621103514493948691527658581779164165752817591812251259795962027740022230548225464078873878164735404950741180330311295216256932660363543485480686493655983048202292484783076971505449368383366222492225100543590177980573785412171398372962211973740544518479390405103088597181682467895241162008017724749332211561429543538373469094162483020659539852461161741833046771/614688158749037241515828024583037529296179790400233832339242371951155346421592906319051094399405334223034008951673620594462343694345185264000810269952172929730075854683900308170237387867112487269680576403133695842058087749828126110338694969202261763440060452152049294939919838199038750938413028673150016133650403249329936245103235919804225828928076774612206456832527833928680525536768588576152637678801719228063477575471093656634332080070694394324812243482385676572261774716739069353070823250621040548697934464285433700660952355668676514451831860842182027640215040*y^10 - 8273648235896921080717607338417257966496143599022135976037303985160798900554300475102242004320511056438274981316381798240657692435823579064146880088133745334892135892866547302513900504197335224646468688818885592820015142318729640168555579329352835324180248582875736401613845833674581489840658084031853757430270957676621060808467258584873336204566978223321703630705416727092461955707097973827529042655090166384977556717377397461063682444441540847666448270115113977397174111894549926386939327087826566674401120327815998394263480713961922166431634631858550918538046642535/368812895249422344909496814749822517577707874240140299403545423170693207852955743791430656639643200533820405371004172356677406216607111158400486161971303757838045512810340184902142432720267492361808345841880217505234852649896875666203216981521357058064036271291229576963951902919423250563047817203890009680190241949597961747061941551882535497356846064767323874099516700357208315322061153145691582607281031536838086545282656193980599248042416636594887346089431405943357064830043441611842493950372624329218760678571260220396571413401205908671099116505309216584129024*y^9 - 8908644241315119669440462580831998626925689400614161248839288139887377612560544687353430913192087901406691052112931791062973002075362618179668183191957965867620464713640885861427484832037621740029233939254173729713092582631322014756942858146407200004077901736256148486151229378615665786599426546128352491769377128295528817062563776864912723766563392625047063479922731587147469745727657367078615063697992028209139172052486081988546023197329058650475143068680231676787061436273401716459359759038340570840521987971800703545910868883823699000256899171909575338129074455223/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^8 + 1814438409273758812860986572373364686318961140121524869595476479025344229034144143785026179970502906074170996999839582033069357618838265347907120320832879351204472755112238764189529036170629032587582806519252126860035404116154661738223504398195258810274883126540779946132696752691127859297556499850129321004809913057422489151401100152777887875831870193120691516167990114638547226958757960316453155247290497574534636592918722905824031459049284157106704104441570083151636873578482453882153583822523156294982641138821276860346602069823297916846490301303822711568995052609/409792105832691494343885349722025019530786526933489221559494914634103564281061937546034062932936889482022672634449080396308229129563456842667206846634781953153383903122600205446824925244741658179787050935422463894705391833218750740225796646134841175626706968101366196626613225466025833958942019115433344089100268832886624163402157279869483885952051183074804304555018555952453683691179059050768425119201146152042318383647395771089554720047129596216541495654923784381507849811159379568713882167080693699131956309523622467107301570445784342967887907228121351760143360*y^7 + 6742925847819186873851737643240005787734200175335338715758532427835692834913435588817756972614348476245826125966792886365261354364137682400669563687323492803402548350525672614743498673542681088308003397018134103507715883450372331376789602350020939024682737010485822031714298364848290072242692415750744024546498761556918564842593714161151152475246509722601587092211061161236764706685000077428145620191801665089981239533688794005411241181694937800537950150999036497637985827266229993696434863796068012627265067303909297615039705139685292722060454298183532493071614521/31255330105883249568601424978798518438788802901706805034198764675482475241775910490799208189800271231679695370424082403108254764119246708339024251014517267613393687526300015669673087518666736640831215749311882839426682427957362344593492964535708225259664090787392337030843381603340953437546425186770339803405952707593047605683215385752757245538715768200620667296569211894678670790005182469973862932820426401426956486888360694405135529495120053948719266617748424232487886850003681492529024911048527485527013616828072900033607746898407280395855857330958408185095680*y^6 - 920048402378150237320116571414313121076150844046938838204328654030344051196082531464322560582430979943162104807950217306397640828850014968552100618277438745190276551483396745243304731475496827364641659764764582423290522605630357521502033071665266558586557684309965239739222211082753557553036896060713805504647964648180472799937983295660376430810266072123307716195190882809222471164432434497683822688158791774962917880847766101642768239202373400352594886952854288417646898464287276421059768924434637644243415091918087873730213817192610649623643419668751489700547942877/1844064476247111724547484073749112587888539371200701497017727115853466039264778718957153283198216002669102026855020861783387031083035555792002430809856518789190227564051700924510712163601337461809041729209401087526174263249484378331016084907606785290320181356456147884819759514597116252815239086019450048400951209747989808735309707759412677486784230323836619370497583501786041576610305765728457913036405157684190432726413280969902996240212083182974436730447157029716785324150217208059212469751863121646093803392856301101982857067006029543355495582526546082920645120*y^5 + 2098628399627894539180406917921017873528894098422012237184970496142361319266146199290335171884522606600760050723455998253757565232296797215957244029951890600675421611098406112571616699464074205207354444345676989764417993264517104154993546362119827230941068272604935146498951219654551427091562261304912999636371311342477614003102750460845503803194212913862671102100698428847077960472552003812873988007181676078759425716854481545652027940471112033116681725796242949155712888219906021385443226321404665546966305755111335474822594385121817897974264234362843920434298285/737625790498844689818993629499645035155415748480280598807090846341386415705911487582861313279286401067640810742008344713354812433214222316800972323942607515676091025620680369804284865440534984723616691683760435010469705299793751332406433963042714116128072542582459153927903805838846501126095634407780019360380483899195923494123883103765070994713692129534647748199033400714416630644122306291383165214562063073676173090565312387961198496084833273189774692178862811886714129660086883223684987900745248658437521357142520440793142826802411817342198233010618433168258048*y^4 + 23754002823751433426394241014244877748457053893903516803771453435643647514673200112953231086796933268107317197646311784412040923043728055776748696284409067044944361782402596736771569244214802694297441109474772876718231329238045092909480698552855854448991101044153794272927603044355839290378118074398350811426801452611095338377322660342640177998417414040218530027311882643961269590796036351341347709916521406550037528923064850545617549273029430103692090790115790117014155947561189870398482994721529104075181222170146038276048695646605188936980060825869001676296073133/922032238123555862273742036874556293944269685600350748508863557926733019632389359478576641599108001334551013427510430891693515541517777896001215404928259394595113782025850462255356081800668730904520864604700543763087131624742189165508042453803392645160090678228073942409879757298558126407619543009725024200475604873994904367654853879706338743392115161918309685248791750893020788305152882864228956518202578842095216363206640484951498120106041591487218365223578514858392662075108604029606234875931560823046901696428150550991428533503014771677747791263273041460322560*y^3 - 3106491151802984003348801853577161701380705966127741111132904934585145310272600903605070253815074896647501810797348900310745267075747825196015990711140211025936588243628417617091683823432901364948748744082979803608348222891407266536069060214693354627261066205148505565108315754744606079671103124230852719935754598129170130853791685871950984286943674011663272369186942305390915303648991478988752903548392961340515394358316223423103879642241510616393064455871128592502082465318818259864772759476540675453281667232324231051535386925568630714407126877531923819306706483/3688128952494223449094968147498225175777078742401402994035454231706932078529557437914306566396432005338204053710041723566774062166071111584004861619713037578380455128103401849021424327202674923618083458418802175052348526498968756662032169815213570580640362712912295769639519029194232505630478172038900096801902419495979617470619415518825354973568460647673238740995167003572083153220611531456915826072810315368380865452826561939805992480424166365948873460894314059433570648300434416118424939503726243292187606785712602203965714134012059086710991165053092165841290240*y^2 - 252273333855069097341484594341626252066760826209693312283865925332853378486221996684689821709257175987510230420262865166743362944880613911459893696098638634357320265895266150465605205916273760408070460477824032661645288598910315092588999516128175776209516596306170049457006482614237888618935627192107222826222212837178114381537519701336545200610309332997499298024791608548186735294700299361031523386478208063927116800872005933515474254620320372828356116255392078872466208319604181044767054955549837313273435636510546474697759771941562446715746782278792669715705809/737625790498844689818993629499645035155415748480280598807090846341386415705911487582861313279286401067640810742008344713354812433214222316800972323942607515676091025620680369804284865440534984723616691683760435010469705299793751332406433963042714116128072542582459153927903805838846501126095634407780019360380483899195923494123883103765070994713692129534647748199033400714416630644122306291383165214562063073676173090565312387961198496084833273189774692178862811886714129660086883223684987900745248658437521357142520440793142826802411817342198233010618433168258048*y - 14826023901172534624307868308065832386121554080413303195309807785610740189861920071714949555464833882246109389922350030090111760760663842842918514478745912395423112080743543034111224294917841086823238859987428870472070584239185840541282364175876389888123454883351553650981790782239560048104481420441181063854020965985755740048082439465123535566035239626898635509691334003946892826937567048859368306134076064665759230400552657738319405622287828601779273092717847746396761389913045017834772166453586664743907180485859209305033947024308300740043236236439003527808899/1844064476247111724547484073749112587888539371200701497017727115853466039264778718957153283198216002669102026855020861783387031083035555792002430809856518789190227564051700924510712163601337461809041729209401087526174263249484378331016084907606785290320181356456147884819759514597116252815239086019450048400951209747989808735309707759412677486784230323836619370497583501786041576610305765728457913036405157684190432726413280969902996240212083182974436730447157029716785324150217208059212469751863121646093803392856301101982857067006029543355495582526546082920645120