# Manifold: Census Knot K8_131 # Number of Tetrahedra: 8 # Number Field x^39 - 12*x^38 + 8*x^37 + 387*x^36 - 1927*x^35 + 1382*x^34 + 19210*x^33 - 128690*x^32 + 113901*x^31 + 953597*x^30 - 3579130*x^29 - 318370*x^28 + 21828585*x^27 - 46543586*x^26 - 63229613*x^25 + 417822714*x^24 + 280957552*x^23 - 1835472712*x^22 - 1661213680*x^21 + 5172803616*x^20 + 6817275200*x^19 - 12552529920*x^18 - 18815167232*x^17 + 32066877952*x^16 + 34612299776*x^15 - 69954549760*x^14 - 45599571968*x^13 + 102243450880*x^12 + 52536000512*x^11 - 87368433664*x^10 - 53039071232*x^9 + 35434135552*x^8 + 34507849728*x^7 - 1128792064*x^6 - 10891558912*x^5 - 3124756480*x^4 + 1430257664*x^3 + 822083584*x^2 - 50331648*x - 67108864 # Approximate Field Generator -0.238509590237000 + 0.477520108019706*I # Shape Parameters -1655591670639455619283686703794474105501081451409942077295667917957209621119676282904815496058873985683500788426925739768218030382987048102398700638361053844313/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^38 + 6340374183530178230679870129303292105597668057601571339563339130139450630322810055739197651968852360889414866499297597226720208531855906538291762873157239373675/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^37 + 4836690334615068017156631011829329962651660886198705555882562025917166659646353067097905946253052609017924780688551249373857220449007641173496322403588537295489/78633077359257454812889844140436935624090189466640083932832631311655258781360681731830733263057411956987434539468472069126252325458331727281727765195250251160638980096*y^36 - 753563322528463024325989735274002839832645289084546735009818850201933998559231602611601657765082827994941743051893036058669086044808583581943861924547749089910715/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^35 + 482296792791005023437641290861054309559556224817564308397985596170481069702252964507989614971959173774984980751232085530481706682337378472772243709562516880074109/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^34 + 253119354678888764792014863320808788745897138954261584599051372646879220838625059748929210864013491386256295345644439149631752945148846015486670115638061761728929/24194793033617678403966105889365210961258519835889256594717732711278541163495594379024841004017665217534595242913376021269616100141025146855916235444692384972504301568*y^33 - 25582874679430390780998158482916196837802979434847935129110757277372582264511630795116423162499384107151430731854420161833054853430187490223101595695184648053427959/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^32 + 44282030885809478732760878585574560643588247168566887744051716795085810347683309280373732730159226701889779729331305060463772117494614352455292674668400083814352171/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^31 + 804766823711154532244534220112775757096320167806597113984553010833086873516118037988959192317222711227692447814161253382884629235517780826136397768792945486771784695/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^30 - 3002334582173549571636772455338354628693239505076883907414455831110487745821856768233800792646188365100211576659284406474461754250445491419669970562663678616183139571/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^29 + 5337940904961509799483852566054858036297295088843315512532256091515579394937156590685395713495804033729334107208319345993771389614020960972833593948778389826233511/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^28 + 14660139375236709846869329651786387055899729583014107585106461764667538151301158799518923238884376199965789196938451195761408053523060357766721520949001615861543537695/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^27 - 51280394109821567593045613481885617043149953511241008069089666018510255475158276757199060695116053263877690131435180828119935271004276249887400218096043462482208094309/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^26 - 16643203760734069324195590203256377269818681315632955843337641257150655714529368824567141373011318280015035810193487076687167423378475841671796630822881704161764633657/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^25 + 513859658397597318894720816022866614858228082827658642050016925103342797265357004984831528995482848071809331534452288763815139032115014742578658887919541495320973540257/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^24 - 124107162516764489202230888592089754107592164340817851663137146078227982667885840174318387250479132123404286041553910467203200205263618270386537506381986574337643560787/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^23 - 877123287720623371964644456283376465348781759755461935429449730550195823914117003855992871996752962475131750493572056648991983419334791313996019757466181633006000519787/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^22 + 340574415950836014429393741623166768447641362492148455138768072996889459721763704646641632644546422744751549528647909253055822224210233604149853841907583719489215301529/157266154718514909625779688280873871248180378933280167865665262623310517562721363463661466526114823913974869078936944138252504650916663454563455530390500502321277960192*y^21 + 986743953710843457451983369085206173490347054499806314973497047783367346391365694011915546006649948377312697515542696973646954351148834243176305026276106152420706347693/78633077359257454812889844140436935624090189466640083932832631311655258781360681731830733263057411956987434539468472069126252325458331727281727765195250251160638980096*y^20 - 12029381897595421478191254940440937894677666466314977791400680220866037556226226778477605278753642375393959166089198890522939125321062206474625180731046909351167406653/4914567334953590925805615258777308476505636841665005245802039456978453673835042608239420828941088247311714658716779504320390770341145732955107985324703140697539936256*y^19 - 385451805872107245866143621947591434834872162400579406977017709282140351020819123805345058632126506781610214639740484831068996675977445507452589156513942351584274430561/9829134669907181851611230517554616953011273683330010491604078913956907347670085216478841657882176494623429317433559008640781540682291465910215970649406281395079872512*y^18 - 2957682718755603291763233576577103921732722949970539929215256322719255507778121725482869737558066726739325809227303072366364377928768438893324875828189245789823741937/378043641150276225061970404521331421269664372435769634292464573613727205679618662172263140687776019023978050670521500332337751564703517919623691178823318515195379712*y^17 + 504260729193407217262429064058760946002689358994848375688797573310277876318305116987571617885604655277409524507764401199456521297163688910949688001224492333969438034895/4914567334953590925805615258777308476505636841665005245802039456978453673835042608239420828941088247311714658716779504320390770341145732955107985324703140697539936256*y^16 + 59865861750839732445530992075642613843978142192416323652752938540196780914722831675353509843901779958863821995968190405480360721341024150780644382923892944584365783685/2457283667476795462902807629388654238252818420832502622901019728489226836917521304119710414470544123655857329358389752160195385170572866477553992662351570348769968128*y^15 - 299223609108480181755337347221217186044373085479310756132564822507115457708722628482603478360532152260574386653857289832887267771683656571184489323226065823698944049501/1228641833738397731451403814694327119126409210416251311450509864244613418458760652059855207235272061827928664679194876080097692585286433238776996331175785174384984064*y^14 + 509101650948813789923239777101013890092167287416273428504285964445394667600163488121451490479383298428371367127145325972089196262694355937787038406462776337411677025/153580229217299716431425476836790889890801151302031413931313733030576677307345081507481900904409007728491083084899359510012211573160804154847124541396973146798123008*y^13 + 17391140687272922308836401134810072939332527389574540008582820102090925024095739360713777570530589081466795126543746600481299260246641714236750711198940845170360159365/38395057304324929107856369209197722472700287825507853482828433257644169326836270376870475226102251932122770771224839877503052893290201038711781135349243286699530752*y^12 - 45736170026789449404820687759021532266629291278624187802028922957722408522172859368497611892405529554015587306017822831391623532254721502052907238620148988228719063/599922770380077017310255768893714413635941997273560210669194269650690145731816724638601175407847686439418293300388123085985201457659391229871580239831926354680168*y^11 - 44206181044428496755682406821068924513956624220135035143998689410480124131794861856405609540133820787286118930225815262090201671377668945575636540456566824657988164893/76790114608649858215712738418395444945400575651015706965656866515288338653672540753740950452204503864245541542449679755006105786580402077423562270698486573399061504*y^10 + 1491234422991043038852787761590613742263243765671452806426233500483935017797580071430261158460718877460544758623019129602793740857215465926654880161547232807807351983/38395057304324929107856369209197722472700287825507853482828433257644169326836270376870475226102251932122770771224839877503052893290201038711781135349243286699530752*y^9 + 1083882191746383828044156015039392200168460270517219353002109623797813238197626260180221157861033220900042179449438210728350833301372927912619697038492724028421635075/2399691081520308069241023075574857654543767989094240842676777078602760582927266898554404701631390745757673173201552492343940805830637564919486320959327705418720672*y^8 + 123054856149113876433444101604383052368273232468335701548547234462542666863992017805486973137689722382068850731016160096312302217942213251518656301588999650008564421/1199845540760154034620511537787428827271883994547120421338388539301380291463633449277202350815695372878836586600776246171970402915318782459743160479663852709360336*y^7 - 420074366491238369551378681378010200770824826638126803379887233944469351220449001686942222319501309668786496718847840032913336909418390659161780735150586444407176807/2399691081520308069241023075574857654543767989094240842676777078602760582927266898554404701631390745757673173201552492343940805830637564919486320959327705418720672*y^6 - 67162393019569071787527215444826956864824667444817581652949819102670086520245316205834254995677205763610016891252676610486689699847497522395303365120030900039442273/599922770380077017310255768893714413635941997273560210669194269650690145731816724638601175407847686439418293300388123085985201457659391229871580239831926354680168*y^5 + 9741778742267331616861394795099917746936356018932683992467133832270538936499694314990970817368162834418127824434862889801451727090809778839101039208843327977024901/1199845540760154034620511537787428827271883994547120421338388539301380291463633449277202350815695372878836586600776246171970402915318782459743160479663852709360336*y^4 + 2251491728261956210339774143469107025140729914288220098782908900660895597091506943512827922271322928557667977268094366665590603904625916012519348370617982377056131/74990346297509627163781971111714301704492749659195026333649283706336268216477090579825146925980960804927286662548515385748150182207423903733947529978990794335021*y^3 + 570826161099002010436197755205168390092350090487307917606321982245472276812937363973660058441116662636276522949415405011492615880275888063885540458932754207460566/74990346297509627163781971111714301704492749659195026333649283706336268216477090579825146925980960804927286662548515385748150182207423903733947529978990794335021*y^2 - 173864580405193842640862106698218417894942775994918363062167363272892860531738330004307880916288830697220867735241868122026117830194308575293078399033747963147773/74990346297509627163781971111714301704492749659195026333649283706336268216477090579825146925980960804927286662548515385748150182207423903733947529978990794335021*y - 40996849914792697668953694892844510815749863447134194647952325509428809441668711009224901082749525400955555015536610682667141422066724134899136446896073118162028/74990346297509627163781971111714301704492749659195026333649283706336268216477090579825146925980960804927286662548515385748150182207423903733947529978990794335021 -4468079148246572702897136053495969464173514280778351776241951665559918763955566185658641402466244770227289205863413475397835231149930024361353878326988548715872089/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^38 + 27124366890504739478517107659708663823534131957524143178859117909478613352330782983297482295231560095682157297049701510917561059628870245093659570044224115043474223/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^37 - 2825932979959427816560549273397902878537018693930171974661195287698159571826380486532633596016577085689806406175982035922028123691828184856218822807235913809297999/4324819254759160014708941427724031459324960420665204616305794722141039232974837495250690329468157657634308899670765963801943877900208245000495027085738763813835143905280*y^36 - 340173674559703418609737607992599197378365964074268378709096762567653232389317695819785196600172985012234421878651711682529931572839790607504930397606228249244706319/13839421615229312047068612568716900669839873346128654772178543110851325545519479984802209054298104504429788478946451084166220409280666384001584086674364044204272460496896*y^35 + 8831456436096192394389135020962608570497576470016525500919181840058144011464091731436370227040989906491842458729991399457079828948399775840549046622234116427956483413/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^34 - 155844419967298173997464510644563769831484014228981482655112643679759801207044370187729909963136175668857824447270781520697637418119046079367707119716259408768474557/1330713616848972312218135823915086602869218590973909112709475299120319763992257690846366255220971586964402738360235681169828885507756383077075392949458081173487736586240*y^33 - 40558079415865063986706676897498426488864007628042990914138600374800848119659999323925748562193449000629928550963248053186871725506767058304873606126634495385223833511/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^32 + 291493747427029322402569310331305846915560410972110854607814383384959135568437991018002298120080402438539649605793108645587188964846843980098071193078683662330611188427/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^31 - 623304600981792715080154555997154768087672373471430869114697713435591289877112172422113538662404476848027600819690084409271295124523142871697180550738657017410388748857/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^30 - 3937476268513212294881345979477850641961986211689578332030782923576370795407142248791178374848808905212524159054518536721045995397805282756007457065773166477555809244139/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^29 + 4071540181826647788382354165176954669915857848550395686185074457438100687605755013461666087058631266937903037552637155879885028200660982832952367588713255621401750709857/17299277019036640058835765710896125837299841682660818465223178888564156931899349981002761317872630630537235598683063855207775511600832980001980108342955055255340575621120*y^28 - 1208077365628737455385967879425035045260904621471814446850339342679761453303386937194583135895812298184143503132485343052807738794734112916765658551865936213700518023393/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^27 - 90623840396009997827423494038120319739203611396507152678748994968522925794144960571429093970466188771504427546120116227093529827698676197741011011407938981072841222501573/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^26 + 10967441973995676241173775204400681084714430740638563552799381552124884888035757317617900270964338451123754096839934878211649749012057812325070602066630613068010188222717/3459855403807328011767153142179225167459968336532163693044635777712831386379869996200552263574526126107447119736612771041555102320166596000396021668591011051068115124224*y^25 + 216154495363317406739122061204201886675635784213780463036351249722230838812647743588851807104535650937860350604304873286652134510201884880010571621076480281791205260321937/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^24 - 8217934635135424031569068727788931020287106990557642966028093375687183365955259899101329364470034118136777335473545313141764697036257245298555205811167646002303615760407/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^23 - 230235779750474945907601696925693585128019902618592210894646355466113713216055482724089989188395646481781232252086507744782938751557367840620345398243604027141797145740647/17299277019036640058835765710896125837299841682660818465223178888564156931899349981002761317872630630537235598683063855207775511600832980001980108342955055255340575621120*y^22 + 951932610209659992886623199764263585054684324646149006702301111214201239210434871880719579491399097249041110778373843947073986743658724084658246101149581334442992845911203/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^21 + 375845609644394339722041882185517209232437861979954836435625374527420069462323746552483448426373394313271485953162366130121086575085961123734643758107648945264107211405007/4324819254759160014708941427724031459324960420665204616305794722141039232974837495250690329468157657634308899670765963801943877900208245000495027085738763813835143905280*y^20 - 164167720236774236514662982711102509361916953433871830851054229827074611227591089293767515554327461662089117305392041417485566738450297584222064922224584195982812351287131/540602406844895001838617678465503932415620052583150577038224340267629904121854686906336291183519707204288612458845745475242984737526030625061878385717345476729392988160*y^19 - 49390682294097840707791410938823094839286465763779380983179134917384758198447318871631326440041559294234939349418416083839549438598418398273771727394095578479464554438687/135150601711223750459654419616375983103905013145787644259556085066907476030463671726584072795879926801072153114711436368810746184381507656265469596429336369182348247040*y^18 + 968645996537329681997910402183941486001239985445166812187716752621402620128803160514347324256163042974727177020715755072657014404934958798695877312789756597083370517091/1299525016454074523650523265542076760614471280247958117880346971797187269523689151217154546114230065394924549179917657392411021003668342848706438427205157395984117760*y^17 + 263666886827163029045823485167083202862632932145103244393670555141036931848798102639295976597890848514166158662558634656925293659568869771210470816887060576616068183481497/270301203422447500919308839232751966207810026291575288519112170133814952060927343453168145591759853602144306229422872737621492368763015312530939192858672738364696494080*y^16 - 64804112330623651241554745678572834451266493720480492989681536883218884519494796072889871421117860890244451431897809600484883498106339972955610825358640412752018427463819/33787650427805937614913604904093995775976253286446911064889021266726869007615917931646018198969981700268038278677859092202686546095376914066367399107334092295587061760*y^15 - 21763146403072806669539561273177753153679467990608322737374382671758409628691710190336380482583348809867459955905410078185880281339624771576832376556425741086951418048297/13515060171122375045965441961637598310390501314578764425955608506690747603046367172658407279587992680107215311471143636881074618438150765626546959642933636918234824704*y^14 + 26972620922472089622728716188925931763906617627089029309064255424744660027755601148617362132556861083241418666987619041652861908663044664515525228225270284818722240454681/6757530085561187522982720980818799155195250657289382212977804253345373801523183586329203639793996340053607655735571818440537309219075382813273479821466818459117412352*y^13 + 7714380309626848953257098063856446798418000097611441714495045355066948254221261624039729371024494459493350497629336557104327343112785034372521132186796548199396753799223/4223456303475742201864200613011749471997031660805863883111127658340858625951989741455752274871247712533504784834732386525335818261922114258295924888416761536948382720*y^12 - 22460780902312473760792905064575201589757408590029310826869647149831035686279466025256232490778883672711913852868926432183105227773976427890093807990512021695156219472481/4223456303475742201864200613011749471997031660805863883111127658340858625951989741455752274871247712533504784834732386525335818261922114258295924888416761536948382720*y^11 - 219195401083983310090131081536591580238149932874966191436876140637854129192388941033307343034324864538428225083649866575395141252584903344167133494211662313846408814467/105586407586893555046605015325293736799925791520146597077778191458521465648799743536393806871781192813337619620868309663133395456548052856457398122210419038423709568*y^10 + 4163728826018836085784663412927057978862282774114450502326125423414277326961461572697911263975617463621008409951768561268660131720012675567230632169394078148545970637851/1055864075868935550466050153252937367999257915201465970777781914585214656487997435363938068717811928133376196208683096631333954565480528564573981222104190384237095680*y^9 + 2385042798056933291359454100035686410335599660711652392927213093912687886393293663109547819143894110446472632665252704044192472806307861159810773460496882707464870681151/1055864075868935550466050153252937367999257915201465970777781914585214656487997435363938068717811928133376196208683096631333954565480528564573981222104190384237095680*y^8 - 123956164268609139754069351300618972641967847178368746564870752912511810563628349582180328934411429453574746525837394323072062981034085899766488859215035228671241404099/105586407586893555046605015325293736799925791520146597077778191458521465648799743536393806871781192813337619620868309663133395456548052856457398122210419038423709568*y^7 - 11283025412310679096327268941466863483477842775836872587605539984326541047335799696153901016408217722499407921310864658831207245344786359325171781096903308159870619879/8248938092726058988016016822288573187494202462511452896701421207696989503812479963780766161857905688542001532880336692432296520042816629410734228297688987376852310*y^6 - 2281982412791945793746261677284476359317356463411116009441789027073018504637997034121319556049727736820461541586614794368446765200865455602965397617550637751623610291/13198300948361694380825626915661717099990723940018324634722273932315183206099967942049225858972649101667202452608538707891674432068506607057174765276302379802963696*y^5 + 19112654829011539395817167356339670837181697610616367049337058271220404737103037704456108814130856733439554192092533763926162667491225822597935355445915037960221910223/65991504741808471904128134578308585499953619700091623173611369661575916030499839710246129294863245508336012263042693539458372160342533035285873826381511899014818480*y^4 + 4196848696873677497776895780342013034870231171814935476790624850717140454139306126621971957354887661022876757908249579954752060244500696630164932658582851730941829097/32995752370904235952064067289154292749976809850045811586805684830787958015249919855123064647431622754168006131521346769729186080171266517642936913190755949507409240*y^3 - 203372009761872183436148201830725564608625106030534861805297387618089044128889447986113719986810838624382678249907307983578224121676605368198669865409872212359733891/16497876185452117976032033644577146374988404925022905793402842415393979007624959927561532323715811377084003065760673384864593040085633258821468456595377974753704620*y^2 - 119605803079504572541826438521201621840848657784908454261965778785444154367110700264739315895409642580974512335042581363340113526355415962586356946844645915659601771/8248938092726058988016016822288573187494202462511452896701421207696989503812479963780766161857905688542001532880336692432296520042816629410734228297688987376852310*y + 3531439238241821951342858881473835688755683368170918437380466305888249216182836817876119468201665250942378466343370170617730215537556342924773173881614782346917213/4124469046363029494008008411144286593747101231255726448350710603848494751906239981890383080928952844271000766440168346216148260021408314705367114148844493688426155 3523039355642782521447944022551988084940422977165598236369518081794481636130936825078720320307637522986699761430655703414323234054573058506457493081872980602193/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^38 - 20513402088602479718571513648330084296086237714527458680296319754912893332997669865872106700181518034228065796499012060668460876842782715061450171737216500951203/24194793033617678403966105889365210961258519835889256594717732711278541163495594379024841004017665217534595242913376021269616100141025146855916235444692384972504301568*y^37 + 122184962396892718997697790099586651848170589333744424955895394953106813241478019082155667153799255539386165266291708476917232499793052503784628050849572757559/378043641150276225061970404521331421269664372435769634292464573613727205679618662172263140687776019023978050670521500332337751564703517919623691178823318515195379712*y^36 + 1344559266239435221406389532038153791000588883267348366458219430527266522421720737285345337913151427360427750269619201322633118848394157264670223281635126583057439/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^35 - 6290397683097652648949831113562919929359067450165280068114640088014453944673506719665207218390600962834795765388571201362274871596755175595567940841242755113874341/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^34 + 847505314074441560670092017480530208982459402919585620547858321114898612452863982382194985969482865304546417770484427505856232674587411154716300944235385513973127/12097396516808839201983052944682605480629259917944628297358866355639270581747797189512420502008832608767297621456688010634808050070512573427958117722346192486252150784*y^33 + 32456597601036804330647219666152290681990132378061392035750003208026741295005412948269226441137560024789055710379221403554977414823301605584928399729005813248412833/24194793033617678403966105889365210961258519835889256594717732711278541163495594379024841004017665217534595242913376021269616100141025146855916235444692384972504301568*y^32 - 213155553587526111809676496070351643666110732453497874096489730275127533241676582910281058312760536059038990441426861539823109542918735867369641883833113430122595397/24194793033617678403966105889365210961258519835889256594717732711278541163495594379024841004017665217534595242913376021269616100141025146855916235444692384972504301568*y^31 + 284567351596043570248821018139229989941860217286863561211541447791237601548552503213651358101127864860472321473551526603705007892907390508900562957516381002942964841/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^30 + 3200213939655131711421528754501758947317333442034357097739106119068247116575202112308821146753388291125580534293068944899206931344881851527096508704481113938075345395/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^29 - 2793872269509113496736672183629698214686634984651041091525453250624957408538656974417085086222721892562454507538546381778330755475636322763104507435897407584016819473/12097396516808839201983052944682605480629259917944628297358866355639270581747797189512420502008832608767297621456688010634808050070512573427958117722346192486252150784*y^28 - 1721661037576838886258938284879993047482732837804041322448158663180543639835388655847757561655157670890457311259208989706899235269292616762810676146341289729858138361/24194793033617678403966105889365210961258519835889256594717732711278541163495594379024841004017665217534595242913376021269616100141025146855916235444692384972504301568*y^27 + 68495306979099550303393092895204023357530291705232802517188140052934133499536776724127200983086668200305901599866661621235136174364814996130014510142996453938014522825/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^26 - 34445222372120822484172810693129281012827651880760813609827365896017789852489344056319133863771118430280311518481015536443555354705259693078483564615208514011847707453/12097396516808839201983052944682605480629259917944628297358866355639270581747797189512420502008832608767297621456688010634808050070512573427958117722346192486252150784*y^25 - 234296446332542963639438615050739282092348332719484654467965777273510898874765492139511831578768377807207722852069577547539387671440459220461796155873336319894299754049/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^24 + 161394226433646468295953940519045580355388019229855053890088290586740658808769706407308773186566330356501420906467765706696133642809016249658812478971394436678725269713/6048698258404419600991526472341302740314629958972314148679433177819635290873898594756210251004416304383648810728344005317404025035256286713979058861173096243126075392*y^23 + 342027437810924654471950689495293840691228308367528184392445145791579464541220999775439205972430184327276689634146359236875518257642154170323397323650063266635847489705/12097396516808839201983052944682605480629259917944628297358866355639270581747797189512420502008832608767297621456688010634808050070512573427958117722346192486252150784*y^22 - 1303424315299863955439662486135332605350809392658213029890399578433662140578038033062667396880547016166518747493118848554901343484389406079622126039209270476530334266653/12097396516808839201983052944682605480629259917944628297358866355639270581747797189512420502008832608767297621456688010634808050070512573427958117722346192486252150784*y^21 - 915902227650190788950138934003588076043019347431288879252792927785611972193729282555285494526986394061963155856846704817410274378999928184615547978437372941368629836731/6048698258404419600991526472341302740314629958972314148679433177819635290873898594756210251004416304383648810728344005317404025035256286713979058861173096243126075392*y^20 + 196001887962063890206625694022028064935395856485114800103010790615073960784057944055406305734506719433228481650085066402548735716878497033673176278042631025258416946405/756087282300552450123940809042662842539328744871539268584929147227454411359237324344526281375552038047956101341043000664675503129407035839247382357646637030390759424*y^19 + 811472842175279639318281947760355216672416230997652959998778347720286674239226695750554007546299138660543324141836027960295534173894739236066537001464083943129114075963/1512174564601104900247881618085325685078657489743078537169858294454908822718474648689052562751104076095912202682086001329351006258814071678494764715293274060781518848*y^18 - 419806815668031538249306755154367291657251471537173739471319396927629820399801423200136715016405961000423253543089567324991420730372780076295506165257901231684458120047/756087282300552450123940809042662842539328744871539268584929147227454411359237324344526281375552038047956101341043000664675503129407035839247382357646637030390759424*y^17 - 513355219671286656902130853471094470497299374880990108558031821528176632382790859318542910179064249335192963449421378686292970120655564026267530418781030515624425045007/378043641150276225061970404521331421269664372435769634292464573613727205679618662172263140687776019023978050670521500332337751564703517919623691178823318515195379712*y^16 + 136100753968872716078232877108361662382209513257224543644249660841584366368026009831464518788056016980778984203810428455861229968224840140260365617150640415683256588701/94510910287569056265492601130332855317416093108942408573116143403431801419904665543065785171944004755994512667630375083084437891175879479905922794705829628798844928*y^15 + 118206617760461041721121766271728576414301411728653744798613240233097215642104912753241046800824306191818949339567550097220559653699309872679488048710385770702808632171/47255455143784528132746300565166427658708046554471204286558071701715900709952332771532892585972002377997256333815187541542218945587939739952961397352914814399422464*y^14 - 148031847756679758846705614992472612276392513303702976934173136705086489762954587542392625820333323428142143818976637777990260986464153161588473348838321291883886634803/47255455143784528132746300565166427658708046554471204286558071701715900709952332771532892585972002377997256333815187541542218945587939739952961397352914814399422464*y^13 - 42868527496117115493303950924102876848464481290015250082557136409167850234669106687105005610372882253771163190652516638798091199124291755115438358406420987836482265589/11813863785946132033186575141291606914677011638617801071639517925428975177488083192883223146493000594499314083453796885385554736396984934988240349338228703599855616*y^12 + 47424753331149102427147418324162893158491577586931250586509549242279657880991799283886405020454822578125170563360054837264788351762944930055393955574615046860437730861/11813863785946132033186575141291606914677011638617801071639517925428975177488083192883223146493000594499314083453796885385554736396984934988240349338228703599855616*y^11 + 6504271842806576177755381939035460605784224156899756684298394990285826182411694786336277936295242428122545530813107813660380027269315314591521219964579262438427124333/1476732973243266504148321892661450864334626454827225133954939740678621897186010399110402893311625074312414260431724610673194342049623116873530043667278587949981952*y^10 - 806216279657478235365072341532837517522541766012307457245498962174803293687925152115587000376255179254618784911757480009190463259478910390537703158052854382938315297/369183243310816626037080473165362716083656613706806283488734935169655474296502599777600723327906268578103565107931152668298585512405779218382510916819646987495488*y^9 - 5395916962793497558493206359119058882308550445002612942584844626321339059453697546576138346179288095443740682874293246301124004849899615225078214807142464460688619119/1476732973243266504148321892661450864334626454827225133954939740678621897186010399110402893311625074312414260431724610673194342049623116873530043667278587949981952*y^8 - 293665171024697743331742843482301097176873797631240925253178076810385692470495205431350830086972298915842524471748756076011992216710351770817028510751162937937534125/738366486621633252074160946330725432167313227413612566977469870339310948593005199555201446655812537156207130215862305336597171024811558436765021833639293974990976*y^7 + 252626077722721106183440660076315249402729889039468300422789725924145584266975073431893106578972307375380139776573897174839399229104156510535732764494933073467156351/184591621655408313018540236582681358041828306853403141744367467584827737148251299888800361663953134289051782553965576334149292756202889609191255458409823493747744*y^6 + 142929807758518498387899991099998693827027099815112303921217821750804516137387135409308563239361133721593580208941969546866051056834227290487768991355578890792506481/184591621655408313018540236582681358041828306853403141744367467584827737148251299888800361663953134289051782553965576334149292756202889609191255458409823493747744*y^5 - 1155420798166262412700199479056693773057888747420374520086078856135254650545613248278578184514331433850098249886185743081217115044071426872675710315007418202668717/46147905413852078254635059145670339510457076713350785436091866896206934287062824972200090415988283572262945638491394083537323189050722402297813864602455873436936*y^4 - 7437280911243848469642074858225210534837930554685669347361392331133314522454679054085593477424313474858972131256217233680038275204700894956941845604227427047226971/46147905413852078254635059145670339510457076713350785436091866896206934287062824972200090415988283572262945638491394083537323189050722402297813864602455873436936*y^3 - 263770593630580333222844301946137868873839356417235051940409869238771291760688690784960113339243500207874711391116897470693409900010814525088974371398166304020153/5768488176731509781829382393208792438807134589168848179511483362025866785882853121525011301998535446532868204811424260442165398631340300287226733075306984179617*y^2 + 64917420560309205312123607536798254049318630308949494183519107889207765994958648561090914983515953551488661847804349252409592955320468836273862539648467443070839/11536976353463019563658764786417584877614269178337696359022966724051733571765706243050022603997070893065736409622848520884330797262680600574453466150613968359234*y + 18067137649035693957166254135965213789906444715719881282307304399248318773735596164695459985335753265576998916850285388309884060130830690493046979166393921270739/5768488176731509781829382393208792438807134589168848179511483362025866785882853121525011301998535446532868204811424260442165398631340300287226733075306984179617 -60165969169234069974905326778789854069549462281586955715171886098678204243604302082360317346741304280833153772226090516942219688618383381472734156414487524123984153/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^38 + 187639950370696318665511216364618920667812116175238883125161043706012240548821466622887687179982201757765820911748904815074096184701771042413124754018468313577196233/17299277019036640058835765710896125837299841682660818465223178888564156931899349981002761317872630630537235598683063855207775511600832980001980108342955055255340575621120*y^37 - 104885006411564388464702567739884071350550620889764860496171456803556433740621446758276890089783773876173735911340435606485502145184369162380062353476299711579252191/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^36 - 4574264974839438283190230692056796076307369290796950326982734496667305391220240933931334397781193308017730852143152129375711432861211565078915567617094306900492827599/13839421615229312047068612568716900669839873346128654772178543110851325545519479984802209054298104504429788478946451084166220409280666384001584086674364044204272460496896*y^35 + 126809731889235719660983286954387051524338118970176380105251180858728054047384857878879849407671833661834703126197596045040592168264054298302969700648521642745571573271/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^34 - 71941759453067327912386108611154504407065475061549659790966533467284711615707263917144732438312292133146528478903761756879014580767422804511541146820607404703932693559/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^33 - 542780019766553160879952106512721213573203099237404165732140277368458632356955775144843540087820397421075391683696438470880451884821424212859266527781827195716048176317/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^32 + 4129598783818208405756351248120257130975194555299630249863598317414995779537278693644931062633619199548635870193188160685931763738516430152548928073047789967641859238329/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^31 - 10800638893309446323532899204562520830728528296297444787386776920340823251998756032332111835514440601352020209493268794179044260333352060440082439252820608470972171099189/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^30 - 52104476181691277751668257823314281625290483471404584505843858040531985237058254920421263352827226449961392728617938778205789383961048674708041071930377115135888928438653/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^29 + 120066827977097511247454642204487549543195430669263297361725197493584207891366172432286829897642760233820759254381475206237201090163437383758202317724413698994302614745433/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^28 - 48084504681425707441639089321323034899944322186485804949946463974633087360523088840831733393874176630695549541394183589577725650671215873874319526702581792652832470022071/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^27 - 1264490627816234419920966143318701198505559375624270791972732433236598753390861069174841341065613004683161177256788221597390349540531313981288481112591968123587088877737041/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^26 + 340600867383191052542752193721696689626423352765856586559586610098055853710610557272047604991583429618058048084364976157070949056213539430963610926474743070968848848315441/6919710807614656023534306284358450334919936673064327386089271555425662772759739992401104527149052252214894239473225542083110204640333192000792043337182022102136230248448*y^25 + 2162515075083640322879699763009702209395068785223929385898259258860083142865278551057004639745607343975937945010029124311270743315066534651616314629188082011141112252430949/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^24 - 237585084667893001907567419774665006633335283310635178665995971772386762543566659816154100644738891451042547082155921378336840836078055122171189291556242643145722447376183/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^23 - 272262434290810306735031712016213601942084099497967585690990654082685414436030086037251587327593134533094288534363652955505743519927107150431544131395554481234987163975751/4324819254759160014708941427724031459324960420665204616305794722141039232974837495250690329468157657634308899670765963801943877900208245000495027085738763813835143905280*y^22 + 14011759226362399798705596470380971064800196710614257322512234794910333120729273446576869107415939938905731024341338469744452392990934045758020123681716989872690661297331861/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^21 + 2860437889573045422722373408766212497150837738953265224797787456165603284943261948208125304809637401002928565968898002717621183022990988647535393423254516283926030044454619/4324819254759160014708941427724031459324960420665204616305794722141039232974837495250690329468157657634308899670765963801943877900208245000495027085738763813835143905280*y^20 - 10362748831037346278654539571609618643170492199825122054141483823219687531863402431805460246146790073729734364086910018689260542199990130373877651930280215293930132107335193/2162409627379580007354470713862015729662480210332602308152897361070519616487418747625345164734078828817154449835382981900971938950104122500247513542869381906917571952640*y^19 - 3884529788291011900251171195180428830335192302437616693149368850782183450024399857245492567670734006661229145910327457530288186809288019758314936489568040865921894832010877/1081204813689790003677235356931007864831240105166301154076448680535259808243709373812672582367039414408577224917691490950485969475052061250123756771434690953458785976320*y^18 + 3403443757998988918727762634981882147218542872587186583169273543349545951043851446346832587738594562885100464420445420788218348736478228466749279484403963796799817033679511/270301203422447500919308839232751966207810026291575288519112170133814952060927343453168145591759853602144306229422872737621492368763015312530939192858672738364696494080*y^17 + 2758962410540822482282941513297285794405625642523579111528618100342039504638103961709557017695201031344410384697209842727678574488635165040094741059537280815744678564116879/270301203422447500919308839232751966207810026291575288519112170133814952060927343453168145591759853602144306229422872737621492368763015312530939192858672738364696494080*y^16 - 4418793116367472364932773147057721145787365275829730153599399073910646488266451754358787274008283558484177002728376592546237114527772293516949253695132238303114027227569627/135150601711223750459654419616375983103905013145787644259556085066907476030463671726584072795879926801072153114711436368810746184381507656265469596429336369182348247040*y^15 - 95601218666297731545565785946374075094753473903448009778031410738372229514284442971290706906213344158330679758397601733497129103462282972130788637893958357505691022434707/6757530085561187522982720980818799155195250657289382212977804253345373801523183586329203639793996340053607655735571818440537309219075382813273479821466818459117412352*y^14 + 35044797221780639583440680171455609993973842790135260536470113414608281423736529423121268166206151981369669990520702425383228035988828921170079279233384254743903972015419/519810006581629809460209306216830704245788512099183247152138788718874907809475660486861818445692026157969819671967062956964408401467337139482575370882062958393647104*y^13 + 28589336095845808111399868044425415929726859545867639711463639216779366960135882975701957312132442793673408241540517907969253565348525817994870206683251244823784060738561/4223456303475742201864200613011749471997031660805863883111127658340858625951989741455752274871247712533504784834732386525335818261922114258295924888416761536948382720*y^12 - 387399806246680574977667128485646822805846838157013042526768856202630175508419274592711974425567745984968161671038339442858390976766756903166893227573182334074604191194957/4223456303475742201864200613011749471997031660805863883111127658340858625951989741455752274871247712533504784834732386525335818261922114258295924888416761536948382720*y^11 - 634671367386416421920185200123394649363718286059254227909349074173964456783863156098103076263838049444604631679010784545465768341413667294334483639318788862659558030815/844691260695148440372840122602349894399406332161172776622225531668171725190397948291150454974249542506700956966946477305067163652384422851659184977683352307389676544*y^10 + 160156235628314921911786193894645968000543298721231056488182918713959605261820156975891347679455940750449503832111559797587509061351095120421744257659763979025969117943299/2111728151737871100932100306505874735998515830402931941555563829170429312975994870727876137435623856266752392417366193262667909130961057129147962444208380768474191360*y^9 + 1142401348785553523235866599198477820131870425243834897381172073966118780901734126366735599638080117882481293824737318899618218078371015517774824228578798994825462858089/131983009483616943808256269156617170999907239400183246347222739323151832060999679420492258589726491016672024526085387078916744320685066070571747652763023798029636960*y^8 - 3679328852984530632038381340093751776146129212084058244332958496329664127523114736440849796491481464189146355429765664071163088127392332768146205108483139698457254413753/105586407586893555046605015325293736799925791520146597077778191458521465648799743536393806871781192813337619620868309663133395456548052856457398122210419038423709568*y^7 - 3336381432259881673289010508494731169859812371004590068865532281376517694760656310734445084954460892533521492814957501586413165246447526434768736373664248590529257645841/263966018967233887616512538313234341999814478800366492694445478646303664121999358840984517179452982033344049052170774157833488641370132141143495305526047596059273920*y^6 + 190613135697467559656007478359913975176447590560938962390977874009587505376604414412602592976876292737761179352344240301529721347235553511214058399789834320659347765931/26396601896723388761651253831323434199981447880036649269444547864630366412199935884098451717945298203334404905217077415783348864137013214114349530552604759605927392*y^5 + 387058125499879677259765688538595760694570502398057327564351441643330409405153825043906680731790863787039539537154725351481460071351523232878301323226470803499702243671/65991504741808471904128134578308585499953619700091623173611369661575916030499839710246129294863245508336012263042693539458372160342533035285873826381511899014818480*y^4 - 3248874072199407076834144955435641364570282125099534383182237704864586431751036537879676959300661236269037824674792412667407068755447519965908211458109244425923729483/16497876185452117976032033644577146374988404925022905793402842415393979007624959927561532323715811377084003065760673384864593040085633258821468456595377974753704620*y^3 - 18907410208714691479072450997171696742569082374669391865186962933933664451436573857745279745397468438015401392483067352851404539293369111405754819216307529126484789637/16497876185452117976032033644577146374988404925022905793402842415393979007624959927561532323715811377084003065760673384864593040085633258821468456595377974753704620*y^2 - 605957294155724043275369959238179079309058255104377035362469972878885878189081303217917058891738020688940694464967800102572522356546468174630757998691998769780188831/4124469046363029494008008411144286593747101231255726448350710603848494751906239981890383080928952844271000766440168346216148260021408314705367114148844493688426155*y + 486726135434964204935106538464237090600961239327425958919860564902253149746747012115926309049004871934283766042329132734114211028207139488122348414503640459939716691/4124469046363029494008008411144286593747101231255726448350710603848494751906239981890383080928952844271000766440168346216148260021408314705367114148844493688426155 -60165969169234069974905326778789854069549462281586955715171886098678204243604302082360317346741304280833153772226090516942219688618383381472734156414487524123984153/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^38 + 187639950370696318665511216364618920667812116175238883125161043706012240548821466622887687179982201757765820911748904815074096184701771042413124754018468313577196233/17299277019036640058835765710896125837299841682660818465223178888564156931899349981002761317872630630537235598683063855207775511600832980001980108342955055255340575621120*y^37 - 104885006411564388464702567739884071350550620889764860496171456803556433740621446758276890089783773876173735911340435606485502145184369162380062353476299711579252191/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^36 - 4574264974839438283190230692056796076307369290796950326982734496667305391220240933931334397781193308017730852143152129375711432861211565078915567617094306900492827599/13839421615229312047068612568716900669839873346128654772178543110851325545519479984802209054298104504429788478946451084166220409280666384001584086674364044204272460496896*y^35 + 126809731889235719660983286954387051524338118970176380105251180858728054047384857878879849407671833661834703126197596045040592168264054298302969700648521642745571573271/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^34 - 71941759453067327912386108611154504407065475061549659790966533467284711615707263917144732438312292133146528478903761756879014580767422804511541146820607404703932693559/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^33 - 542780019766553160879952106512721213573203099237404165732140277368458632356955775144843540087820397421075391683696438470880451884821424212859266527781827195716048176317/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^32 + 4129598783818208405756351248120257130975194555299630249863598317414995779537278693644931062633619199548635870193188160685931763738516430152548928073047789967641859238329/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^31 - 10800638893309446323532899204562520830728528296297444787386776920340823251998756032332111835514440601352020209493268794179044260333352060440082439252820608470972171099189/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^30 - 52104476181691277751668257823314281625290483471404584505843858040531985237058254920421263352827226449961392728617938778205789383961048674708041071930377115135888928438653/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^29 + 120066827977097511247454642204487549543195430669263297361725197493584207891366172432286829897642760233820759254381475206237201090163437383758202317724413698994302614745433/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^28 - 48084504681425707441639089321323034899944322186485804949946463974633087360523088840831733393874176630695549541394183589577725650671215873874319526702581792652832470022071/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^27 - 1264490627816234419920966143318701198505559375624270791972732433236598753390861069174841341065613004683161177256788221597390349540531313981288481112591968123587088877737041/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^26 + 340600867383191052542752193721696689626423352765856586559586610098055853710610557272047604991583429618058048084364976157070949056213539430963610926474743070968848848315441/6919710807614656023534306284358450334919936673064327386089271555425662772759739992401104527149052252214894239473225542083110204640333192000792043337182022102136230248448*y^25 + 2162515075083640322879699763009702209395068785223929385898259258860083142865278551057004639745607343975937945010029124311270743315066534651616314629188082011141112252430949/69197108076146560235343062843584503349199366730643273860892715554256627727597399924011045271490522522148942394732255420831102046403331920007920433371820221021362302484480*y^24 - 237585084667893001907567419774665006633335283310635178665995971772386762543566659816154100644738891451042547082155921378336840836078055122171189291556242643145722447376183/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^23 - 272262434290810306735031712016213601942084099497967585690990654082685414436030086037251587327593134533094288534363652955505743519927107150431544131395554481234987163975751/4324819254759160014708941427724031459324960420665204616305794722141039232974837495250690329468157657634308899670765963801943877900208245000495027085738763813835143905280*y^22 + 14011759226362399798705596470380971064800196710614257322512234794910333120729273446576869107415939938905731024341338469744452392990934045758020123681716989872690661297331861/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^21 + 2860437889573045422722373408766212497150837738953265224797787456165603284943261948208125304809637401002928565968898002717621183022990988647535393423254516283926030044454619/4324819254759160014708941427724031459324960420665204616305794722141039232974837495250690329468157657634308899670765963801943877900208245000495027085738763813835143905280*y^20 - 10362748831037346278654539571609618643170492199825122054141483823219687531863402431805460246146790073729734364086910018689260542199990130373877651930280215293930132107335193/2162409627379580007354470713862015729662480210332602308152897361070519616487418747625345164734078828817154449835382981900971938950104122500247513542869381906917571952640*y^19 - 3884529788291011900251171195180428830335192302437616693149368850782183450024399857245492567670734006661229145910327457530288186809288019758314936489568040865921894832010877/1081204813689790003677235356931007864831240105166301154076448680535259808243709373812672582367039414408577224917691490950485969475052061250123756771434690953458785976320*y^18 + 3403443757998988918727762634981882147218542872587186583169273543349545951043851446346832587738594562885100464420445420788218348736478228466749279484403963796799817033679511/270301203422447500919308839232751966207810026291575288519112170133814952060927343453168145591759853602144306229422872737621492368763015312530939192858672738364696494080*y^17 + 2758962410540822482282941513297285794405625642523579111528618100342039504638103961709557017695201031344410384697209842727678574488635165040094741059537280815744678564116879/270301203422447500919308839232751966207810026291575288519112170133814952060927343453168145591759853602144306229422872737621492368763015312530939192858672738364696494080*y^16 - 4418793116367472364932773147057721145787365275829730153599399073910646488266451754358787274008283558484177002728376592546237114527772293516949253695132238303114027227569627/135150601711223750459654419616375983103905013145787644259556085066907476030463671726584072795879926801072153114711436368810746184381507656265469596429336369182348247040*y^15 - 95601218666297731545565785946374075094753473903448009778031410738372229514284442971290706906213344158330679758397601733497129103462282972130788637893958357505691022434707/6757530085561187522982720980818799155195250657289382212977804253345373801523183586329203639793996340053607655735571818440537309219075382813273479821466818459117412352*y^14 + 35044797221780639583440680171455609993973842790135260536470113414608281423736529423121268166206151981369669990520702425383228035988828921170079279233384254743903972015419/519810006581629809460209306216830704245788512099183247152138788718874907809475660486861818445692026157969819671967062956964408401467337139482575370882062958393647104*y^13 + 28589336095845808111399868044425415929726859545867639711463639216779366960135882975701957312132442793673408241540517907969253565348525817994870206683251244823784060738561/4223456303475742201864200613011749471997031660805863883111127658340858625951989741455752274871247712533504784834732386525335818261922114258295924888416761536948382720*y^12 - 387399806246680574977667128485646822805846838157013042526768856202630175508419274592711974425567745984968161671038339442858390976766756903166893227573182334074604191194957/4223456303475742201864200613011749471997031660805863883111127658340858625951989741455752274871247712533504784834732386525335818261922114258295924888416761536948382720*y^11 - 634671367386416421920185200123394649363718286059254227909349074173964456783863156098103076263838049444604631679010784545465768341413667294334483639318788862659558030815/844691260695148440372840122602349894399406332161172776622225531668171725190397948291150454974249542506700956966946477305067163652384422851659184977683352307389676544*y^10 + 160156235628314921911786193894645968000543298721231056488182918713959605261820156975891347679455940750449503832111559797587509061351095120421744257659763979025969117943299/2111728151737871100932100306505874735998515830402931941555563829170429312975994870727876137435623856266752392417366193262667909130961057129147962444208380768474191360*y^9 + 1142401348785553523235866599198477820131870425243834897381172073966118780901734126366735599638080117882481293824737318899618218078371015517774824228578798994825462858089/131983009483616943808256269156617170999907239400183246347222739323151832060999679420492258589726491016672024526085387078916744320685066070571747652763023798029636960*y^8 - 3679328852984530632038381340093751776146129212084058244332958496329664127523114736440849796491481464189146355429765664071163088127392332768146205108483139698457254413753/105586407586893555046605015325293736799925791520146597077778191458521465648799743536393806871781192813337619620868309663133395456548052856457398122210419038423709568*y^7 - 3336381432259881673289010508494731169859812371004590068865532281376517694760656310734445084954460892533521492814957501586413165246447526434768736373664248590529257645841/263966018967233887616512538313234341999814478800366492694445478646303664121999358840984517179452982033344049052170774157833488641370132141143495305526047596059273920*y^6 + 190613135697467559656007478359913975176447590560938962390977874009587505376604414412602592976876292737761179352344240301529721347235553511214058399789834320659347765931/26396601896723388761651253831323434199981447880036649269444547864630366412199935884098451717945298203334404905217077415783348864137013214114349530552604759605927392*y^5 + 387058125499879677259765688538595760694570502398057327564351441643330409405153825043906680731790863787039539537154725351481460071351523232878301323226470803499702243671/65991504741808471904128134578308585499953619700091623173611369661575916030499839710246129294863245508336012263042693539458372160342533035285873826381511899014818480*y^4 - 3248874072199407076834144955435641364570282125099534383182237704864586431751036537879676959300661236269037824674792412667407068755447519965908211458109244425923729483/16497876185452117976032033644577146374988404925022905793402842415393979007624959927561532323715811377084003065760673384864593040085633258821468456595377974753704620*y^3 - 18907410208714691479072450997171696742569082374669391865186962933933664451436573857745279745397468438015401392483067352851404539293369111405754819216307529126484789637/16497876185452117976032033644577146374988404925022905793402842415393979007624959927561532323715811377084003065760673384864593040085633258821468456595377974753704620*y^2 - 605957294155724043275369959238179079309058255104377035362469972878885878189081303217917058891738020688940694464967800102572522356546468174630757998691998769780188831/4124469046363029494008008411144286593747101231255726448350710603848494751906239981890383080928952844271000766440168346216148260021408314705367114148844493688426155*y + 486726135434964204935106538464237090600961239327425958919860564902253149746747012115926309049004871934283766042329132734114211028207139488122348414503640459939716691/4124469046363029494008008411144286593747101231255726448350710603848494751906239981890383080928952844271000766440168346216148260021408314705367114148844493688426155 16655279340353823277077941637156868636131363243703097586392566270847668692123005344416153628541234983249830705578137147041109081400123335681593729992425308373457/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^38 - 96821385172103405139165989065602474259079651944373213747471072763851088231360189896913194415210924713389800013980910073558883553698153170983327007278656226603267/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^37 + 15623884905870484346860107227852305032477171832052854200370277820582825110087773108855799266928113839229401482978636398072676914700871840541906818999635822111089/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^36 + 6459806142431265141486393544253731666735318468635512753341753236598265711239464900874573965280296653418045706469600867334892069958399244181191760545045153176724187/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^35 - 29787347265948458488837599013897908695885050493418647646233131921420437740795212126781021372846660900957763352066009316445537920272494306118373718327303830229967653/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^34 + 121155456091475793617897457032965507950377847922009994153141799968128757295740722276337249805550575387230151407852360009196356424867122544381576894549336270851477/48389586067235356807932211778730421922517039671778513189435465422557082326991188758049682008035330435069190485826752042539232200282050293711832470889384769945008603136*y^33 + 162615480902891914412726054687617606217083301603664258214742653378617381920278121040075463864941417221935942001205171834496326978228722628232715368324143381170910069/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^32 - 1019329461862039870792427044131397310472988480438761223358934676906541543692785341504413492130526919095877327273326719142599007788151343754270429504116719590806351851/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^31 + 1185701818243552696344575411812698876410205475733536509225041638058757095641219690426815490324962766603010776085037085544285153465138804536013976379280483710002770313/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^30 + 16283499889190783693586832897116083129887315668219665373409370315895849028965333827680380125714405941028966142498583574108803817839815895934482432770252796149810761667/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^29 - 6824927305970561904431341890944054066737919018026998357136314727435875167560000028156251258126839938974965946747090282344133630887557948103800003453094031168003752225/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^28 - 11384970123594343691529683181886325978637985874332693850909325364114553501690249600616158272178799588002680512193922047579155419548875603280804008656560030160897883153/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^27 + 356917524033723442108092472404712357837256382509592781279918544946730960851394239126658456980020160386885505464889991121898682943076262470875648249559783263598972714893/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^26 - 169101530471564214666575480551920426105680129613313009601642278237174018573463147879650890212758723964915856283074728204491883810924074034196990343744222619526174042689/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^25 - 1260749672245664469927202738287014774282872479367053209641139485062729203120509768010952504702862544231595822491924005043154768749044024392699996553024691419521135390485/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^24 + 1645339384299427241472388772681692281108902123236555861786472431252845115876565524655097455862438925585613710290799940149332847303381293099363250316904479847251526746011/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^23 + 821114883130890799989926979190666293755243656913602140662692781392626720011218619135419600422535086058111227479226218821002455718065483566960108500220140664887673197089/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^22 - 3474519856281125341504261609433021324009965693808618618982864526433525850141574596804568694682276008936716486054354178266972852346977164618123404507904289593767760011349/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^21 - 2131524258115474076618536989055965389682411565013518788147588489350757300717181382350185932887692432638929288014955626123966244631371898603621515553736380657569700472773/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^20 + 70615569495083040643348635068199714807026135152940974385528190101173788992388820173989297892301659495467414447128387402950948276485449001987387753787633929288973723171/4914567334953590925805615258777308476505636841665005245802039456978453673835042608239420828941088247311714658716779504320390770341145732955107985324703140697539936256*y^19 + 976761617355134520601431605292225740964871451788518848212714077906057874942496513716496617185978523457285902361870508069774888655170195683513781069234306904895982776665/39316538679628727406444922070218467812045094733320041966416315655827629390680340865915366631528705978493717269734236034563126162729165863640863882597625125580319490048*y^18 - 49599642476029308383939482918048266591261209313158544778751918141035245318395173969076388035426690804385050228953550460724454215137098129384924063456750700785390887945/1512174564601104900247881618085325685078657489743078537169858294454908822718474648689052562751104076095912202682086001329351006258814071678494764715293274060781518848*y^17 - 1297371987735981373789432701223659082049869920626470840537251468535707830269379026329517303400646898849426084687142832472075413828416700525392685676748027991049706865407/19658269339814363703222461035109233906022547366660020983208157827913814695340170432957683315764352989246858634867118017281563081364582931820431941298812562790159745024*y^16 + 842141446324987533244000580250160781541119168200608711926498248372025406426744624892748806474817763255904462556860026470763456181501000289633851509694727519510540489941/9829134669907181851611230517554616953011273683330010491604078913956907347670085216478841657882176494623429317433559008640781540682291465910215970649406281395079872512*y^15 + 612684782045450372035614042324708919471310631105964046977362537737265524394866118979862100083785073844054896246413077502581342581037340524004474549207386510345950673443/4914567334953590925805615258777308476505636841665005245802039456978453673835042608239420828941088247311714658716779504320390770341145732955107985324703140697539936256*y^14 - 59700335965735282487852383327921076709997241732510268640969655296562662317155276612334478063752394370826008451608069875966658471607887823559619198052165077604047452983/307160458434599432862850953673581779781602302604062827862627466061153354614690163014963801808818015456982166169798719020024423146321608309694249082793946293596246016*y^13 - 104294180145762177826897927058919976460461090318556086505470193510349960411721508544667311042637275711717724714555864083661269911345320604430087118768853916664997088167/614320916869198865725701907347163559563204605208125655725254932122306709229380326029927603617636030913964332339597438040048846292643216619388498165587892587192492032*y^12 + 42718595828862615791282917758861799893560062586975872229729050793517392235995145351492733519148473552644675159936421252898971998740113806598206353547370986438650841099/153580229217299716431425476836790889890801151302031413931313733030576677307345081507481900904409007728491083084899359510012211573160804154847124541396973146798123008*y^11 + 55903973721126730512639813415335556361442217312673640331511483062369106963407134067472935891887177422817142826063626772407487449287536597991234518573495043331473024525/307160458434599432862850953673581779781602302604062827862627466061153354614690163014963801808818015456982166169798719020024423146321608309694249082793946293596246016*y^10 - 31758392047365975238275708866168485999805457382815240789022197336574019259509783683665444863539423982352884102865291189019151784799098651246418961820299134028382605311/153580229217299716431425476836790889890801151302031413931313733030576677307345081507481900904409007728491083084899359510012211573160804154847124541396973146798123008*y^9 - 11682650823656585137092683109058370440004325671170524894960638446012197994020816090842935648170809308411650242996164022603087033339909491870206593306925604276738867579/76790114608649858215712738418395444945400575651015706965656866515288338653672540753740950452204503864245541542449679755006105786580402077423562270698486573399061504*y^8 + 481779610014609910255148612988136836139859066612377780415180132324300483073409500115818851842818530858556904257406283607345706518883064737117770674917572116181718899/9598764326081232276964092302299430618175071956376963370707108314411042331709067594217618806525562983030692692806209969375763223322550259677945283837310821674882688*y^7 + 1496754986178483129282309150622067813933427064198898816043731192874764722370713033826806306859638493727601308280391515890326123457456118514789555348983386144890087119/19197528652162464553928184604598861236350143912753926741414216628822084663418135188435237613051125966061385385612419938751526446645100519355890567674621643349765376*y^6 + 76668495128853471763490577745131226403726237823852499964582947428000483867663702945041721011324078785750350028504464781913177566138434099754918645081103951739533611/4799382163040616138482046151149715309087535978188481685353554157205521165854533797108809403262781491515346346403104984687881611661275129838972641918655410837441344*y^5 - 74562184302215494374346642854970834133779137159694448402576061050580525676492853458201931799293478469059457347593026548405219394382066854631032290284419628260507789/4799382163040616138482046151149715309087535978188481685353554157205521165854533797108809403262781491515346346403104984687881611661275129838972641918655410837441344*y^4 - 4267261569891119809763840963668552754768005530182087415002492713426098089507085692098218271462264182193983601676170972890062158834465253150232608029538985261074027/599922770380077017310255768893714413635941997273560210669194269650690145731816724638601175407847686439418293300388123085985201457659391229871580239831926354680168*y^3 - 11748166325799872718815424958206771329632667364324942252780520906698571469129408564998602820802459596324459359757095305478608464462205286227530483896096378314891/149980692595019254327563942223428603408985499318390052667298567412672536432954181159650293851961921609854573325097030771496300364414847807467895059957981588670042*y^2 + 384332073851909040327921164571201958127753243950260580922622065822785388592600974087701895501312867461393015874674715021264321788888273000782037384537280641422927/299961385190038508655127884446857206817970998636780105334597134825345072865908362319300587703923843219709146650194061542992600728829695614935790119915963177340084*y + 43046271194329659721122304827418458878366729542333972446452488351035403306472627582825605930913009191441269555813258139962062358367417238516130753589396166000966/74990346297509627163781971111714301704492749659195026333649283706336268216477090579825146925980960804927286662548515385748150182207423903733947529978990794335021 3033706089403833768298924363657703610009753008921366919654384459527535246440927628883090783834368834217456177887112661763222719667236299332404210055335004222071981/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^38 - 36092157144051026641552505186726696447735596384306391424283776175175863976265461396483806211893674815114503309786559899641726349561401955280069912595039007581989509/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^37 + 1345851086895960114059695501964928632558501001704024930352208667942348619236163153309157158874621155166010133227151825239245249440699585710233574484347842233451231/2162409627379580007354470713862015729662480210332602308152897361070519616487418747625345164734078828817154449835382981900971938950104122500247513542869381906917571952640*y^36 + 232806205410979148035968636480216545853984691913002137132628296882255712613622386715254076548968264464131736611785952434408593636703480673146045001404829438652889143/6919710807614656023534306284358450334919936673064327386089271555425662772759739992401104527149052252214894239473225542083110204640333192000792043337182022102136230248448*y^35 - 2856078330127125745142871878934753894515038088763743208167388108221963210868186602492263523226657038828912033887324094326378846308238421288677052980509931608007364591/17299277019036640058835765710896125837299841682660818465223178888564156931899349981002761317872630630537235598683063855207775511600832980001980108342955055255340575621120*y^34 + 305708410698125823464902124051110601742265377061735764070114161890553109291442880772073241419998662811406505171788195855291697011348703843480243745272927946008580757/2661427233697944624436271647830173205738437181947818225418950598240639527984515381692732510441943173928805476720471362339657771015512766154150785898916162346975473172480*y^33 + 14156238344717502763061491036840392314291424604090821670408847728296280764463204914854373243530215235917493707208160926863913496786481179360417723165890049572164458237/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^32 - 5971108150960181333000424028728478133641253721375913475833467463346686468807624705316100174892162966886850875490717920168001110184548470158507199376032736197761348319/540602406844895001838617678465503932415620052583150577038224340267629904121854686906336291183519707204288612458845745475242984737526030625061878385717345476729392988160*y^31 + 323348643746717339790255704174463745341298397892174192521489368877352088880761761386506980308703122235993602559339068750323032020647648049700484646381083768533493202003/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^30 + 698166555553454843866987118762132041790453250039851720366445146649866238484024980591038487633662752442460362287658072655702309988584676884353662845472829364688420583709/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^29 - 10390820834223182243188285212210398298274795137276285143934410095589539056133603071873159386500844171861232991735830299271557462431976943727905433971288867546972063613187/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^28 - 38095485953704161710980078135387924209758274252834686925810345856396714156338425240607721981905549359684003127448096184881713615295665234034146581318047696176413820523/1081204813689790003677235356931007864831240105166301154076448680535259808243709373812672582367039414408577224917691490950485969475052061250123756771434690953458785976320*y^27 + 62254038044863177818373734896282271532498114592348728921125506120494445409391856463939145640179345728410542318115391788437602795504795919655157573281454407404809150006347/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^26 - 26616167236004069343300610253066951600095777045872976392013544761515411191634652430254348973572980752249294260944476485430775145363548845277636765729700019714208433480791/6919710807614656023534306284358450334919936673064327386089271555425662772759739992401104527149052252214894239473225542083110204640333192000792043337182022102136230248448*y^25 - 185923771176273693276460486268785157003665193708938978043309194675515563972979912404865435868988849970797782833344668916222658463434937117477332198191707136603684400592963/34598554038073280117671531421792251674599683365321636930446357777128313863798699962005522635745261261074471197366127710415551023201665960003960216685910110510681151242240*y^24 + 21713327815754394512538060394443046996234217154654168016835926421002839791131958160183740535211073262976705697439319910938701659395553741675834399621402488448662539204661/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^23 + 472015577598140037292199480035853455714147212188048804911028794404543364185192189917034538273884052413766879797780505214026217383959273212232182948328428548841979724282781/17299277019036640058835765710896125837299841682660818465223178888564156931899349981002761317872630630537235598683063855207775511600832980001980108342955055255340575621120*y^22 - 1265291233245654531459059703303255021529842669331680157147701401572900256672935742592530372954126426736811868011375184300157579428407551032416696259212317444185871908428829/8649638509518320029417882855448062918649920841330409232611589444282078465949674990501380658936315315268617799341531927603887755800416490000990054171477527627670287810560*y^21 - 685483402646446969151937706441768876863886747542460277388016719309669487304767817714652402492783608619552853062291825410695111465601831670838666619887137090671126190125761/4324819254759160014708941427724031459324960420665204616305794722141039232974837495250690329468157657634308899670765963801943877900208245000495027085738763813835143905280*y^20 + 837012371829119540768174602211892552033050754632127270126103667415772067003064336783335302156096985925717769227927117592984262191521854809472051705369834447544123800784417/2162409627379580007354470713862015729662480210332602308152897361070519616487418747625345164734078828817154449835382981900971938950104122500247513542869381906917571952640*y^19 + 331604262532304549438416808612782914535543260057710934768999525329756831608717803597540865429374741980017861268558127101023043989575917956967188810487662347625096287222599/540602406844895001838617678465503932415620052583150577038224340267629904121854686906336291183519707204288612458845745475242984737526030625061878385717345476729392988160*y^18 - 37127752136953556623298904082538354125618272090341814915136399329505226796722570878223288757769254721443412578326227761802140842990566133806905995254615205515761299127351/41584800526530384756816744497346456339663080967934659772171103097509992624758052838948945475655362092637585573757365036557152672117386971158606029670565036671491768320*y^17 - 437159945143871345732206255550341691028440320752255143551803813972241266168886744458521003190915989315380713735425022793226343656882242300623543150187973604534936890303781/270301203422447500919308839232751966207810026291575288519112170133814952060927343453168145591759853602144306229422872737621492368763015312530939192858672738364696494080*y^16 + 153652884241370293524700921981220991429621525511506259295292815529835666863123253147805199650937513100362703126212722762914128309710471550845116917147167607704883368782889/67575300855611875229827209808187991551952506572893822129778042533453738015231835863292036397939963400536076557355718184405373092190753828132734798214668184591174123520*y^15 + 4951063875842610743914021776090080283693967043880064139782577864941754621470317762790893733612235749030891983363831698092733144374699593103310790496935141558047259713081/1689382521390296880745680245204699788798812664322345553244451063336343450380795896582300909948499085013401913933892954610134327304768845703318369955366704614779353088*y^14 - 16487764426303712871611443485022444293493401897163042523456671563405212369502402400344116282162831474219801156058494766728163041255579443861375745620949896288905954078095/3378765042780593761491360490409399577597625328644691106488902126672686900761591793164601819896998170026803827867785909220268654609537691406636739910733409229558706176*y^13 - 4257719739298026975399270382822663582694008843454608176927857322418778628228304775334133883932789622359870184825529062294075168158373340198251974010978341904943258791031/1055864075868935550466050153252937367999257915201465970777781914585214656487997435363938068717811928133376196208683096631333954565480528564573981222104190384237095680*y^12 + 56089123491396473602793881561660111977842778165931175164038053092074979356560327569784037670124899967766060556590327422214466616677691149138346700905982330594654220977171/8446912606951484403728401226023498943994063321611727766222255316681717251903979482911504549742495425067009569669464773050671636523844228516591849776833523073896765440*y^11 + 4190778593509735160349715893544627407554841581790186757228457266410470562043642746607799083868124284130097683113890236656790461525836836242708004844997726187114849168981/844691260695148440372840122602349894399406332161172776622225531668171725190397948291150454974249542506700956966946477305067163652384422851659184977683352307389676544*y^10 - 2471971652570790999758065855247534684168930060772094284857502139262307135917381634000676448846855799449878898689802459024421340786786216657385616078841766848281835343389/527932037934467775233025076626468683999628957600732985388890957292607328243998717681969034358905964066688098104341548315666977282740264282286990611052095192118547840*y^9 - 2518569131628165218948037521089298871082762217042238267822923343095631994418636029634222369762709213132632314140872324538853453862272660391754646672791721051528260274389/527932037934467775233025076626468683999628957600732985388890957292607328243998717681969034358905964066688098104341548315666977282740264282286990611052095192118547840*y^8 + 40324657461674297037275664788485723636214188055966224613160736246835388548313066416958109501692874202113181522455157403061026974521219495049620357059926655145938132557/52793203793446777523302507662646868399962895760073298538889095729260732824399871768196903435890596406668809810434154831566697728274026428228699061105209519211854784*y^7 + 321777949515192687575942312616641729521318528337187740537312841998116677999757122245634435742625415246564325378846807642829517611764147644663427810689424986812150971047/131983009483616943808256269156617170999907239400183246347222739323151832060999679420492258589726491016672024526085387078916744320685066070571747652763023798029636960*y^6 + 10556685813201717889651542783076323096937654424677780026631973835243708132544817899503160077998429972984077828386188471755005307197735884901636829999292673989853363109/13198300948361694380825626915661717099990723940018324634722273932315183206099967942049225858972649101667202452608538707891674432068506607057174765276302379802963696*y^5 - 11469288252265358397209872661844507956744755586400350619017543361624415118819140384743759169516671299767635134093060247512239879567123350812485328023596456353265089687/32995752370904235952064067289154292749976809850045811586805684830787958015249919855123064647431622754168006131521346769729186080171266517642936913190755949507409240*y^4 - 10265998701427432090567720650275280440840113367942694679063301713409690237792690675751676296794986220916659998045472591828766409134694537737636464793982960684574125201/32995752370904235952064067289154292749976809850045811586805684830787958015249919855123064647431622754168006131521346769729186080171266517642936913190755949507409240*y^3 - 604274434892739179658860789041439791609774647265487532340725759789211350897791726285345785991637889188094883449905586403163686432799235969720619918844765666945435737/16497876185452117976032033644577146374988404925022905793402842415393979007624959927561532323715811377084003065760673384864593040085633258821468456595377974753704620*y^2 + 230832495792465987501135087616437124958067121740718940675205390480936782554054598526229031281189296782221303213705827692626757823953595705750700137645660343359021423/8248938092726058988016016822288573187494202462511452896701421207696989503812479963780766161857905688542001532880336692432296520042816629410734228297688987376852310*y + 33231670734159550207392940955629150699521819670184119271212354999133238284482841552039368864538876368698981884397660158316754495355799347810890045924723068863903361/4124469046363029494008008411144286593747101231255726448350710603848494751906239981890383080928952844271000766440168346216148260021408314705367114148844493688426155 1264463847671694065353560129810904350090687251763029192707827633016910633883495219621160679739529507154016559800555453833888337384970935902418366431034382643662657/10065033901984954216049900049975927759883544251729930743402576807891873124014167261674333857671348730494391621051964424848160297658666461092061153944992032148561789452288*y^38 - 1828479884083187136243929303719847911349905893010471360320352316653638192554159325117959674964742686949073130384836358543808320745179277168619954347544655162931929/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^37 + 463470299744680928573842838123263061050447324205615269733090000553401079690915253996292443304457144040762753498282377248671241250753690428257022668432268156510661/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^36 + 492000817739993283995968098944056129824912737541012340493702867885456204610841002812988487963218125353830422294915792673657562066478500337875803670837345700716296483/10065033901984954216049900049975927759883544251729930743402576807891873124014167261674333857671348730494391621051964424848160297658666461092061153944992032148561789452288*y^35 - 2224201522260417382554083694494655022136124659119723107313961486952255921501870500393151941154621527015703402906511388479053477901176551457265681954041097702168080251/10065033901984954216049900049975927759883544251729930743402576807891873124014167261674333857671348730494391621051964424848160297658666461092061153944992032148561789452288*y^34 + 28925354654590954213242829752336628322938240854058664890034633306646733794853104708008713566428932829477010419888153474355076096877276964103827820182781720017890225/387116688537882854463457694229843375380136317374228105515483723380456658615929510064397456064282643480553523886614016340313857602256402349694659767115078159560068825088*y^33 + 12382883091343477993655847750465936222954104171509521864651683056140314715136290937280140023310501142303463591830555687253173472332079131910910916388207382570307470841/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^32 - 76034583525904656850690759940555987141129927136551628254794299713391427917001772694918607994186513056937854669353893826457799802169336529367583299946752519864520679253/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^31 + 76710466505956993116288690642434129912202422603686808472963171637590688968472286879368622110969311308725436375612315753815945838153901753981243610026789273509156492933/10065033901984954216049900049975927759883544251729930743402576807891873124014167261674333857671348730494391621051964424848160297658666461092061153944992032148561789452288*y^30 + 1249519786211550633862800720189966146308747325647635952037579498500447265583472715521072443008621207332996727375032961596908633839070493270875009440085929482838388842897/10065033901984954216049900049975927759883544251729930743402576807891873124014167261674333857671348730494391621051964424848160297658666461092061153944992032148561789452288*y^29 - 1994782957682296965690898816400319240530010491413880979681237305215328824233181185120307391908074823951630260430310272515053158881168072425275785120816571906321819978907/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^28 - 1102998172951316691817009272246831168554931967611427960789901177528117818121206595290398335646277043703467029836649876984300932035070280416407844207588227642429134890237/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^27 + 26909367331044078795494052543672555535282084188120758636703584072849929965715391328211329821516226421620975802163137739396579766419274299977058886527824933143131279056641/10065033901984954216049900049975927759883544251729930743402576807891873124014167261674333857671348730494391621051964424848160297658666461092061153944992032148561789452288*y^26 - 23532868388526379643396084028212630296251639830497383695787077580541355180126519704434835393766789517750198520138094873509657662965636322185914851224941361695131311671119/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^25 - 101874725705559242746308999177887747547587321815811984939323546758952130943916163395890790823835877994203511620457216852998425571564664799849153452901952576222192093157925/10065033901984954216049900049975927759883544251729930743402576807891873124014167261674333857671348730494391621051964424848160297658666461092061153944992032148561789452288*y^24 + 243719633777931309617924004124565798636226187089697981926657991167685128162967789122741034008936239750270060401077184988604178029330662611531544931066996281167687999092019/5032516950992477108024950024987963879941772125864965371701288403945936562007083630837166928835674365247195810525982212424080148829333230546030576972496016074280894726144*y^23 + 71561726688529505063198022515955459926243485563188744600134744040985649644277171218248529318143766282980892622903007677862496674822997435123892113832859066208431462097609/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^22 - 262932174866864318113445941593920665912622473024643330643782686192275415548878755425318152256588798761647704237119789461369290136609938948583976798785923803840490792527517/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^21 - 190926626915901326336545646935108610736731334710924281173386109318370809899951367162192216970464505668353277624015923135276842241373157236971315551050793861372817132265961/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^20 + 166251002143128298075473369745070917298042086131797019888006335027546092749861370532185974824663526709736580649398695579951253973080784657180750972542775989653926924526255/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^19 + 173811662393850896471867801349048959671515061855899403255795105475745237347237449935214627182850045402733208919514255984154136776607089511162866793185841043335913481320155/157266154718514909625779688280873871248180378933280167865665262623310517562721363463661466526114823913974869078936944138252504650916663454563455530390500502321277960192*y^18 - 3378351988558400834763898615651919707683023999889587595503460386430733852107283166813658753420748356331846425943836959733808897220752594632017260135783278060731646479993/3024349129202209800495763236170651370157314979486157074339716588909817645436949297378105125502208152191824405364172002658702012517628143356989529430586548121563037696*y^17 - 114314162016575268508096676689724639159421487089010248533611350558607797161825797984569484119660304232063573067028195874314402467522883253183299736823407884591184437533111/39316538679628727406444922070218467812045094733320041966416315655827629390680340865915366631528705978493717269734236034563126162729165863640863882597625125580319490048*y^16 + 55151183628741369989646484503715078449805903218452705648770703851519001333191998705907780536657513402152674549826604457619054460376953131576458557098387105154426753281559/19658269339814363703222461035109233906022547366660020983208157827913814695340170432957683315764352989246858634867118017281563081364582931820431941298812562790159745024*y^15 + 7008689007961700036916755700982775128045553006506945164639929641733186680574965389720192759110552162922418698750320560738013825140679982315205901495437476936159647259715/1228641833738397731451403814694327119126409210416251311450509864244613418458760652059855207235272061827928664679194876080097692585286433238776996331175785174384984064*y^14 - 31586095947440836831725832449468880310372114091162889154416875517334394707434866008434644408785034786034700689100398686883173059020374048174013864000112660937672214465095/4914567334953590925805615258777308476505636841665005245802039456978453673835042608239420828941088247311714658716779504320390770341145732955107985324703140697539936256*y^13 - 10770177657936908937803732883223826685672352325527997219850299255116121930255520649349013607658382304103350114399034198166749022253030682162703764748924648574791259989525/1228641833738397731451403814694327119126409210416251311450509864244613418458760652059855207235272061827928664679194876080097692585286433238776996331175785174384984064*y^12 + 5705186514738604656462628814007881270738335625944138125112119037174455270844931578362887777617563288796495730717338507802612956838170243894765803020716486663238386154007/614320916869198865725701907347163559563204605208125655725254932122306709229380326029927603617636030913964332339597438040048846292643216619388498165587892587192492032*y^11 + 6739648020157657482901156799425611308513917665194309352434645622123630342629666717768845750642296908573922917779167553479393587014770021735305359939940589234994246939075/614320916869198865725701907347163559563204605208125655725254932122306709229380326029927603617636030913964332339597438040048846292643216619388498165587892587192492032*y^10 - 1979572516340773295954766989296951157934179277720444933558580347921552089170431838812112398353486039709830689140009021497766726812196236248112796573833239250111837688339/307160458434599432862850953673581779781602302604062827862627466061153354614690163014963801808818015456982166169798719020024423146321608309694249082793946293596246016*y^9 - 752298011412554190716985388832963277668346260419357033082869498068935224772872689494559422341327967902918395107599522816690769004294618025207448388491124946181233356871/76790114608649858215712738418395444945400575651015706965656866515288338653672540753740950452204503864245541542449679755006105786580402077423562270698486573399061504*y^8 + 14679742971991503781420457633595020129565152547143247440888782703528460212315050532902407648872979886224581418787030956972770946566680422636912548179551951572823921721/76790114608649858215712738418395444945400575651015706965656866515288338653672540753740950452204503864245541542449679755006105786580402077423562270698486573399061504*y^7 + 176143919373902113689839110926396028464330196205518730656764043741244531304637282714064626170315655621531715446179651876102696074595322954864355544665268359174737357135/38395057304324929107856369209197722472700287825507853482828433257644169326836270376870475226102251932122770771224839877503052893290201038711781135349243286699530752*y^6 + 37688232639635822445932958295798575654667004302671044027271125552410120746862836357783529310072733496681631513699764670270338712019154357134953041739038350349539798205/19197528652162464553928184604598861236350143912753926741414216628822084663418135188435237613051125966061385385612419938751526446645100519355890567674621643349765376*y^5 - 5056002783068753301756908603022612512872392548682659797306302004137129906868505692089545750611025682274695259462858110741568489326606202923862645781658135981808562513/9598764326081232276964092302299430618175071956376963370707108314411042331709067594217618806525562983030692692806209969375763223322550259677945283837310821674882688*y^4 - 785968305100185217429094642129082602094572555982773814049618190646975696914966741558078799166935114148054407327000050012605468359361261958991201166586578038282277345/1199845540760154034620511537787428827271883994547120421338388539301380291463633449277202350815695372878836586600776246171970402915318782459743160479663852709360336*y^3 - 271144595155617425635441747180804282528234325063117319214721659146776872517134112388069715905846427249413422752593364876490345833896898960217982412149021606601314619/2399691081520308069241023075574857654543767989094240842676777078602760582927266898554404701631390745757673173201552492343940805830637564919486320959327705418720672*y^2 + 16860635503058322363448756122090150440065217969344159776534303607909876236403003693482765562271686027313852078998962706468270365924021864986459903526257984243973215/299961385190038508655127884446857206817970998636780105334597134825345072865908362319300587703923843219709146650194061542992600728829695614935790119915963177340084*y + 12148388766087394919953094464140894959747907042144494181825004157896528061168865910687088520618316939018997849697800764069210896853423578638546793418693533414172309/599922770380077017310255768893714413635941997273560210669194269650690145731816724638601175407847686439418293300388123085985201457659391229871580239831926354680168 # A Gluing Matrix {{1,-2,-2,0,0,0,-2,0},{-2,2,2,0,0,0,2,0},{-2,2,4,0,0,0,4,0},{0,0,0,-1,0,-1,1,1},{0,0,0,0,-1,-1,1,1},{0,0,0,-1,-1,-1,1,1},{-2,2,4,1,1,1,3,-2},{0,0,0,1,1,1,-2,0}} # B Gluing Matrix {{1,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0},{0,0,1,0,0,0,0,0},{0,0,0,1,0,0,0,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,1}} # nu Gluing Vector {-1, 2, 4, 1, 1, 1, 3, 0} # f Combinatorial flattening {1, 1, 5, 0, 0, -10, -5, -4} # f' Combinatorial flattening {0, 2, 4, 0, 0, 0, 0, 0} # 1 Loop Invariant 4423488588449340513069180092169891689187813078811146162630301358486107545210690154380023953801292001198048185315829765913778915848543936608816486838801541722211425/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^38 - 11716229260990039944949409290069781119392928993049408036938129514812589709385045017788496132261776126186529239145249232548941898811498814043960910816677582917616891/629064618874059638503118753123495484992721515733120671462661050493242070250885453854645866104459295655899476315747776553010018603666653818253822121562002009285111840768*y^37 - 5098582321016414735129020961955690541119362314702163238066144838206159554623854226085954231948437565736889268065401642110934250147654694874379334861227016587358201/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^36 + 1783248336061793226653470024285097999670417385421311793775919984770971544618171505771626651027457652814069725983436743665095131955476941436270128029728078941785276419/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^35 - 6165869240419555413455635591624005668958908733449280803304080572202701684673667418670064138354727881053473149924883293218154682340313306562239159213809712540085519591/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^34 - 247095872016731816821300742864589617881830587691830597683777928337373594308904549246806370471333606699363740798877863294726683705720522854479748826308468466491023049/96779172134470713615864423557460843845034079343557026378870930845114164653982377516099364016070660870138380971653504085078464400564100587423664941778769539890017206272*y^33 + 48807024394176568656590664833766541101522204728880820171687750001348517057559755010434669662634031271164268608352196438610084051807390506366961124680926973354529536589/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^32 - 229058217825214314119905265453703429584515377795407671217321605760432352465591616810429020144620103863319530952788453876312630432241572397672882037388298184489621332905/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^31 - 317513375907149424602366138003737961130690384638724806849086977252585300775809208563070090394144705102620726587936663876166954981263745743186568453488062777770835506483/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^30 + 5173339207779153215872770757179536726553733895203196402063505255515604140069985663950839239193964049830809970513809757754349922775495867953294021130331957932718926395613/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^29 - 5235528053146783936528834017074298994866461680229547926677968733497615658299773502081343396302567979215988550318181567952945091863413427994188015298554649865380785921237/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^28 - 12261912583496629596450830088806424064548953657918789121889407669714760523092296284573893337750454791424656346239264506833855988142213286895752237104435869293482101895913/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^27 + 102252736735975599020656274209616863149959325389392976387195303543404208648279221026609663601128827662447005685669081086223491259786662189331725433241084661152019422126761/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^26 - 40531551803634853883359678885830593206944218790030560939522946138048160902609459597388119166168757178318861026706418317440039523273419365434437288937971191167611303250049/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^25 - 594704239826301431924079351073495847240256330123463821331271440542206221167865002985084919628215052420417797343457559398847224509344001136402728396230553996161397954658269/2516258475496238554012475012493981939970886062932482685850644201972968281003541815418583464417837182623597905262991106212040074414666615273015288486248008037140447363072*y^24 + 789753833162493791543380675998904824333638472409362927727493547780645431755466290790553267907404927622627939116388951227958458048580801153800992630289846947680730852140365/1258129237748119277006237506246990969985443031466241342925322100986484140501770907709291732208918591311798952631495553106020037207333307636507644243124004018570223681536*y^23 + 117878273753296050424454603964624133503775621323785118600964709673834895838480423180145556340481948121014448026847579454797606051239724640664287110356967391798332760662987/78633077359257454812889844140436935624090189466640083932832631311655258781360681731830733263057411956987434539468472069126252325458331727281727765195250251160638980096*y^22 - 882413985947733363392418472562210206788031670320842776384757298242557348285801568259778041142261174980672562364864151939496852930472504775541420128306325044869758338099825/314532309437029819251559376561747742496360757866560335731330525246621035125442726927322933052229647827949738157873888276505009301833326909126911060781001004642555920384*y^21 - 1128501444863772615633655094311783009785733235231206630660431853051496264722413752303840300334984647393435556439033099666344825225757729347394045226016767851051611234012033/157266154718514909625779688280873871248180378933280167865665262623310517562721363463661466526114823913974869078936944138252504650916663454563455530390500502321277960192*y^20 + 477509872677430290766448575056695975360563437777093409028672249224801987316384580506160160058232066912730214731899920316971049425008176179253204146015237553598468477954157/78633077359257454812889844140436935624090189466640083932832631311655258781360681731830733263057411956987434539468472069126252325458331727281727765195250251160638980096*y^19 + 940325799251847258040228458331146724175044049165818051612448545345787573803002423265733203906961132860264965705221134489570274869263522826532806378002288917148301085919591/39316538679628727406444922070218467812045094733320041966416315655827629390680340865915366631528705978493717269734236034563126162729165863640863882597625125580319490048*y^18 - 6627677401415595051863514906640639326261622789650929561869849167927178853135876850412399968625692097108371979813276943800773485182061737751305646986350541247636642359949/756087282300552450123940809042662842539328744871539268584929147227454411359237324344526281375552038047956101341043000664675503129407035839247382357646637030390759424*y^17 - 616578892097162834716338878340594896809652017405169945503217983562126948056250050739664460967843151352485856431926272248922215022371180465305457747915395238550696048680237/9829134669907181851611230517554616953011273683330010491604078913956907347670085216478841657882176494623429317433559008640781540682291465910215970649406281395079872512*y^16 + 101488589206487910431211824800542187847156293837304447923652967242359420134440215963116803174901064248014784928746968627755669254953933363405859153289162154829862232274729/4914567334953590925805615258777308476505636841665005245802039456978453673835042608239420828941088247311714658716779504320390770341145732955107985324703140697539936256*y^15 + 83946138738605500362636016347415328918249546678223840760123951440879129202619997959422784554694266365768333025879268708226744962191159768923514530967665401290780655244153/614320916869198865725701907347163559563204605208125655725254932122306709229380326029927603617636030913964332339597438040048846292643216619388498165587892587192492032*y^14 - 80469228240247400590436141022472645610505709679525441614884351001869559549877261482815773344782811400427909773121836768137088513806889498588373196222187770329124169213119/1228641833738397731451403814694327119126409210416251311450509864244613418458760652059855207235272061827928664679194876080097692585286433238776996331175785174384984064*y^13 - 72380798726641194699514675042186884798580889350373378730566197006591334988301968549217308087583458610714959650796968523589016376126127695402107502830425425290690006708917/307160458434599432862850953673581779781602302604062827862627466061153354614690163014963801808818015456982166169798719020024423146321608309694249082793946293596246016*y^12 + 17846127654790897800626641640375219740573150313668233616837548675968425995091821611622529830951964755899876314682759151489983964049034710581882349004562115646790234661501/153580229217299716431425476836790889890801151302031413931313733030576677307345081507481900904409007728491083084899359510012211573160804154847124541396973146798123008*y^11 + 45939797657989887632455619380952456844610532887388962530820416065885013033743739860044546985223250465585489320877093038610327268093735004209984325394419954419715014785709/153580229217299716431425476836790889890801151302031413931313733030576677307345081507481900904409007728491083084899359510012211573160804154847124541396973146798123008*y^10 - 5948958306920310090872830607153089536416479068077104611108639499461727724348662692620791267508857104740972211463193375410102089753175043703195451246938304410684597254113/76790114608649858215712738418395444945400575651015706965656866515288338653672540753740950452204503864245541542449679755006105786580402077423562270698486573399061504*y^9 - 4811634900732129331321207575325616983813185210316307801797636639012409351970301224023230778559313310366145000532477948910854987103641347475924080091749895611733457075975/19197528652162464553928184604598861236350143912753926741414216628822084663418135188435237613051125966061385385612419938751526446645100519355890567674621643349765376*y^8 - 518822596912856179898077660135161813816093973032404388961608924788191435425201336913243144073946503069638738713027935058862684787315811184662581903860918283021139952603/19197528652162464553928184604598861236350143912753926741414216628822084663418135188435237613051125966061385385612419938751526446645100519355890567674621643349765376*y^7 + 1069567848728531398363551276149075926125178377282214769661630705420209348075546045014286072268271952152119889975368302229535961665956336254640614317048901665948396090519/9598764326081232276964092302299430618175071956376963370707108314411042331709067594217618806525562983030692692806209969375763223322550259677945283837310821674882688*y^6 + 266435107430679750951217996692947796881623790654866554272965873788900185719689660846847967794917868938951782292066221892401440510958651767428514814238533421395368045367/4799382163040616138482046151149715309087535978188481685353554157205521165854533797108809403262781491515346346403104984687881611661275129838972641918655410837441344*y^5 - 30564254630390725312530041044615146116876652993660856841019813951930423431872127027443891974125169657321054331903020097130487046472234468432396702555977179925151147365/2399691081520308069241023075574857654543767989094240842676777078602760582927266898554404701631390745757673173201552492343940805830637564919486320959327705418720672*y^4 - 11532120256966667827723913621813230900831247364974301349685442753937920137834035134802362235497130745986697817695772323122872355636888515142273245884968409004652632143/599922770380077017310255768893714413635941997273560210669194269650690145731816724638601175407847686439418293300388123085985201457659391229871580239831926354680168*y^3 - 2179623622231974511754194102355450793370299431905579717703029955120468958462703472147047479984350577584188616724013276397689719243724589066930387312486935419937826603/599922770380077017310255768893714413635941997273560210669194269650690145731816724638601175407847686439418293300388123085985201457659391229871580239831926354680168*y^2 + 299773772182231849140472289680707590863978399266155853061060203656192822856766075812241167310271397489234377848877373576579323604277076773923456118701137527602175039/149980692595019254327563942223428603408985499318390052667298567412672536432954181159650293851961921609854573325097030771496300364414847807467895059957981588670042*y + 112243714380307302910943317538726927111075913556773891690310943792897779333233490964458849617931089393206137964215153576122910708099316748797773521578786323585159069/149980692595019254327563942223428603408985499318390052667298567412672536432954181159650293851961921609854573325097030771496300364414847807467895059957981588670042 # 2 Loop Invariant 134198241417342569168522644493837328222097245900630602032483195692600232249405209195870389053165020536767231710927954201153019824802530412865741348017527491626712528893740668145930407351768680343206508721269001350850559198015809020211822240015108932967472267612916410264198963083354394550594229644849542804245305/49547289449473379095248984436004071091797724915981873835196699930108786231048219623490239573948883285457024458681962715373677418839739089115101890012787895217985589937923803380082886906123017025890443607026432813071427217384373395838054672252285205730320702931446278758403051968100063096992239487454119124224148464730112*y^38 - 1519883228252120520023163419689062006655159207660212616338069188505605418912769497237702387009618514715491498613992220624711778712323260024383271733674140720114402607519318492137064648634410592311036911820609338387486085420712172715097663766748241460395628265071605922451449319065209532282887308543313743099813005/49547289449473379095248984436004071091797724915981873835196699930108786231048219623490239573948883285457024458681962715373677418839739089115101890012787895217985589937923803380082886906123017025890443607026432813071427217384373395838054672252285205730320702931446278758403051968100063096992239487454119124224148464730112*y^37 + 6381974355785303387014341184636870519708451582853573265039938442382933325684258496372495347710928195561325196885129032951264839864258332575184011409459508957364070170541939287738868713706886006123815012500541825065279189063446811675588175275795798483300100103388177077391963932764926603324353282779950117957703/12386822362368344773812246109001017772949431228995468458799174982527196557762054905872559893487220821364256114670490678843419354709934772278775472503196973804496397484480950845020721726530754256472610901756608203267856804346093348959513668063071301432580175732861569689600762992025015774248059871863529781056037116182528*y^36 + 52242011823647188020833845951883986301023060751127798996468258929754259678604516383211993380803053782668482597323026580151652556100275787377555757436395625564241151179547363094637535160495270147580184305543715832168365034104459221281948155983179231123725383002740652417856912672084339491618056148105836708025034111/49547289449473379095248984436004071091797724915981873835196699930108786231048219623490239573948883285457024458681962715373677418839739089115101890012787895217985589937923803380082886906123017025890443607026432813071427217384373395838054672252285205730320702931446278758403051968100063096992239487454119124224148464730112*y^35 - 111855932526065630127905158969244172312870703117437730978145371392833644212973575001488639384117665871902934316057959108111248625491728665790320161871444880486993033249882589423536818107110638091603611169837638893489858254805718151639798329070149474837180559334197189427463292250780061920051975823100663693101962353/24773644724736689547624492218002035545898862457990936917598349965054393115524109811745119786974441642728512229340981357686838709419869544557550945006393947608992794968961901690041443453061508512945221803513216406535713608692186697919027336126142602865160351465723139379201525984050031548496119743727059562112074232365056*y^34 + 1987895163443025877117296505325797267839489436240733921223306091197225648990422291182306909353948708804755187524099141254923460908231395974958993672065763839612029501344267527733573550175433247667329979100479806211594322716864225016517502389388509887710737717742348140905237092917165139972639319757465754175575385/3811329957651798391942229572000313160907517301229374910399746148469906633157555355653095351842221791189001881437074055028744416833826083778084760770214453478306583841378754106160222069701770540453111046694340985620879016721874876602927282480945015825409284840880482981415619382161543315153249191342624548017242189594624*y^33 + 165283529036060819216912324297984266887635782319625652047072917516445282326435595700447882991917227143375339925686488048389605715656179991671857556350432425956099595158731315656605083598795562221689588163914840967609802972326021521249467163625674985511506958775136004133988518579412874790023715717771950567528659189/3096705590592086193453061527250254443237357807248867114699793745631799139440513726468139973371805205341064028667622669710854838677483693069693868125799243451124099371120237711255180431632688564118152725439152050816964201086523337239878417015767825358145043933215392422400190748006253943562014967965882445264009279045632*y^32 - 40481933789910826331261410956747746141695648881286958255995290867913118045225602644873042606655879555509804512428849554478319574802809145428820634354627273167207829681248617977066139871260422417717376119111536603281840188353850109391758743364453439944498969092035202789763510701515198415587139072668968908894010163/129029399608003591393877563635427268468223241968702796445824739401324964143354738602839165557158550222544334527817611237952284944895153877903911171908301810463504140463343237968965851318028690171589696893298002117373508378605139051661600708990326056589376830550641350933341281166927247648417290331911768552667053293568*y^31 + 4394024603671146042092172731533542836062428972998226261877380861507702331728722977650547739472322829296969759634959118412264949935724489927905187460357665088722709142831440350633001550260594318017587734646098198539461334172176253543289547556482386828844466837127598869397362193812815664464343548995078298210562888479/49547289449473379095248984436004071091797724915981873835196699930108786231048219623490239573948883285457024458681962715373677418839739089115101890012787895217985589937923803380082886906123017025890443607026432813071427217384373395838054672252285205730320702931446278758403051968100063096992239487454119124224148464730112*y^30 + 2095527009777382883370369081425622243158665473835857602143602216223810235821803558524350920006851491744504843655360995956542167111296860205937901616794676221056723737930138486383057825560069624555690005501902110695610032372547367386621691844855105815802737785353148668443597672259706012713536853987079160736376934969/774176397648021548363265381812563610809339451812216778674948436407949784860128431617034993342951301335266007166905667427713709669370923267423467031449810862781024842780059427813795107908172141029538181359788012704241050271630834309969604253941956339536260983303848105600047687001563485890503741991470611316002319761408*y^29 - 394226162162308472286963905826597137159194001389777471220040495746883547874365391421193258294501524618936425577447995916911697186460199295136891847588815546163117710378262021496318675253567337304117832199263848235991065510864958601498438738239643286415090919185336923517944512846216544765971659889135757804588959412535/49547289449473379095248984436004071091797724915981873835196699930108786231048219623490239573948883285457024458681962715373677418839739089115101890012787895217985589937923803380082886906123017025890443607026432813071427217384373395838054672252285205730320702931446278758403051968100063096992239487454119124224148464730112*y^28 - 82019299630883233537613758190398302503367347614142303209401018224952554783932884002196372845179402979379717705199480509192569938010377072878250269301344137744388745407575093870916267733712931938968116415546154174127297437231016395496253890391536437935908190529983930346959745664227853562930610025239734063838072357329/12386822362368344773812246109001017772949431228995468458799174982527196557762054905872559893487220821364256114670490678843419354709934772278775472503196973804496397484480950845020721726530754256472610901756608203267856804346093348959513668063071301432580175732861569689600762992025015774248059871863529781056037116182528*y^27 + 2800104248048767588511027795887977762249301703963115621129291021528120689298282594584366704170322902475671933837498729460860535023738778265662820123921231172462400012955031194611130413326600347009456893957254108603581416392385819129569888766213261226607630261744434895858041049060804646237836226353132882213550565825087/49547289449473379095248984436004071091797724915981873835196699930108786231048219623490239573948883285457024458681962715373677418839739089115101890012787895217985589937923803380082886906123017025890443607026432813071427217384373395838054672252285205730320702931446278758403051968100063096992239487454119124224148464730112*y^26 - 1466763398525050101208803670904832370166222638059007755411347046416096950316725460037835923321754711712334407865211975649262311951511310817839041739250396701506948145883879944326331529388379156170652492731266638642176168605913502558338888730092528628795907543703908470804216630057812220225775615646162735405215154483985/16515763149824459698416328145334690363932574971993957945065566643369595410349406541163413191316294428485674819560654238457892472946579696371700630004262631739328529979307934460027628968707672341963481202342144271023809072461457798612684890750761735243440234310482092919467683989366687698997413162484706374741382821576704*y^25 - 11923232432910869021157006323434816038579129131902557759383227366313966018346390000587002215946041817499204830925390611689984287858201422532815211195363921982975882386748848352739234683266924432259923420654841494699881135973404307209596407804228097521488014076179175554126879447837813988180586410447381963846294656175651/49547289449473379095248984436004071091797724915981873835196699930108786231048219623490239573948883285457024458681962715373677418839739089115101890012787895217985589937923803380082886906123017025890443607026432813071427217384373395838054672252285205730320702931446278758403051968100063096992239487454119124224148464730112*y^24 + 16443349974248863607579249697093140809381267194025375704599993966864765871300078238615459270093686883911440706712309170679577190331289324770561324297602565591345148548575926395435197048270176130519895297475308022673160137372228390248014891524414980552133481223139903136394267631312144861564815235999532292669402514917601/16515763149824459698416328145334690363932574971993957945065566643369595410349406541163413191316294428485674819560654238457892472946579696371700630004262631739328529979307934460027628968707672341963481202342144271023809072461457798612684890750761735243440234310482092919467683989366687698997413162484706374741382821576704*y^23 + 35843514853003726534025810925766202408721204741664796441319330742877452985287093310689011756752753338689407249723311314244647044755494138372046056471429859906389099596854165231990745412021224194891233923067376577761464264723736075311942665440387853304994760907023564219495813624994042245293214124494046942025848496096363/24773644724736689547624492218002035545898862457990936917598349965054393115524109811745119786974441642728512229340981357686838709419869544557550945006393947608992794968961901690041443453061508512945221803513216406535713608692186697919027336126142602865160351465723139379201525984050031548496119743727059562112074232365056*y^22 - 17317115046812542394423283920264595531761380403334057469793373590382486115920716754013777637565777561173642596797370723812005201337409753214872740520049281740046372888549093066944378920770788784475351438711319598733478788542845129351835059561747953201608626786639921615954218861022373694195971550491234207644013599279531/4128940787456114924604082036333672590983143742998489486266391660842398852587351635290853297829073607121418704890163559614473118236644924092925157501065657934832132494826983615006907242176918085490870300585536067755952268115364449653171222687690433810860058577620523229866920997341671924749353290621176593685345705394176*y^21 - 22787551955780398555663950493763059158267988028791510185510096440334979531033944706137721036490167267885325435871004602531146130726705557469200896122219251760577940505106676503741096559996442333774529391000216182265908704649727103548645979930411566313312732114837775223688235878463665805628644934942430904444222832952121/3096705590592086193453061527250254443237357807248867114699793745631799139440513726468139973371805205341064028667622669710854838677483693069693868125799243451124099371120237711255180431632688564118152725439152050816964201086523337239878417015767825358145043933215392422400190748006253943562014967965882445264009279045632*y^20 + 5108176023071097498518339294760476099953888949125724469623219430325715183058918120020776990034782849181190018132167661405529887356913133397256916316873508029330521769480508775434641987609069452556451495725256772334945621392174654979615551441979934902285280655652257148532307233297843278087221917445237875876261400428213/516117598432014365575510254541709073872892967874811185783298957605299856573418954411356662228634200890177338111270444951809139779580615511615644687633207241854016561853372951875863405272114760686358787573192008469494033514420556206646402835961304226357507322202565403733365124667708990593669161327647074210668213174272*y^19 + 13181166868731273113890972932889494058084647527341405889547004559804838080216704689737421039343364670749583039630646177213322781690856298263528324331412216370718930050325314411170451999490406890548473373327418360664434173494579838499988030447741968761089301769245481760402573037355607968460720179614083663030497495786329/516117598432014365575510254541709073872892967874811185783298957605299856573418954411356662228634200890177338111270444951809139779580615511615644687633207241854016561853372951875863405272114760686358787573192008469494033514420556206646402835961304226357507322202565403733365124667708990593669161327647074210668213174272*y^18 - 381756205318333989924537312074444185517526909061357530549730815730684592200757807967237205826729297219716721846270102223917836127101084889166657945037821122374674158999140674882398453078947749427702628695650552153609650417812606410348908613318047029714904074666346920211818911612778882730308573098209406206951479134143/19850676862769783291365779020834964379726652610569660991665344523280763714362267477359871624178238495776051465818094036608043837676177519677524795678200278532846790840514344302917823279696721564859953368199692633442078212093098315640246262921588624090673358546252515528206350948758038099756506204909502854256469737472*y^17 - 8522667179595517875648180742237592418875938999745359968063336196039763166225980749223599727447348929869309178276809807515911139167533367302864870047305222524660334923147021069683945076340627753521725565149545908966490339948302350560085465178831205131304448768057608579225760671455428319507683044761328528378598680521969/129029399608003591393877563635427268468223241968702796445824739401324964143354738602839165557158550222544334527817611237952284944895153877903911171908301810463504140463343237968965851318028690171589696893298002117373508378605139051661600708990326056589376830550641350933341281166927247648417290331911768552667053293568*y^16 + 3133351332007770874661396870456472907385957024871635814952439681207818853512116684666367718952218958882656090359896364341759785126242953486201399586635942419381195443002118297256972922446900839682171982308470401699309253227081599554425163721601299684188497278753230462951904096220926751470014737619070922332872433588689/64514699804001795696938781817713634234111620984351398222912369700662482071677369301419582778579275111272167263908805618976142472447576938951955585954150905231752070231671618984482925659014345085794848446649001058686754189302569525830800354495163028294688415275320675466670640583463623824208645165955884276333526646784*y^15 + 6401064282291590085231285579690994906959351540547956524808421422128493606665586520235955497412107701559074440990547587761801962073779755072913039629592303442053869810999580056331624031480390651179958978739668743118242169688498648487227168974830409330933693763109328977757762379447512779776120289861542388764011602333991/48386024853001346772704086363285225675583715738263548667184277275496861553758026976064687083934456333454125447931604214232106854335682704213966689465613178923814052673753714238362194244260758814346136334986750794015065641976927144373100265871372271221016311456490506600002980437597717868156483874466913207250144985088*y^14 - 5622869036368342832569577232202149688934616895837828329822401578095099980538697901457107753657196886704794232340631657074855263010536071081009369097338607187083220108218989693707376496133960192526187447777762731007411389976204560021484040734258902115898905685133793193932034788375606893259219042678806282352231790257073/48386024853001346772704086363285225675583715738263548667184277275496861553758026976064687083934456333454125447931604214232106854335682704213966689465613178923814052673753714238362194244260758814346136334986750794015065641976927144373100265871372271221016311456490506600002980437597717868156483874466913207250144985088*y^13 - 634788758226515459975384971000757027413828696011796254820161928170260551960620613451804008611484982155050945827711501972061972617164030884174629232189995098681455851091150482585696380755779261956171768516964438636686267037928511916254308745805395940719380506984374669802522191383231304545306060260242877840126398575737/3024126553312584173294005397705326604723982233641471791699017329718553847109876686004042942745903520840882840495725263389506678395980169013372918091600823682738378292109607139897637140266297425896633520936671924625941602623557946523318766616960766951313519466030656662500186277349857366759780242154182075453134061568*y^12 + 2022701158337644046789011577967821374495929318758837545332467640285509349098665266221504353973154138137704530497805639332246958175566226696887941141524354962529956637038240902209532812356137876193931667045234870191448458925729628650552709571241389177399194193183056138278965531868750632875681897227594842786661680452139/12096506213250336693176021590821306418895928934565887166796069318874215388439506744016171770983614083363531361982901053558026713583920676053491672366403294730953513168438428559590548561065189703586534083746687698503766410494231786093275066467843067805254077864122626650000745109399429467039120968616728301812536246272*y^11 + 789376630502366299842704151514228112344636769423763880479115486455053485894388504241493933182903330081722951184525347068948570559522759800234158963460252458944809038479006722118591113660562466511703873536443532363057810824202431787620716499650250188590820031871249738611654312494265543093562309404127426034007789811475/3024126553312584173294005397705326604723982233641471791699017329718553847109876686004042942745903520840882840495725263389506678395980169013372918091600823682738378292109607139897637140266297425896633520936671924625941602623557946523318766616960766951313519466030656662500186277349857366759780242154182075453134061568*y^10 - 306103688096091683923038028654409217730978245061895041447284701303420511734630988392203584622277710661548942601675498113821012065840565596543351848979938897962986261951732208655459414082856808257203906716741282541795614640223208706157495928177239300905029705319032480776914412775484581122686090458824600941911275958291/3024126553312584173294005397705326604723982233641471791699017329718553847109876686004042942745903520840882840495725263389506678395980169013372918091600823682738378292109607139897637140266297425896633520936671924625941602623557946523318766616960766951313519466030656662500186277349857366759780242154182075453134061568*y^9 - 110893404205832663706975498515316980709987127016073442103171806124380134851307183750347803060473390667942747748315391447527602303684838193847395003485605921720964703641099699533460543642326235929607407535923861543775291775181552712303714149378751053286118084586921811073339980804688578883863893299384636559510505580721/504021092218764028882334232950887767453997038940245298616502888286425641184979447667340490457650586806813806749287543898251113065996694835562153015266803947123063048684934523316272856711049570982772253489445320770990267103926324420553127769493461158552253244338442777083364379558309561126630040359030345908855676928*y^8 - 17167948898881895126854106884796513976378763767682066168712665521135630180506305165150079385080409742394051988856878901026166291854621629525232143504371373155555161422381353883117236165829369187250299552606379314902407779032772612400283836450924345992044428180436874812964411503583569321085697321838626737510223358513/756031638328146043323501349426331651180995558410367947924754332429638461777469171501010735686475880210220710123931315847376669598995042253343229522900205920684594573027401784974409285066574356474158380234167981156485400655889486630829691654240191737828379866507664165625046569337464341689945060538545518863283515392*y^7 + 11672992144347139049097245603492195462672613327177640780915158781036537925559499646345313083694304783169888860890890818750584279915072825784801764744072026723992612294548213270215624839909712077819300119053517682852603809969576022891682924326126771688174028805791905958750320700486405289596281004070107672004577284551/126005273054691007220583558237721941863499259735061324654125722071606410296244861916835122614412646701703451687321885974562778266499173708890538253816700986780765762171233630829068214177762392745693063372361330192747566775981581105138281942373365289638063311084610694270841094889577390281657510089757586477213919232*y^6 + 9421462649033379263575672858699783174078400198844439759220196850270113787583992587429126389356709267830241279159110027100052321164203884416280604179625922168769354830934229740241262877773181215596565089096962546395217411114754007056506558286782710330125185039486315201391535257392053183225286617113595357058835286677/189007909582036510830875337356582912795248889602591986981188583107409615444367292875252683921618970052555177530982828961844167399748760563335807380725051480171148643256850446243602321266643589118539595058541995289121350163972371657707422913560047934457094966626916041406261642334366085422486265134636379715820878848*y^5 - 559759036411379157778791170551114067914436349851995138185729932336722546265169895239269956856739620258916692127413850760069965784322622115378969823088734458973640155365534971124445831710712122645035360762422661367968524302497458689644058994659979276260417600845328152619864900448749575830533296767403664836582760715/94503954791018255415437668678291456397624444801295993490594291553704807722183646437626341960809485026277588765491414480922083699874380281667903690362525740085574321628425223121801160633321794559269797529270997644560675081986185828853711456780023967228547483313458020703130821167183042711243132567318189857910439424*y^4 - 213071723928873702890696563687684086052341440376714346177554955767108673593075101634260388936807042253938771146421620483829459420158065969653865422994862888391477951801695028311213538717933006038354008615839097296383369939524755328653641708628784484591632721801437146525898272606603435400355862524092055545687120551/15750659131836375902572944779715242732937407466882665581765715258950801287030607739604390326801580837712931460915235746820347283312396713611317281727087623347595720271404203853633526772220299093211632921545166274093445846997697638142285242796670661204757913885576336783855136861197173785207188761219698309651739904*y^3 - 27135111825091207954700953165278369623324694906017120822414434374574080856383378119481063578268135539297465517449540637345093882273021300426079192893856236136371349389343560423379024001670666752319438449019790396661997375005462337468499774265638549705332641483530539157238362866259804387485747534044001380581412539/7875329565918187951286472389857621366468703733441332790882857629475400643515303869802195163400790418856465730457617873410173641656198356805658640863543811673797860135702101926816763386110149546605816460772583137046722923498848819071142621398335330602378956942788168391927568430598586892603594380609849154825869952*y^2 + 2229067026970008324669572962112829680482668018208649035783653968400788868227661012828933596355349898856806003738767810955399688597422191610959050456277585311650444118121617122351919321681444739283449246946051970713903360705914840645639686054797937186234552085643400091828824032294558363359694166666095784013844443/1968832391479546987821618097464405341617175933360333197720714407368850160878825967450548790850197604714116432614404468352543410414049589201414660215885952918449465033925525481704190846527537386651454115193145784261680730874712204767785655349583832650594739235697042097981892107649646723150898595152462288706467488*y - 1286623111841963825477982214159173821101194006088661399025123583317638028535120597513415330999243417335452233897671796255312816524074699928346359164232450974547348433309518898551546416223287720484516696568887639799577278002486154279752028506845674366200197579483629902335186003837909653292828172903407833923626389/369156073402415060216553393274576001553220487505062474572633951381659405164779868896977898284412050883896831115200837816101889452634297975265248790478616172209274693861036027819535783723913259997147646598714834549065137039008538393959810378046968621986513606693195393371604770184308760590793486591086679132462654 # 3 Loop Invariant -17062192639469981027252401146036640315610830615766077466501203652786698967482724140812681264094841738510944002684859600329213592008559662279261976847789804110203304420862786832828170637985965151000129290944870673146494540894674251685797741919365483970825638024881406766908585029143194675319458167922113301337964093000111917980641257323909858722015672208109791560382968032212878111773469/119678279538752150236541160743044935411596451380794646418763998788212114674848711659577035141484717445930087012173421186688055194057641292517015682403551950183341537547415056199076844679035768547936351661991102872424632885325371078094182651560658831331549032870712677801173555910674162344817505612690321618740398170805496748781316344139487755189137818703405672238668751188462349089930064076734464*y^38 + 114130295372493453508952538020888119414125359324742932320294297861586622397606008224131046023879393199203199044207191012448276192421940919432626966113333749901598045337342552033259061514078213422976779684831005061611576168156648252859323638190709025877939850608584515253993532577097981668557123492668947951741717346350479189612799097145840878931986962053801630771010979950652551770615045/59839139769376075118270580371522467705798225690397323209381999394106057337424355829788517570742358722965043506086710593344027597028820646258507841201775975091670768773707528099538422339517884273968175830995551436212316442662685539047091325780329415665774516435356338900586777955337081172408752806345160809370199085402748374390658172069743877594568909351702836119334375594231174544965032038367232*y^37 - 104407254379055020461411210740197242120712163519856697274015508170820193805977802271260002901987121543891920175820893066919057117309394281289756023005051877311772615243452792656996194676257665814110739985251621893396803022146199833352742127741103536281969781381470702505481416285862830180509423205933134447713263001424288985195944812314617290436070859055940021900586962362000168032945087/29919569884688037559135290185761233852899112845198661604690999697053028668712177914894258785371179361482521753043355296672013798514410323129253920600887987545835384386853764049769211169758942136984087915497775718106158221331342769523545662890164707832887258217678169450293388977668540586204376403172580404685099542701374187195329086034871938797284454675851418059667187797115587272482516019183616*y^36 - 6423553948027188230858465129748973088832370303062340450057400030838415865617437777596118455353247901218356965362483398315524951085739108454000330979824461990274176716461674915720198401785355298607489382787044031521072501210270404066979019299618324383818971270116154105193878263703814626607408373392924168935217373397052722105506478136367717778389541857163332864787687348890097401025918559/119678279538752150236541160743044935411596451380794646418763998788212114674848711659577035141484717445930087012173421186688055194057641292517015682403551950183341537547415056199076844679035768547936351661991102872424632885325371078094182651560658831331549032870712677801173555910674162344817505612690321618740398170805496748781316344139487755189137818703405672238668751188462349089930064076734464*y^35 + 41946035492019479312643633455115414740036995128977684151085781206391550500158022307735208083057668937277180376226646809100145060664079937261140428702963265315912774039622758447537780439193760732866760563290624274539092349130083106560544989424283954089856199465078326079313151394842338217693820638933996790788893316285461606401520874417340617464885993613023000555483996596590634286147656437/119678279538752150236541160743044935411596451380794646418763998788212114674848711659577035141484717445930087012173421186688055194057641292517015682403551950183341537547415056199076844679035768547936351661991102872424632885325371078094182651560658831331549032870712677801173555910674162344817505612690321618740398170805496748781316344139487755189137818703405672238668751188462349089930064076734464*y^34 - 1317780532556432035786693112121581480373942808183030330997209105349036419499028639628489246776527327760557622796221730542589690029999517142841830933347961077138776956413031662140922091299175264648069013582947650146431088789650418046866371395468159667462494127404215329752005911657866377198203087935266497409492497511561322913863463011061127188884415407683097735899683802057430529565759661/2301505375745233658395022321981633373299931757322973969591615361311771436054782916530327598874706104729424750234104253590154907578031563317634916969299075965064260337450289542289939320750687856691083685807521209085089093948564828424888127914628054448683635247513705342330260690589887737400336646397890800360392272515490322091948391233451687599791111898142416773820552907470429790190962770706432*y^33 - 147851911242992098185683612063067641495555420659331860267833489459182683635674339099725406342999356173689740528491053283488940148723144916067888695210080552132466032528052083170966927850572852678946777610222624542164037798643073652754877257767047070984129481295966206822573713996241019884649093211883295238602849021149074846455228186261030704738515810513282782778981583104954205699460316201/59839139769376075118270580371522467705798225690397323209381999394106057337424355829788517570742358722965043506086710593344027597028820646258507841201775975091670768773707528099538422339517884273968175830995551436212316442662685539047091325780329415665774516435356338900586777955337081172408752806345160809370199085402748374390658172069743877594568909351702836119334375594231174544965032038367232*y^32 + 1321696170182289993972815183724320568306416525307953509225975121733171649509477409690936506262031888579394083092142371391592745508131049538484600603300813315144771325346895831653787264210029176460180887164520572626723218075770455830199773753881978608079564856182660945953187224514047691857426935746494095880629329700825945901745045400933149091034800672392184187277871874433127372201497133027/59839139769376075118270580371522467705798225690397323209381999394106057337424355829788517570742358722965043506086710593344027597028820646258507841201775975091670768773707528099538422339517884273968175830995551436212316442662685539047091325780329415665774516435356338900586777955337081172408752806345160809370199085402748374390658172069743877594568909351702836119334375594231174544965032038367232*y^31 - 4954940424506884660111996139277359126104729482261448361911762984260120054643806941415151389557361316372376891596815876592805381490757351101464364793133700489394447374529310821656241867313327680862198521944560572684400841800746240075147313039301599109191524055173134222075768397953186502257790609361051383634928639666131123137125497575070771713182284941702734426774385286697131835496570199181/119678279538752150236541160743044935411596451380794646418763998788212114674848711659577035141484717445930087012173421186688055194057641292517015682403551950183341537547415056199076844679035768547936351661991102872424632885325371078094182651560658831331549032870712677801173555910674162344817505612690321618740398170805496748781316344139487755189137818703405672238668751188462349089930064076734464*y^30 - 13638718441333880413324895550961161280070920447007490432630173185271528183329675107483953545929042065433598398938870906883259970852203194229722474651091177789267022451704781210332047625892898265157880975798132891492947617356552621432785764241258230737571072305026436827896582414352841099222279676837914020532494374544321945036316067532389442285340291890281081005280750030628322305159226925755/119678279538752150236541160743044935411596451380794646418763998788212114674848711659577035141484717445930087012173421186688055194057641292517015682403551950183341537547415056199076844679035768547936351661991102872424632885325371078094182651560658831331549032870712677801173555910674162344817505612690321618740398170805496748781316344139487755189137818703405672238668751188462349089930064076734464*y^29 + 20799277390362456205485977910678714517908243414442983762514865628922641002121234510876096387862457950407962786685588177934043597366418184491175315326851417010007484422840572801584968933987061341169465257747148150374641425113184543053960030127915481627830134313637641587415284641983749523344774104355078781270764811577221130962839751495963796096523785981779155469259979676378570529783875876375/29919569884688037559135290185761233852899112845198661604690999697053028668712177914894258785371179361482521753043355296672013798514410323129253920600887987545835384386853764049769211169758942136984087915497775718106158221331342769523545662890164707832887258217678169450293388977668540586204376403172580404685099542701374187195329086034871938797284454675851418059667187797115587272482516019183616*y^28 - 38998360963228102678804402485624116451631702655361853748874536263360445903411828080613116903762852292220096622303531827983832591918608317416962572064196652977128318331263763202143465398076347171630437118671887459936564316869386119046300897941985090827135822019092120888753269521622219210704943773186705400446527240578360361615067015250110228005194152827906336021893777363858283228942297600203/59839139769376075118270580371522467705798225690397323209381999394106057337424355829788517570742358722965043506086710593344027597028820646258507841201775975091670768773707528099538422339517884273968175830995551436212316442662685539047091325780329415665774516435356338900586777955337081172408752806345160809370199085402748374390658172069743877594568909351702836119334375594231174544965032038367232*y^27 - 379045763389064998550364886253463801488588587767468772444005002577503827632534947607861717708451357522629770436115083401259624237711896411612335704952747342148420155234963577586546081217341212212703306561422894384505873694106918684554733747557329799356617159733155530302007744934609750193730894684593745928975236135557643941275304149183391976538744005123437313834671415810185525396355058950385/119678279538752150236541160743044935411596451380794646418763998788212114674848711659577035141484717445930087012173421186688055194057641292517015682403551950183341537547415056199076844679035768547936351661991102872424632885325371078094182651560658831331549032870712677801173555910674162344817505612690321618740398170805496748781316344139487755189137818703405672238668751188462349089930064076734464*y^26 + 81077358005984660275282679881820483087880684845217124941586028821257901041727197236922115186705812858484539076428622929734326838071329068128034183542036571024297135097572122695483239251424506291662128461324448275259806169081022727118718561755514637074294925269447397578476639289034604271752489053308945631621977684515752677115025554373260648177422573615601458829304131644141945833735854327455/7479892471172009389783822546440308463224778211299665401172749924263257167178044478723564696342794840370630438260838824168003449628602580782313480150221996886458846096713441012442302792439735534246021978874443929526539555332835692380886415722541176958221814554419542362573347244417135146551094100793145101171274885675343546798832271508717984699321113668962854514916796949278896818120629004795904*y^25 - 13416656166644391401021335909767513946345991373832509668966986124714617725713661570717764943059288760923948801497171270376612252728974688755938860737845563223732167000095829919096444779864082569458500543844453350969407882252617075601022115747037339186834050825750671195139856906031893008045700345561316860692121800350096740610519470797809270885739869085816632987596946406316718082439647600303/119678279538752150236541160743044935411596451380794646418763998788212114674848711659577035141484717445930087012173421186688055194057641292517015682403551950183341537547415056199076844679035768547936351661991102872424632885325371078094182651560658831331549032870712677801173555910674162344817505612690321618740398170805496748781316344139487755189137818703405672238668751188462349089930064076734464*y^24 - 1071371179887613647772891394185711268220373210617851729257367875664389631066912150678653303368842489171147532334004276721856390118604804877233437910964593084120412924570609246131299731101847619698390959618884010169394850101565914580958750575252269351479936983180361237617100364758379693880733123607093752334411485250573405913338548093447062044932022215641436818791341858715769269512240341264139/14959784942344018779567645092880616926449556422599330802345499848526514334356088957447129392685589680741260876521677648336006899257205161564626960300443993772917692193426882024884605584879471068492043957748887859053079110665671384761772831445082353916443629108839084725146694488834270293102188201586290202342549771350687093597664543017435969398642227337925709029833593898557793636241258009591808*y^23 + 609525971470273585844508920305401007574231473966860622800470046731926451894594418446655838585648497369768654317809138017427129904373681318393029538824592795268032625237262055208556590734249368082117818916437881219293072248025739789136181498301938276444576496410730592413902114997241641098101439717706576857159166240438818063137608399142709959638597613507820044491421517934536394397593626199425/14959784942344018779567645092880616926449556422599330802345499848526514334356088957447129392685589680741260876521677648336006899257205161564626960300443993772917692193426882024884605584879471068492043957748887859053079110665671384761772831445082353916443629108839084725146694488834270293102188201586290202342549771350687093597664543017435969398642227337925709029833593898557793636241258009591808*y^22 + 4730835472058233139793811133303791019952750753074960172674537307584300842590329099253832268685933662270077403133273371663905936211896211879980121572546021084806966977191374179250299282286229897654043292251651955011833910880204453698175258596204178301610332992049001518184019353180462551355165473751025659744470891765924889104255205416803655324091818463019308128108002287300947541819619948326877/14959784942344018779567645092880616926449556422599330802345499848526514334356088957447129392685589680741260876521677648336006899257205161564626960300443993772917692193426882024884605584879471068492043957748887859053079110665671384761772831445082353916443629108839084725146694488834270293102188201586290202342549771350687093597664543017435969398642227337925709029833593898557793636241258009591808*y^21 - 815983437552495795837943748065098974916804549155599626978087015512532715849675583383304900268697199488778898964159930447788713702842079432539593365175010493418366824301853545258769634481431863921460240382305013013931683476626557881284829251944009877014882799318083757216800490606840012942008114252380142511978994563011242622633300373811034182265675300650358881417474735704613884496826959963335/7479892471172009389783822546440308463224778211299665401172749924263257167178044478723564696342794840370630438260838824168003449628602580782313480150221996886458846096713441012442302792439735534246021978874443929526539555332835692380886415722541176958221814554419542362573347244417135146551094100793145101171274885675343546798832271508717984699321113668962854514916796949278896818120629004795904*y^20 - 7886102784255324591046680792519760737428614223776910859519036891679413748956430945437144640161155102345495830700665219974736959667195327249340475857908497151185229006296526809647026095579016187743430702712050838129204955287015310380658654425495892324833730777964725312389406532123942813178149601285875547052592464932161274884670809610745228367529410800703644810791877581579545075158360323802793/7479892471172009389783822546440308463224778211299665401172749924263257167178044478723564696342794840370630438260838824168003449628602580782313480150221996886458846096713441012442302792439735534246021978874443929526539555332835692380886415722541176958221814554419542362573347244417135146551094100793145101171274885675343546798832271508717984699321113668962854514916796949278896818120629004795904*y^19 - 21510103914516143543057817840075987919390916300647603436663162531330347082972650509183703061953321201047930378056620625617711134703473801783721415396013032039469509304330816202594884613223751697274608388899501086657212409155894041444825693541930407122819861783309926793698005267349719444296898576594303998397784891356497154119693215957384953272302490306227431014978582021762076776821974059307/934986558896501173722977818305038557903097276412458175146593740532907145897255559840445587042849355046328804782604853021000431203575322597789185018777749610807355762089180126555287849054966941780752747359305491190817444416604461547610801965317647119777726819302442795321668405552141893318886762599143137646409360709417943349854033938589748087415139208620356814364599618659862102265078625599488*y^18 + 219848622413418050376363366800607157684282791095510101767335792676307899477085691979436061169916004735917250853580356549771790659073894186919173742303134253645268605080791406768327122122841556632850311580156122217323796565399452793997436386271134451140121185233028449815120660293012369486435072972800938967188051027673940762124074029854046213131941973731151983002240013510359465289008591818807/71922042992038551824844447561926042915622867416342936549737980040992857376711966141572737464834565772794523444815757924692340861813486353676091155290596123908258135545321548196560603773458995521596365181485037783909034185892650888277753997332126701521363601484803291947820646580933991793760520199934087511262258516109072565373387226045365237493472246816950524181892278358450930943467586584576*y^17 + 184268666987500075500990691411728365306807557289287904424157802192997887775915272574825281263380317872558234943333086618511396813360077207497948983739972025051264206621954631555823662194909751521766488586755016901017959150539767507401148645269304331075256759813046456308414894085781060732392839122711763353507691437702115877838511921644993432689622091335183625064855760280625375675486181480929/467493279448250586861488909152519278951548638206229087573296870266453572948627779920222793521424677523164402391302426510500215601787661298894592509388874805403677881044590063277643924527483470890376373679652745595408722208302230773805400982658823559888863409651221397660834202776070946659443381299571568823204680354708971674927016969294874043707569604310178407182299809329931051132539312799744*y^16 - 934191517437646605817749111470277596037427777940437545759001166036890621454072919881096977369439513995434402899244819324988057973950893440473393424267911013218423332789259807520594527349024682011136845898571083963178447504260346259621590422730628507348049349998992064428913493179549342360564208561794950625254024558196120351593754207887937786487306050076750521588287414457905391545051946423145/116873319862062646715372227288129819737887159551557271893324217566613393237156944980055698380356169380791100597825606627625053900446915324723648127347218701350919470261147515819410981131870867722594093419913186398852180552075557693451350245664705889972215852412805349415208550694017736664860845324892892205801170088677242918731754242323718510926892401077544601795574952332482762783134828199936*y^15 + 58096640718785795056341612137865356352496073623231133908273588831957088371129608514327103335159452216446705444543425241148183312547347980366860514556479471431575748471796276286915768945284980411739012469553871892758954232533704120848573870862115582880100102754577810586269502846900710149986758678254081720728037782104360675143662541671083733965489334154917312500977203231019606742820072177403/58436659931031323357686113644064909868943579775778635946662108783306696618578472490027849190178084690395550298912803313812526950223457662361824063673609350675459735130573757909705490565935433861297046709956593199426090276037778846725675122832352944986107926206402674707604275347008868332430422662446446102900585044338621459365877121161859255463446200538772300897787476166241381391567414099968*y^14 + 468634719071818981999474960207757611644744481042569885355966991757260841535906713682335601403292273713752535955257619665124468294401075915426070744756995246379210163400129985510494150405432873657279974614256046128668909997632150920751171650889912900861441498516243571365883763018809435818129287626596284622037682359355196988003116729242874917376193736993448558647310752687535773935078405677955/29218329965515661678843056822032454934471789887889317973331054391653348309289236245013924595089042345197775149456401656906263475111728831180912031836804675337729867565286878954852745282967716930648523354978296599713045138018889423362837561416176472493053963103201337353802137673504434166215211331223223051450292522169310729682938560580929627731723100269386150448893738083120690695783707049984*y^13 - 373013355058350629257553548121608846920758656942019889260950532427250350396994527202904262217415400758062807396421903800822193949440253720482252782222544035176002662744730376073072188188824496365206147067638473474972538710672428965212819656659005477771690981692442847901866183773921972269543109374169119256021808232220894594562194534085934160846725967467575344960239958821583688783801877126349/58436659931031323357686113644064909868943579775778635946662108783306696618578472490027849190178084690395550298912803313812526950223457662361824063673609350675459735130573757909705490565935433861297046709956593199426090276037778846725675122832352944986107926206402674707604275347008868332430422662446446102900585044338621459365877121161859255463446200538772300897787476166241381391567414099968*y^12 - 642224670165033332178587245982971008161996562275710421101740575594352806422308898379708903253154863100319625004078361043489089872016467347302071368763480695585191765192613044984777837546628486354921546912287588966167809344564469484770434906865482097562462204894372282979901059428970763228579546594881568454758942216062060725593608509833866512718388550238738081970498785417703950841835728621411/29218329965515661678843056822032454934471789887889317973331054391653348309289236245013924595089042345197775149456401656906263475111728831180912031836804675337729867565286878954852745282967716930648523354978296599713045138018889423362837561416176472493053963103201337353802137673504434166215211331223223051450292522169310729682938560580929627731723100269386150448893738083120690695783707049984*y^11 + 77244880746440552162443538018726163164722412695073146527429086943333537035653691004171939961349517920042679064517257119513508673245470126300005494040211066789634744607873472401917779587323838940940307760367260397640409886409882860458849092682709519797431772606616912613760400868444683693369530809539730745163314045178421283523196070443121445465690988776875637349821526042764009699999819928103/7304582491378915419710764205508113733617947471972329493332763597913337077322309061253481148772260586299443787364100414226565868777932207795228007959201168834432466891321719738713186320741929232662130838744574149928261284504722355840709390354044118123263490775800334338450534418376108541553802832805805762862573130542327682420734640145232406932930775067346537612223434520780172673945926762496*y^10 + 73938878864653572486445626984580980225352565914915639868179062526889486860014842684310235155272995223858879961998832574913112441395953372912358610335476945083421034973179188857821973998339779448049812974422272108912929903645468422971701364687193617629071193833925757748732682665727309094070018789763034358703137979393540871215885704583932374996240119545706541627120365213053952670880469425303/3652291245689457709855382102754056866808973735986164746666381798956668538661154530626740574386130293149721893682050207113282934388966103897614003979600584417216233445660859869356593160370964616331065419372287074964130642252361177920354695177022059061631745387900167169225267209188054270776901416402902881431286565271163841210367320072616203466465387533673268806111717260390086336972963381248*y^9 - 5893822147945806037343818744493967771707915957372046786782970646391096082497033717856875454683877381853585523982655721939607415471746851257648591939331908722396584213438871979937393724147961867512045273828504028928112983731549297035800643392581749378345255997587670222858106392750387250622413362876256398394705081516855062132769214520823882843044276583215022314308880885951436197717430753473/913072811422364427463845525688514216702243433996541186666595449739167134665288632656685143596532573287430473420512551778320733597241525974403500994900146104304058361415214967339148290092741154082766354843071768741032660563090294480088673794255514765407936346975041792306316802297013567694225354100725720357821641317790960302591830018154050866616346883418317201527929315097521584243240845312*y^8 - 22691615542821736829611364321070496174652459453375481886337813209554674886521990400941648034909848841221131625524717126998527161069567522588879474393335683537039453738813842017090568384877087277331247120962883608434942317889493277470020315747091218149688770762941202247987648183742155183238189174294691211050988285154652550852427291780367710374360283504246401500568851419659940043078976280759/1826145622844728854927691051377028433404486867993082373333190899478334269330577265313370287193065146574860946841025103556641467194483051948807001989800292208608116722830429934678296580185482308165532709686143537482065321126180588960177347588511029530815872693950083584612633604594027135388450708201451440715643282635581920605183660036308101733232693766836634403055858630195043168486481690624*y^7 - 331004858104264980424003356924362645535089233529666554322858415804586977455467198738334911261042404210048647887110981379875394464712195079148054152892740085236436911453398731776394215907795301326197705364798879114571087065753587042267157711440243381492586781908966323643178678593173969310820412980593626316390664009905369427265333551925123525506654450756583654915534848567837780141226208101/913072811422364427463845525688514216702243433996541186666595449739167134665288632656685143596532573287430473420512551778320733597241525974403500994900146104304058361415214967339148290092741154082766354843071768741032660563090294480088673794255514765407936346975041792306316802297013567694225354100725720357821641317790960302591830018154050866616346883418317201527929315097521584243240845312*y^6 + 254397586996461346757129487359870349499237344111299562860117238436747672270566632754864348896643655304666871014577461931827937980057441982601250378926655958554106185854383904832405021338404895186885638680354763548725481216581901095697312850293237532009078194297596004567680195120859113702664763342385640020170715093445692108498220440203963869968617794672635053680544603729844874330904247509/57067050713897776716490345355532138543890214624783824166662215608697945916580539541042821474783285830464404588782034486145045849827595373400218812181259131519003647588450935458696768130796322130172897177691985546314541285193143405005542112140969672837996021685940112019144800143563347980889084631295357522363852582361935018911989376134628179163521680213644825095495582193595099015202552832*y^5 + 409934666247352284120367183583815869541501876745564904561411475773733274261250376155715532809243506671259539196453827022342517120465858805450129282405130642548683761149978894653576795615898278835378294570530626935850944915464856328627591486188689406067456969615499123809064175288614624333808030813740164808911589636548862666546521681520090787977014033289006991118731540497560683679989313267/228268202855591106865961381422128554175560858499135296666648862434791783666322158164171285899133143321857618355128137944580183399310381493600875248725036526076014590353803741834787072523185288520691588710767942185258165140772573620022168448563878691351984086743760448076579200574253391923556338525181430089455410329447740075647957504538512716654086720854579300381982328774380396060810211328*y^4 - 67685498960213486225060683640411540355605783577339952246726443702652212799247580926467419168160626073663564582274649297217488557757675996152350205876911394617604913623926323283548818696902765860487459026611808513581560525946556381301608512698170036771390509494735202063134014972953263679551081775063223047855078944510052532379530652419902363535087875538131072292206730676549635431033360319/114134101427795553432980690711064277087780429249567648333324431217395891833161079082085642949566571660928809177564068972290091699655190746800437624362518263038007295176901870917393536261592644260345794355383971092629082570386286810011084224281939345675992043371880224038289600287126695961778169262590715044727705164723870037823978752269256358327043360427289650190991164387190198030405105664*y^3 - 28780016761420346620376084244236576534044610645503605631008840454059988446799816281592109854527724847802216618330746001546282758736654981539686218355934754957428807800819067724597177531499681610345469015717533378757671818001272010728058765181498265041498867083674364510287988131246786473557406162981763011623844724553321590255784407039934479287363461640525155700487875696869379180715885877/57067050713897776716490345355532138543890214624783824166662215608697945916580539541042821474783285830464404588782034486145045849827595373400218812181259131519003647588450935458696768130796322130172897177691985546314541285193143405005542112140969672837996021685940112019144800143563347980889084631295357522363852582361935018911989376134628179163521680213644825095495582193595099015202552832*y^2 + 77917621877678228607042502392502434741670448326307339943631371277337534778207546275693965647302827165379249885967672391094321210942378338453402841970435087974535222786176739750773167568586076735562019145448810774855716755742420153888883209045589054601919958055678531349468868437603897744034370439006674009564987917135521704587398957790508542091794978188137636444227351663099958798149991/28533525356948888358245172677766069271945107312391912083331107804348972958290269770521410737391642915232202294391017243072522924913797686700109406090629565759501823794225467729348384065398161065086448588845992773157270642596571702502771056070484836418998010842970056009572400071781673990444542315647678761181926291180967509455994688067314089581760840106822412547747791096797549507601276416*y + 462056091089495506142293090413635372668420363152251928322481058444050484168611405064307053725252062977435611877547888110218925587310798837290558500829302951127379007589006784526035849512819379730224444160553114461274426489140768470061399977795078748293580135370674559905438819684090674796012007787359466522826425448410150471201272824648202301193867369387624409970422899461799043833695923/7133381339237222089561293169441517317986276828097978020832776951087243239572567442630352684347910728808050573597754310768130731228449421675027351522657391439875455948556366932337096016349540266271612147211498193289317660649142925625692764017621209104749502710742514002393100017945418497611135578911919690295481572795241877363998672016828522395440210026705603136936947774199387376900319104 # 4 Loop Invariant -2731477911589676643336602200707201812317027582348501729718784998420783909588909634926195437598914284272829036838215518987677311519778444638969708158519340716186651837629935783729592527063621367385034727801548272416014629740768840063638388604861947224258256775514974771642289790700686248061355097256976658885587167580918181622724633163999385957441910620640328396335187999729368848737122786152332336274600065535140687398877949861185750151929744208885884973371299460479863200464116456233682582231056229616400095869308722803175467394562882341/35348520918258130865905810176337272142422913471935668823648051086501571917467761452877925187010801908154096412717886030010241224925275458328501055417417602203211582500742115257614500929480991769388625853797517969904555250095547678180666720489163322273710753889800338398055225658141543166228643074087944497641941249041601935441766515649779326409199485442207820813513493529626187408624254045715945710860886129062230267091912844779375381044194019663474004890450531411116646401769037785348467933406651618319304528109296974926615851220687179892297564160*y^38 + 66244769210215157083461057864631639115843024658257292362432097966287486340501314469592751699751278243027961399530687279877956104436797055941817384676450433940525098536896710068214187952271375429280471923786530881298685628546982238941584821179290906470911190594094727447721968064637972072826084757158202248220830676327388456528617525039697976075292320061923152842792576456039946672024378134930811099217156649847402037943745395335657822078354700340655980445614997008976925275176813760094053266168051017628340253448297827725637245117162547829/47131361224344174487874413568449696189897217962580891764864068115335429223290348603837233582681069210872128550290514706680321633233700611104668073889890136270948776667656153676819334572641322359184834471730023959872740333460730237574222293985551096364947671853067117864073634210855390888304857432117259330189254998722135913922355354199705768545599313922943761084684658039501583211499005394287927614481181505416307022789217126372500508058925359551298673187267375214822195202358717047131290577875535491092406037479062633235487801627582906523063418880*y^37 - 112716659024590336923313239112123227060444086797606431626803869436761689838676545815919073240161813454843170428735745545750934719214033709865246177504480799511134676107175129147721820863069519535264004351330806927993294624051078820268109993994544446121169426593351042388335184972085761870675566269877428108561087964411289006688744837200077290617075066264630996242570547533490564183407713848636981813192102458166974763720076256900003843958166765816036568505638446267338429266086195279568299854296812096859671832155126015698307149807581896061/17674260459129065432952905088168636071211456735967834411824025543250785958733880726438962593505400954077048206358943015005120612462637729164250527708708801101605791250371057628807250464740495884694312926898758984952277625047773839090333360244581661136855376944900169199027612829070771583114321537043972248820970624520800967720883257824889663204599742721103910406756746764813093704312127022857972855430443064531115133545956422389687690522097009831737002445225265705558323200884518892674233966703325809159652264054648487463307925610343589946148782080*y^36 - 100796971206650093614684921692148795122045974437710856045188895970435206197722635166999428492954308323730791704476024706024401804094026423656826562984782040118468498672953393007338627456099700512799829991268857721589333500230853433720258532484290591996541343735144726635464788255331234756433525870604243868897226025764989486643265491562473273110585690507946650628841389217486133704183008904276350759606281851758733467639267311056096435249347071164249793090739048106559989189125859520013463497559606271936565219928821810590460705268156652153/3927613435362014540656201130704141349158101496881740980405339009611285768607529050319769465223422434239344045857542892223360136102808384258722339490824178022579064722304679473068277881053443529932069539310835329989395027788394186464518524498795924697078972654422259822006136184237949240692071452676438277515771249893511326160196279516642147378799942826911980090390388169958465267624917116190660634540098458784692251899101427197708375671577113295941556098938947934568516266863226420594274214822961290924367169789921886102957316802298575543588618240*y^35 + 46914916707504608342988770477536105933883083984380919855404479257486450198270646564095488412592576572913377293490775241474329921947913602224492430258583870590015371091867944389912775478905522957165314483496643856543555992965788466202446194958455988097538749586231881085294162837868505250786833744759036670606488509608959693509205214325545483382028063091969885190038360370831595347177696317084603182022831897727772677473019035300406720337301328486383125260178874858692541485716667386873423074930824504928249941818855225107154758831153631189313/141394083673032523463623240705349088569691653887742675294592204346006287669871045811511700748043207632616385650871544120040964899701101833314004221669670408812846330002968461030458003717923967077554503415190071879618221000382190712722666881956653289094843015559201353592220902632566172664914572296351777990567764996166407741767066062599117305636797941768831283254053974118504749634497016182863782843443544516248921068367651379117501524176776078653896019561802125644466585607076151141393871733626606473277218112437187899706463404882748719569190256640*y^34 - 11260570475942235987303481598801158912701501739432907141749944494808248791537474455176071923419794503165139716164114774256031852753251542644743181215612116081647842784255696002357695780642212688380462794804577778378860640940178412629751511296204101295136907213386461752770783009735734342977007706628689291419101095227551163270967510133149738284335829613784159325285106045000464022683184659698990425974794317300180988410996328277924622695985639164845415546080809146116714115016990135974384670935740826380837388440641009721672519086232924414961/10876467974848655651047941592719160659207050299057128868814784949692791359220849677808592365234092894816645050067041855387766530746238602562615709359205416062526640769459112386958307978301843621350346416553082452278324692337091593286358990919742560699603308889169334891709300202505090204993428638180905999274443461243569826289774312507624408125907533982217791019542613393731134587269001244835675603341811116634532389874434721470577040321290467588761232273984778895728198892852011626261067056432815882559786008649014453823574108067903747659168481280*y^33 - 16927461422888228546881095056696409180982799027086785125773107282290336315970350598110775550249718078253730254056953183568375280944460175224450217164020076864359517602854692782268531102046417260417486735918015078693809960870747069781880852612799451786002866369243820162867367177151696921637379399922020698370336022570034704322306944344145236255770854649513880256806392261023456067672938356350780889330097081281591094011993021278621449814626308399385021207495890274202536016591207553998172069457254546087080634928686322353805907486634655844723/23565680612172087243937206784224848094948608981290445882432034057667714611645174301918616791340534605436064275145257353340160816616850305552334036944945068135474388333828076838409667286320661179592417235865011979936370166730365118787111146992775548182473835926533558932036817105427695444152428716058629665094627499361067956961177677099852884272799656961471880542342329019750791605749502697143963807240590752708153511394608563186250254029462679775649336593633687607411097601179358523565645288937767745546203018739531316617743900813791453261531709440*y^32 + 1328341073740635375182411488763371030632051255921579140132544166306371110905010465350962177799441968751606345310806314275760960630247406502991562034109375280577634510008393874899143100038393125568916697079449233277714608186192159087351626490620438851703237273941999756879995673777906760167532425325453882250197743505332447512468134914137372491674972694690348881486750950921883823205612021452850091382149603816374445292470433477530052824755845743665284389022806995216797981971456952234604948857149278969828234281666953547765639148768479370954487/70697041836516261731811620352674544284845826943871337647296102173003143834935522905755850374021603816308192825435772060020482449850550916657002110834835204406423165001484230515229001858961983538777251707595035939809110500191095356361333440978326644547421507779600676796110451316283086332457286148175888995283882498083203870883533031299558652818398970884415641627026987059252374817248508091431891421721772258124460534183825689558750762088388039326948009780901062822233292803538075570696935866813303236638609056218593949853231702441374359784595128320*y^31 - 4988044725377297447927026120462524546467997791405724875901826474094654184918948352597631036419212640301002410650826293997607802006182503050517638656082749653643030096877243759917893445916481340285881380159100622543574232744140362092106932546749723918154249241892709548147285369652497462736863823740054428877511460145756358820750331943601330659964312508008368711492574120450578163487072945866850913923396832085053444020716280937029820857134069340737101262088574333116989921475944203582674385786222495192896366199743378484913583754846107527364537/70697041836516261731811620352674544284845826943871337647296102173003143834935522905755850374021603816308192825435772060020482449850550916657002110834835204406423165001484230515229001858961983538777251707595035939809110500191095356361333440978326644547421507779600676796110451316283086332457286148175888995283882498083203870883533031299558652818398970884415641627026987059252374817248508091431891421721772258124460534183825689558750762088388039326948009780901062822233292803538075570696935866813303236638609056218593949853231702441374359784595128320*y^30 - 1891262150565395074735991554427510731422583965795055750938419812649893114951867086049321290201292642765858242831239003310116781809691548628723625211976496877159482394349154199394483651431135101132368069422468709807515520606069501470963509638941745914419176826337473776282264982381106014852743773027274111641308297656278940928898943849051134469418810761807932395883289632964005272942705469495970591828236079947088211649424548692378252363265018635554318858091391648078053122831516270649277315458738218518292547825434729007021146340509345565592713/141394083673032523463623240705349088569691653887742675294592204346006287669871045811511700748043207632616385650871544120040964899701101833314004221669670408812846330002968461030458003717923967077554503415190071879618221000382190712722666881956653289094843015559201353592220902632566172664914572296351777990567764996166407741767066062599117305636797941768831283254053974118504749634497016182863782843443544516248921068367651379117501524176776078653896019561802125644466585607076151141393871733626606473277218112437187899706463404882748719569190256640*y^29 + 100246237617361613570923774416089575293831638669496127215806734325562049298124841335559783889675368535568023791023608999897005283742499645805282369404439453210544444601543936694483431639734296514340703856038782496007141526528305955318614587554756161075723019134850291326177185526768152843243443155850992444918978262751435625979914674852460366241539382734746492676629931925309036023257683577681793905154183778944652005385402847861447961306871453362562884691252129950417714360868672238399207364012196431445608028044206815140351705813552798564144839/141394083673032523463623240705349088569691653887742675294592204346006287669871045811511700748043207632616385650871544120040964899701101833314004221669670408812846330002968461030458003717923967077554503415190071879618221000382190712722666881956653289094843015559201353592220902632566172664914572296351777990567764996166407741767066062599117305636797941768831283254053974118504749634497016182863782843443544516248921068367651379117501524176776078653896019561802125644466585607076151141393871733626606473277218112437187899706463404882748719569190256640*y^28 - 7970927244361240382742731037529141361260031513361259714379308758392972926498987892437444051603126449558924407734965839322481644704282758350751610388286974448861622380460239505272249551019520246255703095794236878559576765585234054728713254543258526330061830429958108458225315574983796305702484951638062839736924081221634189183242159257591984073799327850046696686313492147662815898381789045121193322357302330036267935555549684048512226103886192346335439557047572332378346503343861902511020578841782653144961766243847333081109644867148524536470895/4713136122434417448787441356844969618989721796258089176486406811533542922329034860383723358268106921087212855029051470668032163323370061110466807388989013627094877666765615367681933457264132235918483447173002395987274033346073023757422229398555109636494767185306711786407363421085539088830485743211725933018925499872213591392235535419970576854559931392294376108468465803950158321149900539428792761448118150541630702278921712637250050805892535955129867318726737521482219520235871704713129057787553549109240603747906263323548780162758290652306341888*y^27 - 37869821597525007863567871285951251005865541985998718577168154005449876546832732311717489113826720444163870703608236419509618094543452137559109335896713486587221551061783881373654531618703866813837798832278202158201856259087630219474825337776325562148143490979166877221823901778559947336689047988376955584655627972935524312701270947584963744635703788144636249315708454990979257771159939081376879613097305402522784905414860682147413367592830645177988486476569541647012644149321110930826186485171816303963223551538564362770530641309784555308043379/23565680612172087243937206784224848094948608981290445882432034057667714611645174301918616791340534605436064275145257353340160816616850305552334036944945068135474388333828076838409667286320661179592417235865011979936370166730365118787111146992775548182473835926533558932036817105427695444152428716058629665094627499361067956961177677099852884272799656961471880542342329019750791605749502697143963807240590752708153511394608563186250254029462679775649336593633687607411097601179358523565645288937767745546203018739531316617743900813791453261531709440*y^26 + 634854354551682124538182238286981011577429338778747178297549519253961504862030186527741001832530656422125342405899307387255401450474095159540631863809031506966040162388740796318584373456084887461874891645032522428246254634095956417109756367509705857811873374424639177749426807311503812005952651200897505460705035905326691062926307797254337938669552247880929612548148989126767812803552270257613554712699872552764288349516080643117737850555586675142559852894857336108592967147281456084160419991758530102491911033715862442450281995091283479651597013/47131361224344174487874413568449696189897217962580891764864068115335429223290348603837233582681069210872128550290514706680321633233700611104668073889890136270948776667656153676819334572641322359184834471730023959872740333460730237574222293985551096364947671853067117864073634210855390888304857432117259330189254998722135913922355354199705768545599313922943761084684658039501583211499005394287927614481181505416307022789217126372500508058925359551298673187267375214822195202358717047131290577875535491092406037479062633235487801627582906523063418880*y^25 - 423048556876777097960688261273910056854004880747876763413472742438932261728731049530396485114958416403701004809617901324322679986789505935042471454251598417388700883545915699679670417944503623233728420879182150012818310044431486790715831940798166032734590329555724945987572898181174358223780363729174275543351919095099227630337550575009227385795708013812559971884605729872541478121075556242972692654249209423952931902354657151477838810210468595657998285779238412764601612801983928592227112091129069374767785166605580846297438078128016522770233989/23565680612172087243937206784224848094948608981290445882432034057667714611645174301918616791340534605436064275145257353340160816616850305552334036944945068135474388333828076838409667286320661179592417235865011979936370166730365118787111146992775548182473835926533558932036817105427695444152428716058629665094627499361067956961177677099852884272799656961471880542342329019750791605749502697143963807240590752708153511394608563186250254029462679775649336593633687607411097601179358523565645288937767745546203018739531316617743900813791453261531709440*y^24 - 547537111150591995592686360229874123544476799629678056246468370462806997095608490086802433431452364340448583970880451820703101167128673435373151667084751090419112190968812434034995180708015828314009284647485140609421708708214589531321123916362355220471253192586857905975952680117090160626363493228991261283988164711765686775676433213658458137019993907012235503793130501211959643912418605818094800511318831954781538864480089741002391149300682701406645696803119386782552465617320495880322380953882751332358042763833869841886947003837769399374356621/9426272244868834897574882713689939237979443592516178352972813623067085844658069720767446716536213842174425710058102941336064326646740122220933614777978027254189755333531230735363866914528264471836966894346004791974548066692146047514844458797110219272989534370613423572814726842171078177660971486423451866037850999744427182784471070839941153709119862784588752216936931607900316642299801078857585522896236301083261404557843425274500101611785071910259734637453475042964439040471743409426258115575107098218481207495812526647097560325516581304612683776*y^23 + 811127919642014440989047899320927894068181261306166296333815208133236676835817458380609192846732359496898415792501014866311464949143198973399626410681726879791172414406818078504226379983385224937603809399396332070576270631023809605962627084251424288902356959019615520403548693121435648715166892391401629566633479435908112921993323214120800245330436725121025231638288647154066728807035880128706390644324104272338274666636870202107589373866048216137795865171428817777493962179270862602998909319761727547126650020859961203961502526880867874243134759/4713136122434417448787441356844969618989721796258089176486406811533542922329034860383723358268106921087212855029051470668032163323370061110466807388989013627094877666765615367681933457264132235918483447173002395987274033346073023757422229398555109636494767185306711786407363421085539088830485743211725933018925499872213591392235535419970576854559931392294376108468465803950158321149900539428792761448118150541630702278921712637250050805892535955129867318726737521482219520235871704713129057787553549109240603747906263323548780162758290652306341888*y^22 + 302124627625545025550991676839269551262938421407008138962897965943033053257062761896475590070766697823662004125658690805852977180774378319510947181766207307404194517740246207595299668011575868601014814121099056126927848311795253640016525893695835634039749123233886377039017979033938230168973617744782118308928244253515923276947393206691643862013722544954431109698119098614608837286049938690380242563057339426988143785217481478418638062305877919449478241867577895382739178178290525510737981936377606128683427565821355094705711393923774526496683083/1178284030608604362196860339211242404747430449064522294121601702883385730582258715095930839567026730271803213757262867667008040830842515277616701847247253406773719416691403841920483364316033058979620861793250598996818508336518255939355557349638777409123691796326677946601840855271384772207621435802931483254731374968053397848058883854992644213639982848073594027117116450987539580287475134857198190362029537635407675569730428159312512701473133988782466829681684380370554880058967926178282264446888387277310150936976565830887195040689572663076585472*y^21 - 3043137739888953145132585643161111314906798895071779412433907129111875607558088363021335512653647461230727601945006084034074291228790571049134327109526734120615953687525497352749074404460678372480480467716849431252206636591288018415057188714847352218103979366246046222229846279851027360737242472681111015167029443722900271912307701327740730114084863486852117983804549451722087517429153642563906197743195722726467045321854083078988183192017524376398138862058926482368777715847848506987714609758009667466381466515749897907432357180709765591825302979/4418565114782266358238226272042159017802864183991958602956006385812696489683470181609740648376350238519262051589735753751280153115659432291062631927177200275401447812592764407201812616185123971173578231724689746238069406261943459772583340061145415284213844236225042299756903207267692895778580384260993062205242656130200241930220814456222415801149935680275977601689186691203273426078031755714493213857610766132778783386489105597421922630524252457934250611306316426389580800221129723168558491675831452289913066013662121865826981402585897486537195520*y^20 - 2423824556740371103250914908863705302546518299044289543596137167176242550305759004826496521569041646182865963743752362062921542641309842458972496556742131451137370710195545447590582165588355895059337633520416050496364381942122149388471843076421504868311437087536150961450405859804055713062561922328310037135660136774029793007355616567819262336401838526703868439169498137120667259265479284717501472676276643789008926297421030015550178617547427889490082797332509923269050198092624955440499743679372397601131921819551631441087609653995793243477168979/2209282557391133179119113136021079508901432091995979301478003192906348244841735090804870324188175119259631025794867876875640076557829716145531315963588600137700723906296382203600906308092561985586789115862344873119034703130971729886291670030572707642106922118112521149878451603633846447889290192130496531102621328065100120965110407228111207900574967840137988800844593345601636713039015877857246606928805383066389391693244552798710961315262126228967125305653158213194790400110564861584279245837915726144956533006831060932913490701292948743268597760*y^19 + 3778407978361355552278449976552518372707137405087716850322488267084028915274146854399302174369205723827869471538906523034884088248193071896129241890080424472334790859913608470749857630232024923702579556169232514662336847373789393814135012761918909467148641095663997197032802309895617711568518837636941040431947851626606473723365427298069102919208199982037668168934742253492389822676676881594023997295067828274064256665802413883860694529090508147617567015093464679347737517953934196936071039030101431921823270792697851673568895199339320310470800409/2209282557391133179119113136021079508901432091995979301478003192906348244841735090804870324188175119259631025794867876875640076557829716145531315963588600137700723906296382203600906308092561985586789115862344873119034703130971729886291670030572707642106922118112521149878451603633846447889290192130496531102621328065100120965110407228111207900574967840137988800844593345601636713039015877857246606928805383066389391693244552798710961315262126228967125305653158213194790400110564861584279245837915726144956533006831060932913490701292948743268597760*y^18 + 647431506208554669779678350525995965970400259968547872462665673801026762331379131423098375420462254076203398012972705666849941211263690375511551630700675671765112410852158807626239410989744551671202739380346258435214861975904235397274336295078088193642705697865531521794615704387553859376090971171482418921712755203488536556976794778223327190848029541301655198673344828618745823447088339368616205808339189296431949018033497220703358595222253399820450093097241018927422586941974763844046181268453266996050693543679162861091708032951984123493708849/169944812107010244547624087386236885300110160922767638575231014838949864987825776215759255706782701481510078907297528990433852042909978165040870458737584625976978762022798631046223562160966306583599162758641913316848823317767056145099359233120977510931301701393270857682957815664142034453022322471576656238663179081930778535777723632931631376967305218472152984680353334277048977926078144450557431302215798697414568591788042522977766255020163556074394254281012170245753107700812681660329172756762748164996656385140850840993345438560996057174507520*y^17 - 882786804725345850461811116729823697658396304513366505615538760845556935184148687896078423343359713648422784902806151203584239092823997193829151964727972257226571284798230635694813652486109111765018660104465274602699740064374467312783276496999621486324679098892662035596753088716524581177385672723531985110569919769852856517458988244248320920203937651028401127707318964791966448806197566998056211579092389294647903700181367677908656354005579384493187640188998368683878727112324463575877268486689313007930563626328315728456650336147697246761185075/220928255739113317911911313602107950890143209199597930147800319290634824484173509080487032418817511925963102579486787687564007655782971614553131596358860013770072390629638220360090630809256198558678911586234487311903470313097172988629167003057270764210692211811252114987845160363384644788929019213049653110262132806510012096511040722811120790057496784013798880084459334560163671303901587785724660692880538306638939169324455279871096131526212622896712530565315821319479040011056486158427924583791572614495653300683106093291349070129294874326859776*y^16 - 308984047255413843757053860780435111132790042880310855376988729891400676864636048997045553645563090020967835910575887294320730978884766256535497863311853390431617945578091558835197690343225574052459407253419232139229701502417338037233561856151016957201101550517321495946075600593552172224203695148828887968639335756904843290828154017563319055530523897694852221951410271595314323178256898946091644065076667946269202735875504637570939078137851580108036516529788049275086930773437568584390820678083289167045762777274093453107608382862742609393224169/30684479963765738598876571333626104290297667944388601409416711012588170067246320705623198947057987767494875358262053845495001063303190502021268277272063890801398943143005308383345920945730027577594293275865901015542148654596829581754050972646843161695929473862673904859422938939358978442906808224034674043091962889793057235626533433723766776396874553335249844456174907577800509903319664970239536207344519209255408217961729899982096684934196197624543407022960530738816533334868956410892767303304385085346618513983764735179354037517957621434286080*y^15 + 526365593405658471477502841090580349837287958977056200958262209457180726054760963123836434933009393100500099548771245611738266165926289058596115990410653418227884589533533563573694970322341345883330396007908969490222552633004509164346900866470663567942999254932700344417249242070138275354441182424580977588401553541368953110378626068532216702823696969989652930222684596995639388243091403480886443041732692672238253358349874344844234453639358305054225143135556593095699872451176780943645359618716334203155638588038169168978242530678028054319388527/46026719945648607898314857000439156435446501916582902114125066518882255100869481058434798420586981651242313037393080768242501594954785753031902415908095836202098414714507962575018881418595041366391439913798851523313222981895244372631076458970264742543894210794010857289134408409038467664360212336052011064637944334689585853439800150585650164595311830002874766684262361366700764854979497455359304311016778813883112326942594849973145027401294296436815110534440796108224800002303434616339150954956577628019927770975647102769031056276936432151429120*y^14 + 2527992983202664981054159890258580775197712694468349344059928219875566310840385371590812977672034799763798152152227476634485274939000618226712650591700358343325009444562026892235835607090450113209984639821367070658429118101736487865756906536714169679820804255058410933267465871202018013774056797701669517995479606474871420287139120051508369146191802322264497037629267872160095001565161811108582732629747341498896454333796414546552661005204802950102610022826366848180366268020848146286171228473332887684420323405178777189921309241086978012387684621/138080159836945823694944571001317469306339505749748706342375199556646765302608443175304395261760944953726939112179242304727504784864357259095707247724287508606295244143523887725056644255785124099174319741396554569939668945685733117893229376910794227631682632382032571867403225227115402993080637008156033193913833004068757560319400451756950493785935490008624300052787084100102294564938492366077912933050336441649336980827784549919435082203882889310445331603322388324674400006910303849017452864869732884059783312926941308307093168830809296454287360*y^13 - 1822336623395780782781776725848041511288284769600871767161384259716337224401526920536828732954094337911608807626080264226857506161502021686139139765994513246890168201882695212236468685185248758575878429381438820094635964723086139498078527996873280858811246072454900921577795128827089038324149473132975771267333453553451607868852569162934378029263218521419100357195882299697625123447126679956954596887900406679695571704620150919314880233458964722691196098226503820430036725103184473229531922120392571774004781153962980247675589494175190867124391827/69040079918472911847472285500658734653169752874874353171187599778323382651304221587652197630880472476863469556089621152363752392432178629547853623862143754303147622071761943862528322127892562049587159870698277284969834472842866558946614688455397113815841316191016285933701612613557701496540318504078016596956916502034378780159700225878475246892967745004312150026393542050051147282469246183038956466525168220824668490413892274959717541101941444655222665801661194162337200003455151924508726432434866442029891656463470654153546584415404648227143680*y^12 - 394956815397940126330636639394988934013248620735124538413586548161229989498754413490668877355001684291229878330267565424200092510928776006289525859065160859576020078343748634044835623635489972620640063390211600272500025332091007290476710679934007153331946379530660520000945370590989275596010116528469187775893858961465983529189037157068102957473198904828632448576501948764751214225632556107195531830730663151570051127276700471914203809545675477625738298435319086131084452620994013001676079571850747407799874689717559289694847990073814193562255487/17260019979618227961868071375164683663292438218718588292796899944580845662826055396913049407720118119215867389022405288090938098108044657386963405965535938575786905517940485965632080531973140512396789967674569321242458618210716639736653672113849278453960329047754071483425403153389425374135079626019504149239229125508594695039925056469618811723241936251078037506598385512512786820617311545759739116631292055206167122603473068739929385275485361163805666450415298540584300000863787981127181608108716610507472914115867663538386646103851162056785920*y^11 + 629845051729425132824755627397609341777552961549914314864813270993474783122195797994684503914929288095468287625738078928237872310978275738956692760428958189244849182932572165163296551883208763863293652430795189122240808838200813401620828848129087269221728451923875409273649584336090921590136705689361004644844124869259066007518245977600040375014906189663190353455427572999630565425734278709630518233421935881960619316779454762124228699228889667199351103426025818630109365472690481937315500566680443449116626882157229046783135273401525291597105437/17260019979618227961868071375164683663292438218718588292796899944580845662826055396913049407720118119215867389022405288090938098108044657386963405965535938575786905517940485965632080531973140512396789967674569321242458618210716639736653672113849278453960329047754071483425403153389425374135079626019504149239229125508594695039925056469618811723241936251078037506598385512512786820617311545759739116631292055206167122603473068739929385275485361163805666450415298540584300000863787981127181608108716610507472914115867663538386646103851162056785920*y^10 + 10932029637848002779267614490320913927432682258424263433619924567711866164260238056946324857247389111899795894631303007789380258883355857896441253934125353875613693097861013938259087466604847303603277181185094048515206409335428329837889175623253662255389259889323048635334268889945981725125680756687767197577506149549242836855173335698254653409796956381352843540166236832703145477813291256466801453478443131576201734766738773878445989204464226892310444084132437011448704655292737498397519414646062584903587397947474193270532399938225412564896911/479444999433839665607446427087907879535901061631071897022136109571690157300723761025362483547781058867107427472844591335859391614112351594082316832375998293771858486609457943489780014777031680899910832435404703367846072728075462214907046447606924401498898029104279763428483420927484038170418878500541781923311920153016519306664584901933855881201164895863278819627732930903132967239369765159992753239758112644615753405652029687220260702096815587883490734733758292794008333357327443920199489114131016958540914280996323987177406836218087834910720*y^9 - 37777499534733766384345258293902343266702894705206993753423063960491405569267312442567084773237195231289446776699736896287694058477963194620528672853712784196707866872367533706796092758120541561468974970138479293343069422857905356615949071210114366812097334741804397352194041898309422153330252670053775169794033080695950978190241829414229229694180529889046587501833694008629893852341772373737749665742675112540087372842635974228861447306860986120982493730069213728143488157445547489324580664556209653478019094989123266959584712696355364008832627/1438334998301518996822339281263723638607703184893215691066408328715070471902171283076087450643343176601322282418533774007578174842337054782246950497127994881315575459828373830469340044331095042699732497306214110103538218184226386644721139342820773204496694087312839290285450262782452114511256635501625345769935760459049557919993754705801567643603494687589836458883198792709398901718109295479978259719274337933847260216956089061660782106290446763650472204201274878382025000071982331760598467342393050875622742842988971961532220508654263504732160*y^8 - 40754659618462111243063818415050509969105379133429351887470776538778806698577281129181053413943240673544965477140171067536100035111253352273866221087875712982656164197374967186792072296437187456061595847003215546550771876232637233981419131528612974182285181005941147130489515130777844975141130231222552281274384291003319400987286032465396276759099055945985739942545754399406983642323846315011781417618394671088442502699199460908267285294577049808869996475490429726354441802837345019161759322252598921556256023521937561872620209493027717879405221/2157502497452278495233508921895585457911554777339823536599612493072605707853256924614131175965014764901983423627800661011367262263505582173370425745691992321973363189742560745704010066496642564049598745959321165155307327276339579967081709014231159806745041130969258935428175394173678171766884953252438018654903640688574336879990632058702351465405242031384754688324798189064098352577163943219967389578911506900770890325434133592491173159435670145475708306301912317573037500107973497640897701013589576313434114264483457942298330762981395257098240*y^7 + 1789877975312762952929164830732123081300729530933853946225935178816905694222558061142310585390821918966158338095975577013717270195009589906995980307368477842388091501814735575212176259321825426894842771751584923588711886434064800618198753239981136281249012323772522166904528962122346228199145961881589208113423983554143544806035906654372668601546347936347631614892152952488031142526890436599138979111377365283585463075408506713895174350830009008565528716191918582353920272897077021487544384234879246215962504744304658502430615161928637894974733/269687812181534811904188615236948182238944347167477942074951561634075713481657115576766396995626845612747927953475082626420907782938197771671303218211499040246670398717820093213001258312080320506199843244915145644413415909542447495885213626778894975843130141371157366928521924271709771470860619156554752331862955086071792109998829007337793933175655253923094336040599773633012294072145492902495923697363938362596361290679266699061396644929458768184463538287739039696629687513496687205112212626698697039179264283060432242787291345372674407137280*y^6 + 2602368214060901340602302836154918461638780443702273510595622584677431832820419791941897281207367125237388312241578269594116081193219442256602011458205576841410265152365063142311176900506100884768986106987069298187320829486429942749118050319996592729146762988188706355375025398183588003104086873411184594772224834660489800758829446249820038103555953417708695041281467646089508165785023712254231539365735794509711613365813878895281242820656604615886151475015233370175758875954515020455137133572279456947789523282320338016764557156953544865315997/269687812181534811904188615236948182238944347167477942074951561634075713481657115576766396995626845612747927953475082626420907782938197771671303218211499040246670398717820093213001258312080320506199843244915145644413415909542447495885213626778894975843130141371157366928521924271709771470860619156554752331862955086071792109998829007337793933175655253923094336040599773633012294072145492902495923697363938362596361290679266699061396644929458768184463538287739039696629687513496687205112212626698697039179264283060432242787291345372674407137280*y^5 + 467236166687823490572426668946365972948159152448303348269563568274601601189051898578275197007999649732768507943824256040575518988986036416250201775835576131972420214612126580606431988405382282658980464923139405139597330580039188094812559237991363450369318237488160061758414248047095670457634432354644144027646648834022942526728958294026472531611270163057800923652711293484175542160144218428604691129185820484908909407314776261475016516643577828762084849262326482928874463295280497362526581626111158179565372792547949379056274905989190253251239/269687812181534811904188615236948182238944347167477942074951561634075713481657115576766396995626845612747927953475082626420907782938197771671303218211499040246670398717820093213001258312080320506199843244915145644413415909542447495885213626778894975843130141371157366928521924271709771470860619156554752331862955086071792109998829007337793933175655253923094336040599773633012294072145492902495923697363938362596361290679266699061396644929458768184463538287739039696629687513496687205112212626698697039179264283060432242787291345372674407137280*y^4 - 255308733758131403787190798892422462208731687212945085291241504364670884490476987490371667246283372632145513655393883297994388188186665196437321759886190347001105398215113358487080369674290422533060046475295804263184412293846495040350911043955471582514630517252724841210116396994723711725183558099464698170362786331400100554844781003078776791253767261121452918436140439992748151481539421635151152939739385488244656848902914612074894684538170992597527915389469371073080624351131436596620874127779315764743918748627382957095526198590265806651899/134843906090767405952094307618474091119472173583738971037475780817037856740828557788383198497813422806373963976737541313210453891469098885835651609105749520123335199358910046606500629156040160253099921622457572822206707954771223747942606813389447487921565070685578683464260962135854885735430309578277376165931477543035896054999414503668896966587827626961547168020299886816506147036072746451247961848681969181298180645339633349530698322464729384092231769143869519848314843756748343602556106313349348519589632141530216121393645672686337203568640*y^3 - 59584349872405071083795604505390485022628219538343555146677398958965995772004599814428407084156791679914752125206610288580007423341372626452669230488094539261658774446548953183172772358638668731343547121191843232181864543180511467518780759681193060743518971846898788646304037914864614734394313811664047925405286855964127625380639244687670241890874674939277062107912527176613937319454202627236960176300436676480993255092738058805794311701214272758267786206882166387226605569820890229093754111122130335143002676775027214367094396054834354003957/67421953045383702976047153809237045559736086791869485518737890408518928370414278894191599248906711403186981988368770656605226945734549442917825804552874760061667599679455023303250314578020080126549960811228786411103353977385611873971303406694723743960782535342789341732130481067927442867715154789138688082965738771517948027499707251834448483293913813480773584010149943408253073518036373225623980924340984590649090322669816674765349161232364692046115884571934759924157421878374171801278053156674674259794816070765108060696822836343168601784320*y^2 + 1277976880659916588411235505237149549360200069703423115773645882567560609324819159810255424379221446678274433337045516797506844646009997260507847868970662062512925439468424437461850782638601578496626094145246833514200827762065150791523830982398378858220277881778756483338401938051228324593277372662034263085695635364889419173707241309581152642322817617504684081534339986081960759730792570308892264296686429994801100819941425322143956972976420278817544328778360012418628309551276590831650694648450222153409788741900446822365936078290665939/14631500226862782763899121920407344956539949390596676544864993578237614663718376496135329698113435634372174910670306132075787097598643542299875391613037057305049392291548399154351196740021718777463099134381247051020693137453474799038911329577848034713711487704598381452285260648421754094556240188615166684671384282013443582356707302915461910437047268550515100696647123135471587134990532384032981971428165058734611615162720632544563620059106921016952231894951119775207773845133283811041244174625580351517972237579233520116498011359194575040*y + 137851193648393249652879233066704163519427897662345955675831726128005771516017127484713940046585196104033342678741770687660457025203538932187155956989067700147276872620918265983027477127265968577509945647203570377323310307857706884305340217786782031326842528569085620844559882865253800606885171515657129581154153427860855635109142628727367132565742670828725119799407088027405703134899776502076031342367328125121137804433250941257630049578195990031888322980929264543672541474939552906695213525479423555221643566317672989833018931102369072437/1404624021778827145334315704359105115827835141497280948307039383510811007716964143628991651018889820899728791424349388679275561369469780060788037594851557501284741659988646318817714887042085002636457516900599716897986541195533580707735487639473411332516302819641444619419385022248488393077399058107056001728452891073290583906243901079884343401956537780849449666878123821005272364959091108867166269257103845638522715055621180724278107525674264417627414261915307498419946289132795245859959440764055713745725334807606417931183809090482679203840