# Manifold: Census Knot K8_21

# Number of Tetrahedra: 8

# Number Field
x^40 - 23*x^39 + 101*x^38 + 518*x^37 - 6348*x^36 - 2631*x^35 + 102765*x^34 - 98775*x^33 - 277318*x^32 + 3031021*x^31 - 10045023*x^30 - 54242865*x^29 + 175158427*x^28 + 505126429*x^27 - 1561051910*x^26 - 1452570498*x^25 + 5607155870*x^24 - 881523848*x^23 - 2771072522*x^22 + 722421172*x^21 - 9993072141*x^20 + 9990729804*x^19 + 10595322199*x^18 - 12578087488*x^17 + 57653448*x^16 + 2715305340*x^15 - 3565808469*x^14 + 2083018934*x^13 + 1375166904*x^12 - 798665963*x^11 - 121918206*x^10 - 90259032*x^9 - 34155224*x^8 + 79323312*x^7 + 9920832*x^6 - 13341056*x^5 - 1134976*x^4 + 895232*x^3 + 73216*x^2 - 21504*x - 2048 

# Approximate Field Generator
-0.0800258359762650 + 0.530104599869854*I

# Shape Parameters
-613905837064739574460269506125882852948975440618554658371796992273112904818363819601595777268526150016898342991746065597112509598864859012243449986781484842420397737908346024250902646541595852875089851990825919047355/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^39 + 28584318776068499282271030422909913860852795347665028910425702496516071392937884997765108886814019870143037754259720822346004750728313530290355239432494353415898791841004005085080038482062011358266764747984570239710323/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^38 - 33075890791664729949125323908967838230019701149027565417282312486864652599298262178772219360029479082395470259902823530936079763589061380038632207349695595898633356184029681539478473303856024255510978429425103073568529/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^37 - 296358843874859123454619229195337485834736789047815461878195818989554515548148669476317718262363286616480537019584317464091736339231175363641721913753836514880934713806663616444742656375112262955239026763340902203776587/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^36 + 7934885089019115734973975329490102585804279847876588796888831809380144435447049392426002693344045191203885390140709438217893211473985912143397062091002348102596924938878018634300136488971401814256183660895375361826681927/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^35 + 13393551858621205823860689878212675619391088756634544714831413464179670706747731196021037328473342471097288112440673311217382259588310198271766023080467805529138454011013606388431157137271801471061161415221024183687727/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^34 - 124748449996494086068777147546507777155883087564152777511284041379346585805758881997464829546204181522316599164533591544848717566385954414602014587029523486502310575729502166935012230892815859658175557981560579217772411405/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^33 + 19681273467549240341352963755225836051027621370149721780413445797439956906159271940485219142450948497889454306847701800364993768017518799816901172007233849511199516043231811918232033688070923923139703397942931942134836545/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^32 + 134673238537725556072003710923025899471260819703356828083366036981858166089289140673943067464568773246543611390265072304603054654243021452705087953572347042912662956040268607433830444278270914531770932010262517247978017349/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^31 - 3777956691168540670857572184492432848477028505131696888624039784153831339372208925997304354770042712377803122241896328734625916435022476488572104915737170504779469865788492557263710470188091200846553505806693901811420879015/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^30 + 13465817152317767885399675206648909882776158234316620239070128659699459979675768767935584521874802210856667088833440227146760716999876068147541651741309530936409305460899259129473921659217026923881081835063792545582329275557/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^29 + 1938349030465985784707533295091066641958036932472702864952116435402470921604097904960891826248249492121478889252363866183867783122115408336582229621105365195362754514260180530074344098935611515910203302641717617363836157297/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^28 - 114980732091884878579393760481441977113398896692361069998715958160459230016874013448301996005474011047398407666097962574154459522681199625219362352541003559734279009526504969790256101084774192039694786663123195925606368737917/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^27 - 67559779401674631889539725707844471749263829145277239289982345517440637639421934750648951259402331922969577938489877318135563636175274148889167412868050477582987891187357364263367066767399073701124927139123946815095910687221/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^26 + 253279671649850215158685681537939538088237883419178683422354351512096311203665894510229331574050275266398767915912957209860278289022316789375897949396246900706793785509549225106262020384163437022843439695296862486100678709933/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^25 + 1070373973184509135441422953588035141991381398479715837395758041288532422856204503454753581824890130720573087026205595620007047899276568371963459434074980751487671932057831234741647327529108446318333138000970266761607534535007/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^24 - 852333730337592089771731246881137171789404213007488029118622438851015568866632334336420078338146493511991222892093244563674479713536173339008772467626703276785432378072175015988920683849732727952193722785751467114293681789085/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^23 + 431435627778922305603836260408703118105305529123355024781546028980217963457099049370445524353013546648953557848918415955779895664628215515678530422532221935634649198263240150456304799659992152388108317897890891934465279790703/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^22 + 585914177809179241720214310358662521659895567003589408316393226274159233882195585145921017132168001518456557451603198364228003391449916456231330469275305837163781789451672540103982333476972725758017129563129658753568386453645/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^21 - 604074468910326798621249513589418622284124549954156439916952175456188386038678529981937363600116876962267242717198663861407309419734173530848223498165382769716560368611639506946069114226392740335829113531726834221568968271273/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^20 + 50528719497475454037145512405666121522790351716070317949274899430295720871113045747891618395734630074888808826311090949252910029194753825543506439532619452389788763453228239546560187996724984601512103932396384304546365206315/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^19 - 15966133290268881480134351379560218505321331957917235776997724010113695815278539414833801417006510895218749743544596239469076745955367138010877886403893871000418487559150664697531707058281068801724135184799667352171393031877465/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^18 - 5723055471315288861501536435209283016451738790310092342479026664985934716533274261803543511861635324190918941627171426695807261426652672761978171992431720747039858013365072988014779676116310947610248239378511427142315935351419/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^17 + 15140545978249858778731927177729457426746691316724178296844985114314705224173892885211108654442591344571076452714408223693816057073999255385869313540134012709680815931261922260512942741105058706968288247062117435560812552523003/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^16 - 6840082252736016320053625381481213883475965994380143580304850030080431332939666157906338284822204413475629412319310848765214204834391229344408731409496224675427856451805063588833016512602224956616679731423258493953216685328237/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^15 + 34629140676924547550474170193156623571390444055516887204359639427177700704188785130962070352041494558260029503365627149796760449251032606106084797808603831875936525968277236685703761127488043289559360165331956862275352776717/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^14 + 1994219137981886720839991329475124721900446051843181626992493660101039837180281240721978580352578925624337021121736877019774561291444393827421279900406532682207325319114807200980140749963729648299583215112566225498836361149323/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^13 - 3762394894366230340578091461284099783265454040852986390580677550958277251438381444342920907136799474603060405856733499380157020137750841807624411185184977611765977958363178694408440857821801063729575018636643484688120040396757/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^12 + 209789943151642362472973353456673641929191341730007379997612051189634787969765612084938204046795408574210903077468665050436846399703294952613216071011864086255386065473857582215583760141553209951263353998322737473026879079865/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^11 + 17942437137376641231834292434939959427676571316903558513285437514811140741323109013384035166227661299998033705230710596028234320323920743779619812234507377129506549122287299171468344711071526699545241382424168367381924717939/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^10 - 212488686065051544305007960243528246534226252614910432936406831228377786986732938525420172302959256105749091545822329242908194904441681466970142922325060462197497113854092344318252554194995478682125132976356878231981937972115/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^9 + 191794527043105493151686135148620036271229687631694133451944244537406944998182616398852024197471412976849490839125069650432921054716810140629388145646546322670187610247346356755656136549709119309256444235047731507367395917799/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^8 - 18554687523072766951497229733363307953366044829819293968382565942810568723433623452459728985097579679942216595770949952260528655812586395016892236401286723253135927701587806271082274091286406754659863889119518295170489266731/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^7 - 14261771104058693660512199597058984333238839090532674627564343603341832440532618351534299187339777005437678935433141969812241050861895847975332659537260507672104238756703341271407069789146362494901591122426840152165544310313/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^6 + 989411599908806761104590701592108082857990116651794962014317024105601934079254759770274557019478749238235461450037115974241946070402252019305711823722216359382349913326194924955337202270044356665225582302452728582297173709/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^5 + 324210121063455988319469256559827198362542301522827929076676106386522206199606038554753191940059285828269300096265081903798740113814109916395515237183607023687114131250558757388810603148219865044726601470955683826028015631/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^4 - 38200403974630820249029818041296346392056211680801498229210109790835340411352453960158556110611386111066129875244655133437115003613665010109183903510249730035722864594337738296463227176996439336928822281385304397648807779/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^3 - 1587697146130399850007916934065793415537242798610734596279604082037208621335860302683149733306249953101283388551698505147155388561886471111466560651438812824240862289235829687163413337102736602830591470312376089024903813/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782*y^2 + 155822641525587383863323523553094525245341086348165968142679723568668688286331992722849346007145941988759076393378433486740729907012773265590039094559986006311970545939797472406732042330354534759570889797374760214728653/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782*y + 6616406551603220259929392600238094445679523692844002475439826272369902349227239825550074817927181318859558998828167072633152308622646156267470621076009647164793643498521902901732587115012779744874171479584137134600978/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391

-942435726487882462054205991981432109126825859760143685249873907472805121871571484641832070358632922812191286721093565033416175943233555811565042230077140982241855765483262509572581262373730407736727278023354291933353/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^39 + 44397143129539711906069148471984621980931376931750271799181487201582797979940606263238672017029215275032437142367235624504614380303897704087808431508106461515603084054147522135273963389540299296445152554505507860637213/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^38 - 214682719780714332988277157628532282994876030176091363179841040275643821393167165386439945633421314172695634270555030724305426380551898542264313645562156552031995361824762561275171558541963008452597593040203139680583979/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^37 - 864386726747380621705216386154678700437924207618886312937777287937686063784511673212112787001640535345955268325525474401111645565577621564924216852607060665893888118465948321538424394326850173374129774370980027555103113/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^36 + 6237915261364555935780811194588861776391595931908569469459570938636257427486198855534498486527515494710516726832184103678024016855818235481250416993957140575175636918200998977894897468705664025939654112692047486160072193/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^35 - 901478344636218182470023076840242955116110797770091785760061668779297817443402061023039558963817654662485300352173252222899290443063155641796457656389291602787290311094850534696937942132524938952454673539538791245961503/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^34 - 194645963860110441498668298227932097735743864262721743207775562690775688293808853754813955479640139163395856384992087965608104582413471164135446559548436152961967369849254782310034982283277931322109995467663630737726208395/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^33 + 293444077111689227974094631959997076006997609566381038128829042759489451165962179370933756572305994984712980437415131497291848631528201444470610121546249582639085544325265307571542325329489820496029267206823747514447901929/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^32 + 391150152026776000656181008441435861097796598145960706981397884328893108499078490066259272310268136598182495114744319652451892267813733931296140246210881319784044388577845851062019559234738548733835815800998684797749167083/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^31 - 1490565768613687916642695407042091740055949305536054930377054019819993994203734946819820317588633009513622482342455886927083180629946348824048367151554084081247704741593326850849834925725517090771373027965956368573578254725/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^30 + 22162094836664250470576872966597823980474754182537914820998256422058887049495125785177467892377245199489004257094793693532746016419924862790320789502293436797289639239175880151752404267866118656043366138990057901684994317369/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^29 + 90880362012952009651213650963608617194315111001681104874465932847312398230450264637140845947540437777402097874660722614113254267163513684572615976813614354383072201889606467521909160436915721131846553610604948474881988875617/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^28 - 383686137101711773233734553196092424566720412955272403545393214100794476171585155141923942202003545570124312566457819569001044344059984478960476697990290782336892245043584497368841193695941203056111650966297233330810514335213/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^27 - 755604869722116986860804248765135094942762003483832523156875132912886134255386769149083836255710175828936216775864081943578134359179279934069495295223537090975503542756995195271905207312497297376764968160039251033848379195909/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^26 + 3415392952768370720536215477311769669007206848157071271555966310638373960451371942417950850929570661729366939022435811098156085077658175445211712023863573925050671524740184447018568814126710513796082157426439460540412043381663/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^25 + 496242885617427338040163009926845603949419992117907188634132587383671337911962558731807154280456975395763314025454004365349082059757939278507576081766318423855613478358820037615908206000768415641357284853142348847387065237197/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^24 - 5798345474724581316278848923165587068134697963096754266115473816927028542589235062076753187958788690733737009997680467912722477359121542850206635585670464534384005329274825414491491097783005109679238229427797591394568596562377/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^23 + 3852146645385328674964812165343913419959645359452452203360479486335307532804424923187464465002836527108430362432477692068873915071750557032162660404220321418822879896166707747535182999062425552814030389120654885383398433791149/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^22 + 652788497696043162448687889080540475049683496391413690333719762527714419714565434668119295954262777082867734744260622810322274139448029023239797765988909770700648357305509991421470747743428196130663497273057416886520769201355/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^21 - 1632080903193511121451471926601169184383079263876228699852050133556376188436321535863546224324932999027795480356403344188188195653248337078339081043494804878290756443957665508940508794911179977006657598385845838107531321993367/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^20 + 10051065521343044775952217217039154316028400215270736633439470833978879838781725628756533955183819555374895366020933643184637539298391176410476599918600883924849262125854240599327630461575342304088399656752478346556936996271019/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^19 - 29754882134073214926043216582035519179936238757315056403948298475322239336475820834129475070645512339662524051967405213564443101598557887807336054690540211309013533494809517163813891095646886590147057132109964796451752632475819/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^18 - 3317693528237215889847581504519134353565043323066825934784931140516294451576498871092275383459182540084726287957750341957626785147312098104191482684714266090831402709326130537820275547723167483398786487849239873697749868950297/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^17 + 30665973389273461856562319413102494963391252738142385435180866668614039589839934167764093050728310998587158657801175669693255498421377220693385218474379322617700430849342454287353601189637659819433165803367849303315644017602969/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^16 - 914648514842665670458760208904142149663634365053469081369963075030597997144855295717964743106242234277872880251950462257910308809604613596050462555547491186327486898179879390161690688849888650927885269451783426582979433609781/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^15 - 4171367359617531867265729834521245232302210819325970719542793851569439991893893174947051700712467361126373118185470139632953336036908120524691748136795408684240893722533730545460397832782833143118958894232442543489080297327/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^14 + 3877784895893856997871731393294005019686137451986849690811053440782277392058177021785090624886324967083120924531459251900842196629904435965275908845415332057025404062488575640842304693734479537964890435818008331982398897768379/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^13 - 7964800263238501749691992902248676414478356561230986182710797269877759010619819595439532141291139936579928651167741002568625743512710203537319416688672841758447416234672823222998672497766105820051450828210736995002742087766919/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^12 + 392180683151970239894152366623089484956522797542264536203182516174942827205987910306781162924709862554779693122135889690782472895700736613090728060816696716623940076425485339249648052687459044531932305987176849251640787631889/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^11 + 912810528179658234320722000091226911239148977889855238585139777584949474863033813784785111132555305626277829478763727563204759666623877161900531520094967973607582931981520795831416331294113064484625066472077140113341142667207/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^10 - 589907000348151614371489832966988298232873889212703486163206170188560574509976017580347617802829355269165181540331484708647008805913619703179943628969811484331935182519640598026602368642057811143240149477811080044817006619265/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^9 + 170742755568184622634616971169383682609169326380167842068013325320312657987076700092826013684787669723363014932773036314456627730380038792871302544457676522524050963711485127192633493330092989746714207389979906774109498021523/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^8 - 13563182025977914705904729522143086594722282456662314775209693944641973354863909303538754596085716272713031394413654977487277418623105855335757013973064554217968225303860101924103680201772565952889263116383388249967633730343/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^7 - 269851966618691301353512983699963311097404237263233359980000043632275568838418621043713606284537342043027708019517193446979765399453012518211129140082936483865324593306456105649068808066426298045399769456753168127231016239/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^6 + 3323804943856203263135608847854473856090966403562833202267279513019201526276760721617311267185731251192982350541124757322608164637003755151797343584440828715454320373211622972967695682256383480410485928141376640871851793993/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^5 + 401417424354655239213502897947334235963319960046058501605741026963605311915989144044584091999890423210783131942054149512667746032729381810673295847816147858736170077928102731328300111542962326803812533046558671301165851267/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^4 - 38018312690144106752154283111029606847158288016267754357854957972877144252802932367114568336685730910546696533503990184462306774529846217331880453166561022890424562240132931874138580046799827435272407841038728551407360797/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^3 - 2112315025350736696211206525349489100733140448300201210815921412123979847022233447808261302760342506038421776973135965948776035804145980474859997798232971770893605877034283953885218231003318387361529412466698957954400117/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782*y^2 + 256924463807612534503135609857560302119055113346851701844670870804540491589428877533190285487182388648255223225865352589522872260668626127778549297709982301151438555418553845939609801292970329101473202499865783812759915/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y + 21899283774965974253994104618632923225064336114522113936947750833033167081194857517542953064112787326201466698392488917089620006245291052715488922104095871382196531085785119376340716554993500833001775099664280497405431/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391

-246133668749284278195074275756975152947687569668201652967723220574155031257484951598273963211958812780941790693902725371760517669470360324850541479317862832421875571893269776569476345087538350638831571175446575519452119/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^39 + 706699764459382978998183633277600416044257100907174298167750431746343544289267751988786684953527972556444874005075679795233659629412381793943652378632685062752587741072517306797675100880616974891727573603658089313590087/20878446251950308809107513232455478897722547953623281458288690917826414391957738385524601523470319518954780268716869197212483532712508852702539815629154863060383748745509826478177145285537649300188841493199831696551871968*y^38 - 6181620757445881752847453036310620302282686837700606839336128294364599367506790168143536455709417929572910958137279159795044568356671589060394011467237798650013126373622605947105710175015993518635575439534975832558296345/41756892503900617618215026464910957795445095907246562916577381835652828783915476771049203046940639037909560537433738394424967065425017705405079631258309726120767497491019652956354290571075298600377682986399663393103743936*y^37 - 127359221518977786105307510603791102556026004915052581672480171843441210323047604648677640214481673406073035506982466814849003736693697125593905949111214693438397520337028938399220030153259066335616127689447704525264361917/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^36 + 48584352241589490202783357994936128466704120052274864409477431369482418772405291861874474367201056264910265702805921179843509849189060037566721599846204281394219703947795833660908371308475180100965937289892762459498365201/5219611562987577202276878308113869724430636988405820364572172729456603597989434596381150380867579879738695067179217299303120883178127213175634953907288715765095937186377456619544286321384412325047210373299957924137967992*y^35 + 674799170861792278603192035942561289167293122463389420829757412327994416373755673776927406114994077827959403667232206805842360763197294610675134207710938542827833884805670830129794613339370048756854404535464248697724453863/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^34 - 3128640343618336872735238433811082848091655972283597007359068481604404214949744571392244023889009623060615456427649670656603051271839477040899896022331694170299819404669095745231880516182885008979827936472732106322879650361/20878446251950308809107513232455478897722547953623281458288690917826414391957738385524601523470319518954780268716869197212483532712508852702539815629154863060383748745509826478177145285537649300188841493199831696551871968*y^33 + 5914367522260276029181391616265088077337716826893668900909850013625843708248424315470388816110696628165283819304188065587950137230236023444151461995047307304270110457320170357303508208664413233286954471558909913473368570561/41756892503900617618215026464910957795445095907246562916577381835652828783915476771049203046940639037909560537433738394424967065425017705405079631258309726120767497491019652956354290571075298600377682986399663393103743936*y^32 + 65049419143817635954653601603988976826433163489902308073630366161859467675900645209144754141757846654672139186631550228763406389278029821874292549598705124416543070477379868006409563288065510671689859728049521983265687735459/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^31 - 740349071078421434420795366897063974254237956291101302259783734059742078481110758357490878177578601604013196462239646240369438160125693944784892114157794132226106178584054866008537776473345618594103712600557362594747596650603/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^30 + 1230005223033117925296873100603045654978107869277485578041769155306092722057724975536283756122398018322314369420993927856574014385842553887856437253635765844973011855205852167889607163213282095075235416057543005197749457643107/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^29 + 6654771776326072877225979026703778493563993577196799874120991922952336908406587815136477521000440740459802511948163503039706670756663751762925341407932023236198310376724067280792025602473526980995980129949661627668038201632973/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^28 - 21160507055640858785728028276799411669375521045694634584505627012501920428650700783095760806213887975913993237964205408684083482800475378263804719089205421232339817453327268997479208168738232972603053394770614632677164646232161/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^27 - 30881205127672420264265237947546353946820545792233468220088598769900153508480704961737834240679929942153783814150621875950995463330127401532136922723054284267861892046172276747813092688414523527195524377714552513867610269382323/41756892503900617618215026464910957795445095907246562916577381835652828783915476771049203046940639037909560537433738394424967065425017705405079631258309726120767497491019652956354290571075298600377682986399663393103743936*y^26 + 373840402516759719329341791018831828586795435371846934821915768642439414503827314794949494322857124574286140263411883257068574944228199001641976393858874521251113668156761048888656306072047861625027057902806074764594485661791811/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^25 + 174756428715291609205870880039928962192326027614676744395471248086875295922323359830258452512955602508430385961334636725507158398116235874838959797526347491283747747274968725225467208351897134456913661114496164140716668053204269/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^24 - 38560319351026853332954565223586929334124167378407090204445963005012931511557883603990286092821925292665794629713793054707372862496501296143452994332468434192772135599273652152923234907119510268354848884842932621790025211023987/4912575588694190308025297231165995034758246577323125049009103745370921033401820796594023887875369298577595357345145693461760831226472671224127015442154085425972646763649370936041681243655917482397374468988195693306322816*y^23 + 6812054785480610045582340375696447755863824207920341346282192520719678997182316644701686913244568071726029827562705609497873387250525408336809153217557864870899717311718482711772140264214666472714701558991169490662535851114339/4912575588694190308025297231165995034758246577323125049009103745370921033401820796594023887875369298577595357345145693461760831226472671224127015442154085425972646763649370936041681243655917482397374468988195693306322816*y^22 + 14290772688592327802638453852432773902541616079550631026677534343566361675419539175982006665090287829734465165545301667227891872682504314266956948117940701041386676844311309441937151728080594382325244115481493727866115006618749/4912575588694190308025297231165995034758246577323125049009103745370921033401820796594023887875369298577595357345145693461760831226472671224127015442154085425972646763649370936041681243655917482397374468988195693306322816*y^21 - 62890680551946173086001499006407152269716760039128378899958671075059717300346993864763420531944028935184663574408724491656967609643376447473283053436349953852208775806651150195682379033431499879917551414073035439010808374790571/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^20 + 2522079942277426398474992259877696236063389404102291486889390943824011186804412142619127427306024037475578195827065086672726181308123674712682414259026656396451426261940219157210133864290540540894663549733548648410208970098916919/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^19 - 2398328311356087178390063503518263393128670522746577417697980800759902251610125837654234913279985457576625017678463283864743486407998013490702040841622607163491216665331558921278436716322404580567579453761366010775314484617011379/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^18 - 2279848609370440234684181554189318858568257307562093517907585022361827675420198191819602513765499208895739217969838509839143347968796730878624402238667026308743336901622865774180370082209967136599704906527007623475929795049471285/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^17 + 2651314511504861430163597793046771160131553625327819562696405296308664444275212028844323869967976832763894664603154613901239812806173485467016014925523853229414993027610869776682074489971046856575429878566979947067655221745163407/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^16 - 34443192321296227858708830856148081471469473117093642733219726807046935568204642162026765842124316202990238956546802447741479335762732536420601892464221801059466673497192316268778060180161291350732021037500282720122184349454727/20878446251950308809107513232455478897722547953623281458288690917826414391957738385524601523470319518954780268716869197212483532712508852702539815629154863060383748745509826478177145285537649300188841493199831696551871968*y^15 - 142082362017550127749839000286307101509942482796994627658070284605732542613721306621386062173982340908439546074247721491929119339420365225358487931868224413663620258899986026471871566821731282073788870841227704366553782182657219/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^14 + 812014475121978343733841959919950155570921137220432272880788985099887654682969929225854371690564554346053886454261182763474310919583838498737634140953470007190550577791824497054079718163573141374157991316798406909762499891062943/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^13 - 512479533037070992334439896923176972066176585707245318848855525555834117276276042044147866904375625330860976620179794342005791649163523403812796075137178033003062976201610648798201008501678988919295234532045721335241135290794157/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^12 - 114974321236498470175160483951904788837165471460169446726475802909498374328138284165558344095721975885300143656538492286257952876182415999022476518345263571851580191364406102824723199273644545316479647214056723305042077529942739/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^11 + 110766626407250182344749981093561137163112593112763466126933038815877190867779053415246859901604955784265531471743770766953398072182522870876546207523702943151652816187145057548337478615494591003414508929678179838408168812322979/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^10 + 3104041231324740357623774522116402279279269969566405091758276454458068985334343794290014348844307029393275847901556013282228258519328497695554845227210198925444697541801499887361958024851949951795864459167999984399879623187129/167027570015602470472860105859643831181780383628986251666309527342611315135661907084196812187762556151638242149734953577699868261700070821620318525033238904483069989964078611825417162284301194401510731945598653572414975744*y^9 + 17470620828564219593077689061234057629065948744046813793085022128583512463316209674094108722703367492372893300496736881789575700419016113816443688646705685903231322178401858226929837579972473079779174195677527290955134993595595/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^8 + 4347601680595895010360469469249074851316494629277728855667417061328764733873274201702622053969216204371596032290529971271562340131327273877297181162973662766728980835635921467848133173163747350131149862510958645693791115064257/83513785007801235236430052929821915590890191814493125833154763671305657567830953542098406093881278075819121074867476788849934130850035410810159262516619452241534994982039305912708581142150597200755365972799326786207487872*y^7 - 3376529919979511952167741401693672358268081548908115601164909022492029735930406154268711230417411906961154380440017225597767461878379833203156846152850620274086721147930412794700166966396942454380290351055892822724402854026527/41756892503900617618215026464910957795445095907246562916577381835652828783915476771049203046940639037909560537433738394424967065425017705405079631258309726120767497491019652956354290571075298600377682986399663393103743936*y^6 - 50577427622876477406611550000819635246660062229252525522410396454509851232593099740998870299245080687503554617515144269140000965058112671221853242107802705437773152179522227926749158920694697007134195708836577754106543400779/5219611562987577202276878308113869724430636988405820364572172729456603597989434596381150380867579879738695067179217299303120883178127213175634953907288715765095937186377456619544286321384412325047210373299957924137967992*y^5 + 91528163648535755660939894205961385423531463825012223828720863074205373046110476752898190893971907255913050768879477337223200489538583100353220304933986719020053441283858841701513778250501010326856440870763877173674874997763/10439223125975154404553756616227739448861273976811640729144345458913207195978869192762300761735159759477390134358434598606241766356254426351269907814577431530191874372754913239088572642768824650094420746599915848275935984*y^4 + 3723447269335169381058959904300573813987344507063253107350762647221971448284266118627369294719549522880612146588741254478987236579758094952091589995898479771027894502974856631546639137647155359587008992356149050555174683359/5219611562987577202276878308113869724430636988405820364572172729456603597989434596381150380867579879738695067179217299303120883178127213175634953907288715765095937186377456619544286321384412325047210373299957924137967992*y^3 - 212934195366406419562000609708401188458299568169900026545745813336715295409400608083538522332454787753152153382413536509672942327502910946412433925542488000445019921494562461836121768360731086707432129559866604565845874717/652451445373447150284609788514233715553829623550727545571521591182075449748679324547643797608447484967336883397402162412890110397265901646954369238411089470636992148297182077443035790173051540630901296662494740517245999*y^2 - 26548348601391484975605588787415508176198830100869341214293394975325110308877620089792404380435849462128522979062182373073837347316980262267590194878775801492694858257932759613440229341374736090141963951166526862492966643/1304902890746894300569219577028467431107659247101455091143043182364150899497358649095287595216894969934673766794804324825780220794531803293908738476822178941273984296594364154886071580346103081261802593324989481034491998*y + 779544002273475991105330403670316683814589162356356801864200118784300867729023429859416456466753129215574789202772734136414537941363397499796480360272507987617760338852695977082337158863557783681550515590566938113474560/652451445373447150284609788514233715553829623550727545571521591182075449748679324547643797608447484967336883397402162412890110397265901646954369238411089470636992148297182077443035790173051540630901296662494740517245999

-50126816265395637270449579518973876619685915522260373128793284773910716904968603186855301624286792556217359566121483627997620781116343959318860976948187580850349282008383889410799086754579722159999874417166042039214779/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^39 + 289103522230352097561191246539233318494345638032608368896084240236779825566280221724775011035509675855447067315418821900978905349049726317213712794885085438039956481082710054491427953557873270463067304396297896587339547/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^38 - 2572365503116729885876526860483263454977679683957937710631785997096258020707703073636293452203803759318975555366533554464771616772812999162330798594900122135264289250446853958723653659741293112595242094894944897737736077/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^37 - 25578420836423080521125658138872479977566716202327422850341676055373262335240700765207943689969284157381593619122154496423516860431431168610559269020634716785172482191566981817825063852251049697925424311056843884253739717/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^36 + 19991800810611783250732740158619593032389167308626080846103423965364325974614755888945955767179624143318368153788253656130081114439268731766465491210900342813515658795700397643141950034465941459128342950382908676872767635/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^35 + 108907753848348244954360629368590586058376549414038047022466999770605733769549435021608034689692542455948787105945011611178487361765597331854296798326818039901840423710666492806219240124530497061424559366391627033197735953/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^34 - 80486386197697766085293638122947174913071379408620263073424760786430630533963904536214462541187300871112640697452737649564478591843316511911694018175573772315252166407247202447583519680802642158474732860543766222723584561/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^33 + 2657559055778866850077974348296128519694639200265620772705166685420937832991043155056542177201887568572045365075551320958512157538199712035891922351492227589138204679895948104221479696102218826392821665957431150332555794059/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^32 + 13404399929399896127037119461618075621174358530600688303411935964085323679217501394219194046066211411965172301772964516676245033456826273174716588688486729921619076126827884349793401853336612038207240118099902512476531636275/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^31 - 152768233094399061769104504949725426586965653372379181773990495036097063635512752315466493469213719791068701664851102507746745225497552490115973839862084253300887974205610538149134269382915581391929530744896968160079510702431/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^30 + 64316212171647254269420104365388271371190169991953228758344685180950925170150309183600017305995286552901893836840553001269204337466484690934946504376300637653064453378723914203583991633668013834336054660981570621870056301457/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^29 + 334929315283990203407793685330773666459548322157777531393002761101803222416582284164459200030519927470499925502642985956846758214067644642425844566516063445829738780779117198312676356707337787455398133604986273347123978252227/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^28 - 4477590236813342366205763745438316913408579171632512456230068418154890852380728845829023468996929183494549601877119929808515197236964958481273887516331781005912451636889420193520502887137159140628536232637765698419628257056627/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^27 - 6156699387490182196575543009690842841157939142491748433266570054081956008615369118174995231712993354556734529542425655927815281988839523526705183777805319932380904390016837478632332737786381367190177308682099619037420695231375/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^26 + 79764127049403751878542822009114920144709120466889854565206179819144114909907606699492960408203723195983055837014573939101537242739495610470330685119334114120560533112174693668043617449911728958140053671209202214027843329970899/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^25 + 33297756355761117292178270815472223368848523540878754297966225685547288937867146074614226483867480188527200589155509536425080216115523848234174706804915184240749787226140176193204770128713226720050083128812781299844555793803339/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^24 - 35488712428064807405814148352160375509684756634163878233257557459346362496868509293457855969998690975233666344579896903421338605279231742828028337324915318166366907957140269687682760580832533567885371927529293146164370846092607/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^23 + 33010227239125337153543345589110005494726792277494510441877996717735888614810518373632070737473739467333232430141870740376677923656248015680694152951288321424639113935853705234688960040452455588089536450293061995323308527888111/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^22 + 63945382912108873435052302568287937367736471966819951063906749085584594823022592383200641542366245927872552227376557839078894971862964722310503322782496041370166761072714600828107013030285038547798615329646623951807475447109849/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^21 - 22442762391884923827398276946340758776624247782939920728473686932140475545457103385333817156786360897355323668504977456295742393722970252764249830121851113497497263209474654879535948857622372712911422366041009548317162779942021/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^20 + 506770957098868211082672889992408962395806422529151063772659230836895625160338265803034282849675326505570278226015799107102350431301412579765795021900892972168751498646409340000909639488534982319566691934251309813693249823420383/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^19 - 536472126767964107357965296073217168943470095945788342923039974025285921291297905046819466465726100332089108494427985030487111482803861036672097764114003262216745437057265077695863686846105170147990200457329206721622749096556311/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^18 - 481067844638446305666647940528247562369004836291974912596886428258128570370091980646820055177046016984932502443276571047625910639026991792976005084093861042728944913707775787604348768755254331038120860735115179963271027046767735/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^17 + 653661604730006281117209491189811905006828928920906159442192081453656037373689800086443316168770281480081731530996476404315496012390422533230690905756621097969647699073522875494442388567996234279784515728926209388347957456542277/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^16 - 30931098397217768102114992759950166944920255013444412502824050595823038800554676655363930306547663737531451673825953937509681484421976542187784460625096106640524827669662257673768119619556707290840058820851888735905920972986763/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^15 - 14972537869514990249532753455824835774450004918062670522333656711336744040291845793854052568989156675992835038465603359517099174585736860976316205492949985195874009044492753175436037551639741513153602689021737085858074389875025/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^14 + 187690397784256816610474235538109932027743179953062056696169089538881318100568641519663900277452613149987534115516878106118912547709321918572092864635868599497212801324682849894857579311099125056360493966739108402985071159775171/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^13 - 119270947922702664102646053588488301393017741865024009164555943393413150450462939348409370012235530076570043964683387153346707535215967963547265618812919365151382653115256388990171353930025545764440835229528999744458957696251429/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^12 - 14162891257596573495335795289447198767220594273112594796044283552637600259320401388524479266912350634923658999963509816261694997865000891168159482772092268103674531557551221893114961490880489650383371967540144490642383926689455/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^11 + 41927507117206569425214580668044493715661013027568572548072079599257788897260161230067005211264090075094974989504042304819228339804185205427811484569717166699462949489722964488986288800037551314439456384551802631885158981097993/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^10 + 1603645555812675342866001721782283184069600094925575912894274391744575964543651989336240064684980148812234160549559608736724831659372957759887668524517101936438921206132928344196074625302674155204927634466795969893667632719781/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^9 + 1210715327885770961726170935593930019218511684239289305593048527913587126889701244808581359894737236442537316492116746407364842101818934348714378888951178578134161259483512503594984341311099070969850245107408495754805534835605/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^8 + 183792073921642134450653020744915270970587812400524804547927275435777341052455381812963095833745220002692953026501630626288066069101008636057206656537015160134259914954076351371908366326184269245775933287479019711854625890579/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^7 - 487160578220998530547897969421608100364280298986890752712491630247918068095081174778529183756236333647527645708584783864565937158389935859082412125577215468862392293793289478581446638662214971059901893494598226265692231303669/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^6 - 4751702669378672436401094845051942007757397318672012338927433505571733422539490373117836461807785540755031219736669480833931897358109542510066410588162591218787452702056402230051366885241920617761620393424295777313751100951/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^5 + 19236245071043282155955277377279921360557442419563852242224268230222517477813262606801456702181898525320776336069434276270079689925615603741488570398136460009768633075585291234403043069306572905635332981715412942711922863451/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^4 - 7200264789842079255957470877682121082949051456075932604023276662590916827213704031915191722767519551770671862927960423990084631095727621614481421692752152200849556069244710912648030717923115081120136531614748193746959707/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^3 - 74422050991770212950098066969600338949161037289562722365411038452910985218741218218789291724896407630238226782548173803618445723842295114850395369688920785624693669514927850678582784661898408869389250898835184982639353871/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^2 + 933899244210210049609405490653577184625174626142329891866433633805546718345108148328466395292713131158266747726900610152287489628151534545693819464093358875664274935823060064429151461723972638346754770473111429821140086/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y + 1631255092956887207240154352471548978270778362866003495193590875966274907858204847497151253758607054974985908526887024213248771492673048685712768013895226987384445968905470150685595356664943870059987242592654314715525915/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391

-101805169595482370378498030682248203412837256895410194908749576668972351740927204605541045003905069022111621030279029372783171869323973749243665793741543967776363010702129072620761943492759670162059797631063181975015073/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^39 + 2348042276466982842617583108107760898576902343920630923360470567276281917237010928154554923639758471722408907577924838826826524876508351928921085174570240875032140861159754687786156790076242700731308410133290214954408407/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^38 - 10435489761113241397715316813040036833086798072647779720942669362107193544497043917609248698990256909228593191007634813687456081277558642537913177406757639358320491615475375627069054059877816734182185785594518832876211441/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^37 - 26002273173017025018498821573665980254743874151836272616334632757158125206013107263218901794416016409347156281202317558690382005462916932284154084636678768677593846617386065825847709665490350160261245965470157365334520741/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^36 + 81166143750857408775972595918999477334044230587317845414443470927597929353894289854107598180141920665062511104805035147697948701133305179775254741994906037360321533106315103684569610738402047997412118870171660136311009045/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^35 + 224794297340043859728703677241979176490396170444987825678637789545731305116515299243260085853874227804989764819288213415642655279799118820622964624310086247923984976432512083136737740002240620150285154409888616938766825623/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^34 - 10459505220101409298739940962582422203194271448101413120144178200467286696449900337125810626847213063615772752931333040320241575231912499208024030868063195530991052524259059849005912837265067715870460076213195740508836610909/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^33 + 10736235808631318861308176846066568389869879109894410814980393454286769830426995899434416017241416213735786984197651203547899004492634982956839633793130670405916745054857065588935131105878447384594781423488494744868019707499/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^32 + 13634834604520573510436502688984859438481719910778617753209465783320081785014103734307600210072420740092995335095655334311980288129459601577723864638395805153062469067647134393831517102434205176274724753751002071215984668393/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^31 - 310104906552845159092675917233405177213106290152594449593579684296037128287300157935476702397508372606352548677721693603686854154520356848802866782209150741693089782004425816063334073270490059445599074344400887906213516333633/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^30 + 1043268013475210109931178618476300838749645577883746681038696825742165296829618892427251124035555117218510000687094627731821158784486348180899297684335970929311139371467402120691676707441199142285168036473506974179918742818303/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^29 + 5447310088704707468522853212810471861720847572909206598139204845892697909403220741857825084865278653439092449830696260905115066167659346404857218620779790688843686383646255973204511352509007233879403257434636822627293797103477/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^28 - 18155299644039836257853516004554456199179989952268806422571039844729825054593921659781553454429763344982132629566820400628966374218540713389559378891430035049747754853224983410129418616137589212794382865341456944988793778450719/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^27 - 50110023948603319030067144108875454522919365816039803377294900541167586034198021819474703081073267865973958873338546186133752050806331371396813137288013022418429499646733776334931988769370859113405599653318808620529312959367417/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^26 + 80845538679859750818579418122013588138360045411535541722355717877778144255829503032771960941693637297164505546579037907320258059984822968621542140086248716369446887661337717451839049396321500995126949052291402099133031160266517/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^25 + 68040192980443568169232628572026527665699902502952489533534009149574186413440585955864346459635747404383519317614088789919109282117125450444836932482604547627990057077992155320503870212890732004196375610661506798694168971181591/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^24 - 287826066051198989195835312872763755314244508234095583362148071094499548371485219555832390830920586831674651390796172467375195611536986578316050259993461535070133753977940359776499735654485624045008189387328390099698543228342687/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^23 + 2049417507165091738223017047923587275315600883445233237126263753969674652863869234711220053329536351836587446035865757186659646835592762864916715010022163497458618457024627187885325304236520920362612860467688870209568731246147/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^22 + 129917292402705394901435907296726603999898124496522377380649156900853283819255935874216475426303606315932777400798035479187947358200384018405840681345997603616076105046705760245626445176475468091503242548657989211151536759927833/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^21 - 22506483628498085397681840541929144144857569572758440833568649083117282688575084301179965102057376815570099370585717725240659895074865874988733927089236783398661800603611112088407262896506117259119593091995586724737596891782417/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^20 + 1029030268412384153948417439091117513066908739938975426612425360706491113522898420187527856151137770609633665794075379316619981006731975281162228696934855591588843195502423121182845883793480738145280838156917479220249305737168197/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^19 - 270895453099790312797491879245643503312151376731391323610842374539963506702666921546347736367300606033580326067618573672562876744627624128515217216250458560630319617498821156451021704713476573294720837847493117684437476734708411/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^18 - 981657041431111768829490193531167467327951402742101361832848892569670714100500229348179141500819269653846175172384979741640989142060321964023812010752312238623355810584591839192856221296003674826149240635126298245276880513468123/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^17 + 165184406790455227429156934627511420967258875143669363089397544744865436141607732428829104622997893393237778933284416573623643077877385723469819071116391222371153473699115972271757537039451593962235751591919215814356705026662317/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^16 - 30076957779041827306824154670335583279095085676342144513534175341317293368817253124371836191792156502362949854582360188841637013105443871469084700553284087144947204793755972034359456046502849976323528059566830455988515938284579/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^15 - 60831029289772008063434957459406489782249449354798600202643412533142216383087038286350586706772151853731705151431619319565472275919607744219920909245192837397467936377241388380275420902798408363129011009956129108984850976364801/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^14 + 380514070585264648384535226313963513023726597795496065195622088589619219156393745717330611912711218510131077907741168404812205844816345174435750596036320955463854008586882545938662510907276123412099092753663383565368511318127877/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^13 - 120115807721753273108373095399230090878805068340468466594927878592310233436795473752518781307309479625460592185506534611997193858841977357849330378277224650750502482308125622632266550319229362445340763978832089421068533815803091/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^12 - 29006422680017244201476228170753464202013463094241276501810752390944292660275038041156589394666345917733214053281702704474991496421054961956293004696019001729002264396701833780542763920841333519545491536423645475003289955826199/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^11 + 84488605287915499273088819159352094930251801181823022508577716229205424724767633790000100407728934608471593777918358320028226620403894456668270412193816378379750860285455065681656007010139485422136252778167329422798940745381915/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^10 + 1718859943407422247533062851989271660434134228708806678728524330440136527106975124264500835224005801516875743481646643742787726977947947991030133110663191485264832986866838547116662854456188757595491902062202395568897845013231/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^9 + 2452749272791522186841037567761461186320435604486096711453338671416875034775366273284978736828667072521210525211225891826014647695369891321854246806160714528659272343461099564576648768255445560281743028964133489003113219515151/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^8 + 383717952629098705405422664897862555485303190027170906007687116065271021651971208996536857226498959092760157554319037981657433772966848275401455812716627815115560449101816275893626835542332331149547261019642406337762888089381/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^7 - 492179157243199474430590772875361482249332496758767611662375763752859650250127289491962795404912937710477921518897413135025194366783977755920458642465572042376457444597249805650567179958820622579711656257324519372119593369555/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^6 - 2606099328151140834889000941291770803376957059670189359558522413267421922345511061862975069288578127099602306914786449743814825063270276314139170487837203490008752077030268829405507966370485090647471960839807183094140477233/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^5 + 9736913115025550331316318572466771726897926488113038363051044419412672525274708380613243047756342485710280861304562605419903045843405676831584514872065832172911114304466082102113221465027459613986342413970460502475184448053/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^4 - 10644922922236595738487215404809630773907820537061556076115657166003205792439547752040341654047536595293799181679147066177847089272660655482826438610248433327370367025210723090496942885583576677763911019005465921437888673/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782*y^3 - 75702458769364306415538608369331554288436277043616270428705457065411376461222991331547457219240980662381283601671013029448938054064137624325751392718259617655878006214767145890410309383052913412249121605928094838728418341/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^2 + 1821354055150630476869434157945027424034554114046269236440220101838670799764105649749770383188158761994839770653351706327100111363890913830089909034258500339384000091805640834799601499024798267288914166572196884047344663/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782*y + 1664940988425565059921714130621314924287052034346867715617132721929054813248697296482845683159311065479561695482702062051621273731492692083572111585984217902497513449305688767780656138933755221882721931701247230411726288/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391

925531178604605627675464211478061324810660063567298872461514457627397142635606279464421977311839129127245922425609722284718270873214137286212719845506474373953145599996640434362510081047246823195458845387695877541601/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^39 - 21347973848888795533359015476957740417919418125184803143383004347763832092308212129411759636123612416662643130096035278864463510906048413645148513778307744402866559651232962226703957876244123874585797188239986204891109/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^38 + 95015632337520604725971153540788201919464893965422680536930504862346921883726070397791660183091463137227846106920964954175610139180798176970741192495964990717543950574409084094612118421223073789893291471007088557142495/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^37 + 58756956298590433285201825067933914175735901427561986360862938672118404404616772105852567234485850991963467377124278137786219319027961452691383414177318557777774254889551580613735654219822666951157862710117879785419761/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^36 - 736512402995494514472316567431176809776297540096003981931166944884165482327047075184968683042774008399147602310479993188350441831443015550638196034230013703230164183321102630174299808899149900000701187524713512861515027/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^35 - 1979938272428184149476079974463112297384555097785578282703570027541675451763487532988825634885489322070660373530411121207495173179079817751030437694591712485390381839432410493728677599592119200848229169599257973471227487/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^34 + 94376811919020316851604642318263906504795455516304215861383642742060836298263097152744382739328289553823887839185950615512012967106249912611916410182789959118849357698568767895458865278115823055797678735350304998936082351/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^33 - 97874413389258824171069773084267195259383249848719074837673715552276273580494229318277028368692700297347647112576232389841076301074826672310203525866778091117507778199707962967117213497415467540839106139667221971997274421/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^32 - 59103887598666190254446921708632985872344177829295293119777141013903284670266671988164619699520108083851224366728810376133106885564347697811919140404327168216321372153179286381621748877573498506987657695294481511219320535/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^31 + 2806020848078119553069332570446089877352479535217664613476570516546984228317506654875700766251086518150641995266941409825381349314106841222059614433324273903875611706967002495141405951061832215824766884425215913792118267465/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^30 - 9515162122715642932929449434959789511789941245745773698677322768145112230285324986106531950299735233487781115902998619448552312119086935091071747435356353376862038904029481109405758231962047505976149123452183847213091231509/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^29 - 49166986969964918340205549163044843920855173075850533701120312439518924060403864668620282104584428734366962278320026718792216568512778544452844060842771279490333191834115677237291686194600337465626570362589838214916169388263/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^28 + 163933662429309791964312198772425073793254118202524067177303661048015570496037025488117317197110778874104533350587689880412878693024279899521007254383287710129067918883560772597839451752533163243078637079343751653512301174737/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^27 + 449599042107023509852834057216089929414253277059124349773100540913978378894457780623251648661833864927488859240983649824809022843272601229945613412142320208155567961382960552910195576527900429375366747986206149733758137880923/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^26 - 362518140175785790966188505011673321867243893599013670681021465630266911385090815145539920260883844336898288157937930277006228592132816296545397176963439259208121778927978808851723888788773766184531167664375430444848543766201/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^25 - 592111527426191256590222894588553237707425553303618834064014405392498156707941581141649808174040547304221794317828736924121768464505485493514234702573973753399614982616991834446089579762997732706485427231088449531419166619443/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^24 + 2526518478806754397045568897860476895761709675444460506123400997117111529116916711670567838167206632938767766247707433816271853103777197395565769903762451600781277950889211667099021926941131388985914155500158545105681260604253/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^23 - 328356507225296411859533863103356603494551709884644920090451792778751061766177124466209330175431538453083379260297847873994582906286475761419417081862367919745061529531890858763612873908038748038671339024357170420693426342759/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^22 - 868045249924578167409428745619714177405545149393353640682206887348919656249147493005895300987242031982987231000940983482522413327105981805291764568858386335927207483757554181419837618630939646349800561333668020328729528287525/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^21 + 17683849843874938544921540280930427863838716235016586353351552533303375714891876029806575358274223229031541875673798453396346644789870104344489784892286740079990108904276255608160867623926167312817943251748160682196951160157/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^20 - 9520228040772001489582591768811771997143722796817563012946985377043328675807425212870779890257108672450592406810996192861465302666208861421944314685206569825117686067090618894926472907751603325503108001053945364700907038191541/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^19 + 4975651064483431634246332110303451902237409572091798400261465670040719343911237181276066364707106371742820135355203203513418891852283652630025554801662408072445209152392257356663717161000742572174124734571106398830835239356849/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^18 + 7750315745992122753526602328445583658226593211699706195260445090189428338350106217744904399988159850492615556881222093807693775635630028396843381417317006343206702012387986945340837081578318561899783719472742327015984245255927/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^17 - 5321781027135585694448276938232310148171712971641119325433620313427908483227741712943369916202935137642067203579763715230599550360888728933853710954092825386770190132500511941013881120705057857497265673394562842731548270181561/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^16 + 113742365430764917234189750362022611674004572116690634178730510237058338044378834096351180038398454354950617919776948724942303146183793606593741838577426693196333966087526177085996592142431198178092230473828604124119792318489/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^15 + 209616690500728978685679009656307797608920249809992724399134532502405334109664063827048305215368263146838597532116168994712403918505397997881662262566582926984110974063296330957408115925714919174523483774749338952239806355295/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^14 - 3031455823253636289084380118214302977507881056941864197474664217509362321631074826436706376889685090135878063195732705573232272359382742602079778290240945267537743811586361091089460978419834303824223704719455007855664296521213/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^13 + 550609116747782662252109779522540507441096390082039987855530438689491089390980486542830544198343237446063340105451265915636420273344390851349880574534712671002879234548079482345796521910781118647956980187070435678116686433791/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^12 + 173558762205779241234023656194917893352983390042052955365332471082667805107415163224321558054857807355415512494724787663146969957890760640556449335602125295522389396720836628488805204043838929000038671041164839096446939181787/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^11 - 449522559382335505213669863373710353892468491658326734337349541051171539812912135250468950546112214202909618402921315381218019694957789285599858148198168496361497543005603725545375230617432214574007509529191804905664228810299/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^10 + 251417550380613949089963308870740180115421677714915166695652090921645966183524218836193095076138688957557308833012779821506813369034693153169521594200841008006117697675712495861429939807292023810822459958267692038458730759/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^9 - 35631725278838976095962646095486383288076476150715937050221422789350772851026242263020567652692572800199227020630759598066171139075678843693523421135157406890006415494586127309198338652746465717673103743436551602880258692943/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^8 - 2532969119471690317210161088327764499904853103297711218131267831366207131133155870220278298780138410871791960291858200182632521515658194708859006008493426159416955949887095660437976693949676514688893415644243124151416978477/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^7 + 1633727922414089965506872538719315830826723312315252607747411189268789116388660732728307469248773371066366250889773382109178561224111305466379081024616416823239240571307712229730300538793718058497949866707927044232435783179/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^6 + 55548986130577415669417585145810606706387308867302529427197605102354773281573193674324286489577058936132597930003432742010087835898230574864377397678924303907372029516349955671896847024656645898901631906156762607118245835/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^5 - 84425446533222761275443074257593371548123211281718579028272895482322432163897113597177763886068723946519248110300373390403675667095218312057167107322348303392814945804460270425726475510802296649821421896554557390940933709/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^4 - 1231227960794203216863503275415235671731215477621200892289812868950511486600511477841898437863886135789610183210183683555349484185676192594111638963438248147226766409328432877003944771985371723490760910387753516529488316/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^3 + 781537431572797956737515439319449277515044907711163110316312899017675618520313610834779328761136610241374236195101302018246550389538117213204552028579645544989718030700592038855306956719934751847401328931398958527509784/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^2 + 44692700325353821643570606981238721248862558592050679835093197221748734824360647609887058307583534693794508118690329544064173853735865448078708602951856952139928304792931234003969189650073426827517093899008326939658454/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y - 5062294362399166824369159180880826441453239247014830166977671343942087900826800982622698422802686540028387324029596164329923299791857398021682850714238390097971979838604442727966205382320525498748975256545553784895107/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391

925531178604605627675464211478061324810660063567298872461514457627397142635606279464421977311839129127245922425609722284718270873214137286212719845506474373953145599996640434362510081047246823195458845387695877541601/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^39 - 21347973848888795533359015476957740417919418125184803143383004347763832092308212129411759636123612416662643130096035278864463510906048413645148513778307744402866559651232962226703957876244123874585797188239986204891109/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^38 + 95015632337520604725971153540788201919464893965422680536930504862346921883726070397791660183091463137227846106920964954175610139180798176970741192495964990717543950574409084094612118421223073789893291471007088557142495/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^37 + 58756956298590433285201825067933914175735901427561986360862938672118404404616772105852567234485850991963467377124278137786219319027961452691383414177318557777774254889551580613735654219822666951157862710117879785419761/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^36 - 736512402995494514472316567431176809776297540096003981931166944884165482327047075184968683042774008399147602310479993188350441831443015550638196034230013703230164183321102630174299808899149900000701187524713512861515027/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^35 - 1979938272428184149476079974463112297384555097785578282703570027541675451763487532988825634885489322070660373530411121207495173179079817751030437694591712485390381839432410493728677599592119200848229169599257973471227487/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^34 + 94376811919020316851604642318263906504795455516304215861383642742060836298263097152744382739328289553823887839185950615512012967106249912611916410182789959118849357698568767895458865278115823055797678735350304998936082351/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^33 - 97874413389258824171069773084267195259383249848719074837673715552276273580494229318277028368692700297347647112576232389841076301074826672310203525866778091117507778199707962967117213497415467540839106139667221971997274421/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^32 - 59103887598666190254446921708632985872344177829295293119777141013903284670266671988164619699520108083851224366728810376133106885564347697811919140404327168216321372153179286381621748877573498506987657695294481511219320535/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^31 + 2806020848078119553069332570446089877352479535217664613476570516546984228317506654875700766251086518150641995266941409825381349314106841222059614433324273903875611706967002495141405951061832215824766884425215913792118267465/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^30 - 9515162122715642932929449434959789511789941245745773698677322768145112230285324986106531950299735233487781115902998619448552312119086935091071747435356353376862038904029481109405758231962047505976149123452183847213091231509/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^29 - 49166986969964918340205549163044843920855173075850533701120312439518924060403864668620282104584428734366962278320026718792216568512778544452844060842771279490333191834115677237291686194600337465626570362589838214916169388263/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^28 + 163933662429309791964312198772425073793254118202524067177303661048015570496037025488117317197110778874104533350587689880412878693024279899521007254383287710129067918883560772597839451752533163243078637079343751653512301174737/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^27 + 449599042107023509852834057216089929414253277059124349773100540913978378894457780623251648661833864927488859240983649824809022843272601229945613412142320208155567961382960552910195576527900429375366747986206149733758137880923/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^26 - 362518140175785790966188505011673321867243893599013670681021465630266911385090815145539920260883844336898288157937930277006228592132816296545397176963439259208121778927978808851723888788773766184531167664375430444848543766201/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^25 - 592111527426191256590222894588553237707425553303618834064014405392498156707941581141649808174040547304221794317828736924121768464505485493514234702573973753399614982616991834446089579762997732706485427231088449531419166619443/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^24 + 2526518478806754397045568897860476895761709675444460506123400997117111529116916711670567838167206632938767766247707433816271853103777197395565769903762451600781277950889211667099021926941131388985914155500158545105681260604253/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^23 - 328356507225296411859533863103356603494551709884644920090451792778751061766177124466209330175431538453083379260297847873994582906286475761419417081862367919745061529531890858763612873908038748038671339024357170420693426342759/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^22 - 868045249924578167409428745619714177405545149393353640682206887348919656249147493005895300987242031982987231000940983482522413327105981805291764568858386335927207483757554181419837618630939646349800561333668020328729528287525/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^21 + 17683849843874938544921540280930427863838716235016586353351552533303375714891876029806575358274223229031541875673798453396346644789870104344489784892286740079990108904276255608160867623926167312817943251748160682196951160157/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^20 - 9520228040772001489582591768811771997143722796817563012946985377043328675807425212870779890257108672450592406810996192861465302666208861421944314685206569825117686067090618894926472907751603325503108001053945364700907038191541/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^19 + 4975651064483431634246332110303451902237409572091798400261465670040719343911237181276066364707106371742820135355203203513418891852283652630025554801662408072445209152392257356663717161000742572174124734571106398830835239356849/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^18 + 7750315745992122753526602328445583658226593211699706195260445090189428338350106217744904399988159850492615556881222093807693775635630028396843381417317006343206702012387986945340837081578318561899783719472742327015984245255927/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^17 - 5321781027135585694448276938232310148171712971641119325433620313427908483227741712943369916202935137642067203579763715230599550360888728933853710954092825386770190132500511941013881120705057857497265673394562842731548270181561/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^16 + 113742365430764917234189750362022611674004572116690634178730510237058338044378834096351180038398454354950617919776948724942303146183793606593741838577426693196333966087526177085996592142431198178092230473828604124119792318489/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^15 + 209616690500728978685679009656307797608920249809992724399134532502405334109664063827048305215368263146838597532116168994712403918505397997881662262566582926984110974063296330957408115925714919174523483774749338952239806355295/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^14 - 3031455823253636289084380118214302977507881056941864197474664217509362321631074826436706376889685090135878063195732705573232272359382742602079778290240945267537743811586361091089460978419834303824223704719455007855664296521213/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^13 + 550609116747782662252109779522540507441096390082039987855530438689491089390980486542830544198343237446063340105451265915636420273344390851349880574534712671002879234548079482345796521910781118647956980187070435678116686433791/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^12 + 173558762205779241234023656194917893352983390042052955365332471082667805107415163224321558054857807355415512494724787663146969957890760640556449335602125295522389396720836628488805204043838929000038671041164839096446939181787/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^11 - 449522559382335505213669863373710353892468491658326734337349541051171539812912135250468950546112214202909618402921315381218019694957789285599858148198168496361497543005603725545375230617432214574007509529191804905664228810299/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^10 + 251417550380613949089963308870740180115421677714915166695652090921645966183524218836193095076138688957557308833012779821506813369034693153169521594200841008006117697675712495861429939807292023810822459958267692038458730759/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^9 - 35631725278838976095962646095486383288076476150715937050221422789350772851026242263020567652692572800199227020630759598066171139075678843693523421135157406890006415494586127309198338652746465717673103743436551602880258692943/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^8 - 2532969119471690317210161088327764499904853103297711218131267831366207131133155870220278298780138410871791960291858200182632521515658194708859006008493426159416955949887095660437976693949676514688893415644243124151416978477/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^7 + 1633727922414089965506872538719315830826723312315252607747411189268789116388660732728307469248773371066366250889773382109178561224111305466379081024616416823239240571307712229730300538793718058497949866707927044232435783179/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^6 + 55548986130577415669417585145810606706387308867302529427197605102354773281573193674324286489577058936132597930003432742010087835898230574864377397678924303907372029516349955671896847024656645898901631906156762607118245835/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^5 - 84425446533222761275443074257593371548123211281718579028272895482322432163897113597177763886068723946519248110300373390403675667095218312057167107322348303392814945804460270425726475510802296649821421896554557390940933709/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^4 - 1231227960794203216863503275415235671731215477621200892289812868950511486600511477841898437863886135789610183210183683555349484185676192594111638963438248147226766409328432877003944771985371723490760910387753516529488316/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^3 + 781537431572797956737515439319449277515044907711163110316312899017675618520313610834779328761136610241374236195101302018246550389538117213204552028579645544989718030700592038855306956719934751847401328931398958527509784/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y^2 + 44692700325353821643570606981238721248862558592050679835093197221748734824360647609887058307583534693794508118690329544064173853735865448078708602951856952139928304792931234003969189650073426827517093899008326939658454/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391*y - 5062294362399166824369159180880826441453239247014830166977671343942087900826800982622698422802686540028387324029596164329923299791857398021682850714238390097971979838604442727966205382320525498748975256545553784895107/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391

-92122110867168555033884234628971360135422254079557976854726458948630235010830048606457872484171172658804015926748630223375848389749664482839589555441801928242773123336865212854432172573089026045904300088994133605093709/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^39 + 2124090795212111027196473137730524995433912437452260150691744861660291899872593335769068099928366618882948692210925508029674995753394052827216163155304469307259304320899309342914634981158402605343512234468784493540946995/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^38 - 9427609584466246119931736929160093524505404124556818353697857961794285849167237477184319737052434108857462637801634602427327313026369656597825970480154236157736373955620834539719405750603130508707435161601807105391400325/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^37 - 23572681949219230237480848570137506490324095438970925077522184723249712325935449513714665170857443262012858032782153518356664135765649498958495231721576015294206280681589482643274154681359731201829766421072571130785320181/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^36 + 73420282165811843512538751526104366953729054904759621442830241897676652738103688619233277606256470301388800654789148489925770699932042526836430336464884339161730366864701574289232393704743687482208022841519568841362746993/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^35 + 207853604307488791135864290657167079187194382308794111874020403736412553194504888363002422445503014512717297848445781318677121106332306286094440720845147102683225561457858355290429723661390252617809225996605362738436263531/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^34 - 9469855865820755226183292973467263521535458192786024629479341708010132495193394380847956696777794982970904206404602829165589766923167580691765847207624341893027455265477553705526341991592146748896861848690356804351221349745/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^33 + 9651012632132147019161677889572295175659256664000323414666079029672314974641387030672068436097965543138326446265994377602248833816991140532098308460557982709569322498961290262132713105832165369211852214441816682988649362247/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^32 + 12422362627821727957946345693298522526398421476515566843249911728931390861310615464965050992257193133316115740217577853228075662111197536956557024247796252682013197705695181035520560793981488334326549932282199323434991758001/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^31 - 280579680704514212208902223679953450360525553355736812191670487457557864744471608299818497569582777978523710570596014029412181311776680000348652938539051810239376988147781515899062448426088112118247129640328542224808399507213/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^30 + 941922911283058608224744781134143759927264079113930148078143297502689884901192438720177839245297845655141356708324743596946447016403626957058531204270060994048497377814106684449290378588404748556673073042576937376143125694747/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^29 + 4938683507747743120519390317006062813936420826988879229068651365873668514140144528213616501089989826942976167403902096473021177258760973925960418918323353439103989068032881055238091555898540096955367190045481178117306716400617/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^28 - 16406520335706615598239051835432686559056190619230871286557398332512271674663430925285320587475762241083292976384682381193470000738335603749259887178356795213830064517533855587580130244760046792618085391449228335043698097336395/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^27 - 45505061442494605800455459861960068589902115797226627821645337548690736130750602747294320420816381270633465964803451030673581686026431844444249265850624524298785299795754511997813353916348849916453941074657486104717403217848669/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^26 + 73100205254299216155826371527533444259775820645960646724559466939569905316032768238718806710313155144452495427226386483734529389652326212757500094712842722106490065320749662383556645657679089650808590456372031171252068551246541/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^25 + 62280311074907488816749986049924652498882842044697973966530425090065108843150589729990999294462477398344085233801000168959599809064807344651912002656496075504653701052554598316976359770625926129719739394980169445994670301518651/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^24 - 260893991628889516028006839985970126699160132510531081185265870948683875580695828758968564109105204754149720576758090382443415999553683354669842207680008187424976054556295669330032600526745692743574843746456619155656307325011035/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^23 + 7146651200313997895720760396371066115869124390263654596462988566552180837104479110191715884516960278726149835653534144656299101114885058033016308582725279471812470614941592191625371937160660142796278039547925988687804402775713/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^22 + 120884146134756049326628046658842486357185558787252785696579867647695464103732637442407904620389390728970039044582995061538757685353570865191100755599253089027241728003173404737658046380254275534327631497035682776652018047902389/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^21 - 20720161145022457285276541660064612393896179653258375401622019911643165500492513000046322418411308707424615198869902248738841725027908137639118772144251933248268246905055451384738028120356532529346330061671523909035672657090417/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^20 + 929224255297638117496344733915864262689661314475723484513346420187321898199393952578384265591460708383147264113488347157932786959257422308863966526225620772500564674312035202349700208475975639087770678564373358120430909934329057/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^19 - 243303534313810960802373296753912190477810177178430434206625309610024341505832795810987265000913639313840820499535788651387703087166780536923802420866225245189367411268659546309874196177702566324667656657891553710962369376723057/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^18 - 905453104261241319235306042237404942347257334659876773269747002301298969055338549280238307985201884323482808311927760729496437356362454139187182916104439427260869783059510584750160765659283050414802756278191069733157946482937103/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^17 + 2350927597281310526468590783569379335060971852034994788996776414384117909417785751121102546428697421408648372420318141100906934447240290555686710159815636909628576000701664081290362515862357688971484435916906969991778389558575/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^16 - 23904274521808219732639369127840022435702946224642434057993421536584557223517702430996064969950441475337291295740349342933263813253461360237170987845283014433827948327703192045573720749620736200174779687506074815277022115747203/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^15 - 58646047448962846902207229765158053205460144957504082333960501140875857930067135755528597063381161256914590344984074755689884332319348352226659790860976452388580941495006604787928259800925461576184980022186057944472597087916949/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^14 + 348073050393456009645258735680536972069894309573904269493034123507581177426043889578711513389203020020635189423783390527256405174230958331404503968006454224604372082864577344503773373670762926954143189288516537445328037422784129/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^13 - 107528940189703645960724651943495160868290718060962114803369562235907658928063119722251253393191470533261979427813725717971111267281484755245226286824040245153908858879976794995363566478393714321566252953306422275125815674446203/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^12 - 27450708314846490809825795520982558626242791884622340541259312186337543144163950033190255089038689376484504922396864454379040385246533531178759738011741224775836587597901049444346671357675344860006688397685322549674869003441835/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^11 + 79077202961389356185193962931412105478946933428533191100724705796033123355971026490499207049158444441073252884045460148903421756745973531008753762333537222028512911788724049172771125317438891102477002373583999088185945225870783/9247201108130240579812324199841873006603758263196470680487724697168792533462250911235809671294812797322532437355568364163314505838066204657180264361701807860654393908045874703137282340999374084512704882801309540341313536*y^10 + 1821618652556340542533620764283846375542845596612646799217929183353674979447724609333747516780022253554630171448129922559135156545195077311774479739345677788057333077075025585880540818033480578620023827175254111035459927197191/4623600554065120289906162099920936503301879131598235340243862348584396266731125455617904835647406398661266218677784182081657252919033102328590132180850903930327196954022937351568641170499687042256352441400654770170656768*y^9 + 2072506554714979012234025731871486614275125911480834289811737726455266321328940603955336273596971678284543218240250310984140542240729342609568888621243806099313837067646216922652398288042715246354059956262017151308214216348051/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^8 + 368705173219837131717372865721451199455108029589804901380055151884376486520058352004732332068501840906199874280175314632440840817773238552964042378280898542856651892349704893459201338822651879500721157084711566606997357647537/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^7 - 455285375689020814324458319247993944782502336577591089649532691155413384447329359471505772210836589912100523148297533222433788253579987714314218849500055062507617063113410991333176646370003680094900036362762216644608154067547/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^6 - 2521471013452722612819619128351887005733957817224561805905046609524984631314373530087404928148701437190027927118279748470238375855209382712234286081030448274274000771006229469333847490039387578610892986603752722263949890391/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^5 + 9263837081087611351978683193327714086537994812073429879307446847046385404122287915297399146751107963065202628042944158243485066200966310685647522400704572772503209565351591425731873493595930229663617697643970956759384439115/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^4 - 13306137841961697872512086613235138671366483726228352481366551291034939294319788772018892697430616895835667215873447901522124817527042406764688386982967619547156055576966949443198151694768683137268804332671998837137486741/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y^3 - 73842180973086359585829315466527046304180298532934843500026959525905815045311966326911391306604835506670836086833647266259835751075263687380489333281843710530847116961124423643646792775255542594986555104042522923062038377/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y^2 + 2003477349362288833803109417017236706586890263179390560694255890499880149187664390850624013325391637049410626434912475531575666293169390365287203489235806373715205583478631820994035890868793631162060021968209332624107123/18060939664316876132445945702816158216022965357805606797827587299157797916918458811007440764247681244770571166710094461256473644214973055971055203831448843477840613101652099029565004572264402508813876724221307695979128*y + 417043276423566598606374392920451795091936826362125675508694441007812971161634375321832121586920126752071043097155172064033160498716817651342371170230099161651645741222962772796717651749962686785036878087030605855821522/2257617458039609516555743212852019777002870669725700849728448412394724739614807351375930095530960155596321395838761807657059205526871631996381900478931105434730076637706512378695625571533050313601734590527663461997391


# A Gluing Matrix
{{-1,-2,-2,-1,0,0,0,0},{-2,-3,-4,-2,0,0,0,0},{-2,-4,-5,-3,0,0,0,0},{-2,-4,-6,-2,-1,0,0,0},{0,0,0,-1,1,-1,-1,0},{0,0,0,0,-1,0,0,1},{0,0,0,0,-1,0,0,1},{0,0,0,0,0,1,1,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,2,0,0,0,0},{0,0,0,0,2,0,0,0},{0,0,0,0,0,1,1,0},{0,0,0,0,0,0,2,0},{0,0,0,0,0,0,0,2}}

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

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

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

# 1 Loop Invariant
359494919765565512511810228867303315668334747952830812348345639522574350932360256355279552412445927677617600498165829754714083478291378405774096092638669620735373913896636418421349322874741522861753203467208849787022249/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^39 - 8354691092086727866036699915109598379750806364482609558302299860196109910493971500187597984611576454060964384839146651858809907658003817947999274735262351437177406792602408474430526641286472627302728461064642225543263587/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^38 + 38337166734501913277117922938937490284126871852704827979415355580300516847989990320296694971578545029252960383971402706445097255985878480442655602452546700866366206322620143724265262083999316536513380107306878998434174415/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^37 + 22061666464463106915916956656865984255216283469708815973052628334481070492825590028208152162780706516617986907436039174419204463536751568688324848336270333346991834594483246366722955468722684889005487397221626911227055751/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^36 - 1161019650310566262698466739817266700752259470705971479498361809423860941031600130302871123059099148859875448120627527183426156817401497011042349774198658956885407867223491033563565901180985022550048021753200142919673916687/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^35 - 377432801878047456308348735220048863764727396719487841984461024630405166747904400045684243361507897754409701037226495281514750345199963589574631730889201890675894142382070954847645742722235727356776409442762619925225309651/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^34 + 36888975514000393337358247342804628512618593048534905153063753179152166323646280704879730958583971767050933448202574330514200448057286576021170067166856509334199129735929781022790334410342461133163454924335028869482926266545/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^33 - 44383809977434228346476192480797694234278263776436802633805479138791146212789753695326717910432471153261764128428389758232812050238280957591914704171370482993988309229928094462033129420014531287009272593379837222819860505437/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^32 - 21682908853765312155025788644215888671973906590320168603687228959591371952916649536947627781054265498472425807767622481346410640214669208623764590616391681928151631808584404753626409308569765158517016722119063301386178256979/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^31 + 1107617810517170744500657971550276015616739033295133767314209579515763405903886416995188811855245171631612517032355167637818189116394965823120609856344802764350715865952722266304336763508315422113554352809632356223789165399307/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^30 - 3882494829463892773260034034125564275585153119821446512151440129034939553124488307992786801870328082232133898036176617277145966685140919920056623939314673232192109920511342188014289098174032600409551783063056374803902174099943/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^29 - 18498832237797407535721050160581446960832437873240510040080114767275511642994595422128567845477338142925480423533940456537859542021246479702013654709612129902329415870844322551875287317688107083000047152315859943322768973572119/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^28 + 67165633217379370087525561249053178511580523758349216596092745948609137138703336370240995474853643232206856415595026096521104990986829206061377259677168853292496604037057719557757100156059055479967356288070755933054968787688877/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^27 + 164319505329493634896332372410518149073070655401754074473308318074069911680600603508298298963369720950932738572812359248050481739977373944077797318068933895097847365264732589401032865663383517472067040378673235712766496062694827/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^26 - 37274928283386242901301428669866769408379550653882267051911841766779239250561349190024788456296969301060312433083374048895501596124016640152259607807454955667830153397390122243055071249743036668162204030719996516194844872817809/144487517314535009059567565622529265728183722862444854382620698393262383335347670488059526113981449958164569333680755690051789153719784447768441630651590747822724904813216792236520036578115220070511013793770461567833024*y^25 - 92210406056141499639075390416477713974760732927017207041607478437843691413190868497111818801311724191525817307636439075523756012907264168928366653703286474639756316867040890675920296342204139671388236927218416521403266896282821/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^24 + 1033291640430151387201088900909082933172635423427850714851094223696458641239576362866273160191756656074135496937246009447031776232740057552398205099938296516411286952016823590907389721847494942658571093667300161783815983449508637/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^23 - 208909241929598427173390838333198549196226486582811852503123890727462228707553961651284488593584787901522540066608993717950928818170965260739852103823887963064150925648698074828724604818303422825026172580113407017354210620292349/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^22 - 332414615713817457682217539711491675414120654456579575308083097902201176243158838229334643046899934065377432888155798926929660116440388726404932306695328703314921355154196472686700299578195970815517068126489264860352920265802827/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^21 + 91752620270182257573250576769858604484842690794511207707377735269916318351311951135727720950131481643849653967507044569668944039584787285905839998810400528076932612957128733682421306982209363642134293778528752757697549728659007/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^20 - 3723421573138227131601165607851859793469524766719116764518484995774954111805491653047937085084353871411674069318642458751608360878423251937502463516927498953539324234505755767354322381496748180624753909673326306769384830219620401/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^19 + 562870135464791113142783029822317332978037630279635644374956415568867327015124492374994444543380501542986445699465694007243919407986469544224600442947361451029634301126048495325391490149542280551183320119539280863718536111232129/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^18 + 2495132140380625103516377770486958033200182675001720800117897450250723567661047833600435191801259324693713136022657169240062700335701759936116616211978260889449575015087406854659382557081773430408539053237137166237765691079074833/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^17 - 1207919574127739600033544425736465815217505706062538211031069307104755536440898702192619380435333122520386819839484716022098487402838007211907900118855071745631997272898866140899479072756190570082000864776265482325770541012969129/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^16 + 669923632423698590809628744964030725562668131974482790039105437961356840400676999301287770882017392750268531675616400903080009908515626302153734583690339865750126528823092763348881187399628901522886650576309828089757522185480085/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^15 + 88917477976628734062104241653415445774078888756750509224906256831073314443095602403537267629272913795394836499516076898468302686709615235470245981389723195689945499171999746095398511054331917737723363645708296737026210946196199/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^14 - 1292501784687675888617407079337880460548664045257755115073728443280852678202533858044415479342468612536165956177602877282490082555281068686516970747744022064988005135048312208652121855923980983312312021518379649116730583421142709/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^13 + 537356454446709792066828287096283932225332441575249616554107749942394065619695133431555987014068803922834192886557903286213469846037339228597256455749556491742086176378741888545169958903278791892488806906923760267909073740549977/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^12 + 80772744220479678067312460310829185770679292655847864243214662778679804523758970309174122943182728324690640738312334471499338153957609007812508362353540297425474708245826910775133689435323110271991490630497557270113503088626505/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^11 - 259266350975788164856558976269371828983997567605199825065788324776165743569467426613178018376017711641732858761297531498208189977972041214029728168210854790413193311323069077698724721166877908366463375674678536020192949740779871/2311800277032560144953081049960468251650939565799117670121931174292198133365562727808952417823703199330633109338892091040828626459516551164295066090425451965163598477011468675784320585249843521128176220700327385085328384*y^10 + 14801788490415642462860564094232472291137494847756639815611085297897048953226277679922604142957505747305713154980341591019636807096571925088659482327664229292731273387625975197103290746946282669810855240285986952759678923288627/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^9 - 26713271061987602584464146929416172030264947313409930306349102624191885795452475017485285578673037604990699649659391914884282258192462229510755364246485422837324895468909051193895073354425902955502068936642361643134184984847761/1155900138516280072476540524980234125825469782899558835060965587146099066682781363904476208911851599665316554669446045520414313229758275582147533045212725982581799238505734337892160292624921760564088110350163692542664192*y^8 + 195431409151433197473902826182599835779985528360844400489965400591654106548867042633714014904811775542901965672537439916943882648360200781980754596847745408127853346142162444876525361336842255280847537515645706165618859890693/577950069258140036238270262490117062912734891449779417530482793573049533341390681952238104455925799832658277334723022760207156614879137791073766522606362991290899619252867168946080146312460880282044055175081846271332096*y^7 + 3062626051401354254083176009438327841437225659133962129715735294666013925437504971445376087026029193945103451133601880710512417704986047287927161146655936920745641348272546284828882645320445749036903295102900248714684312765263/288975034629070018119135131245058531456367445724889708765241396786524766670695340976119052227962899916329138667361511380103578307439568895536883261303181495645449809626433584473040073156230440141022027587540923135666048*y^6 - 4332798375012339011382793351699771959344528773982602873261629481392312452797020774026037660378823798476394573839003841985959975935601653624440581035144586505762915835445784992466162238508617467913381648237766915876718128107/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782*y^5 - 86799878503307097363826426458115202857794951927208280990876278857882473816787282103571565499045413883120561033338069541112829223352530567758839720010742214261535913874700379822331694548120995898412218016803207404325738399827/72243758657267504529783782811264632864091861431222427191310349196631191667673835244029763056990724979082284666840377845025894576859892223884220815325795373911362452406608396118260018289057610035255506896885230783916512*y^4 + 3953420220257754395105288773397531799208160610042060942502284723459594332165717803290389509153962065095961702319291688208685985794082900708779383046984170187978368904280861829407428105623465352196176994809532719955823890857/36121879328633752264891891405632316432045930715611213595655174598315595833836917622014881528495362489541142333420188922512947288429946111942110407662897686955681226203304198059130009144528805017627753448442615391958256*y^3 + 207002013235122657418581299929537134013276030602543072560365987246069521336266895050715829252649929896479439489620061985945448962354461093911286680535502312868688888343752626279470299347016104276020361615800895358870318535/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782*y^2 - 23596478312282726846913941531333131180053951436301493129451960743653581117254107866529512963232296010252056653780514822091176601007311849597081427446420431932684017662140021491125533171684044060781501638197216894370385185/9030469832158438066222972851408079108011482678902803398913793649578898958459229405503720382123840622385285583355047230628236822107486527985527601915724421738920306550826049514782502286132201254406938362110653847989564*y - 2416059684326757851697633408073427019150070476709487185887913494329591129869764818835722130960372261104757363500191061115601636832100959160629334154654807993877230331794644222729457953908611371746020671224657886605863045/4515234916079219033111486425704039554005741339451401699456896824789449479229614702751860191061920311192642791677523615314118411053743263992763800957862210869460153275413024757391251143066100627203469181055326923994782

# 2 Loop Invariant
-203701540027797977524493575259746099131701287243217924154398714056255047612727374058869392235515965021615820192243375460237908376538237573338090269856379922966421999798360274313494361374921882547024661626858667475871521850994267609093859748014094842958226253360288000041981155537429055232598286597594225190525789896459227907092964307389472873830733071936623523164686342164205/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^39 + 1566063220500069448806049094248230320424886718080246977462135488881318056560892042788454844776755685783613472577583432554098572783786613119509634956633491916105425433898407864726008377825633019686674965980059720601897815853658238060664866516133504659686415600571115051999804008738339556772033459790625495843809946235988981191379113680197024003308196403386926557476934794648323/227688037869353196137373365644025510802117390809235890178162007878852609826831321154498240519150098067860536529101509835749138867341006764097617070986094157001955196997523205440648423382146858706747145243630882623127805075147681312298348803311107340296987914631444720489117994322378955260191923028394367133316292137701593605590659273905212116722386100317524654997302987589185536*y^38 - 20893205899140434922788466960054033752423222534097771153724354943832957294722648397198678536416829827410042072194288169801829182497853280179593491980723262543427772830788607738828909938277846108026131078806869941255040176126236204396873288751550707431381473850341504018931011028763088593466831668257666034569798253594091667633992375128688540331196470866513279336236659938007335/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^37 - 8646436996476484983400801075604629611371982953419773176773946332735891982478432947980097292070587901584807073252049920259904634295158030568072259013313392334298988915431740446985596062092590386564403573668326742081862187083586111075768907382054630654299188030315126045096464150349125884443398646051426141403848712230132630233221812543320903026249816632640329812059064470806889/56922009467338299034343341411006377700529347702308972544540501969713152456707830288624560129787524516965134132275377458937284716835251691024404267746523539250488799249380801360162105845536714676686786310907720655781951268786920328074587200827776835074246978657861180122279498580594738815047980757098591783329073034425398401397664818476303029180596525079381163749325746897296384*y^36 + 324468563884746592431639011978484826059348060376984512176904685516904360199928924843618732340753741772722666778586124753791423239059086384708400305309501555261981563189007957271816679408484003733232376974176985555274781728550681341174256248769874993678456480851319719613002844012309625001012440121656031494344818365013159694792120310146385204626191256572014379925975258707842067/170766028402014897103030024233019133101588043106926917633621505909139457370123490865873680389362573550895402396826132376811854150505755073073212803239570617751466397748142404080486317536610144030060358932723161967345853806360760984223761602483330505222740935973583540366838495741784216445143942271295775349987219103276195204192994455428909087541789575238143491247977240691889152*y^35 + 443470526183782423898473513644392291983627256276273457121540941547130011706451330489443594232631570088585101666982482339625377694650068350692403969144788452038520293773866744735455277598807171069787765569757574203421345546451063980445971638961926419930295270487434755479963477399551883130498730401276706364120015898838752448677539852222513485667924749755133178720492238258719707/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^34 - 20845548942157610523519069191883306496120092693536883178972300027046431425432437321336387280920821079518889228798560891856751925565131280116267174296309975857029981099790139919378709282496138383540819152581026547671368233729387308106360171542034900625773903053232039320160055845253667784450644437432132369365511583690559260657998282802105143375610501242911074487926087384202969419/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^33 + 21496373658216896505096743274169909666964337170302660651228112039635077328547565345717659429012325575318032754826725775629877435374582794113710551227385479878346256178167284536639364399441782017740414988492265662894142765474205933113265580023562459497239057252987890797277370995480215827300863137883080254760687940721034721555979269731856500863967056663312638925028542951281849885/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^32 + 6656070063724448506362278826702842570998271994123889262140231609344502992791118699979326936902486369493542259430205847197267055820486009579377260193845795457849450171978210988895728761104637885848776724695297448269349071369800398570341327275602450638758372193666959037675624140925536504114344454389529959630885943582298887312319119791867686176813700394609380594118105154559605899/85383014201007448551515012116509566550794021553463458816810752954569728685061745432936840194681286775447701198413066188405927075252877536536606401619785308875733198874071202040243158768305072015030179466361580983672926903180380492111880801241665252611370467986791770183419247870892108222571971135647887674993609551638097602096497227714454543770894787619071745623988620345944576*y^31 - 618913931079113695749534801946607357680141885791194630775795511017548907295452201721858492726125969423665034979175954207910063774889003686267991393070268213941270877931878385652218915485258106865300786406682949712588095703177863598277172559913213368724629932021246422283384926418324338184373691249727319858280920755103341372208701976927330145985996159318429819893547049435032351921/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^30 + 2090552119629013445496546164279618646019603479642769473900689798056152189451580658630569222617136350309237809577713569679716290541936140130845924713980566558410953761046562268078324747792432930051775688560938944062684476107685329959506548537465855797110990396515662080203468874952410438629549853813124315589447619844106803854526469264776882740859040552332729465861004391331066153681/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^29 + 10859970262897774259684303964993692004389978014411315773662178566660828907742930103254822510764849279868914694486691847819078419197892648340165085238186982542251286021415899162948123346659661544684622862708914242116334640578272299850715635217694551629480498300148240721898060967693332214192346831679924636183918804734176700370640737840809118963801796465817680938292010441677125240631/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^28 - 12062867133358829568304420789480545071819206267450257763568433338010683433231370366210537390001726347278130235524830160839573239220974933434942310471559620376037582833900588459892742403431628853518539049224338914707894611596357506425062352338686915369988727832334515706526497628349670859714661592463752798489446041349313414806022365232095816808317579496847548074573863346890647196923/227688037869353196137373365644025510802117390809235890178162007878852609826831321154498240519150098067860536529101509835749138867341006764097617070986094157001955196997523205440648423382146858706747145243630882623127805075147681312298348803311107340296987914631444720489117994322378955260191923028394367133316292137701593605590659273905212116722386100317524654997302987589185536*y^27 - 33201212921766284999279797213329576081940671334316596620290657126237692063165426523428752454435250537494094731143764305088433870914832729336193058710843704936094191103169384946190358631573507871984649813415409706272522955933750265862773410688313046046187684901110411134668519932432708549605529201642548484884650793329936695001077849731692614281563593283440148676049857533053842147657/227688037869353196137373365644025510802117390809235890178162007878852609826831321154498240519150098067860536529101509835749138867341006764097617070986094157001955196997523205440648423382146858706747145243630882623127805075147681312298348803311107340296987914631444720489117994322378955260191923028394367133316292137701593605590659273905212116722386100317524654997302987589185536*y^26 + 40142383798988751135230411933135806043890196270341803043767449168323277439148793847482670742389334517702141808978897573893490176841156278342596767144888949603447756562813017916728057673726772229565271921436383872663272080375164246779601890598170421242466287817599356335796916255717342516437193196201846967995266555716399583321044854198167757574909924025356557157543013130304584942455/85383014201007448551515012116509566550794021553463458816810752954569728685061745432936840194681286775447701198413066188405927075252877536536606401619785308875733198874071202040243158768305072015030179466361580983672926903180380492111880801241665252611370467986791770183419247870892108222571971135647887674993609551638097602096497227714454543770894787619071745623988620345944576*y^25 + 133204786548616660140673909433646761887222294823320215154305069462923392932235621794991628017589492586935210258515585280562058383203356720689395370856819362284779571699906949802924595590726790160445139945122110518961402274513219909112398558609277517364453032222032450681940530072017958756173501885411322136950033756321456808011845867703985058141469025899020181494446613975609553965361/341532056804029794206060048466038266203176086213853835267243011818278914740246981731747360778725147101790804793652264753623708301011510146146425606479141235502932795496284808160972635073220288060120717865446323934691707612721521968447523204966661010445481871947167080733676991483568432890287884542591550699974438206552390408385988910857818175083579150476286982495954481383778304*y^24 - 565316598764799508086417201558474976850753523420880689212713583419333114930942577633873522251223033955147961451277577946100012138345333584888450234314398453217315341624150799454481733128089328061206295793316737989402847563922788427966145654552792236998916229865444537792161196409389521279128333045772375492746040117831202183155308312763829490072932239831359024166413879644711647560261/341532056804029794206060048466038266203176086213853835267243011818278914740246981731747360778725147101790804793652264753623708301011510146146425606479141235502932795496284808160972635073220288060120717865446323934691707612721521968447523204966661010445481871947167080733676991483568432890287884542591550699974438206552390408385988910857818175083579150476286982495954481383778304*y^23 + 68906477851149435560461310001738358704320578609244244548081742420717069702176223368083105980111235532028550854354637237948806066793860699420004686474071113216546887197827396727014188477841777832588607281791590467269498168335231574797887124475876507230973744600936483101832740520706399992718400809745841089122917699383130296117891653646186875882289906417372516982640487091581506392861/170766028402014897103030024233019133101588043106926917633621505909139457370123490865873680389362573550895402396826132376811854150505755073073212803239570617751466397748142404080486317536610144030060358932723161967345853806360760984223761602483330505222740935973583540366838495741784216445143942271295775349987219103276195204192994455428909087541789575238143491247977240691889152*y^22 + 223327880557725147196617463370185752595911945715079385954830476271952782771944202116413091758502912881289500594655320946294096615080726074616038620940059874050020730016649694307613994493043631508831847644152466588493388665785370493619067195796248355322372943869663404849896531536659523613937357764039472838307803187755638229259664646144187276930829412446287722740762043321239139414381/341532056804029794206060048466038266203176086213853835267243011818278914740246981731747360778725147101790804793652264753623708301011510146146425606479141235502932795496284808160972635073220288060120717865446323934691707612721521968447523204966661010445481871947167080733676991483568432890287884542591550699974438206552390408385988910857818175083579150476286982495954481383778304*y^21 - 9397022045900589603320659189886645732801987107883697833679179667633787606614672198334140576016459477676619518500812469539436452535287765535629737270213484940211044153723096805024816165374390857728141593208472336474960057993131663536646718339625572520603520937796909767695812066602542742345476989056217878767100386275169662532647382970858294814406240055115020001773302624620531568543/42691507100503724275757506058254783275397010776731729408405376477284864342530872716468420097340643387723850599206533094202963537626438768268303200809892654437866599437035601020121579384152536007515089733180790491836463451590190246055940400620832626305685233993395885091709623935446054111285985567823943837496804775819048801048248613857227271885447393809535872811994310172972288*y^20 + 2081634364797737899239428642295318728801389776474871918288966473231698103464083506081490185364054242915007269289872474310020825859036774325943461363086185540210586714962764472101694356994403189830470725444643299220517620657225516984159761649081007986151137686009519293592832940784333287530162210054774922830218849577607595986926896439976256329113977813196423626292317849709335668437801/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^19 - 363500337345608644425676781940677228987760659723914934491497830966404798968008021101408930503150432672946462489663975601425383368117749791967777660060800385468716500146525466745165615620566771912732707669768428276543416896932672306836030694044514286940045984729999533726547357273145887271006661098330094798124484190219018587207601361954038538117087034723359194643501205323928874882563/113844018934676598068686682822012755401058695404617945089081003939426304913415660577249120259575049033930268264550754917874569433670503382048808535493047078500977598498761602720324211691073429353373572621815441311563902537573840656149174401655553670148493957315722360244558997161189477630095961514197183566658146068850796802795329636952606058361193050158762327498651493794592768*y^18 - 1831414002009612329896180675203173437269836752868545201927075024771471505223552779946618090353844177515823932322935182562523888978995349928322437887559417003662188476346082267285767698823786820218489607719516312800500125490929025496786029937615402926287497961121699985697796509920526411674642627585579267939953708974430579198618538016241771726142311027691207669067230415331457763932447/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^17 + 1242026258059765803761664935577890309676061134478705579958371706768501614899645001859316426648874240233289777779828006143696668975837737522307582570971564029099585634285561040993879828478857037091285194171995310231609246227511785349579720342888537938303699324600947782667378376729609957310393278579698200830389789208069146202253302360414371139061539453537682014600758951983318504395105/341532056804029794206060048466038266203176086213853835267243011818278914740246981731747360778725147101790804793652264753623708301011510146146425606479141235502932795496284808160972635073220288060120717865446323934691707612721521968447523204966661010445481871947167080733676991483568432890287884542591550699974438206552390408385988910857818175083579150476286982495954481383778304*y^16 - 27313398602769958024212434290139445362421877253934021272042586790380278249659544147532052662906692181106476793250458783545835512636356146105452503220022819838346732722286430644212152410522614743173997346938644248665657983115620926379302947313493370473038960232025379894489367896845934793319325007305043878271409277386127433679810745028194671688463297708445210069121955261889784304255/56922009467338299034343341411006377700529347702308972544540501969713152456707830288624560129787524516965134132275377458937284716835251691024404267746523539250488799249380801360162105845536714676686786310907720655781951268786920328074587200827776835074246978657861180122279498580594738815047980757098591783329073034425398401397664818476303029180596525079381163749325746897296384*y^15 - 79216584086203584885759210677821026748559714172768567260200466145846727923782209953861838510623721613290014105206897534398012623948402776769989121802566632796415496008210328115608536828711957878526644483037904492287981168334761215497727453784788423658098529688091045246105245725358583845433905267045602343619930489834040596513782662123869225351763241121072627074319920723118682895063/170766028402014897103030024233019133101588043106926917633621505909139457370123490865873680389362573550895402396826132376811854150505755073073212803239570617751466397748142404080486317536610144030060358932723161967345853806360760984223761602483330505222740935973583540366838495741784216445143942271295775349987219103276195204192994455428909087541789575238143491247977240691889152*y^14 + 713006824169604691651650790335515459248156607508802028479806542231846084966091135401498357187339517863843700923239454938974425852566693711585169843328587083070593423870143605608862013015841328874562647950085919525166580309657351784241511635811670379256001474913224148601894933878930800895290495122243068843589032573315153420894185064475425628770113762667792934148350906895014452399001/683064113608059588412120096932076532406352172427707670534486023636557829480493963463494721557450294203581609587304529507247416602023020292292851212958282471005865590992569616321945270146440576120241435730892647869383415225443043936895046409933322020890963743894334161467353982967136865780575769085183101399948876413104780816771977821715636350167158300952573964991908962767556608*y^13 - 122889596212970696311090295149078969847630734064950758371044895679569831695328593959302605203249957077161706431149328908197111123871425557281639225823882916622144973387599256183253919378821497980211745465608090206211435090298036153038244770032972916449105473826774893958718746923475550547320872929549952155329941529811149788715090641987424543042609468812104800432114159558957088286425/170766028402014897103030024233019133101588043106926917633621505909139457370123490865873680389362573550895402396826132376811854150505755073073212803239570617751466397748142404080486317536610144030060358932723161967345853806360760984223761602483330505222740935973583540366838495741784216445143942271295775349987219103276195204192994455428909087541789575238143491247977240691889152*y^12 - 5856794543168529148226866092888984624437326898658188658255581914901928963804927954633385401402431213217925193166374911590351594518530350992716314986838845379327671163569443994874677600840801562797571902245765570790153541826105954238048031161893975534223489716938893983342608766939188930814990381978503450754679743160512729917759022696923601475682688040606811452731296139050476188021/21345753550251862137878753029127391637698505388365864704202688238642432171265436358234210048670321693861925299603266547101481768813219384134151600404946327218933299718517800510060789692076268003757544866590395245918231725795095123027970200310416313152842616996697942545854811967723027055642992783911971918748402387909524400524124306928613635942723696904767936405997155086486144*y^11 + 43611528070012051585459693600615160362901160719714587045620791257300723999525630127010061195027133986071494557411527878348979471843947626614831248551483111219781183379023937424278493931874579792546992396893810556450717869546643989778900513419227660582655279146722589948486838437534541391074696691839378449177780774971328132992836228263176890886163477804959507535642048864537923988397/227688037869353196137373365644025510802117390809235890178162007878852609826831321154498240519150098067860536529101509835749138867341006764097617070986094157001955196997523205440648423382146858706747145243630882623127805075147681312298348803311107340296987914631444720489117994322378955260191923028394367133316292137701593605590659273905212116722386100317524654997302987589185536*y^10 + 444840263842044887412993646094355129178319148849562333318928594318805345103062160851886931676079067399815053525257475121451271510743159335038408309489497304804389743274540118484910384619778373242134708779440164545755540982569607023981916437398600344039727432484215027163487721230236396421359156695975678156781563002975277244060673529290116536044019168357312723478155974655983178119/170766028402014897103030024233019133101588043106926917633621505909139457370123490865873680389362573550895402396826132376811854150505755073073212803239570617751466397748142404080486317536610144030060358932723161967345853806360760984223761602483330505222740935973583540366838495741784216445143942271295775349987219103276195204192994455428909087541789575238143491247977240691889152*y^9 + 591174239168306163180782390893300822433798567027495985907490328661525755867353784988750859582390161315191341782454246940611036012074056861804740676328755135478654786421669052063876012714033206343717816104107318352032147211554184212758568855888846180978728213060197879271493757858104058213884952921772077083551029913593864257964485035139705810037611807870879789504327800941996308625/14230502366834574758585835352751594425132336925577243136135125492428288114176957572156140032446881129241283533068844364734321179208812922756101066936630884812622199812345200340040526461384178669171696577726930163945487817196730082018646800206944208768561744664465295030569874645148684703761995189274647945832268258606349600349416204619075757295149131269845290937331436724324096*y^8 + 163121283835817378584928735419366990078498615798534310380048323021092637206696388093428180913494234941391325105671444323246932056033951194569881704532659139055074746865920704445788497753037814321494668974057262896262007940234665115388200573146278882686533058152848442624937098846160726075881938894031549379590634437140048411246726875320326829358674958645088559933434296305607823993/21345753550251862137878753029127391637698505388365864704202688238642432171265436358234210048670321693861925299603266547101481768813219384134151600404946327218933299718517800510060789692076268003757544866590395245918231725795095123027970200310416313152842616996697942545854811967723027055642992783911971918748402387909524400524124306928613635942723696904767936405997155086486144*y^7 - 429585430339523714333007678477031233129695019796061038408525821093168923175587886393287751883004240729927003037601135125304189352538387118990596561636263652993251565384590904548252228278688946726177588866608744244630228181061022729714081659628647175365390433859068772170551028388353982447109863251620655630370275855671634112666586592821614972921789952137809619419488806252318679765/21345753550251862137878753029127391637698505388365864704202688238642432171265436358234210048670321693861925299603266547101481768813219384134151600404946327218933299718517800510060789692076268003757544866590395245918231725795095123027970200310416313152842616996697942545854811967723027055642992783911971918748402387909524400524124306928613635942723696904767936405997155086486144*y^6 - 23803922739916818473143299732216648558854286283541517806577937819429487440261946943904899350525996087099359931329744638745709641306863491968932870656701678008939336826145339444085290605714501249617406044871834121753431478365858835008528066995641009750358374826824696848164313572937209240575310925032753190778633824786544362141320639692156877491062083686189829381100086997604308217/21345753550251862137878753029127391637698505388365864704202688238642432171265436358234210048670321693861925299603266547101481768813219384134151600404946327218933299718517800510060789692076268003757544866590395245918231725795095123027970200310416313152842616996697942545854811967723027055642992783911971918748402387909524400524124306928613635942723696904767936405997155086486144*y^5 + 12821818168142988456493974727590694212843681251638503288277407983061028995436369638712160724450704005950928868572138016610524210005915896475218514175723493449151617036901028751744935469425387855179327175915997251604989341412565716943636422782451919841565201617585158217899865873213249024616442195922240227883701364538815854895552967342321560427281984202915775759810847288254874497/5336438387562965534469688257281847909424626347091466176050672059660608042816359089558552512167580423465481324900816636775370442203304846033537900101236581804733324929629450127515197423019067000939386216647598811479557931448773780756992550077604078288210654249174485636463702991930756763910748195977992979687100596977381100131031076732153408985680924226191984101499288771621536*y^4 + 422740919621651947420927244371199516161850932999772975392633033088629702524182953419236502653464943275871497025413613197552861835799835551119909491631715792004658361387516604368996147289957910214821865491473481066101674157649024919546152696598128158145021961022030377661023881781202259830659434899639419399166557355620700135183528299555240395832870717508429700742443514518895367/5336438387562965534469688257281847909424626347091466176050672059660608042816359089558552512167580423465481324900816636775370442203304846033537900101236581804733324929629450127515197423019067000939386216647598811479557931448773780756992550077604078288210654249174485636463702991930756763910748195977992979687100596977381100131031076732153408985680924226191984101499288771621536*y^3 - 250351271485005587538860150232503852919143031345156092095138163303136983724152635183508407429873429502539419124189095658071938004196318260743736417331031572637018761713311432469577257117354684473636526820774776645924181658114113023775770970014530831576269130852301850921026469600578501649909064202833451489512072774156954095444482171218995339287696681670108693285033834276102681/2668219193781482767234844128640923954712313173545733088025336029830304021408179544779276256083790211732740662450408318387685221101652423016768950050618290902366662464814725063757598711509533500469693108323799405739778965724386890378496275038802039144105327124587242818231851495965378381955374097988996489843550298488690550065515538366076704492840462113095992050749644385810768*y^2 - 4641296193987984103904024440023176471186451204642530049129647019109130917497763155394582368991982250105198391682657097636143081159508191566566578809943410819724561866910375018801902666944678160739345236582800523401656866861064465524357281846452975332182519667283364098607545464028081331977738495049729580610248658274504048293914621860702478637394308048366222681513013090542527/1334109596890741383617422064320461977356156586772866544012668014915152010704089772389638128041895105866370331225204159193842610550826211508384475025309145451183331232407362531878799355754766750234846554161899702869889482862193445189248137519401019572052663562293621409115925747982689190977687048994498244921775149244345275032757769183038352246420231056547996025374822192905384*y + 1383205120376400368089107202993008694497889386662024883528154868434174894689047935534263776817484791823632533447603639050568223255941058171951871410661358234427628982288932075291289832501205864795668482473438985960120609791944694494803840755974591626787337517543955430318887315292436275872264670951237770661236855528036665550799361849450227655497885468862239108398295100162435/1334109596890741383617422064320461977356156586772866544012668014915152010704089772389638128041895105866370331225204159193842610550826211508384475025309145451183331232407362531878799355754766750234846554161899702869889482862193445189248137519401019572052663562293621409115925747982689190977687048994498244921775149244345275032757769183038352246420231056547996025374822192905384

# 3 Loop Invariant
15304539012707124175365454963874500149132464125146368158231768018318056240474341089769559431321982031378042516387242459411790411859793230278346245555416931588141296459703701048964870870442151843231073808830920471168880079227253052582400541556936035728300931209809823921864281240245760036354162763598538843520028373537249151307757836318630058582826353738518154982987149668085828966927772078547804659382189764115865773520210426774042515081536314295074899/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^39 - 350090443756944069003743166768556817778237253705417034690386388854259448328616950772370209109848232996182302752374129304541118933254279627558298461523995878940921862482470105732743642331503188811050495732244321657744449991774108621540878058154221150423291151277531149448650783903254863204970939525550049209197527368507862220077154184473980709559465698381239744237361473626484530051824842938657802125672339901279884741655101572469795094465237103164311741/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^38 + 1503812864922443151823070945974587077939705603239011647543975331952471476189718231790930510416702308116222179222786995228028440586949201743634645573605868170589751315338102964791527054261402736084709036944299439497446279154595578386151244722555756344198105215110159317657560903262393079698553629532600293494590427038385645024232060118775407116879575874234504551295933283368565652150470051379419112224956799761332928915168474781600298143797363689065023587/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^37 + 4036801484123059533485313923644725283600596624014930660186594962837133840161186297940288892209645884383993134613001618941861235617718965000116940244075141079580565093637732774448290546718050514607584718806294874057835915709176939727831386131244146385213283750847999259104666039792418581421642318919431158510655575043753519656241997621648501496188367608445577872809651650755796273248591749841608583520775807177906247958122254221673991186988379902189586055/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^36 - 5997389921201956871614153744056739785370947065263630544388029537967622744941290786677201456700040121366888045581615231435577624060126949987067502755684860441505751719334412096862163005578232447818977514251113168274771251261349901915596188157750511758568621221573306063148317071039034186796702339933177702572256864426415920898388997531824790597725271077958686270139436540027678330772877780742324748240289816408901923973514056394559429529186620314190630593/35306542665759434092923510853371747184988233253040598681247894470232917851013913246778883066831444017049050268544040854355867509493232234700374076386694956991031223626898449781562864130575188970723796571210754115935213652442966487732753401634494576497522960506933253327094523856309949443402354325241030918769231229854563534233245348631846102674015896038589308767821051856877435486324922052226587773025488088516747571166077696063308532064150390002647410048*y^35 - 51319519304334891277407695286240046595346888621539622706963518578766994373133134007711002567727440671733062661763861648908724750922014653336822579016993388018248163698566479933998766997370495367120616727997432615049815689361790370908267569691658958600976500522140262632084458353680385277540951729797669151130456021517623509456440170336577914949253737744477929118144897388714573923803986918245741968183176012106150823580545053930235340638814717471621911669/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^34 + 1554732309881012436075491545873358726689612992084864091022238393920709289159312358433655721889266500907244107138626609200507902316439298245798046006399638984717076076545788161963919890266225443907737971383439800966949106995594813974886768275061002475700291453391438893702308808345211526544165965247409519553349407088129198595367321802660248959372443493357759079968825848644339897455255213332691940412624863691485469153876234304627909333392827008676104048607/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^33 - 1322088041770950327701648191484156561967359533715033392018142377676740970128460769107750626216938564845405983557078127103429042217563601613698247798082448240214721850176359344507896318997384040676549781862381166471705055271899718442354552755883183235714843692611540682040967651866437584498656667788471472291365805605530708448092098779985383051504683000347611911874061934004515557075587353114000744394818412853598049537480555496308562577174454556261889613969/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^32 - 2111247342825342218968929422376973158193161512915590689924596621836026504417949815440607205917851541537600162916946379601796942850382864113981210499529893868754192306226463664188704666467848691622362334619940971884493979734837638947740253821115635489408106637239281100522808888990947766005565921400417210005775810076396994770228260328238143609926581877629260099504503271029055136857520827254864800640652232087939371175313460905109348344782709775885468680675/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^31 + 45680387446071936907666167252742297354335344991155651247508740176739509985341018964127715875416729775157795924301459520447308592621272547964819513043173448103262308088334223594470463180303133768279672728475635193526170321974169709563627088498346583488914708605412582874577426928978637138696898733611981123216525682728924381570498629085789310214056750541077583540991202714349698708261987717393486150231380144976924333588131180198993552464642082178843373655419/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^30 - 148507370282735259099096121145676613666429754649799914537442917805124375105147767555799991615025303313615652040396490958670244546903701311440273264452499244827143177088367183259046484125070799902339857713301039319109017385716372056030581040862289262060009496596517230584762928546664434385631309559297864376783786160232094034359796121761898257274105337304242005289469023224854367503670924946247780371523913951061441143866598360697677976862400149946636487433269/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^29 - 843203535430595960618581560103315466758139132167194752285581475896793800509841249444058980558470397842856468162783454280512409823096260715948182652492508512605458063738541122457734846995803477165437146349757040390959660227398767450292977693465122837469657060010340278246028193941375475658482454866667583999726668909685062574435563968856404539712499222026361345916903210150940619069081365289406184251765243710024179696240496691893916721485749823677475468981583/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^28 + 2556812817969170593858380317629251895204597214780311521953411755635997675553382713398592681728017485151389181637542638032323682095085743334242888448593359350059789531290420134546898604155386938108146302006099400645835483467003687529671105335954088957910646408951251152810699563993548862958670196166932388449198682442468611549400452424087370758615396568233446052768387445153798543528386184588852091272053835499434238737735576192839026751683673522567018388169645/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^27 + 7951468400630426083661641026764400198426972122317512502691463701192278328816174421630815755160270564970230716889240153552671852852963096286842205346241337175598766634130009563948061161670561473972980482200390811439743541410638429303386561731718215910401760676803386536607316844204688977450498347352058667394428692697395855862634754367445399550214005058811180894913520447701240475125224528962999814165790528428242494178278926034848650709838938435039687105228459/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^26 - 11289341887713988306226640144779881610214070288428068811785412706090206492297656920758775504662291559059419874908965625880017166585425105294867032296796798829227277234972665479013619863803489008713275067391262699399379997181300008445227716061163677151717804175682045429993341166303828253281410360532843472405133764041551770222756830464946402419748239126109133475391008048082477901290399613624522926593791597854108388648798585046102652320730222903729624492643487/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^25 - 12068415064580400063590934280124912668076287067287027967398881418318426373155389489308992637863329833915974645885395694142228508436304130492027034498380121419649788841306210946915693320113354059335686772639934898111042007389081265596157492606226103088343297583079051493723202514657107538322237712467922797827070293897275521754479942611979080917311603411707010890719340352864596989811202859886538468529848187349548492655913776428749813164336266636942205792113489/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^24 + 39992202020564501006585058929765798273997040343664802653303932308972605640584263924743496397944053488007444779841136524995644137126720765757061385685444669951453457179512428066837970874569636125043444053676131432174833960177009849570978785568031105552771944890627637070498825913498303614398273737285918412439520473925783969814474071587123097775433592173256204550342080906277735870147457896710996396631744880582743649042299542994585035118778895237674671585684805/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^23 - 189618358860439713434901974229025886124849867846823500593111869757418758841529640194006164201801082092594186189590617312048868867042550226064963299693241867609744639265877362579680243473416888876995690607507479020920035984752426633030918002388430673027721791220546282746338518416392464060739529353699607227650695408135679167201096489817064246097737932720994997142503456913732528418453321948552732971112716608091657934482707108199783977893541290406654198223769/17653271332879717046461755426685873592494116626520299340623947235116458925506956623389441533415722008524525134272020427177933754746616117350187038193347478495515611813449224890781432065287594485361898285605377057967606826221483243866376700817247288248761480253466626663547261928154974721701177162620515459384615614927281767116622674315923051337007948019294654383910525928438717743162461026113293886512744044258373785583038848031654266032075195001323705024*y^22 - 16653630007675145460989634818441163433567731696005558933427753544552693793110404812010121414301859981100210679892963199407534476904600101127344596267929560371839967071675369265264358665805308878908624101616216662671207986798917621400121661227004331899644757690343557196871563698692923584822446162406780135092363479514662169517450058598121067745829533090139432102404404018383731088159415882505316971779075057589161879294351916643335638471855938911859249632920739/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^21 + 1271721957002393938322924622016657805238287229659244736035872016721666966413985878528496978512470075979564171816148198360978276966581841143416522560211754184045545686656434737213422148375417716468000714259106361591814188905328276022191314766578490877320845423091968126573584050786727610685290916306424847869630606984397863147531761365484769322543164787997586180468148293778495848195110062637081021711598031249289292540626722569139596742409137907104320850602167/141226170663037736371694043413486988739952933012162394724991577880931671404055652987115532267325776068196201074176163417423470037972928938801496305546779827964124894507593799126251456522300755882895186284843016463740854609771865950931013606537978305990091842027733013308378095425239797773609417300964123675076924919418254136932981394527384410696063584154357235071284207427509741945299688208906351092101952354066990284664310784253234128256601560010589640192*y^20 - 155966274959745201524207682143473936119888317530829073861748672187255337157140365788948969003712290296262989829721354779178559889424395041211424710839553661156360485288320874225200569680465985232240724312549882426997650399913260796622035070654857360113325067420777133778969517738642290302299802967957811533915959946936834455245003776562022964188326598132382583026561354068852212501015645747669208777505241430462592381898183246808854493758630436332761017538346191/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^19 + 33559820980599343009553666651184866016599661168966706068646273935862724686867112911399216116709038409889958628999858964580533132611186806671465430630417561427479433707645060741332670192895971933753641661628240104003521887424281547051214248842667281327314504271061785437984219807326079360379214510760407265652880586358873278569791174034173989538871904974363075495300036435279803700227044889460887382884169974342801939845248925543093380159905874131367544240946523/141226170663037736371694043413486988739952933012162394724991577880931671404055652987115532267325776068196201074176163417423470037972928938801496305546779827964124894507593799126251456522300755882895186284843016463740854609771865950931013606537978305990091842027733013308378095425239797773609417300964123675076924919418254136932981394527384410696063584154357235071284207427509741945299688208906351092101952354066990284664310784253234128256601560010589640192*y^18 + 160046887910960685999552852359560636144434087881696280741524017488589107435413539768357620377852927198545623337448057058021711531070820201058422818163374863677765367835811599850269809246420611461243218762069509051234010365797386282835434592180708098290657435356805661121886755601048888719642114416449228820219190017694630758169598991001552448424876328632111500347577000788700295194007449746184114531095446739072643226264174408289816163752318751749495682207145529/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^17 - 2409718852116400630781646581993619326144082366030941069315959590825843550745639578055274274283559740741038105130314506105260900423036637450453024611880964825602235710124514632647192726434522339885116618149921905066428422330862593264067411615178654764827700019258273532907675201359091132645123733748517270316828801804400321230367981824014660052230817785972940918734797006083071290651368499769798982434929756210342168473345190694191334129662529985648135086941285/8826635666439858523230877713342936796247058313260149670311973617558229462753478311694720766707861004262262567136010213588966877373308058675093519096673739247757805906724612445390716032643797242680949142802688528983803413110741621933188350408623644124380740126733313331773630964077487360850588581310257729692307807463640883558311337157961525668503974009647327191955262964219358871581230513056646943256372022129186892791519424015827133016037597500661852512*y^16 - 337654949062233223873290186464504360791273224693207717849729600809578815782938733839432648701295753422502769209004860506535713718664004092259394227652851963140608153463186970849117339315831715527884745990681450264017785859369888615425886509947794363991732060347288616092994984916198557038908612760134477198334792654200987112005586707570693461500414787758199081406094893314578282474653751000006315614869194606754319587696913703713230068456838300097836529317025/141226170663037736371694043413486988739952933012162394724991577880931671404055652987115532267325776068196201074176163417423470037972928938801496305546779827964124894507593799126251456522300755882895186284843016463740854609771865950931013606537978305990091842027733013308378095425239797773609417300964123675076924919418254136932981394527384410696063584154357235071284207427509741945299688208906351092101952354066990284664310784253234128256601560010589640192*y^15 + 5373981441425013496111542310871413713554785939711371517119339559298112420980087559837663215723685542758073125853589700434151728819187141576381822176503784288674534549003617163806970973689873718942329137611529698221683986459614500600619028974486974725677538844432344262939956245477747654975317859996320907115224942349593239543012206205084648673644740044096882170514707865571277610783852823684494468768122146493435359493667172770360214970705373581095652113031055/141226170663037736371694043413486988739952933012162394724991577880931671404055652987115532267325776068196201074176163417423470037972928938801496305546779827964124894507593799126251456522300755882895186284843016463740854609771865950931013606537978305990091842027733013308378095425239797773609417300964123675076924919418254136932981394527384410696063584154357235071284207427509741945299688208906351092101952354066990284664310784253234128256601560010589640192*y^14 - 49838278128609033829935218170831051192102868612004788088905907693027877103324970348417743847652109576679582362682194420099652863036230278434629039285958156498572073055317988055497035990811322130896309451692317753878590240448923345140854949890841335200859055886265885835227468578867729777621632000493156516821809460274273501795560226366087366141823701925497831126393325616756385799644560068550326286101714054155396762936062092297448971550996727350368103627194271/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^13 + 13763987496066501491203431851502914830433672191712908699687584920641722559255603358355990865128091681114838016570047011312784702850785742068680102729756760363165351077440406627025188681922545481764348348915488137221884643566188011068370895802679704929596516864004743608580519364781089278149565434462443837249729554234084743034732184082312831989093182047324193114026272039761903594455496778389871695458188289298672669250586083730062120638485426740669035322724637/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^12 + 4611193126905620757320173808999743665257757512247886730983126733683057425651026143762808578650676314564622964685391789092745734373759807837488728184779198431996073481719031180596123588468172136072873078718173945653941270498177479970054308396959512145987677486483366648700724223379893169606822875156483919824111013180681145270595993588632723550649261265250210407842761210017505978004165467227265404798651652830033783699640886436937727904794344881863215018167199/141226170663037736371694043413486988739952933012162394724991577880931671404055652987115532267325776068196201074176163417423470037972928938801496305546779827964124894507593799126251456522300755882895186284843016463740854609771865950931013606537978305990091842027733013308378095425239797773609417300964123675076924919418254136932981394527384410696063584154357235071284207427509741945299688208906351092101952354066990284664310784253234128256601560010589640192*y^11 - 5982216463855500155805039725213816013482463597455234191355802656393017917787376796680853820623177854336658492012201365899289212499661280752508865198358385251976524801511116516850254351800759790257142349162609091577881147261420546224765298544400799699938550314142569257018652436311863937137472689194823879333459852262623167535189335542081542808235345229708271081753816029713905262348200589250023467406876188602731013854452125425341076338645729442068047155331393/564904682652150945486776173653947954959811732048649578899966311523726685616222611948462129069303104272784804296704653669693880151891715755205985222187119311856499578030375196505005826089203023531580745139372065854963418439087463803724054426151913223960367368110932053233512381700959191094437669203856494700307699677673016547731925578109537642784254336617428940285136829710038967781198752835625404368407809416267961138657243137012936513026406240042358560768*y^10 - 445660740736839486120870264895376231199322399279517057203432555312607853630053152026173898759211623250259589881591289413452689542125704451951029045309767832209294622805639882692349921814646190838774572134966727920971446170502142996459304352053723394965287994152868077798629501380886960108470341603939189551365845549154739050904902245262981975098249703208270207365588591935356662713264177700856947877070118440165103849859313885875942648006700957273465673540929/282452341326075472743388086826973977479905866024324789449983155761863342808111305974231064534651552136392402148352326834846940075945857877602992611093559655928249789015187598252502913044601511765790372569686032927481709219543731901862027213075956611980183684055466026616756190850479595547218834601928247350153849838836508273865962789054768821392127168308714470142568414855019483890599376417812702184203904708133980569328621568506468256513203120021179280384*y^9 - 567022900116590751739167479871516642967168848957017655281009239474107598783716417488132215675795024388177832338921549873706007217620429742637053750184330516292465826258071460905511770118435227409506026312801870442144322814064083454996171828406299434826096512249579857857911741812760286431785905969267056723327148754247443301934498660251836868200442014826344479810370214566538348150403396713597286772239043132239370095112765052889553313899780342607578317276607/141226170663037736371694043413486988739952933012162394724991577880931671404055652987115532267325776068196201074176163417423470037972928938801496305546779827964124894507593799126251456522300755882895186284843016463740854609771865950931013606537978305990091842027733013308378095425239797773609417300964123675076924919418254136932981394527384410696063584154357235071284207427509741945299688208906351092101952354066990284664310784253234128256601560010589640192*y^8 - 103799649287606376933178101820422152183242169044302783623206948937043289210980440245630943402960936945470569358462336756694511870577759646406423819185214520579870928727111472926542220822594908426183368974120458638216978959252194500783609238752644640292924763088364569042320191206761249987112703319790340266405329587165401899813826172622879315130632009523540140952818407664450327164249705198698009803564334306224851412651027530500932055104813120155375200522847/70613085331518868185847021706743494369976466506081197362495788940465835702027826493557766133662888034098100537088081708711735018986464469400748152773389913982062447253796899563125728261150377941447593142421508231870427304885932975465506803268989152995045921013866506654189047712619898886804708650482061837538462459709127068466490697263692205348031792077178617535642103713754870972649844104453175546050976177033495142332155392126617064128300780005294820096*y^7 + 51468519102965436212200717485091027120012056848160449179474831716395144031069721467059854626337545812768281179912505261894496513206166917530531392232325067501422698932502089563567914725987388544626293589579942388261853144443122840562218889144732566328407634291073524975976060281549507942849453197501395281978469782902877986393444964888157614356569388144871630963157176480321972800111860393420732790467483699768786778049360802697367864418778011496843172807593/35306542665759434092923510853371747184988233253040598681247894470232917851013913246778883066831444017049050268544040854355867509493232234700374076386694956991031223626898449781562864130575188970723796571210754115935213652442966487732753401634494576497522960506933253327094523856309949443402354325241030918769231229854563534233245348631846102674015896038589308767821051856877435486324922052226587773025488088516747571166077696063308532064150390002647410048*y^6 + 5792838611693727183296079690562171218063537540281832731218049287756626312620190527450508459668464407501556820862310090068282224786572926482478424187204660661640880550432230168947668688561940418262725217105583124846849801448883752505454343514469534066769404110552958490089868924508716779849461526263275404164886291509878187423056048634977211930588615150110770846203930168137230001484559670366342542921942835443545338847612972634219137701799209205510935122237/17653271332879717046461755426685873592494116626520299340623947235116458925506956623389441533415722008524525134272020427177933754746616117350187038193347478495515611813449224890781432065287594485361898285605377057967606826221483243866376700817247288248761480253466626663547261928154974721701177162620515459384615614927281767116622674315923051337007948019294654383910525928438717743162461026113293886512744044258373785583038848031654266032075195001323705024*y^5 - 1296151310161414074109633443031036401873693409080300906635632973107803285536397078253277623101470714482125589547396267680010047966235587176716673320560414123457368447982609030166888838436937057381516262422958686388020025714304832831845181076051774434268162763351035420720282342087202281984183509801500904332084024735904493551444792420364513507961888130504716105240649357676559980388681026588892592714334987663020412851259203835962268555846311097850018061355/8826635666439858523230877713342936796247058313260149670311973617558229462753478311694720766707861004262262567136010213588966877373308058675093519096673739247757805906724612445390716032643797242680949142802688528983803413110741621933188350408623644124380740126733313331773630964077487360850588581310257729692307807463640883558311337157961525668503974009647327191955262964219358871581230513056646943256372022129186892791519424015827133016037597500661852512*y^4 - 117484983466783956485672552267943103276035654742843007285570673049406487267272182435357499126776941026076905832323624142390868544617656427030705558895511994514878544010050423063002046303492932235919734981586327283694931720163575403346116750445060077372259758161246367176705549448933567448872666823793621925772042516592198538995845807818143693199578799229799365999659385491328057469007339849305006434144916261375785366948161264516817801575482847394427788147/4413317833219929261615438856671468398123529156630074835155986808779114731376739155847360383353930502131131283568005106794483438686654029337546759548336869623878902953362306222695358016321898621340474571401344264491901706555370810966594175204311822062190370063366656665886815482038743680425294290655128864846153903731820441779155668578980762834251987004823663595977631482109679435790615256528323471628186011064593446395759712007913566508018798750330926256*y^3 + 4449652616008070023985793447377157286199582709828169940381659501921527151988362377119422258984662629848540003445387085028790893994994912594552583623671360227175930091804178074381493703100050064882264523319751392899423010244460532700495257937151203964444811879426269180132973298383641380246636720452174668719497644893591100772897726587952079470390327120053023591873424624717734200272863716888888183198556472869893239213056046535018420662075509880664380433/1103329458304982315403859714167867099530882289157518708788996702194778682844184788961840095838482625532782820892001276698620859671663507334386689887084217405969725738340576555673839504080474655335118642850336066122975426638842702741648543801077955515547592515841664166471703870509685920106323572663782216211538475932955110444788917144745190708562996751205915898994407870527419858947653814132080867907046502766148361598939928001978391627004699687582731564*y^2 + 449592676831858209849847982498962027817821095073894553118827259566091251196816604624261481307859890728331876471638374114612549596698865935545610796537798249375879538337389885436549118987635958551099709267429598672950974884184336770774966340989333169707772034493310127973801414027546903787749622221863039654378419143081482731572779030260595554628123874924150093035615299395369546829430190572436661177594004284745608941351681230935595599490519113208962679/551664729152491157701929857083933549765441144578759354394498351097389341422092394480920047919241312766391410446000638349310429835831753667193344943542108702984862869170288277836919752040237327667559321425168033061487713319421351370824271900538977757773796257920832083235851935254842960053161786331891108105769237966477555222394458572372595354281498375602957949497203935263709929473826907066040433953523251383074180799469964000989195813502349843791365782*y + 17565984869981287767781604099303826942957831988103695245114880481910651109056064384843995420336438096278990323852459363552594260774528395074767810893297472248438800801654044649171395458439706152615443334120926974630454673420819157190986368288395921319406101061497354818885608598326150457472782083633690080069821674088432497271991985360210276891061487945233582083676460444766087883633498745965157488485573258597222518710889815220007911326961775700438721/275832364576245578850964928541966774882720572289379677197249175548694670711046197240460023959620656383195705223000319174655214917915876833596672471771054351492431434585144138918459876020118663833779660712584016530743856659710675685412135950269488878886898128960416041617925967627421480026580893165945554052884618983238777611197229286186297677140749187801478974748601967631854964736913453533020216976761625691537090399734982000494597906751174921895682891

# 4 Loop Invariant
8208057035194711891965545396723673707765753036116796369402997695143823451010637125830915890854197255322666458837367337989898925865947262981354559894075468644338975204815043520397756100250209816276691742564346277492566928915453310269767571816867970192314234401033135325192845267092427078610533347240219316481906800688131770404818743565639713117619851540008580753802927608588153016468539180527349516675405337822390336402957173115833300683382766286430239974007484101211031656333516135246653640499658573834501175109239068323594705394289784420592503775155951010976638523399543777955642009475122334167857224008210823/156479557361514486813531978395662203141172148225683041022229175442235229462047233494393647075292553224410270663213639620813658784458759498152510161688970142394862933822108034586139092199082803863558135308169164260949467937813824579427080196899082555729683723821976053802739449652251895319142472683531599895730182009440901045430538443603630468350106491597213572633927879877667385311734900979481760619530150192587095301359397325111667970285504307709451073197760797333919160705934999842770132288674387689148360331911706608370413053335547158398302220502378306413994427188683842708408093467079078760676165505221143088640*y^39 - 2956538720827040295697507919204074737734051972447663877961567003378306453978287319010024124903583536374359136454835020618976801593400551906504387387424335242030531025727346123567913262030992761868404628589667660488575973001348601959951436993602555549274084707719276866160730388871439798028209823332447697844535324177954315764860254253231337091543633473326738689844007968856469024197693802180699447630482894679636808118304475840020234235358626579382933208518151786545664756219307254719719239658839701599659933346414550300755571860021889707688147283117744706977353326018474698173138092094740039536088900682608373999/2503672917784231789016511654330595250258754371610928656355666807075763671392755735910298353204680851590564330611418233933018540551340151970440162587023522278317806941153728553378225475185324861816930164930706628175191487005021193270833283150385320891674939581151616860843831194436030325106279562936505598331682912151054416726888615097658087493601703865555417162142846078042678164987758415671708169912482403081393524821750357201786687524568068923351217171164172757342706571294959997484322116618790203026373765310587305733926608853368754534372835528038052902623910835018941483334529495473265260170818648083538289418240*y^38 + 2363505692471509311425040140314207192607330454741790876681483693026270327656352089519250635707065506526421237909907898588378041763086825481767140803455482327456323738554174644783946625799745215412178442818334152055150143032709681060290308359388694954362959599570665019273027359607938136035307017018887562138005893769670469291590607522751361268528815494292738374148408535195866350525340645499067316105332581334515738435500369707230859071835109336221780844402485694554513187548230762154597473702073865911324703773449977354577625946469659178248570102489739498505239944941399559991186328046560044259966292376244367819/500734583556846357803302330866119050051750874322185731271133361415152734278551147182059670640936170318112866122283646786603708110268030394088032517404704455663561388230745710675645095037064972363386032986141325635038297401004238654166656630077064178334987916230323372168766238887206065021255912587301119666336582430210883345377723019531617498720340773111083432428569215608535632997551683134341633982496480616278704964350071440357337504913613784670243434232834551468541314258991999496864423323758040605274753062117461146785321770673750906874567105607610580524782167003788296666905899094653052034163729616707657883648*y^37 + 24636829485678537719514871886992506821181278013065023212590179916849511998869188826449763341141329717897502726953349435774620554613646522329580745084821898135149839806705353739033057799249191010486023235775789355644946013977453762711644434316618223785222555668643692049402756239984436637165641049496267073468968088032973053067046487357628111326751307893342848845315841771262176759634283558110795908174089032977755943508779747128047702791120694258332728869849526169045030141574168289819284860999731230989793468156854616086324495241533176634876705092551236706701475957581883580695433897209360910588440881231935763317/834557639261410596338837218110198416752918123870309552118555602358587890464251911970099451068226950530188110203806077977672846850446717323480054195674507426105935647051242851126075158395108287272310054976902209391730495668340397756944427716795106963891646527050538953614610398145343441702093187645501866110560970717018138908962871699219362497867234621851805720714282026014226054995919471890569389970827467693797841607250119067262229174856022974450405723721390919114235523764986665828107372206263401008791255103529101911308869617789584844790945176012684300874636945006313827778176498491088420056939549361179429806080*y^36 - 33256324915228629981223045777346311955452063464610217767773098634641470582080301618874742017401824726830051453059234166606785905122341724753983664338857736390380172095023864193460083765697639302659827742763482924963737705405127676089970487856212918111818967198557400628613394508152590754092287068871541041544040650547107500493239021678936040787075742769081505424783727981215732560868942844021680929051953833081073408007225831737143947881118510286701829185919983131262859854752151475588574870931899973761018648119623696713106880063763428497110715241138750231180134556584119355261871484951290032171657419114013658039/104319704907676324542354652263774802094114765483788694014819450294823486308031488996262431383528368816273513775475759747209105856305839665435006774459313428263241955881405356390759394799388535909038756872112776173966311958542549719618053464599388370486455815881317369201826299768167930212761648455687733263820121339627267363620358962402420312233404327731475715089285253251778256874489933986321173746353433461724730200906264883407778646857002871806300715465173864889279440470623333228513421525782925126098906887941137738913608702223698105598868147001585537609329618125789228472272062311386052507117443670147428725760*y^35 - 61457575859029548267046955444568092662120317622159438406160297025630007603608557081609013635420778901128551347747026385923050667161677384696164563774617673400593082880575348219162873562953287651580031719399476859521613216789292978625081568972643251508501857422478305658174270320794941520499972769967815517140665901872528017611242019891225802072771448093623853993155944937637397589634086722711536785984532869037961717748906644997085538387973029042702425392548253939943620163102443358676239681013830091248198973526813539429289052052439056590779438562786220410018355164492766159907587556020419314331591289668486360559/208639409815352649084709304527549604188229530967577388029638900589646972616062977992524862767056737632547027550951519494418211712611679330870013548918626856526483911762810712781518789598777071818077513744225552347932623917085099439236106929198776740972911631762634738403652599536335860425523296911375466527640242679254534727240717924804840624466808655462951430178570506503556513748979867972642347492706866923449460401812529766815557293714005743612601430930347729778558880941246666457026843051565850252197813775882275477827217404447396211197736294003171075218659236251578456944544124622772105014234887340294857451520*y^34 + 13169425904802366887946893095418111702578642200917516242575315145971911075840433243245978830692944853038231291864442881896637227839578957890252165360072927649724276097600986413287865773391462749460822210564095731206741006350566949188608987619446205225167574315746340116455806932045250054139820911609761511043827089514302318994769509199874518508434885705846136111285618676465871239141149499701992271508942449992777851881976206247925288693725354282613891644434922734132188287556061934856225600825674169962413449743031280560829462662656240207271465236448940186242224650473222320522200703633043418778502224270135143096929/2503672917784231789016511654330595250258754371610928656355666807075763671392755735910298353204680851590564330611418233933018540551340151970440162587023522278317806941153728553378225475185324861816930164930706628175191487005021193270833283150385320891674939581151616860843831194436030325106279562936505598331682912151054416726888615097658087493601703865555417162142846078042678164987758415671708169912482403081393524821750357201786687524568068923351217171164172757342706571294959997484322116618790203026373765310587305733926608853368754534372835528038052902623910835018941483334529495473265260170818648083538289418240*y^33 - 2176876569530304057216996573616846997256369179816646746775247270250076025891008832018393416865144113503833854356047070449356778514151120537358699462573115411038568212796523076510558878280601833132444979509328858176304394450695156361302864986580653395220902429346215441087248361634558783624569869779983335372990245987945782598870290169223942463998646185108328962873216376167479746413437394435878814844046907726269068946475188578716735447538704565607312029238381239654669273289579518667806476528922504549227170298613439798245226428062236490094616290006285085434204564106248629724311388859373907939576649837157496811471/834557639261410596338837218110198416752918123870309552118555602358587890464251911970099451068226950530188110203806077977672846850446717323480054195674507426105935647051242851126075158395108287272310054976902209391730495668340397756944427716795106963891646527050538953614610398145343441702093187645501866110560970717018138908962871699219362497867234621851805720714282026014226054995919471890569389970827467693797841607250119067262229174856022974450405723721390919114235523764986665828107372206263401008791255103529101911308869617789584844790945176012684300874636945006313827778176498491088420056939549361179429806080*y^32 - 40139643041292839246075470901908904501695163522964297254027801928183840078763938416665350863534348502822125606708526615208528142036013812215903903796332604567466423258796070645706641421356385323487491141849442358030555713311331562485779646422070269331307293992487334943952156348506536631973522292325287337629572857502534363030602619015744827064901598266029688318258538459762384321238101215875238809657758992325566383579025120800459498300010556715669327399877725150911851971092079387050450949005526110574658817835011217173088113685082416058752043291919466180270680236577546797875775046407538006652434394775670513321549/2503672917784231789016511654330595250258754371610928656355666807075763671392755735910298353204680851590564330611418233933018540551340151970440162587023522278317806941153728553378225475185324861816930164930706628175191487005021193270833283150385320891674939581151616860843831194436030325106279562936505598331682912151054416726888615097658087493601703865555417162142846078042678164987758415671708169912482403081393524821750357201786687524568068923351217171164172757342706571294959997484322116618790203026373765310587305733926608853368754534372835528038052902623910835018941483334529495473265260170818648083538289418240*y^31 + 94724719559956410848739960398783002542590139323320118923631608842158523296827629565424797080027460828292322456884104496557481091993277747469453396023076549380548554798477599246345559334324951794203933219251519049584407384315095594873365936479715857853466345955824821208743935940605424800472446047396738715006821749762710308315158201360654820521283492984495184935161672138925216626683730667572974640410854568627307645239174953154803758164693336420379759392357741995983477154205473319609381674726957784259204097830905640747534335311341364000274210616624489601000791056511218308847659027809426437892653354373865023034603/625918229446057947254127913582648812564688592902732164088916701768940917848188933977574588301170212897641082652854558483254635137835037992610040646755880569579451735288432138344556368796331215454232541232676657043797871751255298317708320787596330222918734895287904215210957798609007581276569890734126399582920728037763604181722153774414521873400425966388854290535711519510669541246939603917927042478120600770348381205437589300446671881142017230837804292791043189335676642823739999371080529154697550756593441327646826433481652213342188633593208882009513225655977708754735370833632373868316315042704662020884572354560*y^30 - 1132986472853245335832104097561897886833252856019119391856685268140963677923108893637565179845897721951442217248993313051997612940782825907907526885021811253242452009706715109642960046603236131805665416685030001321916860507229822815068327061908692319898018571183982568350750545790743209330821147650457898225592419482402176834493830922481319383715992968871997739975406851985457609967035477856210666929240391443418783136760263340553461812840396531641927566708850962176153280003596050145797091465185983564018585240956039780563251559335835707089483300882168771958657910944573071686729114385016627138156709004232364984906299/2503672917784231789016511654330595250258754371610928656355666807075763671392755735910298353204680851590564330611418233933018540551340151970440162587023522278317806941153728553378225475185324861816930164930706628175191487005021193270833283150385320891674939581151616860843831194436030325106279562936505598331682912151054416726888615097658087493601703865555417162142846078042678164987758415671708169912482403081393524821750357201786687524568068923351217171164172757342706571294959997484322116618790203026373765310587305733926608853368754534372835528038052902623910835018941483334529495473265260170818648083538289418240*y^29 - 512780922700197508647768015952747021289088754973568866562408615957269508918934506317753433971532734128762169558068445682781503481193195190848395677396066116474077251540329253729311447498787521665783700370492160397202695670050975617957432871654298842584955978727676899339751104135454078831478353431938067890959203357651510660202617646109794152936355111625350397887118214454261187117252700369261698294789913554637524384199747366624638021003451642218021466586051962897781445202797701483636161981452191789916058585321756753867207779919096123537713220839536837564627265224404574432296244070904628175886431314335366155785327/166911527852282119267767443622039683350583624774061910423711120471717578092850382394019890213645390106037622040761215595534569370089343464696010839134901485221187129410248570225215031679021657454462010995380441878346099133668079551388885543359021392778329305410107790722922079629068688340418637529100373222112194143403627781792574339843872499573446924370361144142856405202845210999183894378113877994165493538759568321450023813452445834971204594890081144744278183822847104752997333165621474441252680201758251020705820382261773923557916968958189035202536860174927389001262765555635299698217684011387909872235885961216*y^28 + 6434464149640917701402892392674640729568545935556913321648813568682240939401998399049495299554741102691536574667821403364206028696023115303597671572351839562591628254632876750024360228758796217542030360143615695695779025270014844174246754155707946371019009038567247911685612486598169315561491350798679902235478687209924825091552468013678926504990048373537002280089193235531642253086322282172601087464513557969306552871899483552276388138632240461705465710461418791441677852147494305904182577844324975534465983502927384726101168016383385855586413271524224699303351424670332650421142204274455274860749910674415879760981011/834557639261410596338837218110198416752918123870309552118555602358587890464251911970099451068226950530188110203806077977672846850446717323480054195674507426105935647051242851126075158395108287272310054976902209391730495668340397756944427716795106963891646527050538953614610398145343441702093187645501866110560970717018138908962871699219362497867234621851805720714282026014226054995919471890569389970827467693797841607250119067262229174856022974450405723721390919114235523764986665828107372206263401008791255103529101911308869617789584844790945176012684300874636945006313827778176498491088420056939549361179429806080*y^27 + 76045364325908444264293353942764946769960234967113540420964081434281287090370861584021291314197564894418673251919439334723298320733356477489961729996410888922286544510701362925084459042845958753112041247255426471412046932714063549582416196228729566218113747244830724787759926981694902623161336938712656256825614988670076711684169023141931394690550845249479721912078502670270778036255515454280579137039292607588243130761860515595144478448378891292231946250019600819597037599319181783847353705003029930655079623754330583241127955898576290523545559010636604458685791802602318054283028167967073939699533532601793599759612889/2503672917784231789016511654330595250258754371610928656355666807075763671392755735910298353204680851590564330611418233933018540551340151970440162587023522278317806941153728553378225475185324861816930164930706628175191487005021193270833283150385320891674939581151616860843831194436030325106279562936505598331682912151054416726888615097658087493601703865555417162142846078042678164987758415671708169912482403081393524821750357201786687524568068923351217171164172757342706571294959997484322116618790203026373765310587305733926608853368754534372835528038052902623910835018941483334529495473265260170818648083538289418240*y^26 - 168793215059068749879806956626953576461590574769681818895056544978694264584180187521240986463082602907253107901530534623916077161488117987650048875247988157680861978759701679842788111265919500529113502386010941170610102767206173675315168515354286099635496841954637165734262994464102355786721411233767206501136408093035037221807572501001644009270451936551364224199940019418702261908886115386131686835181241584338151588475939157133119328386374294303618891049274530186256546485866062971448061701240026208757451925313840054306253259204090455426040014353237273050830671420752535785326575064719965345556978263146174240579530693/2503672917784231789016511654330595250258754371610928656355666807075763671392755735910298353204680851590564330611418233933018540551340151970440162587023522278317806941153728553378225475185324861816930164930706628175191487005021193270833283150385320891674939581151616860843831194436030325106279562936505598331682912151054416726888615097658087493601703865555417162142846078042678164987758415671708169912482403081393524821750357201786687524568068923351217171164172757342706571294959997484322116618790203026373765310587305733926608853368754534372835528038052902623910835018941483334529495473265260170818648083538289418240*y^25 - 68971332507681632129019497828233552760204801512196493234470495886688484900204019151634634365801844091050565513235745302550011891082005323320286979977794020938296331139787658022901116116039976983446507703824452815824422877609002246276091516127353461178515261454129871266109900150613901700462566266129237378093997034059513414380043703827668513168872202388668456444741517940930840437405910658073282344930501298752784333497375159476555627137761433645404757046350837671084277745522208282495292628785194310244978498797876436162813055884700531571743636599364435591466338260276696094374240855295654198153961917322304982024899433/625918229446057947254127913582648812564688592902732164088916701768940917848188933977574588301170212897641082652854558483254635137835037992610040646755880569579451735288432138344556368796331215454232541232676657043797871751255298317708320787596330222918734895287904215210957798609007581276569890734126399582920728037763604181722153774414521873400425966388854290535711519510669541246939603917927042478120600770348381205437589300446671881142017230837804292791043189335676642823739999371080529154697550756593441327646826433481652213342188633593208882009513225655977708754735370833632373868316315042704662020884572354560*y^24 + 304710100797070971004937524127705304552198415621165570583555152123321752132892961197014366934949275427187143167388520602591822319770331488507486312544348932364528222083998005752402587105996647365660530738383339076954428437403488122818187571984952791291228272764803032708101250572489244942233388913467377451725593833482279482171700277190787490074216215431123427746945256561767557250324929706487272906415306709040077954141118075171385094700880031979068127253279449580878064517168876827952879537802109054473435516210808856880491277092682321845531824256227037685986216527044605045275910816696550065542506352897443148296528583/1251836458892115894508255827165297625129377185805464328177833403537881835696377867955149176602340425795282165305709116966509270275670075985220081293511761139158903470576864276689112737592662430908465082465353314087595743502510596635416641575192660445837469790575808430421915597218015162553139781468252799165841456075527208363444307548829043746800851932777708581071423039021339082493879207835854084956241201540696762410875178600893343762284034461675608585582086378671353285647479998742161058309395101513186882655293652866963304426684377267186417764019026451311955417509470741667264747736632630085409324041769144709120*y^23 + 95170149937855540031232935421192636056349831152666294175362830198951940531156309999233601214639827137634410937261679457832720211266412834922588657987125015934801718972719162361096638690384631351551601966794895457101119270032957465910682670395600887103174149202038222707183904083034260413922617594125671225058653416130294693089857364152921569876178100594698059492674389087468427783193430070049920966098762525337663721492557590378549879987305345995216842187095887623693565694394413205485611809412242928641471385092926871849438004571761198187339688998279905147527374772037466902197493129569977627103395515747362930659076909/1251836458892115894508255827165297625129377185805464328177833403537881835696377867955149176602340425795282165305709116966509270275670075985220081293511761139158903470576864276689112737592662430908465082465353314087595743502510596635416641575192660445837469790575808430421915597218015162553139781468252799165841456075527208363444307548829043746800851932777708581071423039021339082493879207835854084956241201540696762410875178600893343762284034461675608585582086378671353285647479998742161058309395101513186882655293652866963304426684377267186417764019026451311955417509470741667264747736632630085409324041769144709120*y^22 - 24828554064409151924038116634567436994602211122107544929649063788966376215741843560536876122079005173137492504589710074094146659582873812063415309277375427983831466006729247493536286187478155001339745775803669177396932687489790782341882223680414888056027054283467116303821565444442348369010500015954312214574600844223851485296698482761303719810818412218544431683143710638808955741924248346399475062924470016129307105281785217204158925002044799737519614359144849093557171633752033285296257761197534213745890586563873635926047752081773472353079592929917303716029971715589609153807677592651174093313618928625449377503010661/208639409815352649084709304527549604188229530967577388029638900589646972616062977992524862767056737632547027550951519494418211712611679330870013548918626856526483911762810712781518789598777071818077513744225552347932623917085099439236106929198776740972911631762634738403652599536335860425523296911375466527640242679254534727240717924804840624466808655462951430178570506503556513748979867972642347492706866923449460401812529766815557293714005743612601430930347729778558880941246666457026843051565850252197813775882275477827217404447396211197736294003171075218659236251578456944544124622772105014234887340294857451520*y^21 - 25200146141115240920736447083307803611221640239315652189844946911618424126330662596299733055314768033256439658278817576031551806503803621840822796664307639205873224527035674669247824762227922561689891628514355794759027948846023439928499833507860431296854669837310321029616879068875945434711780916092607527278486807660401979819986414572619581088183225750408851834113222279127756111427793452977243345739385616544784569388171704562002667475156455431236010314729035793095288437376992978540788558687035987035518639850333721447651226321658822441117690692211528950509311209227594899503651258577802608244248409528145135332751589/1251836458892115894508255827165297625129377185805464328177833403537881835696377867955149176602340425795282165305709116966509270275670075985220081293511761139158903470576864276689112737592662430908465082465353314087595743502510596635416641575192660445837469790575808430421915597218015162553139781468252799165841456075527208363444307548829043746800851932777708581071423039021339082493879207835854084956241201540696762410875178600893343762284034461675608585582086378671353285647479998742161058309395101513186882655293652866963304426684377267186417764019026451311955417509470741667264747736632630085409324041769144709120*y^20 - 18408741107017326903054995119317858964229030630810324770641090309683391547449465511012190251773678696699383699234970010138807328265784682881295585161161511140760347308542521506261117958532694883213645278294977281335805860157359394452412193602654118433888633064442216822318867763245593415061185369971260020101503397261092124880420548683701896370742043015656076135843581580623364396490288288542499665294404429648537789276160487116584936524002959199969100921939102951131425956420177516980989312420009893052922345945129046767618452639519759068219903126900569383557139301167898302104085380784313038100711946728105362712700401/34773234969225441514118217421258267364704921827929564671606483431607828769343829665420810461176122938757837925158586582403035285435279888478335591486437809421080651960468452130253131599796178636346252290704258724655437319514183239872684488199796123495485271960439123067275433256055976737587216151895911087940040446542422454540119654134140104077801442577158571696428417750592752291496644662107057915451144487241576733635421627802592882285667623935433571821724621629759813490207777742837807175260975042032968962647045912971202900741232701866289382333861845869776539375263076157424020770462017502372481223382476241920*y^19 + 132846167969055247346228677607412037545702647843790216445274097754753514805918913629678356279919729186876549051605200931594449404937386787657695608554228600703450881648503911870901376948354571470059538852821615544861052551935289022403775410643336949771888416338454455027676119186614091394981313891619008711488336173742570881361512599070390784355516108402237670389106249159234856819891847195457922599399710004117551853866345077819901615568575168895770483949149916185111425625965999153638714250069557709326989186237016478649849278941732734739759241814943457316103035604354202329244253470487890960934130134337860253307455295/500734583556846357803302330866119050051750874322185731271133361415152734278551147182059670640936170318112866122283646786603708110268030394088032517404704455663561388230745710675645095037064972363386032986141325635038297401004238654166656630077064178334987916230323372168766238887206065021255912587301119666336582430210883345377723019531617498720340773111083432428569215608535632997551683134341633982496480616278704964350071440357337504913613784670243434232834551468541314258991999496864423323758040605274753062117461146785321770673750906874567105607610580524782167003788296666905899094653052034163729616707657883648*y^18 + 19656937838393329013720814591217830322998855059818218966526224484222926856440299050460414949732033797817804532861725900554972898233312377790362623256153082056694685603819910163880075187174033278507463091398286766821266792839433169656205210779361982708160440183652090630389240652702169820881308582151649279501558326516740909288544724888333977236046706369197293029201334242138488032029699465640566688277925125783045852015757856371851089721665375962942830866909524167515211960603797952744265628343028471552056896771689973385703327915001027011177200215599548243931050369883681105433538552775064795425847405786089633693699035/27818587975380353211294573937006613891763937462343651737285186745286263015475063732336648368940898351006270340126869265922428228348223910782668473189150247536864521568374761704202505279836942909077001832563406979724349855611346591898147590559836898796388217568351298453820346604844781390069772921516728870352032357233937963632095723307312083262241154061726857357142734200474201833197315729685646332360915589793261386908337302242074305828534099148346857457379697303807850792166222194270245740208780033626375170117636730376962320592986161493031505867089476695821231500210460925939216616369614001897984978705980993536*y^17 - 166116041350906321955546098769824461026243568780734334786773275854679970337772292977462151240511181483731713513755772268041489355649883704414237440574356315033723637916660352097795828597465179016691039429342742661998580960448684967748575657854490711325383326855130752118210919775598563205665447380992827081941427440871045038697907767843752157551925127839310385287296612097161173155392377534033282415376171950580102771155849579355778365936484580306103732330456251540879596901148853138634540297391518385513926708624538085078669989675125993007138402131714897772514936272256697839396997174873859721982804930159589324135583913/500734583556846357803302330866119050051750874322185731271133361415152734278551147182059670640936170318112866122283646786603708110268030394088032517404704455663561388230745710675645095037064972363386032986141325635038297401004238654166656630077064178334987916230323372168766238887206065021255912587301119666336582430210883345377723019531617498720340773111083432428569215608535632997551683134341633982496480616278704964350071440357337504913613784670243434232834551468541314258991999496864423323758040605274753062117461146785321770673750906874567105607610580524782167003788296666905899094653052034163729616707657883648*y^16 - 45586475817946454896223150242856271227384072745545459426652204526310491029340262579472280884663859021058069539773824814545048522932050157650438224908481733058401855352347563955598524048764036138924674966436566200645164404707112899752433075131306536515481903937193159517153459151369945820316374198819823472464644092279241129179507934948028028598496922209817460731330031654179784193838537576700003655500453151746143511605073481686086008472278986754095563202086171519229947025008824739087124188669267889401449178929054961617877335418677322302411725097692822982144751606058840845119023022460578359620870628071576114039328655/250367291778423178901651165433059525025875437161092865635566680707576367139275573591029835320468085159056433061141823393301854055134015197044016258702352227831780694115372855337822547518532486181693016493070662817519148700502119327083328315038532089167493958115161686084383119443603032510627956293650559833168291215105441672688861509765808749360170386555541716214284607804267816498775841567170816991248240308139352482175035720178668752456806892335121717116417275734270657129495999748432211661879020302637376531058730573392660885336875453437283552803805290262391083501894148333452949547326526017081864808353828941824*y^15 + 3065387382584301137645252393149017827428397397066279601521613513893607764877781619064217903565361019452249589431575715381649293102348156767654722909450787529376900384459394188642542157818569978566251173813193425193360294269506530281308155242684552447801428285058445309401662322686755007828844464518791689075263785135200460015211345586810803226890294747758842109676700483418858932398936225738250240347170019674918291721522549079860375158173338176163257872990525876088397084174253220941488010992598093792340938172814591141806020833696737744238941585836556076500484396302121243245194543952940904501153609286475972607811907/41727881963070529816941860905509920837645906193515477605927780117929394523212595598504972553411347526509405510190303898883642342522335866174002709783725371305296782352562142556303757919755414363615502748845110469586524783417019887847221385839755348194582326352526947680730519907267172085104659382275093305528048535850906945448143584960968124893361731092590286035714101300711302749795973594528469498541373384689892080362505953363111458742801148722520286186069545955711776188249333291405368610313170050439562755176455095565443480889479242239547258800634215043731847250315691388908824924554421002846977468058971490304*y^14 - 10428533873707559203025136008206657380006839076893519466175022903610172674014981673012526534322036119756293361071379645638860962192725093474399993427420395203012646886275170211942846827489915800407401876154452501161051548703593685962680179964648658751848551413044295375291380877390411923492276692464671925631313345167364365402851857839275644813111543237826676572203092053319729383800101626684479267287663396643835435180101616387670433302891963597963396688881724044577540781284163242069832321597050805218085634467543478338759082466050394576750699311642014917401982442406844330026871566080363876397165898636802416252239897/69546469938450883028236434842516534729409843655859129343212966863215657538687659330841620922352245877515675850317173164806070570870559776956671182972875618842161303920936904260506263199592357272692504581408517449310874639028366479745368976399592246990970543920878246134550866512111953475174432303791822175880080893084844909080239308268280208155602885154317143392856835501185504582993289324214115830902288974483153467270843255605185764571335247870867143643449243259519626980415555485675614350521950084065937925294091825942405801482465403732578764667723691739553078750526152314848041540924035004744962446764952483840*y^13 + 82116514436316391739901754210929014028487959242449659328143891248783086323004259825290552336058301331863577676377967620498203029446914102676679993565544858688982780836658065293553822743611771978624355969370172366917380487821990096532757937343569396045409638642006347498469981254522892957908294141399806869923101020175058604522735356457130776027173949756521247401479837652316717743418993235191225752781336966406638097547971690750316875724168127494408165594070231897782611667328085169113872154730117684943131100746111452273113556570625752467327004539972644700455096754655478889497369881812045429302547076157987195288414707/2503672917784231789016511654330595250258754371610928656355666807075763671392755735910298353204680851590564330611418233933018540551340151970440162587023522278317806941153728553378225475185324861816930164930706628175191487005021193270833283150385320891674939581151616860843831194436030325106279562936505598331682912151054416726888615097658087493601703865555417162142846078042678164987758415671708169912482403081393524821750357201786687524568068923351217171164172757342706571294959997484322116618790203026373765310587305733926608853368754534372835528038052902623910835018941483334529495473265260170818648083538289418240*y^12 + 7447100050718698060871866043594610870292281533585083833637809454731602456232478355665879582562748288753853371181757254878364520310520572299373844028324881907925128294889830826269006276755092642662674513521777087441990208252756381638144227383529136341907447552369462964386474546613479427295634949284922025575401964891233748486436943561535406730860877066809901267674778425979942898131148401889751391882810329575971219746540218884454242739490958890529896245904758712885262637181864964638226043832861763996930359332383392403354909332417491422931690760705075483333833797382209502611000954370920707570455153190774587723148543/78239778680757243406765989197831101570586074112841520511114587721117614731023616747196823537646276612205135331606819810406829392229379749076255080844485071197431466911054017293069546099541401931779067654084582130474733968906912289713540098449541277864841861910988026901369724826125947659571236341765799947865091004720450522715269221801815234175053245798606786316963939938833692655867450489740880309765075096293547650679698662555833985142752153854725536598880398666959580352967499921385066144337193844574180165955853304185206526667773579199151110251189153206997213594341921354204046733539539380338082752610571544320*y^11 + 76696695584235246514194408183235169189889107721750007730229037227354982103571701787960184268068726826713962272738125557263306207952811150882848073474726220701499049335762987502035695578377974592804371199179249137519869732927139523944185391018200250783240715334052907485217745321878086038395407462151083207017081636718017089795530242751053677822375113885417800227543820156800148153884944549869096193496136615875531095628284971878284227105926873763091257256868263322128059847683835617501518899000531626307490062105575226766495985256421332803717733515574997845932357498510801731875707864889440802392623196929050666448057/62591822944605794725412791358264881256468859290273216408891670176894091784818893397757458830117021289764108265285455848325463513783503799261004064675588056957945173528843213834455636879633121545423254123267665704379787175125529831770832078759633022291873489528790421521095779860900758127656989073412639958292072803776360418172215377441452187340042596638885429053571151951066954124693960391792704247812060077034838120543758930044667188114201723083780429279104318933567664282373999937108052915469755075659344132764682643348165221334218863359320888200951322565597770875473537083363237386831631504270466202088457235456*y^10 - 7169167965448173567342223413692303335235242458003211667094285031131515039859205508273032927814488991327048727621212766010196964042741701010332190284870141966270853148016271364693380006568768666136637589033714457814007614096900309630558396328328504031291895100250877633542607933311213232389225634254297962223158715613185775155748026043227776418075757407665774716210814681916648608770068166746165962759033995484724468192791080121041782746362881435168689665391776063801188430527163818707204413199216634435779694920274011220912021829751998719959903037909728557847561765292218879665245231569812936891602398112945128015204497/834557639261410596338837218110198416752918123870309552118555602358587890464251911970099451068226950530188110203806077977672846850446717323480054195674507426105935647051242851126075158395108287272310054976902209391730495668340397756944427716795106963891646527050538953614610398145343441702093187645501866110560970717018138908962871699219362497867234621851805720714282026014226054995919471890569389970827467693797841607250119067262229174856022974450405723721390919114235523764986665828107372206263401008791255103529101911308869617789584844790945176012684300874636945006313827778176498491088420056939549361179429806080*y^9 - 79722806251285619835464424448277946794263576248967240636858432609426934501258864743593367910026051993917099740444832207493511669810545519402410987452130348253326916434075587823553896462618720199018256775424154650026708862792477889069332623936804565308370308190831252899332154908506784154167276337163973236459152804400838445097909456333112715110310081430388482275430602079122485070206316882946210263657355403498096162805885110182430501002173589118787796390431351372466106571094422731482077002826049785841645989131903207946161527937400729800821010125900458798420128928864941397030210720342954485021027285872193977178093/9779972335094655425845748649728887696323259264105190063889323465139701841377952093399602942205784576525641916450852476300853674028672468634531885105560633899678933363881752161633693262442675241472383456760572766309341746113364036214192512306192659733105232738873503362671215603265743457446404542720724993483136375590056315339408652725226904271881655724825848289620492492354211581983431311217610038720634387036693456334962332819479248142844019231840692074860049833369947544120937490173133268042149230571772520744481663023150815833471697399893888781398644150874651699292740169275505841692442422542260344076321443040*y^8 - 37059468893031770632543013135824158808326002637228421860602159332482928758622353387033221221533507888845084475633728559391338335909285529718998461753753395637527010721279129680279287663006426125449227641809380949948801051172054821408178416219244058973627628186156541375056264742788442988046216321520033431548902173381213679642165535806558501332315277617842885882971356632080467422842163888783245242685700213135712622886172934716660909036442016415682708903106012353460596879659046091372975348696621896458665075782139394475953575504487532231844956752254866150147479611558582679328368556998464108450073123221248670789387/6519981556729770283897165766485925130882172842736793375926215643426467894251968062266401961470523051017094610967234984200569116019114979089687923403707089266452622242587834774422462174961783494314922304507048510872894497408909357476128341537461773155403488492582335575114143735510495638297603028480483328988757583726704210226272435150151269514587770483217232193080328328236141054655620874145073359147089591357795637556641555212986165428562679487893794716573366555579965029413958326782088845361432820381181680496321108682100543888981131599929259187599096100583101132861826779517003894461628281694840229384214295360*y^7 + 52403716566400577791765673207055234655878517215461993865484021766989231337744847242427867567400827806752191518840329576633417019378107550719302645673101369141084813281892513569343175717876676535801171967297570257778035492607989043410199305569505531535068009912911604861622971708678506795597232045158385585738031062405912368107591059801588745874185591921431048833363751471572066629774850963856374293923222781552509349408838988178890697268881136130510762258328152706324366466865891944923873530080832056480774974743336971629675915364731264871401102210920441677388298795355910469478608777682720527663735071698421436621991/31295911472302897362706395679132440628234429645136608204445835088447045892409446698878729415058510644882054132642727924162731756891751899630502032337794028478972586764421606917227818439816560772711627061633832852189893587562764915885416039379816511145936744764395210760547889930450379063828494536706319979146036401888180209086107688720726093670021298319442714526785575975533477062346980195896352123906030038517419060271879465022333594057100861541890214639552159466783832141186999968554026457734877537829672066382341321674082610667109431679660444100475661282798885437736768541681618693415815752135233101044228617728*y^6 + 7729223451993766570245565546651954787542239033676179247631326344230297290799526650620120737491777996593956173957963277753814370590050404756679879503976780922054883638369929062215407091200023116804380146312560742747519402275075409784986792806911395478716946008307941761447607080502153606741201299089763612017347582136769795780285268767974316837306270274105467078351646779407011300697552304172790813767170974666808810246998489136390516360588310195598995721819094506671306053282646084699050687697771901829753305342477921764178454027911339825433486554939509672334884087035924080113496050503253796090457476451955609494553/5215985245383816227117732613188740104705738274189434700740972514741174315401574449813121569176418440813675688773787987360455292815291983271750338722965671413162097794070267819537969739969426795451937843605638808698315597927127485980902673229969418524322790794065868460091314988408396510638082422784386663191006066981363368181017948120121015611670216386573785754464262662588912843724496699316058687317671673086236510045313244170388932342850143590315035773258693244463972023531166661425671076289146256304945344397056886945680435111184905279943407350079276880466480906289461423613603115569302625355872183507371436288*y^5 - 815608228508350593500307497867939845966271565724804099415949794072379730744845346761390422898893455256858232873172156063244780503530314908740224343703325474425850908452581711391145932879670953879428333135369917537342399194410439094227902180517753785615784531475430088819618931104392952830436993296847416328738553697177795012109386485231275906209899475435831962675381478016219920812986461087275729354783444400786377953667280054099413391519729994900100700327211254343218428941270829346726693807149851605683240196890089254356647554346348075577082849443063175083173668842563907936851868997230807804794716309662423446863/9779972335094655425845748649728887696323259264105190063889323465139701841377952093399602942205784576525641916450852476300853674028672468634531885105560633899678933363881752161633693262442675241472383456760572766309341746113364036214192512306192659733105232738873503362671215603265743457446404542720724993483136375590056315339408652725226904271881655724825848289620492492354211581983431311217610038720634387036693456334962332819479248142844019231840692074860049833369947544120937490173133268042149230571772520744481663023150815833471697399893888781398644150874651699292740169275505841692442422542260344076321443040*y^4 - 2459618753312837128532958721708759384838979950124358235363552805005510782574724489721904271425022346025276109358328415090663644996725199297397718408197458106393542923406414716782337713185146485946708727507750167040219536676972148257447460199150019036641223083406848651954218568130283408494302597742350570039790833093553617117818502601848665390140065675213357385242472080350658968108666435244045712784852117404550338014916177816483675249704494786729624266734210089386248185523862891853589842588018015884673896641664222030707776460660262651364539274247034860236600170011911789302762558589157472576608279830643254024787/19559944670189310851691497299457775392646518528210380127778646930279403682755904186799205884411569153051283832901704952601707348057344937269063770211121267799357866727763504323267386524885350482944766913521145532618683492226728072428385024612385319466210465477747006725342431206531486914892809085441449986966272751180112630678817305450453808543763311449651696579240984984708423163966862622435220077441268774073386912669924665638958496285688038463681384149720099666739895088241874980346266536084298461143545041488963326046301631666943394799787777562797288301749303398585480338551011683384884845084520688152642886080*y^3 - 10676465933283699609233835305550705828788590090604354403463520091038775042505887961373229459030298029549609326220011179507180804254570108811579116485271482218484443893941180376847074383969695229872305187236988281093259372526200779185366146737746952652681795056507159097618282696841233135921895352689566065503792700960584048845081189962150031581611181824000026656409738208205122498053495086835410664772270746623709240981086939074872091202688830213660191806064938423187464121100754148997003162107457749838881304020328105883848752563786012286674442313998177288249379616680620604681939999314442758836396068047267571799/3259990778364885141948582883242962565441086421368396687963107821713233947125984031133200980735261525508547305483617492100284558009557489544843961701853544633226311121293917387211231087480891747157461152253524255436447248704454678738064170768730886577701744246291167787557071867755247819148801514240241664494378791863352105113136217575075634757293885241608616096540164164118070527327810437072536679573544795678897818778320777606493082714281339743946897358286683277789982514706979163391044422680716410190590840248160554341050271944490565799964629593799548050291550566430913389758501947230814140847420114692107147680*y^2 + 34726575940009269381486385726369806591955908067073503715439742017368238589487176960552278104298370564719282672230254092639038119205991874978156801652846499002705978240954714344789885560651882468887111853280442283276525634068986477385247769203429196880256447507444507231186278030729590420303970918438842056601797143380726837155910317398717133897448793962924313007178916976643648599922659292606429147672546959762679285964543154161189616873609885974251464388505978889963730407965555869936504726270066621361664401531313857490027257970832215376169869502847287022182585186082426914366796567716203169877987679244599522369/9779972335094655425845748649728887696323259264105190063889323465139701841377952093399602942205784576525641916450852476300853674028672468634531885105560633899678933363881752161633693262442675241472383456760572766309341746113364036214192512306192659733105232738873503362671215603265743457446404542720724993483136375590056315339408652725226904271881655724825848289620492492354211581983431311217610038720634387036693456334962332819479248142844019231840692074860049833369947544120937490173133268042149230571772520744481663023150815833471697399893888781398644150874651699292740169275505841692442422542260344076321443040*y + 316088692455188320144161514876194914696556660811590212933792807359760053537326516554483473932451760557272823391233890886576363732744268305195677301055773946325292301144876201461430824833838867086319778311185613906494731669116850644723291713070403791719704237467932226025477482397383423151050418692540160244842272121641084397675847363057523472169756368744597892367830262689152379348450674845318687578755925017241851193893053926467431407426780324836128413593597091204100191185442957480203998089705965151536310637988171412985899676414482133806056084222011058516160273702816612224978851776914844934906185984488663009/1222496541886831928230718581216110962040407408013148757986165433142462730172244011674950367775723072065705239556356559537606709253584058579316485638195079237459866670485219020204211657805334405184047932095071595788667718264170504526774064038274082466638154092359187920333901950408217932180800567840090624185392046948757039417426081590653363033985206965603231036202561561544276447747928913902201254840079298379586682041870291602434906017855502403980086509357506229171243443015117186271641658505268653821471565093060207877893851979183962174986736097674830518859331462411592521159438230211555302817782543009540180380