# Manifold: Census Knot K8_92

# Number of Tetrahedra: 8

# Number Field
x^45 + 22*x^44 + 133*x^43 - 113*x^42 - 5637*x^41 - 21936*x^40 + 75194*x^39 + 494115*x^38 - 578181*x^37 - 4962074*x^36 + 3319418*x^35 + 29478912*x^34 - 17595257*x^33 - 118829246*x^32 + 86604344*x^31 + 368765681*x^30 - 324392811*x^29 - 971572457*x^28 + 784952993*x^27 + 2136875617*x^26 - 1074774511*x^25 - 3528338731*x^24 + 567504726*x^23 + 3982461846*x^22 + 425803188*x^21 - 2939809335*x^20 - 867427780*x^19 + 1430349667*x^18 + 626466767*x^17 - 474408527*x^16 - 268074095*x^15 + 112633085*x^14 + 76862704*x^13 - 20650499*x^12 - 15493140*x^11 + 3184867*x^10 + 2251948*x^9 - 410619*x^8 - 242506*x^7 + 38798*x^6 + 19212*x^5 - 2294*x^4 - 969*x^3 + 72*x^2 + 21*x - 1 

# Approximate Field Generator
-1.29195389969863 + 0.249648543996536*I

# Shape Parameters
120116318412547286778446423521063980264224262593185869609254281472922402334461600081535137261931028614564924641872489453358562670346752445176647970120332824073882848461207/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^44 + 2724839822495766622056335340559582083595004162699831146701574623653010816604415327404808131298158206709594053758709873033188703773654119124598262888441969597960986085836611/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^43 + 2225875180581965075890577922864617607538996021988846957853103368933756656361115149882570156156256056657937691740448351559976108919632462162580583559983408113621712029216293/2815903448004569905828028897527584878933416464145155196175596175935061247494888814310269911004004885250027951266134858996198780996168149538149235957065326046723896153747*y^42 - 2147522269683939793710460359504043801694812754718545618770138506317934198981210402272949885461097473796740803256834851638497045205897344716753620174667925751026134299105327/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^41 - 170818656375923699950302155843521322472740032882115180908582703996965866948483017528812215785471930588856041756793464273991839454882248863997149706550828057887062165679100855/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^40 - 774838560900201493429758934386095699616217459326675337042018616452037929515730240158605705418393999995059576808868549813963147037297737713875979815310418767926248169610486325/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^39 + 3552937555444418419489589938399349720693148783198367125340474333450413017517996711835025070221094293951632071439185483857656284401439396961536571459214670970804669880820824961/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^38 + 9285610040889122437295877209835378508349463078086212010153106477633530517675456849322855261318663103104469090739148971484031625065380166645806753739672530144924807081366579597/3218175369148079892374890168602954147352475959023034509914967058211498568565587216354594184004577011714317658589868410281370035424192170900741983950931801196255881318568*y^37 - 13741310137559004952422052722230511946616637663868261531097943475903035268732552952960581184044285731862254633580882184789069264588012923839989001382649869747950480392412874895/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^36 - 11289309524754675570096718496204913598598922434091128234872255234884040575620081717380007294577617659107087939957589976514386447886553238792152164468751366564701809837135489606/402271921143509986546861271075369268419059494877879313739370882276437321070698402044324273000572126464289707323733551285171254428024021362592747993866475149531985164821*y^35 - 7751015733717655407413343877908869133172184036559024557764575658517788677222157937878594821002788606506905071729788937045139708411654496816483465014739792258373098529961670757/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^34 + 1851407795833288539244497567093037328135304163392898393305492256286759204890523216542713475158684306262447671102746347358687802321158205487138595333467876478634242570846456407713/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^33 + 319784280691253425097001306351233778592200241662614511027214929883396107236337705351205901520462644005727020929657079644768255258742296952464941511210078007635815977485811073063/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^32 - 2152776458334223858891824939162435321963337997484801387740915313877339744186412556889356550968997721407631068403515368108399773230709664110289822742645957792026238074437280771863/3218175369148079892374890168602954147352475959023034509914967058211498568565587216354594184004577011714317658589868410281370035424192170900741983950931801196255881318568*y^31 + 620306077458179964757104548523549378906127019633894702576511575476845025098335725079465345493096279202525450684227210111619584942060474298732396440360010181858058079806094130641/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^30 + 24388246689087136126161765405650423369278952033385346432404190833541527425335594808719203483386640492705125836321677838439168005292255877098176356581986658531072843099311490606131/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^29 - 8264920885913944492863071485330703408223029360596015284392446303068658397092033635666731531598131016447381349960302189305300352561900131646994278804067007240625987768588322608099/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^28 - 33723616703079328842690753736754623755142165176502235717797093937630501972831111734995420442947766922936440400011789158824037552972171575506972687634953843173349318138771889019237/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^27 + 12110508614332227448603740808324862796436972118528491369088603699447843674178473630995567069599668802821205278651737696601068213591669357930750935556513041137182404104644553694211/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^26 + 74481701500878305318298435848112788998164717605345150068350186660178658008010454337886549214002204746764795294314597583412719837994149208469215915677713354927927849962222113895643/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^25 + 50887121058099468340854739661115304333996995726390016783838578783390791251907891437547999031850736289323129147799105795800615788287162988195930095207678828540193689355936612699027/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^24 - 57602338058309775275991906900114627458002788661227928995789083667024011759012274266906247864884991880979838220324445123183644987618977019303389537607768480517531050804091536104130/2815903448004569905828028897527584878933416464145155196175596175935061247494888814310269911004004885250027951266134858996198780996168149538149235957065326046723896153747*y^23 - 108745587278373582407423826009318010361137962310108389062701209553920621255034473986864067248743410386769154577765506728220853387915570404906853347348313327982018931625880940869211/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^22 + 7948523012341480637099972941860733589689739494218008581630362975460038404718041932575821843412137224075584880126348189946576161796662575875993994665290905665914524009934597610166/402271921143509986546861271075369268419059494877879313739370882276437321070698402044324273000572126464289707323733551285171254428024021362592747993866475149531985164821*y^21 + 86822048452114881292696635325276833066921440861959915602178066663803037192388490599992795506127998929760339504772693936264661489144701777690876665080333075004914498578468783827393/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^20 - 239717790206364509883480193695762023523564862864602126475659502086537636487602926311873628915068871981883802801588277179071108777249930011191122640171616702576328442637352778341301/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^19 - 292122146314843471882154738839868576222053461050042533866056389958347507515884020748692692234312939804634574414912172131720862235653652613649777209933888736508650920112734914407127/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^18 + 14139661406870081190569364058567028961178771403852133633148465965208911608051100122608187401090603971985135728481749030326951082965943158000650558136337086944613206170802889474771/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^17 + 146427271720189806857105318433499766532966335373374069516031398310801803456897265374194480380872788857189616131350072478829872254136210855312281116599851638271267049830500198386989/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^16 + 3270474101352079095850476946775277490307302063001713524982849001414182851739240533545830398928115610351964988267353581088935953504822010884685015792832629835859011249439526986489/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^15 - 47615731988300602615240915315401163979477053743328968040978292456174945554394418459439958678678383793537460652424342344727117638601067177878461603173805639407883435380343930492171/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^14 - 4299081142011713857545230422605597695564277687019966168920736961770045888156931472814141426382133630059300288494957952493966376920317574926696326584496537174632143273004163332369/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^13 + 5370756621363998545172056074252471839590953457351004170394353551928629760807879049544162178505464493959723224613279778852051815596692711424627702757328812472466549219448161374905/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^12 + 2786597462501815430059792482141088723353479931419626016797957619694683626978537263070124840651072436786913244687196750133857520339934128336669965540050582434314587072808139356713/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^11 - 1794568114779249052299931308122703759286220506423912106801091686192574736667446508357540670122946920981479085383313534965138382259355788653890013973088964290055908098782207055757/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^10 - 258225496385767560820660708366789750209840767406875664941690011121400816675984431452840621449424243826401741708001660103851372952071993924177154227674511289366532557122381293171/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^9 + 118244616721169579672572628164501988841073535415667308911525781760312787334348859700128118781288261437727273315270701332461550680009020359121243814488949434132333718292439140961/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^8 + 65174859499947953290857918300156980287969051950915747960177974685796642746110233105263271907342092417077668576473145021024324645477100187358435520723618911239486288626485238921/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^7 - 24159925358285916673368323139287017897255759461458169059671243160904698441007341669936061766099189088919427770372562592635689550328567409060756514810852076173447534003726444663/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^6 - 6333493931615797689867549730146203018190049700212774117302385631694940522466630148751330984201413083035179508344237308341533350085216691120818103759169599261884143060732775367/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^5 + 32439165028075639518739240003623575640180259091878923856322762250576474870337204882697600646217292566658294561891102200875122842146380474755458072966146745819260252113307243/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^4 + 421286698289123271537090303138714085183018242625113555792638380631875009494806082859084150015844838261821895329916892082029949013302234653888132319932220124344812046778129283/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976*y^3 - 24872037523766521502591292318750827989958990433723549761108664828220361374553320522971738467786346492532107288449273375921992256786268441390506117557484427238146253232068801/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y^2 - 5631304049076439153790697356559000652393991796523754977810668065973125900501401579623958847867392051495704115808107482853430111401272902471743752668591956192836344156843867/11263613792018279623312115590110339515733665856580620784702384703740244989979555257241079644016019541000111805064539435984795123984672598152596943828261304186895584614988*y + 563637512966720261250601348609734266426376108403421437943343864454485907822903530861039461651732728216163172020060119073971668800060984534342110583261921665562810169002769/22527227584036559246624231180220679031467331713161241569404769407480489979959110514482159288032039082000223610129078871969590247969345196305193887656522608373791169229976

-278453506212404579617021663805095510474099440501609844159314716733371590951096346634916110219389786497769569075094582507272608256442188825391635476205714666735205918556207/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^44 - 6474440997759594537003538048426818228359443841346029486789999118513542750676146936375869625929259514197338993444625031732443730922162245456908281738382820186384319154922723/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^43 - 5595289909793330643664407562519821793125073263877197147885052226642816966261768202481297278486461761079607860433686762663126561778176252668589745938458848321991264870422685/47870358616077688399076491257968942941868079890467638334985134990896041207413109843274588487068083049250475171524292602935379276934858542148537011270110542794306234613699*y^42 - 16292267321088262982920438091620871779442160919510385511992364524847731681956136248036820870633108345520885911433204050028248813362414632214539386073827346743952000782732313/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^41 + 399909268594126833445804368858046628737173611933826125545374512208224463672496183374498733174956749075953664280190125040438921616501876626689995628569657200868458019602544669/95740717232155376798152982515937885883736159780935276669970269981792082414826219686549176974136166098500950343048585205870758553869717084297074022540221085588612469227398*y^40 + 118708650402811303277425752305534467050365411421996582904111120521128704497196962601454860445253424099928700751440138531734880343648233957631034418105498282426812436920119937/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^39 - 6470884400045646930390050933226069453187524240648251999341568197212583917826378075712331148293631117169944242713767363470525414828234365087713999768860072787875016052189744421/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^38 - 23162858541399976711780731572935496415226857446311241119186640184943805741135118391530182558018439127844947483222635076861777420774408598330035360758545624748388903240602093981/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^37 - 7306103969622821598177078238177606288283988155841657992051728301414679269432832174111107225616452079612762477039464814694137598253991619544871584740790110505362789214381855669/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^36 + 27661562596959931376301932331912062242799609832755745969585095639531636640399702225923061446696328430338494739488973973212351259828479955104971551239036997051638869324489135319/6838622659439669771296641608281277563124011412923948333569304998699434458201872834753512641009726149892925024503470371847911325276408363164076715895730077542043747801957*y^35 + 406974552414746282561086860462071049078799500484782515860826987937735206679077348999371593678596133104296030462340388743976985687405859967911820057860534663003227210828677221605/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^34 - 4517633428370521743592606072437749822801870091231076787533414198876731356482078337670105479011600123930715181444501194709611640932215432866885423213210080599762408648506392536261/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^33 - 5315745255792500155157790129669065865039164052348863904388281371778461838139337019588951459876760911488970900623307238845626783227370176524333982168204510192521986869699464983831/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^32 + 5327401050550781334409170065042807108640131818448528155317404712363818229365662427551996707741862307181385422479340597585067845313651242199503980821511723841122116737049132324231/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^31 + 16840648089996454515881232469023766521572917679997465142751913017130158267103420723928827093245027984299364974677749506290101152059428869744683694652631229677706103987231287512303/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^30 - 62496583974236562163644763709900437388898804743824514936970475203354127525319685535015599596025638631627166597451290172622361058949472550465663721099559184559369042908452513652727/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^29 - 37347452589614466360415042029196727967478676831869325980326128506623714299547127174973587736371875990817260749328258274670115264954588279204073577497872426604138530275954249682957/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^28 + 89465184160668573593448229461675743827338543081122395332079450381947407703133955921151922454427628866844665217711737777077023393529616745299509397728095233190965560118534124806035/95740717232155376798152982515937885883736159780935276669970269981792082414826219686549176974136166098500950343048585205870758553869717084297074022540221085588612469227398*y^27 + 120684682235569757440698169240392460201093347700164429013531887928748024762778939811800293064561435303601425037602855006158794800616951419275230390767896708591290269385333258729565/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^26 - 199180063931230716324497552696264338494580585652761297537590270086352807050171612380290363968416558855213103114152246844794966233861334721270026857258069653207735136950620824321027/95740717232155376798152982515937885883736159780935276669970269981792082414826219686549176974136166098500950343048585205870758553869717084297074022540221085588612469227398*y^25 - 442173205417328293588954822874092752540424264731859972245480384619733400551474961141630669526556738390595177642231704404828135568956422239571405620372626409761539211866879437565251/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^24 + 149773180871993410399506007587526730693459273696138425635895552592396121863971136721179528436428927934068838619516841111721593428465395202211335843494648646117986429967314459554411/47870358616077688399076491257968942941868079890467638334985134990896041207413109843274588487068083049250475171524292602935379276934858542148537011270110542794306234613699*y^23 + 512432519381421869219478649259057773310526960623128271285188713140746289865650217393888256198797308260605832704075033930790575808492415644058919809402418689086457318525325873769735/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^22 - 18998129435794153488547876227601541019898755199129756057500670756553502826806873745718670982334496941145310487598337352761760297265104034451640665437404812995519133035446080498761/6838622659439669771296641608281277563124011412923948333569304998699434458201872834753512641009726149892925024503470371847911325276408363164076715895730077542043747801957*y^21 - 340563189884203775569530213332739848152124699552368746715684735283145899917908099739638967118595478787097314754363634825891580780772869857261772861341167486021000390376861400214737/95740717232155376798152982515937885883736159780935276669970269981792082414826219686549176974136166098500950343048585205870758553869717084297074022540221085588612469227398*y^20 + 442837305065618994431261824367546115787293967188308624279531472463860949700479722048536092288894538450396586255581104686732195028483411915644154213200735620698836051819832488477837/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^19 + 1054232952318891780707494595748953543013360781507024018870586457966469769397293117491256903070436387054977811412624618113805192615028288616894883793489527634132690704407042141953663/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^18 + 4258185520028153382466096146760657969054756887066435606131184280447194254965374850079290694264846675663585861754054218617459933734104499909216431465808819962775032661941851005729/95740717232155376798152982515937885883736159780935276669970269981792082414826219686549176974136166098500950343048585205870758553869717084297074022540221085588612469227398*y^17 - 501677576927769593070534225596364769718752438757056246875982682730611519989133543401126058279194040523058842361981196047578038929054647207691297171375942231138454347938114302779989/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^16 - 52297081684220977093031446100060693765521907728559417206264607811435288334490796498334212395469636749357146332434563019504178354354891665261549979703455143039865379777519487013245/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^15 + 156468108128429826645280962377443754436654744182389904974024808079516763285561233316568488715671720422740561949708979926908537636072640437257671823489293854528787795175115936560747/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^14 + 26452929743406617366771620068959152738368064550566295733565377766773224457430912871700723389127665412585599589075541553466330725622238578627512262982728774803145484018239695371481/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^13 - 17055179490094733336955344167740421388051824874863649531075602144281558784161791961313828303866527904587049124210872984684277338783959814616513349144220256734215446684203414891325/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^12 - 14641761851065111649535920413720855386196094793025650698495968835033367185932985394830675610642971087283637817102174580324327045423555310055154141845695491156611017642338961241033/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^11 + 5632932692337427527095786413824020401522818628777767936069475749794005952500107817586210145839276616264164412430755300355092587271260754999727461758144305379803470070016224386157/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^10 + 1308806345206720786790447449114397213055771297744132788383764512950009776267372582765600314478717259581088923017725123208812134349283008835106249532785108046997080221499117775019/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^9 - 381757275646155690640772032420536611892220772668050044122737885679469496699558752017065549080510759649101538650421384248945873311353301488994362490500282126638459823207045745901/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^8 - 327574988335804777801306654547822305710022107868651949869291694499496010278103825616160823531535530853818384070564246672537615080709090536609038742114378334045202816976725101953/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^7 + 81468167004277524426583450642490992707737823843239963620842979064173775982407793027015571642769708122430504033001945935620170464167163822373425125803763472707651243733027931423/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^6 + 30769011820273764243405941226877117336144867536467929163152959348731192030348330172810106355951278339087481306825540207803756383138880990546596983844275547858405361276176246055/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^5 - 6635860500678926319329147929902934198321980884125669424149381033308617779281152325451960830714412267872197047166185383713585407449757001403852654139536739394494731074221379/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^4 - 1967847698995223425763248060392028477499665001221821280107752995757359925674618580828228570989271735365248733725982462348407578237363049408492286831002887407841300148665373899/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592*y^3 + 94058416163553101938166439668237320597562372843745943144974348415273195073727359193839911611235553963100478504011455446001076462870172194339487465900231014288065187144053129/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y^2 + 26289576338724805485626704140865651251367608756992336505581185993936927789724108881836366337626941473300712140475378564306113331782056847363960303308144727144388866217845183/191481434464310753596305965031875771767472319561870553339940539963584164829652439373098353948272332197001900686097170411741517107739434168594148045080442171177224938454796*y - 2173454882872174777122009361775165970286582436431008292866207808853554377558651755321469558625516358670025608919935183254169522105652875111871549900546231610936940494803977/382962868928621507192611930063751543534944639123741106679881079927168329659304878746196707896544664394003801372194340823483034215478868337188296090160884342354449876909592

9472312751404660403884815327916132534022094652963699734145148009925506097483242387226494872202941215074204307694861025244501287364195137857235932331733520166965923818640295/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^44 + 211271315754596797759566830452114008033338509388190114771847152589488232195018827262843765078712363306303401787887868120928221835054880859693206104538425565758115649990502611/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^43 + 165576692186961843501637678942971316752145987178141669918721598197634758039261508368314639136331830512948166048442127400696532292283379871171197926114391538255432041216472340/813796096473320702784300351385472030011757358137949851694747294845232700526022867335668004280157411837258077915912974249901447707892595216525129191591879227503205988432883*y^42 - 655426283002502337777642598060793822240912299011384641339344648135614518857344711890460149565345545430200212054917850280199861658100796899718113571954806909569562507280441159/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^41 - 13380182816947195096158960612766228667030686381375300275265254747093762971386402118058108624482038177362796618672342027038519123489135727745351937461147824369298721198720934319/1627592192946641405568600702770944060023514716275899703389494589690465401052045734671336008560314823674516155831825948499802895415785190433050258383183758455006411976865766*y^40 - 193872165752729914255421743484305016657325911574558187815801414136128245561863895977877349950298617318504012552981938941928707813746556539504018392262916505699551365470675567/5631806896009139811656057795055169757866832928290310392351192351870122494989777628620539822008009770500055902532269717992397561992336299076298471914130652093447792307494*y^39 + 320505391987936108987192096351470245167265975585695063712686176831603041940312350858994011258427194569528406436887613064284869015380061271762462672980730639922554964793012034085/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^38 + 694723867879889451489072233159181380631197292060994151370185763514195388022426080250614866768178899491980671552139423327624672390594033749186932832019354220670725783932020672613/930052681683795088896343258726253748584865552157656973365425479823123086315454705526477719177322756385437803332471970571315940237591537390314433361819290545717949701066152*y^37 - 1978788092365282049189592757224412294313976422737003495058838743869849218443197033576430589787122330807957004861209311531519785516785583442507948669964270359571283010020753666691/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^36 - 855938780261419765079042551985362488185288244784190162879587185878612848645060535511002188620875042660086888103789295308468041484101140784904838764205894488802906065648153341922/116256585210474386112042907340781718573108194019707121670678184977890385789431838190809714897165344548179725416558996321414492529698942173789304170227411318214743712633269*y^35 + 8284719229968750764269855022611518447039707455661430297944603949726060217696370302080456058699080548345656732543821403623799993570678293292716453280730052589649644578318795532827/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^34 + 140775123826279229125819777290893604672704545995071664676722842835470843734823614036501827636803402521997191260857379035923680467069196696016842988195420423788404575366613241024513/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^33 - 79424143177960967099927597133371754581774244281052305281898399762027761600026888391785966762257589926308973394087670424212746856437004004457618578828280061487256443050322892864097/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^32 - 161955413841135434948545888868169824190447293297216378404106107573701610563061584389472337234837129178995390789802369946444588612793377297491253657108529774545504619151094975305751/930052681683795088896343258726253748584865552157656973365425479823123086315454705526477719177322756385437803332471970571315940237591537390314433361819290545717949701066152*y^31 + 467096858011845858577818388609943105610468714839243142184668655036908311399048701916971019518430484073408377243594191687158546192601867559980689500593252731564802055193272671628673/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^30 + 1785385030269625551192488823169554594832256879960620241964083641835200160278317133360928822591051725053505074064944796607003499173876413273551117019719087235649524273137346499712663/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^29 - 1944233789856519057325932696267266311728225719180126396957752710664091406226649442781907666474725829082933889226907840763237619594223877657261747190576544095041130880762901966139867/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^28 - 2398736039572052554344083663746114751035733504036365720901154262566208516401380677340615859236048736474825055691281656065198536043306030564774326738487243326028991655972464169879127/1627592192946641405568600702770944060023514716275899703389494589690465401052045734671336008560314823674516155831825948499802895415785190433050258383183758455006411976865766*y^27 + 4356217248509385844182756930432048099506103731892900227383682063975937595747529863029939113257166778078892277413222388229352595431319521600142166588802621512668610516308177118146963/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^26 + 5260054974906035555678360463423514922216165759506486888622600662531938291018054862690791846672008696455734573020519268063738857570386562302067448694296718056526085759708843072054973/1627592192946641405568600702770944060023514716275899703389494589690465401052045734671336008560314823674516155831825948499802895415785190433050258383183758455006411976865766*y^25 - 3400495821952199072785193532877030058670263143266333783888990136621006423448531147805771336258103258276383071424245334591861694041215106836917057198499665850223040832751238818073717/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^24 - 4163188068248135105858645965707877417330363806298678423418375329338194866927156028743432996522575815776366734948848853328332391147414801705432567390912514677168896446737984829482609/813796096473320702784300351385472030011757358137949851694747294845232700526022867335668004280157411837258077915912974249901447707892595216525129191591879227503205988432883*y^23 - 2615951083081894192370390658577080766003999362838483763360580600446001126788922900568208037689695679326332326854081608649614738319825719303627965949457977001360992982455231639401183/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^22 + 611940785769907009005448749048570852653758292436319184308250364538897369007520779101922049755022161013277340017763671357413296730110379233009135927600035843704876243751077634761769/116256585210474386112042907340781718573108194019707121670678184977890385789431838190809714897165344548179725416558996321414492529698942173789304170227411318214743712633269*y^21 + 3649783963936860287137793281745748792065533325254429689572459489465368123978533267513295188768976121061699630647239291178971202467610256052844061516948392482086567632149923202117685/1627592192946641405568600702770944060023514716275899703389494589690465401052045734671336008560314823674516155831825948499802895415785190433050258383183758455006411976865766*y^20 - 21381925484312457370842532315695573945212648192491633154499803772706081206519411776921185515169081151451108033389900411167701887565919086229314623505210909464490213386452520271297701/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^19 - 14339084745524966016160338133967293521987263125799146152055333688745861009415351718126134129616386676540252277498186607113210673378310867265126297113673920166572561252006669784765975/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^18 + 1946206162436026964881798236807425008059783442280751186972030900312957997813355252293197297382337343692739572425124681182356323044269067463503935025664279039659530545017236835256379/1627592192946641405568600702770944060023514716275899703389494589690465401052045734671336008560314823674516155831825948499802895415785190433050258383183758455006411976865766*y^17 + 7770137909913845896098196008655302594898909241465617807868510168155160898917499166081204982248726397764173465008689716447626664955602521883516970854545270528802439197024793689835245/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^16 - 754371307960278955690048075651778451374876964082630571100294800172718390527948759394189837123482639837414433656739450262828039754276920312955918491332546090548347189022341475398495/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^15 - 2665086119242257564596152094199157731267231209277617552577705516138927422683235790609232730086485113852538025927829696829920844819427110890432435723204128193792412254104346298740187/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^14 + 37032709583886108248881529579482228336515751289087570418190600479607758669584957735976471484656807739124892593463387561150067380467422517449346460958232751186013492846760855402479/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^13 + 312028537932427369869230718954087985629716016640951777468696365189689204711697687089659440928141743258233748138160843462741030383324575540725835919230383586448708751914334069792285/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^12 + 31659745818962146185462086342294712325347278524739004340544050103579260874653800066961327992487339638327995593521178055740640694191851488824984404048172916278848423429703836714433/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^11 - 104900317357422199220231888977229822096427540646200937192202924782044916223051151585277445003957278461799402620049035149426728327170870960109962997581777607488184568267174803604157/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^10 - 3913729433781250383636084334806490341644233475482733296508580622189268011136759845571325295043389963396752404261731913982826207613991580623629139057799697735732764455020705036991/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^9 + 6610949005323270090183509275389459557385940113450256693551955463691577529620857195100320854328792976302707973081214593993421758904219664639333431741902922693116142374141906470977/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^8 + 1031251212787196377467839709370036104796776110843451081567635616914883112882016723888896851195751770519119258222681296270654115839956010451613263393712409085546771027108648102073/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^7 - 1259480492447419855834517958559767732660443216303536285920248139114445779151522192711324992007121520194680161008276922768901838556696838681630684580033412438209722283200458236719/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^6 - 124059257678682217185406980992773664821884049819999459035889190580679333252466418060384898219958561311051315983849538588557691907985919620022590353045890216109129125000688787351/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^5 + 93192169569075418699125084183766433869749656077488128135592928737711695489854522402376965571649338986807555005156646442057876309935724827904218961817232740900593835551445651/7815568753645336881481876123750031500713155900484512381222062855656496523659283239718300161153972742734771456575394710683327228887323843616087675309405802905192854630808*y^4 + 9735673317774407224143672512473646707931152993649047312487100081498066813557038674809481933508529093023967524697615778078731303582003857851137591963851019093757460212651923587/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064*y^3 - 975692160939175876404082385947365982901312450887930674880234919246711275087367384503156307223645046920307569787288198819356413537380094378898891495245757497551394879885769181/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y^2 - 114875169807900149711149267442463794018958080464319524808424090782805844013510246208771272106826038065566785653078607062676164843170325155267366240789236742891947630051068871/3255184385893282811137201405541888120047029432551799406778989179380930802104091469342672017120629647349032311663651896999605790831570380866100516766367516910012823953731532*y + 13214232706337667351423626322234027453411721406712259853778409230195022615510049075735595561677344263480070478078200272177824212052515151071694036851862901850413810645481185/6510368771786565622274402811083776240094058865103598813557978358761861604208182938685344034241259294698064623327303793999211581663140761732201033532735033820025647907463064

-366907242295028803270286788968579795694819249856220377402475600734311655649086145172175630986009129143485955881526942971882251035874466334815027034196367760642247525159489900383089/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^44 - 8151762419618264845428275452603407409367013831053302417807324175478786756872970548242997855548816325377046656501559350619559086358386417889810844017657843028643740100422924372654793/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^43 - 25301123704164645251275936645885904791194097005099932272497265708647131753764084243724640222574724466562896796406522083501832204676592165505267947668308132671475575752256578104485704/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^42 + 29778398557643423974359810731071378025223405473877459636963032188680020614075700384562364830670789798526083377223150164292828718044245903468632021915455186999021289786364956738146905/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^41 + 1035291480350911929687543195284453816515489771133499114796242793745278493999027343859611623778638454812765869716888761173051755246514282416492584155048307316567238315197549204634944729/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^40 + 4250854882038870067714844249923992427712404426527557514660742024043653359716952849795956191744081309114143441345395640229307867722660438582298306204631835482292084061030310075699918929/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^39 - 12783950770115002948126682754140493685234924831654894858190152680896190499773564077717479726542754803146645832201891333481822559079665974370140233594006076451887082893913840322973278025/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^38 - 186163775765256988169339365459760700444243498194499949809679027378258137824578216168101025994458242633142850822107508356951290699830197189781934570778831328514343344637787975867809443157/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^37 + 84726131508054698303145805326575444136577587682533569759449983647097324828922795573241674285469235384752037919256275676997938017418910401903106777262076859736427356703428015231319993853/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^36 + 921090460499162756961317226881135409805063540985678556407993176481275199602652489945400406534320447760620534298572074901669855805506734683733135921449811569153801136940930214223912278142/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^35 - 400834550943406694830836958247318852770373321313506014931175968422519895981463814078455697248581889630734684882881890025731118623708939843953636757263660128316166208846751537304894811044/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^34 - 5419219486279183428955398879418826147836416480003787394662547101786748164991571716284003915998791408730788768421989306755846657385397822046446551907717071300192832849494311945397844382341/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^33 + 4017216351739392381806355651888585199210655450892705687342982983333879613362394706324274220898291166821246953503988300809106496433930744266095276876446889784494277513886006911514131067861/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^32 + 43578062908360613219756652831133617041622012364457965213714465003351356588641449383895443135185877622220716108497074429804478803087134075702099147541764962280009467163996236659886745068379/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^31 - 21877865382192993862108234890710904186616583221423044381050417640857710318589870657657700768265988253139664621816329301834263308248721026306403617306120637087230513981616255645942668546243/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^30 - 68235815727795035177250959614985673688751367364332147221334469266615116237869047081957236388593612124648979113682441221653447795058822872815993656735318828950692797088118961347789027199086/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^29 + 87176921196359388518918813302837150397232530790184079555364074305131223262664723459385278682251817746424338591468660054320596753583947524585210529522831927690286014665197326953459473542775/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^28 + 182138686021485876749221051132162192703935692708272820099793912576073361181381545165137758765952386373182340432234836210017202985629921191177267255927640807774458316920703687769801063867606/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^27 - 200457640306397832796255414594130639083012657928486536906865763798480296327838635617720724565932348800848622166629778009735430370521228461652537681210810713873308886669605989503300110637813/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^26 - 399042525560356712185105124111481264119056912244090117628533643038996047678479677834032358346451674973673436379127776028906128339127714608010611619294780834669566008094782919241859875737865/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^25 + 201271852541460668804127221575486060899434586726168629555297556028830583154012011369214417563323040572528837495298706566932188042882745737110365667199937841418180861218386444578278746440795/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^24 + 636861681963295831750580311411463180953246335333921817563038245657131266090950053692850230459921997442592207090402253767982441103132018050092956073109599057120966206090617055262888826251874/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^23 + 45832750203168084608587342177421601669021499529939501451068758696946590697755556801228600986590825180339244747898775624448985704252716852790491675642430125530361951540581925425530861812637/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^22 - 668660058115895368062610011013696692774935044465386628319666795331975338311631384357470567254196444523495081765499988593305719451066028679191494141224008145226862986589773174191025067636755/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^21 - 224603533772040243432529729856940855258359812379313983725470288682321042191649193971011041353615762479776534526033560648834744985981397968426498321891131565936050476018013036942761469988226/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^20 + 869741961030232850903383974725158338194068415595477401279330185082067135224353471749185781996041549259728710833179707286728753683238688835119392807562235439416123107775454620373907155278231/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^19 + 480363927499479495148089495954677937427386168031806554294947884655201481144998526275221769158917155307685026998335359811674741361283277670256583748504935995495363269477021288430365942756295/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^18 - 172689456734955077852224295492217376418076637954342340992546814752932087973238484698382987524141597706082700121869343640408818096369030795036749007898096552495330281999555201925257052068406/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^17 - 271866591579201290264982858623042916652363858436712348331347460750551116414726450708986678214106126333630457732511695935476814953299843985339918344134818438399764255560258361963998037429783/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^16 + 41576473453193685833282218977170208964888796672677483085005877646928398560646516883056848222997176045818969935365142651518770769308752140990364347868639250292277616072003505245747718793686/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^15 + 96703267852561175900295857856610659371008178237151170918971544032917913549999799253582852732467887433479488796336181489842251871281621691163197809204462022361272687806941771283921411829951/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^14 - 5800679924274344007200499624209881636259251507241289404513734196096233263568650907644257658802851660074187513631582632284341386507887322532942651297585988322804808729115799816124027266716/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^13 - 11733820540464230745560331898585748551825459670319033578256866318296382298159073807017783506303414173296948038253327071600960152246689427401199076433517606761982717530377694838483752867530/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^12 + 866131471514886054919191345310438664058814133419748651392516439347186458749443516014820004764297219755311709424281272884801005009445167438607099505570509683289636624668319570395391317183/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^11 + 4070401152297527764384406813111839293655282192918026544225893738552493533783410372611682145181010167648742852012070753475461752340439513013951945566549556456388626068066535331776568667131/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^10 - 26802661476197214004365882415048889230189893490148554218277524481856621266955667911842898812763547688289626546981269956638394037904562179130701035252447037503248058824372451052803253984/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^9 - 261109771131428033819019381616698540545683160180539932503476813388566024844089662803057307633949963857090364468326516710391928199456862894941160417508303186526718165477766541089335831895/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^8 + 5228630902648009658015031477816004670334783179719340764724769250080158905247242895395291363437034679532639933162973288497672561897634613378143579344292560867806485022809763245639330609/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^7 + 50052459308100797600858491967284370972057519125345049905497779026019725358068452016554634187727974282713510644869220366613291642960169013237172284620131805600873464774013668701806984041/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^6 + 534272017689174089530814736784929017606035435156494600006675911807376381102000979550911319089605871851904426075904987954910060958809412287534428975176966754684786646071431193550226267/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^5 - 3185893784793771780639830602547045641552850305695092429566983914086418180087412490744479503221558669460239234663036423658179401295290851540352478969645056262404153057053808593573036129/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^4 - 125644936776368461306733382546869674692345885172943107632155945221553925406801965282526822892453311001939441676122625879724341176718360632706451886750087050311924946123000351003536433/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^3 + 47623247449535744238750088719477995246038637465777869282451606881842550205044220037762067201582567279955079943295579717443242737775839949812212798761483203773555147526905528080614066/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^2 + 1640117250038504485104841704139138062340798400300857839666739592018546110155048078915552873008012319414416372879331469169526493983047382658069011375573352731309620828325194405560372/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y - 440917947922806466470505978496877215482824740902527388486259233134128937916140186721728048668739451863096293962891074487991402701988871500261368540262302805680900655876317335171017/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486

-65289557816478292596081479873790939790087307745048487721948205423278790696760650407808428995191731767588989166663734543385365616296116849341747260911141619778624632453218825575281/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^44 - 1413573211117890336334910713717828944545778146556191528227066485917916425813463511579400774266028124392031229095775924000816408907343481471019136028345774034317688475496697707537815/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^43 - 4096280140171902636416410529861377923769060344529252618394802033599636066378093304899670792239908808384353782491789370748137465281408567824205409938144876999296437210217540030932466/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^42 + 10178246721604490694841066464344189154506838565058470253085841685743261960957221388163399832148041702146459067046584532149581892562172218413064911261729487661505235817949731237365753/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^41 + 182041177018227864887452595128752052146770556717063799276546832939588844970762402193327301024978740804576487373038484139774535901374230762728428384670700939924917167323086603623116072/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^40 + 652517121650400577391550962251173849508216824683386506226433866558472364910860209309715592488490171719366282420008764986529265521722890854766819671205898405221245396150931920448135584/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^39 - 2675063774665074639128794046914419745195674867098229372701426999940803522160131581221641465295181332391520752469487397038461794404957311504068169617075744346847321779082811101204844519/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^38 - 30321766609302360327605518057627518652997903045108089935476469548038376387106532819893698955406703606821120402308542488245975729618190818717080702798104295445113740549409466533367094927/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^37 + 24097507731502992540170153013874705767804585021256508673696436014345445701434538275648932060604344068979774040699711840190821778968005964596864433455380047253587498075049007456962422673/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^36 + 152846707592727345963398345989444386161741471843027341440593257207591120729011245629182409550664437525527261644682786859260427233701376373931607425753307651272660776376427381247190401536/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^35 - 161572644607866863966890809791941011960051090664895371570203380824910990008104037373120640245081649867372698620341717421924828864733661505365217329077313936892884688426275843423260997718/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^34 - 898960481343452007158130452172189518773608972163692941417848921880458262049735278183902444477932561693971427412649265001812910287997772239594176028878748078875074176565791486582063240478/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^33 + 1779640307317193352520668349931497008005658185057305511106050122735161841910903884549229578461195362757762285131126552895477381045258795688026754934007032809404721774347604762333662361097/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^32 + 7056269857283739649244026898672347463061438385611306806299994054005033233835585500585459071872763369565680087318320715403708435026216923410283175270718630028659189450220624263155407158741/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^31 - 8141070035913466817350334544458071883742935351051134090362642439021150449771067388184742462551288473943753401120012629399139268566589838269230613589125776823009936843696976693345795368383/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^30 - 10453586394086542783994867043323577947388592636225543709100535087656768459605651185315383717360202093299488988961466740906471146358440705736775941125655528682717424970087187809079067745926/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^29 + 28530258144350662707971784986721613602511872823662651970503079090390938934360260775216138619280406474838380637396790408045656575898374648783885708833446558134079315439904175186063587524461/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^28 + 26203875276132059018781037950408843734793614531701040175559487973566269782571199335316997251057100531844758561683487590625778382733153519504679402202474234704970339586929759658243479774173/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^27 - 69575067413728899006857394571907975699421451258417861281192901671257163201551583147166873146410163090375565922985480785697829007067177484772093604560821234096499206394523052629626109388941/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^26 - 56127245559592870794963007746413150768408752319144002295886650530952653162722957812539691372687183332556886177440256131984956748121451539525230349336435651344356789201763465734854573843151/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^25 + 109675665116111263815499626008812323252830360829775631355797439577637973025645343205874149141672989154565771682938531797470000817495130714502264490447291789672549106186024716509535827934217/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^24 + 92776132589910460960446748218887370773702281641306972777542495551052848743016313469205809745652620935176475444949567593914858339533921719777316054574328896353646308976548618161479781454778/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^23 - 52104404382411704484243457895866002701129614441141344159500862535951050367845848058183268760090705376376246067844966105113339693295624593190457230206313146981820783039431656582164191899412/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^22 - 106941008602596302281005556442934106076363724061341667120924431520572975564312447117787904701944719565424972460749304478048998808907833310416817031316414245738338465950310769428953659016463/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^21 + 26763213017450678599027348414670576147408539377238820656399893960108943968147097750098657488083862820258047346215473289979321031837820752293251610802439488959100280985005417320313816215382/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^20 + 164613819028537600762242604970011733598729754721977253388601892976814053139327211398914633467671408232344949590977328559209325171755924789990037581338771714888885222564860788411106083133803/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^19 - 10152586635566268458107245770550683147720862663519409125848750420388632294257254990096623650359027158632045140484900907629467160719043798449393228291605918472761299021151855578243404205723/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^18 - 43107415915175554161522544935969212782240406893306586406533459772754109638662321473620084054783772171844900453712794089414858526453194037658857947739296550701145533330315099486212231788926/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^17 - 3632961703206101351564226754281650627399522037979075540538174737665401677207836648139169611674688831096687548544221315624606308147481717345695354652025807783962236874692996240849873384207/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^16 + 16136799944793912675795570509565348737861471812243190356979295646206339560553915565926724664932943024424794258417264596453143741014708563861804029833758774506028297907494718638745214359232/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^15 + 2974036521750807150600169865547506031806324414453055431523388108173230628186706522792370203515755478406673545263978753463642905538319272172680380427847286993970767743184628986962380222573/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^14 - 4557734230996934387100530069375853252395571771062128296094107421229636707260876599870297699724786738018517111814131986908549468284670993258700950355790604557024472681273471735846956574317/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^13 - 451150765100252766003095863194066337053891280884102544778737335526032900438932811510147440885172020020976252681180101687517037724761779042664418602875654451902452093575186234138544239908/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^12 + 2016093824302477036547651198455315876738102947436247210193502520835037305424009959945508812087705240350459875940818901478823690117206636150687356452709834036259730168624591994659661608271/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^11 + 130071289767092341826752022697259847678565403891763978134961079262528545454680347245407510929471732656208431343155431540727339424698541815108721698127133905990287048414894514630574720493/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^10 - 172313238993085937588611301753356814826716558181318142592776703392933696293035047258514692963202836083039306430119982223494547850818177102917293765541503629856221849393331964288765201057/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^9 - 1219029637888872384720264349793627312804211932234155530990088846888001781099090615068979920180076861900812953961768604722783881965499673652810864839792834553714794235221211514235951185/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^8 + 42746143719696804388162975284045288608660952075278396066280016471681176392601137646350898649553047697667475579052316146457519171440753058541784291886812359377916557102219919702437316067/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^7 - 1833170504787046254554583518976994046693529906857946232381430242332197433524132206794453681910147369176174343478973601327639728962944286165042274349012600227336228765341010440989575499/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^6 - 3680124982732008973214011911542895159468828824546777284606464581665128004396812294071906576515751130059324185293124752961575823967361029302335076353902176533842181946601119391750881447/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^5 + 277823718891202018977521598780378081738303521503830750031694701256613845069529574365131852457552592916247189808940005349828535878815504400141877438846589164800545196693582318541403163/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^4 + 217890150578569140607347844354788292951968065623094878167392484841951585819380980045769203433457989687250024063298127018419456265586850783723584411640679928537115599019347950818207237/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^3 - 10552198051926610169394246448231548901951178074653453311948801105182476239412340943466590318191004206966205490680947289960359357863533246917969403861778925007573459763877937254029362/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^2 - 3295262807636752580323065902111589097905693874745240490027791932219657295826676915697661125075714694729576049621486933055830748487341276727340520039247699907427450758833128639172605/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y + 577186567962601577750609518911391745731773273492115751934471742968826934846922260285329946683202786700716663958955318470738124996060377899398164250830951375473417362431056488030163/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486

-6804156896354911655339822067080801441670452998909267890422722717666524898944566301663567441725198141153014101815102286416377356968910509198432309574233563732404211339529/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^44 - 151563758960157299673011405255924321583673243579884791008240222781829877948539883726941332212094888568541632476019752773491434254217718553143982422978689740947519224928461/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^43 - 118399030585287076487697974731349593417090159662043763787541914985431995898473164705385741140599943905101615489917828206791806198093402886254294138800519647545165806197570/57467417306215712363837324439338466917008499268268473391338697468062474438671200292046324714367446637755672474819078755024464918289145908941821141980925021361712166403*y^42 + 496467391234192965850911992094703443522545992365448502276434565020794959526451973040449191922594543426820989704565124004421669834097479170124429798917944691804610219040913/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^41 + 9605007190072289255255321963878285400426391711526825857966960417785953416378580910942912850836150921762241063499628110243473946418386757354402257880875535645176938834848283/114934834612431424727674648878676933834016998536536946782677394936124948877342400584092649428734893275511344949638157510048929836578291817883642283961850042723424332806*y^40 + 39970779264917140654020279981226616849785267081257782822469917684726674531734257589484316522769686683867492426270598076676727059963097752812565435808955355762095244073591883/114934834612431424727674648878676933834016998536536946782677394936124948877342400584092649428734893275511344949638157510048929836578291817883642283961850042723424332806*y^39 - 232318183942765674745614882191745687280736072483242043273045574104157533318291203361027843601446240698022238512539349750129770461754698781295603115760952549290714913573881303/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^38 - 3478028544941436812219175591627676103371956247565772024757272786001978595605740895625174505845129454035402295947508989296110906820765200807886423872428578829288935153788609197/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^37 + 1468938239349877021831819705377289987206331785589382261269126009467316676806080971948788567283933498121653560154333277660831864623538819507305945477518019493904740139721662957/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^36 + 4288393403405897043572330863671681122457753043537906034259754866286963171744289651341388093645937202414736809885837707796470427042569061865570443618322383671016795032861494292/57467417306215712363837324439338466917008499268268473391338697468062474438671200292046324714367446637755672474819078755024464918289145908941821141980925021361712166403*y^35 - 6427897192968129598686536108414933171496799684988564263555034471662088459254745013708242784776284313806874330702655034596371718165933987138944506756347431302983557718669393505/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^34 - 100744962189383992222955496223067781406998181181278573105472105908128989144621883633590724307175521746875801976770540740578370098953945588004877076091685314022607059050675134539/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^33 + 62678968852654947695741819110685610895532501907403191679711249079835285884600008856868818218055878997387275516507653444809156772125122113531416233876587283662858122425253075783/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^32 + 810321241534664392294818287646810302071204548999414394460303458860711268690272140759492318088796927452286246482934946557065399700497347122636894327720490455047133689376506159935/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^31 - 357910484660362611309633943117942460233828925289059331692241543315572514712621425516141165071290983730710726022898054081579045231775410954952293399284848916162841577359571580119/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^30 - 1272927067440517596982281072177438643338766055854016422847858300270487459664292079494615072575860230070237566963610117424367467543410556357450292621218501946210142628188898278837/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^29 + 1464752417268093675282513937197007757550193542946851344805495510625645288634994943819320941810830204762850003775363574642859528640641496348258953334573729892320984641494390460285/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^28 + 1705773072626715970091714760930938380700334440536952766440200484471219943042248940482679206734069370941130988400387796823573717238031923743871515110261119833723420103740361231045/114934834612431424727674648878676933834016998536536946782677394936124948877342400584092649428734893275511344949638157510048929836578291817883642283961850042723424332806*y^27 - 3305705716926655020529320771508919625311485774512656713849909528522143497218646147703145454299208990042289103538064731932403727463352957657213027893767171977724587325616089548533/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^26 - 3737025303365702916310164829958999443014712906208845937991953030825436296152650291447473763417597795818276135056774213503706673312062906687706151391704782729998586810252184308319/114934834612431424727674648878676933834016998536536946782677394936124948877342400584092649428734893275511344949638157510048929836578291817883642283961850042723424332806*y^25 + 2827466095912585209308249603389748153253372920426827578621085708228211920641211478529848508606055313319638251204122604345306439704490998148572731355068866271341770020372771057651/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^24 + 2961573584930643202637909692040881557731183004204106968395661950539334606542081214748268358359220068169724659007276404874767967741971262162546038097781724758707931502988300895825/57467417306215712363837324439338466917008499268268473391338697468062474438671200292046324714367446637755672474819078755024464918289145908941821141980925021361712166403*y^23 + 1563154885887074812910119555240433153074512791646934130820477040655654440801035718563659968935231717400599368523675833024399639746799793840423124573578382975994853100177252312805/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^22 - 3059374326674062542223170809312714016037991752918641952064223252702999964129292891855216195064551410004867524893765872292901766845283929315471249428297559846190928596290177704795/57467417306215712363837324439338466917008499268268473391338697468062474438671200292046324714367446637755672474819078755024464918289145908941821141980925021361712166403*y^21 - 2445708829928231882756395262939390394126308959720333517110509547193007251091326941822896547147366542313794175875482919020926561553715762746170597079194585355179904823803577477771/114934834612431424727674648878676933834016998536536946782677394936124948877342400584092649428734893275511344949638157510048929836578291817883642283961850042723424332806*y^20 + 15410895411626312311458653506392059830961407852218136120510345924060788306566997584279929580787014170039566237379002583371169577459609807199879770450702861700712124678678387386883/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^19 + 9798671885968617950376861122307776600991807322640151701074162288740375418507082594265150597951240781729139116000083816440682043947055170563014548073694670521977927167862402341449/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^18 - 1433777379995596304292690498653438636669840113854565731055641408669008386606550340199431993355096315139265084837888395671987737801859278577362109658442095079608127394437493666843/114934834612431424727674648878676933834016998536536946782677394936124948877342400584092649428734893275511344949638157510048929836578291817883642283961850042723424332806*y^17 - 5356928487018172522629553821956443640532588684784669061749318715144874669819669430836048053255158071411673477944619251372482412772903433421180336128496519239923272884993233843115/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^16 + 593005385390343425178971763386744413158757024420385152504845769869243299826217692978551114802823523659444284736010595610331103415430632617786298401286612286800473914700641644345/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^15 + 1850751779879955768747683266945052982791976454245419697259288370949247992427592163467755762252250462553463775384960208183292626115940709908020007431291776574307378012410706906189/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^14 - 46693504617768176484540922689703624354295473370826439960958703022609820810407297334409080086898407401822006418087867665110881362462805057193574078406593189848083435620640688217/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^13 - 218262487340420350280823107784169209173922044717040191225227310652026887614220374649768412696720500131860110454382171415012399730369483696516222401876176447539162159517600433623/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^12 - 12738375900217720989626755477973181215273502574027192315962950496076799600083808184008909047966078713601997908421222828089410073380218067594025280220350829679780151843552258863/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^11 + 73830329344273391715364900142402391457748631956444639052590592419640974067458063614902370644337154113217655238796598805905992589507244054893888954557114698432990498753947734627/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^10 + 1979904844998574358214425197889640729064282663737012555147599319197866021295222563656078084573403681218338837240806022324947959230832992343545133769075338621476500549673264149/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^9 - 4669167617280873563452355336667750089681275187213296868431921172763724782581002972202208493598295110657925237312236210099518178691542805653801639448820776772764333507635743663/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^8 - 544005342411610596749373263846052127460769901701495969797419218955506661485936963195350405361559916733669294781840948750706469724515811804730818810533989232509576399337340631/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^7 + 891504245865728730329294207544583258305390464353388373229850228087503089510828718399559596292409123997735511768994355590557283265945169103554327465603862150046143959442237713/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^6 + 71228880546998937598208474478394140040947257442271081008524357650424735486267133989810761598506657956122631926219115439852941442644781557651766539210305731964848652688443289/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^5 - 55467220327067719030056628057984598522246079193170481516718495351216538758984113219204908818241302200605281240130168123598256136699023247276400979511317600496296347642285493/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^4 - 6084455874262028511083894806424705201933644139600573973256107225704219419335241584722911489236343895658800591454151883897574391853045704888798542210291545893794266007322141/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^3 + 743644651698679116208533630579903102720859459971376942810341995931899706725898297368166931964187472696890936273255360657780602193130201318989787094247475654980833359263115/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y^2 + 78534047664168623234376813506141599396776495277118256072680301424610098251388805573147049027444303393833339221823368239454833474888877062313758572111623614052695397317681/229869669224862849455349297757353867668033997073073893565354789872249897754684801168185298857469786551022689899276315020097859673156583635767284567923700085446848665612*y - 9351371631468602858472084906739174664971620345661752006832845519445594031627389281978188760762516713845330219807087325661551308216664582270713541757002011593902045226143/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224

-366907242295028803270286788968579795694819249856220377402475600734311655649086145172175630986009129143485955881526942971882251035874466334815027034196367760642247525159489900383089/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^44 - 8151762419618264845428275452603407409367013831053302417807324175478786756872970548242997855548816325377046656501559350619559086358386417889810844017657843028643740100422924372654793/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^43 - 25301123704164645251275936645885904791194097005099932272497265708647131753764084243724640222574724466562896796406522083501832204676592165505267947668308132671475575752256578104485704/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^42 + 29778398557643423974359810731071378025223405473877459636963032188680020614075700384562364830670789798526083377223150164292828718044245903468632021915455186999021289786364956738146905/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^41 + 1035291480350911929687543195284453816515489771133499114796242793745278493999027343859611623778638454812765869716888761173051755246514282416492584155048307316567238315197549204634944729/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^40 + 4250854882038870067714844249923992427712404426527557514660742024043653359716952849795956191744081309114143441345395640229307867722660438582298306204631835482292084061030310075699918929/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^39 - 12783950770115002948126682754140493685234924831654894858190152680896190499773564077717479726542754803146645832201891333481822559079665974370140233594006076451887082893913840322973278025/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^38 - 186163775765256988169339365459760700444243498194499949809679027378258137824578216168101025994458242633142850822107508356951290699830197189781934570778831328514343344637787975867809443157/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^37 + 84726131508054698303145805326575444136577587682533569759449983647097324828922795573241674285469235384752037919256275676997938017418910401903106777262076859736427356703428015231319993853/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^36 + 921090460499162756961317226881135409805063540985678556407993176481275199602652489945400406534320447760620534298572074901669855805506734683733135921449811569153801136940930214223912278142/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^35 - 400834550943406694830836958247318852770373321313506014931175968422519895981463814078455697248581889630734684882881890025731118623708939843953636757263660128316166208846751537304894811044/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^34 - 5419219486279183428955398879418826147836416480003787394662547101786748164991571716284003915998791408730788768421989306755846657385397822046446551907717071300192832849494311945397844382341/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^33 + 4017216351739392381806355651888585199210655450892705687342982983333879613362394706324274220898291166821246953503988300809106496433930744266095276876446889784494277513886006911514131067861/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^32 + 43578062908360613219756652831133617041622012364457965213714465003351356588641449383895443135185877622220716108497074429804478803087134075702099147541764962280009467163996236659886745068379/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^31 - 21877865382192993862108234890710904186616583221423044381050417640857710318589870657657700768265988253139664621816329301834263308248721026306403617306120637087230513981616255645942668546243/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^30 - 68235815727795035177250959614985673688751367364332147221334469266615116237869047081957236388593612124648979113682441221653447795058822872815993656735318828950692797088118961347789027199086/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^29 + 87176921196359388518918813302837150397232530790184079555364074305131223262664723459385278682251817746424338591468660054320596753583947524585210529522831927690286014665197326953459473542775/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^28 + 182138686021485876749221051132162192703935692708272820099793912576073361181381545165137758765952386373182340432234836210017202985629921191177267255927640807774458316920703687769801063867606/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^27 - 200457640306397832796255414594130639083012657928486536906865763798480296327838635617720724565932348800848622166629778009735430370521228461652537681210810713873308886669605989503300110637813/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^26 - 399042525560356712185105124111481264119056912244090117628533643038996047678479677834032358346451674973673436379127776028906128339127714608010611619294780834669566008094782919241859875737865/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^25 + 201271852541460668804127221575486060899434586726168629555297556028830583154012011369214417563323040572528837495298706566932188042882745737110365667199937841418180861218386444578278746440795/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^24 + 636861681963295831750580311411463180953246335333921817563038245657131266090950053692850230459921997442592207090402253767982441103132018050092956073109599057120966206090617055262888826251874/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^23 + 45832750203168084608587342177421601669021499529939501451068758696946590697755556801228600986590825180339244747898775624448985704252716852790491675642430125530361951540581925425530861812637/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^22 - 668660058115895368062610011013696692774935044465386628319666795331975338311631384357470567254196444523495081765499988593305719451066028679191494141224008145226862986589773174191025067636755/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^21 - 224603533772040243432529729856940855258359812379313983725470288682321042191649193971011041353615762479776534526033560648834744985981397968426498321891131565936050476018013036942761469988226/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^20 + 869741961030232850903383974725158338194068415595477401279330185082067135224353471749185781996041549259728710833179707286728753683238688835119392807562235439416123107775454620373907155278231/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^19 + 480363927499479495148089495954677937427386168031806554294947884655201481144998526275221769158917155307685026998335359811674741361283277670256583748504935995495363269477021288430365942756295/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^18 - 172689456734955077852224295492217376418076637954342340992546814752932087973238484698382987524141597706082700121869343640408818096369030795036749007898096552495330281999555201925257052068406/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^17 - 271866591579201290264982858623042916652363858436712348331347460750551116414726450708986678214106126333630457732511695935476814953299843985339918344134818438399764255560258361963998037429783/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^16 + 41576473453193685833282218977170208964888796672677483085005877646928398560646516883056848222997176045818969935365142651518770769308752140990364347868639250292277616072003505245747718793686/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^15 + 96703267852561175900295857856610659371008178237151170918971544032917913549999799253582852732467887433479488796336181489842251871281621691163197809204462022361272687806941771283921411829951/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^14 - 5800679924274344007200499624209881636259251507241289404513734196096233263568650907644257658802851660074187513631582632284341386507887322532942651297585988322804808729115799816124027266716/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^13 - 11733820540464230745560331898585748551825459670319033578256866318296382298159073807017783506303414173296948038253327071600960152246689427401199076433517606761982717530377694838483752867530/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^12 + 866131471514886054919191345310438664058814133419748651392516439347186458749443516014820004764297219755311709424281272884801005009445167438607099505570509683289636624668319570395391317183/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^11 + 4070401152297527764384406813111839293655282192918026544225893738552493533783410372611682145181010167648742852012070753475461752340439513013951945566549556456388626068066535331776568667131/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^10 - 26802661476197214004365882415048889230189893490148554218277524481856621266955667911842898812763547688289626546981269956638394037904562179130701035252447037503248058824372451052803253984/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^9 - 261109771131428033819019381616698540545683160180539932503476813388566024844089662803057307633949963857090364468326516710391928199456862894941160417508303186526718165477766541089335831895/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^8 + 5228630902648009658015031477816004670334783179719340764724769250080158905247242895395291363437034679532639933162973288497672561897634613378143579344292560867806485022809763245639330609/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^7 + 50052459308100797600858491967284370972057519125345049905497779026019725358068452016554634187727974282713510644869220366613291642960169013237172284620131805600873464774013668701806984041/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^6 + 534272017689174089530814736784929017606035435156494600006675911807376381102000979550911319089605871851904426075904987954910060958809412287534428975176966754684786646071431193550226267/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^5 - 3185893784793771780639830602547045641552850305695092429566983914086418180087412490744479503221558669460239234663036423658179401295290851540352478969645056262404153057053808593573036129/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^4 - 125644936776368461306733382546869674692345885172943107632155945221553925406801965282526822892453311001939441676122625879724341176718360632706451886750087050311924946123000351003536433/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^3 + 47623247449535744238750088719477995246038637465777869282451606881842550205044220037762067201582567279955079943295579717443242737775839949812212798761483203773555147526905528080614066/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^2 + 1640117250038504485104841704139138062340798400300857839666739592018546110155048078915552873008012319414416372879331469169526493983047382658069011375573352731309620828325194405560372/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y - 314257330597608893012843679133533336150463939739581331956732296242474038999025906941189987591673615671466782421405919054876633592452494122653502409138621049239279070013564078021531/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486

220436888289749574966223767686294251472756136004898313897800300569347216090059949594088237383981735757021736568490168256496909916156907100835556882741076804186371650364439/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^44 + 4923987954263749896365540212179001255837351580963661470130462254683549307815636098573090294087340712127438361350833257599146150693184764288569722593794808714994650199533019/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^43 + 3873538414957534119578766334527535884930009978142875881420400692549748688868569587584924727940778288869236233717797434047568373977293514377521279327787928544290934025032358/6838622659439669771296641608281277563124011412923948333569304998699434458201872834753512641009726149892925024503470371847911325276408363164076715895730077542043747801957*y^42 - 14259264784192193985703275729379712112847992784076371368243943624436672211174149131130762677813756582294045506570250289170650487776049948177657605318028973251761223701554087/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^41 - 311557750308573562461685480772367520494838776112304665019995782405639705566079882413387105793441104772542460452175280374763837331987361157302370544350156245381019890997044183/13677245318879339542593283216562555126248022825847896667138609997398868916403745669507025282019452299785850049006940743695822650552816726328153431791460155084087495603914*y^40 - 77307470369292205167812111847652689684003824484441166767383120982829499464051429023454252657521865866769157421755309430694297888543011947311408219348215453098730183433528305/804543842287019973093722542150738536838118989755758627478741764552874642141396804088648546001144252928579414647467102570342508856048042725185495987732950299063970329642*y^39 + 7376110426604922443125796942193762472835826498726632346621356737866146781602704522617119560754791152308867447319372094475721249709110105778347942264911135301315007185706193673/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^38 + 16243274081464675823872067260812354429082778805538840855080038600259453218852060628244303035439074239209955440611617848475594941184180483048136496051738847308136639736665597613/7815568753645336881481876123750031500713155900484512381222062855656496523659283239718300161153972742734771456575394710683327228887323843616087675309405802905192854630808*y^37 - 44220148353791579811709639039311061050664057893048559064229320748039366006895922834784979124694970698439228438156275768652098103663974935036963416794763634182509234906996763599/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^36 - 19987627616096397989480560292763626622419898076413374204155688376447991350219107963382041842645932354248170698881255473590818773814505683107092051946306336194828649197732367724/976946094205667110185234515468753937589144487560564047652757856957062065457410404964787520144246592841846432071924338835415903610915480452010959413675725363149106828851*y^35 + 174617016841165817751555273652288832391091772330450650684998009338532108052353803822251585050805447202316491532694123222365288773695282471442265945987816888853066527698489009311/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^34 + 3286372496385433057730826062153640226401115389543522784978385146143221406866798653838077128260505119349537261181369698672230579733425619186587895119301232402390881728958931736653/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^33 - 1634163547930793072271431874301321436246350113298708575213665984166176974211140069580254041813896632723229887416018103347093755148412056078111648686121149281436501839468197399529/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^32 - 3784431072913414700375439654076867246737297383428587005159778000340650161042310641287517758853587893880664692018450352033206919446269605235324188430332980853343928531743547912799/7815568753645336881481876123750031500713155900484512381222062855656496523659283239718300161153972742734771456575394710683327228887323843616087675309405802905192854630808*y^31 + 10011789614537625788195491022874635746645252404561868675097549201088204092633985256584596709970760713698466097882917623188908896005269370818392049280709295716729382343766078914057/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^30 + 41825753181446866580255588092850756467211302651559976749816067049073491476302010524605712199959323280964728139741059052813558667904040960714473123926784454525654807126849088616095/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^29 - 42582614005396605022887335098616176184317068778420109442404053479491937967464369187432414809678395037318655788672052105718657583327940190574182414398551124887969777715147590277211/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^28 - 56351858535385745157445199021764853293304502728532120949577172494605708769337469899965814760551558101120686136757975468058133649878120964572093649279959033241158172598607654836431/13677245318879339542593283216562555126248022825847896667138609997398868916403745669507025282019452299785850049006940743695822650552816726328153431791460155084087495603914*y^27 + 94351951602212862537079037870074513679568605444868347214761969527691760882255717214812870499138224595500428776231057692328983953839066878426125904243739223991771508778089251511563/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^26 + 123666808940013405234282245160989653737590368142231854566298981456373181181104068605306629339991992403438715442056290296136535395789229318869693227673199504361007034605638203243351/13677245318879339542593283216562555126248022825847896667138609997398868916403745669507025282019452299785850049006940743695822650552816726328153431791460155084087495603914*y^25 - 63826927368188044850312424618332937114042234967481567387930533031995033944077674574267593582892879243920443694491174848023274963931319926840041746324892108229767362917261490927237/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^24 - 97677775656695619854581630864255385051737864464209152839987107315202245187297963596085313204642060788386693356276390879194031039713577183905353411483885546464849023692961550400961/6838622659439669771296641608281277563124011412923948333569304998699434458201872834753512641009726149892925024503470371847911325276408363164076715895730077542043747801957*y^23 - 73182887030522339118693049763685094325628331705574492854672292120383038491141445461705103028979769858047938412835026881370645035701384753985643842162963156948714152742590140393875/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^22 + 14280195982937901634810069472539090761848957768155717130298553136042653124171544184979065807694587465147075425642751586141086354662270390859640762746738009590665246948645820365701/976946094205667110185234515468753937589144487560564047652757856957062065457410404964787520144246592841846432071924338835415903610915480452010959413675725363149106828851*y^21 + 91578007950650010341744984486981051813815856262924244340385245112451295906443437923983365856849086277247633262116779015739441457057911850932358554268776662011543442519620113631373/13677245318879339542593283216562555126248022825847896667138609997398868916403745669507025282019452299785850049006940743695822650552816726328153431791460155084087495603914*y^20 - 493449678812224632100011934552758443508190222447745719505005754076837481149439176818214618010878386868965346420147014508174714019319727983241466163475382248831365692534294743413909/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^19 - 352236398139709674959436315455654903369667698471608319403902845550235779105126735511754821770309351715462261411649522686217210281952059784458663779377352687819311558575890858938695/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^18 + 43824853309515488355119393127734602150260911977227963461710388617983056153045948764223124893514794671505255118862410450388256553029584567855300436594571882028149330477117331437331/13677245318879339542593283216562555126248022825847896667138609997398868916403745669507025282019452299785850049006940743695822650552816726328153431791460155084087495603914*y^17 + 189477560138766849864313023015953826765648261183584522467086299005579220043624743818067408679820864722355450586795042823352622531102248486506113905936047612838991999476894432444557/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^16 - 15721633122970923227493994817724099369546544549821258941224054336034227853817030125317872635342579900338411743853888057295414347771544826194862324594955804489205465870302575541491/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^15 - 64901565983414786718556917914763219751108389902518957480439940866282192148381515014484413830806671571492411878181723704289774522913676252325677418103111335423553101789707958861275/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^14 + 141674632858397737635626403138703253374233566809236130797119150548277978823372171679381838756800577097185932681890393985245056322053951869376834889414094022330167956562950238795/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^13 + 7624133989681537137004749901973592622217774464365258725082574426166042335928929877980818694357942891201053002224876864194991089272566437008880079801589737190694439501576145058305/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^12 + 1128511866642308837027826761300388995651348853029253827804032155122548262234627621613030334358157192645467065026589784380390067130900842384569198314961520715334890539470993034449/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^11 - 2588089199043037876517016087613405536933090988311212070305541381072097717935512253945900850709558399817160438995914138917895999117410763934927644884060499959244095754401446606701/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^10 - 128684622251418897275183413326491085332199044511529497841274639356143070016487508768906292267987044736666691560161851921186033584687501669729222268771508632409631336282539053011/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^9 + 166082025279328025750711575340887017921152869768688037035944133771583250768721359180970165006496776108145457173841004611542472887479583285574461690714635488612056702424574494665/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^8 + 34011039564985247241251555625540261384109495862366230892469918541787525165152861645741699494695065376946559201337079162703479348057462972257721327832923174238355695084619793577/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^7 - 32392056766199315666056008307163255217449044000163838791854808195808128534029936488011668600596238844426350794485779597460583324491182229840231867062214801365891388624052252183/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^6 - 3825765403363049757706351436858441446252213406899028417183857959863302518357740090889554870437703910323638275555674290472882082046987901628086949747133423680279148750832793471/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^5 + 17387656984562584166585837446480970019195292292677363196178440558882842923644660890608721718079680826699185609641160900149086618767016602934350421451591554791790187353164301/459739338449725698910698595514707735336067994146147787130709579744499795509369602336370597714939573102045379798552630040195719346313167271534569135847400170893697331224*y^4 + 296266661259266347542234944924265379539472918661765818696965135377626900863617929310116106896438404793302382652893596702317529687182003146860706878969560868445583074946921395/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656*y^3 - 29963026803157614662455676581099910230542142998299524992124055962873024094774129342866071824292367654685279790748060384365501035674664440102012532900599892178217610654080157/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y^2 - 4084789683087827046875538973249399680204423536908688353350605208109761497591459923784207091541611523227845183136879518776966241377562874056413853756516846295158380030968683/27354490637758679085186566433125110252496045651695793334277219994797737832807491339014050564038904599571700098013881487391645301105633452656306863582920310168174991207828*y + 456000330656029689376452270867816379383187188395549349769655161850763444041695373189783898770907708522548692670720085200548765787933667964281318686326155309281763836067113/54708981275517358170373132866250220504992091303391586668554439989595475665614982678028101128077809199143400196027762974783290602211266905312613727165840620336349982415656


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

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

# nu Gluing Vector
{3, 2, 4, 2, 1, 1, 2, 0}

# f Combinatorial flattening
{-137, 0, 20, 1, -38, 21, 20, -8}

# f' Combinatorial flattening
{40, -78, 0, 0, 0, 0, 0, -2}

# 1 Loop Invariant
1822309765882422807727844230696579838892508019180547561258725565075285875934668327601643014965523331964666975836546794234045037989201062525433419630700068236113425063901025021338742851/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^44 + 40815219291231474343718778453952848346615485004886454799310992146619492343403806952839310208712564628847598532286751242937761534039542081969846125395725916662285719824574153135124259447/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^43 + 32323142830811181598651621480732139469801695520858169888628961400503032886735401186375923082000077510823702509662434406787778027444316405199987275414049250259082980691670507241396971179/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^42 - 103282415763469268052072013601539942372430090894670997011137739082808023080436150588759846312501780856994849295124431970773543472642951646985834626410435448461496457399826612768411475491/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^41 - 2578594996164098560549797415206215617623179251626934058435910214968808817441507869988248249921460286792464814962205240523477028655647111245902018878468014522231084886189386780122769467201/253321234650395146915324598726687758664721602325892113059053873783309797834228559561076122154131672383259023082970310866229538219072754755215732262247363512883243171725506514298972*y^40 - 11018459469372701567007285998061303828911303972424214796506875487097388020825512327344390915688417993210693245401624304643335256112384076571641421458037190477882833964283475231815640698031/253321234650395146915324598726687758664721602325892113059053873783309797834228559561076122154131672383259023082970310866229538219072754755215732262247363512883243171725506514298972*y^39 + 59772863810579992978431136581436158229524833885006573702022178538786122347509722148872728881187642675889794940427169801206513543063059468486500339456343095149876788074793553928668337768273/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^38 + 948115070934670252335904993293506799011137359724078792538545490473335874604801884917522979106584301942815555738897923620946557496729065146030449384469935204089555959147708708334725082319663/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^37 - 338603589081031336396244245219148269892514656195250072953100200116554976955624463535532412958025530940631327817249475696346865717270093713131131400971463535946050125041881465218366859894667/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^36 - 582199921961441605562113001132846442447187002343532478076790848363563394232141054714544400544413659539916448794034238169382685472138686494817620640702906171054005120654455090317404913466656/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^35 + 1174535223538510316283016464213505388415094099246436834438940900181356362122641245576633052512066674921119463353757618411271190428391565760143293134639095289158663828830064503834649560056671/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^34 + 27344433415334653196359452726449594074352372566469129860147846677228599238908397877009757790081144575962028032052116206954059633492298700594632009118512172532209631023076010451945276040698129/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^33 - 10337533645537982619633935131989002697172698248552176037004043924439706288225936116210275601910186753185952592921643805592443201032933758234639412673696904299065053161728496852788172578849453/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^32 - 220862515980486722554588417834100408740870823175780413768816988778774705676683535534666513103241405057008681436576107197236580460983793813138431723203627478714518431760668383291543616959734805/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^31 + 70088550937756096693614784743162301955320255881889086139238846729040205554832215989993689148867638300843847855583591271360837583973797130112143067642633339354301008177169040022382728778841149/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^30 + 350358659068997335634579032966025557642371483925109185555050886971915706259541262165119631525145198776630716557914507327267286380871245663219105945944448716442250732302868232205870572429092539/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^29 - 312971689872880520241649867714001410480981945728197335194089319522370527649500700402781939133193862591303511879772333785797120713055211323231848048809400393615741517393372310642085793725891519/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^28 - 474402895457843784525038940872273527794207463088438996446975853590570554904853159126373362927410174576265012887858277461563759197239742617977157052675617993076928263287254489315895086724876485/253321234650395146915324598726687758664721602325892113059053873783309797834228559561076122154131672383259023082970310866229538219072754755215732262247363512883243171725506514298972*y^27 + 677646872637187377192332286898548279241696623875801587099828550991005430095203725508691075500660747712023942340992519471710574455878748429009308936603322280194196749928832051245066029400653127/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^26 + 1042670683935320047790642383383198340492341942571714139544854561480149740845422717064545794529838838081568040553270783683583321787058924844125899587892946933174861280104760960878794447231687677/253321234650395146915324598726687758664721602325892113059053873783309797834228559561076122154131672383259023082970310866229538219072754755215732262247363512883243171725506514298972*y^25 - 304265117222198435103428590035724335156583247556857348088643946957376500261929602025527707462973914911950103394181963898507220983957710022356464402026763134747130726399156221248827966693424673/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^24 - 820836553537972932444515837492923927477102367443578037600777802733042986772772187245992771790523504643230628391152074536961653867839589872283514444212556916448346876176883205595618475538920491/126660617325197573457662299363343879332360801162946056529526936891654898917114279780538061077065836191629511541485155433114769109536377377607866131123681756441621585862753257149486*y^23 - 786367117937647506667097102986968781903985538459504027754778625744064220498361791994203661996005946478751543993997710304084814396368373560647734764714507457600356439850062867166611399852700823/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^22 + 416118887700593477789789147280234961363818670183169327716348632594550853207984138528257867672144511981338545156255103600461674553588762158703286409996868822348134692370260482046188066135747481/63330308662598786728831149681671939666180400581473028264763468445827449458557139890269030538532918095814755770742577716557384554768188688803933065561840878220810792931376628574743*y^21 + 856250813614144357242801437942899846523539633632324586925897039358991781378276804630499580563038749729963531834850366656540788021367904352230942156813359218429070122730294212634791831773928937/253321234650395146915324598726687758664721602325892113059053873783309797834228559561076122154131672383259023082970310866229538219072754755215732262247363512883243171725506514298972*y^20 - 4023303752633683085037349259065626467814563870546283667347773882642934470606394910838620683540948430685174377390937319112508145050132735195576619156697580316285806977153887013508869283327770217/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^19 - 3189717792478865537236507661001876870128058956721099160231977898264355755596105032664413666355439543150575763886596196450229714386877315285540939387916134161334042031085834925097024888440768091/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^18 + 339247583302507919687800562058065323561595806535411802858926799391933161489807448263777556241497445571217729775047049770356822581959944125237153163177010566484126620122548576793211853972551245/253321234650395146915324598726687758664721602325892113059053873783309797834228559561076122154131672383259023082970310866229538219072754755215732262247363512883243171725506514298972*y^17 + 1691414669005529393320684689844023381932627655545294508286291609061574181950629347459340644312130003374943312562311853347879527687376851817923040473632717228859415347297254994056384700041285313/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^16 - 99876896894887557263819009475786004922205058125500036745692401840070355608897059893454339659755097288132460161122607228808492412320888722703598845017466950036478956678441598151704892128636495/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^15 - 573929610889299813169526554456567578379400718730071956081044532502676088382639418516852547292441543704381515431261937350920727205077803731354884600092369917200999384389045590664379160170418255/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^14 - 10481841568346671926068546793577220305226089286786693297119203510278239174603514278925331841048826619307996374708468547420444145244991264781151597213348497533733006140306097385027435894476373/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^13 + 66966562395791275746734961833381981934528838257735093198889942984581179319061388799787101512196989658749794555453658085394409274639410014244127935223926595103512953765961895804083901611906965/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^12 + 15312020965527300366368893222268483812101964220178192646708140877817595720430416224190251571343474827877939545647656807472280549364355186214434688996473299082295950233664830217967011722700509/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^11 - 22696726930422839779583758760310853619105329029661681890858457167894679260335615803282306605883410529171502030449400144179148544227809026709252188909420704725671316430265032251514268745095249/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^10 - 1594542795640971429215198665427759053906326728300739766006979532647640644970038879193599860147580220026211217847701435934673859342464736021741448280080718652975398172946381682490394506609355/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^9 + 1467295216913104399012396421377562620606424936608697953783413809307250679203749289177179124338744045158262955827708095008491416752432833111578997486683721532331563298865397334241175134407045/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^8 + 414814323376679119980297963824467164581958601354864584066501642265517878181847879675093652604327621978237605606454405250972311767351059543819604792743770752006620270524916903641205376339821/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^7 - 289986349776046768089661076701616111374677796048335906218184486590661035048527731714006318254737145913458003234994114047414783482253081237389303107043629815822300692140826369390565174935835/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^6 - 44029760925694412587420140829347233006333427200865347061976340500499343853048601370934313289841847518479499828019148167372570219784486393637156624142238005959840580073156336708349194734715/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^5 + 18765323784710452428324873950133617589861527684527837574527326503278132833400359317993051476053079840373150504039460580370984456463629738263115989136555432579633558943804498515287895391079/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^4 + 3239253803177706377155537307537027870681795746708766971645738953604824927982372685155626952380373195206420508875475098079757729757281845447053707603082896781867846396305491947230311439455/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888*y^3 - 279455541185672285044098916023550829554253260741337542028405784809116984292406872382372606422885520047838001008100200353878097138982912185666819952413022277244905385147503370655060777761/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y^2 - 45012196255696730255649700409579632963353587981398405939679637581268439625684076610420258647627360130763036559331528340952391381711975870229046413643059494171293580182236238124548366043/506642469300790293830649197453375517329443204651784226118107747566619595668457119122152244308263344766518046165940621732459076438145509510431464524494727025766486343451013028597944*y + 4848996637255496505750411915500955949276039561158059462382759951965542919232443785897085541701691739854193709564647801139558950152375999271515157586073320610469364485646434088372046957/1013284938601580587661298394906751034658886409303568452236215495133239191336914238244304488616526689533036092331881243464918152876291019020862929048989454051532972686902026057195888

# 2 Loop Invariant
40256174535943022443373753263968051418780550997557552272120301759563357070723698002715279018787221723383027323850977316031134927220475049856572589946396206056434245122660666834642008254639884002650915585460286752391134799439591341609478245861426194655580419232918520666202281562820626008541510175797304774321366906271106660428312305937044110214477125650906054246078935/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^44 + 905527040813758964117659196387219707497192037370501159243647611015143584079875063705804675255358342977052205672452261350600780206960502773655647962151456755607012961429919457603381126536816654950158193805600861441962223812391207968294379371896585965943732782130111060486031951195131927641183764764572480567653309562593132940695496742602706738904041928681664119394674349/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^43 + 2898720022745750499601451593129212059188830477630328534710107668186964005321566160737407441351549124580901231253660760557494813673173750698178506857010325223478397795178476265974385510802274012971972426266893506740243201916958933524986070776866872649381573279979439502490643480495411881487205640161900913892837722772394991382630317044361338403954888738225732355972256503/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^42 - 1773925820668192900427812732410157477282972579143041891491693637540918088762536763767551227417706406185682152703464355125923965160168725580636051900505517114790731154269594456090497067978539575244143461919600937918695820034965982359947212146533883819271986555926785159213205622662254657864484963107334084139899379050752154856288616392551021203278599081918651453058689517/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^41 - 7135771645469069876671956947158027115243218217710923799830565214757254351329629385676160219155433141539756852065670283334185594149659050969721760493963805348268444508999836596758639959952220193830618547566864781133152654159903477450248551726278383504186692004990091673742306871877145516015422488446973028384929418895233302506816741937153979033476680811305576997865124141/5059170744635186803212774382175239386899323069130672290106529521501458426143197527393155959898411088920924857474520716490790184367559588327106798410341292420092958685266208536804970818571929877901528503813918297712265924551125622687231644757467667600751741380136821850155467751655058255919098030928920807399150264642853701727861698381065489494270540083029159054254789*y^40 - 165909440867459009479464070492939775711696645246059100133873808484311938931586560158525822590670165654881086619011865488558355177770121576358614602226507402068183527951555604202370857565968371718577622844445516955197175924721993657112640652551752959260210154668257260693953905436104622823531358891722891099260759332468077213482010615187067562471713871746759157428811664869/26982243971387662950468130038267943396796389702030252213901490781341111606097053479430165119458192474244932573197443821284214316626984471077902924855153559573829112988086445529626511032383626015474818687007564254465418264272669987665235438706494227204009287360729716534162494675493644031568522831620910972795468078095219742548595724699015943969442880442822181622692208*y^39 + 639505083069627951632028458134385804833405721178543613023110811137493635066996687857662666434256963037799614764517772860234415316068468357381043166315694543706244830756240506873510222099115128845556744644403527796990257414452218244672520724370761006245133400284408832062270466961774078942240740814234806697822769937072059367493706083766531646763147174822201453026900494027/40473365957081494425702195057401915095194584553045378320852236172011667409145580219145247679187288711367398859796165731926321474940476706616854387282730339360743669482129668294439766548575439023212228030511346381698127396409004981497853158059741340806013931041094574801243742013240466047352784247431366459193202117142829613822893587048523915954164320664233272434038312*y^38 + 7081700869429210148034882379160804743208482946484124657689600822696163910882989370869184696259578880698360649290183521895451071336310383313856549670185083642815991792260563252437702160826018935314414949676097266905183666682386604913281745927448046713694102240593289281983893328008072070972095403315455830805222313011056361820403727069598505177863299547494016525368167094027/53964487942775325900936260076535886793592779404060504427802981562682223212194106958860330238916384948489865146394887642568428633253968942155805849710307119147658225976172891059253022064767252030949637374015128508930836528545339975330470877412988454408018574721459433068324989350987288063137045663241821945590936156190439485097191449398031887938885760885644363245384416*y^37 - 6538981371241732540176058272449269924430427139183368420968570977817624663495251907840851437350099763946680555978478036630668668954920268502620958226500820327240977365169053653088508417334291247956631664691560041738334200813076476384999413843996971618296461014395504460318918548749351802329497510459069087388644832002646709684340859269138516807886647160367963333730255968527/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^36 - 52055935592923764913120729900805390738559309621645595301216012586429210729933409290345063781361958387796031015167746570101387928099412920740076631239391541642802804613054760440863971652289208343541228913268826739776124907351517039396114843271246084806259732687194968774797396737450567953861227067200693793442569809123218789240218309625406705837379343513143344882164211598517/40473365957081494425702195057401915095194584553045378320852236172011667409145580219145247679187288711367398859796165731926321474940476706616854387282730339360743669482129668294439766548575439023212228030511346381698127396409004981497853158059741340806013931041094574801243742013240466047352784247431366459193202117142829613822893587048523915954164320664233272434038312*y^35 + 2062014921942055021976528072633740286920611013482068321880135269909522526587504156027823777010151793382072153669414320834137319564468236687309860531422909399401757417509881509795650480773995180309107771921139671870370739507174059969155769928536739757072548842638045727688981116890586271756599044112806411964910466288957301416247722497480246143867906852651385231423265605355/10118341489270373606425548764350478773798646138261344580213059043002916852286395054786311919796822177841849714949041432981580368735119176654213596820682584840185917370532417073609941637143859755803057007627836595424531849102251245374463289514935335201503482760273643700310935503310116511838196061857841614798300529285707403455723396762130978988541080166058318108509578*y^34 + 305753288814020434635411110745817557565930267635146519507988556193938297399092964435761271264679411615859739122492917210460066905990873166665311599805017159185075001209745530133344348292274538476527827686901824196678903357834451738532758488154972966048915514556677620641280874637134868319230398626117658392269578156638600615736578945370568393170860435351747730736368700230841/40473365957081494425702195057401915095194584553045378320852236172011667409145580219145247679187288711367398859796165731926321474940476706616854387282730339360743669482129668294439766548575439023212228030511346381698127396409004981497853158059741340806013931041094574801243742013240466047352784247431366459193202117142829613822893587048523915954164320664233272434038312*y^33 - 38870380723930420653505030612976927620347918920444977454161221470592986543971797164926812244245015465990139910638103247934931646430686721481913054999093413145041929239706853340112003687843986234670078292757032359687411056742885879677570298325470917356693515603699046902236134075783747440105888993259228922008708605986190183777069302060234884504989729292792461960936840116431/53964487942775325900936260076535886793592779404060504427802981562682223212194106958860330238916384948489865146394887642568428633253968942155805849710307119147658225976172891059253022064767252030949637374015128508930836528545339975330470877412988454408018574721459433068324989350987288063137045663241821945590936156190439485097191449398031887938885760885644363245384416*y^32 - 4959059980024528531733358998273369387423188822279079059513283169945630806624647317907811379522376483015931707466118875773609108143015590055932206947318418930960881728711159733717665861106085730822011146256307548884291733294712743812454872443166586751891801348102391472781100418099301677299113641179893354480578453444682470431712580313394825251042133530520655403094104310802525/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^31 + 1102406252913444323847938216253230598993456372662705410241091295862443649800729584582452854939379871809656698907041536792709383271011848281647869017895090505489901817665795899410829905792613158721122785046992624876146548086293099651736077132067517602380448549165981879764256978350742846748029845204730158237921649186483815522595187872710908926428043423098950093660585485592937/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^30 + 7930375997495468976381797902667079404645055731508162717500547046546716123878323381206619943789318756297970620509537368987607080315716261785262673923265683815989040428596105452108947199144114168244416115742583335327918246370002339712044888695324329247116156267470856294708327072166577312664431163981858483395142383954198737875291380263195409015320415510843875375007704845508623/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^29 - 5551561249828242044059533489676007748270933081945963303877632489378031642545205462494370960239826116304517435669685232210072464056730063288311258343364746455261600260008727702285077714220737907997708605317199432010185887600365857484279963888597921160740347525488623972642922733158498888395237528972752841602777884266493520078195920202855244456210075906920375649782666244052785/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^28 - 10826851639062158723718209249967641773797161326771796702402369625545647237017339975815781885439167112797462667772304647253870437338723714941840028437961390448812984527747432921611642516987559904357027825878675264282963245700779946463088463847147526121570126779455993078999247978053167234888726653700523388186037953467362789945527663501076624978828036648478305291824429123896127/40473365957081494425702195057401915095194584553045378320852236172011667409145580219145247679187288711367398859796165731926321474940476706616854387282730339360743669482129668294439766548575439023212228030511346381698127396409004981497853158059741340806013931041094574801243742013240466047352784247431366459193202117142829613822893587048523915954164320664233272434038312*y^27 + 11435752950666974756495477902217375268113162816113146813809750365927656118969100576269426352234133487424836654000888316601313381773040702682353779537132540058256521137044368261654483722206882118899322234295650267801238071857743546328708859376367583307104499110253480315048641670473284670613173253876721163676656723274836096777799820196040184608219926604093595134512319711331233/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^26 + 47742538155022560298888833880484588957458260955411040644179745869909509524581411104320516115034485455626640872107687187059976282459559267721235982161092179626553817673511499532417348873505557857242661351796912424381924036026330306548011140766759587812828153372755873719203126398562331998806423662261392885462504058063508266967417417772932782304570202366134654973379947271725767/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^25 + 985944636788619608254996385762045783185088467699454514749769319241167968523379088818639606147764744507739962901723766008855884004138986900055868701367909102842198509786411723273575573497269518099248804845080035263067751920306084401468204896586122514612638354034637055579614037264785041168614041094552607032642257108545468868776854405635858224787003711113860554626103392896863/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^24 - 24977345335295164591269538570600511294219081854839878991979889847968182522471440471546873199454902706611938990854672139746323337363634360505728225782267485051523556684456557673618362768629592267116921097362396301295885588408528086869040226295687754368012983169967326739224670944749901578014822887265516544796886043663844710392508776252678881199872973500284995130239374274341929/26982243971387662950468130038267943396796389702030252213901490781341111606097053479430165119458192474244932573197443821284214316626984471077902924855153559573829112988086445529626511032383626015474818687007564254465418264272669987665235438706494227204009287360729716534162494675493644031568522831620910972795468078095219742548595724699015943969442880442822181622692208*y^23 - 11858574381444822730049498238851688965687949965763222584321763452599375034664133383856176281714154074805272804378480044653796678137262890516041856494078579462632132317415035734667907220353291026039752761097651998300959059939919624268041379059971420695758109678903304308135324773527090091357544781562815866185920736218132579088737940510208329911824745165985739197490919232405391/40473365957081494425702195057401915095194584553045378320852236172011667409145580219145247679187288711367398859796165731926321474940476706616854387282730339360743669482129668294439766548575439023212228030511346381698127396409004981497853158059741340806013931041094574801243742013240466047352784247431366459193202117142829613822893587048523915954164320664233272434038312*y^22 + 75163056366500250152382904865322330816328693230189708895476748842175173904705908914886585994387286824021326411364671894862551062243676637868464084069927081812543274361403313035031630854895817614567442956512953086078695243774045627501773781626966271468282621119256122315780700336121858264667698772743841022523245969147527167138737220230668015467448300628185428079109896054436019/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^21 + 14992679120878461949683048763271829643816467388378828794178822295080406509585946472162798582479251251417215357230168647526439520930212888922398230907117836899072242083286045670128256285108886992842029677988518336805438520705733773901966803348606630918362903630496594276384564715044335453967494457387398175723391130964091136843312896516585236573860292036337242982471003684315591/26982243971387662950468130038267943396796389702030252213901490781341111606097053479430165119458192474244932573197443821284214316626984471077902924855153559573829112988086445529626511032383626015474818687007564254465418264272669987665235438706494227204009287360729716534162494675493644031568522831620910972795468078095219742548595724699015943969442880442822181622692208*y^20 - 88491013172159527401523944729387404577857546434003090751478818237766241785290370486656628091796736631928905879774057002376465826966678778709533182475780484636377222969211944869370753811068326449413007681306632062009235522111685969954022212347188367542667844280339974292826096910410759711341194062641769866614472203881605265289377025632208581209320794759706402008004324501253047/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^19 - 26984781249139742289363904080430984031065954230006413817727561644974491917638010664535984688968625220698202059119280633080627577930921212206729008193344348629033410266634691376257039186609214121680431510635084955615943829631259286418671945749744125793292340196702226160249882099537230377770314100654910125380648844458523686176053040065363850167533218042962431309046552310089275/53964487942775325900936260076535886793592779404060504427802981562682223212194106958860330238916384948489865146394887642568428633253968942155805849710307119147658225976172891059253022064767252030949637374015128508930836528545339975330470877412988454408018574721459433068324989350987288063137045663241821945590936156190439485097191449398031887938885760885644363245384416*y^18 + 13843359931586173307372624135043205581270416157846120883608544651190137528891128238672275391015739768673817141592402294962010558960995688926802632055170200244348059668329721573849746786065617219451724137578323343522129739232796499284272709752434486614542417524949685749676800662068045903827791931616928964874513056284466427729698835858392777096796517969011935975561544523017723/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^17 + 42403137623659981874322778657060966286166836283821184470599455305817272271854908376292886750726850290204141828665050767909100163218003578018244479949946340412384232616689441292200340867620966577550690362618032827180389054798078741402232347465769740701175101074060927077202636714033959014940541321016170392678699143153242034016109285549263756996502738898867983385980720859639251/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^16 - 27475363541632422630395912489812472288322143412050421681362270926125806400241529283872065210052695318439233401519693080637208795318015261425692256789918736609315080405115161432526194559531645097411900061678500281291617456960598055188547798689486003930284557058878480537189139844525147170033475150899074189986903010843934004112806021111316073562070676207485348007391337843731/1686390248211728934404258127391746462299774356376890763368843173833819475381065842464385319966137029640308285824840238830263394789186529442368932803447097473364319561755402845601656939523976625967176167937972765904088641517041874229077214919155889200250580460045607283385155917218352751973032676976306935799716754880951233909287232793688496498090180027676386351418263*y^15 - 14317550690756632644686420812509429774138970400360506929560756300978000157901245463826676970076024914499574027678276986662052187263202950764972217552813902784184777602119389395284351344481610990510333332176209052644531156313179967678639349619931909869359116764961575395994624923824880902237007346225877537749646702780311528384419683617877693294039131594547521323930870808080387/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^14 - 50433127120536309744058261574739931597894245650474634504764417507491825107879243434748510804067378607382182572214800345368620292064524661405555959106375337094772201865327091324768956177332194479022242297535689409046253668850912102558241284777941178806828741324260931176885033609375691958445486228019921096081576819927044674586207992488367516617629780671779343656026656474015/6745560992846915737617032509566985849199097425507563053475372695335277901524263369857541279864548118561233143299360955321053579156746117769475731213788389893457278247021611382406627758095906503868704671751891063616354566068167496916308859676623556801002321840182429133540623668873411007892130707905227743198867019523804935637148931174753985992360720110705545405673052*y^13 + 835247733858178199236826961026217690126802739851436449924976625929349838509532252157697067056267717151382977228701467759867645289336139029292013734411278985839124483843140319204849556361135166155124415902728447727263947561793143951968688184594204126912396542613076269204103904368327072133893158870995008572331706466005788720371514362522156949649160274483921389218348555929219/40473365957081494425702195057401915095194584553045378320852236172011667409145580219145247679187288711367398859796165731926321474940476706616854387282730339360743669482129668294439766548575439023212228030511346381698127396409004981497853158059741340806013931041094574801243742013240466047352784247431366459193202117142829613822893587048523915954164320664233272434038312*y^12 + 540101815896228398991463414937782377705588984588707325870656879592447085631229077071827033156426206675950504415301386697836663703062863575608081653082325787497485671824583709554073045076492446337257872558748983595578154755408962799236498054970729364301689330270164859747592779166540802871212931823643645158215290281365526647929852221375594708185184407664001237223156108311679/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^11 - 570795306317703906865600834940797878247170379752144720781460004571136407358529962269605539879010726144428337932989151128375717833847115165688270775507989695426011618299286374598348495292664676957450174033160965806079211049922998813998034843813039228706346222257844195412698150854721964702044616761173643965061995745248963060048964746038758932770968006402230084235034542857235/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^10 - 53563625776934971959138806175426963740880752861513001213701731177692698638707724330199327366802680307081552012474375274274961272318355542434737427515601033699985053768185331321080767340293327491793398485053664071909978272567987374674884431075574765814780358872610570001760028664998898495559991848088081490884736661527795167228229956916779332190848218509950786994074004170867/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^9 + 12543172971082646132061454439103641027889839156863565633526484887365414702259082263223320870790327099174947627532465039132577570644968285261675731651324684486427735701551870074314840200916678560540088790651285765403668297127042936957687347192560478418800468384640348616594703980622600837914254647071257461302447699145666063610861461053021809245121551504814226055761526631597/26982243971387662950468130038267943396796389702030252213901490781341111606097053479430165119458192474244932573197443821284214316626984471077902924855153559573829112988086445529626511032383626015474818687007564254465418264272669987665235438706494227204009287360729716534162494675493644031568522831620910972795468078095219742548595724699015943969442880442822181622692208*y^8 + 4582709040277739684341960120561736808436227579736006705527545680081280183538544162408588124431360206996106782143940633062606606559493586276095352475958837064922089095594802460765525430736847052032711400572020358662435941248048267526193057827909898379745142110719460814357228884655585201139284840540275336666599761571299643344620240485125042811598063503539642315109674514705/53964487942775325900936260076535886793592779404060504427802981562682223212194106958860330238916384948489865146394887642568428633253968942155805849710307119147658225976172891059253022064767252030949637374015128508930836528545339975330470877412988454408018574721459433068324989350987288063137045663241821945590936156190439485097191449398031887938885760885644363245384416*y^7 - 7628685386700794278943327500834746519124805111844894975944294473724733365128830589365498003189314357525746606358020103227009586789947955679335872209161386397714066781720620344067847514502147159201955058409198872753570562812145596731690364098901389730308286582449700871711827363973096557685590178023136495997215620215558050183427437565204133449886802530916610466967692999369/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^6 - 1389043344693463903161253413962812296372345163815750437861216706518064472178462183197863723391047535588591850127564355862627972509804287447649482238432715050481366834395111435673450439387920705060647712679811228370995481318995804116436391377166757968784116097152242591056415278485755447882018794494376938055571668135558981321021720181048927995773566376778346312680539810347/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^5 + 169706386036317481036730338614842340301538611534702582784557642280719025398607403658172752021236369150632183327708136399797661712581340020271331179054960850001815895131737027427173943391588594248893250675649930135041457617257465757896103342454059550087947958444618567760946349279764252280724239069585096029430200216742593243226685566389086134013947339037792992366499681199/53964487942775325900936260076535886793592779404060504427802981562682223212194106958860330238916384948489865146394887642568428633253968942155805849710307119147658225976172891059253022064767252030949637374015128508930836528545339975330470877412988454408018574721459433068324989350987288063137045663241821945590936156190439485097191449398031887938885760885644363245384416*y^4 + 98335181303611054834723414757431542088721824039825113833184226599738351319662850961039555522614252423408027094175486913972834720771217830565639639779531334300586029453226416981891541452406974377625196945491447311064856939602334972864019358011578162629540942123736312365206071832844661401759381931911833232348837939366902851295336932910886713306043403012312515578504637785/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248*y^3 - 8168994783209273019953556365116889848054740484329334041415678133037204265246866281491273344106515272436288149731603596348341217195193911330628460353580352800475199674752735893682330404420959277794521658470119002835855784571742642181953094657162556168263856589404530425612172000538066125218805499779007483007293235966563949347388349919876495399006408067971452614695742327/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y^2 - 1393208011403286835732990163705922882225814610425972292759353122554279548963496178378351548252997269560319666798786445787054881133637109132872775224176780640568789267539050192049675526002753069663560152638820409401783641080583694002930018635757968083440024909846469621553812382722323530841930189419689369315522900448953541106487735580006193967897210239572495785937991797/80946731914162988851404390114803830190389169106090756641704472344023334818291160438290495358374577422734797719592331463852642949880953413233708774565460678721487338964259336588879533097150878046424456061022692763396254792818009962995706316119482681612027862082189149602487484026480932094705568494862732918386404234285659227645787174097047831908328641328466544868076624*y + 108748527840759330971314179478374022536426753682690893906797748205989333484698901333549827709678409184246772165437364386359612432464030733067884839360180000976813801187273011279229650354657701260576300280230914014608839912847035236553407504116958574724524654137833941742278259690300621938419309873244570958448113268973322643963636891807579001932954079783100371434834907605/161893463828325977702808780229607660380778338212181513283408944688046669636582320876580990716749154845469595439184662927705285899761906826467417549130921357442974677928518673177759066194301756092848912122045385526792509585636019925991412632238965363224055724164378299204974968052961864189411136989725465836772808468571318455291574348194095663816657282656933089736153248

# 3 Loop Invariant
9905984542397252194370295039783393216849712303983383848181092744652815300837146344095181703506850459711998541475155466907709348865635969994888927118116883413667851255742954880169647934200437700787451182179887707734455125604029649307186917522456885716756932264616054294487766253209013268489935572232312403930499990742338903897834147100002721469321128008482055055902879597823334894761797228667697372365973965516379559617673286300541818899223105914344685713405453/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^44 + 218732008669314266830252819013846047763879056871198440574806100659691374641907578555338638323234656470975841192071942117385543825264403856154619818745841170216827088839411912237613651498233342090964777178084566489241141884525694935106803766570538485371562591278714688725433424582004336684276803221655387260365906297542266878432420541357891488660086948908780355113424046562825741908170786967749643726949116703596134663838176376718892596901525707389613011696845555/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^43 + 1336628328621556575074111725268606249384461604326438583347383374885719185047338235359455727991470879816544531963765916357979919986572850461486613883929458157656951207495288360056168463580453041651208219868595109470006357226352932957496918425165897824389908861011555978519361535437188036384928564367102130058850886422736699668154462165669404779670348168442774569147643106906573356959307415161374468355171609146574837390293779714423308357996087691240094747177438141/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^42 - 489577642775660937248151675205464449784029580882678610024064617606655738333594613114312792071934769605269414163428499979327405615480336901569875662190813504437706562245166983402999035973106119911208306970733836517112662589429743757612438885179829741381626284340052898305293446532160178911942329312760762198196801341451198456292965283539790260571000523738189078732409195809286362728177510802012374308063203116918573653321960399271853660098764882386725562808994011/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^41 - 27861192458025745667991453869573706713185541355007802690702778982923055961340111055653909340502857795041274126652107026084678821854501582198262380083890106260224290175354853218504534762913240159832731676096870977286280144905597958526713145265296784190325973290457753660677209765114478834351760015699473388093799524480001766709335808169171205465654947176519047898468773783186522769443708050627701757246799680744613367119084365731084656673636772581544147468601001003/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^40 - 55486470361022303501609573841977320808955582857230574813579315588185386366368792729786630122121901624204941308539552339941725850264894492390720394190740216931838490116302328341831241780246677845691241266841878723347723952376494993505428614575165601689075019860544258242074062206800384074863410845768526846468495494802853264470879458695502499133256544302524775316038077562284628343772016826960899946657972832283516669533719230969590903137905889132261450707438928371/139235924741973020086150671804859425009644551661579967032014648199995358825381241322672156887628976612321668839463242094834711841953884131074826248422892165402592722951615562634940960084306668294085468664675572220355773585414841045632730117538108383198500718330246721182406322325566019100760159787521398961256046918915879732882623342859687080889461363210789063809607055289437746103493071634658422384356377975875580028099410182053873913614336878928777712700865168*y^39 + 359361961896862103991393447721393156876848253238089047358027663908425670557964058059630316684527275491222776475882462523692404533124564721062967340734868437729167592337213570235395960567095042037886836796165764123873696163423743509974144151506082409636300049131260176616790220094920963478391134548814295542841722760696492848548631605945594074726145642652223539293969790197536211287489875397105984482351696951997186460294012494348775836852100720651068534020662760975/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^38 + 4920111155802901453317714514393085090820075325782064162392802695846738046527450628282003809510604291782368181433645530135217009669321699720758907258442092686354480725321788036338375935097013814543532878211408932971539047243888666246332667226248481600109878293796815578730712332265089482369771247642041915193693352828265574745396326442847402545505520759165534057226650350369413443237467117977362013054882107954744003624935027804037064284751360646794964574033245189157/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^37 - 5223658590372300472714534199717425616264641527938118658943227629947291296767504599828464623559987002407955886926171029283768891476294670185304094619342724719955361101186825987404262619982435853120167481120687870437750625926582092453764282664105197192943092299829510170832467100794112457799419662701482887701749219036171726709693896661755921993617474902359546404749828353315943830583959027645012862595231539853741785803875589331710193892267107629514464845118453105629/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^36 - 48851378682192029583510437087962943444984782736779351947998394750482282248307444762780888512307536543206995015738295875266414750003509456610529969923087671157038558428977565858617488131432722866119264618886849751807116164252216404166349119603182555124556079561599518356220789795237339584071166390096974932387504374555679962826003561134806349026479218319066559466637302816107748255174204742674784726446679406606957375071916704912104050369384231016798907464822039304379/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^35 + 28158746219006750895851017898458243283168585295404504019154180964379548393872090863996709971874882989357219825268016067130426304361180258104723182105053528361694415200627185537495841068462455460077841888151874261365496833171954387883487648357287012058795033438635312179610717473806371962589997965399752889571550343644813680595670033663968003416651076847339548819904898259818183030745878557558864795575970243440924238676338391342407796714130107399276853796384344272151/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^34 + 143543894875680238632863877808429954538766040478928768142871427316860128842873384671209958162290987699889640372452558876710487867332888911699842369323272910350794315877766361380269199651306874107525856190006156237812182482880900017577627766323940015061568802001797876043001979090148127994597533492814891828233086102186843139987776954152820889762293884961582472467022981169604960001666154716872007330187880007210827420836139779902098998201563416863840748175987190146413/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^33 - 73446195476122171571885317583921501836799477041051470119026161232601717158217379173131657854136878883469223534018984453218183166914600763947493995680616105520279035704644139547188023966726530148516766105354706001409611048779828615456587853205745216177193540988656820627694176539652374481635727220682560850311421521470177632653132958720961007280097107895377455756794915458682699763431581362481113296221946372045631419300060328374849720656451165608840256523293222497911/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^32 - 1146603570398284878148335346599500554269348146130147960842514740891960915581599597982671588340627876529170505293229895621533929180970240741699757054993611235547317066896215497984384922548511339257256500066969994202553831050015051505267479201229700541713110988763646467346710928490367754501952553212663222434170181788780755293025563042911877043017805782483331031218063248350088932451057143454288597304589809493015996146770938077894183338228515539819502052308667224129481/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^31 + 46453955233536490522131429787169036784514092819321919933572161183136901942004340818152499705510057163629081110656020567717795181162903478400996681378788556240366116883457675303606468462513445438531208792987316319235428228378024628875464023755297721950132241446778003543663797424262357420325352483141101929559960787626236589302158797248809746565449645950680284791465835844529791807915619577831906245945455958403296346707534301484481512354401405204249809291191207792061/34808981185493255021537667951214856252411137915394991758003662049998839706345310330668039221907244153080417209865810523708677960488471032768706562105723041350648180737903890658735240021076667073521367166168893055088943396353710261408182529384527095799625179582561680295601580581391504775190039946880349740314011729728969933220655835714921770222365340802697265952401763822359436525873267908664605596089094493968895007024852545513468478403584219732194428175216292*y^30 + 442950151031827592069355338045915285399762657718868176640214468138322125222106435198510115149603670447562493676538777740749628075832567392874703639387066822863472823265965292486679856781699994915629602513865233381351517323634487774848680746901782110429546520931215945811907080064607994173041372232516780097944050783440256985779392552553271809419057144195634869191182563844418029729562070740318134653362760347895197379954775172614025601197221952783502328808603185585243/69617962370986510043075335902429712504822275830789983516007324099997679412690620661336078443814488306160834419731621047417355920976942065537413124211446082701296361475807781317470480042153334147042734332337786110177886792707420522816365058769054191599250359165123360591203161162783009550380079893760699480628023459457939866441311671429843540444730681605394531904803527644718873051746535817329211192178188987937790014049705091026936956807168439464388856350432584*y^29 - 704031344565698622019363048606600073607104688927181411343018113518802877497687441173402497003703159663955993822821309861095593668576160396131135617985095836626444368275723462318254113642355590069926632882062300191487391539057475341050074229274190889914179634739800095828271738981482912225434704175061791716293973217798501686668842762281350335667394784393076877966538588491734921565946978074033445780965827051480396649149657741689475253103253059314903576313664760335367/139235924741973020086150671804859425009644551661579967032014648199995358825381241322672156887628976612321668839463242094834711841953884131074826248422892165402592722951615562634940960084306668294085468664675572220355773585414841045632730117538108383198500718330246721182406322325566019100760159787521398961256046918915879732882623342859687080889461363210789063809607055289437746103493071634658422384356377975875580028099410182053873913614336878928777712700865168*y^28 - 4664006870000049707945051813273882922431644301760807115195538918002079798888171395038201353131717231755981534119180758174866235859540841659234322632095158409180626097918108177734869477835289535311098720489038672032798568479919691209584079466136622965796483479437272349856298051608837738200485673823404208284331542218214525567970811465328091285893611960738440987083455230999764601737863936747209489081674568244092416401383770566323770591278651923612010015064228889155203/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^27 + 6601957022575465102659389061254598965372114381815485518283130779431346805776097469291095788131198890021261640252532815845067638654853661245332656284822324714451764018401870555292496596931551050614525174972061494141521774050995680920928561240102377879598947962332221821097858225772731882877109996128483043945905418740824993535514644918580223698218450877184350640565512670972433179848816612514654824494228331568468075933413595359299628462095303913153374669644034559312339/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^26 + 20321938113432215268009366956405530481982160802527557054325981066848063840758019627067245468274930354737075929561906310110364625267466283441167177583882012162339764807843323666797452808638035410180032260288107583238615047527151927245795176154207961060482338733588539134985357026616737999125814330444953882835606282226670506123352470730822856338051234623218934690677326241117493054477028400856876181295597736758365041471768931852736190588223407299941194137875064156826549/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^25 - 8016706111885398575005905703680377768866731290302934392613576260904899483030202861225882665612756943189261943363250484806228978822009270865659407089556111511880393816623433087786562209360214615776334532279125304839081837641700357829469622774038183844700127911680565607020544877185569018980191222036595406755920366515061267238154937522761706188478655246219160886602439979997246305659255475292354666477979936575359925594328919665358295400255193707227671632341872751173905/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^24 - 32591438019513890441425283523644780691267752174542399631059963346244627453877287701986505511682231685541981364058457021500562043226061542538026632404632669421713705840769923415086337277631364576756724935944343868037177846575759842169323607126543613986257241583319519304176721362721330199626139763951962759625063191342207028561076156487212958541489437835524064998331399674386238675548984626303695029034789400253409795793881545716104102475212280377415174324597680979809499/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^23 + 1773300112725785149743664150103357573817777615287409736200071533657570343230898298024157596409586525160728349467578226710514276716606661941204213471576350035682176314563640654230367019135436054593938436943849506981025469404702330200479316924821624851964314874892603938403737273594063633892025520380083484237293813192430908971468732403955177621443255780008927055161092682677040879870747557106513563020205202662826478136532500566660664402330073959081599389778788833449571/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^22 + 34755555186816300726978452362681315716624906293465518756454968898497563474885837064022419103693628827532173692458634418576851167046268378605666151886818239877354802394672957314251510715836276119098160148799692238602665870354665945439092686315131713809990352331071209606329847703989095950582740581573990456350719599958181246275262811602363484510882599401754700522740722102999610804411985566933670716732195974986963496707027167670429748296549270664300097159404975180766733/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^21 + 458473912756836594597101802309213845208803707530980255968046270603103961177307879401653391092721691305356146670183711936297092703685007281356492566470086820957782775338262828916218435479575543074833241207820351170079009402041179726368216104190065909223554738506296094283952141685467069453906383568580209749484419396569238152267654192765291720947422451262868204481079818644025298021171841132415382586509974701851144762092189154809826977291608748615863706682628147866771/34808981185493255021537667951214856252411137915394991758003662049998839706345310330668039221907244153080417209865810523708677960488471032768706562105723041350648180737903890658735240021076667073521367166168893055088943396353710261408182529384527095799625179582561680295601580581391504775190039946880349740314011729728969933220655835714921770222365340802697265952401763822359436525873267908664605596089094493968895007024852545513468478403584219732194428175216292*y^20 - 23340184319243478610755938134154724367645389523869094031558015388644773377186763061831751607244754670431564167227178515148763597406851684952174019601884509588742379636329975515078071556402003780655071406558162332344431580915858712639936627741712115272971741941415606051382888528503615579980959784619612772591100383361786779440240345323010574310443522206180784128896708215619482674609402375997501398223831004588099397818267946736762718996054080820664536880017039908867799/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^19 - 9433595078904379917335546931111372737917882464106193203358429902066159079061248675581706606735693394561101607021974169228683705968373097744723211589415469684533769920407932586746232461373548333280058921560257341306714890235888417206382100873233586092584271747310631351901474720051603817024316867782622611360280418702162946686478430555410327387222048295387605392499285426430551335334445057046080310655373605727823127451240039354962402300465631961864051366601390590763733/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^18 + 9887196264047570514155885197114284007367924928674098298206624800628673642942169970652106674463677632907139457830287979854575146538658760677284355706896717413730479461517392132873650494924945397787929465579014720415895175480510265115452286622443497362935826645671662303240585093956104409092566046986355745227745528474248003944428730735308711380043444571785916436944411280211789996754328678074674968997655023390147363011025320914773074703938173435147412893633377196235669/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^17 + 5619446998049300928487467781034026540520969349594392842017765505988070379657283723226161292949435857315625567911052331810015853968303176076256619300041416278855602408638154702894120105662941469697681783894187922083492494483792977376278414111821854189937091580851566641166327188874770316320498484841096759379950194927691144200107606943427280158758901491962721668406343993884795040900090919492344886891312143690575642810692127749046728246019553905867658201634225609479545/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^16 - 2731195628168961203425644202875379597417134637806358306744543340603708953304425506006132990415106362233456419872366809575386883073387677649287745096003672391238661870806733760166263190490799346851864104844495635728700414487402698775282717180903563267230662343680444976077199604353157910907962011201527925253041872790582853156360398113701708603224949335407081041692829460538704448385801617956182629133997157029882002437488111426678286974416969761843463230605375399894099/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^15 - 508992255823639191957002337825508549508737215211831488029444476509120873611737989988412538972926585723594480737098016792132163711370124830883410052010732366375723150713866621695251244505468881828088890052128494916023910059021633317210135000589636272631555760334070649821813604225162363668614177785790764053737881911840992387290827099079929945270337972694288748856671357087347796667577014620248092175749167300426895812372526522443384727704394074658228813567330569991383/139235924741973020086150671804859425009644551661579967032014648199995358825381241322672156887628976612321668839463242094834711841953884131074826248422892165402592722951615562634940960084306668294085468664675572220355773585414841045632730117538108383198500718330246721182406322325566019100760159787521398961256046918915879732882623342859687080889461363210789063809607055289437746103493071634658422384356377975875580028099410182053873913614336878928777712700865168*y^14 + 523982028627840831211825290690255845867789001124369062911171793827696050907507894935305186663916811484845794240050525281886619394766016073749664626029973554233962382887390476384249082927438154224098783240021202521821840100817892834650179031277296087349057308584764548777014895839921368104478966421250111626122600352690922950619035140474422436345466319168769463426259647390045136428145229809275557124701757583074688658850655752509565648075894147820441919180367984093699/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^13 + 246864297309360781813470802925419638982294013493667718441294889923104318890165000699826226931905838642142798247747198591776847562930815623552199456189242951737342324045414486439956232142347311497192126028526763112631370911790349358276321271881859888593497009502693621876944230891845209288465009278340147451280651529476127506690998313570322802562261017957971469666229667034758935457371395252631990301917196796723056152013769593102622508617049311146311493046877949608893/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^12 - 40381672314420498274906974664456229792329694752756731908464898934253521970416699177142502871555597625245177323358853184144836748299811625123201350079217509548455746157667241703547301169829303503803918188585500154461247604123010723801084429236684362205832605546968642715707031511558704130755528908881383728127375697761021636974597572132424236522701320283031716036306237115277129531495449610283399855954840618981584786389483483378813258329729315018483525012557352470587/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^11 - 83349722794938506480382920574777367080680765139280252178894927234524957709067830080269506770583478862729156564238996272813975933458770577072774024869189703461985605101526848085635948041830177785350205724969758830814647926622386399679732425425577278528070315840951677254223446714512891820919177296356374505525787984012739202959913873258937884728417353564024471569366074341705663516835292839993529303646264202340692428854708302156728863532885617901040511508517739335795/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^10 + 11741532624480316506962429387430029955490281965153349192757470481620687251051768958243190969556291645484675424252218304948669107389781042432860644963376149792549728007113525954656280505287305621163291339326523570341425048673880186982658362075148541413945911487883802567279305387957876538424765267386955103441750119116585027709833359759387638021620071618170331505359114559675794513656466953074540697961829160572228214644845566419379954987347375546243759335026500298197/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^9 + 5023707749016031691487576817170054572859433171960104959642766067787041718693665964280169131446457704480981689297855996331768491052005032532296910329530003651972228970535807003380006633704592430464972580149381426865481366519498056825252074626908562536530815691020808347915151503938750369147109434569964768270820685551683664162948445582910531425269179245698208843039277944462849720900298088514246621825720986104436327586391370758587759216515945536656433861758997030073/278471849483946040172301343609718850019289103323159934064029296399990717650762482645344313775257953224643337678926484189669423683907768262149652496845784330805185445903231125269881920168613336588170937329351144440711547170829682091265460235076216766397001436660493442364812644651132038201520319575042797922512093837831759465765246685719374161778922726421578127619214110578875492206986143269316844768712755951751160056198820364107747827228673757857555425401730336*y^8 - 1378146970917944530428454942901768586349528079806708337099648540841472570618946086368694212288037097783228706050630759707748844100259694229543938535891823281934714941021636795207198157460425915687268528639496611393286747340460340477036518341177160374829085349813491547589606648606116264202338485816849964755678914489851047904295156154368257279105566413755564031128911229730115071695276975816306719256070452990196072742309780579327632519131749284275678999586848891981/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^7 - 888181790808519780722527471108322436772603641129766596133227841197062395609982916332140833023145746337593025612493082464174042835374589705749592363073950265070562288468425221021384115646521330061011503155427062542652293396140569018811940546100780886087237449258353593295419600264777892115285172645270499429950935240235617497884325384020870300426093727343403645924696369915823068587713893355140726850565553775390340864229832801033013532285715631815403690279029497651/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^6 + 93166366949084036972345373228008401891313417518741435412926563634774106816346363573784254217827414321463913471865649834042299763263296727030273145481204597782181480618368251534720511603505394105194671051180242148334754700371987071816768538203741138343398173262650202814401261539413374309087947842375596743497012430875747368548900734173354321506320114070952456936934335011247083304939968688182674780710276528304999658809113116364334118478913585475521886374545649869/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^5 + 51035946580664548681237453581836290604767890288782920348576569143936894802695931925999236082209658536189012095730781058739292315488636258827203772241979620698360485572764913371389908599611004863215344667307234498138854042762946203020055804862913345379822059521356674872899939906239857117100840899256119520298475963911723642598906109979671217942355216886173956085960936558881816525511770848172522658828924037092185630600945414529452110767967035375968083287215605581/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^4 - 3530461638014585651691643398053098821280989604765175853185683300045048316278593011427335982395652892025103078953748317189424222174487553876626741553093386141734602633616122171037408840177567032145735090253487154628933048548558976302875092581074925042988794653769442157808563932453398749461701722602471100934360575844473354571298639274725823873087028420168513927402068121474280020983427305455789969603674422943793891315136354853507737915796000427515098972245401505/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^3 - 1002636146232197964846666693353869178365338041183944920675731757510034193909970268328765749415513561957411396042292883205948104386533787058051008481477233851334123464702038121172635502903327366476239177202528528046574878157422450102628071125540588630148245416285304371986259043555910438485859894310785712212405481617395030626028910322008813198049037530438575657671845274956879955742804049640478607352447315236754422761440462705445160647057938092623322384727509995/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y^2 + 115703048153759820198213436825427718791827495935566143186400143235773922615764457712475537176093521288527475132988118515780890331182547623652973974622533145218084344112922368686590957839564745649942072014121628286913310689728112210063667514379917841131661513916757813614713483910604158144584669672111972126300162068172384175869905408982900371598282539823482019063568770371341867223721203188243742784271540661806044455742666730392674747909468093888416390042511259/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672*y + 5474436962540160262621165243517921032773976803537955932293916096805582652342036719404424429405741393608739808748500669720557946472716697813377660818270893204514722567755031479075159125574185530023720266984908891771877641802567748020482548415323541832629653591890592427597949180162805973190285192700411087100410809053072547423125690262669807130731269323114298912531243004689426750382861341049856907239441464379583232110898538797629446383640607732966780512718773/556943698967892080344602687219437700038578206646319868128058592799981435301524965290688627550515906449286675357852968379338847367815536524299304993691568661610370891806462250539763840337226673176341874658702288881423094341659364182530920470152433532794002873320986884729625289302264076403040639150085595845024187675663518931530493371438748323557845452843156255238428221157750984413972286538633689537425511903502320112397640728215495654457347515715110850803460672

# 4 Loop Invariant
5070219963335242252845138486238926392050882946530645188196579053761819669731034182245686004993076455322478047881134852517828888988317323847274047214888720422645979629380621195716653813603741027590841728379328212108339156057180778013779849141489868345848468174214778131478943947776425685722016610547707661663816040649446561405189381685173380471772260047846479854390303636824193246259843339771062336322489903891320295291321700919544710848473688450984403020718035771701069307013283324855762215987641095430227046861733184423640128980370018255676006353659579852217016818967463241289628231682068091397023092186060462929026758850686511936571164129619254851/711867244036676438150773280877576141497727973792651633834843696638254214604761847889489171704990574558083461191583975509542683784252213577317740368273506276297411510919817074047269455350444038916088529622395730502522349685774956977653737433965869655050019439479080866943020273907927932571104944021305599965138288106097408200220890104105015843829560005441583212727464998930596683723065544253127632709776363909351369464419267782035947404058462687113360988356480072072813304420959799053878164002075228091415627577451258713893131767102027296909458093696556880691673167159941088889999612493898725241925526774367536067508313174036514241631202544240329092096*y^44 + 1685424733518969147885929531984490186782702151011995782548800998722348115627433891410669872133345715689665956500405241997956198027855809497671015482190958440286563381806433321505241670292540857323685909879215990505696526086707253887399383811505569284820401098255036291710431643746282380078904513913937642002054029536741199513839554898007678631230898017146771102369292832440985529232602714174414334338546052720871055361461554825506307324711987170572209396480682227238626813437562608758305507085428021349608336419621262222552860585483944548117194597252488784289226222629533475957922290022207367018215191120074281987741508072972241374978960549845416497809/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^43 + 3465023420163258686538075924282047105111031675528426921989507315879006052817586214185670195030416702812333410423718863454984630634638073346009243565190802399456463593657144079418332269290992922484201729414770058680177967633687234820645427180011247048966048222898144093171960801365820740269589449373518596249488792359166162119100724693760274522416821443467791680808510430938331152892010031692699706140683014956262248065261863148917534221963454495850136734200618721629822963594770558902796645653765283972175084728533250897044294457339889329824122448869595547204697130137527417549646615133721551167400301061568479125794052640437181745307890861207318610093/3559336220183382190753866404387880707488639868963258169174218483191271073023809239447445858524952872790417305957919877547713418921261067886588701841367531381487057554599085370236347276752220194580442648111978652512611748428874784888268687169829348275250097197395404334715101369539639662855524720106527999825691440530487041001104450520525079219147800027207916063637324994652983418615327721265638163548881819546756847322096338910179737020292313435566804941782400360364066522104798995269390820010376140457078137887256293569465658835510136484547290468482784403458365835799705444449998062469493626209627633871837680337541565870182571208156012721201645460480*y^42 - 6732129408785511006060477309885827012287215522704308732935897993059660367701467482597653473438748927985191837681020165257772960701108649934414001296438358861250410454085145522562122609837930533371473169478797181243495301439562468928685880734741970526661949727606985558753499239057356589860503377426068935996204801371285427158379494879969869572006302467636947773345253309138625086577319503883042568971795220819779724051748927883074302615384387671397077950118201353561757292790956425755976475444887478499893237443146260516092044406297804313522685309380106331211026846124717272812268704923842714105383121387392497231112225599034228174496325127163663601567/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^41 - 214322946960305977864628897432313261301406207181923517220446668938829544719895295712908927645804407119287823158545888424738775792246331575006243378655721167063691199192466621459388239203101999119638809200310674281108634624865496548621304278137227163448707177059662004778460038254347739636641341638282227783030364804591751491330034958978051816489411242732807133820549072440188570695773083993383132702881836897144645145396040728769879361833532122383988119720980034313486300739373847812368463789616743397743140261328569186584213114125108918096050053705536914061576742822993379487472301691994884092543432709968935534907041017010107869997389406159397461744507/5339004330275073286130799606581821061232959803444887253761327724786906609535713859171168787787429309185625958936879816321570128381891601829883052762051297072230586331898628055354520915128330291870663972167967978768917622643312177332403030754744022412875145796093106502072652054309459494283287080159791999738537160795730561501656675780787618828721700040811874095455987491979475127922991581898457245323322729320135270983144508365269605530438470153350207412673600540546099783157198492904086230015564210685617206830884440354198488253265204726820935702724176605187548753699558166674997093704240439314441450807756520506312348805273856812234019081802468190720*y^40 - 1738141068225216849185894405875102961841194403266841573589205220871662448075424196282965751339940070914933400813102955892997104726803998111331037552048997017277782413093636285715348048499579137711975812862580922879562625086775007968312317625160559731464893122611259553542840011363972384791164043177504187362238049894713140714784401008535816713537438968572081722823632968841599644516576115706019951111608293622005681042515732666395170745387081266055802387755661947511633147941893885979027342688637639134819836696081071281306390310512940204322133247271753748724394922907520383682323225593257834437931126392384030388753152577175136266106205684313118006522593/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^39 + 1797025996508596609488225281300951251212874741349113518035592721862883564710850481362805212220793737934379877535903400062485468311052601082507136448185362973562845570797183805026892397911447885377724348974749609508589088288650000714097126806139402988559866623609573028579145382828562696497450709004312996882317723391760474117180365825107999076960020991737934058019067509629293443587763496766765438358042330848911227153239687495748741854581148664329877259768651250409921909414345353114041673176008756769443696859307082045697908751773405295885957922620919875164743245233315682190431303021424441171106040216288141280534800709294775468282104473097707605200111/3559336220183382190753866404387880707488639868963258169174218483191271073023809239447445858524952872790417305957919877547713418921261067886588701841367531381487057554599085370236347276752220194580442648111978652512611748428874784888268687169829348275250097197395404334715101369539639662855524720106527999825691440530487041001104450520525079219147800027207916063637324994652983418615327721265638163548881819546756847322096338910179737020292313435566804941782400360364066522104798995269390820010376140457078137887256293569465658835510136484547290468482784403458365835799705444449998062469493626209627633871837680337541565870182571208156012721201645460480*y^38 + 38255571487043088761142794204741697272310648844999325964711828374117123087673526150549728577748481610587114747680903476778928550716944134625179352201837886954214594153307933800891848196479933946088021450781993601852481519984722930465335491466911050761830768555888809731098540571557135139887213243245005943456136992557986292411090456011929222321199153910244006385924845470654585276069657794359622812945405525247987897434537220008402604960419263772679538421929839127406305447514142166913702312714136687012931965806458877334279792311047843407005251340235570459013249932881869114751349960382929694426302106921786597899959152817479199518680406205088416503357683/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^37 - 7440901558529672021379454302028549555819826511829265271764741742393818773412086102162518836675450954827848159330822892042200647067436631094593422446156930011566015933273565053691204615681630593124729130829475311808438851005629806583300834404154702445705724596209037680241331173210580684675206228874336195796137584161264074870164137983806977396836662510861549435024599695031160529878541336665926138284535955663499636538198094366592722465217994980886393761172188200963654850458521515962430275816211129124286364868084635784880674014978112681199510382716676923072249616762229464263906410947039978912844246628194283428487669042433933227865282481830929466159717/2135601732110029314452319842632728424493183921377954901504531089914762643814285543668467515114971723674250383574751926528628051352756640731953221104820518828892234532759451222141808366051332116748265588867187191507567049057324870932961212301897608965150058318437242600829060821723783797713314832063916799895414864318292224600662670312315047531488680016324749638182394996791790051169196632759382898129329091728054108393257803346107842212175388061340082965069440216218439913262879397161634492006225684274246882732353776141679395301306081890728374281089670642075019501479823266669998837481696175725776580323102608202524939522109542724893607632720987276288*y^36 - 379137519566013517448333760295384392144222097846636690345140482873810553793509136343605670498904853700372620229170927617277947938177465986268321906696202876283987513548957279155023428115480653966096405062725703841815384443302840879811239088666613628998236593846336279915024278986357462236030141608443106940842913017882477191786390127167682550142258446042832782861597251957373538334453999353158766719896138615629522338647431989478559135348847385925879984391388564297944219068863602684889770381257420113256337402708110550097970021143754484780923715081773738537204239221489874325519945317844340528285631799637601952013919204002802476274148572251597922830004159/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^35 + 5847332503101289570129202389900413644145135410811307655323654198359350417307859503871566444504262910818957156160669606611240186335368052934836423326616865032892131991026274619771665976977994777590615115051584492374687561951155568757812541125618082918247397942916092519071687667179071477378290600746925082522373940848833405178260050301841672215393353314520175042548030118636147018991713086692412671575749828000428760837072682983484881298273534254004622297782526246372706915098752528555324441730685402100741081961270185778455612881426489437231181670179680681988090141896055956392047367544236888462672127480097602290493162357589071507698660156691380245978599/333687770642192080383174975411363816327059987715305453360082982799181663095982116198198049236714331824101622433554988520098133023868225114367690797628206067014411645743664253459657557195520643241916498260497998673057351415207011083275189422171501400804696612255819156379540753394341218392705442509986999983658572549733160093853542236299226176795106252550742130965999218248717195495186973868653577832707670582508454436446531772829350345652404384584387963292100033784131236447324905806505389375972763167851075426930277522137405515829075295426308481420261037824221797106222385417187318356515027457152590675484782531644521800329616050764626192612654261920*y^34 + 557515626157879351736182557375606573258791941031044928992994656098545054140761515452694597359914032310800270379638268100338476138188305704593906709658488321506596253719953149055909203342324275048764944751590728918682681076882876439314792893127403864920624790953789447728288340514467615979943702789872418981471901951129405707550770165066852315398396943325545337352541836275662731619259893485079378277500645810564175147761678557493420187859179427347570807432135676641305200675233713396109488533125525227668950295179722177231541489246058670272890864358088817451861799714024479702168731021848990121325903991468120727515551937246950311934409260641932534775206391/2669502165137536643065399803290910530616479901722443626880663862393453304767856929585584393893714654592812979468439908160785064190945800914941526381025648536115293165949314027677260457564165145935331986083983989384458811321656088666201515377372011206437572898046553251036326027154729747141643540079895999869268580397865280750828337890393809414360850020405937047727993745989737563961495790949228622661661364660067635491572254182634802765219235076675103706336800270273049891578599246452043115007782105342808603415442220177099244126632602363410467851362088302593774376849779083337498546852120219657220725403878260253156174402636928406117009540901234095360*y^33 - 478445475530374995128076868911590837989714080235803499242079627516395999052854702949265813275282864952523800054778164568728596393834178095587330341167100885560378054157233306084495239093012927316649106585723824665679025305534839623941198999150250064172848830788780683382798986487086452054730479839772266472618019162246949886610813928597392299904061949236851376466267503691492712573880471265200736772188680379743257186879252590994292911146502860637008247710914176978573297958486953157867926656780277642117903040740674456732322498421221414823519288513467722619263051801889909945822747611444535911118493256806272019931740737627392221865821799675957159579516443/5339004330275073286130799606581821061232959803444887253761327724786906609535713859171168787787429309185625958936879816321570128381891601829883052762051297072230586331898628055354520915128330291870663972167967978768917622643312177332403030754744022412875145796093106502072652054309459494283287080159791999738537160795730561501656675780787618828721700040811874095455987491979475127922991581898457245323322729320135270983144508365269605530438470153350207412673600540546099783157198492904086230015564210685617206830884440354198488253265204726820935702724176605187548753699558166674997093704240439314441450807756520506312348805273856812234019081802468190720*y^32 - 2981369739049985731933009064731918387018521440383749395284526676426996963306627774976189362140769752752999027115163594370360076419902527959008631236924990621996387572028376819671779425064664098378917167310609128821234096345476678716030276061721315347391923754051805497847501472541564071456876827041520446561552318496116047491813271970369024696058080086291055573490976890918026704691254373959608626246762274568885971045728120489985443988947108397085734502263103071640061364799625871299638776557403590248495038911962558217161639671878245479231753776483941958048038265631468998594924471193477635385546990536163629255091716985930500456294220107593453985017352533/3559336220183382190753866404387880707488639868963258169174218483191271073023809239447445858524952872790417305957919877547713418921261067886588701841367531381487057554599085370236347276752220194580442648111978652512611748428874784888268687169829348275250097197395404334715101369539639662855524720106527999825691440530487041001104450520525079219147800027207916063637324994652983418615327721265638163548881819546756847322096338910179737020292313435566804941782400360364066522104798995269390820010376140457078137887256293569465658835510136484547290468482784403458365835799705444449998062469493626209627633871837680337541565870182571208156012721201645460480*y^31 + 335466485139146150818572862075071275409605614421369450803040088271736506458560958763012778083845482698290463216238508468472146817025405196290663170074723877123442966663713513722833793404731720127408615743900266568506483000368529314591690407747021154737501861195779454042512146638407945150815914427546438915863934767647237542671091231343508149226293166646168793068570390186994545510878777124628550797716329763702888695905371920186689990464068668115079716499614408285377615831185906522912305404204886716859960567745601399346280184618640795577555240300406337937406655665189494463801413489239982858057508612383157184104304151673900766537921040706060505763019217/711867244036676438150773280877576141497727973792651633834843696638254214604761847889489171704990574558083461191583975509542683784252213577317740368273506276297411510919817074047269455350444038916088529622395730502522349685774956977653737433965869655050019439479080866943020273907927932571104944021305599965138288106097408200220890104105015843829560005441583212727464998930596683723065544253127632709776363909351369464419267782035947404058462687113360988356480072072813304420959799053878164002075228091415627577451258713893131767102027296909458093696556880691673167159941088889999612493898725241925526774367536067508313174036514241631202544240329092096*y^30 + 3096120779245651145196774063807116389786097320435707146099696846971581393519061117037935475946935981617279287741309406506974477487607586307221561300909071969850231091433136907766755375677512853841585398350828338767179005136369242409283945542802818691879296688969352301104112272993481937690620673527520900487964573967240636586205231999467452858111082178926603725331454226764549225221804582735249308823722730069227973608130513337946145667986363803871172736052016712055997122048702239284836574591529082575717228697048211388509421228793337530257590708258339202523818072878411686481255387456879581952497565010398305962025293440157173690584961117951207985476084143/1186445406727794063584622134795960235829546622987752723058072827730423691007936413149148619508317624263472435319306625849237806307087022628862900613789177127162352518199695123412115758917406731526814216037326217504203916142958261629422895723276449425083365732465134778238367123179879887618508240035509333275230480176829013667034816840175026406382600009069305354545774998217661139538442573755212721182960606515585615774032112970059912340097437811855601647260800120121355507368266331756463606670125380152359379295752097856488552945170045494849096822827594801152788611933235148149999354156497875403209211290612560112513855290060857069385337573733881820160*y^29 - 217700463591709284614713087806381898657824284996165882914572995069084965614367339085077575135232136144681237087002371963272801618052277776236982478360485646703569313747530730577176862114402571152936083510505815229495942681328833940443045674879157079615103891524275487760623384727582114159853903056368374026322480942282082615284036807344574154970029822958117183339977343912654741440761403446053124340434139693913350669337586013044336113304994017922117856215296512300554273823069471759719840903175584005465827302894276444953931609738879301833304079963404352899575151182725776907082443381439030168422520611675436275438772133506689270295142252155542816105473013/118644540672779406358462213479596023582954662298775272305807282773042369100793641314914861950831762426347243531930662584923780630708702262886290061378917712716235251819969512341211575891740673152681421603732621750420391614295826162942289572327644942508336573246513477823836712317987988761850824003550933327523048017682901366703481684017502640638260000906930535454577499821766113953844257375521272118296060651558561577403211297005991234009743781185560164726080012012135550736826633175646360667012538015235937929575209785648855294517004549484909682282759480115278861193323514814999935415649787540320921129061256011251385529006085706938533757373388182016*y^28 - 73966277996444311750320990733695348037348831113961582271945309632682018254748965255707260930877797808259958984276727828098759680573074652999955296705900919698185610752039080011784633019181890418420577023747222143272315222191046321446569093394162278661806892420354805083549232257259994968660669650021116712960509879181697868033077508670562984221228731129507366609106129593645661599142081759370245917285094790075907136684681733074918917825373550746990890158990384709969850303565184878923517478467527032924263282994510419942121238220087875815601380079027180586498552488974166360256380627842633514106229365706047380817185891481977307544483504303176771984034665021/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^27 + 5056772864934733462077093456983964673439124209455687472925560358332281112506548774769379329139540559299748501406456032076939061046308031166999099907983803344718109598862228413867124318041039005102920597998204242347970210269309248759616404315228348506053471763837971114994218343138501830560686645553488787316450656966476898305039512871126500393877257757844605017707941031942469827422882634649040563713592507974065204556743996803309899698144019743679503597457185420414089352977575667529226044187978390780578081307343418425830324551479004030038394029468449395550475720872433061451313353049651141454542528740815098036878821118945731224967637373488031454870880963/1186445406727794063584622134795960235829546622987752723058072827730423691007936413149148619508317624263472435319306625849237806307087022628862900613789177127162352518199695123412115758917406731526814216037326217504203916142958261629422895723276449425083365732465134778238367123179879887618508240035509333275230480176829013667034816840175026406382600009069305354545774998217661139538442573755212721182960606515585615774032112970059912340097437811855601647260800120121355507368266331756463606670125380152359379295752097856488552945170045494849096822827594801152788611933235148149999354156497875403209211290612560112513855290060857069385337573733881820160*y^26 + 161691255731397223268480860009850236436138115291041961283744979550339362171643424792424809328860869168726684861114060574018128139099566913868454686208288681355290483296788619373751066233509492997180916145801746915552983340724706887683093414051342649189225184575176465050360570313105473418053524649820335063014581445997702385983506335624692701744000261125365519044676849975204414364179332001841077665634982843744014987101617409894995985281574328350607370237151579191887485466738487551822634410183014649988526399397269964972307844346517374279774719644663106559748370052884288911313231060289271530094718922207504005877087642106324914323068344063804164866329212987/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^25 - 2519258877797030588212178179625444074251798962101134568247301010577382013833693495623842364824339083950151916799139500567990868639204285806222171034191174600943655478120011394554282079420229566249090682951706361101186530625212918827209392831697270413861747899227006578091663398293155171963541226429459253279502496954884053005308631604375657490640154874197473019488697418473064620103051294372221901956010177372544082272997621005424554980552848580889641855965842453590503241016799044929502250816012956382333385541403666910401986875465314415398154602061185025084074178121900816504175380322990377830880619632396028283466271447423040354972016130624564509672445673/533900433027507328613079960658182106123295980344488725376132772478690660953571385917116878778742930918562595893687981632157012838189160182988305276205129707223058633189862805535452091512833029187066397216796797876891762264331217733240303075474402241287514579609310650207265205430945949428328708015979199973853716079573056150165667578078761882872170004081187409545598749197947512792299158189845724532332272932013527098314450836526960553043847015335020741267360054054609978315719849290408623001556421068561720683088444035419848825326520472682093570272417660518754875369955816667499709370424043931444145080775652050631234880527385681223401908180246819072*y^24 - 64661208762286655373990662406569545327933248391680169343959414594815185523358102618946708201851765948240698330819902644099574556408364802415943457483615615612457652432178371754344081567835282672253618095979269726056200807536697865254040236494167115640804771391891539004017246914768643598231275183606083750544236785934166732456272837416685276768098351590492459745240902516945942303406136167548415790726506951230855978158451302073422431611989229007430025436774254001405263992344103789802926761440864608135379185748145473111725570234158895266986861024347959086427227152594329861954004508445695805775888606399646350714737113836046467921710834263047388637119973279/2669502165137536643065399803290910530616479901722443626880663862393453304767856929585584393893714654592812979468439908160785064190945800914941526381025648536115293165949314027677260457564165145935331986083983989384458811321656088666201515377372011206437572898046553251036326027154729747141643540079895999869268580397865280750828337890393809414360850020405937047727993745989737563961495790949228622661661364660067635491572254182634802765219235076675103706336800270273049891578599246452043115007782105342808603415442220177099244126632602363410467851362088302593774376849779083337498546852120219657220725403878260253156174402636928406117009540901234095360*y^23 - 145261805877553804217687854131294935699681029187593430548062553859381166562139026647871581725540777811294918790230040867209654323565493771386875937247976379934831169856167386051384467125787419885343503557578060193240496967623198407205044750563324989873856804084597350982721583101515162866516213049418279729339111418465816221550150711275506645870499302921825746156993330975091098593445616467402716555508685648158899446759121580850333923876379617080687886441809035786770648283843145048782264014513943819982164466333290253269142814016737000586599853813538968611708112588625864761856712515671221054072308235571037120022137307997309367612700388642204720417451333/333687770642192080383174975411363816327059987715305453360082982799181663095982116198198049236714331824101622433554988520098133023868225114367690797628206067014411645743664253459657557195520643241916498260497998673057351415207011083275189422171501400804696612255819156379540753394341218392705442509986999983658572549733160093853542236299226176795106252550742130965999218248717195495186973868653577832707670582508454436446531772829350345652404384584387963292100033784131236447324905806505389375972763167851075426930277522137405515829075295426308481420261037824221797106222385417187318356515027457152590675484782531644521800329616050764626192612654261920*y^22 + 11399348277791352021426600597355439541992227660526256981698165763448753876549053559984380809207677472180904388820186467220737428333503987093861164681333185150448831859059444019928959506417758365545429122608143209215770081660073348105030892400931150305826189391393812754269752719875589241335260790335895671665211577379177174626087885745219120467458321718835160431109597780432652716800676806165763062971484711983693093222889498293877134712956284345420983582745064768661915197185410033515382408028270464925800709190574052047811362941028644256477430104394942871691789295134465720899349731443952458699084999512512501440197989864608469420641998930073936555339508713/444917027522922773844233300548485088436079983620407271146777310398908884127976154930930732315619109098802163244739984693464177365157633485823587730170941422685882194324885671279543409594027524322555331013997331564076468553609348111033585896228668534406262149674425541839387671192454957856940590013315999978211430066310880125138056315065634902393475003400989507954665624331622927326915965158204770443610227443344605915262042363772467127536539179445850617722800045045508315263099874408673852501297017557134767235907036696183207354438767060568411308560348050432295729474963180556249757808686703276203454233979710042192695733772821401019501590150205682560*y^21 + 80020133172567968136727939981199726289224464231483512512577534052966685751961464639896991336287961591274629221674933073470532503286731492331695170083194065137414970496933602236511307675408460475837777083621893066099637138670931874747394662573218391661138762109080152702208036586194844909392286883269725690183968757868760592720731936412761959661359292780487052195137091095176361830738362420196474832059502765664147015246275657099222363248802565546612798631516460900386471043169565571966259400808332075950201077635709800342861081882551352508723796216068193416377337507865480020532187003261285803770554721124411685071843328622655381427339650225865733257689709/11122925688073069346105832513712127210901999590510181778669432759972722103199403873273268307890477727470054081118499617336604434128940837145589693254273535567147054858122141781988585239850688108063883275349933289101911713840233702775839647405716713360156553741860638545984691779811373946423514750332899999455285751657772003128451407876640872559836875085024737698866640608290573183172899128955119261090255686083615147881551059094311678188413479486146265443070001126137707881577496860216846312532425438928369180897675917404580183860969176514210282714008701260807393236874079513906243945217167581905086355849492751054817393344320535025487539753755142064*y^20 - 60286095321278945320921758881916326323329239438239496597810721953660060230014812874871371797593332299982097250671784034412394264304098365256052483146149528624078885716889970812274940296109383166107448338906046023399833791272043452411957915199979332533112659904336146773899057219082895924958624805011126467602302253263111218360567610711780685234262251120958061643702370419254075295275910996353133567999166612338302494005765566725113310934602185824655848049840180442563140752322599533788735922177896467341992594121552910444768458763386931725171326321208071138062110590381819963950978620697765267573688767930570089792336028432639809272199201006907968005931424179/3559336220183382190753866404387880707488639868963258169174218483191271073023809239447445858524952872790417305957919877547713418921261067886588701841367531381487057554599085370236347276752220194580442648111978652512611748428874784888268687169829348275250097197395404334715101369539639662855524720106527999825691440530487041001104450520525079219147800027207916063637324994652983418615327721265638163548881819546756847322096338910179737020292313435566804941782400360364066522104798995269390820010376140457078137887256293569465658835510136484547290468482784403458365835799705444449998062469493626209627633871837680337541565870182571208156012721201645460480*y^19 - 4863067464322622900276827969791842086865049648143704596297080111319982183335596357790817571096903002871830510924348818366002197980403392142818393403770173150734070737830617305673529845306090485704651298341308808133526339913314846610870211648180790770036033761420496457094504195913747991264499677117690558260261040568138096015976762013448734751363316218695712861753516674479353049510852583561839979893638914313436843995872993004955532960583397760090500660218022356210386700915508242125652105468044476278400123789983076324679156870068449059836026265253382846525501919147004686368732162006486977823485913182301011390390202561690120673294187682223627656446394577/593222703363897031792311067397980117914773311493876361529036413865211845503968206574574309754158812131736217659653312924618903153543511314431450306894588563581176259099847561706057879458703365763407108018663108752101958071479130814711447861638224712541682866232567389119183561589939943809254120017754666637615240088414506833517408420087513203191300004534652677272887499108830569769221286877606360591480303257792807887016056485029956170048718905927800823630400060060677753684133165878231803335062690076179689647876048928244276472585022747424548411413797400576394305966617574074999677078248937701604605645306280056256927645030428534692668786866940910080*y^18 + 9301091037791022841308166531911684440890988832278732810299971289560777972398754727722897087197290340692470689062305956418236346111232175062871178373152748589141054530347470223981843192147570893101067155446273133460333864129830056447371506774078456210094127562458521087773082434198706847526887381157195491155146888572653436462905694195509055812724485251964487497793028440048487324417672842125129868992978012258635818772201465194406806899662690750088564897103613552333045044903544855441971760302794102295089469387310805161048686441873785482742241041217759692871802173027487335723448917624610707574810183225335478789768942733954376510038126050814274775583125157/1334751082568768321532699901645455265308239950861221813440331931196726652383928464792792196946857327296406489734219954080392532095472900457470763190512824268057646582974657013838630228782082572967665993041991994692229405660828044333100757688686005603218786449023276625518163013577364873570821770039947999934634290198932640375414168945196904707180425010202968523863996872994868781980747895474614311330830682330033817745786127091317401382609617538337551853168400135136524945789299623226021557503891052671404301707721110088549622063316301181705233925681044151296887188424889541668749273426060109828610362701939130126578087201318464203058504770450617047680*y^17 + 50590546340744582537765836216838457441970438807210051629470388836698514957296472106010155929832479502723493483952644968952232793289999291041033663462873570308455389240535244909855828680240850212895866002395175436429085622810468465185728250631512535538432843615525472441342411328711652760939860672399833776251238960230347261532921514610713346564613812464140615112892748996192354204817555577479870539184809149801106897525311048846765250867330218094172610278628470206732805816085258265731086824662806632938411592174858531459776153261319624215445828337755981422493774148236552302416443194092749838321853740602314810505823331410036588269719359842389156032398598449/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^16 - 9709583815253832167935365128968014652154538785436292494456016045250066446547770450551254837864297123795820019228437891068803119840046141863822397235528275552146728496190706998733653599655351776437433034965170874455043237095218922710160679729768543687753778149022014841249996051985458787417829350244422869482460910107206022434111673787069314551283906987235892632540561409432715152144906367615672125549000267698257834581386995065400700432440229029240795196490938414523438266352231463241042660008841045070292256430185044712966616413154557331778441678365963585582696098128288087318132343638982517916678332736007778069782276081598181806015502355962036154296698823/5339004330275073286130799606581821061232959803444887253761327724786906609535713859171168787787429309185625958936879816321570128381891601829883052762051297072230586331898628055354520915128330291870663972167967978768917622643312177332403030754744022412875145796093106502072652054309459494283287080159791999738537160795730561501656675780787618828721700040811874095455987491979475127922991581898457245323322729320135270983144508365269605530438470153350207412673600540546099783157198492904086230015564210685617206830884440354198488253265204726820935702724176605187548753699558166674997093704240439314441450807756520506312348805273856812234019081802468190720*y^15 - 758756820818046998438752904361271545487631374868065147110414162846519945920794716830502176347725813043975815188091400736303237719701162539173276722452952590954926476976718826256996287618609429244262381080792410084786551926070099550395335097992268015494559704145693954719543682700820140322186919294093764373587661237907209618677568361819427361985845166394483132230099693330290936632470506295525537338227884914124980874776219711985328174521331030677742396469316490054192036178508288512602286362586796381800102927117229564463989854386969357253847541407058008926141497337724411146199371025831572760983887260352333567713397189092043108259242046311572217842941647/444917027522922773844233300548485088436079983620407271146777310398908884127976154930930732315619109098802163244739984693464177365157633485823587730170941422685882194324885671279543409594027524322555331013997331564076468553609348111033585896228668534406262149674425541839387671192454957856940590013315999978211430066310880125138056315065634902393475003400989507954665624331622927326915965158204770443610227443344605915262042363772467127536539179445850617722800045045508315263099874408673852501297017557134767235907036696183207354438767060568411308560348050432295729474963180556249757808686703276203454233979710042192695733772821401019501590150205682560*y^14 + 553754457514638097161490818843000613305413994029921430158713511637966731304308314099074835823382757914009774270545270770416759996659510089754066197698313252269675520396707454626953037627776879428805752973658534576401216285426310143245560078853837405210761686340566273212086550947782274059669631379557680693792135256764357557824341268188373989083492857478667375853866049483742161720995001320734234273351466620948707827057846680522471106107669407909945279764175795375067623266588584692181335403122477757884265999055374573331399890312570419582240180316585393081524480431202863794818266555840518313058227067344128325962634216040501166140075601250419816537185259/1779668110091691095376933202193940353744319934481629084587109241595635536511904619723722929262476436395208652978959938773856709460630533943294350920683765690743528777299542685118173638376110097290221324055989326256305874214437392444134343584914674137625048598697702167357550684769819831427762360053263999912845720265243520500552225260262539609573900013603958031818662497326491709307663860632819081774440909773378423661048169455089868510146156717783402470891200180182033261052399497634695410005188070228539068943628146784732829417755068242273645234241392201729182917899852722224999031234746813104813816935918840168770782935091285604078006360600822730240*y^13 + 4455517805351324653581071696755561193411208675576860805894072781120775686709286277628708719617554254621064106643342726390631541577335919059755955488429591275526272665887712357566229105731763545312629936903087167800278931455727437962255769271955536788115256508055659099517698324664879404289857882483160965962951841615326209665692553413837597468776557096038046976543767705668465642921996656064012548933919030126571559565702268623832965934491748526863926258572240885091067680144365821900569735632878218379463484805426325326074594699430545527677258616315685400980760665775562670836074249027418404148391460160268807790312170895163912576854898298785484637940647247/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^12 - 85298630104877822057039876674616478024700497556532781382281184676297807699951671408730301565906859027688857777685043741491261853137576484342908215318491895810193512871456724236839674268861039275362187602000230114323439436218892157702154526372827778222804832409521123152388855057067731268672107753689659649257485362267921908091752848051299518712772668377250562279839086692826747925022827060420412010560802422447814529135650676696523803650318211631582896426369514375704214147740671929033018082407345110876153542862479136159058751334510154291854138327372700824987188084914155300445190970936829993839757192383347396936715961929334497580170571896991943897675473/2135601732110029314452319842632728424493183921377954901504531089914762643814285543668467515114971723674250383574751926528628051352756640731953221104820518828892234532759451222141808366051332116748265588867187191507567049057324870932961212301897608965150058318437242600829060821723783797713314832063916799895414864318292224600662670312315047531488680016324749638182394996791790051169196632759382898129329091728054108393257803346107842212175388061340082965069440216218439913262879397161634492006225684274246882732353776141679395301306081890728374281089670642075019501479823266669998837481696175725776580323102608202524939522109542724893607632720987276288*y^11 - 774559993115287137892224258771293119169406746649839657075964192122807041067118290698014808844262421615270665670588531121723465828945401169518387740214263709254909907785891190124041320436193331127468563408064714595176519918864962323631451492693255518662781269895164960610735151514641731385528152621007730198308959745079451634880762321911054433591004162727961884265723939803491589747539475099425417474551916371366992484848099801557082587599099276978277022825259804762326164319454400654485549273927892645528273332500414653344058561128427150578534964556723999416117161611119028745820286581658536017418114802784533415880876299637913506904444399194460272062132117/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^10 + 2326131256856721359949703247485487100400746132344056486730113579924192049627527811765364103048866336636762466846174976398862576877638976671965479366493047844181193455984356541337164311348041815249522613929329490556708912262895082605058664610919439195004414261131877473126509123559685885170035260029070055238013666889219010291172082744004295988215355058814255781313389129666466194776817333731158280691309068150949274660109388652886351856667034302454733087113197695183219014796080299179799188790988261105198263383172360496931758172314647157079878513042562682772292840401850134741320583851541368275755162817921160040614122167756717268029791200212210103253627/444917027522922773844233300548485088436079983620407271146777310398908884127976154930930732315619109098802163244739984693464177365157633485823587730170941422685882194324885671279543409594027524322555331013997331564076468553609348111033585896228668534406262149674425541839387671192454957856940590013315999978211430066310880125138056315065634902393475003400989507954665624331622927326915965158204770443610227443344605915262042363772467127536539179445850617722800045045508315263099874408673852501297017557134767235907036696183207354438767060568411308560348050432295729474963180556249757808686703276203454233979710042192695733772821401019501590150205682560*y^9 + 32887656942604254430485128630435850662066325400410163885429784894879300259579767974888272417766030855483394984444099258187864354984017124699609867885647288710996456720440942796063014949956204098987650819472237660432772181945701576328063496764896661754139905904290424053917090878334601729148731886959528098521314526520387687893417999682501929715749678097560703413159062502472979369052246117711097719162578474621014716945606116597013976580074807391249713867061436388596898419921678969859139839496865228773472679060905341033017825772931713185504033940345901778666508358037594824857240046893346727541405188457286454049711948688286166322792256271877641752072441/3559336220183382190753866404387880707488639868963258169174218483191271073023809239447445858524952872790417305957919877547713418921261067886588701841367531381487057554599085370236347276752220194580442648111978652512611748428874784888268687169829348275250097197395404334715101369539639662855524720106527999825691440530487041001104450520525079219147800027207916063637324994652983418615327721265638163548881819546756847322096338910179737020292313435566804941782400360364066522104798995269390820010376140457078137887256293569465658835510136484547290468482784403458365835799705444449998062469493626209627633871837680337541565870182571208156012721201645460480*y^8 - 1339214978780490824857787093449113824662474200788317883119555346999579936185443681410111349968136506057980306229239384302864444079178979589645082858847410298009528850526538843656175583441483194660188588478387536010036096154236535298507323029620659494287153567696636648027948795281018173012301017113130610830096987404016145857147244239318138711142785554984762445435624653297348114243392426734842896515329593113054329032612124681245715392700305837318268192705364815983561070698871402961224787475435877018246547162653899569698570853870583211044171922977651566552975417162854462383572258667995899379203898143593790766604436372873852508085138570855335752441531/2135601732110029314452319842632728424493183921377954901504531089914762643814285543668467515114971723674250383574751926528628051352756640731953221104820518828892234532759451222141808366051332116748265588867187191507567049057324870932961212301897608965150058318437242600829060821723783797713314832063916799895414864318292224600662670312315047531488680016324749638182394996791790051169196632759382898129329091728054108393257803346107842212175388061340082965069440216218439913262879397161634492006225684274246882732353776141679395301306081890728374281089670642075019501479823266669998837481696175725776580323102608202524939522109542724893607632720987276288*y^7 - 1873027231153615489600973517097768254283936042597721750438213498440829681586982338403178379197539309566036316328648135409196209498745972679255880007593130823974876540998275625537907125232506185225803319958214735974798609336615364134993148495706399157303837892769092935230950723958169985084896919439158094800026527199215776792806582248790256613290565597396886380599783634240686778300589593212059885829774240336462943754785523483535408038784388661653296359501249295518548099982125475409054071810736632631488128862618067037822792060697331345905450286244518848047388124996955261868297683089657168318020102481904774094341476781595418124480870935960195168487593/2135601732110029314452319842632728424493183921377954901504531089914762643814285543668467515114971723674250383574751926528628051352756640731953221104820518828892234532759451222141808366051332116748265588867187191507567049057324870932961212301897608965150058318437242600829060821723783797713314832063916799895414864318292224600662670312315047531488680016324749638182394996791790051169196632759382898129329091728054108393257803346107842212175388061340082965069440216218439913262879397161634492006225684274246882732353776141679395301306081890728374281089670642075019501479823266669998837481696175725776580323102608202524939522109542724893607632720987276288*y^6 + 414513271055603677285395263440424072972451630751034454316857072309794741570482830555615043853966745036549060941772204387756227092611161445868945412799762655345921711567089628283192996475502615676533889884026864718244785179143384279663609089476970341026288099952464609444901054282290676611310380512083336501610987207042109879254272879034429100558119879490670950590491049568947456805824221544014653924598082930547130542176395646859915139663082309890639739933006757959178380820190769951185391691191704326827637070809100483975492398837742871750177870376381430961990064422195791570638151678665532048824252155343101396657539354323679092259446227798100847204509/10678008660550146572261599213163642122465919606889774507522655449573813219071427718342337575574858618371251917873759632643140256763783203659766105524102594144461172663797256110709041830256660583741327944335935957537835245286624354664806061509488044825750291592186213004145304108618918988566574160319583999477074321591461123003313351561575237657443400081623748190911974983958950255845983163796914490646645458640270541966289016730539211060876940306700414825347201081092199566314396985808172460031128421371234413661768880708396976506530409453641871405448353210375097507399116333349994187408480878628882901615513041012624697610547713624468038163604936381440*y^5 + 150130744735148303392582065913935386658432141461942602294637250830952999163774513981860150256783558001431467168380320246392753592636364730586991484143468602679785003546651997593071752553821971734349933841484717352657388696620069995948090386590384202561821138721284233151698197431640769446002333058863952984169793411957083864578358216932102275869522004308501257230246669235766354137093441844018561637265812739621473345441192186379718847747926251303255186917088629220914437660219939146597178401511457514885424297429964914371992885698585228422241336091703638951304701936323233778224335798970341156996070225243990823689127706790042620210517265947996154446593/2669502165137536643065399803290910530616479901722443626880663862393453304767856929585584393893714654592812979468439908160785064190945800914941526381025648536115293165949314027677260457564165145935331986083983989384458811321656088666201515377372011206437572898046553251036326027154729747141643540079895999869268580397865280750828337890393809414360850020405937047727993745989737563961495790949228622661661364660067635491572254182634802765219235076675103706336800270273049891578599246452043115007782105342808603415442220177099244126632602363410467851362088302593774376849779083337498546852120219657220725403878260253156174402636928406117009540901234095360*y^4 - 1570351670578920212067087128441079184505738519801876891900131180844891100001934974780399983024760137610487892458995549709803668753668619441109550366379882341771433988285440842946087446457007111380692889495919577254346642815268245402846407267414115805970222682264451803252452104812256876646069083955412963530793556610227854835614700887399926558713163617453061909589635840214377112540465241811088781458632132370309958186132357689178194106923220610315612964127312660043658202274572743394434827946463385933481846220709714987594507153295947021837252567535571671687949933001684029097557196613251978491197686753477481138744883264668724705535730610601645466261/1779668110091691095376933202193940353744319934481629084587109241595635536511904619723722929262476436395208652978959938773856709460630533943294350920683765690743528777299542685118173638376110097290221324055989326256305874214437392444134343584914674137625048598697702167357550684769819831427762360053263999912845720265243520500552225260262539609573900013603958031818662497326491709307663860632819081774440909773378423661048169455089868510146156717783402470891200180182033261052399497634695410005188070228539068943628146784732829417755068242273645234241392201729182917899852722224999031234746813104813816935918840168770782935091285604078006360600822730240*y^3 - 2063149822478072162809789308257192901461423771225702724235104092200868949334709264462214656109535243060139053535245297449147500716932830521526918310541685023458308383699418670864164698286987563259974289970424360565632781756958208611441816030321161953562458605963572907803987835121529778163479473529999557977437381325586245807015620217890411815580065893047705265563855395054695422856066880763861617512411005146373473055436224979294547188770834512705215367278410912020554180965013629933443009213143396359962739224167690108681587886667578223302751396004273190213593301261905866576331893195960381655913372941719507218595857010410455986561485340087237302413/1186445406727794063584622134795960235829546622987752723058072827730423691007936413149148619508317624263472435319306625849237806307087022628862900613789177127162352518199695123412115758917406731526814216037326217504203916142958261629422895723276449425083365732465134778238367123179879887618508240035509333275230480176829013667034816840175026406382600009069305354545774998217661139538442573755212721182960606515585615774032112970059912340097437811855601647260800120121355507368266331756463606670125380152359379295752097856488552945170045494849096822827594801152788611933235148149999354156497875403209211290612560112513855290060857069385337573733881820160*y^2 + 80017204594505050717957282476418599789425708807992726343186131677010127982819370501674343805482664291733771424819990587856311369526018470402199442706709625030971843322179439919465901413495224165768869390261837952748302690507101301496106917867873109522252557848559756228905274077665912202071114114074089056221509824309434741264837779627145274598984214072697536470733208873638780053870532628149109170347160697477452745619281981094652943173461997324705312504948328322415179311572710469946580104448080643051535138772019986347415257429358674984716501003228465953180631534962564763864273780228311928301075922970010644053701359070262984194323551184112428989/2135601732110029314452319842632728424493183921377954901504531089914762643814285543668467515114971723674250383574751926528628051352756640731953221104820518828892234532759451222141808366051332116748265588867187191507567049057324870932961212301897608965150058318437242600829060821723783797713314832063916799895414864318292224600662670312315047531488680016324749638182394996791790051169196632759382898129329091728054108393257803346107842212175388061340082965069440216218439913262879397161634492006225684274246882732353776141679395301306081890728374281089670642075019501479823266669998837481696175725776580323102608202524939522109542724893607632720987276288*y + 51163611115037226866663818743653214313631862971855577113055228895533192052311799133688688982049470529070785490109919563848411380272075366505604123893288742814764527229938307959411708091907009760983612209264466693404908804969940273913767795424849952888992303512500115556815324052995571889421058405620613813742709805614056589118691324373518782842777427944216210138470698379762377375865445221715434949957910842834576372650877942802980182054262611660866103097175126936296352999751742594402000761058554940417375633631603310258204028548482444818430682883047114291559111780090518634646261929036986692075678708112283692797321621276150289151572035043482811161/2669502165137536643065399803290910530616479901722443626880663862393453304767856929585584393893714654592812979468439908160785064190945800914941526381025648536115293165949314027677260457564165145935331986083983989384458811321656088666201515377372011206437572898046553251036326027154729747141643540079895999869268580397865280750828337890393809414360850020405937047727993745989737563961495790949228622661661364660067635491572254182634802765219235076675103706336800270273049891578599246452043115007782105342808603415442220177099244126632602363410467851362088302593774376849779083337498546852120219657220725403878260253156174402636928406117009540901234095360