# Manifold: Census Knot K8_11

# Number of Tetrahedra: 8

# Number Field
x^39 - 17*x^38 + 27*x^37 + 535*x^36 - 3322*x^35 + 1429*x^34 + 41462*x^33 - 142671*x^32 - 34523*x^31 + 1096265*x^30 - 1885103*x^29 - 2009365*x^28 + 8860889*x^27 + 1593140*x^26 - 11474903*x^25 - 52940936*x^24 + 107459283*x^23 + 309273867*x^22 - 756887343*x^21 - 882290687*x^20 + 2568169852*x^19 + 2391244296*x^18 - 7381100112*x^17 - 6392135872*x^16 + 15603680096*x^15 + 11361226048*x^14 - 18568542976*x^13 - 13488066560*x^12 + 13231817728*x^11 + 10549178368*x^10 - 7698317312*x^9 - 4568641536*x^8 + 3656704000*x^7 + 866205696*x^6 - 892010496*x^5 - 110231552*x^4 + 82968576*x^3 + 21757952*x^2 - 2097152*x - 1048576 

# Approximate Field Generator
-0.179484180706617 + 0.193996599837175*I

# Shape Parameters
-207906746934595062149798804565031012508864583397445583428782472924010623482728557255730144488807015157128438078858182301867381692699878201773200583047034528465917886370560975/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^38 + 3421420881958764527022212811422410677924085545403444819507144656423498086009062010813096490686082016258561296178286520495544744440189530664084516363579816126455017960155676153/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^37 - 3772037761350588328797697735039829511853737546708548834695349991711817167180629757382024988972575033726854837653129894266189047668758416795222413741263785935926327394713233267/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^36 - 112974631065754670008596929906223919285249011412905879139870665577275295549683162495829289282277269744192190125069524369427798519583915644649637888353507255109846887238399386679/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^35 + 39299552237104661519677180728989161313293489601744812643376647782163182503392889385037081984701255301980670207963514587418845078092326283548698566510912776413919301900747863873/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^34 + 35063749131423411026723189968844953208882467752315432109401331735688330099747354991260439541617266588541581649214649343417224828208579025348891357230416837815293783852881030021/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^33 - 725376953323351786770850729397657412924117632309722881886313556213554094865720884399537692282730225305295769449625049881928688553371195145065862509119263902086868644706588547/49846288832476282309283739402418265602056755447618533815305234269951640506794738780139477724600735792741526244366530571300763152013233897003105106555900376818842065938387640832*y^32 + 24994571145271829091275388258425798855603253467886730236529093109101622605907327608700639962544517658700067094048745792428414624537653348553542460981196588597931464259380046762761/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^31 + 20032885310877572619362189756132865005713681561770941938212382735539321483540497626115141219530842523294289315097245840005272604701502545109459065599216424998209930027984339617783/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^30 - 214518023596666842766266605442247275440913696909297003413945431382376654143769696353200736987400637632972364119063541334111803955591815805059845087477497764760377861034812429503113/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^29 + 275874965744380513150454336882894509877214020245728207117948679265640150750210153240894879950171335268972054477474866133553344954199143056627004080802967726936726241060522267888215/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^28 + 548849025389415894040982166406993497681048047687454731027825104327684626193727128626053347925328614341985049867630200071754304692850891827080599265721271567840457986499667430979153/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^27 - 1511094097954438476293445788178704817478642011303723267938340239574329455918701965793181845918078299282460187260017331454717526433117558757787338685419228540118684039767406024646845/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^26 - 560282178506005657858886271523539794832415576009061322939497184434281317897697308400346620643277303589220801067798661588210479474058658335808790933804671063392187908309216709815815/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^25 + 1631004695160792950401804585415294198348915225244721835901273545097046812544416253881890475897932364240132833093601983974845712415230252173375660360673562293932886077561399090438077/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^24 + 5932133042938039230419722350670453413542658630087405175991174939185432874798782930208244201557097274476282277650556890587313977948373994102203038852686877068699680113596082010657849/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^23 - 15738896551665274851212403479892072948401516758196550119584802068771786019932255215488107819848164159880162342250281982066358832558362700019281093175613901603678024413561286331397137/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^22 - 71892758391429282168108268988154833858872401845121780395832685679711541381053381832673805864362348853016242873049509020624208170566422612715863295457671399037539188364802262362467799/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^21 + 116463925045157802787690154502954077955733904098079241695603448935189479706838758252703950559759132874727843986698365806961591074348358578985816637652982835734606152941762913166352083/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^20 + 241359883267882020411001917057186321170309014897866820569219123220382236928844592159998929743394412304708238556666906945244154593655049131001762738170065096341609070327205828996961919/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^19 - 195062239025087460880459538292287938002836594955707765950972364535750845368833421076360418193583146294346031777673548834345794557295311657899355651581456376386064511095816974343799191/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^18 - 173551211905507642087635031864487573755637940901960988124622567999766401781552014654469312021986500115516683167717198607379746743943996029428588158038669907684730331725293354370849225/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^17 + 69778497644866801060503674005034545627557972225334877600060166003217342976300731038921069449936872542589709994475295986242800813657225989659371398025514025281263785753671198987169961/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^16 + 3700234784500828763595824347022134622909865198846671807138864300188950963417945832727601549006989866489798480387922256493343828113757163064606484777591649952304553323506950716270981/1146464643146954493113526006255620108847305375295226277752020388208887731656278991943207987665816923233055103620430203139917552496304379631071417450785708666833367516582915739136*y^15 - 16393142418164414954205968613991591012702146344725500102055209678811883898314200504602866335408361735176505077930901315898138383321906121627380379337148496752729918824788881748952233/4585858572587817972454104025022480435389221501180905111008081552835550926625115967772831950663267692932220414481720812559670209985217518524285669803142834667333470066331662956544*y^14 - 53000674668853659910460276065129185610661623113968120759672298885917492225358284189921284038620164901754414361701609948711329842722290969773167612862558309970431996100507391418458247/9171717145175635944908208050044960870778443002361810222016163105671101853250231935545663901326535385864440828963441625119340419970435037048571339606285669334666940132663325913088*y^13 + 605761017475550473459284253333031645639139896665561915554889640451118809807569557848857967205922292741689746874661012063482316587086910504290522089564745819825977561090488981014173/199385155329905129237134957609673062408227021790474135261220937079806562027178955120557910898402943170966104977466122285203052608052935588012420426223601507275368263753550563328*y^12 + 3502242562479853712219539973920482623195536612598788709017345422742704378655100273283601115162762669861794155570447166211932019915749018356554135371612966363674288123804006165495365/573232321573477246556763003127810054423652687647613138876010194104443865828139495971603993832908461616527551810215101569958776248152189815535708725392854333416683758291457869568*y^11 - 1095914896813916954988013968327017988177975481403286118493183762180787424187319221786778358780230969822151294345534198115134945553756562532995846929581079307129946882166153306484773/1146464643146954493113526006255620108847305375295226277752020388208887731656278991943207987665816923233055103620430203139917552496304379631071417450785708666833367516582915739136*y^10 - 48681469652843143473032945217026346084931519602045400772276286507910238645266455846106910198172284487092011769928298993937217610081883683653487630527515546072691837279340664592843/12461572208119070577320934850604566400514188861904633453826308567487910126698684695034869431150183948185381561091632642825190788003308474250776276638975094204710516484596910208*y^9 + 52082405802370252879264665797180300915600776089262977465597919298589624704852541440858026881957916081387934981400498422839782304363692320813609954964666812154392944824971394133365/143308080393369311639190750781952513605913171911903284719002548526110966457034873992900998458227115404131887952553775392489694062038047453883927181348213583354170939572864467392*y^8 + 225891853757991844698527168407013176607950099949866449293950973517708317303402970977105672441027325529324972593424610840253887485776956848943398033556076453989436399759604748736389/143308080393369311639190750781952513605913171911903284719002548526110966457034873992900998458227115404131887952553775392489694062038047453883927181348213583354170939572864467392*y^7 - 21832319276718335632039104860527592641604965538547758370362340355106104203472601301225970342649416018898992109163404972621713900344332476441733910861572926802306105853790732687249/71654040196684655819595375390976256802956585955951642359501274263055483228517436996450499229113557702065943976276887696244847031019023726941963590674106791677085469786432233696*y^6 - 3501836610866259410724884030999802381893328672694977925559407372927806482380612460444053102993673103273550576261513992517770543515203864555174698562504513596354921437614831380125/8956755024585581977449421923872032100369573244493955294937659282881935403564679624556312403639194712758242997034610962030605878877377965867745448834263348959635683723304029212*y^5 + 105348715507625613534487707023768656718145263133966852241849018779381935759053704996773516558612824549630856241754079711621346479488256886647932006741409758893045081149566281954/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303*y^4 + 10646744847171821645393559024335663599737234733724125022891382281532771058906582708369903610123273398630439248689961795246618878316672224767542382661368982639033005381629410733/194712065751860477770639607040696350008034200967259897716036071366998595729666948359919834861721624190396586892056760044143606062551694910168379322483985846948601820071826722*y^3 + 30227767963405368959724867546506544171239151908393394601094289471748392624170895789826410420225975234873987916451039532097845534766646718498093624664468685792509057499867964769/4478377512292790988724710961936016050184786622246977647468829641440967701782339812278156201819597356379121498517305481015302939438688982933872724417131674479817841861652014606*y^2 - 9043080766868121132159492614473240334700549159010262868508885503014142863015547351016601413242802268739875180136785276923771574391913822955498681467560774011024042929376436063/4478377512292790988724710961936016050184786622246977647468829641440967701782339812278156201819597356379121498517305481015302939438688982933872724417131674479817841861652014606*y - 484272431788501943437257030753814135127016028127338280301503705734661944538656109345347866868286031206228860676277034973028066116534511922460821156734332598902588559535784286/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303

521688470074345999629916111281448992626638625040979404534696230600005102900368853586163930719442754759197592632417720839422764756313483189951150358719916985227051792800032183/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^38 - 1708275401176819774456813909274910875167874688842705681238493534684611927565968218276696961928876240663091153430884200074469914352120934357466271339468409904051198652799801193/679672512653015547917408259708594995055581460385548883820987244883416389967175082381489198582513780173533299325290832008843753227282764850757286640297380127537423774041576993980416*y^37 + 8750491508181008737938853032498828070280352795884030601335706227689248011479116753165869771555949026268583862785559167987044143403535533446209878830272063321540885430108246251/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^36 + 284178603397199336723259078159372344118016597437127397152252993815325898133870671425007990578013833862465050807897365354106486404967767993896768098665319391525026355881419263567/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^35 - 6070233516925434067350279651373315901478345770506227126256175145869625678894473151425859880571732793936144594069718745957213159791810782607957468611943017576046388494881008977/13274853762754209920261880072433495997179325398155251637128657126629226366546388327763460909814722269014322252447086562672729555220366500991353254693308205615965308086749550663680*y^34 - 217109789665686650651527974398426304722132410704128324658039132810902099142661502005869691022986523157907199749591472778168806068928917608527490064389899520458671416094490381537/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^33 + 232733735053003870103164295635020578219328080573747521661671356945091635002083555132448766341906982387184809142141873352944835587515992220503402547944511030471459682046354339351/36938723513750844995511318462423641035629427194866787164184089395837847280824732738124412966440966313778983658983197391784986588439280698410722100016161963453120857284868314890240*y^32 - 60932733341172538400701131773477030453429543918031952913396928358525203733576759571612378575050489009647076909507435429073483064662842199430818072458751429412216390108315754266309/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^31 - 55311818382719402540685975460336700381600735832432637127680995987016715178229487903802734897927658552008359939705180903503779839823518728115393717111618384969803247865508071933067/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^30 + 533570353891001734255419539520166856807024325616411806384501063233346645634652111858344842554247307136715572188991505444256674394917416852157354632585342123298849660650391139089961/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^29 - 647971014829713316960054191482058399099747016325538014860577768878576599386088762620832577137504092129261994793642825964084894712138318833045590750426685231644047883091913494799007/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^28 - 1430850821866654605772908398273017547017988487573152955588324062110901222720861304351785066820345658463181973667729467211232419764365609131655044634869545978751006447940498406178569/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^27 + 3673349095108892493100321414729080690852126299948758970040068295848148031458724310102372110294885848321216620603777239660615299686948922350501119967129084814371085515301857491288029/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^26 + 1558141231608959766488438364933272235055883190676444759383482111352511409486771218102619266495896341416374245720502655174210732762172094314732135216786336767647405497770176809819299/1699181281632538869793520649271487487638953650963872209552468112208540974917937705953722996456284450433833248313227080022109383068206912126893216600743450318843559435103942484951040*y^25 - 3842380901827817586618885895298885174176614663197741736019540935029435868357257996275409894739896342238236870406726536274583611039834979165904835646895019018346451442154478334646873/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^24 - 15030720380926876372062123985244260889199751800306688569900393952759513077295989926254654384418666801633944538767979697367489801886983772355876531517338375230743762916944033231953347/1699181281632538869793520649271487487638953650963872209552468112208540974917937705953722996456284450433833248313227080022109383068206912126893216600743450318843559435103942484951040*y^23 + 37052675992284520586307037813965646816156958457211699919588352415865331547716674500600402173765189328458005404578548065045179851678588445936449782577318821004621323358395687161733581/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^22 + 183376764929844841516092367438420083367724662646919853674667231110829969226126129261347022106704140375864896191416926504327922693023835978399773770713735993488462533438585617444266563/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^21 - 25183778242544646069837922558149693760390030081031220693751614392132620255186843675016280069335687204942376185874212212222609239038009645200941638044511200752186959992091113634545033/308942051205916158144276481685724997752537027447976765373176020401552904530534128355222362992051718260696954238768560004019887830583074932162403018316990967062465351837080451809280*y^20 - 628177961931742121702923908391007591590674808610963754305557289178159808961627704785682166440195550409084329739995967309554608135582967575579195092595335127882054152536347576216778847/3398362563265077739587041298542974975277907301927744419104936224417081949835875411907445992912568900867666496626454160044218766136413824253786433201486900637687118870207884969902080*y^19 + 463799816547357880978461525739215660019378563272903285381745267014324821263348734102810714360004018735504106336660340395929796990027486926991779618463086181525765152507595648374930071/1699181281632538869793520649271487487638953650963872209552468112208540974917937705953722996456284450433833248313227080022109383068206912126893216600743450318843559435103942484951040*y^18 + 113579620974210007992821145680293473694771068350244930092109855825053162927306836680237241323908745044260705349518080226076887108991616147260405518678943605258967763944033280865192437/212397660204067358724190081158935935954869206370484026194058514026067621864742213244215374557035556304229156039153385002763672883525864015861652075092931289855444929387992810618880*y^17 - 332053279964068981615009451268958966201967196503476681669229819649971521022680735779867058320585641626227671766640538387256044180204276339597747816682040248081191578166061954797955839/424795320408134717448380162317871871909738412740968052388117028052135243729484426488430749114071112608458312078306770005527345767051728031723304150185862579710889858775985621237760*y^16 - 62116834409962224926847029902478766479128463254130025001701740308032876710291579735951366817939422614588267596197836044319909139128215177424458225256858962504231858139090784252488967/42479532040813471744838016231787187190973841274096805238811702805213524372948442648843074911407111260845831207830677000552734576705172803172330415018586257971088985877598562123776*y^15 + 152185747681342797026886717758146003607744784773068212993219251595340478314872148682317183902916150932360528683868947492266077919153663860831341593964985785712152634657227821441381859/106198830102033679362095040579467967977434603185242013097029257013033810932371106622107687278517778152114578019576692501381836441762932007930826037546465644927722464693996405309440*y^14 + 27811190502760288025677964465000971890172754374631890688281218750205196280740171430256497059373811703359773743081626216928891661150465981711074233648201438247351615505501293410642009/10619883010203367936209504057946796797743460318524201309702925701303381093237110662210768727851777815211457801957669250138183644176293200793082603754646564492772246469399640530944*y^13 - 10086543500565327077839678422125061359020199500373985566006494705241404995005642513941942398902719684555939888850817056228422218720674074328151204971942641278688617992719713466339/9018243045349327391482255483990146737214215623746774210005881200155724433795100766143655509385001541449947182368944675728756491318183764260430200199258291858672084298063553440*y^12 - 36377720921086886810163805771034641534633512305753583605309728747931291022281373910617759194862484099155406893887822263143314875297350799170190218027870361826034801148934045462899961/13274853762754209920261880072433495997179325398155251637128657126629226366546388327763460909814722269014322252447086562672729555220366500991353254693308205615965308086749550663680*y^11 + 1490686636397889920434929279442782174767317019864153386125710020026972008591816800008227481386991351627961958321434830019491292167374017588138775221479794885462058769219801145453181/6637426881377104960130940036216747998589662699077625818564328563314613183273194163881730454907361134507161126223543281336364777610183250495676627346654102807982654043374775331840*y^10 + 124599554263561631708290749729043058880759078806034829391069889995150363987128180242353349117794063752449476348578922515305938867396490130599530496660066056312686970161183642733297/72145944362794619131858043871921173897713724989974193680047049601245795470360806129149244075080012331599577458951557405830051930545470114083441601594066334869376674384508427520*y^9 - 14122824360007916098992792888566466246014116352492645837075092852664944945982555316637117572985630980003574573623708113223348054524658059906787244798682698609272328808600497452445/331871344068855248006547001810837399929483134953881290928216428165730659163659708194086522745368056725358056311177164066818238880509162524783831367332705140399132702168738766592*y^8 - 292889254478608094960608034195192360599306168539003302316294385483051083570094404897112415236452701097871362435010124775255877633516072112197244922790919377930930430035147101201319/414839180086069060008183752263546749911853918692351613660270535207163323954574635242608153431710070906697570388971455083522798600636453155979789209165881425498915877710923458240*y^7 + 17217735915198876752056414584521881961642630231363966746982383065243500940778525264525038373463965318463721079783382402042147649514254766956165683773441148540526219270972236266071/207419590043034530004091876131773374955926959346175806830135267603581661977287317621304076715855035453348785194485727541761399300318226577989894604582940712749457938855461729120*y^6 + 38294242463326388213235756762808046466774134005384162536387975990953529279252165894689442043671758283124672976667478738335433214101999272851243548369745943906193178046989787428979/207419590043034530004091876131773374955926959346175806830135267603581661977287317621304076715855035453348785194485727541761399300318226577989894604582940712749457938855461729120*y^5 - 1075142527111798751571081608155282653106525206572054848952589979220499866139721960655628009361918086278663662604855886498604131595870876260472919474642861652942498912650002745577/103709795021517265002045938065886687477963479673087903415067633801790830988643658810652038357927517726674392597242863770880699650159113288994947302291470356374728969427730864560*y^4 - 14770282732560526871203327491287324326931396115047461379298370082485216152513115777782061355136529100284841669508940907464583177833082798179672361491133833115841608294219972779/563640190334332961967640967749384171075888476484173388125367575009732777112193797883978469336562596340621698898059042233047280707386485266276887512453643241167005268628972090*y^3 - 27419790656616922325651547892441557070668136229878716694513929834014859084219293305891812983982418868717707824928957757748257818414332360717678521568492615235525940452359999761/6481862188844829062627871129117917967372717479567993963441727112611926936790228675665752397370469857917149537327678985680043728134944580562184206393216897273420560589233179035*y^2 + 2264848819962281421226112122761230859794701943879845404885754974565296251054823124498472094036585625926948322822723580512283516110753173100308287530066796866517817167780509405/2592744875537931625051148451647167186949086991827197585376690845044770774716091470266300958948187943166859814931071594272017491253977832224873682557286758909368224235693271614*y + 8951484712156136489330202994905607062152868923560091770208165409851821302640829557819640431722073388854586558491117414725539959068573273447136048932665432170720419179670087093/6481862188844829062627871129117917967372717479567993963441727112611926936790228675665752397370469857917149537327678985680043728134944580562184206393216897273420560589233179035

44247162725644505593692182826502069228169540262232820972132651573328927946263700488256084697860768135694833563645759690060449997332581527667032190701175563835996359015733528217/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^38 - 751190127691251378696475779376340791000024438550987575121324509312130440350096491898323533824120693657660749327260668728435693224184811234223529927585301979844981537020378866939/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^37 + 1147091885496906621993397321993574751975714897279004279347766713716833643600646216224712969617736846970793782226607230615605709280082471205530088363598830560734581872983352564997/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^36 + 24153034378371107658183550957958243466536512655690106914453681971416417721834062756156989728359783982104390005223563514323282052282344781803004434235525384670541620933481564509905/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^35 - 9142386982881501130224619627348435730993739704211592814640755311210818295117953021515426430083019313399822196969392779583969069634646673602622698258731571139441102720068243415311/38667959484060481143733005138989555031201915697957391896020143653509365413302977840260519007992673186804482534909869891503139210595354116196776767780100381914955819599308582049579008*y^34 + 43190746311339779641397057995902537802948950684228658662893929790846080601120595426957713332502785570114611887418960699280663397580138279038688339809969822943475284245530969026137/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^33 + 20681824889060656384371524582727480578175550328871956453257747133008370216340801942187255588467116164306608809077363046320004158498609459743888666286335809146512712169334797860043/6724862518967040198910087850259053048904680990949111634090459765827715724052691798306177218781334467270344788679977372435328558364409411512482916135669631637383620799879753399926784*y^32 - 6149419116371743985515710156290982924944471023596414142402631245584605858891106085150411831115138012425599871891217019701553181985793416221320280841482023299233966995782852507364147/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^31 - 2809101885836702695570105489751307485311702844943073053625148983134619215852644474402913730319956680322036399503356425981162903642847246364038299429097633705120100762049752457343533/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^30 + 50364413358614554878857699837665366621177159212954532209552403892629856128029811341898666487584141510238467125615098400238845631611240496901662779749223591945603979859908520648800983/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^29 - 75461248340098305912356609646773702369238990513729632467612112401298197447862240456959782059887333675242111906540289844796639094570913476120119507282232042554625056901007147982560481/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^28 - 114528880450303034252852675871594269753400764688037652409203374873134946420038769612698309485988463437216635651294578842014307807250629812586700841329892700381600858896797687898307799/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^27 + 391387715785352204756148750182840025578808821048619806706402585767219598657698701091747295174953028939496639122411260471704726166270600309439888147094479389903678668715831333550429523/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^26 + 92752946550134545368670886489848916679895146662172884365309385995790915585289617229421266974401560185056091591311101038448286293232985770967682479745245834054683221796391912204046765/309343675872483849149864041111916440249615325583659135168161149228074923306423822722084152063941385494435860279278959132025113684762832929574214142240803055319646556794468656396632064*y^25 - 593492497271924190539838080451379466499907175931468250410137852273627849342491538201057675998499729255568109667261605065244488223227884434091238965925384246364172509575172261311113263/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^24 - 79712838702914741486050828659412449077032543884713975885510978557409597350150078087467808887179866232362055352453972170669832771695352479472472948327676790081999980007012743766273977/18196686816028461714697884771289202367624430916685831480480067601651466076848460160122597180231846205555050604663468184236771393221343113504365537778870767959979209223204038611566592*y^23 + 4538376195537846239623477804077938339260873522630423264545968483064664107771113703220049572290237707177504904977430155451028012920809053710617956056118882453032186949181790196522264011/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^22 + 15420187252629936322640230595253556639169929194099111587548865811086758833537879349203995069754580648028215168219313000093164331329818428215309562112126041212404645153984609690156572741/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^21 - 33007248360604242867403559117138704457411600392071854759107002145879662079254194893854789953753704084546288290766452039372403595231357142205139343863281438962797630698487199737326875101/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^20 - 51445782048253710673555568746093608996734669778802026435653399858001942063123619789192484688919581851026928888962623940293859430191815186501714797852052472479666863069221686876643581297/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^19 + 56707008996838835381160625392105908816400452418040334256962337931470624999511463621059092938352432413855776097759458981616373788734857453345672365749298612751420765830133407759203462849/309343675872483849149864041111916440249615325583659135168161149228074923306423822722084152063941385494435860279278959132025113684762832929574214142240803055319646556794468656396632064*y^18 + 19142374554100519412084570577441124790775445686931477756310206529683239728592574230056110682605099957730396599781303833462229869819485483867894130860007159169086395097941325938720484451/77335918968120962287466010277979110062403831395914783792040287307018730826605955680521038015985346373608965069819739783006278421190708232393553535560200763829911639198617164099158016*y^17 - 40384106303146230587474431278708912161372945716857980970083447144961053397641873688331491062912588462872134197213730215987274733512302302185567479912164774759175829601709463667301579437/77335918968120962287466010277979110062403831395914783792040287307018730826605955680521038015985346373608965069819739783006278421190708232393553535560200763829911639198617164099158016*y^16 - 26058123807541130538067127129585328608657136704865880985268252543128745031619101268281753663499763946904489293139988124556569702512752393598928584741745323475543909706944700978193826167/38667959484060481143733005138989555031201915697957391896020143653509365413302977840260519007992673186804482534909869891503139210595354116196776767780100381914955819599308582049579008*y^15 + 5338919980793553821361890151368769895968259071521473250133641863166600761509947225306488877876622158420743883781583397518239111318514440112662989042964615820185560015764685247580116173/4833494935507560142966625642373694378900239462244673987002517956688670676662872230032564875999084148350560316863733736437892401324419264524597095972512547739369477449913572756197376*y^14 + 1698415501209766906562036300625355972012002250719252840435398479246324486981708738018523497954269547059779830816102276936470047268285004202436555061574767801060605477242095845049980921/1208373733876890035741656410593423594725059865561168496750629489172167669165718057508141218999771037087640079215933434109473100331104816131149273993128136934842369362478393189049344*y^13 - 113053097883498835851080301930832796270359200967772435671792951066744499872587918237522564292722680476349535599425516207196452100115427734332326892598234385493451337397519479158642681/105075976858860003107970122660297703889135640483579869282663433841058058188323309348534019043458351051099137323124646444302008724443897054882545564619837994334119074998121146873856*y^12 - 534717851830515060957027829669841773520361200415390781309399486843469294490202599712177694109738269409546741879002572146811329800561983827663418676136462784211588028783332153245894693/302093433469222508935414102648355898681264966390292124187657372293041917291429514377035304749942759271910019803983358527368275082776204032787318498282034233710592340619598297262336*y^11 + 24026136901631104522621829540203345433885477683142024547291084046591795147678785048373472559109585524487476486459645980124670226384672852723840158202734216221542339161061325865774451/71080807875111178573038612387848446748532933268304029220625264068951039362689297500478895235280649240449416424466672594674888254770871537126427881948713937343668786028140775826432*y^10 + 15617693099025974626141225288034376265345348174970346815725023232152332132197178655969896522274677337458157877644188209228657068984143041429989260167799655790742914149152240397047667/13134497107357500388496265332537212986141955060447483660332929230132257273540413668566752380432293881387392165390580805537751090555487131860318195577479749291764884374765143359232*y^9 - 4398380978064286424916726764746149549695233408469408458263557690757093483241919195720281293023126276598452996136551242403805819228452472234943991909410343029480780336910513077454647/75523358367305627233853525662088974670316241597573031046914343073260479322857378594258826187485689817977504950995839631842068770694051008196829624570508558427648085154899574315584*y^8 - 72610208947026980452956214412406725721462366548230994062788515798752318844533301402206545125118137081984719474614082130865341252532603753647953133465816455028083932941534220118356335/151046716734611254467707051324177949340632483195146062093828686146520958645714757188517652374971379635955009901991679263684137541388102016393659249141017116855296170309799148631168*y^7 + 3885503973703860496953066714825879862960427651066709493591095432759180689826388426434257904809043426270803247727562081931911776721653431974462555862502594504837468517992485223638935/75523358367305627233853525662088974670316241597573031046914343073260479322857378594258826187485689817977504950995839631842068770694051008196829624570508558427648085154899574315584*y^6 + 2653196528297185863595471139686079435160005167236827953152679445412430975329341633694634602304228545874991161490555269079718064014243211199672947282450825233581510181831705606236731/18880839591826406808463381415522243667579060399393257761728585768315119830714344648564706546871422454494376237748959907960517192673512752049207406142627139606912021288724893578896*y^5 - 3430480905116959814117949540756724521873735942455613173354703497439766353532036838743715157843448364082614674679189004343109054087394712924414770829717380910482793460276536101125/1180052474489150425528961338470140229223691274962078610108036610519694989419646540535294159179463903405898514859309994247532324542094547003075462883914196225432001330545305848681*y^4 - 2420167852098786290531527109983713826477018992029710594410144766023479888628094470764654620176573231383287463520872665958020111652429660892721701742488254813214908237480195657581/102613258651230471785127072910446976454234023909745966096351009610408259949534481785677752972127295948339001292113912543263680394964743217658735902949060541341913159177852682494*y^3 - 20831437293643104027509461620645836714812392302441033270660378861451990343577814389360109752841755493477573745751545149792840147456217141995853944344253745503776139297375136130663/4720209897956601702115845353880560916894765099848314440432146442078779957678586162141176636717855613623594059437239976990129298168378188012301851535656784901728005322181223394724*y^2 + 50042995456654628255656183620299140367432139138187378438898960512735889011359435461246888223953647277547064364434624372925601982617909825471371794412363413781327743397326360073/69414851440538260325233019910008248777864192644828153535766859442334999377626267090311421128203759023876383227018234955737195561299679235475027228465540954437176548855606226393*y + 1743151428250661285381716182691947951016007325200625656793938807028448302763440962526308023340083398975213737280029785623626959151229998483182128723146737220033149422125349225944/1180052474489150425528961338470140229223691274962078610108036610519694989419646540535294159179463903405898514859309994247532324542094547003075462883914196225432001330545305848681

34453917226758605176981458637437934681931607468763901667141174343972396458324444371123755207271387615380887844850504852970390246912460337429051086768379474471229958730649921623/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^38 - 110376410934798043250353566908950830676248622275814642563605995090937136061973582703309348031803053723801807986340859664345588273936631161570206704543284179545390700645622988509/12913777740407295410430756934463304906056047747325428792598757652784911409376326565248294773067761823297132687180525808168031311318372532164388446165650222423211051706789962885627904*y^37 + 371267480638054240990360501218605083763542057667987019762735538831292138212635972146049594793000691402355031967736539335949201835022760670244113058451435609378339321516267912631/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^36 + 19081926126423228560527264964179997141549878162053701336409011778453664453825238832388109549943213481090234548688541042405570424233648558402228861063270245488804047966593207805347/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^35 - 24024406387871398157597881417947570039422453045006681153165661715737448921586991274514579259313044225928237917563900161125514567095059883683374857337573127673314301485327916437463/16142222175509119263038446168079131132570059684156785990748447065981139261720408206560368466334702279121415858975657260210039139147965665205485557707062778029013814633487453607034880*y^34 - 54287484364802454761182682890116067186161796101083152213969860957671732422064237963352385807780216657951654039284483484191626742864110860473228193955916814403787118589639942910937/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^33 + 7766268020766421972514400093950321789356230779651446377082091066414755336939627768962897771738262474244273379774804024719825285825888993204583728050405128266566707397644964157123/350917873380633027457357525393024589838479558351234478059748849260459549167834961012181923181189179980900344760340375221957372590173166634901859950153538652804648144206248991457280*y^32 - 3523008562119184800321965110672630324666917663384587058234245894133626156485236750632941247083575624996399686444601726561584749386815688935033720865254729746648817265380287463904309/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^31 - 5344835737786628528203597006978670220370532904820067760307610486305121035022737395762728783388493607174786715136106103467580086680883067799362611186912183193683680795596498871790487/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^30 + 34740739387200606352637250533294976032417390506210355263107764973684111076906164564133109172144329089132374039802495626909452378845742147447047365806320735784865403627199569503694301/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^29 - 29757320664890212931011247392397311041777255072492001160355798885320520228104604156109925478794697525363704170437479255715029415822745728571957011817737570719759479715346257576572147/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^28 - 116229655386713993374812743333958151452471641630485679880017562865458005892832530966705057910940315526370461041073686289113982604636231816122112667553574877464587395993552214022383629/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^27 + 218106038772352721385550397828845180361466549867346388050766497055655469693450269682094114126527404951028068298342543881541426205454436346262927488958863867681363461764497010517440209/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^26 + 153514731577345162187162086498480358611155060506407822977002801165119261474502785012472246002295960642133366592473811955670130138692602130508536105554322282669306392940915905642644569/32284444351018238526076892336158262265140119368313571981496894131962278523440816413120736932669404558242831717951314520420078278295931330410971115414125556058027629266974907214069760*y^25 - 225971244961778175135591925157539144468005658696796236125270085053912855919476735669318922036665087497397993846034831053060569907504985572051051294443873736002049980534076413062695513/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^24 - 1052840202961455023186039914016885752969085453581131852319050361983285906443687312912986237527204622247338133062633870326265226775568589185565682008085305420631907528765261750662040537/32284444351018238526076892336158262265140119368313571981496894131962278523440816413120736932669404558242831717951314520420078278295931330410971115414125556058027629266974907214069760*y^23 + 1780704185128791107081575513723546049832662524102933022099059625040958825487954175809635885712661918406643994499445147552511606187029245384113107566046395223425608935257520523829292421/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^22 + 13344529101778372664449143118584503451766323239231009864975713236028746597678823559077041465034150396733073160106158763667051521449739219999358844847150306156452553635471015704845745343/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^21 - 1317932575487784328021094029742911423339155562021292326787949942128278791634743346464723633183992147837518676902222360672334064594089246266226027480231238107800371511039426412826797013/5869898972912407004741253152028774957298203521511558542090344387629505186080148438749224896848982646953242130536602640076377868781078423711085657348022828374186841684904528584376320*y^20 - 50131251324342442919006245699045189799517502481294770437943292968425494561694185909494914006072316563039360538929864233850036278842978045929446620396866776528560045931060539085646720627/64568888702036477052153784672316524530280238736627143962993788263924557046881632826241473865338809116485663435902629040840156556591862660821942230828251112116055258533949814428139520*y^19 + 25054822228378309366605866459231857459386869101975631350034944288270344378495494602616343247460868547319399889595418346500631879481927953477900251358845778539774634568277405897024991501/32284444351018238526076892336158262265140119368313571981496894131962278523440816413120736932669404558242831717951314520420078278295931330410971115414125556058027629266974907214069760*y^18 + 4645331282185416456427487409644536926023996260231528971012520090403551259930128516095755213457506883266226822873768885865520439951330411037916290495889894848038346298501588594998095331/2017777771938639907879805771009891391571257460519598248843555883247642407715051025820046058291837784890176982371957157526254892393495708150685694713382847253626726829185931700879360*y^17 - 4506864734709923845004977111848109291562483830036192950259402342959017390224035714058970488176711989454575279891940029428698972923356633005237909942960136718020169870292137116319887961/2017777771938639907879805771009891391571257460519598248843555883247642407715051025820046058291837784890176982371957157526254892393495708150685694713382847253626726829185931700879360*y^16 - 160175026680073945722094639200125465120038616024941711453016445440938416599866554140341598672215456242125372951081283986128129871366932655157998672545954110728953431261887249380208699/25222222149232998848497572137623642394640718256494978110544448540595530096438137822750575728647972311127212279649464469078186154918696351883571183917285590670334085364824146260992*y^15 + 7424269202672604057865191714108429648980285746553841731691627678931848874134305407124179397395245150985295032137539864263513110985112267697457349003908744068406929021683178923321876729/2017777771938639907879805771009891391571257460519598248843555883247642407715051025820046058291837784890176982371957157526254892393495708150685694713382847253626726829185931700879360*y^14 + 589983117562708645415139996449701877330190263486016375349214850916592534705253794884090419267792189645515570067281492306380899692422428982221499955846524634730119570914343879141609591/50444444298465997696995144275247284789281436512989956221088897081191060192876275645501151457295944622254424559298928938156372309837392703767142367834571181340668170729648292521984*y^13 - 34054698736448007461857439109563450008897156534124416639284288255733642295609160802704547572852839440069428533772670962663561527821093407712726814402542727820929706411440868646344447/21932367086289564216084845337064036864904972396952154878734303078778721822989685063261370198824323748806271547521273451372335786885822914681366246884596165800290509012890561966080*y^12 - 3098733381072791596336983973628571241224192828624230321646545791742088006563773352255573640279885204995731689748257645531209187644230717086548057089272095564319352585159826803101921181/252222221492329988484975721376236423946407182564949781105444485405955300964381378227505757286479723111272122796494644690781861549186963518835711839172855906703340853648241462609920*y^11 - 243765849386916136464310006324041584031514617592740831349584193814514833396407230515123320332775431708719175650441818446174148243094988051835643618759856254070181342810389488178457919/126111110746164994242487860688118211973203591282474890552722242702977650482190689113752878643239861555636061398247322345390930774593481759417855919586427953351670426824120731304960*y^10 + 10429897379160329435334151505112811234586942600572473134528011780723040603258627402912642300340623757197315759479983688553853950057727664423376216985846576984186190719141712921028347/1370772942893097763505302833566502304056560774809509679920893942423670113936855316453835637426520234300391971720079590710770986680363932167585390430287260362518156813305660122880*y^9 + 5610268752847166051343743894282083998160623710361949311288857628493201662011992612098117014891231726115071094713259779907072811200669892511009621467758062257088876567760917534418135/3152777768654124856062196517202955299330089782061872263818056067574441262054767227843821966080996538890901534956183058634773269364837043985446397989660698833791760670603018282624*y^8 - 51829047678246655009734709416712743569723660704687454653215427427313889386094329801816229101600695996337148497580497495618341001254894512516857140254700558668830123103553460529466363/15763888843270624280310982586014776496650448910309361319090280337872206310273836139219109830404982694454507674780915293173866346824185219927231989948303494168958803353015091413120*y^7 - 876106998444387889689212854025799460278103882954410720852665235694803013650712891521428419108289179955982924827394024872940693232714042199150711619850574649190089731789369172601137/1970486105408828035038872823251847062081306113788670164886285042234025788784229517402388728800622836806813459347614411646733293353023152490903998743537936771119850419126886426640*y^6 + 510907150071413278818207937528329112789055207938618316104710006594601480049795844449421562730246329209965453318969567646204313435827023296117128083671091572664864596873565546047993/492621526352207008759718205812961765520326528447167541221571260558506447196057379350597182200155709201703364836903602911683323338255788122725999685884484192779962604781721606660*y^5 + 228252416714919934592801012223598995701802143574538669475960190381865735458563155489625919132351222693928744297203395907316376964222288806949931289245046141620698868786006397145663/1970486105408828035038872823251847062081306113788670164886285042234025788784229517402388728800622836806813459347614411646733293353023152490903998743537936771119850419126886426640*y^4 - 7033822522606708499719884938047783678562989918272821368811274755616279017580965838344233730035922139839417160712287601841173741072282653055135831163433285307383707421195844042231/42836654465409305109540713548953197001767524212797177497527935700739691060526728639182363669578757321887249116252487209711593333761372880237043450946476886328692400415801878840*y^3 - 8907525359249975158520715201139176581919053581775928050010974248745159225921364126762694239292410986130398316042339346634219759921832366475440476126311870658800206033165817752597/246310763176103504379859102906480882760163264223583770610785630279253223598028689675298591100077854600851682418451801455841661669127894061362999842942242096389981302390860803330*y^2 + 94659731955851821087816011578642987588055510496135684221080251514725147387535237217915736360949734156154628373465178305176241062509281562709302725764417590205882881530540790235/24631076317610350437985910290648088276016326422358377061078563027925322359802868967529859110007785460085168241845180145584166166912789406136299984294224209638998130239086080333*y + 473123021905028901656348806694683267461129047713860598154052868158733064404885301549115404577237117945252098259304484898724816184237785722077200117758858338606025567807695209038/123155381588051752189929551453240441380081632111791885305392815139626611799014344837649295550038927300425841209225900727920830834563947030681499921471121048194990651195430401665

-418703432026841045781109799046057057973546372146019940817836216864710672034843158625923569563800961742500810338422628295369501579760170313231312287437147453526903629406335325163/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^38 + 6926000132524495618111543462410286282430235971676427320354725519584361735174346663133573265668542560010225220619579247049535696675229087249881290197703543354562840685596946248129/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^37 - 8152807777943794520020238244802308204716439466900440117622805511454300748935095346137164848039391876657302368986188162349406807412552855721549612072437406077263702175726820172255/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^36 - 227365050427795600537696015691274364076636674547089259254280644584840899976204678529228732163213535363763241600298511700867844258684589015587249974448179910964927351433217063781331/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^35 + 80393078049611609568357986368436372893902624245182431961118887256163218343811579083135219381635530201182181212236307568252667753374447101574351395536412564521713208664463014061023/38667959484060481143733005138989555031201915697957391896020143653509365413302977840260519007992673186804482534909869891503139210595354116196776767780100381914955819599308582049579008*y^34 - 21100948410456416425915054622280880507107858689521258054160297230001200190963702558900901808741681988888025332942438582534638337296071180815815631636137612885769335658140949467739/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^33 - 188051697608142044002719848755975738267417075949269246323342573746483313825108321596738488237547118189937489926097987351293866832336734405221320983831699642420720615311966856478025/6724862518967040198910087850259053048904680990949111634090459765827715724052691798306177218781334467270344788679977372435328558364409411512482916135669631637383620799879753399926784*y^32 + 51809456687853654229261031545907365030169683061213535648481096739787674995977917083471935483938886865705639613280786417797447239681172165751997426774181087032591883391748956451281049/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^31 + 37273502348782091194492933003013192594198285402407618953721770465665122309819986145551796681617854328393828239409940026018085488555702095980880535007024770308860240941914848165673127/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^30 - 439182475821791692457413248246600445978070841199685865700737848274408281182678392268958048920581980316676500069910303398800935296193864903646571777396394098011950247321311286918856597/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^29 + 590098535316698320121693734056348583953181652657969050593875789391392659438871013528576978048574162918238188224680103802574217702785692235602439253044075016296443825282308841644276355/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^28 + 1088683212883403439498787270044074006865859684355095482337104268414017397597524604764517027652774910535282305331922701899786208581140193770142680036404418739433882170281526059650556485/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^27 - 3180741046354767963310209013533559808672944210072260681477566266753858167575371023564995556680080356986345720254318221583794310575082178953622409782262785231862047872689519271933182265/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^26 - 1033896945528077917875686211848419400218108960728253101556018073561185000271409213830365841674081746398317130253066028761230329759053569315482388096304169156240836312590168753811725575/309343675872483849149864041111916440249615325583659135168161149228074923306423822722084152063941385494435860279278959132025113684762832929574214142240803055319646556794468656396632064*y^25 + 3696564551340555713397717095505288526411067444295562957747086005469149622713292063500921018421230044424783609289355488591105231014510681545859434300444738044420539682134423400004956253/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^24 + 698327270601053435007286692864046506553082185872106064171858013071966443495766571662976209222622885862975965729115773524415982727741739396653178116181932822376599305775356364413055243/18196686816028461714697884771289202367624430916685831480480067601651466076848460160122597180231846205555050604663468184236771393221343113504365537778870767959979209223204038611566592*y^23 - 33962326888151806487750448442355637863207648695312973935616317007203058635106227455707721066284453369907434999288497797010561537936829787507260046661907730350035499439893462713909786529/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^22 - 143774303765164307814346166623008437689332989981925523612013398505839200833957838618589102497537529849242525980674021433307679793775798236704909440421069799781904722052462554411361459983/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^21 + 249314030570607073040062612510955471454441320862055442632834108279332245253784362109994187215637672802769551912799393962980897097204028924362025678759675111667724940794173277864770004423/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^20 + 475934399714810319145550797627599840209902712541982977793674087735473274954207353008276904531211477498219637774974806514429345959848321933711119588402038820836947145927986935614869718291/618687351744967698299728082223832880499230651167318270336322298456149846612847645444168304127882770988871720558557918264050227369525665859148428284481606110639293113588937312793264128*y^19 - 422396146584595349523503913746982526563228657781893927508169387066264376798633380163303483758710266725362857045849200579159150755692681335780750760353363809959793156965673993403420815875/309343675872483849149864041111916440249615325583659135168161149228074923306423822722084152063941385494435860279278959132025113684762832929574214142240803055319646556794468656396632064*y^18 - 170370930673652620481691020910478789597421977710926638644064865121829669527599300541526211901638631391734855061711237447778365913031187713804803008218680574080968103576695713455637269359/77335918968120962287466010277979110062403831395914783792040287307018730826605955680521038015985346373608965069819739783006278421190708232393553535560200763829911639198617164099158016*y^17 + 303177647154397733052891195647678303591663904624700015787306370449800061596469890684384097728948120212712985618966176960285347089513876596614310200541974525487025363154024739735077980177/77335918968120962287466010277979110062403831395914783792040287307018730826605955680521038015985346373608965069819739783006278421190708232393553535560200763829911639198617164099158016*y^16 + 232213753759542792754475109138225490490216453875176744417194524210595742015942356688909212219571157513534939454153524825157139818615937315398024798855285380464698253258587236191190327847/38667959484060481143733005138989555031201915697957391896020143653509365413302977840260519007992673186804482534909869891503139210595354116196776767780100381914955819599308582049579008*y^15 - 147348826985098149386227564028562370366245140690782228881268262492761890042048452977189996894938368416003832519992973051267363537756592763009494917987538777751778845791819711828483042805/19333979742030240571866502569494777515600957848978695948010071826754682706651488920130259503996336593402241267454934945751569605297677058098388383890050190957477909799654291024789504*y^14 - 13123968862592598040503623073344501896545211018005678792356994584775483643210976709494387216997761102354157675961603316546797558480116900363042774694659470220970005033163987259154811397/1208373733876890035741656410593423594725059865561168496750629489172167669165718057508141218999771037087640079215933434109473100331104816131149273993128136934842369362478393189049344*y^13 + 381029306163328320381390943457559051734207758459132718141799668201240775557462306580699975139675553364012782793294165723035941345936613506262729744558621852604934764622682053888792419/52537988429430001553985061330148851944567820241789934641331716920529029094161654674267009521729175525549568661562323222151004362221948527441272782309918997167059537499060573436928*y^12 + 898921676464083981189247079634433152575628196638942089893927450558587738963143853646705885174644928749639216205566881803443005010912683130711709818301004935203198571388326634762305155/75523358367305627233853525662088974670316241597573031046914343073260479322857378594258826187485689817977504950995839631842068770694051008196829624570508558427648085154899574315584*y^11 - 114957853184873269024783837467807784608137202917830724154142850528035571150402759916064335905807564070730032063332116218543752985573004826703700717980915478758548040184620336136758959/35540403937555589286519306193924223374266466634152014610312632034475519681344648750239447617640324620224708212233336297337444127385435768563213940974356968671834393014070387913216*y^10 - 211927174465673671037979084115165520019258720074429577010537771725429170330533324117977468158901764728151514323539892814289228294415052604641857625517209225331664055310089421961829289/26268994214715000776992530665074425972283910120894967320665858460264514547080827337133504760864587762774784330781161611075502181110974263720636391154959498583529768749530286718464*y^9 + 217211787703470338790764836557427850955946756012011608290916481938297668115656268367298849533053858810447475635434792614874235732556680049874931227707320909316440855511389748951820059/151046716734611254467707051324177949340632483195146062093828686146520958645714757188517652374971379635955009901991679263684137541388102016393659249141017116855296170309799148631168*y^8 + 513598071645197001925124498394423981214266556343431579393970958545638968209912777019156709671587885683625469272597497729532630439925100753053491992342877758170161478384930256617356547/151046716734611254467707051324177949340632483195146062093828686146520958645714757188517652374971379635955009901991679263684137541388102016393659249141017116855296170309799148631168*y^7 - 33495966114361075564025627017420827089865039947169725800035112915508630820288493837558392849093010588102383127774902018277708775742445696581626679593292113114583261201545412973111197/37761679183652813616926762831044487335158120798786515523457171536630239661428689297129413093742844908988752475497919815921034385347025504098414812285254279213824042577449787157792*y^6 - 32376250775914822612590986704579040701722821368696246585368624089207974505244582692789885901390682353374481470764748322157866941463448406679488137880344481222145217719242373044969027/37761679183652813616926762831044487335158120798786515523457171536630239661428689297129413093742844908988752475497919815921034385347025504098414812285254279213824042577449787157792*y^5 + 3574200843959796449729319043251447054656959918618351344553440946921036263884842443012874826771633305749415725363487710251453212340417884260951799087178333601287756286282443799079875/18880839591826406808463381415522243667579060399393257761728585768315119830714344648564706546871422454494376237748959907960517192673512752049207406142627139606912021288724893578896*y^4 + 52837041737569443265224483183171886887514001224789103685734697441814818914082028056764072899921734711091488543507681764282720016487493621222646552445789561656607414114845721768725/410453034604921887140508291641787905816936095638983864385404038441633039798137927142711011888509183793356005168455650173054721579858972870634943611796242165367652636711410729976*y^3 + 9605759921431425963756267135835506597550094884224401085094031602554926345800611582272572382415107750824504924529488859173088056699342659725700893611658251807417882601690596887173/4720209897956601702115845353880560916894765099848314440432146442078779957678586162141176636717855613623594059437239976990129298168378188012301851535656784901728005322181223394724*y^2 - 489400028101676308120407612625821177060637524503803484604580021629661767960242356697769483157122807889643299460989356381617615485911722594769792312079518135108342362251653887275/69414851440538260325233019910008248777864192644828153535766859442334999377626267090311421128203759023876383227018234955737195561299679235475027228465540954437176548855606226393*y - 1407878201979349263702922245782974244502353069397988260970999754106480126012422772292207301857418296423656268803974891848087360694928313012361386648603094616965968464735731557431/1180052474489150425528961338470140229223691274962078610108036610519694989419646540535294159179463903405898514859309994247532324542094547003075462883914196225432001330545305848681

242136215894250971718628515376907067563508014063669140150751852867330972269328054672673933434143015603114430338138517486514033058267255961230410578367166299451294279767892143/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^38 - 3700502176333076394917087152277358123561907072287484215705216552896605281613119814923996579402817234938688439590638432667003798605143594937370578666147758033740166983313044481/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^37 - 305163934772752817641455707668330531633454711087822854943989285429059920746266545463996778650302611233032973226833068855210596307163150374947947111246142167725090366578264445/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^36 + 137086951026125446527061651196724940170184262617480087650042941267445704498451768764644604365211663415119929906210366643817385781510498772848714486908961542078295094465248763039/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^35 - 72303405883649048504011258533704679984434449986712140662632040508840362347417684078870528537958569793145219666644638293918002597549499126738518520578588992069688227864017365711/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^34 - 911573019074464530043749634854052962477138715158850803312628331281805880735702670193935572633049800366530925701632525309174489258690532304960097411862528203329518135035613771589/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^33 + 13545277561337754031717838484537542022962505901634808457488682962111277326129599310945496941526091276846803461116127599645394550279157348660105299844835075315514912853302421159/1595081242639241033897079660877384499265816174323793082089767496638452496217431640964463287187223545367728839819728978281624420864423484704099363409788812058202946110028404506624*y^32 - 17461738053177099104041372538565080847164433398319146580261460724493351102359844618827151028339755912721612928694991253499259137647049287188112713811445079687065675868635366475009/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^31 - 58348410871860884479192988753208560404701494105293510198482592434742112367468667648866002129035954645066453666661047624043753212345867174656642386359362859351819960939187033978311/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^30 + 225379688095555896272397909897399296411081749913966366050939214512525945347753924603508607197119107953559662344444930192342761241218348266119337921495248713271553263553779600910329/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^29 - 27415659797566504007168559338059092903344254016870880277711907331010909530287731141220175963702025876533093735588851061156455349055147404163640497556684763073777478603667923439503/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^28 - 1038289968939112630088310660566107889569176321170500956034912855368044800594378673059147218155239451085296136271343434456395959944523470887791752113406676565170402412586855131695625/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^27 + 1047844081140161810458942174175579693633648867853701721545605226146382219153139739788388361502672842700494921789217469929051234485934903752889773027894718688297763546358903181136821/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^26 + 1703972543449321972835353704672487680287705590066420194908224643012859288499280614303793721073713601221433049034468330328950009746341506838824646839829162199272601524202115868996355/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^25 - 537360876149565526691460420889857860976038497066993915565294150985769504095440068946243654212138777816341381759202042368710419586175476888055558301718447417503803451554558016123869/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^24 - 8040463649630654681248665705587220669262592079260625772849265642362439559408551906597156305300545166185874061697526790669055856035035786542934484202203130074236788868740435489171001/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^23 + 2291251976577256321258208603075094583836493635686181445861606263303148904559743926077363773394347078263360140487585081434504250086200571562483563136203493006000656271474768065482073/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^22 + 106364196933692410794352683846869157181799425111354439422157592631238059802469363391181502262974328586376861798678780848834033018812875970647093343920547870470737808885918438167321255/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^21 - 39484320309415422623064342631352166208320260833613607528131818009657988340431628031211296453602674855816337957493236025078228472553222322964869882544074980755754108595014016100910451/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^20 - 446562378359234614763426632535589556487230710054398790795513033703219322793560914890934945976120576242179238056046606508261161610816045449610457589785600164055342459019109585722076407/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^19 + 69563581600607262433741272932059252790855173641486726549742698613127342415123574994085532292516047759433800093613846259175923543931613928197847898302154842118999985512771250623174499/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^18 + 339813950303125504709116476876782266861167884050716919005149851605859953414624642698562340791652690721642627123014319133726529175929564523115409760896093228197648355173917047066790773/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^17 - 49852744376531361350924689052372736070187130312819745062584706760641618288223760159182649654292694521004025496989102554023089243049522158242718239185314586065591386642175149466803277/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^16 - 118146234880116119650925637248248022720777572689580502684341928705833979374407265526707827826928301280556068278389680590319226655630475770683957295377671240584767288332819549021459139/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^15 - 338261464342685177734420423312222052414523394913427862827372417887280184272950460083185498712228871931861613738807989184909810391142027730272975021195268265303947769318856308049963/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^14 + 108556386597375093462745649701836443952024571998228690494697160552444162630498295240354452940736630088008740559885179837028283550461359645450368685984215784968322998402473895888092383/18343434290351271889816416100089921741556886004723620444032326211342203706500463871091327802653070771728881657926883250238680839940870074097142679212571338669333880265326651826176*y^13 + 777163596037654561430638983961059794889114670559193827480927771303931732284978989972113047261050698528497343450517255314465657812137564443364940823325991962471145532667076609828267/398770310659810258474269915219346124816454043580948270522441874159613124054357910241115821796805886341932209954932244570406105216105871176024840852447203014550736527507101126656*y^12 - 26690118232282141467241424573994516967790112626371148433431639173804978733067111736384456008770315744832012536309764333545347891909050139542559185314459603721575408606864803499595659/4585858572587817972454104025022480435389221501180905111008081552835550926625115967772831950663267692932220414481720812559670209985217518524285669803142834667333470066331662956544*y^11 - 3875674310447612325935393016580731322176894410395106080756141080545176734930541030487475482691359837433871385983860865433928118404585210160645158063970655057227685306614079730464059/1146464643146954493113526006255620108847305375295226277752020388208887731656278991943207987665816923233055103620430203139917552496304379631071417450785708666833367516582915739136*y^10 + 156103727291035202459445568130472563849419161901836924818465178230175483565209675074649890399621686732190223648164096167044062224599037881399398827826099893772557298448867562913263/49846288832476282309283739402418265602056755447618533815305234269951640506794738780139477724600735792741526244366530571300763152013233897003105106555900376818842065938387640832*y^9 + 664585564056192637561803566939139679865703416638771851584940703269667211728149946888699111538626901381499586091869001123142502291795648628064573271587962780509589294840915503846893/286616160786738623278381501563905027211826343823806569438005097052221932914069747985801996916454230808263775905107550784979388124076094907767854362696427166708341879145728934784*y^8 - 374241367587244991354742109989124352827930319493015940833083098518724409900163171111124505050958044479349277532087656003479938455621157535479968795344865610220064467654531773539643/286616160786738623278381501563905027211826343823806569438005097052221932914069747985801996916454230808263775905107550784979388124076094907767854362696427166708341879145728934784*y^7 - 29452075097048891799406091213911571081072302543049034214789778798513363639170415143147711351090434234871192187809507524302796494848227617312293377909358149267966228907052973351191/35827020098342327909797687695488128401478292977975821179750637131527741614258718498225249614556778851032971988138443848122423515509511863470981795337053395838542734893216116848*y^6 + 8658454718707872563957818959997323099155017683519970535248110016087256344094926555928892132344780777705012231677612563404056078525466007964006121932316660471999145782709855598879/17913510049171163954898843847744064200739146488987910589875318565763870807129359249112624807278389425516485994069221924061211757754755931735490897668526697919271367446608058424*y^5 + 3707957187195868845387515339204522667179749765969355184526931276478371101203400768738341298015225621173110641190624623526598583074332108222042278742853526690878276433308882801877/17913510049171163954898843847744064200739146488987910589875318565763870807129359249112624807278389425516485994069221924061211757754755931735490897668526697919271367446608058424*y^4 - 27175279112937718319709452588132759595369186624496224166703407972997960465857378868122297576198503231336637429625687480549725553041556078695065361885757647539596470168828800873/389424131503720955541279214081392700016068401934519795432072142733997191459333896719839669723443248380793173784113520088287212125103389820336758644967971693897203640143653444*y^3 - 336478038308842930590211864885858351820212224849007185337577662085486963263218145977212966201858047460228771035696561012381085476683749315848099706316556933842848968461877167199/8956755024585581977449421923872032100369573244493955294937659282881935403564679624556312403639194712758242997034610962030605878877377965867745448834263348959635683723304029212*y^2 - 5065231022091269153539350385111628781733993370554427984290942841879960962908333625997236972596052469907745099192771290358590395465232236857984773329996941469025816139566458450/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303*y + 7105991039714113358410464491457983794192485046500909747302870680075495084860922913635209945769658143914959737431677137031659309925775775265655396840623443615413688691233298919/4478377512292790988724710961936016050184786622246977647468829641440967701782339812278156201819597356379121498517305481015302939438688982933872724417131674479817841861652014606

242136215894250971718628515376907067563508014063669140150751852867330972269328054672673933434143015603114430338138517486514033058267255961230410578367166299451294279767892143/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^38 - 3700502176333076394917087152277358123561907072287484215705216552896605281613119814923996579402817234938688439590638432667003798605143594937370578666147758033740166983313044481/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^37 - 305163934772752817641455707668330531633454711087822854943989285429059920746266545463996778650302611233032973226833068855210596307163150374947947111246142167725090366578264445/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^36 + 137086951026125446527061651196724940170184262617480087650042941267445704498451768764644604365211663415119929906210366643817385781510498772848714486908961542078295094465248763039/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^35 - 72303405883649048504011258533704679984434449986712140662632040508840362347417684078870528537958569793145219666644638293918002597549499126738518520578588992069688227864017365711/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^34 - 911573019074464530043749634854052962477138715158850803312628331281805880735702670193935572633049800366530925701632525309174489258690532304960097411862528203329518135035613771589/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^33 + 13545277561337754031717838484537542022962505901634808457488682962111277326129599310945496941526091276846803461116127599645394550279157348660105299844835075315514912853302421159/1595081242639241033897079660877384499265816174323793082089767496638452496217431640964463287187223545367728839819728978281624420864423484704099363409788812058202946110028404506624*y^32 - 17461738053177099104041372538565080847164433398319146580261460724493351102359844618827151028339755912721612928694991253499259137647049287188112713811445079687065675868635366475009/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^31 - 58348410871860884479192988753208560404701494105293510198482592434742112367468667648866002129035954645066453666661047624043753212345867174656642386359362859351819960939187033978311/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^30 + 225379688095555896272397909897399296411081749913966366050939214512525945347753924603508607197119107953559662344444930192342761241218348266119337921495248713271553263553779600910329/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^29 - 27415659797566504007168559338059092903344254016870880277711907331010909530287731141220175963702025876533093735588851061156455349055147404163640497556684763073777478603667923439503/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^28 - 1038289968939112630088310660566107889569176321170500956034912855368044800594378673059147218155239451085296136271343434456395959944523470887791752113406676565170402412586855131695625/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^27 + 1047844081140161810458942174175579693633648867853701721545605226146382219153139739788388361502672842700494921789217469929051234485934903752889773027894718688297763546358903181136821/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^26 + 1703972543449321972835353704672487680287705590066420194908224643012859288499280614303793721073713601221433049034468330328950009746341506838824646839829162199272601524202115868996355/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^25 - 537360876149565526691460420889857860976038497066993915565294150985769504095440068946243654212138777816341381759202042368710419586175476888055558301718447417503803451554558016123869/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^24 - 8040463649630654681248665705587220669262592079260625772849265642362439559408551906597156305300545166185874061697526790669055856035035786542934484202203130074236788868740435489171001/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^23 + 2291251976577256321258208603075094583836493635686181445861606263303148904559743926077363773394347078263360140487585081434504250086200571562483563136203493006000656271474768065482073/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^22 + 106364196933692410794352683846869157181799425111354439422157592631238059802469363391181502262974328586376861798678780848834033018812875970647093343920547870470737808885918438167321255/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^21 - 39484320309415422623064342631352166208320260833613607528131818009657988340431628031211296453602674855816337957493236025078228472553222322964869882544074980755754108595014016100910451/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^20 - 446562378359234614763426632535589556487230710054398790795513033703219322793560914890934945976120576242179238056046606508261161610816045449610457589785600164055342459019109585722076407/1173979794582481400948250630405754991459640704302311708418068877525901037216029687749844979369796529390648426107320528015275573756215684742217131469604565674837368336980905716875264*y^19 + 69563581600607262433741272932059252790855173641486726549742698613127342415123574994085532292516047759433800093613846259175923543931613928197847898302154842118999985512771250623174499/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^18 + 339813950303125504709116476876782266861167884050716919005149851605859953414624642698562340791652690721642627123014319133726529175929564523115409760896093228197648355173917047066790773/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^17 - 49852744376531361350924689052372736070187130312819745062584706760641618288223760159182649654292694521004025496989102554023089243049522158242718239185314586065591386642175149466803277/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^16 - 118146234880116119650925637248248022720777572689580502684341928705833979374407265526707827826928301280556068278389680590319226655630475770683957295377671240584767288332819549021459139/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^15 - 338261464342685177734420423312222052414523394913427862827372417887280184272950460083185498712228871931861613738807989184909810391142027730272975021195268265303947769318856308049963/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^14 + 108556386597375093462745649701836443952024571998228690494697160552444162630498295240354452940736630088008740559885179837028283550461359645450368685984215784968322998402473895888092383/18343434290351271889816416100089921741556886004723620444032326211342203706500463871091327802653070771728881657926883250238680839940870074097142679212571338669333880265326651826176*y^13 + 777163596037654561430638983961059794889114670559193827480927771303931732284978989972113047261050698528497343450517255314465657812137564443364940823325991962471145532667076609828267/398770310659810258474269915219346124816454043580948270522441874159613124054357910241115821796805886341932209954932244570406105216105871176024840852447203014550736527507101126656*y^12 - 26690118232282141467241424573994516967790112626371148433431639173804978733067111736384456008770315744832012536309764333545347891909050139542559185314459603721575408606864803499595659/4585858572587817972454104025022480435389221501180905111008081552835550926625115967772831950663267692932220414481720812559670209985217518524285669803142834667333470066331662956544*y^11 - 3875674310447612325935393016580731322176894410395106080756141080545176734930541030487475482691359837433871385983860865433928118404585210160645158063970655057227685306614079730464059/1146464643146954493113526006255620108847305375295226277752020388208887731656278991943207987665816923233055103620430203139917552496304379631071417450785708666833367516582915739136*y^10 + 156103727291035202459445568130472563849419161901836924818465178230175483565209675074649890399621686732190223648164096167044062224599037881399398827826099893772557298448867562913263/49846288832476282309283739402418265602056755447618533815305234269951640506794738780139477724600735792741526244366530571300763152013233897003105106555900376818842065938387640832*y^9 + 664585564056192637561803566939139679865703416638771851584940703269667211728149946888699111538626901381499586091869001123142502291795648628064573271587962780509589294840915503846893/286616160786738623278381501563905027211826343823806569438005097052221932914069747985801996916454230808263775905107550784979388124076094907767854362696427166708341879145728934784*y^8 - 374241367587244991354742109989124352827930319493015940833083098518724409900163171111124505050958044479349277532087656003479938455621157535479968795344865610220064467654531773539643/286616160786738623278381501563905027211826343823806569438005097052221932914069747985801996916454230808263775905107550784979388124076094907767854362696427166708341879145728934784*y^7 - 29452075097048891799406091213911571081072302543049034214789778798513363639170415143147711351090434234871192187809507524302796494848227617312293377909358149267966228907052973351191/35827020098342327909797687695488128401478292977975821179750637131527741614258718498225249614556778851032971988138443848122423515509511863470981795337053395838542734893216116848*y^6 + 8658454718707872563957818959997323099155017683519970535248110016087256344094926555928892132344780777705012231677612563404056078525466007964006121932316660471999145782709855598879/17913510049171163954898843847744064200739146488987910589875318565763870807129359249112624807278389425516485994069221924061211757754755931735490897668526697919271367446608058424*y^5 + 3707957187195868845387515339204522667179749765969355184526931276478371101203400768738341298015225621173110641190624623526598583074332108222042278742853526690878276433308882801877/17913510049171163954898843847744064200739146488987910589875318565763870807129359249112624807278389425516485994069221924061211757754755931735490897668526697919271367446608058424*y^4 - 27175279112937718319709452588132759595369186624496224166703407972997960465857378868122297576198503231336637429625687480549725553041556078695065361885757647539596470168828800873/389424131503720955541279214081392700016068401934519795432072142733997191459333896719839669723443248380793173784113520088287212125103389820336758644967971693897203640143653444*y^3 - 336478038308842930590211864885858351820212224849007185337577662085486963263218145977212966201858047460228771035696561012381085476683749315848099706316556933842848968461877167199/8956755024585581977449421923872032100369573244493955294937659282881935403564679624556312403639194712758242997034610962030605878877377965867745448834263348959635683723304029212*y^2 - 5065231022091269153539350385111628781733993370554427984290942841879960962908333625997236972596052469907745099192771290358590395465232236857984773329996941469025816139566458450/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303*y + 7105991039714113358410464491457983794192485046500909747302870680075495084860922913635209945769658143914959737431677137031659309925775775265655396840623443615413688691233298919/4478377512292790988724710961936016050184786622246977647468829641440967701782339812278156201819597356379121498517305481015302939438688982933872724417131674479817841861652014606

-873739310924211702762736315474222384100484966043838206286166959206906445863980579506528312716310709095682636514801969731273825387692159404690779341855068825707924889742797727/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^38 + 13931487142840640538531401525107854764691036773296778565621333029701641956875332615025374665277458927635630688127638894326250798654735154229765929572701730203593044510349242201/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^37 - 8352825904171715499312990117862463288565106299354828198434098200289671003218404063248829758375822299036548727235042343912682411076979046845820053735986399821730615548498624115/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^36 - 485229377241420271277539603802044121183731194477985842892833611535213808464711135049941445330961706779497746392889867044499814157662941695603253630790672861828357258056301142479/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^35 + 300330645750023945108867698156803471595920844464982860178077559960859137824039728574533696896513407238998575598967856574362128525100487621475489030564077087306163661958208237387/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^34 + 1574837625287810362181363025710763757980878545322793609421021942211374323123219826752529686900309242002489215394263073926526721137036658678487060768438870414031087683728279966669/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^33 - 197084639479466204103887022980445271521862805987279559381567869224116656180674423816007089908881363014691216218264294402726834884016146425875076849451505738225161746230127716105/1595081242639241033897079660877384499265816174323793082089767496638452496217431640964463287187223545367728839819728978281624420864423484704099363409788812058202946110028404506624*y^32 + 86758850771059704146398618100048437181423591374031949103042691549162454619779625949679709224814161735116045717391070929788678068384581714464152341318342486086938481978970913273033/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^31 + 143625995994486538322825762202410475764490962962929192128247647026531131781981631070353501345959348476433555427890045055393994420980259184860179368843083142787594597032708373096223/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^30 - 876599673967698754967745893983553073374617347845859799342633662214274242102485508274651291237109071996407206799972989481539915267063375909852787977546387782685237229990370464971833/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^29 + 689488643067891497822418110724215193365456578205118428083811676627142677594168181866346917271898498774075999396375602018741955363947276283643883227490841544876486375644386298590815/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^28 + 3044282444096921792050828824811441861381471350863906981864007911328624883886043555041962532323873842175729510345095057423041761465702964472675353164715120344580975747073794792863321/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^27 - 5390819917544035621043058031993876930060474435984509550027818321440367078051033698982863935373384034351588799145824521184768138058455692635259694569555428889449219788421545436202869/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^26 - 4130259820985029502359588785839085900886635802584763036434515320551630607235608346612247025317113181439543206093497029266162774726640263629874469794174699497895534859132203582070027/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^25 + 5507538140074594775645842266044260408100047841520717476652407219610186422477470545101678939650928875006413845409963735643409718052904629148895199887995985944871321612883256924276453/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^24 + 26921406604717772590058240012509513125505493081133523979459115874664031561868167850845189740450003919929571139026820637456414128118903633193233717613578713086197943563781413722887765/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^23 - 41734644131651296049236214275577441129870008516388817659533684059364907544426212015094218761263111685463165157930298100195615216392339942469154293207930429950586655336923484021750241/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^22 - 343678806679374562418917157383283687872397830141156767357362997924625432475264604754402909558909558582990173713880167474842949507174218097780852939266834086340439231848632360969435727/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^21 + 347191433894352980538153768704318623725862811048198812666068615788699571190983635886103652973990682848712418508825444144114475600052481099549930315918858965145944671921876464319866643/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^20 + 1309378805747462741656643357207305824525670749399738232632717867187246793011204131615306411286701038096336566060967591667461480062593842464759545008831929454975549466085974153061932951/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^19 - 604075655901414265387696904408828825747224908839272631942486995966702288390452913551790671025997853573914936612509679631384406916367132978876221855862373735642219786348131921637517059/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^18 - 973377348183909089684778321215725975480119103967791668311049537597160880746339018193077521347439287662901344554987445517593975592331016037418716625807250140126345248551095727186853327/73373737161405087559265664400359686966227544018894481776129304845368814826001855484365311210612283086915526631707533000954723359763480296388570716850285354677335521061306607304704*y^17 + 435654705785461514697020061627834887267656389281940351790256226653559065670757328828488641728304869697974688820587901378456774128138132217168607610082479388094484181734021821969609215/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^16 + 335939348651977450131710052756290319163232013644503141790967222616111641917524748347662176972971986035263413723487869264453946117403189482440685192321540230826563871199595830459716517/9171717145175635944908208050044960870778443002361810222016163105671101853250231935545663901326535385864440828963441625119340419970435037048571339606285669334666940132663325913088*y^15 - 173764172125755076764169106500057113234314650056984769789476483322412692393520169187621374283854000961185266506999012217875390531753386629229355379131679236479725185837904644903481905/9171717145175635944908208050044960870778443002361810222016163105671101853250231935545663901326535385864440828963441625119340419970435037048571339606285669334666940132663325913088*y^14 - 309602800704849443858811125199933749536734852927692937562271463793266346460721755734907889753022219975731439522985962386011526059925533728376286106248771351501624336916417218796855657/4585858572587817972454104025022480435389221501180905111008081552835550926625115967772831950663267692932220414481720812559670209985217518524285669803142834667333470066331662956544*y^13 + 606627836826654806740578596680854633620885526834520304435814848881955183596479849084721713764653844073755911485128050218937336243757373750597237509837917623435904643562730411434193/99692577664952564618567478804836531204113510895237067630610468539903281013589477560278955449201471585483052488733061142601526304026467794006210213111800753637684131876775281664*y^12 + 80966361827373944269221206620080125432505899428572212937594542316723689403952259278802438063601142785232498672558091004305913184220091551522505506282399708730793368081355975351130341/1146464643146954493113526006255620108847305375295226277752020388208887731656278991943207987665816923233055103620430203139917552496304379631071417450785708666833367516582915739136*y^11 + 3773489775256741265486508381743659641737000983137169402507865921189903501644287683440711653926211641219948732283001689460178854658966285553265103218157481396137237205789883436723245/286616160786738623278381501563905027211826343823806569438005097052221932914069747985801996916454230808263775905107550784979388124076094907767854362696427166708341879145728934784*y^10 - 542504172481450000849496811647085570889081103054550771866622786612418389176852522709923275248040888990880191219273655469304372773275507155681693473637271761672333918825392585506153/12461572208119070577320934850604566400514188861904633453826308567487910126698684695034869431150183948185381561091632642825190788003308474250776276638975094204710516484596910208*y^9 - 810350175092224950915638382183744494127994837599641781266386635863717810015033653670471340305180486275636015311598882418231147385269013610781949280857113316959036558078069518839773/71654040196684655819595375390976256802956585955951642359501274263055483228517436996450499229113557702065943976276887696244847031019023726941963590674106791677085469786432233696*y^8 + 1365741720489583875745889964736920532884393468217816562342588489626848713845999186484901135544762999060676814148150987685597953971903963218951202958901690386711195726187949156128663/71654040196684655819595375390976256802956585955951642359501274263055483228517436996450499229113557702065943976276887696244847031019023726941963590674106791677085469786432233696*y^7 + 13124148807621079026082991403180312409525443032283476049550471999496879006087967627234261904992235878231148839102106840886533974172271437047449712238775226007708468271949859524061/4478377512292790988724710961936016050184786622246977647468829641440967701782339812278156201819597356379121498517305481015302939438688982933872724417131674479817841861652014606*y^6 - 55055131752858482819432635317588095498720704954698578316192425059235283363662020510685673946827693396216445198541390540653786488016134532029003193461150452663095400950742601876375/8956755024585581977449421923872032100369573244493955294937659282881935403564679624556312403639194712758242997034610962030605878877377965867745448834263348959635683723304029212*y^5 - 2865515040018708548633273862075663870952320211272268014801741889182474088381339246489826288449540237405851273820806528480787661776496067323212860870713143532343228469697868302545/4478377512292790988724710961936016050184786622246977647468829641440967701782339812278156201819597356379121498517305481015302939438688982933872724417131674479817841861652014606*y^4 + 92690801890925419132734097020851256342214872102115882535419373000434134403276796842776866314490707106240668254579972030181665834163425742232032544981206545582135472538573898298/97356032875930238885319803520348175004017100483629948858018035683499297864833474179959917430860812095198293446028380022071803031275847455084189661241992923474300910035913361*y^3 + 406814844095367871459341918113122815626643885229350833027870265134212021092304640814385826221327316046183053496491331716566771925199230753226696685478184781737638574794135230425/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303*y^2 - 37964040620697111959805078477416667299522649070459349959437244050402885185213408669337048887554372796721969028543576011972114781741657923548492985673204366715652183251204324572/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303*y - 30560509690365435379623334003273360351678482547293448546228153479851146103456367880883946225036651579122113633783507447619546672095772853149928653461046625591882197721883562337/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303


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

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

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

# f Combinatorial flattening
{-5, 0, -5, 0, 5, 0, 0, -5}

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

# 1 Loop Invariant
-4457246995395257265385954198600182504658413159531065685577255175499844659826562923844987099327396823383384169578417514184600310786153118611138674858923490791115778797076332801/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^38 + 9312728673753067634642984525268936114973411655090379130125363198708731089332934582496417342058205508768614803009275256228853207486141876531106240722772318113750581289843278235/73373737161405087559265664400359686966227544018894481776129304845368814826001855484365311210612283086915526631707533000954723359763480296388570716850285354677335521061306607304704*y^37 - 24780365463475289167689230496409512931239796624497550516029015189490578453495587036022598275681377234057432289343614698212270288568565836373593452854101433598163828420440342731/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^36 - 150743244690791088833766088843919642758853676759880754067880458302313751137235590518929407910450505019530578374652799955488513986186316665176615641278197998546151413979520509133/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^35 + 14108655392601915493978061611546336870859516703736216696518779056279952278450893678432307275986616649359175587453566341454462313572224683414954893106859637889465406283680878631717/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^34 - 2341485888533021996677024419836818296635401756331917953586905831406482343490299604098216751347571905092563856552765086149383671966931008526529726541633456747015094929427229581945/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^33 - 8047607603597723761018453000203646130046017444409095708516797773300348422385626407936461894109891272861299407177553656635085802431217672344052741829419166451862848788458848366081/25521299882227856542353274574038151988253058789180689313436279946215239939478906255431412594995576725883661437115663652505990733830775755265589814556620992931247137760454472105984*y^32 + 581158461646373743771941025434832446784060028800156847007525352770604849862199816524539976741753922233999899634957242994373912730077322793043504263737600219823724167382410186371615/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^31 + 159970064462930146716878734708444329468949808132275391699291625748873402162210614677381595372756222020383488490420183630571958783497003644050360656302572738209967037096825994021539/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^30 - 596130484821962626167629138633567595176706461867967649306325131433425237476516130194495340607599495882372269717776165307434806324411827036847356503095090044774313820418640486564637/73373737161405087559265664400359686966227544018894481776129304845368814826001855484365311210612283086915526631707533000954723359763480296388570716850285354677335521061306607304704*y^29 + 1739412788887715564505030581065924973158083827597017439873869680800667920899154778324902331141777033155424478258206485122100573095883384976337704305007353968992010934080114509400255/146747474322810175118531328800719373932455088037788963552258609690737629652003710968730622421224566173831053263415066001909446719526960592777141433700570709354671042122613214609408*y^28 + 5460860161271473648826004735783929908987717645127071486745585248931813088793840392158100886412194401740008123641804085335488089639652472197714186766932228020309482005288408607404197/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^27 - 17871714837843897378448436630467198471038883293154231270038671201703441924025849131549150874164378412102491315326180911162801840840908786183564577396088693575130100038523241024605623/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^26 - 18456989065920202711636141403320385922084771396933991412178228833171355697920798806529480650736145727657505921972178264899130128622185289174567441973339218868280120909038194676956779/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^25 + 45020490555761872001038493207214521244897122001208123905342515827894259702126565599757298538456338350764617372243845002995887205332953507642312570530322144182753706824800807421310417/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^24 + 253589917289854303206621745767186311577499440027356566314546300941234133032553681275041743710120556776135895825562994021749639925183023719928658028661998105435744673809353234252685511/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^23 - 407039987105168125162634071086347961333116802075758329824845273514156373919011660910136775605905252177210739337005323233746956356777811049526937715950424891807890591260657110186219693/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^22 - 749039354290609041593368882031783275979277219337796324272963172659602683113787181186070440687802308030256284045616560178013457141528977756789534002270755347796715029521863009831828219/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^21 + 1457805594940681956669969053068117811343581059686137897105646971431734997122195746843775552899103067782913158907825478909006057162979629402465822783216838445960582400258597796459644515/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^20 + 602742983759266679236346790431729366468733970972278623709519716533037795981732655895142063052105022303629081322280598018357500054605565749518971408706110988299909708600105918340340239/73373737161405087559265664400359686966227544018894481776129304845368814826001855484365311210612283086915526631707533000954723359763480296388570716850285354677335521061306607304704*y^19 - 9905246415001446076434816319268653083817944757510481081517671783663780809453605912564839399104116292964742553309768159468554421080853126580484495354709085320030148782848055008341910615/586989897291240700474125315202877495729820352151155854209034438762950518608014843874922489684898264695324213053660264007637786878107842371108565734802282837418684168490452858437632*y^18 - 6952490195651767968486574220546223216161126049671131467236565312154463634720215599878441817202837853323234525779585406010348251569249596712191599461997956157299273263745774505099574795/293494948645620350237062657601438747864910176075577927104517219381475259304007421937461244842449132347662106526830132003818893439053921185554282867401141418709342084245226429218816*y^17 + 3567699036866420574653148830381276381908349754591668524866648904857625481400047740124920145483722414189219727169016531276980828895933678219620699500656206242336582646802354927385818921/73373737161405087559265664400359686966227544018894481776129304845368814826001855484365311210612283086915526631707533000954723359763480296388570716850285354677335521061306607304704*y^16 + 4746688756908816122263771368994194749155114332330757817897162585528145060628898131077881106055140444060322982248566631722327161121378973131032452200908271991477144376720237862549057365/73373737161405087559265664400359686966227544018894481776129304845368814826001855484365311210612283086915526631707533000954723359763480296388570716850285354677335521061306607304704*y^15 - 3606865323434337007089406351432602367066151543836376861782812994059926478766670706532019029444457910777972714682575034284325124747743063722854069645956105259346821977167192928836915937/36686868580702543779632832200179843483113772009447240888064652422684407413000927742182655605306141543457763315853766500477361679881740148194285358425142677338667760530653303652352*y^14 - 553885483535192183920694264748748144195699639972628795316602593278779603429802620036874011215352016293010176210903187639359063062885801490342503104585761140091630564898116051340600267/4585858572587817972454104025022480435389221501180905111008081552835550926625115967772831950663267692932220414481720812559670209985217518524285669803142834667333470066331662956544*y^13 + 20389172777525753833986571467518998073443829385795372901424553731961686992268058634450459388350762646710510156743885587997265864573126440652077740044332996012652218638437311237082375/199385155329905129237134957609673062408227021790474135261220937079806562027178955120557910898402943170966104977466122285203052608052935588012420426223601507275368263753550563328*y^12 + 166320091391028268612191844014538716231303154515143672404210300837097396834985904100243293430235341020661491688489565679040736539330956634292644641639678283734764879525208033435797581/1146464643146954493113526006255620108847305375295226277752020388208887731656278991943207987665816923233055103620430203139917552496304379631071417450785708666833367516582915739136*y^11 - 121730239627862149896854857786440642998540792581694752047867243795887802038556083767218039482892643621882560924876329778146681538351670150195653129878883099546467443675367431277976423/2292929286293908986227052012511240217694610750590452555504040776417775463312557983886415975331633846466110207240860406279835104992608759262142834901571417333666735033165831478272*y^10 - 5491192162976090942836188057228316768728410893043112517780250378585296971716326344559166749855866694850058511788499150908547490136678823498561151068956415873260741342803802516443155/49846288832476282309283739402418265602056755447618533815305234269951640506794738780139477724600735792741526244366530571300763152013233897003105106555900376818842065938387640832*y^9 + 3012401160648235277600107433954369991951514094094431671000767938879237315796817077419556706027243791241135808797729695786545296995217865526609489457960042678362943690976680701770991/143308080393369311639190750781952513605913171911903284719002548526110966457034873992900998458227115404131887952553775392489694062038047453883927181348213583354170939572864467392*y^8 + 14587040278318880808788120087991895746408564150657001438611383333427498681659910201976423902060755911313786324364231003973939164283866607720479090441803247029917970503301939832774677/286616160786738623278381501563905027211826343823806569438005097052221932914069747985801996916454230808263775905107550784979388124076094907767854362696427166708341879145728934784*y^7 - 323202746334020657049685292364313366059960784933869032256076973025019400641445827638659451465343119385264958182806367325986796199565919608356493197111251741188851789065294150705119/35827020098342327909797687695488128401478292977975821179750637131527741614258718498225249614556778851032971988138443848122423515509511863470981795337053395838542734893216116848*y^6 - 1110622248957763403013342456745476277641807234148006028309181791331881275814919405584289849743228460096905403964945141924411492663466276435901443094446265067677868689089464962223449/71654040196684655819595375390976256802956585955951642359501274263055483228517436996450499229113557702065943976276887696244847031019023726941963590674106791677085469786432233696*y^5 + 28357498281708272948977863347873007877751798863969592957703133605131789119153324848589846559594971292919796161908486273408145660777198876997205098438765981563531020840492615185855/17913510049171163954898843847744064200739146488987910589875318565763870807129359249112624807278389425516485994069221924061211757754755931735490897668526697919271367446608058424*y^4 + 2909992354145108355667736079306854686472290025673448151888933886693801396702876338775722493191334745771763050911344019807736626817957824877693382256341366132547681126977981858363/778848263007441911082558428162785400032136803869039590864144285467994382918667793439679339446886496761586347568227040176574424250206779640673517289935943387794407280287306888*y^3 - 601079770549225895952019341928829853638680592726542290473297883663135463835982895680370154021813176226294589097746514583439394109572581833105184319597341593274816622789584408323/8956755024585581977449421923872032100369573244493955294937659282881935403564679624556312403639194712758242997034610962030605878877377965867745448834263348959635683723304029212*y^2 - 1638831241605528959734721200342181185123820836502682240613154663212859012620253659932512353076756381315203446310325572987002425131871867313674438175051324532891092795770707274977/4478377512292790988724710961936016050184786622246977647468829641440967701782339812278156201819597356379121498517305481015302939438688982933872724417131674479817841861652014606*y - 129672908715220472402488669899591968037635681897313649303550917502806436527965147615546839546627868280370632026321736954121972865514119251168943388148811797855657947619604343020/2239188756146395494362355480968008025092393311123488823734414820720483850891169906139078100909798678189560749258652740507651469719344491466936362208565837239908920930826007303

# 2 Loop Invariant
-3253168520445189368422945923637238779819332567927140963136270614159366700956605864212286171097635241446533376304980212223615321204303245396291352163619273639543468184294186483458947768917416263382828394827044034629381741196368654332633893234994212985464720723230269578553154011138625828261023882551533879292996397037742849784135/36130207940580201704500739357979813398294517360418899046745793963575066519327647291026134296097717287711272950613273593241199210899136719202675891110913202123264875114258726863812599340416629627745341792138771080081548894777238432115948996059907920100442336542665324773562171395189519077042963321919010231970748093173882486565407555584*y^38 + 319207401488514133993339500753016447337021083535968622808338011750056974252661448170281841662901718809590696368118863707099442321349509805086770637860645543007495376815902297724421266361375009827328000836806313103867214035942086449784322233143122981660114669611327060326164901216086736076673126075938840466324749181248377888164659/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^37 - 319249209116494674404846609605931700098589080186636732121330729095568235884228193729451551012834197480001170018929997846991304702151101805006819059562400813091460715761252917108724956734118142509031496739325167753926682811254434893146848046891366326711699099587342374155325675199301495386244512825252320541722434600372171170492799/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^36 - 10673660940469230250983200020558922108600290238818801448489733895438699977592945599659949260130515931169470114321034871756947919203938107029927318688690257755771675067181697370334664650301404366538461099054963308661764570800608430854892865756746639848916322303039625720534890360830092072303199191862508251036271095227502376311059275/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^35 + 19327672501302696968678583124565458491270954142599642577597218567896889510634214594764569892971580580113801182081462194540648275167640900084839063554930780092895113271086384703782201402850700705903652455688356212986102840361320679309535481455620710889339676774547110399032059119750841713437107812444989456596652948505857868499212905/72260415881160403409001478715959626796589034720837798093491587927150133038655294582052268592195434575422545901226547186482398421798273438405351782221826404246529750228517453727625198680833259255490683584277542160163097789554476864231897992119815840200884673085330649547124342790379038154085926643838020463941496186347764973130815111168*y^34 + 862699069110715754270070585255774260916571978905904416711370598153616135367144608229877597997093068703488625479068362430420804141348769675295290172747254478028080115072338132300542843314194423359834466620737991431812924850525848152311829147327999158902334801029420526677997670161535243204117557525466009744955183327169974151031305/18065103970290100852250369678989906699147258680209449523372896981787533259663823645513067148048858643855636475306636796620599605449568359601337945555456601061632437557129363431906299670208314813872670896069385540040774447388619216057974498029953960050221168271332662386781085697594759538521481660959505115985374046586941243282703777792*y^33 - 35104946158252028922953390641265266396342960885403873673742775153892651677082637308893872035324810064145277869426359310049769940502323335484535115721208371890518560155225230591469043924365553824444980747878414971567106372118638175433394780678875454423720331839146955601215994763533656170163334542561902886084799154025067629187827161/9425271636673096096826279832516473060424656702717973664368467990497843439824603641137252425068969727229027726246940937367269359364992187618089362898499096206069097855893580920994591132282599033324871771862288107847360581246236112725899738102584674808811044315477910810494479494397265846185120866587567886601064719958404126930106318848*y^32 + 566309079501867231058020887853571553985263670547306605871943452107856565119654621231399576858628402109328532130041945046324664195686824585763232939602068326214115844895733008631517168388448203749006876208148091824162006304822228303529814555297128140718640412808808620356795583601995532869367524725274613788487954706413140000628773561/54195311910870302556751109036969720097441776040628348570118690945362599778991470936539201444146575931566909425919910389861798816348705078804013836666369803184897312671388090295718899010624944441618012688208156620122323342165857648173923494089861880150663504813997987160343257092784278615564444982878515347956122139760823729848111333376*y^31 + 2196745944783867074374183837769968721268892968841191810063841633255307748698939565564009628567604888439022715078720475690665016487507265695614983307686952458865796047848338313359500697715779084322992592524402512773028995120945254597903897774245789688032758630142272437486842388409396188210005531402139728213377887895075134622847392135/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^30 - 20184666526671430532387433880026683518599791398462798293474118605852020647525167342585302040035415242460459116654792396013463186211293875258204256812564435819325249688690114732611079918320522965541083069128692893739191443809689523608227558609682907011524362882109344657159204635166118701764338574277234458924568983287282628809129661157/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^29 + 23716112812574124735120878412405848244433752120064358240292586940735273846740367544984427853702150448851338101041518440845917447908558270879357085549153462510641912937685900027107369250336303306005906979098331457014496814514855501611274886756630307260881644286967030767658123000709121307818933172502093221972578053223177111120628295807/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^28 + 56083408597416409878233339734064933989845541997434486409321357306994384943845416333360671885118981589308064065155449169170112078648645657804465416011352137092799214451183348228996322347532921898399122391396484130974314616340323546646067470734852750975536197873705959944192732536590032343821448812461891002435509317959762590144502011395/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^27 - 139459274773962713425873293709962240743523338680112234410300458477665661248303260880787626118763425558553385746757745928376976925328413679427157068886176744014027019556018429905572720843537594021109361147002619038083877122134387178901894734738669478253502694254281076715807788295355001593852673079287239586276999963444287977483709762207/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^26 - 41239530174664990620156973881296047171386168833960126334413092323546902575362307727084598723354560059704219326823988554277343701429762451685273140920171099517111221207345980681357897920168604590446261171196400292651393091764517914666970482882209994489679531164014780458177198943242950700865119713139333746082990782596850364416370173173/72260415881160403409001478715959626796589034720837798093491587927150133038655294582052268592195434575422545901226547186482398421798273438405351782221826404246529750228517453727625198680833259255490683584277542160163097789554476864231897992119815840200884673085330649547124342790379038154085926643838020463941496186347764973130815111168*y^25 + 78078991401742134441527375469394785837148095390539897123043582346172918822378829267885454627512405666461187618530353371176259538952216190366586098440529837053671660723685106789830018418948710424158925508448460784749261153631977543879667656237395230506775142394297159479801909928427523133829302627091836223457385037158909777424707480841/108390623821740605113502218073939440194883552081256697140237381890725199557982941873078402888293151863133818851839820779723597632697410157608027673332739606369794625342776180591437798021249888883236025376416313240244646684331715296347846988179723760301327009627995974320686514185568557231128889965757030695912244279521647459696222666752*y^24 + 378599717353978827717199090036979938771471783652633676500470331948551105794657720960574992067144889329672634668244767377221612927697962712932314296675010083397287415060249916780688997243550014870784818080281398880265676126264707958879833389876870887582109912198023950580578404989259866996641316326162960999545091293531892392189984345915/72260415881160403409001478715959626796589034720837798093491587927150133038655294582052268592195434575422545901226547186482398421798273438405351782221826404246529750228517453727625198680833259255490683584277542160163097789554476864231897992119815840200884673085330649547124342790379038154085926643838020463941496186347764973130815111168*y^23 - 688402176353001192227335702199046528254706429505684106641726598641295460928607023380720057026871949677701634640531563505045679701138962763766236608771926530646350203771324313532039817185184530718754782830747737469703446560512706305670129398060151711820335420588514702156819584469728369418935949491795189658129488214093055789074514130639/108390623821740605113502218073939440194883552081256697140237381890725199557982941873078402888293151863133818851839820779723597632697410157608027673332739606369794625342776180591437798021249888883236025376416313240244646684331715296347846988179723760301327009627995974320686514185568557231128889965757030695912244279521647459696222666752*y^22 - 7002442876321098804004539557787327457000033523767259303742222983891708417690847985258490181223358529336555437414959543868980969765292328344443169499025251800907915836143101674089551759179182782282832319091804923978281861661960921173557295466791958886600646565528575117166932783940201586761467386104755911517463078179787306938609408691699/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^21 + 10400211110134912131201671360991391142308233495604621033763694552753816837636935012652180264216044772352172083801237398756838961563295212506459127603526245225315827696689685500036053682446054142689607985106884420790402757868843289350225515282722921357341414011948531998989832532386617156702238064166998250239667542045039333385322951866001/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^20 + 8123236789954252043706586133817226478191398939586129245686542693756762487461087100581362227602337124334360691300630567210934851249270221735379483506354386181006764855452134712753839221707619414859794924667951770686285339759425243913446532984729208812460897391928361011824726534748202841954959648124940148105635777380861595482967504058173/72260415881160403409001478715959626796589034720837798093491587927150133038655294582052268592195434575422545901226547186482398421798273438405351782221826404246529750228517453727625198680833259255490683584277542160163097789554476864231897992119815840200884673085330649547124342790379038154085926643838020463941496186347764973130815111168*y^19 - 35435668866622352920195452886040777827375185457703817930530889671671134978479762529503672314154401426436277529064386592288440429570600830503265575113593043121450194684834258380916955573288295373744743809753230247952066697630230215503567989830030982134700922029049550163581617178112570431912737029567074396197292172600616780962128483628343/216781247643481210227004436147878880389767104162513394280474763781450399115965883746156805776586303726267637703679641559447195265394820315216055346665479212739589250685552361182875596042499777766472050752832626480489293368663430592695693976359447520602654019255991948641373028371137114462257779931514061391824488559043294919392445333504*y^18 - 5894318303391746489901381417768721059508813701737229150659367578361919132705296165532889900843083742616829208010472522239951700737282372759420491095685934780404483745080011868111884387374762709476343374393743175060073745176750451067915979426854813664176810394888584045786400375126854409437847530421595293732325037519094837819721643293645/18065103970290100852250369678989906699147258680209449523372896981787533259663823645513067148048858643855636475306636796620599605449568359601337945555456601061632437557129363431906299670208314813872670896069385540040774447388619216057974498029953960050221168271332662386781085697594759538521481660959505115985374046586941243282703777792*y^17 + 4241864648792296170131959492685722220799417519993167973712691940742098849179114114309145559584887674974222970638771683544465528806902118246601668542125486937205933281222418908882372119376251727222653093232005004386917634746654616814752874698529818255230256131490893778554671385405422011954152975695696048600490661463162566679482714995653/9032551985145050426125184839494953349573629340104724761686448490893766629831911822756533574024429321927818237653318398310299802724784179800668972777728300530816218778564681715953149835104157406936335448034692770020387223694309608028987249014976980025110584135666331193390542848797379769260740830479752557992687023293470621641351888896*y^16 + 12104486657468980427625353076643240415653578777644713184996193134238416166723310775145832253276102778964214107124599207339913289794122585798274339866215102184217291058597916233734702844938685564039976925868610971412652381685849623044321639187210876874455683630253404887738320706251387861119192516876868456003150361695744023566656920410401/13548827977717575639187777259242430024360444010157087142529672736340649944747867734134800361036643982891727356479977597465449704087176269701003459166592450796224328167847022573929724752656236110404503172052039155030580835541464412043480873522465470037665876203499496790085814273196069653891111245719628836989030534940205932462027833344*y^15 - 2956217840268955663174926690792960814499795517246394972648543160319868159093303951548136240555993353560698629704177759199571520244141990234657595794751188168644363652905274385298713666034051999015948574310446602400863440998586212882792581318899904159547059835011266104361326525498277662189351182043686409855230642966274778544168329272377/3387206994429393909796944314810607506090111002539271785632418184085162486186966933533700090259160995722931839119994399366362426021794067425250864791648112699056082041961755643482431188164059027601125793013009788757645208885366103010870218380616367509416469050874874197521453568299017413472777811429907209247257633735051483115506958336*y^14 - 11009392738495897962071842333906362130705787337285451429633040609391470938574446609663424912315239034233978394946681197793844743727910259305299101992925102734226429816748524928047631399103328050771003901305763617404382524876571761168980042881440629892175115520005845473146407773845744756411273239989372200682420336936064808143183194571593/6774413988858787819593888629621215012180222005078543571264836368170324972373933867067400180518321991445863678239988798732724852043588134850501729583296225398112164083923511286964862376328118055202251586026019577515290417770732206021740436761232735018832938101749748395042907136598034826945555622859814418494515267470102966231013916672*y^13 + 105163384682469543120695653243368960514796141580200914660787282467845966494676265065892733770936995877897631028621223003735150703033772399537682799506399128882887415717227295860223133152154478161243471180021561677435623803542457563353684554072960196420466717736371143717247586637706296470043271286127485458959632813576167734546257185635/147269869323017126512910622383069891569135260979968338505757312351528803747259431892769569141702651987953558222608452146363583740078002931532646295289048378219829653998337201890540486441915609895701121435348251685115009081972439261342183407852885543887672567429342356413976242099957278846642513540430748228141636249350064483282911232*y^12 + 491012928167134502550790401077896518977229537881577422025293305412765775196658991236847521695124623764539972760505237238320419981668243968348064476828862477108518089734479290213764645204377859081427211401159915012511935893779234778396211482959214013831483433947696212877897828724834353720415064419644126933195765628927494543844836569935/282267249535782825816412026234217292174175916878272648802701515340430207182247244461141674188263416310244319926666199947196868835149505618770905399304009391588006836830146303623535932347004918966760482751084149063137100740447175250905851531718030625784705754239572849793454464024918117789398150952492267437271469477920956926292246528*y^11 - 1108369014833023603808664198018282647562429433991329638664251237862957663210614751782026575037014791795491978209171286680514625205971939590398926928566182859602661951750965192518334002418227056534844514163870603269378418723701811681001165670106952800540353481957854348369450373206587990063593990031033300227166715264584860539203988281/6615638660994909980072156864864467785332248051834515206313316765791332980833919792058007988787423819771351248281239061262426613323816537939943095296187720115343910238206553991176623414382927788283448814478534743667275798604230669943105895274641342791829041114989988667034089000584018385689019162949037518061050065888772427959974528*y^10 - 10372544697848150924256810159632384741785178857274801920138161961881256066205186701602140769354337276566403778833893460538842723228940094895362227703149376783159753785222760350491332042478649549634636452434231750567251717892798003427823074736251277396645718720926695409532138568568291666468025971639789048034506093154475365138950110935/9204366832688570407056913898941868223070953811248021156609832021970550234203714493298098071356415749247097388913028259147723983754875183220790393455565523638739353374896075118158780402619725618481320089709265730319688067623277453833886462990805346492979535464333897275873515131247329927915157096276921764258852265584379030205181952*y^9 + 6095841491078122648510120152287840216318740829290554255009388733187417777164082508267578663553925702069613662380650194917844682332240100370462892978099763585482615772318410594298352753505075347583874311616289197353063606089965360370014642242687882353384605572105069951708091643557967508444892163029451672615956560188467353570992729513/211700437151837119362309019675662969130631937658704486602026136505322655386685433345856255641197562232683239944999649960397651626362129214078179049478007043691005127622609727717651949260253689225070362063313111797352825555335381438179388648788522969338529315679679637345090848018688588342048613214369200577953602108440717694719184896*y^8 + 4205500405238937379664992929258751502403325054297747080313977906799344478543216357133740153937736546133315604336060342616358891402891475149196326882136773162384128695526131325664154753577783104985508454282160865263264053333979784970812216299203743163859718341140081434468356407013338168615052646902692732683202459121470429224665126127/8820851547993213306762875819819290380442997402446020275084422354388443974445226389410677318383231759695134997708318748349902151098422050586590793728250293487125213650942071988235497885843903717711265085971379658223034398138974226590807860366188457055772054819986651556045452000778691180918692217265383357414733421185029903946632704*y^7 - 3083636237463325566163467128112368096884513323746922361931514633501533212112176935969764928122772291891380921361174793590695859171528756356966282734091461587139215151910028530336381884377593549225400910312988714503292937217983106204962944502496076399956959329652747251546682929988379887239566159181962405328239543592870008352033880775/52925109287959279840577254918915742282657984414676121650506534126330663846671358336464063910299390558170809986249912490099412906590532303519544762369501760922751281905652431929412987315063422306267590515828277949338206388833845359544847162197130742334632328919919909336272712004672147085512153303592300144488400527110179423679796224*y^6 - 3436106977881923308715280723527708903516095544270868525229142650028425666072952582446006456315369103765806996762554073314276774436026924730894871814268444741049218482290456100961983470153159717280944354595261035902434337350792356510808377601162345062515269132214679631654207544012969917631516733379498056685944079892864549879561536635/26462554643979639920288627459457871141328992207338060825253267063165331923335679168232031955149695279085404993124956245049706453295266151759772381184750880461375640952826215964706493657531711153133795257914138974669103194416922679772423581098565371167316164459959954668136356002336073542756076651796150072244200263555089711839898112*y^5 + 173302473873723359041023561770256495089325316819579350161717054977198358896526868206128448446831893764032654604457893390855534559573453158892896152475428800303337173633729514994233226495006292154698881420886781165383223977983356862416029139384625637349694644989888903103797888425326671522463935396846635809388335714447836542911672805/13231277321989819960144313729728935570664496103669030412626633531582665961667839584116015977574847639542702496562478122524853226647633075879886190592375440230687820476413107982353246828765855576566897628957069487334551597208461339886211790549282685583658082229979977334068178001168036771378038325898075036122100131777544855919949056*y^4 + 651793729108901990705080041477528867308451896043033745168192660584213313109033567948451841150918726690843942608076057108087954275361537333881744916273094956329798238704215657960987718067084226737864443641895801927347232111051387029031566591415571417659948952540674557884884212662889357798613816622356810211034797528432954866441689/35954557940189728152566069917741672746370913325187582643007156335822461852358259739445695591235999020496474175441516637295796811542481184456212474435802826713825599120687793430307735947733303197192656600426819259061281514153427554038618996057833384738201310407554286233880918481434882530918582407331725641636141662438980586738992*y^3 + 1859703797596881341219255460694974950743660665975430788743831085610309463146736970696226530545368095991904722712369539491690283578591245327681711935102130571152734395823729430726852419741002789768171378391560875387705313789214152928391103289323099101283719961391456126237084927435058976852031328851258557145057499891650870869359441/1102606443499151663345359477477411297555374675305752534385552794298555496805653298676334664797903969961891874713539843543737768887302756323323849216031286685890651706367758998529437235730487964713908135746422457277879299767371778323850982545773557131971506852498331444505681500097336397614836527158172919676841677648128737993329088*y^2 - 751603171828611999455100353978895366832970552405554572926375751516107688398621011130982312020463490091690457068501686115943271411039361259015847937873095870559256867220679431332895268435511145350729169749226739956705750358119252654494675365971787103292966860812899719308768280095862558340115165515891215866980199805347334822155383/1653909665248727495018039216216116946333062012958628801578329191447833245208479948014501997196855954942837812070309765315606653330954134484985773824046930028835977559551638497794155853595731947070862203619633685916818949651057667485776473818660335697957260278747497166758522250146004596422254790737259379515262516472193106989993632*y + 1661874075159982039063496982602600951025013913482773087761967607096753578745258816521570642648428412268742083544480644465657345907795252618857486776252656858138561458925785181953056561090313446392859780685573834010041971186644387865516930309399397785089516632940351943998818242265260782314582878802577219436673347119383841244215867/413477416312181873754509804054029236583265503239657200394582297861958311302119987003625499299213988735709453017577441328901663332738533621246443456011732507208994389887909624448538963398932986767715550904908421479204737412764416871444118454665083924489315069686874291689630562536501149105563697684314844878815629118048276747498408

# 3 Loop Invariant
6257493836406344246553734727345518200802676203209840943208463911590907118483862155457750934802503512723584240246982814426768247437940338942113462906480207086455344831589412494554536013279925371213986524390278022303605824420654020026022460584050709591449421060768908127671474505775192119540806910544083105050678471573836000283769676443646527082944896404143272996386909272826574660930689679088080281262018191/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^38 - 102671741669633913149033683651389516364561942320028804200943884528673610591847443617996044278510594464806302648652080067708151031171091689624433682145378858165559098801933281526232182438331314399880725081929506752419729296687183640119047882223047720696249602411594591004738496049247418046187562145135407998319028486868871451500084714190241703503490813459120454983345563847371456664138948759640265695999957791/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^37 + 108070719038607231218413181938489203994638528222941109806813424828352817115884558768315198468169315952532737076692497936543414841062253907692656301203702317457987637076208230140355572465745936377763275499217050959720786029454980725779851223597848406680845209604857818677974229734019775857071655169979847415353813742214763936481500457131301719735122349252653859884502902606557525679775329590498449910508265741/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^36 + 3413092311665135982770358772780197282616902195278364811096516068142188040818494219316496384120787849075863627922847122207405610622161995512046438463885004516807260474400766578982381164633559238727184009476732545993488139357510551274057197836689580556520928760059068968137776234696799994208340526439739141673717643505325531640055353086872113574543079214988522421051383080786996123252908306005675819395776528209/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^35 - 9383964787873025245448930912133315766999774003330281116059506430737786650677232524308636086282535466282817554400575953263055057718218433050091959599684801711948091481478352602501362173968074915487983988421992711882520019737279468482001928728873768452024227335601269509962342449319863115263700617247354516019871467627879393791172825995242962968996625317341731352934914177252303876544420152315509414206792341511/25353351163633892797867945636466028313568359494068626326454676318449127938160653172510560557449728171479185423134244646845986981474129003550362837084002675214651405870136278722298626420418481399323152812127288081550656464843523975491293442394438171744599050083417817942876346179301901317114924224424903315823411607248349280524406987561250710554496221071833955876842526320709721202370641387787093673253875667173376*y^34 - 2215433435576204575205672760249676762101710350636961199473408731781690154160744797878020970335608710610215348609875324195973549409471242957769130309484713249654311077176180293298406621102151481136689694826417959539201674747710924438225489353548647972597259986390191200214016327989865892256306645697778703221857408238975249515282979333266830720566516671305039829373441197782184875646732783444107117441270462125/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^33 + 5617128983050210533939436853252425490098123348990140869394768505327851275000769491719604873266737297242018040110016007583025807309902808686882005282591859222996050200043302238635806642573476407352477810942272087407777159849492116853663034375697952419741999981003201061608285872397485062824273528214521739434932804879873336530229866160396157661945569208001689141240949035027662619995634476877886569309056087107/1102319615810169252081215027672436013633406934524722883758898970367353388615680572717850459019553398759964583614532375949825520933657782763059253786260985878897887211745055596621679409583412234753180557049012525284811150645370607630056236625845137901939089134061644258385928094752256579004996705409778405035800504662971707848887260328750030893673748742253650255514892448726509617494375712512482333619733724659712*y^32 - 739788213403112642971636448195552411701023546173877681266774322947613981394469967370615324150577237030746330378250705762118173579357005055065845817726851221382804413905359600884312037132534342313356932294309810998872596987821966116842020528209593854282302895426933151515937839207961387733258366319287525860695613791384661116372890167419282213116969576389959399974025339185575034499373582868995200803696493989033/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^31 - 657414000374074764359917780875828023371908867667430876128224434587053208286864127606311052006867331535056973096502116662301717485292643772151770771304867454825054089462573943135099378367351071677628923808961504523652648591460114266592465798335745779577118187234651955494204186290606437351548946953020858607030551826804663243342522551228728570498594292835022153600495441176115563589955126348442849850764864074869/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^30 + 6480905048982852647425513626939217666048345422919058916293869102465086728068205134979849839840639612724328018813713948823080813341572284945136143939348754228588645570500165060862404261490958623233683073311905590615892963453489356002514446570423498434519004960984462715516182935381872903464127942637620876463233186376959748022250833640330372954533754337495833929626142387527567443402987041743379004270075257282303/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^29 - 7952522860145229824625184413152553100368314784433563744604601055069815802416462572860736529516576214974520659390696142156938618602612920953197228449120897237220533850133801457608521127719209581677270775134463381358774947854329806783802075548611143667100530282733928056139841354093928997259786066440431893229819645633134278090840819576296827100080128609378542568615027164305549893639023503205868460612354402946169/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^28 - 17367217924638943651812266796826725249737950859142382889252250329969894663747390468270272018764679844339707861231398007645090481423242256810015285117109885549615703532198864145269258211324319030199517563678222979223786556734966393833434805822272063377757559297380318839996494629114348787070516175625680728972541409725772513916939914604376647463534567980915013574897428892160037298073735492336798398796606861903219/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^27 + 45286580099354056506026658625173388763242859645388248975327316553301380962680534460675560025133506350844129365724993293192492051825775131218744449948631090723691081847934841881445211608919671403365903821216955448181566015926633553268695562710972818377227329531026337733137370647986906320170213995410957735553138694069338277983034273841270719891367045645148642219786919406277893215124191493873629214849951539894527/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^26 + 9243746781634044427610466576087378284146697314080581787363558853772386855667345819045841409528596434436073861608664515068875996429110741756981714719865169552191302877681121004074936466199096869226841046356791634633478084713430575829531043244631348103331750911093705126260164551634197141833410454292897450041042620298437485002857495183943848884779969195294778324632532993267231845046018108400277703793985771693729/12676675581816946398933972818233014156784179747034313163227338159224563969080326586255280278724864085739592711567122323422993490737064501775181418542001337607325702935068139361149313210209240699661576406063644040775328232421761987745646721197219085872299525041708908971438173089650950658557462112212451657911705803624174640262203493780625355277248110535916977938421263160354860601185320693893546836626937833586688*y^25 - 50534657094271535989886592673673340000882522518914628490955302264386094873804868248764406856522985648502242190205846143461489763101939279297534109041417772443968665973245969117896399921383458604799568693955097281350198034444993633821528193530342998277116596109968814315260839041111939234688163495089313161264141454832295475970745033942920165708885172188554306330149374467894817818981567668611154899621276991968465/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^24 - 45188749704758307317411543994713103087588492398104206166736875784617051087069294587861495607656036846251889791178029767627964852669795109166977730441723403706590509286880537945644863023321420787112619689910314385485014765020795321334400415753687551483548748871726433948789595089261478826197766226370814400107912477116097535726968830533870312285478649189552578676128125909929194453452855150209010440091412800845637/6338337790908473199466986409116507078392089873517156581613669079612281984540163293127640139362432042869796355783561161711496745368532250887590709271000668803662851467534069680574656605104620349830788203031822020387664116210880993872823360598609542936149762520854454485719086544825475329278731056106225828955852901812087320131101746890312677638624055267958488969210631580177430300592660346946773418313468916793344*y^23 + 459068540397928981058803684551200776402480573235074753939767604306371467139858103877767367628973762022327217479878119530990891608428658719391918044978178596181189021969006281651680784168983882798264611763882192387864958547541413854715548217376935143025519085345438218927785500808009671197033833833574843866780766249070465231183502723951585901177093111317350674027112862271047548052317326101126354723998000776283733/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^22 + 2211578801875372998116187307685472419004856508376520297694863828487344076202722692985437683111476243294200057881404290084202064163442586519185958431234362866389594805059044667724584172471858856379775975538820683923141005027644886835363618123219348906789983359177480585096131554585717778101632640386818248701461212613656186965448994659423320269414637771858215880356232144672666618954929499944555844498772684603509237/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^21 - 3433632728181670431649916327662928508227660702645444866189087394982537518624281182183545686258050567436402021355773817480463228191784042202849453413076647101847948235346224274441901597748303213411861037850467348297751694580892961378439245239050243668138217064522115719497828224268115138593080179955983068546812032053511101117069698487379388872796590875667810231544181002282945128098894040627372273851918215711228345/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^20 - 7580607036557572808611093174187556411736170162788996058534215779791036563489116496052723406515325593344433158932566839941418504966531079747304009642012776602748442707002255795888146094340241613793734197516042336339807151108492631173460414725052839343933498681637969126692830251416117927314510316487517552270572908272935634742158645351840582808973589518988363594097289203242761596004851259399803121903077619463180537/50706702327267785595735891272932056627136718988137252652909352636898255876321306345021121114899456342958370846268489293691973962948258007100725674168005350429302811740272557444597252840836962798646305624254576163101312929687047950982586884788876343489198100166835635885752692358603802634229848448849806631646823214496698561048813975122501421108992442143667911753685052641419442404741282775574187346507751334346752*y^19 + 2908015698092611753084661937330301333731163869052855984650665362835874568990237952670072075949717268181174469653979572475968668994178048882143236579264769108406424791397929628884596495372725736201768566851650518640071367432349792300917112315673428602802714956379266541887538933163944113338658305983573470432418883773471491498608246722268896133475311061521796087217703361420302054684799712459510811462966820135016875/12676675581816946398933972818233014156784179747034313163227338159224563969080326586255280278724864085739592711567122323422993490737064501775181418542001337607325702935068139361149313210209240699661576406063644040775328232421761987745646721197219085872299525041708908971438173089650950658557462112212451657911705803624174640262203493780625355277248110535916977938421263160354860601185320693893546836626937833586688*y^18 + 685460520672576145314900120375580768464040522510884250040132068115086641176067822289990645958701695630684169959931796632342870864661991437499178375921447676372960559831123700657601572396483450365896430090660291974657269002774506622780891308231127027399280412494535770735181234353063886763485286334484260379744031652982255002291092016544065046967809459391235321483837712833959057330012494652488220827780280704612435/1584584447727118299866746602279126769598022468379289145403417269903070496135040823281910034840608010717449088945890290427874186342133062721897677317750167200915712866883517420143664151276155087457697050757955505096916029052720248468205840149652385734037440630213613621429771636206368832319682764026556457238963225453021830032775436722578169409656013816989622242302657895044357575148165086736693354578367229198336*y^17 - 521379314409281274090638680787688569362286987272787154074436262583880081951872929597631216987084785201876405810971346580669087483823120394145974073188993363522576135355318722546871545605036820515109529703780514787788125453064583385970292295589244474584632933469962917939493387656339997403962029240315311069410474000133628619731943456227078674752196855517383414169797042825998769522484456532766249207598086888613613/792292223863559149933373301139563384799011234189644572701708634951535248067520411640955017420304005358724544472945145213937093171066531360948838658875083600457856433441758710071832075638077543728848525378977752548458014526360124234102920074826192867018720315106806810714885818103184416159841382013278228619481612726510915016387718361289084704828006908494811121151328947522178787574082543368346677289183614599168*y^16 - 1874829774747682888500682214320804132630117204415943024362027108669671945307305016836871579520750916797885678487256185474627636147355044017734570223215143847784861117500159104029744035885958370267845312138416393756577792584786554208189082436957784438019219995992392310404209641658635355265064469066280243077793714240151633554052601295754845991619502179702885942400204327859287562492587586590149589028665688325422465/1584584447727118299866746602279126769598022468379289145403417269903070496135040823281910034840608010717449088945890290427874186342133062721897677317750167200915712866883517420143664151276155087457697050757955505096916029052720248468205840149652385734037440630213613621429771636206368832319682764026556457238963225453021830032775436722578169409656013816989622242302657895044357575148165086736693354578367229198336*y^15 + 1956287665370115502458511312302731046535465539783600075541132620291210623570471906045769874482567319744308627221925184572604411428828533365620801915077660252555391921553204747174595946804962444854244051374726860043333573483663547913606818934377518786237230924622893626275811968158688849492436553853426609800623874477128601609339730278550650530838355212615288027013208567602814686965006371673518184312418630610936827/1584584447727118299866746602279126769598022468379289145403417269903070496135040823281910034840608010717449088945890290427874186342133062721897677317750167200915712866883517420143664151276155087457697050757955505096916029052720248468205840149652385734037440630213613621429771636206368832319682764026556457238963225453021830032775436722578169409656013816989622242302657895044357575148165086736693354578367229198336*y^14 + 1700039304545438943251997416628040406283526770843629637349900490527464851443296150579531996751530874048039394831413231036996716025357297617536721489574456864444766195565655516980758779546137977190064283221737043178501533246912299788330336244279763452576764617250028870110918810012129322320175128005113937664284366068083871156217279127287948461687645379714118237571592540896138526306998946963823751160140269784441765/792292223863559149933373301139563384799011234189644572701708634951535248067520411640955017420304005358724544472945145213937093171066531360948838658875083600457856433441758710071832075638077543728848525378977752548458014526360124234102920074826192867018720315106806810714885818103184416159841382013278228619481612726510915016387718361289084704828006908494811121151328947522178787574082543368346677289183614599168*y^13 - 8955783278825079179337109936774599629771327694375116963357361915231362880879454007772893144008325805441938756291686457752997536196720969074637588649759498332277986912387470793719775127698416841408117985079787284431297279102931391824070408903717667272346541665955597792617772928388182370003954767519214385240344826911592732846870874647096516009325467471368919188335198491333938998510546061171834292891859101202211/8611871998516947281884492403690906356510991675974397529366398205994948348560004474358206711090260927812223309488534187108011882294201427836400420205163952178889743841758246848606870387370408084009223101945410353787587114416957872109814348639415139858899133859856595768640063240252004523476536761013893789342191442679466467569431721318359616356826162048856642621210097255675856386674810254003768231404169723904*y^12 - 456127413940345594715800662737339546991340655367077839093250295835684218008061322424964159024940270111873869021764904343340667076259479357154038834882713274164633681420380355546679724635262899842525186436972524678667294605243382959337913749262847238869208461663735935842694155851782042563340145404316432207934676350296574092129928364140867679188891477210491674478682969848124906697123058951706436783473143649032335/198073055965889787483343325284890846199752808547411143175427158737883812016880102910238754355076001339681136118236286303484273292766632840237209664718770900114464108360439677517958018909519385932212131344744438137114503631590031058525730018706548216754680078776701702678721454525796104039960345503319557154870403181627728754096929590322271176207001727123702780287832236880544696893520635842086669322295903649792*y^11 + 28568462129966849604407899399507725162591014514265829973566473199964514834475170299001114261710444234320342700604254374529071783845257822607234676777987531009367721412183573511412162009565057741801009528413716395210832128377698703594815885500041299003429628710582033247446587720542269777992690173551645471832072644682388886549817358192278446532751807006246546182347595279304798245550927171605050910696037115556055/99036527982944893741671662642445423099876404273705571587713579368941906008440051455119377177538000669840568059118143151742136646383316420118604832359385450057232054180219838758979009454759692966106065672372219068557251815795015529262865009353274108377340039388350851339360727262898052019980172751659778577435201590813864377048464795161135588103500863561851390143916118440272348446760317921043334661147951824896*y^10 + 1611998690230615624115614023588297751869525629767911960161581713957550119179034862643289483506398075672742401815719042230859637020914213564961565904332543895974298332840979358423068671412718500937958351027345150847554721846514554943716475791471621707141229415240627959117173512463319596078460638060023595642075262780073909085650818537953855806511511176500606803955572235688520655494078596747189894927803108324627/1076483999814618410235561550461363294563873959496799691170799775749368543570000559294775838886282615976527913686066773388501485286775178479550052525645494022361217980219780856075858798421301010501152887743176294223448389302119734013726793579926892482362391732482074471080007905031500565434567095126736723667773930334933308446178965164794952044603270256107080327651262156959482048334351281750471028925521215488*y^9 - 1821577947002414235897241420533114766622751598718122200731577307571139023544865285382060979430620874917303037371155319011586182670526080581771879922996330036143509739050016884572062776193666668261489980913957049193472598098064427557427243578965270871454993228427296253558603463779650341915517790921839425038543329155120519757952829957956845081135270779645310709612325382671616506902085869221520198104073415054105/24759131995736223435417915660611355774969101068426392896928394842235476502110012863779844294384500167460142014779535787935534161595829105029651208089846362514308013545054959689744752363689923241526516418093054767139312953948753882315716252338318527094335009847087712834840181815724513004995043187914944644358800397703466094262116198790283897025875215890462847535979029610068087111690079480260833665286987956224*y^8 - 7729173421768958549574322991266190431114277425564956765096957887416512589026335888555507687055227176066857568434687719568976395675438496288374316713081222721790952121346379405141649580441435129399413343426535899785809417205533080532336253617905436070976619710458206253993418818009290524071469670820730887174740535524418427310514976638288882559865149908022331801184704069670944966304025084532501398353291881735691/12379565997868111717708957830305677887484550534213196448464197421117738251055006431889922147192250083730071007389767893967767080797914552514825604044923181257154006772527479844872376181844961620763258209046527383569656476974376941157858126169159263547167504923543856417420090907862256502497521593957472322179400198851733047131058099395141948512937607945231423767989514805034043555845039740130416832643493978112*y^7 + 537833946891734069544388650300995849167840983151468501962273246835507536003687570023157821618268728199423285097772291541007532484110126048686927926795401925862429863049656851773168173416087621854081231667850583196323360080665705124879626592839438820459462195877142044545434684081066693588389832201740955456188185636096168735473045511531899620554356141551798822489828295672978469391264124975732794865850741949751/6189782998934055858854478915152838943742275267106598224232098710558869125527503215944961073596125041865035503694883946983883540398957276257412802022461590628577003386263739922436188090922480810381629104523263691784828238487188470578929063084579631773583752461771928208710045453931128251248760796978736161089700099425866523565529049697570974256468803972615711883994757402517021777922519870065208416321746989056*y^6 + 511655020017922124117068352697058452110696221758374290798479465720165261174097572815699330163930525039826932584125565283026897609034949159525259866030401682240964367603261657925588558747816784523825519559564513844103455753307106950833220233587168068261079564719621509340372743381849092097586773581217688292977378464658294064707146245780535984730756822720157216514859962078318008190405349800852864849732912331517/3094891499467027929427239457576419471871137633553299112116049355279434562763751607972480536798062520932517751847441973491941770199478638128706401011230795314288501693131869961218094045461240405190814552261631845892414119243594235289464531542289815886791876230885964104355022726965564125624380398489368080544850049712933261782764524848785487128234401986307855941997378701258510888961259935032604208160873494528*y^5 - 1452698595268242431112141073598899316671260263744467280385816472211917231961993598280304620241359752340063890505433212582188013631623893689988066187419286089229232030507878073385178707924980099475119895114738565978268679053721815623893436524670608844759314495125616783259645755626251680544064384248512687558145883449307306097884560157184130591464082960931518019743278322801666461783321315389703025568174847383/96715359358344622794601233049263108495973051048540597253626542352482330086367237749140016774939453779141179745232561671623180318733707441522075031600962353571515677910370936288065438920663762662212954758175995184137941226362319852795766610696556746462246132215186378261094460217673878925761887452792752517026564053529164430711391401524546472757325062072120498187418084414328465280039372969768881505027296704*y^4 - 810584283820387099400648687637776389891010968766388455192065926071395720603633856351629657837017404249123502670673991910925164999169215443839323687483221457923973122805317585906868331003072049051178805257039121019838819772094976028198845029226649392047423449649097936508855939843488619110961731475433787632477929630844265376562183032088627595785676106606148312290082174651362929375996570667921745229961717425/33640124994206825319861298451917602955121061234274990349087492992167766986562517477961744965196331749266497302689586668390671415211724327485939141426421688198788061881868151752370587450665656578161027741974259194482762165691241687928962299372715390073824741640064827221250247032234392669830221722710522614617935322966665888943092661399842251393852195503346260239101942404983814010448477554702219653922537984*y^3 - 1314844551938114605389652806701706007836395153061657012768694082213710666101426026425626866341918545555881093697067870239052051540428898275121954002407489422115108255586019689804557417799731124536154693776459798705019883527087418101243225078657479666770116059804857808980277227121290336575799214624782857701720840523713809327536164115860775159915172580996717732702481357159456120950620320106468681322721757979/386861437433378491178404932197052433983892204194162389014506169409929320345468950996560067099757815116564718980930246686492721274934829766088300126403849414286062711641483745152261755682655050648851819032703980736551764905449279411183066442786226985848984528860745513044377840870695515703047549811171010068106256214116657722845565606098185891029300248288481992749672337657313861120157491879075526020109186816*y^2 + 167890725904471824077330060936709494295405572958574665352555647645681309029828011879996794709883160271612598569518663504258014564168167002731530859312963314767956697522124245495998991838309005183482534443119593271124247048532990085287723186765478499350230686162662002332822102620457319805410063457552271681294584513966834938994942849725462197875626924520863516899613373332875509927507515939517866164011022479/193430718716689245589202466098526216991946102097081194507253084704964660172734475498280033549878907558282359490465123343246360637467414883044150063201924707143031355820741872576130877841327525324425909516351990368275882452724639705591533221393113492924492264430372756522188920435347757851523774905585505034053128107058328861422782803049092945514650124144240996374836168828656930560078745939537763010054593408*y + 5922153165961797879253730137349736708979739051333647774692753259846309646970230508034539483026913936207235668615430785148913543688809414603946496468455742062442383803256863023972297068483166997033382095007520373377158711207102601271987459371929377136075150571356631942905144707074461825329347008775593501531318604581413802636719504605856015350449023280486181094506106224511880683766459553490767170973944737/24178839839586155698650308262315777123993262762135149313406635588120582521591809437285004193734863444785294936308140417905795079683426860380518757900240588392878919477592734072016359730165940665553238689543998796034485306590579963198941652674139186615561533053796594565273615054418469731440471863198188129256641013382291107677847850381136618189331265518030124546854521103582116320009843242442220376256824176

# 4 Loop Invariant
214929391757372247993567938499679277330131196978827678858894239637101955895091530594617813247911342386998493834826760764347168720131697091244100408891244218066787424622537629406631532558733976919147479776357824392241890659532282259883009433625271045160231908633588776817278457286450291064963133624020528828130864092120717200274140203867332000229487719188987969425048409110219378845051745245615038067362596704692280994552100118686273673164145535204322009737083726507423023757138669955693926115610284528613052028747358710120380749675331064372293373802300315815057/1097255448389897185972039609908392730564099006521366117838521304505668816385579014300451685405125882588316191268027943898511763908180725951366456595175734858288327795007699914144890724368932454923848195093914937032928376394842426079269685304212171415712072786895641482359945224897931720853276356787696757228736600203693399704481340314793081608301227647754152490993634813713598743443238957449426570092325454729939478201002425479126787959769130435485752751697311413981164762985127455008213777341313081958814352086233755289748919034493726382668242509520588389552865935360*y^38 - 451588400594625166936143595624800231628988406317830289974760270622376853727888958795745397398374467333174832290792476078781606776837778936389747988771782532605418954320875677578221830685018981665509238642968763370365022114452692336590487705762354371066954621305186246076200298382276939493701104008819417968377624575052694958942455214344990675510011872090408799226868558091819504445586523659421281845377834455850527884318882565409669679997273674938684872695658190440795408514971264548598327664584864137464178657690814956044141459468677459285816983105735334432271061/140448697393906839804421070068274269512204672834734863083330726976725608497354113830457815731856112971304472482307576819009505780247132921774906444182494061860905957760985589010546012719223354230252568972021111940214832178539830538146519718939157941211145316722642109742072988786935260269219373668825184925278284826072755162173611560293514445862557138912531518847185256155340639160734586553526600971817658205432253209728310461328228858850448695742176352217255860989589089662096314241051363499688074490728237067037920677087861636415196976981535041218635313862766839726080*y^37 + 10630228028737422092082201194428609932234029770480550626893842512892587196023708743361026856550428316408577219267349595898991389950526194684942501077247387752380601473358606145220044957164032914901950151796173834099192347357485662740530762018112182633531236472245843255969382925045143159766731274210785970586327271547297870510921147191334874570430512552530517497294134899886291746561944252286222484320058987418035256728594060476289760010527043656575948080824995742604004952111399544433928414109124288086649015325107684239745467072854147545179411367791500060936559/3121082164309040884542690445961650433604548285216330290740682821705013522163424751787951460707913621584543832940168373755766795116602953817220143204055423596909021283577457533567689171538296760672279310489358043115885159523107345292144882643092398693581007038280935772046066417487450228204874970418337442783961885023839003603858034673189209908056825309167367085493005692340903092460768590078368910484836849009605626882851343585071752418898859905381696715939019133101979770268806983134474744437512766460627490378620459490841369698115488377367445360414118085839263105024*y^36 + 1000095691147360882931117495718984385593781951931807489166891633249748930094004416747657899382072690373717574071749385840813555167647339021159410012244357628448721515037423647835416800610683820921093569101518273403506508245197294954442112258495423115620289567909259512111989268034377258854629872612920105883712276646976383069994964443776575884406115272702175309848442611604317050443273014603233953252708024038496828720138976376872669470973064310772108750039636355567617437800807879235036241635292326812984088068521395016273930152456814659184137878220283376864981361/9363246492927122653628071337884951300813644855648990872222048465115040566490274255363854382123740864753631498820505121267300385349808861451660429612166270790727063850732372600703067514614890282016837931468074129347655478569322035876434647929277196080743021114842807316138199252462350684614624911255012328351885655071517010811574104019567629724170475927502101256479017077022709277382305770235106731454510547028816880648554030755215257256696579716145090147817057399305939310806420949403424233312538299381882471135861378472524109094346465132102336081242354257517789315072*y^35 - 82617300986399459540294494408130044844117235640751364729966478058922027825826022390592608261997145108105198090268920635564843050298862319502224958352313125427398850117078046359987990021958409771607171830336342413620085895616787804019484773398579683930480610898265057837729675957286244269226189154236493467378101466230527093384718996914249968334836702322779303505640626661111559543529917572026428240287969724145887471519603994064258417923834887737834038570934229572267072464736574093117538442532532222753937371758617308748606799816598607489915939460040418041924366413/140448697393906839804421070068274269512204672834734863083330726976725608497354113830457815731856112971304472482307576819009505780247132921774906444182494061860905957760985589010546012719223354230252568972021111940214832178539830538146519718939157941211145316722642109742072988786935260269219373668825184925278284826072755162173611560293514445862557138912531518847185256155340639160734586553526600971817658205432253209728310461328228858850448695742176352217255860989589089662096314241051363499688074490728237067037920677087861636415196976981535041218635313862766839726080*y^34 - 95138293990149743290762860147639800542152237266089178180444736724165808776329713249578690557830839597619772890852889730673981520078042587800673979681512848825853679246845209418319061918050695260205848431425541547284242726318142949666763068291139923902187438139014617748974803422469305040889498144494944024708316524304426953539422124185795439445876141865264893656530622155900473036597866481892035448670074623837434415668925893150244968920962445166661515572134908729027345284327395725228318903483271265675503126833551764386311408986345708572685236556537963148093467/1463007264519862914629386146544523640752132008695154823784695072674225088514105352400602247206834510117754921690703925198015685210907634601821942126900979811051103726676933218859854299158576606565130926791886582710571168526456568105692913738949561887616097049194188643146593633197242294471035142383595676304982133604924532939308453753057442144401636863672203321324846418284798324590985276599235426789767272973252637601336567305502383946358840580647670335596415218641553017313503273344285036455084109278419136114978340386331892045991635176890990012694117852737154580480*y^33 + 9877458296574969728430872620736294552741204727786345566232808864931202948529011994831205996256343061473952486841853177450742684639778438327669944296349371930334588942809554268963253250524515573688810910235017375074818835828228951262800386009078254084270639100526966767860953222086166337746992274476491363513374977475278675218013255275895718651190266247146158600750736271064625493891366634490772362303920554885187147415794805218788506335215788272779265541980166893597192598481906190139350778849088801055352122216553546934595019509394567167282093002609483978163817741/1221293020816581215690618000593689300106127589867259678985484582406309639107427076786589702016140112793951934628761537556604398089105503667607882123326035320529617024008570339222139241036724819393500599756705321219259410248172439462143649729905721227923002754109931389061504250321176176254081510163697260219811172400632653584118361393856647355326583816630708859540741357872527297049865970030666095407110071351584810519376612707201990076960423441236316106237007486865992084018228819487403160866852821658506409278590614583372709881871278060709000358422915772719711649792*y^32 - 67924829955995523180398850257455614452891653311172880988907463860877376861326491074256309149293946059314614726251177959535183316636758453436677226267722375357588778397790014390557241122708078129867832317996849892247587656584273034258951660608588364520650566524070967822542199792310250098218956732114732193126336980057515807260774355318111431818866784653992233854891248958494717083977340242676636704251540050221682333741451477614658710708057174370340936144938223632732312329736357210660942181452131866459525017980556828734415903332978623435356508015883614536397567757/2926014529039725829258772293089047281504264017390309647569390145348450177028210704801204494413669020235509843381407850396031370421815269203643884253801959622102207453353866437719708598317153213130261853583773165421142337052913136211385827477899123775232194098388377286293187266394484588942070284767191352609964267209849065878616907506114884288803273727344406642649692836569596649181970553198470853579534545946505275202673134611004767892717681161295340671192830437283106034627006546688570072910168218556838272229956680772663784091983270353781980025388235705474309160960*y^31 - 2865470190447722061565919895372186317021998218052878103299027297799364669410179959468521799497935203359996178576864845185020388264821136407702432517430424021833410328558432774629188160906088372219499880178541612516004234375166716909211536681430649931413404966913892518392006506832378207043987396642866712737711176549795436856241183030558401150278145363849732583015477001788193958059034721814171529791995397073310198197949561457087338003560956696197523505046919268398090013315979078422497279939301303236392274254414908635053727562942720024540433152562820771632383068093/140448697393906839804421070068274269512204672834734863083330726976725608497354113830457815731856112971304472482307576819009505780247132921774906444182494061860905957760985589010546012719223354230252568972021111940214832178539830538146519718939157941211145316722642109742072988786935260269219373668825184925278284826072755162173611560293514445862557138912531518847185256155340639160734586553526600971817658205432253209728310461328228858850448695742176352217255860989589089662096314241051363499688074490728237067037920677087861636415196976981535041218635313862766839726080*y^30 + 28506776013430850049778238912143674635681329572780948557651445669636377149970083813645656666482964459408926082579420399363763688406097512937286036463226538299881445959007850792697420312481243631597340781269574231319921440995023033585167959432400975497042583923083755091301031555902146321331997606542322906600641806211839518615738913464622479903190899529810726602129250842595409290437231643868966740593925676856269217957679737509420334021926622537599811458300864137045151128887199645734313728244515591102138088535430710806119694995649394242835081516991264994045383092653/140448697393906839804421070068274269512204672834734863083330726976725608497354113830457815731856112971304472482307576819009505780247132921774906444182494061860905957760985589010546012719223354230252568972021111940214832178539830538146519718939157941211145316722642109742072988786935260269219373668825184925278284826072755162173611560293514445862557138912531518847185256155340639160734586553526600971817658205432253209728310461328228858850448695742176352217255860989589089662096314241051363499688074490728237067037920677087861636415196976981535041218635313862766839726080*y^29 - 35164797547715470766531694914923154542118549845698332808840049716757446463603567942946375110801163140357270516417164718863865676012633816602798244327609626193806632415813607009847819336997895552020734894614575739501621032419436572370495884348412908875826254153180794317923551474040472675790573402982877563353849648669771748724041108303465813813629944991434583705477715471198269565156803874611604222547359868282888337952459892530969112663439778318967915272708696850610707157749413816562289186878482836036019123844757166172639561110063150032632194653595643845514586901507/140448697393906839804421070068274269512204672834734863083330726976725608497354113830457815731856112971304472482307576819009505780247132921774906444182494061860905957760985589010546012719223354230252568972021111940214832178539830538146519718939157941211145316722642109742072988786935260269219373668825184925278284826072755162173611560293514445862557138912531518847185256155340639160734586553526600971817658205432253209728310461328228858850448695742176352217255860989589089662096314241051363499688074490728237067037920677087861636415196976981535041218635313862766839726080*y^28 - 8451001222326326958102369719908171883017324818145919816414417782756638833409562751828506757441514838937132616425564150208530385553426176686561745017222698048944078869600626956841965218477226766538460919073379263982467098768010395649824329471951843493175275148009999153249116842470122681206247864343578498268498304343200618601936734725401799490521795210005416798089378610003609661537896867055598933327654032548396533063007698210422848650269571633154914431385541638653518687848765803469633905739259709814640430711632546668384368936148566369725432448409975133896412503323/15605410821545204422713452229808252168022741426081651453703414108525067610817123758939757303539568107922719164700841868778833975583014769086100716020277117984545106417887287667838445857691483803361396552446790215579425797615536726460724413215461993467905035191404678860230332087437251141024374852091687213919809425119195018019290173365946049540284126545836835427465028461704515462303842950391844552424184245048028134414256717925358762094494299526908483579695095665509898851344034915672373722187563832303137451893102297454206848490577441886837226802070590429196315525120*y^27 + 22172343863790495723775686520259738568273398137271474686210584745315892202569292844210839579991645087667207760909627898621187673694689168940440364004885049103268717619914764685910900382832846005462574475268095576421143308418466825715122730383584332735514710423092519064373395807176518814209134922797862761491120705993638828578892791065812257088051676800268942115015820894719455898051979626286268809885373862450957909613373903408255459630669076041363823484521408155473861575013852302075068094088727138333473900429042321271600315064783362727664505541381510064429524179683/15605410821545204422713452229808252168022741426081651453703414108525067610817123758939757303539568107922719164700841868778833975583014769086100716020277117984545106417887287667838445857691483803361396552446790215579425797615536726460724413215461993467905035191404678860230332087437251141024374852091687213919809425119195018019290173365946049540284126545836835427465028461704515462303842950391844552424184245048028134414256717925358762094494299526908483579695095665509898851344034915672373722187563832303137451893102297454206848490577441886837226802070590429196315525120*y^26 + 53693377841636817344926578681373881359653052055122948739829662000326902300006558018196192005685125799034905209704150152474437444652401001700361897818214056622671746478623775596753163652981760278192859193604403496335608735220760482131700565258541495524740701648645971193642458642001465100037933415133902685740920127133897027504508709206349407856039804301143657003808841729542445209017409236691596372290160282419617809625533821804017380344791485611816049550810784825250492920870033736548215697449690722647213830449636824507610973999676835567773951376809640787762464260331/46816232464635613268140356689424756504068224278244954361110242325575202832451371276819271910618704323768157494102525606336501926749044307258302148060831353953635319253661863003515337573074451410084189657340370646738277392846610179382173239646385980403715105574214036580690996262311753423073124556275061641759428275357585054057870520097838148620852379637510506282395085385113546386911528851175533657272552735144084403242770153776076286283482898580725450739085286996529696554032104747017121166562691496909412355679306892362620545471732325660511680406211771287588946575360*y^25 - 22294717189489050288695110728697031902024433826090834812031904290733795562851577008593200911225386869909714528432102245725527180212760077386732683931348449597428696705990068504447931766587468841811067751432663547859164873353295333797288019935118656101846383182362434443785582374457749446691103249598883053333180706215838477710549784816995007992179069997762458502547352757216890070035833963340583756179701367958356437248873879288427723933952288524354135289028372050843693010036344984592477030196650514816915491992991599581592669568816678302233741526301885793737044977953/14044869739390683980442107006827426951220467283473486308333072697672560849735411383045781573185611297130447248230757681900950578024713292177490644418249406186090595776098558901054601271922335423025256897202111194021483217853983053814651971893915794121114531672264210974207298878693526026921937366882518492527828482607275516217361156029351444586255713891253151884718525615534063916073458655352660097181765820543225320972831046132822885885044869574217635221725586098958908966209631424105136349968807449072823706703792067708786163641519697698153504121863531386276683972608*y^24 - 529241647294530188203455092496610977190374676391500077706549230353893047008610558885895279708668653813337631285081971764028514588739253872206293206203636216276045702814066726336923682333351895148364138320850794061524625979857116234027188325619700882819925887744757815590264623829454828450149599611284235002815942557611724238388317015780932714943235769672368106656143985748874234017169218549412605137784836966844696127594308121991297357448275225871660479105909835974665452642327325951257674554804973603144035089101436950594373412348063324822946210857936731691073440930187/46816232464635613268140356689424756504068224278244954361110242325575202832451371276819271910618704323768157494102525606336501926749044307258302148060831353953635319253661863003515337573074451410084189657340370646738277392846610179382173239646385980403715105574214036580690996262311753423073124556275061641759428275357585054057870520097838148620852379637510506282395085385113546386911528851175533657272552735144084403242770153776076286283482898580725450739085286996529696554032104747017121166562691496909412355679306892362620545471732325660511680406211771287588946575360*y^23 + 202909552913495296197737843405434556619902425812626879323718871237123393776001533005488114319007644229787135458803868333938372857961655733714468476755904931141064764007989787112258265204652710122416481231084140276300882975862086502720622241213938205144301494739009711280177624350485480428594572766760251235510467506228253646093326789538905023531780343804218313579574817148177458381396733009508089211862889205567504640462543392854078995072955926397611900355446865000513298086547144426430527062798569294263310705386049754466820497083784817903855765127750308162327838738767/14044869739390683980442107006827426951220467283473486308333072697672560849735411383045781573185611297130447248230757681900950578024713292177490644418249406186090595776098558901054601271922335423025256897202111194021483217853983053814651971893915794121114531672264210974207298878693526026921937366882518492527828482607275516217361156029351444586255713891253151884718525615534063916073458655352660097181765820543225320972831046132822885885044869574217635221725586098958908966209631424105136349968807449072823706703792067708786163641519697698153504121863531386276683972608*y^22 + 1078477410796803078372421702437672617926049712229987363591467242689732447197212959935147949830126517564731670910972194551040309587789251769028018628195262312446145331052582445195806813915204697119934468478626864858304056705469370001940727784573001329358406720172213950794733849682547706606232352177683840716391132883969176028897979060435272182290983304548454716657142573279362918209837110757700362162248898454039628189284338457614355477714732231459910370332200899171949444099416536113002283188235859864486122351471820284633363121373597142690753099490707861659772100295293/15605410821545204422713452229808252168022741426081651453703414108525067610817123758939757303539568107922719164700841868778833975583014769086100716020277117984545106417887287667838445857691483803361396552446790215579425797615536726460724413215461993467905035191404678860230332087437251141024374852091687213919809425119195018019290173365946049540284126545836835427465028461704515462303842950391844552424184245048028134414256717925358762094494299526908483579695095665509898851344034915672373722187563832303137451893102297454206848490577441886837226802070590429196315525120*y^21 - 3031872118225550413215159519865338132803411139727570869349186743309828934159985895080870882391549028895848005746335182969173550449787700968064161152506500422539425050990920795306056418523945422533917041743028596852552136847431863896705432432381252848277444837856265358486675495435033004664550072908862213306696187100921342771503255777176522827768311368055068936143432330505032174276277364366460806102151863050379517376863134094879126090853063478466538284806254882215849022146347468422724390272053871485391982097131441662430540718070205003229379737604074971794258722151753/28089739478781367960884214013654853902440934566946972616666145395345121699470822766091563146371222594260894496461515363801901156049426584354981288836498812372181191552197117802109202543844670846050513794404222388042966435707966107629303943787831588242229063344528421948414597757387052053843874733765036985055656965214551032434722312058702889172511427782506303769437051231068127832146917310705320194363531641086450641945662092265645771770089739148435270443451172197917817932419262848210272699937614898145647413407584135417572327283039395396307008243727062772553367945216*y^20 - 33207764698518469579818983497737984462454122171224795957053079435621254359409370311079153279651889779352967524301966325618310394812501986157417914470209654109651180620130290201323831103936912784789157530193312131232855584192991355228276114484779775982384919179935578189951111886169024986390545599339142634639743950015446469324039427921332071760489785485492115848303137836812438877824245839653265562235495618059268699336150315752984282844223130450642036745865465861429291309522523753447119889491357702029163181642468984307383742466166153371829209015893948809591635659036047/140448697393906839804421070068274269512204672834734863083330726976725608497354113830457815731856112971304472482307576819009505780247132921774906444182494061860905957760985589010546012719223354230252568972021111940214832178539830538146519718939157941211145316722642109742072988786935260269219373668825184925278284826072755162173611560293514445862557138912531518847185256155340639160734586553526600971817658205432253209728310461328228858850448695742176352217255860989589089662096314241051363499688074490728237067037920677087861636415196976981535041218635313862766839726080*y^19 + 51341458127556592899406338254358441479546107227259161176766763013097413732179412583934431226800760807137087539914020992141491521998061157482376037344733294152052229016177494677404501134047512226655756687675330155337151209234966477411523404482440569772097831030099035121471684530783967392834539140479030342129646671802700632716911179498821847872543936903757347489831827559088745457766392022371937877208069333786620834970041248789747778949032500401310545879535911568745693876310303430643344634773466748339666684697077624641662565857170489752211890946034845759542095609456933/140448697393906839804421070068274269512204672834734863083330726976725608497354113830457815731856112971304472482307576819009505780247132921774906444182494061860905957760985589010546012719223354230252568972021111940214832178539830538146519718939157941211145316722642109742072988786935260269219373668825184925278284826072755162173611560293514445862557138912531518847185256155340639160734586553526600971817658205432253209728310461328228858850448695742176352217255860989589089662096314241051363499688074490728237067037920677087861636415196976981535041218635313862766839726080*y^18 + 16006104010643058468293784487644958478309918238262152588485994038330582717112848726492424380900688212352254585387078020015998142230355876962531512394987920531188772501004362777537483685162426698536653297141200374637341765928154166927805269938142999199934996920141704979345752006508693346893905470287176510754638814229093751774318854355273785220112462560826724022010978781435211572311097514302984657383032699782771146224497340425522861601704156903790972394241803578208752601464926997582160009261816386591509107862452209499504432266980234616539831047840004619644752459244713/23408116232317806634070178344712378252034112139122477180555121162787601416225685638409635955309352161884078747051262803168250963374522153629151074030415676976817659626830931501757668786537225705042094828670185323369138696423305089691086619823192990201857552787107018290345498131155876711536562278137530820879714137678792527028935260048919074310426189818755253141197542692556773193455764425587766828636276367572042201621385076888038143141741449290362725369542643498264848277016052373508560583281345748454706177839653446181310272735866162830255840203105885643794473287680*y^17 - 36819106911294767936464052843790092588691836733735866573423106763727712468455563380108034240200410339857652254613225030469508259053334037109939081949763374515918010565927730545224913125930339338625743954742662939941885004357732246825335912138679866125959596745315895055650053529182269219218504167731556946608875160711767554751981022396373081863875152445770190275383677168043823612525669993993128301215176763771027893691709582481543206588125227797352842446500566939364913207540291726357428478081223312241729400130352335696023387983446006946577178954350583480884015922257679/35112174348476709951105267517068567378051168208683715770832681744181402124338528457614453932964028242826118120576894204752376445061783230443726611045623515465226489440246397252636503179805838557563142243005277985053708044634957634536629929734789485302786329180660527435518247196733815067304843417206296231319571206518188790543402890073378611465639284728132879711796314038835159790183646638381650242954414551358063302432077615332057214712612173935544088054313965247397272415524078560262840874922018622682059266759480169271965409103799244245383760304658828465691709931520*y^16 - 8206842131169870848885925583810965154795539736260355526850070639186636622870070584419887442169291045341530228501112608982338441642014022123489080926955307203250085835813490491291692560451480989328060850580729114061695439244727338952912442060801516664366931652229198609908077083824082316193723959465977267044594030537516692620862792682757084819792167068270199077863868387203168687103980264615319292834391099258774600993939499634403115343255347219858242844374841824861238157741028175917569623507401865561545055113908932077721552149327292732338284460826619087266215575139431/4389021793559588743888158439633570922256396026085464471354085218022675265542316057201806741620503530353264765072111775594047055632722903805465826380702939433153311180030799656579562897475729819695392780375659748131713505579369704317078741216848685662848291147582565929439780899591726883413105427150787028914946400814773598817925361259172326433204910591016609963974539254854394973772955829797706280369301818919757912804009701916507151839076521741943011006789245655924659051940509820032855109365252327835257408344935021158995676137974905530672970038082353558211463741440*y^15 + 1922073318703397226511274167270341826227728717014846592441292638451711177441012764276667739292154397154538480220161605748929453290439951222324981215697254668410726825802584786223789609741652763730735830033803786369414380769938327609235791041582884544033587064026675898897609081648779552136427279757875077093904476901688587968202370018443095959682684471987534977283984196031561410723510152663432186689362414233289314112961546378145080241526291264858654319143203640160241285119534831903143975747527832479878202651681340945695386140794990280277862946287153823241283553489267/975338176346575276419590764363015760501421339130103215856463381782816725676070234933734831471223006745169947793802616798677123473938423067881294751267319874034069151117955479239902866105717737710087284527924388473714112350971045403795275825966374591744064699462792428764395755464828196314023428255730450869988089069949688626205635835371628096267757909114802214216564278856532216393990184399490284526511515315501758400891044870334922630905893720431780223730943479094368678209002182229523357636722739518946090743318893590887928030661090117927326675129411901824769720320*y^14 + 1487837663451044791581332867027986921182218475617354334876848461401299765972192125405572622175487718619331740385312381854064906526254023174645729252323202688488360402008178844435485967641168195368393764998973264531995210343904109090724992778594069466898534608714851737818725832662952988593151433172010681766149692756617319232454651630063170949601299221553433659860025576136012870251324677300563047574686996173236968537454559583891583445541615506570417009015217191952951471073283359112900237825261631152998117284096154502888923321700253120676244516897673321833641314875879/438902179355958874388815843963357092225639602608546447135408521802267526554231605720180674162050353035326476507211177559404705563272290380546582638070293943315331118003079965657956289747572981969539278037565974813171350557936970431707874121684868566284829114758256592943978089959172688341310542715078702891494640081477359881792536125917232643320491059101660996397453925485439497377295582979770628036930181891975791280400970191650715183907652174194301100678924565592465905194050982003285510936525232783525740834493502115899567613797490553067297003808235355821146374144*y^13 - 39842984139456870174778371506330384731146292673976845996442230213652955047508121762840411128578531130425552793354462163951938266380722432339064645490146922300941217750734077171650602021428937164118196036738957674955893915565543963748866668653410818423307215754593802887040465137740363523528625158179542224033748858663885340814284494039569230690187661885071913726326085368070042754066087923485267934253105083402558472831215923345212207583697573786212283985668014808625099902527994741890930677308454907565560684694070341979217069239211500196327779030597955107144418992243/23853379312823851868957382824095494142697804489594915605185245750123235138816935093488080117502736578006873723217998780402429650177841868507966447721211627354094082500167389437932407051498531628779308588998150805063660356409617958244993158787221117732871147541209597442607504889085472192462529495384712113668186960949856515314811745973762643658722340168568532412905104645947798770505194727161447175920118581085640830456574466937538868690633270336646798949941552477851407890981031630613342985680719173017703306222472941081498239880298399623222663250447573685931868160*y^12 - 1996869639475503361147753843004246183220974626219863287940100876396557513345114513305363455062108309237319102903081582879021041734098817347162664080780276237049314109870201067058845245929144789312828578536153194633859007345545405599208397444792470315574678227352521927118707408657522440964179780369855481539737361427786611173300356054576375719734342119131989635323378724725687559308532996267200331452193921222004797970212346014625633264834521110841688010833376938223923395827840566866908777994671702854359631442358812905773158636627341026704632894641836000705426845850037/548627724194948592986019804954196365282049503260683058919260652252834408192789507150225842702562941294158095634013971949255881954090362975683228297587867429144163897503849957072445362184466227461924097546957468516464188197421213039634842652106085707856036393447820741179972612448965860426638178393848378614368300101846699852240670157396540804150613823877076245496817406856799371721619478724713285046162727364969739100501212739563393979884565217742876375848655706990582381492563727504106888670656540979407176043116877644874459517246863191334121254760294194776432967680*y^11 + 262988463185751676361543021250601352464253928979528598804976788146714661534851074142172022764894625584821020364313548506030325621917747823027598984859791420779378355180539860774073635993438397645239418741019275704865944813837697895434177989933134071019229372050212467979209331218623569805191401083530920112575083534828318832359165775272434502396819137467116309898572734691001478151816175204020978560477632745783783305797744350924351643049108394908434033057624557903368394453880519074590966808434809233191859599520193533161350235616876252586267758761710640484380083205853/548627724194948592986019804954196365282049503260683058919260652252834408192789507150225842702562941294158095634013971949255881954090362975683228297587867429144163897503849957072445362184466227461924097546957468516464188197421213039634842652106085707856036393447820741179972612448965860426638178393848378614368300101846699852240670157396540804150613823877076245496817406856799371721619478724713285046162727364969739100501212739563393979884565217742876375848655706990582381492563727504106888670656540979407176043116877644874459517246863191334121254760294194776432967680*y^10 + 28253161161406813449450604323457081456266115155711655729921683468425981978996149403756815182843363890670960118860406639614791046220324360270508367899050042630376098577521669543928906933098089748044496988843339141253250631433765300367353187309402693284105071338641473560388600757308054175307147036899157150033509740827666413115786157011048430778239819434940719807353379186844310843538590193851744893864286768712108737124198746914974319823112690342471484511994495851240724599783960735154397903115399132259502474020226013265379917922491062070068720834401769852991728526799/11926689656411925934478691412047747071348902244797457802592622875061617569408467546744040058751368289003436861608999390201214825088920934253983223860605813677047041250083694718966203525749265814389654294499075402531830178204808979122496579393610558866435573770604798721303752444542736096231264747692356056834093480474928257657405872986881321829361170084284266206452552322973899385252597363580723587960059290542820415228287233468769434345316635168323399474970776238925703945490515815306671492840359586508851653111236470540749119940149199811611331625223786842965934080*y^9 - 5998769400932654180378791882435352217006365330292929299145011619763693989514656983646488056939243299940921201141221878101039210216286901966743790857646322509936817828521662625744110792533258124969819805755105833690829047838371369096467434136311395865683295854402311218368809328691707604624001908793047839343848376498354429127510154848104600834446124561949166475780301316030625926297322733021561602837531278546361253263587313713976657015213241506464436604005287457636043329987621681797118349512789338382652445840241192374202304425349728948666046229404681153492863034251/45718977016245716082168317079516363773504125271723588243271721021069534016065792262518820225213578441179841302834497662437990162840863581306935691465655619095346991458654163089370446848705518955160341462246455709705349016451767753302903554342173808988003032787318395098331051037413821702219848199487364884530691675153891654353389179783045067012551151989756353791401450571399947643468289893726107087180227280414144925041767728296949498323713768145239697987387975582548531791046977292008907389221378414950598003593073137072871626437238599277843437896691182898036080640*y^8 - 8458530886648313538681415465626002720877836323457993780246832222367720109406369148963506465928384785564079501151220278330186195805101820361318712497564463463194994083404145355936693541970279186871613385108727996810760002894552137228062070342661433303449447734362093436880286584129035161750895012806647284758292726160436027628169348850496730028760337792323540099363169340803125839586594843586156216265304497656843811610037584330901932434158987998037174111603356763563322377402748555552417223593774317383035254317686289928743903207405652697113326370060964856641405383387/8572308190546071765406559452409318207532023488448172795613447691450537628012336049222278792227545957721220244281468311707123155532661921495050442149810428580377560898497655579256958784132284804092564024171210445569752940584706453744294416439157589185250568647622199080937072069515091569166221537403880915849504689091354685191260471209320950064853340998079316335887771982137490183150304355073645078846292615077652173445331449055678030935696331527232443372635245421727849710821308242251670135479008452803237125673701213201163429956982237364595644605629596793381765120*y^7 + 616841713338282920656735284875364369367735967618399647598482866664123636809089464018114560999620959580945813611078756299353934095884598856013419439734124490847185614589773129396442010000135245792993615819291343651886069224097073137004379559126508317624527055112151023769328163788268978169273419771198029745283501326031234169324306336253436851081453354676445886491459521253231363757563179246458974108022760034417042308270170514216263539883081650710363426158327982329348113398030181858311764271534175127210864758658368381294620565389528698347470994352709567836894774537/4286154095273035882703279726204659103766011744224086397806723845725268814006168024611139396113772978860610122140734155853561577766330960747525221074905214290188780449248827789628479392066142402046282012085605222784876470292353226872147208219578794592625284323811099540468536034757545784583110768701940457924752344545677342595630235604660475032426670499039658167943885991068745091575152177536822539423146307538826086722665724527839015467848165763616221686317622710863924855410654121125835067739504226401618562836850606600581714978491118682297822302814798396690882560*y^6 + 4458879655314079932463436577131516480090977272881405142126461976840726561148259687907748886843287466312559559590930324954087937110106268422248033878832987113628250239319387145153070546286700572031390868413402147219328947816647733226272857082044489902290658557464985046837404478024578711986564249187868209611195832369116765244089463266525328354335121742026856573271805252483524468090815971225499413296971249195622824421321349774876924316749030863930337290725205649077294271137741183621464450275063415986555491263869084870115775378999174891177135911655874768990781444511/17144616381092143530813118904818636415064046976896345591226895382901075256024672098444557584455091915442440488562936623414246311065323842990100884299620857160755121796995311158513917568264569608185128048342420891139505881169412907488588832878315178370501137295244398161874144139030183138332443074807761831699009378182709370382520942418641900129706681996158632671775543964274980366300608710147290157692585230155304346890662898111356061871392663054464886745270490843455699421642616484503340270958016905606474251347402426402326859913964474729191289211259193586763530240*y^5 - 217559101609222286767877070843819062301029175269933804997583579741922469133819436200969838983550848774106586043256606618807135578349492512536917675266350945313966604869652635067554083849612761342858580592371890033669103921170627873851943106473145525077369480467543095308622332471925480072201815684093709355230780231296532970475551160657523069498043145928424273218214806375472955275713522789247524512914264966062303856282842665307266943038104938476085219358029667431587876706144037436321184616771562354925835378626598682450964500719792953794848147947014935704048438631/8572308190546071765406559452409318207532023488448172795613447691450537628012336049222278792227545957721220244281468311707123155532661921495050442149810428580377560898497655579256958784132284804092564024171210445569752940584706453744294416439157589185250568647622199080937072069515091569166221537403880915849504689091354685191260471209320950064853340998079316335887771982137490183150304355073645078846292615077652173445331449055678030935696331527232443372635245421727849710821308242251670135479008452803237125673701213201163429956982237364595644605629596793381765120*y^4 - 7020724294548643409653696916131918247666932076499645247771695360569921766328111647534654630641632468642228067301807594163942741842796832747185082413391442093271074558030472325056398764600578843847539313079416641839397842330285471467101171787039784748264885679265605261179342808689665838962418466477570610620891557371613600055143243709467691595912977119454926516513363589560449219910596639250738916735920340159579363061890564550311617362888296240164434167324974429844527269639040820664884379344915551161067972222979208416043582914025530094307500063911209942343860387/186354525881436342726229553313246047989826597574960278165509732422837774522007305417875625917990129515678700962640615471893981642014389597718487872821965838703860019532557729983846930089832278349838348351548053164559846534450140298789009053025164982288055840165699980020371131945980251503613511682693063388032710632420754025896966765420020653583768282566941659475821130046467177894571833805948806061875926414731568987941988022949522411645572424505053116796418378733214124148289309614166742075630618539200807079863069852199204999064831247056427056644121669421342720*y^3 - 11150129981842519682071267640103134263833638327410901865922234428398342276215582722577644133205235540547278772054949523737535245253429809805111206946833246228327330252132449702529734957784350265099408431117077581579097083201487967106732661747995859198233189603209684355544937132864069368027935110980467178956638028267605320439333417786645045585389960821178800696932970623516823816778829358288247777269664605175982793016862112262695448907860198720502183333732238157610910690236164685097764254301983502582868402619340995651005886637280512890180404867723334535543510567/2143077047636517941351639863102329551883005872112043198903361922862634407003084012305569698056886489430305061070367077926780788883165480373762610537452607145094390224624413894814239696033071201023141006042802611392438235146176613436073604109789397296312642161905549770234268017378772892291555384350970228962376172272838671297815117802330237516213335249519829083971942995534372545787576088768411269711573153769413043361332862263919507733924082881808110843158811355431962427705327060562917533869752113200809281418425303300290857489245559341148911151407399198345441280*y^2 + 286987145471299608856272800934130724377698404185990227686488241127862274612634678784754492865109951722153306796704111189007239859980402608328074501768124352767899067690305735560852318501782978065957206132470397096356018327970539060780906659455317427633103692146779655193099389115531726683791896010348292458168423064623939514376673478514508042969488383180456722197128845107435396146805182122197370490519226592321946816483549379317228481012164690807846172174725675051886829185892170629849129828779136175688637757258683637622652984883630838010200992566736079274350557/214307704763651794135163986310232955188300587211204319890336192286263440700308401230556969805688648943030506107036707792678078888316548037376261053745260714509439022462441389481423969603307120102314100604280261139243823514617661343607360410978939729631264216190554977023426801737877289229155538435097022896237617227283867129781511780233023751621333524951982908397194299553437254578757608876841126971157315376941304336133286226391950773392408288180811084315881135543196242770532706056291753386975211320080928141842530330029085748924555934114891115140739919834544128*y + 195548519875967620677129246929494709442685861916089556791226098826960970716701263693619154005208257105843552809396239949281851039835058160839329806566478794196353005716606431925831258078538565262497073206626238198853025547880328713059078133918113733341020268591896780942833691266550029013493452321047403928876019064771673217647783642914323649766724798891391484406464437035094123191043221313528456529071345897718439317473041058150416104207134134844938571322120013621499250059834390161522781368801330193162924993057465857303674489494635678200170277537096473020323467/535769261909129485337909965775582387970751468028010799725840480715658601750771003076392424514221622357576265267591769481695197220791370093440652634363151786273597556156103473703559924008267800255785251510700652848109558786544153359018401027447349324078160540476387442558567004344693223072888846087742557240594043068209667824453779450582559379053333812379957270992985748883593136446894022192102817427893288442353260840333215565979876933481020720452027710789702838857990606926331765140729383467438028300202320354606325825072714372311389835287227787851849799586360320