# Manifold: Census Knot K8_113

# Number of Tetrahedra: 8

# Number Field
x^39 - 5*x^38 - 203*x^37 + 1092*x^36 + 14167*x^35 - 41585*x^34 - 700486*x^33 + 3734171*x^32 - 2541083*x^31 - 54511843*x^30 + 37222281*x^29 + 113652894*x^28 - 5766446*x^27 + 139332022*x^26 - 69540810*x^25 - 25060632*x^24 - 249153248*x^23 - 579379233*x^22 + 368717504*x^21 - 32712438*x^20 + 174378737*x^19 + 296381743*x^18 - 275172309*x^17 + 318148904*x^16 - 58351804*x^15 - 150950597*x^14 + 52883834*x^13 - 1047574*x^12 - 8026382*x^11 + 6678317*x^10 + 388454*x^9 - 635849*x^8 - 4428*x^7 - 34064*x^6 - 1840*x^5 + 5772*x^4 + 215*x^3 - 165*x^2 - 6*x + 1 

# Approximate Field Generator
-0.585965512009671 + 1.09903570706539*I

# Shape Parameters
356865612038465748007372932770487295979455301301661834983014479430202113451698588006059749839258120400974793595865932708953586027227954269205335139959925220755388618921741069858405407428314041097636908335974/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^38 - 96620945867565919826225804950738945816381838341882179308657542955398053180368836802969156975017715106002725965220377901212509353425044900491643618392684656971231991531022060112975992969602968797825822653299/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^37 - 72181593067421020609417467607979680621232253627756168334476476034587964189708257784913922897854952851532153503117071252894549748224557342466463182801289189800151168056100360021837955547180846975882185221830667/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^36 + 400121141407243624059139696806686654764146163003554405460290081573517047111572821816826569478236126803187362561103029028242295287541955355234409579917851864999660362361787526520423593419716435352919294697712419/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^35 + 4998543226766289225710136337142022540078193627329438397848634196117527900013954362124091750916113450667684388881553661765881986152259522285485159537821653461748521919295118790576136118309854811735849809064608095/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^34 - 15564088689686130369326707864988706666927624857589894267527793207616686909889416568137057943576788790820645281735550962605665883792806231047065042848312945731254332639960325240792750838261785579221178722308553621/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^33 - 247771954381245886998161423042535545812440953554187179541557252227136176060844448403079004943450018564641201574309875715650046282387176191324980822376586852132588570635605058083656625562330236837059551179233371538/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^32 + 1368443607338261118201345066990012956820186187280174776824765314234385662198235291700516715541028279596727285603974328837485798821699710226877747379369185446835541575808143246699529509689580697430700818533682415690/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^31 - 100213223780823733370639893551987182756211526814911185043083123264639358847338395336932420748188603073031340821538912114859851491768450162711629356328801846844452881679225753521729964697006365527745706956819470458/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^30 - 19304336856150718228565932702496468762347551325905721379864386465321774201412953182262589162909951062821041812221609585165368842232494241788005909675511576219383090400152573822687969218282714036930285262956286506424/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^29 + 16074759538538591562340298596958382048286993130657509141383236566369274251105477091308204662516498354059931124517654309300417737901353294704546928099494481145691355340177999879544901377603821213136108165095432691848/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^28 + 38383467332476875165966568350773126762150795153538494564448649129038307147639265876001587498284347099990362997839501053424759960667825693231039161632290685346133637602885955949432473056427641786436604934370776672259/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^27 - 7695582773039646733812518435997771014455348526807271153360832028862276634245274057036304166103821276078348387526766909058102374874101919743698930192762298638327036514448819305357404910715720489485863226642314374675/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^26 + 2660485815223589213879869835360270152070751798227974011470977889263760810896659946595019904194008454462638434777174064063987463286383060450094829285233297362223293106226815578086326066164573604346404793789184394451/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^25 - 32094032709610873316599512023208424613550754818135345256879956776485515658268739024805288456263436391064998476980502664603626813721863645199186987825710143940848201925475984102035985911650271287272967432935221799209/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^24 - 4712599086262888370606162372490879866458127844224615696099462496052949134003562313824497619040080292392171055431499791515929783327914087759554843750361958992090715111907921643498696609395469378324687333192189571092/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^23 - 88039149102819877713267411686057546613770328158356568878748823302185930955928239380343596822161355701491453433771253846196074999817188506861078320941537470728976082479693527477997358191152524707153493375832812681152/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^22 - 194042259166073872148490012085429180052456486695078463131124940687422692135844818087737152822924084013288393500924059313221373218321171077615621731745340520772538102314424553626405780040800676753805410445704193281913/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^21 + 160246116454884891726376340324877945431694028157795792144169864248733087750340883070555646533830628428068527977191286268941164725420319726504457248144636852046541291185083060352209019791381764284071132827922549085430/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^20 - 33268394237256118333183763116712477122524129470037258755831328894830567405586035342130688173394747190087018822035743253783401452693186297484444102344383760993933133671498125526277465742440241548556875350367245784815/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^19 + 66078839920639814299469125465827175660524097511874978516568235340515392070312478456374665944886834432686065294677334849985300175714258849090783476758291567965405829823600453808178904899494662995683938555178074932776/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^18 + 8773356224001381046681053765383065355004399826462691987334354381679080340252030697702100819956666783371702749135269246548766659687934031699290802328109546057119847745970438734939184575480024544883711863859211565274/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^17 - 109078481920137000516228282285689833585189897253018696827250662791672218890328474508320330107829778329853119263560089411575036784236286740799665833265613671744064294842140632886675660114603991722857030177150447367/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^16 + 129043008251882294893145985630466640233984462593789381957007065718799630704317203042292897857931893258509454010333526108952316829860766053065988318320672347622725344579471311463937045717973156495667978288711183324330/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^15 - 38742305079485992304719766652918882003255700834913123651147554467368434132131560314851735176451544537472553688734354428192953528218730858305206312860026643182951397187919249738437005690339132569533273388649442128400/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^14 - 4474553433596637267653795840265977184074927279957103387252838612362868107185496590651216858473383937997360718162074015891471410669573343238782667064174787607859268902350559387759689549852666882140887079062545265768/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^13 + 26219165350307594455537283742342749482230403768872239343873959845127570816321840049371244457350501851238512366571843959512298281571883745105116924305750931774077592684466712846919143078969650255461260647156278646216/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^12 - 3855538456410634576743145161097155713172111089899669451884583682131385037563680956293548716787232230393966223406894827781222535311553868663420191424199120647244900655409486083083754166578877825001836503165375921140/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^11 - 2434580306395765941554351959087649195021043835197006342045990851141713753745948421216530330841412773075470730300204393894894826631300250744938888362823653880197722885191522174016222712871254069309717411654734567120/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^10 + 2771783222039709092464469575763322922421244974646700414316381898164040824136779786238938947938242360720479281211787011294138476789459129638965078708113328224423442564797638924032479077392514680448939870092962642358/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^9 - 13301419200127231443276057892866056979914291453371795625892604123328005326888125002899466453978698229451775378898646350205072799583118939475103786452284472100825843630949958114858066729629414184067743389728048967/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^8 - 204861814546504694067768530968356443599275479876500889105912787232558659150097695758964693554897039458314628682205257541989499003217096620797874963110221714228542671190467826929726485262733349412627634897616540253/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^7 + 28309130029931313645345352875397208926142450997227515007325515501458209112922273297829288191355570185505219723435078856186376743293431343735782138890624808032039800484979755027995727555216766485133154528404766244/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^6 - 16011389323470905248946761156204829984704513773488609838055046587566824314124327416676833393035718038844984811383594062600371877548519272844450209046533629920464787591673676254367899006989813645645330496983677444/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^5 + 1651200178573429541775673130717233980051829302472633952055679602886910779175344688226273089039134077321112281050679942652383681990991605869298443730071112911681915499814895346693345318819984066508535182503945113/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^4 + 1933036765474734731520853481718682143939949305827510954817789526657428010294622442078989181474495235683581098236693377808703500388748795190385128544226487386074077848643223023366279096703360530262479581136342654/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^3 - 200675506530915540965882485017776613455629887331920006373264132111566362091188884640325441165932128998871382582199087471674509828780854884844141003367669271390835237410794024191375637220643131336024433714731663/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^2 - 33763195627131379555046132363075745053438608447904830410957630307413286942770320842997399164716586314858606234613665996810443133911908491712451357786843214577923974393159741467817908911825360021734322321937111/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y + 3137544671864413864189214891678349274139245377714022052792604730114522996851028295573116786767570016100622403393899722763951758200411050507368903789200489656848837105963845456366053101340226674346578387949055/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247

-189426270986214342108369248071412084606652491075536200169393748318277507363521268349963907235179098054658857177914880909746809330173852037684520421063471095437916026629845695939889114854854471841768593306503/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^38 + 51038750055919241904856446363084550852702663764455154198273532628839012626920341972167810682275480239127831780166824466886715793202777218528748728032436000324969257651867060601517191349595882298576066414194/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^37 + 38334069497459794462058164103619661973564609418806491879867085909654103362642764950344613633605391252779804348118891588105994905968386909817297150835313154477908011204538430303943501974521007357439425078695965/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^36 - 211409395364193746415865418510794401786077948827673836914123647237137075048953058472618985208576953965633244959056823301047024908532774226169356562343718629881129011755624153570042778207012064856052761868630049/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^35 - 2657614123832670751970630190550771065818314645548453510100875852623145218629243903674785417786936563697974042532072186087115834554197004980326676183921774684250083798004471821944616721870643844215089424723394029/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^34 + 8190365113409638643600874595338695264052833294211657881650977679825816224041678638533379005993101340780760398018279920916061842588372015747748480342463620404970130804355518747399299515768073175579651386981221848/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^33 + 131660031462615905648564196880844765289100349521465777616794220516221778973245306707517623351806347588673014479169973517085557432016686149805184865316471485345741984613840762070958081262454014947638523468609916148/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^32 - 722907338787544260166324007156368264226435807721427718289924147981224712206038013405798394223159696210877510745608075438696084818562068918252731151310103260746126433519595821192207090635039051515745776286617935805/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^31 + 51839557948979974741809557841418473540864836405920371710269144138955850584809697545062477954415371755266935237379352522546233284150602744056055811717137355908737173649442092712574329820219834124701471928077397419/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^30 + 10244020993974428915364098393625821943964413907528119295238532016155490531539903644476039461863850105953612722663898138512514832025298434124794338493380243444838024907155874972437510075033535723219303495884682258361/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^29 - 8263921592638212736061366749758279715626474595920067231182245810850280607690125870000485599399987924726781168334057550795513556366693348979033838601740607569233432428995380538068764928513478226832411016073367018393/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^28 - 20339554127408148280280257063180310894073544157160986933235694848436850237669522962197928023380110080765039808120383838548722013024440685575367812600160847427131487257051579268159165950819275363614296821944411328576/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^27 + 3385169103150960014339596285883326719200890762073997977069679603224605981443085436364536957974338611279990875687818858536020656169442596712875230273197215706814415970271006776607183765900668869316179661842987175576/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^26 - 1432124862826875632499843697697294871566319825009052858275287420526911462949285984837936486296692045247668838175954996822058077830442454408485960669224132566584669064506909247444067371560477422935803303848344420440/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^25 + 16422365000652917987947889540812273503448075154453313679154222630081632372626110899974459053177882389002976007559646363400207504748761077268376818639881611816920762541413389728746668146309274249573203661561610481225/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^24 + 2236647307760977901514371867574336835195107801283142221943144410564711628025062910522342869777602958745479300187970810129753603600491301147770082892975981280901092794490915167197738972615673614600808036390933606923/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^23 + 47180008874042178806183884177714753505229864875179938097874849383390079724650480424690988485203647067654593273490994210024967528872681917423882663411463673441799042170387029414584554983220080491613917140436369163252/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^22 + 104178394327976957960802498573940087000439411565313036394108056844237023637677412096990844114514018260322529286506511805721576509095100580657669184176481796781968601858742031609502895165981946330315026896579657122483/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^21 - 81322480178294515880766260352663761950054705570426913229773321411393084686674929297783944527421076511911146483699344899266898806213973095140518682624922506464878614946664276924185157009300561522772198919336109666881/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^20 + 18091773726912538565877974447617445026178736916006323260841113104537599791274690835047077497355970364095059677953406747455047000787459152932564319493425190142824208554338755567352033662057813214169157066539997763629/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^19 - 36455856964354034931399109872803050365141026897016580996814686586195708371179604913613718665256046542353335675873301319116856988221189150998724444904014595460696062145577719045622800221844161932917214267393891822139/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^18 - 4685506225323333857857585999670050711945205518434757833118604527911315061676363398759325287663330814231041585549483625086485825796144497322251579166534430904094840960923362195124260976396944177363783039103370241785/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^17 + 55688674055560926474712941116944893960366865179277904087247092600992944489457698065358196053683317028639866483925385500106736112756093451225120853155708553682110327866072013376726039996772189070191351690156553656/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^16 - 68231625691374514658478885870012717847396950054874996307732197624758643722878519664012375651776263808668144368532620631123722838105460269141656317111554903672196394475839097111686642264038444970932688004497042222562/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^15 + 20145922758270308773325252215157705935738626621029160723950440634173961187393793290406237454436269188640079088221525202966746049180687899808908290573098514787667010279607001056506519669792743411956433284099225782046/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^14 + 2267501420985457387465264156165274685841533556983399173642487208785870853814511702098036602602120633399845745717746060271101606539779871402634998501720613599259198785417669507640825372923668913309554422009172001848/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^13 - 12727560706349214243754656365091137904094951653875749002965723393833579999975691953596064057048431143550073211213243045838680901104494988301552116692799497871068253866101669178305115250536892828524860882599930340624/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^12 + 2192952777352855468323805104360089070739765090128220279500870555372326007223811913323773000759082707926406777198989528615251656543673921917185952371702236003862616653875940599334472365716716840850871893757972219310/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^11 + 1096037536104459062372768368480402104690309949587500660259774271641905699762263670567422606100443845064799805695842117909468189747553641229772793967583982790725578547540996464033360797023024111370993217108506024932/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^10 - 1362002327545827907848338121539492175328152913685565180308780558986924075163240615312692666164213858159108263193233282756177198706943719079892991929795549982910382974992214220467173573015446803442447403373086246201/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^9 + 5593115895479857508617109637288605935484362774084557085186929678980947161734640144882608369626436896950018219407408373443135680647870808854700693136453854446231515733125839492356478542934375322681834557842949225/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^8 + 86314811779514271093578528090220432710224553259834846834756890588687680164062283954859366298193789039327837335824332119234515972232220746540561762899470516314870464936831962364271091408660852337262074430151361535/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^7 - 10409775235941245995705453567909680497076542979281541443572377798728315037145559089895820273470192591799873844850481922466759404096558337381421056854107700362074522341163320822705988411382572683200629659840709195/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^6 + 8450352611883352199260468625101040930649123810345345672621676855942666273044347742042215519450548846085002504163904248483152815112467858943642797292748301379481805939846403608280274751735549309059629450404703759/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^5 - 622101635663953267887460575501977983960529122800641948277583396036549431021749812584597694839502779660736789335339947758838611692483778098145691277001900081461583761251506801231683118154703847889847360033043770/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^4 - 843705866419979852905409233184149972116361240661029525334926624224037133613722981000942490912698116942951045530121649593795335771176066005900100385190420837963025113153574928094643037502592383966897069527016315/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^3 + 75007257917622397878252549961548397051059612942935037365056096083954101946161709534334028274878818471332245539958544677528362873622863045357382260153299600015866224527644014283502761523649774935935659587058152/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^2 + 14418520085633550888907767131866649551492541699385426204932878731985720776391300301514535395344452422668288946669295738088529468608854364212231064757627241651680400827712984696930105313834316173681375813066665/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y - 943114286906141053768773975373193241523649434993509875697169305162930441866911645361899079631599779613295484753373672840446142620469490752802325289813050472125806535327802959758180741368694732083444398528325/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247

523236818946953322329543836373605294751375514966994796842108875229384925642227526812693451375384486044655512133151228987722780588071515171815504596666133280684439619868510547818986268270963583605834055490137/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^38 - 147620203195129891471901197196841795692810459721398051110005917596172154854737975542929003294321351576120197381682649447974190691624426499315959264484404266528132092649112824593313882085364434437466401571438/6649112302678696621550340025973914325675540731336200993637656306626075657695414483578712038744638960506163680368087334372252320043161548577378591486555863404876378908228939733589905611316380133188911140559*y^37 - 105207429842545794562242680126533495837671450862265201986132057365694640253865401838725490616916367780907197633055321525347195320812914197625669212229975065684745343033573647758795401988225290882733645268148513/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^36 + 609305020310488230215963984860373565559855417165417660046805390630615467723436629016328144085800843107965256217304204110597843407839880783898432411042717706946447275138656973485803225979072841828048400997385518/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^35 + 7193333966399251995088251849166613882060580380014331096788138663752690125741877871113945586312046192821118857599689234385426295723683388040952462487168048654287676528512857686692602438623339101873481836028853489/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^34 - 24353469986271879476002835140167129873242064566983216263861908385851306542972533539313188102510441442921505870734510915225952919649619319959548912304185164745019612151297100776895728739972295873157910016278970849/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^33 - 357758610329220536536845961889412249404414428457407725488811862315810369216588594711775705464448788660654418083413925308666649058180026628485115937712096193414782302955748905307192323880512795074646915550742204087/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^32 + 2082891118387046121160449986229838564800709433879012624595393365898973082471830956155269110859048051021418746902298194248934454957952280742769679210327311710755048346043058593001253288800748711833322985868426141226/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^31 - 189046802470617428752257900244402991350588780463045611738712263191158102445425725263936990167630156576614861590308170682476024702514064050640514240666691412151556043842579924722950248572923458490738527496598458746/11484830340990475982677860044864033835257752172307983534465042711445039772382988653454138976013467295419737266090332668461163098256369947542744839840414673153877381750577259539837109692273747502780846515511*y^30 - 27779342543932484574696145236084397219103386406625934505531174242428676086958365508542542229683938708050213837393926027865153514684298076801568094878070132380358084361703600894877561371356755681222311662454067769059/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^29 + 29500003686758860611426859270878434937333949404317766146210083237139820076684491008219804390148105913922324086088856126884963945622134909918602192719431102455644832632137389102966524196253560602536113311980767295825/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^28 + 48899756636451392960124949109766654770403402275643164617528979166013685393195142607143425916002382097079746721608920113567382669916151332368606221031757111772542794169211087173174549812240435825738242628647106289159/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^27 - 20794541510470883033419478796419788059403222749777850949105316785275133603922386955939726755679260067123469861432405239043158396311865062196694406145703020539124596773643682213342204171002137147578720733308025549818/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^26 + 4228886468224227125900072225121175677402475140500581008540186393259789941184454759803876171030661261041037999596034444340784968526830132674865950906661472802856694835352663943845122183212079693945000527757391403311/6649112302678696621550340025973914325675540731336200993637656306626075657695414483578712038744638960506163680368087334372252320043161548577378591486555863404876378908228939733589905611316380133188911140559*y^25 - 65156963914879826627307141388486032132111296720046427292018818722787612045060675044321054411460308320847970684400141112018052317092573033732393266064986635224656167957036570686525612679128320275582382481392147631181/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^24 + 10123822566159456103221368151003684656322901548100162814291771534061690807288865592528415207621684592979499257987596677415207893726558041005301022375084971367595820725216521432556276405899726678857758281153568905260/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^23 - 133629950442716311133343195634950924394895818075060230446818386790805645134738191074830131714356116725747677738524716869469616542391903873555815768094483439430178899762082164340505860960963730968992711012517001490795/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^22 - 255174374493071596990111682118721703388991186638561411528168992794577611533950754315087410212389768801090419389740601828776079614172494832114559302097733567568119013586540847295113843136445358705694565424669254694847/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^21 + 285263930477831961045235339723844361894291958730622450794432393794483762295802745670769365610384204156865376473720061690865520248937684667221370555824361142646475904020542784866970717114388505227228051767089141877334/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^20 - 119656480967096482808411309600384491620929272901324866790476949322650935485163615167937249337699149929870151643292431579578033951206982596640529163948966302968192398278939334491922994956670562420081259181778764670942/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^19 + 132917574091847982774706824482380378382972292365000620041656827535234917460085966809986073280099065555146974699063389506296616479290180896707041737631555988524476122340757068695498429481614813696259704162834435600777/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^18 + 9835358782890678639369355147485601959579220163834348218289971998639018908107495381989383152313889479273238042366315976979660711398430288272913745027637792892729017730894710354146165789700305346598308791214951700652/11484830340990475982677860044864033835257752172307983534465042711445039772382988653454138976013467295419737266090332668461163098256369947542744839840414673153877381750577259539837109692273747502780846515511*y^17 - 183601191305300615321318312947461450046017843979335566166388218454783001736526499257076122665850224185432821826266818204769422246158861458121075013201184920613479654595798785046523600864580118495635876051039743179894/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^16 + 232730211067652203102976590827515965258490846618260497941252098119936435085937012775883575307982521164537706002286580173705784256696812568286544621156239262595073971675082189011710603927371571927796692879375550100429/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^15 - 113632581234051772437155797387203064236747622810663484102761147506155027388890805770258036311000342579442100759731442891148086413964954055367233555795918878964613447766930814029108148955204601479289502511255884857649/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^14 - 3553380759902789762024918490916730788553973305822731595501101020119641213956256020917039069411567860355681753128534736036478342454930061291582209729649011683909636606156691837602066407521050887517289431193323603351/11484830340990475982677860044864033835257752172307983534465042711445039772382988653454138976013467295419737266090332668461163098256369947542744839840414673153877381750577259539837109692273747502780846515511*y^13 + 42655131280441039191547093099965204981981542848991599090832447334319803242351028186142081355168346847023834519796149706656933799223721879663653379094519732203815620814164175752460805537680739214119283734510039364496/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^12 - 16098930348975314425493503230930791379617158313291237556276459346801483579770222879382686421545756021886259988098399899570749231459326244899056317353519730661322571266337424051739979166277907785954913152340851349649/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^11 + 1379057721485412500166383052108637856795566324596486380341540320482801525845350661033052199150597908101217338350071791406857156851492349530042191852767534752757990390686949955138860334035871706129118161528608087277/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^10 + 3138516865773660554625865888500142118177740199521116871355516387993068301309286317780151289255362063191119243718875422055283051752651517009678254250133599909758582268153433462106342884310295452417201870622186275864/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^9 - 51086505196313317443584646263991458080240974101512098914086550140892367416011591378424069612401084863842430328298915215291407527520883167015360062212994314672523016584442976491638662376663701092379670946853894670/6649112302678696621550340025973914325675540731336200993637656306626075657695414483578712038744638960506163680368087334372252320043161548577378591486555863404876378908228939733589905611316380133188911140559*y^8 + 12447577770022531131440100426808782299716762292796345769915443250810959633839711625432451808837603001042579205672204048423096317925564917786556575922706367232264664289714750858566169711729555074149716255346015898/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^7 + 3712167503607143243402332142494507073321529287568821594678931393961813367384653373895018080341295580090389864478234438785247897551987744908852657128876064941306494646262532914677790445933964857381418380016304939/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^6 - 21097912918392018523492479649465311746681311334865340587910978059650476266312403260740757740027686954258437983326429990770035971590289240395723259180538648836927095726941950355289409496970719870251727342447992060/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^5 + 6736417078214557144004401060098953145270023409240503219905686450811149484385935648849355316019799484959309705660440771155426789126173786177960927160766940217967162264653566598488631157172411954191445191015411705/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^4 + 619795369717957058931578000876311062886306643020276672781824973069829383349036605280727069015662758703659399161776745426196114768848011557368849209770887746301811902654820533879830636600644503952053278245473151/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^3 - 190533292327863073814038170122005206392187258924872940677145383608777485456671968420279644449948242675327378612904915138907439555997858667808046453483167159129831748763201488386777254467122732184693624013635779/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y^2 - 7575607032011519479469058518597021195328902436214507120153816491073299778900907438626349149400136232859108565638411847540344037026353339809169980470201990392145241003511275583343492145586435779609841168608484/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621*y + 961402327628909645446186317377957179254124198274692956523659338718293774173617130205018716032752004557644432315191864511361747824034393795935931775730375418883847043089264797959168966234366093344356975210765/126333133750895235809456460493504372187835273895387818879115469825895437496212875187995528736148140249617109926993659353072794080820069422970193238244561404692651199256349854938208206615011222530589311670621

99740333695069152724625569746686960504289344278616745890086245314423843005687615206792453463814136979002043942139970963908782926355195259703417646097157174261206877811481976736837188039668762267137978938488/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^38 - 27793762339699923982827726861068883186822842129466015098733627592994852862856380254853259423404587238475635331824549724727431438835883938646403377961405150380962068483117671183064901852172897284188149554910/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^37 - 20094041338711969997089464383007266865795515612750623151088469590307398807213397267098678073297497374186162122660604427121282324755377248477567724138947781609187281806461706369186842959550105700869364871396042/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^36 + 114846521608452867203062374607216055640355789619312229539893420051468684378678887028541097525055660420935384522294185203521455242329199769588719437465676067499904697845605473300214650657261106568620520239067792/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^35 + 1379661955822269528858182213451069497345243213698906778003438431798054332572465489668259230932018764131825085475971931505406751451554837793674102951929458169142677936619050376823996848499772233422311477961985108/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^34 - 4556532292713131773032266426879907835847406712827772496053296271607254803891355139034859317917835430762580094762398483973214464758412301255154979788355978664320590232926824626591721498601803816224331607872476435/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^33 - 68557618825020789714193974047018492384254543874050624075946507220923523574852855763772870415416806189211750642030200751448525067982652987602225332591430099674397974258442889692574739098476383540256608602703431366/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^32 + 392731789829352214558864627395848141375350245837988502644978250290165667338676764535176070721504422394891615396688733206926373679786810262964740716791713323851598669573388898856304393584257490379375655884769641710/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^31 - 33409304181203687213621989682607677702976204520043114040296404163210965683844933431867869376028901327136198522317362487678826872362501098329032301052632533270662393609128803395339319880221462323722402206298698987/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^30 - 5337090221367256691205692042281451847712984434330172304291447611439980912492635904197066926502101870142973423940093442992567907866649596373905260824042866267257046974508758050847075261834903942520685884502214052420/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^29 + 5289115278372146297936180814792988462112327241703990353754446033858183099195320276890910932231625754317812167067941232968466342780397536085053914543485887317958594832296170632221596724616018901440676790507513828641/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^28 + 9903912893122930150016146151536376732371640217936498212624939651364870792837495609934793295241900683226819256997249893860016411772821747586556071745239297542600762204682161609250666150242110622166945378423957212840/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^27 - 3555252411536261798342485623261738437825307091899490197354771983213100339313452400693094684507761007828972558014493565949629091315304751806767756906783197632770311287366578150293501620547897056648772885738550086162/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^26 + 772510549844823307731415672222227259708975707233924872750565426941915352165233248495291068465254321790848375574261286695848677949530487121495928395688303809002858951818393084396238953072490962761491321526343249245/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^25 - 11296911972789761145638163327821105065135364799536973517683643538952063934335507556829105801589792585359684177155231394511585455262363806995669583284792346790016709586596997705829283465159992409702807354672497878693/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^24 + 485130361838066759011115503280176716257946356644718387971294790215325547914810532557454723417525664335325640975086558739825120152746781156439956887032513725196724410712075612727328171753461908089885071012491546317/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^23 - 24900308059228500956191909183819268979889813839135143071379847616260984601546599397808180683211421310576808019309941394527041513528588284909869568280387719241668913512810972554484771760528795535992340803137094146673/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^22 - 50398935407905924347200010133146291046838322793772725355674926065595560239016631251585279543189472046531323113237018780530530961658022232969061787591541010212168234378559052852919309541427269706652884068195397367030/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^21 + 52207513351682462230035487961779762112063974398796451192228142980244632484463473369768232620110173427005485334566553230859402772682703415248677551335271378496606073460389339904278182090467927834726746174204222014791/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^20 - 17196459511519071687059651757579200431847665732374019018542216984647642272627595703575994306424970385503801246256759522882894800536781397246275930306508296831887714928924807175746995574427199819174920015521931635991/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^19 + 21903150862062703195931381773319358478617478938403950230389051079461820618592804874466890816806807410356573447095578022591341456161145651421252989575318183225059765978649418087605494257044779994774966908474411509653/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^18 + 2106382709970044666364810819576219072436537405946045764163349000669901423938515811178311366032902231137782891827593986016643028244145538947786536043062860537374854728555046233804547887826149208157584836914800992160/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^17 - 33567771881117848203114537167973612015828389500564060091760839057067323440356316173323443177710868525335202410258110259538499476313923420667845829459346773368719222838967573517003054445284312111080323147860724354/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^16 + 41195934544406489952494166687679147507724115065826414232892139584861374671679503974485883273034884783582893798116606278859740809704674543599951958332387153977147295077488474087861070309615026892700939884079097033861/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^15 - 17479254061001619437506639247131397674462660768268792713146358180991478280325072971340918769628977924111949784714050034256950125494234662738007523788997572451252056773168263761615807071765503924091505940296697508408/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^14 - 963564844733164382251040669701468955818670728256690291603933052618875086570267128163952992861658385568585009971603863921078961962942789686816595909207684327316068171287149909311463468793033530498321045604970443643/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^13 + 8422341875023318707068107809472625113649829284743504781990197793739100649100158396716566197437447103925749709873690222333045515753011082411014309186061242018064230077322151496366327855777078282094861287942829333683/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^12 - 2270876816229849584317323325102097328525785150685733171222907723178066143368279353381511547633539914328126311862868973353122754932254975614025754105506263048536870586168980545833669347992612539553926963408445316590/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^11 - 200412131061562123756258338755788331275498399162379601574088040604174955112688645994974075777036426763295639578432146570009495379592929061922290172747367643866492750470315572486975774338138924611789595246103691755/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^10 + 728733064547282115800752259604752681664730448314860854030605476160181203300544382050297407460535639624360081614612461937720704729481900929028550539209994304943947012746994537232676284837042959917375028167240979880/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^9 - 8307544608783216411054651482062701380335046824743449205691496888414491217556184641014718478852274987555769887494424210933988550853267565570251284092681073028494984399045332039714723511095826401368391078927202517/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^8 - 28455962839674007374298731079259065586537238839747874236328514667505093700384032684751487065116574356462158016357757275525046892027535416069690762907280762233933845857607700834707859492820908446918045697151881432/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^7 + 5958293723620715127579158542251753984595766379737918294910986179108418865273586229827335873825527353423824662275239758414227450118842017939455857375175535252153739351284038883082616456491299207119128549515933243/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^6 - 4390021377204085020864125055589970846576301556979992978698712658547931190251959601738914191891841581977789494924474911029203188245857666477408744724118552780739715044378584567246287029270745002472929707563092062/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^5 + 1113563394760630409867818730766009990303523039053715053134121268776678754468764281744179260384268092085987303861347888065536045298698105565611581171702264873742797505217395481210647138829200024684773207876508591/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^4 + 331385390026702537384448408774904301027164260401289033761632726920034157744967842457377287182505992967652903455382990585661022595994244926890541970109623997032298884096478273316706474211672540338040436532452742/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^3 - 61109183232237951194313548714017824503172432413335589856583672448538227695398396572936250350720821284588257444975526400383371281332484615639378156878320651502115726779343749194791247713288492648005300089451132/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^2 - 6289057745090269084768786104425792325095755135029880644118271792816085210818754801014732750373504982414720521688721351817257314019586135302463803506585276648999719628268031932786065648998394070208064589225388/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y + 658729701144160744071196920465652898739909560241578269193290758440320222816867564461838460350305383160506769924304311885702868319974054166453808362508576724089956041975559432337472251524789406874509087222109/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247

99740333695069152724625569746686960504289344278616745890086245314423843005687615206792453463814136979002043942139970963908782926355195259703417646097157174261206877811481976736837188039668762267137978938488/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^38 - 27793762339699923982827726861068883186822842129466015098733627592994852862856380254853259423404587238475635331824549724727431438835883938646403377961405150380962068483117671183064901852172897284188149554910/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^37 - 20094041338711969997089464383007266865795515612750623151088469590307398807213397267098678073297497374186162122660604427121282324755377248477567724138947781609187281806461706369186842959550105700869364871396042/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^36 + 114846521608452867203062374607216055640355789619312229539893420051468684378678887028541097525055660420935384522294185203521455242329199769588719437465676067499904697845605473300214650657261106568620520239067792/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^35 + 1379661955822269528858182213451069497345243213698906778003438431798054332572465489668259230932018764131825085475971931505406751451554837793674102951929458169142677936619050376823996848499772233422311477961985108/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^34 - 4556532292713131773032266426879907835847406712827772496053296271607254803891355139034859317917835430762580094762398483973214464758412301255154979788355978664320590232926824626591721498601803816224331607872476435/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^33 - 68557618825020789714193974047018492384254543874050624075946507220923523574852855763772870415416806189211750642030200751448525067982652987602225332591430099674397974258442889692574739098476383540256608602703431366/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^32 + 392731789829352214558864627395848141375350245837988502644978250290165667338676764535176070721504422394891615396688733206926373679786810262964740716791713323851598669573388898856304393584257490379375655884769641710/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^31 - 33409304181203687213621989682607677702976204520043114040296404163210965683844933431867869376028901327136198522317362487678826872362501098329032301052632533270662393609128803395339319880221462323722402206298698987/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^30 - 5337090221367256691205692042281451847712984434330172304291447611439980912492635904197066926502101870142973423940093442992567907866649596373905260824042866267257046974508758050847075261834903942520685884502214052420/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^29 + 5289115278372146297936180814792988462112327241703990353754446033858183099195320276890910932231625754317812167067941232968466342780397536085053914543485887317958594832296170632221596724616018901440676790507513828641/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^28 + 9903912893122930150016146151536376732371640217936498212624939651364870792837495609934793295241900683226819256997249893860016411772821747586556071745239297542600762204682161609250666150242110622166945378423957212840/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^27 - 3555252411536261798342485623261738437825307091899490197354771983213100339313452400693094684507761007828972558014493565949629091315304751806767756906783197632770311287366578150293501620547897056648772885738550086162/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^26 + 772510549844823307731415672222227259708975707233924872750565426941915352165233248495291068465254321790848375574261286695848677949530487121495928395688303809002858951818393084396238953072490962761491321526343249245/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^25 - 11296911972789761145638163327821105065135364799536973517683643538952063934335507556829105801589792585359684177155231394511585455262363806995669583284792346790016709586596997705829283465159992409702807354672497878693/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^24 + 485130361838066759011115503280176716257946356644718387971294790215325547914810532557454723417525664335325640975086558739825120152746781156439956887032513725196724410712075612727328171753461908089885071012491546317/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^23 - 24900308059228500956191909183819268979889813839135143071379847616260984601546599397808180683211421310576808019309941394527041513528588284909869568280387719241668913512810972554484771760528795535992340803137094146673/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^22 - 50398935407905924347200010133146291046838322793772725355674926065595560239016631251585279543189472046531323113237018780530530961658022232969061787591541010212168234378559052852919309541427269706652884068195397367030/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^21 + 52207513351682462230035487961779762112063974398796451192228142980244632484463473369768232620110173427005485334566553230859402772682703415248677551335271378496606073460389339904278182090467927834726746174204222014791/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^20 - 17196459511519071687059651757579200431847665732374019018542216984647642272627595703575994306424970385503801246256759522882894800536781397246275930306508296831887714928924807175746995574427199819174920015521931635991/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^19 + 21903150862062703195931381773319358478617478938403950230389051079461820618592804874466890816806807410356573447095578022591341456161145651421252989575318183225059765978649418087605494257044779994774966908474411509653/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^18 + 2106382709970044666364810819576219072436537405946045764163349000669901423938515811178311366032902231137782891827593986016643028244145538947786536043062860537374854728555046233804547887826149208157584836914800992160/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^17 - 33567771881117848203114537167973612015828389500564060091760839057067323440356316173323443177710868525335202410258110259538499476313923420667845829459346773368719222838967573517003054445284312111080323147860724354/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^16 + 41195934544406489952494166687679147507724115065826414232892139584861374671679503974485883273034884783582893798116606278859740809704674543599951958332387153977147295077488474087861070309615026892700939884079097033861/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^15 - 17479254061001619437506639247131397674462660768268792713146358180991478280325072971340918769628977924111949784714050034256950125494234662738007523788997572451252056773168263761615807071765503924091505940296697508408/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^14 - 963564844733164382251040669701468955818670728256690291603933052618875086570267128163952992861658385568585009971603863921078961962942789686816595909207684327316068171287149909311463468793033530498321045604970443643/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^13 + 8422341875023318707068107809472625113649829284743504781990197793739100649100158396716566197437447103925749709873690222333045515753011082411014309186061242018064230077322151496366327855777078282094861287942829333683/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^12 - 2270876816229849584317323325102097328525785150685733171222907723178066143368279353381511547633539914328126311862868973353122754932254975614025754105506263048536870586168980545833669347992612539553926963408445316590/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^11 - 200412131061562123756258338755788331275498399162379601574088040604174955112688645994974075777036426763295639578432146570009495379592929061922290172747367643866492750470315572486975774338138924611789595246103691755/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^10 + 728733064547282115800752259604752681664730448314860854030605476160181203300544382050297407460535639624360081614612461937720704729481900929028550539209994304943947012746994537232676284837042959917375028167240979880/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^9 - 8307544608783216411054651482062701380335046824743449205691496888414491217556184641014718478852274987555769887494424210933988550853267565570251284092681073028494984399045332039714723511095826401368391078927202517/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^8 - 28455962839674007374298731079259065586537238839747874236328514667505093700384032684751487065116574356462158016357757275525046892027535416069690762907280762233933845857607700834707859492820908446918045697151881432/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^7 + 5958293723620715127579158542251753984595766379737918294910986179108418865273586229827335873825527353423824662275239758414227450118842017939455857375175535252153739351284038883082616456491299207119128549515933243/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^6 - 4390021377204085020864125055589970846576301556979992978698712658547931190251959601738914191891841581977789494924474911029203188245857666477408744724118552780739715044378584567246287029270745002472929707563092062/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^5 + 1113563394760630409867818730766009990303523039053715053134121268776678754468764281744179260384268092085987303861347888065536045298698105565611581171702264873742797505217395481210647138829200024684773207876508591/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^4 + 331385390026702537384448408774904301027164260401289033761632726920034157744967842457377287182505992967652903455382990585661022595994244926890541970109623997032298884096478273316706474211672540338040436532452742/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^3 - 61109183232237951194313548714017824503172432413335589856583672448538227695398396572936250350720821284588257444975526400383371281332484615639378156878320651502115726779343749194791247713288492648005300089451132/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^2 - 6289057745090269084768786104425792325095755135029880644118271792816085210818754801014732750373504982414720521688721351817257314019586135302463803506585276648999719628268031932786065648998394070208064589225388/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y + 658729701144160744071196920465652898739909560241578269193290758440320222816867564461838460350305383160506769924304311885702868319974054166453808362508576724089956041975559432337472251524789406874509087222109/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247

-1481713034278572777624762221883125684485804555026506327730492333486935516013088986174050165615156358408985429228278914605321886091925876970719866281676485668228549226726357434701744008068913850028374376708/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^38 + 398273088172634516129805907353425743586267171569151826871215349652235225595504747768069844943185566611630021380369685817317256657371917901660450459563656605859717887719354633181397856749675984265615300664/15869003109018369025179809131202659488485777401757042944242616483594452643664473707825088397958565538200867972238871919742845632561244746008063464168391082111876799303649020843889989525814749721214585061*y^37 + 299986958641748560995546583462993642918934562245041030261041692397246493711045966965967892818487970950817770549651270062932146927064821960261719069240519547115460675542145299347538026464122729730583614718208/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^36 - 1650196981336487175135729576612466436161199645015936869118472196699836627523676896192547760288217557722246843643148574801553545626750183554177996768432621374103137620539010413028835739684637943437251684926326/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^35 - 20816632022490206393642496455027309393941153960316894623404851747237930856125692311313867794695483457937395910126892581772896539415674928317795423181549886288385206010383699715050458468175257883182751316792375/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^34 + 63856706580457859527911660436122414060893003032001007395316569432055411577979944098300024059195814487064732695164782391355558402328645950412166351898203301124156225619812512843672695402147448948815462982487208/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^33 + 1031209299057637521753733455268265365671891197688868852903525424013566452179607610924235293451022683052012850950580082230097529417287629522935721524854705677939806821387108902365319816061527332313254558696999712/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^32 - 5643820452265296004247165271397450294558421687959635145953379061206422548411550431608881138624013257917366692237566848253808370543002276415871713718518269980651997071114958510736198645598785542509949954757738344/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^31 + 396641417693555830049259280274864439291436321800748111019359877970770471118096829761654106738959591227007142658547664931622160407531998709944651428239798031788756365485553924067391732780951730074468388597386270/27410096279213546498037852135713684571020888239398528721873610289844963657238636404425152687382976838710590133867142406828551547151240924923018710836311869102332653342666490548537254635498204063916101469*y^30 + 80341984499531106330045106419353469404669260943318271434315604067917689317301988010292330759815563537585385637965829023743451498679045995510222566131742699185630915864566852631424382491133087998134123399935251733/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^29 - 63796926183565268916967511842323062750806335618126037978597340480485395805844727487420468402081714475826629451393134541742004156508536814212586278289929467609806392631149322007438640662040323926028549703011930923/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^28 - 162059748846759461979633670085596324399621192121263915526267068413888029316487046121831210342579565576635854528177941414107808041739418426802063422991236258011644245605241258380759636617428586926552016377949683768/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^27 + 26503016516086792713613626741657638393649299254260325355336443260253055012569357499364369636816784182732963532858324534919330891260136806126297862110252317932168091662629558892970199357291766953682509468463686629/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^26 - 10973668239303633456175848779813930608920354379797955864698416632661973082179891344799684357352045284029134941615994168802518232332114794413196531321394308389375554847083377127120403265715007523048275122073374002/15869003109018369025179809131202659488485777401757042944242616483594452643664473707825088397958565538200867972238871919742845632561244746008063464168391082111876799303649020843889989525814749721214585061*y^25 + 124838723401416406463272056950754773168893649487811431035532196890208250040480486070744062094131176110683413177827250512913180251358475476110450010078025441341964165845233411867437934212976821824367383055968692732/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^24 + 25246559934923723276801044284729634672983995042546658096480827463077054323474299960668237528210916032242993029747659773387032335870917330213799380576047725478793874258160277384777019464643424777175655978818504828/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^23 + 365063209113125762518622545930360055736504326430131679076562456570425420043603240281266539872617924318270580786722326847210177520631268077782048328105128939925755220223631411964851731309658696944786982772517845178/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^22 + 819749718814786783100674774420651518493321715383481421110827660483773971366788242914795525199593452284003573575955563544885277910749225970893397512537069351912515867340265534693044591073340604975201010133879931019/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^21 - 636496405802916631412239554532777224801272005804683659564690256248427741204698772915433716208445828039307289485151353005838570821224176761789863119305846164944811857038132085648553795542467008470123975581229725176/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^20 + 112476750667635040447981503718365730970732284278953948412244040719761790482638783324894261318216160463787323936513404498489570889032814062272117457358558431470435930288838722941205524476078816039876397886817034915/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^19 - 264534060414044148350963035512968746529980773791673065081658611521542863419606666980025308614388060558790104870306172093272322092710982915700134597616159337758391673081998760172738338938375481018644556746871259785/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^18 - 37613217862938843168549483376048148459729394722933508745782704082733922954683996279216708908429132930227689322084147328064033547306038183102428513385283484978425315376800737063422858200251713192179373416303882964/27410096279213546498037852135713684571020888239398528721873610289844963657238636404425152687382976838710590133867142406828551547151240924923018710836311869102332653342666490548537254635498204063916101469*y^17 + 454727737672590510161828371202967600871913986682224568234106284078811069861089386400697695768398994960870852194173097741819115036195919341022821095784227381321432542092525704427839284388747802551160890943409252070/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^16 - 518557147209741029337889977828130991434746779370909712577456309153046250973394079784974730504137603663933005204786910024950449504568263234466508254930484157560904700080350913962140052072915749517899769556213489101/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^15 + 138351534852032136901322610864896059862968540764445129689065573000848409465865191077108078541978518168095041280782974009200195695633253888680202739847889200953991108657691364134172047196202423117000575632079361755/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^14 + 19410132720049700502738065731156710500436883722699422529228761823364945394413288569136156168184898135960408924924114340716276212905025734754970593807513072689085059581703943856427428487273308962781498177246476309/27410096279213546498037852135713684571020888239398528721873610289844963657238636404425152687382976838710590133867142406828551547151240924923018710836311869102332653342666490548537254635498204063916101469*y^13 - 103925243226245552034883886922431087620348213670665430224894789633424750365825950627914137426145300916728063551034553299531851971957008602047491058396306297621167996550644706643231267712762924244980902680522468446/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^12 + 12287783531304069067447366875639791430380277286469257749544400355398821669887426565256952123774109922909218752056970705479256746031801897545973696571011352537365650061566693646025700952339274083046536243005660423/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^11 + 11456155960873280591266310541665183228747168181148855961292073092564697002129835281306201063217177564458855085282076194739594187621253707083438328055178614129926053277771025306316154579642235230558225095622488026/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^10 - 11524541990367334071427201664892027788963371460178725996962518942890682500382228132551708063278128590766575499713653332123819575425525915264387750244258506779153556658334819137705730719249063054394358492914163662/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^9 + 38456406785850520446868975999906037658217762008035720296653222805302017481901406085783741544516873728790933060320040182831346440406425088261326459965683459541812170080633688576697578551383540636814159171898671/15869003109018369025179809131202659488485777401757042944242616483594452643664473707825088397958565538200867972238871919742845632561244746008063464168391082111876799303649020843889989525814749721214585061*y^8 + 916523806064937556583756543659289750631358820460164673279073960290533983075524722130128830358786892533525609601367142812022206061480715239224715014037837903945090800242442267666243052538616130560879887693597458/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^7 - 117876482489751613503232043877050303213533350514429858040430973452064704035042359157468241516889334635088605084030797885984493097041428848089579918003762088375057195235880351326984515075917236796603060325983644/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^6 + 65978790733307795032001690662875884660259252972954329635559587089581927050025637496564875544329197583559339848504093012978915941565838643396594139662295932653114613609131854277881537450097779534594255587788591/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^5 - 4477269142311506359177916549521106689277798191935191503053092026389456176091886112886553078796434294243103845742477779527655031044341757144437015033291220854394886758966059839468288329218074451712457186391526/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^4 - 8473134590557660924887380267140347962917285770255230907841557358996907050205850363157595940777670090939200549949935082765151502334480275904843466547450007965307934341077975822763820543925023763455390293768757/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^3 + 778796811424703319694924918784449047952592337648760330265528887618197197588079896929549936049312720627362702374867584093358497580214638818950749381987007355700100135660898351030024067550860560066688818964825/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y^2 + 154215994134026216002743589342157075867997524160521220863862975068990510010547138171975115967132396375589801471616476038711282681987316791605864923302662805174424907555132488146326443366108753534013555390134/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159*y - 11106827196392145266374622064815366307842926915390645897207103508102565235700672108900189988886852553939002952891408507271822351958336445278012195012867368925336178714034158787592912865147302879028375056479/301511059071349011478416373492850530281229770633383815940609713188294600229625000448676679561212745225816491472538566475114067018663650174153205819199430560125659186769331396033909800990480244703077116159

2814717770694417155559514821634048895762150470256525316085429706184639723627888516060961389089845322077067722509815675904589489909447880750948869679267355280120096705749657639598222632356721546910780804617/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^38 - 777266303670644086021543309265489122616190636813299178706423526723407190086870770037385207199904081716466452264286670682170685090431183617133126515683403988674650109926160768329619089180893156004487861886/1490243655601452291182794802957486113782346186910456851036602075232097234627763758198483301371927109178317874120250426644941776221433256602393596225995271620142612152788130775612578107287876042001333306183*y^37 - 567689253847493429844223709186151143667866326886133680714487994265358542412404363400331923441751212670853447363543218416711753726119752674791775883246641543405795873021116187933441458623741070255312314154561/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^36 + 3213483762711810698312129953043722917294150158592599071048700132273606723732281322034537189503830955824431217847363258426286633098165392789345078101585593673966799827616880599629729628227241161580353370107073/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^35 + 39072022361786581023659926461091334823608288476459029014820918967045755761716625266364492021104857938458251486990551671723738441169355602893308596317312290848374576995432031563641161165474065704279867296778538/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^34 - 126634570524844204393963856021746259954219189417890718391379887784074212214977053326607163945965827924579515357724218676747213087705663990085406789097965390827168670592224458648354797047880012735882297973817010/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^33 - 1939626145424334103562886920175126320992484075320359135374469447598403206440655408192683385115077417572177753370933449189055505526456979919318332316362611833559165112722246466111410195850771751399568173330276526/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^32 + 10987203829023045239838230134474322146646292693393828980575318583021354245106797433230423926475923546475890138120689966652237302490649953867216917021330142247576887164876659864907192661679491961241031117526021739/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^31 - 9902611797787510541308289626448987573804127651900300234820757508966909068318313161522201539263417517507576416695148225533412048508625337939266977860186269808745064181330474307394621591663472354070934247232296394/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^30 - 150801785447005915756882110947236310253411658468439623759891195525651248658361099959807566300064798095989743511164787421642248851904619309832701585882883227374806586355737441500988935508598245025397538194270327730/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^29 + 141920858304266577912099169924641591265919588543239642197566677251107335067361948489507646110310449587588671529779397031296449546100703169026763880368511832128158946800667555033398902952796534157298166735436525566/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^28 + 281813325970967718174139729868199622762622967531798145950246852603433364990909289629444136253786473204750601759560058656664468147983087780619684263972132647895897282026321283643589272690655988500086815478176893809/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^27 - 84808422526372004769210093192959380531827760905987361571350150136506602276404043157949361613324014450128226494919305133781309520033146867551940009424837226604885886889940801131514094926070067730626080291138511340/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^26 + 22133084354633154820463634409027479924192922332989428571057403548563348759895572744117808856199574511422995131619172788870054273134098553096592593146725863334817227279642327144720359904302481233583556165353539596/1490243655601452291182794802957486113782346186910456851036602075232097234627763758198483301371927109178317874120250426644941776221433256602393596225995271620142612152788130775612578107287876042001333306183*y^25 - 298028203385940403096207060230930084657063998797381481386434091609252564960879956010228630635517435642259569111983296326318359546902498568649937759843878794917354887441193982416251134162491007042635190174225894608/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^24 + 9869321043171238550755672580829658322813277541991389080997466522651745371060849596095258613419048801160343677937087425835525047826747894278666945530669007938383722188083231979453259270894559823225285220824411095/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^23 - 704204629931830830728319872348891005797058393639718781006025041239265733135600817583421837076403833113928176418954715104693185257720517020268357366188840250098007382428019293696717294019781662640761424825219047875/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^22 - 1461267109311450372055031129201929131122978423434387590308884763095900482082239427390187214474324673272288771816180563811285542345910467853865560154875792659674676304758724255893943499486769132067983426791152699307/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^21 + 1385554181613614320780522331228639615545243968044743458876050217688572587010365566036738916743581334104608119034481462543199057422814051547854469074380474757416322482089427090214674871895172788878356704924622319911/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^20 - 471335439754867886531841486901685168668476482291743957783006603976791991453064272884202173367693166372598118484566546478557781876133009090359148889223928170788470827350841642328950841169636557530181106305842697095/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^19 + 617615532687593334199628928984404616993070800120077720492210527721480790660791581282430154464138809396842055992156086588114004902689388587089602872338732241682508890964439587881852592548119379166800742906715307318/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^18 + 691211142439617558319798660610432093367940206654007787870309815233313785241186128376776180510450679024549482856280522410490768636599339893457392900296581311370031890560670549723581548524708613224679292440473134536/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^17 - 911340848140565051469057083414963377647067945807770010213812369978467680519990653846952100243123808835098289821024769498210467207756095659884725642271993175802017096724398089008946876432182803925979574743338652/27410096279213546498037852135713684571020888239398528721873610289844963657238636404425152687382976838710590133867142406828551547151240924923018710836311869102332653342666490548537254635498204063916101469*y^16 + 1150900084813475356097674442640969820348909249426672869080037299062393428929873911356697387485055885305729579657537605649707153526615150851452461336722768101215697397385070792193722828818673607189008393965623925076/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^15 - 460064724381592865047770596078356021769688631736497774145121804564403050989674648898864000219869011750755194969351143772948602702341277401953062039124895815000806576524927037461697544299456842386094989023016194528/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^14 - 300573973727107701937247757309879016324622841578189268867467437518301225466902049523969852348713422038147109774722748054979107964764671411777265074442779044979213563419225604471203537387358332641854915173729820505/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^13 + 229403595159381481779463384412416486524807284052648803264439850077475489796717515338215642564657606494309228486008014125026964549440608854380048223678009940565621180158961813971200438135790256957801924139556235994/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^12 - 73481450420187530387373299458629664780951213444135977518336210840963858967170518634563301668869700710492836140663493283368680912875220897517689902089516157593639345630203783714383621406910896184199639825662485310/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^11 - 1838213700748867195225119798834079989049201860671144670262917811362694421842131394126901928551312656387960290724832941200771785521757625616295916844798142462527772326727810895890631002643363426931433705827924512/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^10 + 20095903463086155331665629139032312569935403803297292513763871072355119123467583667135815233577911338133301214516560994588334216521568934761638743440285111406159766257643435824639653987248636554821147796244403217/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^9 - 258647437524830622087634900255538126219276232654740425802728520562553229357616627348847708956742650055410273217845452926589471458795436906137992527742257003857313221366062341177424098234172331509468430586803541/1490243655601452291182794802957486113782346186910456851036602075232097234627763758198483301371927109178317874120250426644941776221433256602393596225995271620142612152788130775612578107287876042001333306183*y^8 - 13861372476961075193820131977500997336975846602075956316994215679707951482188227246187960749031319091539070290030777737372193038084915396956923198736891973043516712866193339088572796433808043831471281401128186/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^7 + 44522646025689285561174311527287101978482880835483361315246093221898015333449591925691669599110702230455945322400634116789697520681737558128361966404436885540207766398622101162119757568522745350885806914784435/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^6 - 149442754614021952397578889533157405173255733129415138458447632498979574800715801268551883371124613549787844246012872333008805077544092068426704541221364966264124851144446337815148655034494190548453858669562669/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^5 + 34599274550467507338019934176406331988769967141015873820034159453030777810301511162813930877117441962476199348182245584825684228625536098655358650559581686166153455725019324451574213820794295898632451813493241/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^4 + 3438078791701997113409446566368351354928028006853505851544306533868216855725391340863428940645719085889473633648489148547068992931387150619178854436454665062680572641337664880168662433868508833795082293497838/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^3 - 572574284023213155284827581898238091937260174501790063792923271536771796634918324515078655780840774655736256208780881449571187670560207082462770523252543525406402811131245437512258547116002254439306855747188/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^2 + 16281779580439746353103123382289162305529438747418282974666360905373065900250574884847143875571778258805602434880552411570052389652162233220906671083095331150353252504870745107836093164121823869473074821881/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y + 32339196221097969470579177934460593553869028007827909418061754079581241317153983494828812411883925819815345022847543092767513998766293416017168750536966278823170993822464447296193231796161975535118955252604/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477

63000263751816019571584219644155030664426525996188313647597001003839415832340763587430853902923486027193461380914081392472625430698815128947987770602669523741369946126489146225137314201316074203367892786434736/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^38 - 17670754192601893656032026381810337768961414177058168910820852722059127521816468069486537853858667175117239084873467695892117910442870510303066360999138184439554243420121854586034686408792176379378874836944522/624412091697008510005591022439186681674803052315481420584336269522248741309033014685164503274837458745715189256384928764230604236780534516402916818692018808839754492018226794981670226953620061598558655290677*y^37 - 12678465720633874218472235756431614867069658982105384120118511042934538466008847377457399650896624849010465846322436830503281510756333781849874243935747412605446158799446637896672869021612307173489315021710454181/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^36 + 72970511715918152728280776479184825692046162823356986818040595690535001360640676025976032433000720094669818088925709318131566743460430330303709416053871399779168310886502140099030513810108378750206552201899606065/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^35 + 868490159185612957255331869547158304404286191992213808401971539729897491130346842082436947398439800968818997725368432716486733203602579267743890979864113006721701914229485167515998045733811761047692040936190650023/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^34 - 2905775634563699530059043436551689680015475588221635004619619963089264382259578539729682996863826219175838252758676024007802460111085333044203287474026959533003289282974403009631963811153716632928627532773553837936/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^33 - 43173437951057909336932742306525173930630609020285646265131338403850840108479868827568119291620359532050918807668949310030917830516096527120048019890133507740456096336391731905804664599331146035872365470099913684415/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^32 + 249467216983045773913834131262151589358612858452745423250499910743898593868089374195470985411142142326039721357769739062724088516926960491549247275445326334312712293545846257878740026005102607552238668805851170974092/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^31 - 242257565307986188693319272706532783839951242812851780091139442464853813267961902357293264707548937236029107001890494883050510666309951488779613295773902758984016062477389638302909643489679871628382867915001875568716/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^30 - 3354349266982761830045836540177821978466042483908918864280636251462818472434359819354251144415019221723525806924591953575421681751659699821587196347404001786923562689466117776841018780326424393304480069899563794932452/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^29 + 3449400885295191082445296390190649255871940026180121350644616330778361033584010017662853999046205912903751702108638597562593105817040012608948333842092038147970531025333149418525125037513565137728152339253588532001134/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^28 + 6022056438940682758221960704166618307699735285930692758224747812107782498754645471938514323833596422694214487924483975177144300319150720616908435507148251298466291920543198514081538331248032798301225151752022680999128/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^27 - 2345507951211176219468113281145495810599866392965597849619169530665429250880509006994110238292473994545354956831718699836618096157419590989583303593158004269271782301165777681075216766224817612950409737432293331564321/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^26 + 502923803879294418007276767852277047200581656799354444998985440435934344667486079250205533939933620641027079338907519421277737384957043261633530693612776500710140812342920709594597064983421931335333821635928513993460/624412091697008510005591022439186681674803052315481420584336269522248741309033014685164503274837458745715189256384928764230604236780534516402916818692018808839754492018226794981670226953620061598558655290677*y^25 - 7525384195529505568543255565882099397559432464851781763953594167284678258964201358932277669582655805633112829179750791192193000581433374757629279752309435206360618472558184725134798980732621452593404787832689900356727/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^24 + 905458921778141684928889601011927075833740155735488128988902846657545540517836313213680434751845099448349699845175858895834209299036634842875113543613954128189939181833069196329133062886321703606839763053851941831776/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^23 - 15994733407603948221825445943677712001498649944669417142767896554661398296776080962369325118670621583208792879227693698230548987014222505273874208122677246622507808012406659181628917857471664988880976545178137926961194/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^22 - 31236313917776021103059530514821710295870291317160121430805451665995119796596218436349342354923180345587760706702609619819301467097068150097161237240440977505642237259616609509791104121387188788253614864215725987846897/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^21 + 33503044409883638783847268370481675555678982493463152481924795217188384069829168915002938386988108245900557732200474980583426219613753427957168530017417747960286711136834387890288414212891512832027794503912887099925073/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^20 - 13121781385271356527630840913030657575431189949618608949339851363532370593724227999749942710141247918970596409406707985998610450497423532702278459774434959759969373304069206676754488105821433057919422542924985123200752/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^19 + 15309763481688057828470808602282425688349557390964327114594460498156489035403227813789236041295557121983676544681089390862494719486543787599655699343971525186426901043688515596235087925175877948373747101407269471850733/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^18 + 13633092094836981683662999761613649237737731352155909635864580941257819072160494557550266113815007569340382398321024351888710325906969863729276236313440582375374994267097361263411065171898370835755074957163075608135751/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^17 - 21121626120586765350138353740815429777588339582029472769803298358676558865083107211787438589970474526513597244096550123473373730809745822148868550980440601510740339608396555172812718349833493865045550379693240311448/11484830340990475982677860044864033835257752172307983534465042711445039772382988653454138976013467295419737266090332668461163098256369947542744839840414673153877381750577259539837109692273747502780846515511*y^16 + 27243748198588731094067779213847877197971048375381122763423121092264639156594879185429695869968084587074465170686783186637847861821314157504445692650438042525993148597172871370222809043097087905872514172739309444772524/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^15 - 12651803814050560563668102944731315135209510156863628373134366327111403030492122040291529487866042379591381713038488041016153205682866340200798839630293140107801504686654069166482501003609085442992122615548651835099535/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^14 - 5333661593899520511816691481611159120047303155017216421124448262212831896938968378843456277226843462947974866647114788047703531988911550287833342344852796022061424064798088506909631982661994895351616510256497633956350/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^13 + 5091438299991398095460276823228084908809148413215090847139202778146403093815842333557874835079361699413836959326740673392990238576658338878973226519249481215294824062221227103394513862458421843552204297127386829542923/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^12 - 1748971624040051622356725784578217979840453355350896879281847241163963146851381551357709916712743380984549697792687034529477285444160620069345220640406719665212700915615576257348056570355364132665134509639737433984468/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^11 + 70518850597490672899267398313061953281713797779047861966999646698804496043393663729951353415171141930701194196374756584474258877570903839736016356245499027389971513506392839847216286317623776258251746803671672872754/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^10 + 397822744743261864971107196674003851969451680159167986286823471188868289703304843037146275152481662936633753857111388736066566090205042148063338739498368758464811169785627059915929389334611041599106317871523036172276/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^9 - 5633811728297779185428207745461938861625832047466100310627474966192258042846846035706645859010597583533707142871360101268319574534706518387196442578208091372198630663754425740608377891695662454827079256560857135158/624412091697008510005591022439186681674803052315481420584336269522248741309033014685164503274837458745715189256384928764230604236780534516402916818692018808839754492018226794981670226953620061598558655290677*y^8 - 4634129041443132686939150733960319217246785741485874061131107788419733483760676061231244194841571464967467004693002640383820958710754426035053544311131225865076738745446791569998526858507088187452868464054789329659/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^7 + 1321511736083119663994342863611788707139206070212087855202638316299866705848475334154909322155308787688220360609345514512878232060962528995955529752782288196849823395613657475841441698559850678989592176394031191956/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^6 - 2596105570735095263579534915090559163547289409486838605391684584009116701997862218718933621993945791319885176770265245630198656810751882718535114634668021766667277186203634916068052336146095366806336731703294846105/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^5 + 739952264108814482480292805646980263499705794267152685695092638375973357841158968730846482935361731194403483466609803689401222458601894739094089112029942897438209144149260700094435126180335255185851875256387551146/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^4 + 118699873029275155734258132186313820075557157509706759730241574410950968975382288204448990014520392662044305453188021923911860219293125066295607751256521831996516821742576499038054188666390175187974449560262588822/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^3 - 26085317389044180438086781059037716755311350877249212087802569945567781295710956283094641320943927930695762223144655532365798154015733447783557684298581814136040615404600160817213673162771864728808538885343985306/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y^2 - 1666074616019558072795754055560483896516011508831266228537325450927013739731955859116907906965995055878468460912264067340254210104760967792218131539778814803468158171521816605624128866213759796044305990137041455/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863*y + 202690247584543513836473959511845711460347789429453771294210768506219659668976870798298057566630224436951040977404697877100314198455977849425829438503383077636238365213254510859645311978571875568130895447569424/11863829742243161690106229426344546951821257993994146991102389120922726084871627279018125562221911716168588595871313646520381480498830155811655419555148357367955335348346309104651734312118781170372614450522863


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

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

# nu Gluing Vector
{0, 2, 0, 0, 0, 2, 0, 0}

# f Combinatorial flattening
{2, 4, 2, 0, 0, 0, 0, 0}

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

# 1 Loop Invariant
6509515586498564596100266532108739824961233813244101857266539205319356274839119889100856142149603637016175695722136296831706187316499728497917824619965921498782450804286250195244479208682572046275324873778278/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^38 - 2197309614574727114537138675381655569826160473432578281841628598864064762943546814299273341432026020331616972213363345018072934062973989369445485215338682831441832488624364324192021381690652559624847493816962/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^37 - 2550513141447121609610709128517529414660824202752395269000844048896179211605732674181259301302191905504345990381778549078505973956278590729792613622812226263079312620889807874164460400922717727619631942734689855/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^36 + 8974979695259778184566575996295940066489259018111670396404458931627481137903389637586912835331818104027530111711454396532650088361447880758497570550729079751036152489067605593958239091951272733358381804158990455/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^35 + 164280858823895101463289085493104921805250191023604884215802827623919090033866726570169939814579685800405795875701845943252250289897780159187857747475392270191227772568290184887936650008439151596743731618790362897/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^34 - 400781076383853975616116387737209247935717217416824471127674585133071443975956324096497661963166337227896265773446183455481604313802507551614934356112706112230673440899117848260233643841303897246467286271805122558/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^33 - 8350546303586529289291627827588851921419033932415057325244691992857391360093185741383500034598670915308275500703167225266798417668615593016634216977285350798541038569326062468710183231260788125979871507422647600073/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^32 + 61479773910800284165174813331597324536166261209117210661791548869800185169071602446918582762011746620378896534982806228979492673411923349092631364238698980978295223746025057926611519855167262200106627624369996050207/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^31 - 9272829896933204261283948979677339225266843735610822905863107092467189646829931348214212471993778417251773427445325357473580716994155122909273945616005582680990187230286292926751680261930641659692846136930127261595/56629258912855187064946202512384472323729155102597360339390878858819694915855022811542365452133230148776079216569516212507787496414463750890956656587820321565419261805948969473277968076939289596050665634954*y^30 - 661063719768222122574986639899572674953720379522318153873822496547237218861317021314888407106798501915150147684366401482714065968754251008642670421023442060722884580721207305706199954039783040619595218936966487328217/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^29 + 1483668246966746336624772727904654888967664352932347017344274937855174812625432973267841233315028377371673295217543321899183237019073568167789327234421880302946218674358513912747244004656247669889222975042022285567857/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^28 + 778532936269483884308658528935929818616334596819960803319957454203414090731041976955597652903340078973286158849194107551393693143527245492483642017815591581408438373575857226261757797543843903299140022934629149706699/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^27 - 2107040490018014957346680083968160142554166491163336788267725247673605057807895267956052370672884508302062001527727988845885922578142801519223024166735265070675359239822930781300850849413843657539424334907056686748923/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^26 + 50693359109762236344370179702292707183921926519345220935017950408757316264081520565318724025449448582813625234099059374029844767698312292488665630472189605307744284693400391236491068891748993117103885396327569219979/16392680211615975203010742832532347251605808056015025361402622827553069580905401340183316315091198200961496615322754693094359538435765822626329558485947987821568733680669438531738359180166636462014666368013*y^25 - 3566267023377532388500638449720566231537148577152578446033750207238205574958992644425459186238243058134360014117149749178117507555343101183740011012883954164629168605029015490824115991176890564764595738930448640240153/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^24 + 501384496738179011561363166310453697239118818118010985439901565802192801665308980003700545139443122482894885205531745456394701448219016988065426401913526420330751036206343780383612697082905043384418485955370347812487/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^23 - 1466980438608738114539299078166101768969435986323028798520279618972973430562626411584486154956900329087701532668941903478108375301699301493961961244767373000912643315995729446442278510892439641360185675963604078028056/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^22 - 2905654738779073926092378806941054761220209971714246577390966419765879050401002222532966619070449022672487234094901813548087142492304458863743247560000095854642771707052592057131706880340552955825355901149413102025731/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^21 + 15390283396521641615181021351626269583397658672836360813774316143101435359165027998922295144229132203004192785915097955788063237476723011309225332934432344689387640278684758816363244891389117079939372108755296957052453/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^20 - 3592744254437236682954227551100410791202046536947852605931275798924407194416674381845348639253557199622074008360434341510329020594871338310235501670754412985747842925681567386815298657925470104085389367623368596268974/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^19 + 3499473335490906743190868362174191135259678614766865383491083199777037248758026579342823618484259788098080513650453544131632001933572772719708113775738751283296305508330065511190351221765798832203525236978690892801059/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^18 + 15287013657565901532174707161137571381682534422612091237559019774632534810187771685607121597564112418457857656710263753032294124640613999007184422239000906587585358504417514772712548760353311274654250144856365863168/28314629456427593532473101256192236161864577551298680169695439429409847457927511405771182726066615074388039608284758106253893748207231875445478328293910160782709630902974484736638984038469644798025332817477*y^17 - 8626900557358709583656023397788365239307935667030093828828733799599893340815777435642113508891409469651841753219822766603299646652886324906308981716657299637592043859931802646536819946860614108922088969539641206447/603022118142698022956832746985701060562459541266767631881219426376589200459250000897353359122425490451632982945077132950228134037327300348306411638398861120251318373538662792067819601980960489406154232318*y^16 + 9129752163471480070541622692472284097096985999720610000729758865498077115411937314242266701927428384333877129871512240286817434861961389189622364083313825655513811160394816655680392342246957253217391864936992249166831/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^15 - 3479014567469712288946083577809475315754525717610827084359017367419518015382282570706749127036295463330642393684302055630656235710506391630248653846770508920420820235043789030561314277086908160403923046989292496396022/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^14 - 50899055037281478499614267098741915267406043017154760650960454660765615316074227642710303906999236367501779347849804632200361719276277318711947479994534115096773049903298585691065854704891768673751714864881045696961/56629258912855187064946202512384472323729155102597360339390878858819694915855022811542365452133230148776079216569516212507787496414463750890956656587820321565419261805948969473277968076939289596050665634954*y^13 + 1576185980674707987799629891006950944870702943207311303104405977507444286205560981904424992109620567037545260016630887182562061134497202814270091007647025585624199956526780445715292511635827391990308642353977808659410/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^12 - 969230563417278057208401944708360087600480882587016130630814834128566812490458651129022872122641492352446574614465711341869067504495224379881732437290552428949497381907446339830595784240212708816615679093902671696459/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494*y^11 + 20008370238928845828479780333740369101565412167887343542584531504822878552604269796858376599353007768217980289194641470451289574345473743934365114156546666255502985769371803120521817125258369086131140374517590341925/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^10 + 97475686569492549329314617784123468400949881994991378344648556744148286496418494518279790925460330545054619127425835870682128800679813460870258103728831326957012810967044955055824907046092087388526075997927431084158/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^9 - 5879995512011188401932449429241564267622898474641098177003210515140865614426484545771878541581221171700887311526789500334202852744817607312916148767632270192761459208537200283445730532659888514632697566590408980537/32785360423231950406021485665064694503211616112030050722805245655106139161810802680366632630182396401922993230645509386188719076871531645252659116971895975643137467361338877063476718360333272924029332736026*y^8 - 4732335828882491196317030303103683411622129275482363410910525099077806023104802209234115193221991788070382305266609723413131455323843196286912288057627754088107321395822131175128027763618444466377886132650702115137/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^7 + 3410842417941683601851563662042236652971506660063542960411722405621764545936171871821685549620605352301995302188690344324082631964551730218907544349384834940158408498586543161735783617195232565706828896744998418483/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^6 - 349365735081243690262037416339652118485780620853440109398424132891452413237252958772169999812854546770377993597224582420413574969651553562060917851933976573169666515566193165562746283692618633983822535669409322354/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^5 + 384383338018049975557853905298396964981120437289861819935283992557852728754538811550570863774955373827064880914822109557355804904370365007574824107312358503653118511118263812037772366616849259134475034587580335167/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^4 + 51848208602522078648630773955785933410689183613795948017188195276975687243642639239204929432761139127835890868454572826909965811225622791246074121560166228793662140645230676313445764600568170320488072490543912120/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^3 - 32117004163595134404005650694272289987074310712642934330473738348427144040277713086179212566144953586564324982144278237210324302164556847389613722488242949917180115270616038788897017455505972156168197243313608656/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y^2 - 848120992406582072139104481891811351933964586792733369872909510949540565057092885123939676170823227123935297549922122659224954347236137807050004568376284749393011144993685235719944383761689407267597905966795280/311460924020703528857204113818114597780510353064285481866649833723508322037202625463483009986732765818268435691132339168792831230279550629900261611233011768609805939932719332103028824423166092778278660992247*y + 1149959729933477453066027235457239826743264659494037514683725125368616760484532435965067709139052244555389138139092880663903380583817471378182317839963149747990507016492934954223817695934969920696103948335109697/622921848041407057714408227636229195561020706128570963733299667447016644074405250926966019973465531636536871382264678337585662460559101259800523222466023537219611879865438664206057648846332185556557321984494

# 2 Loop Invariant
-55696287571565202251138848110486083282894290194496318702631411798963642725091978811969120566961398775737844428047466622499363532327601406147262798937441924211492631729777020912267303408076745492669020916321117044661762280397484404718282638292152488098508653413738791742194671917782230283049887247071862567996667212899445869396242383723843225795796047048893/469376263013351470998113209357485739599701928384952326533718224216940819776291836055049691199070783955287382402759276621471358897768017204151999084676780604420786255732217347247050924192246677092082518260568558539554986676841085501417199224722436501537453136017400716767328911934588735303200200711627098570329769140300538808882147822043418638970908759113328*y^38 + 45039068742592935616958904951306962256996782199664899869104741522927758589478922473597601718590215535940828577871669687811812181344830483552944927626429074597523007423713329174057525062125994033187085294399406248470003058562031959130807287986667051757204882060194662011825131891360521329360947777350201106331258731862213390856421462599363730648514507584861/74112041528423916473386296214339853621005567639729314715850245928990655754151342535007845978800650098203270905698833150758635615437055348023999855475281148066439935115613265354797514346144212172434081830616088190456050527922276658118505140745647868663808389897484323700104565042303484521557926428151647142683647758994821917191918077164750311416459277754736*y^37 + 5635554489041606987017220664628771074896470728592755092683697344502313748298211046213650124586439180681547180061932701182335260063830639895901019253263682392610192326789555310364944287729782585334216186126233060725917241362652416343591532741905275672776171924293010709826605723660050196667332290135937892764900771925483603476345645386987230762182535476963237/234688131506675735499056604678742869799850964192476163266859112108470409888145918027524845599535391977643691201379638310735679448884008602075999542338390302210393127866108673623525462096123338546041259130284279269777493338420542750708599612361218250768726568008700358383664455967294367651600100355813549285164884570150269404441073911021709319485454379556664*y^36 - 186559843664639076991879777998178205899760446112926932109378944546889348157762575564177145816349546880772738263483897089079631655135539542188270418444128495604604537462354394602877838932898749580184941564339929321909837686366943697766282278775017376941514459290436735832851536943286948217879070706654952760183841552511052065749216737354397972752578383621077803/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^35 - 1172064245777326830817964001112527157291499908467241738164680811658007855660323545020266557627909536909729316074552458087009209286855516271567646731514606097068756948871398953611060263720873682089601802814555980015499159111990888786044708302423020522778571823491206500814207626843195539973589411666618805292661417808652237012236955434205710541679058838302679757/704064394520027206497169814036228609399552892577428489800577336325411229664437754082574536798606175932931073604138914932207038346652025806227998627015170906631179383598326020870576386288370015638123777390852837809332480015261628252125798837083654752306179704026101075150993367901883102954800301067440647855494653710450808213323221733065127958456363138669992*y^34 + 7231225576528573621800831092643456289383071760639895354038330278616664159593775338615644570856970813815796908817604253523963569904909898889468194654162111363073397436435930285492455902788102063198381971113735403341183403247996240381884346286464666505889499251955926815731176306233717761209010369005488100828089688542536968715538847694789921267771371675835383349/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^33 + 38713391024972745314750406283664281895949109266645245839819271322472463494815727606259488319089718200268669606372597768350893538018160195453121988981465135021955808717564228022226861610627741968201655706993855878587197803885745222182700307838178545566614853275527634705704796475899723062585955020697165870718075521391726134676663765305408381748762848037937750883/469376263013351470998113209357485739599701928384952326533718224216940819776291836055049691199070783955287382402759276621471358897768017204151999084676780604420786255732217347247050924192246677092082518260568558539554986676841085501417199224722436501537453136017400716767328911934588735303200200711627098570329769140300538808882147822043418638970908759113328*y^32 - 212657783265157632941738584806087775301382605594641032543521202304643391071457376582512382909703785717113687655321039858296888614003592831110337589414401819374518552355175615369038779012173696812156559236188500062363514902861002701407886502915367139147026561908142749742623157055382218880670680781289156648823752930935236272114520703942804391055640483264526946917/469376263013351470998113209357485739599701928384952326533718224216940819776291836055049691199070783955287382402759276621471358897768017204151999084676780604420786255732217347247050924192246677092082518260568558539554986676841085501417199224722436501537453136017400716767328911934588735303200200711627098570329769140300538808882147822043418638970908759113328*y^31 + 2859735772036631700819922146624072886464823307568246431205097647430262389564066764080260756304598132709439174423206268748557943900431089180141970964585366216374024875464124625166950395260338700942409043605220917209134253892473719335611727980943170108461101681558776757828068438272166401459736269090406292581434704762238974256644231594564284712596029149294848533/8000731755909400073831475159502597834085828324743505565915651549152400337095883569120165190893251999237853109137942215138716344848318475070772711670626942120808856631799159328074731662367841086796861106714236793287869091082518502865065895875950622185297496636660239490352197362521398897213639784857280089266984701255122820605945701512103726800640490212159*y^30 + 9040582560264169453555739226489541179847209383200499730350914976015194076947894942589132442597620593506997984619380856498891074332621737312413982351887156280323980703759906893293969211071312979231560973197011852686966301755592189205731761360995668487117848977364336009804390232297495613770941757986469789792805771330541198613577389205904736193741571515500516320091/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^29 - 457055057781597182239766335457314162534539454967689697744235391282936629551549300537007975307633125908083243959839064524023604693719578223911012640624459066552400279631884323078671890861171186510711848374517577010870366059246505704640697998908917546924190853755068850568990581691764722151330402471186736305139004948384645321241708662435007735095605914123808536179/88008049315003400812146226754528576174944111572178561225072167040676403708054719260321817099825771991616384200517364366525879793331503225778499828376896363328897422949790752608822048286046251954765472173856604726166560001907703531515724854635456844038272463003262634393874170987735387869350037633430080981936831713806351026665402716633140994807045392333749*y^28 - 9003362897626182594118890166715928693327554990706431259457237489183713414729501252247456330054383640741629095638569260158553467959020847177830489748007166799496242442620076347729242246075424354712546653315265237639220468244234828400169883513884824979707354420092850946312150935163723465642157555159028431750631023754767404801064011379484336352743598894407049063539/704064394520027206497169814036228609399552892577428489800577336325411229664437754082574536798606175932931073604138914932207038346652025806227998627015170906631179383598326020870576386288370015638123777390852837809332480015261628252125798837083654752306179704026101075150993367901883102954800301067440647855494653710450808213323221733065127958456363138669992*y^27 + 513763093717540571235055552956007964386545214247714225785769458004424172106754298151241048086358941367911085724059769419233664799787675862144030119640695265559251102111859726643243573214939527963332165941908998723504150370834722719302433774662639217040385348678392833531810738517088143729329500909942333403668132064978879083271238548744790810562266452262568301455/234688131506675735499056604678742869799850964192476163266859112108470409888145918027524845599535391977643691201379638310735679448884008602075999542338390302210393127866108673623525462096123338546041259130284279269777493338420542750708599612361218250768726568008700358383664455967294367651600100355813549285164884570150269404441073911021709319485454379556664*y^26 - 627492297567733282246844696499864385393637545598819006194697106314039938237788969838218107369618739399458010804853547729284728019948276779839099746694460668823612965149214062356069082612439422633948301147845461050552455301315068150415804201996256304047629236567194924655565210858353902203302821305152363635280869825931289594914242721550649850099343902487437830683/37056020764211958236693148107169926810502783819864657357925122964495327877075671267503922989400325049101635452849416575379317807718527674011999927737640574033219967557806632677398757173072106086217040915308044095228025263961138329059252570372823934331904194948742161850052282521151742260778963214075823571341823879497410958595959038582375155708229638877368*y^25 + 3631916118935222049578095686853760265064131970657189118163413902499109774209272255226342150879986273561551615201429160341902139968642157237035811749100678812423929678815275562868272645766861381350320293042638533669099082930783067951178752873155589675114921030823490201780939153724962234869275615724580585831018155632041414303981799193771721818921167479009505122809/352032197260013603248584907018114304699776446288714244900288668162705614832218877041287268399303087966465536802069457466103519173326012903113999313507585453315589691799163010435288193144185007819061888695426418904666240007630814126062899418541827376153089852013050537575496683950941551477400150533720323927747326855225404106661610866532563979228181569334996*y^24 + 135135804727033694562440139890876139514162740825366004736017147787171485236367616083446730042362195551003999941861406281299062248251748564865868287035514609235313813726870078041622694888316952326590891781221141634227021019868436651763686044799606298994655231482950056815987738881513346935340858874327556606146443000605505324215797216536695412605384503505022835894/88008049315003400812146226754528576174944111572178561225072167040676403708054719260321817099825771991616384200517364366525879793331503225778499828376896363328897422949790752608822048286046251954765472173856604726166560001907703531515724854635456844038272463003262634393874170987735387869350037633430080981936831713806351026665402716633140994807045392333749*y^23 + 41499851860312155505224761006278778548670621596436422359750304661153237291185320317644255250640664742257118597772701342203394468459527535120639259485838252347317751085614686421388152127764918058874957584020095525059297101558650727525189507053958323169030099442795614551802983243049554861282548226552382780311433466656172546648418470803172481129241972742379291445665/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^22 + 11472935584871342305738082870797873366345713367639654110488082670488206578751947874584425207684115829528550510882168319007420872762622875635598463653622807237227121360853210627381291117245287000480938272001162351982464651027435758326188002817307007646160056134363666653118310143821592051304057472942217075880325156889273300093193307156619494221325263442851879636673/176016098630006801624292453509057152349888223144357122450144334081352807416109438520643634199651543983232768401034728733051759586663006451556999656753792726657794845899581505217644096572092503909530944347713209452333120003815407063031449709270913688076544926006525268787748341975470775738700075266860161963873663427612702053330805433266281989614090784667498*y^21 - 24103786665027749174179079991596363798243959874463315713849738527266187768534529431199426613654415464297082527950470633079694380103501547341870861126236583303174984421735733434570294659324084021179870999779929865762554852771336519948998991776867735330807557890730464078659559623370394718456365847402175546624374079112985332465258726447361453581975053317106276577367/469376263013351470998113209357485739599701928384952326533718224216940819776291836055049691199070783955287382402759276621471358897768017204151999084676780604420786255732217347247050924192246677092082518260568558539554986676841085501417199224722436501537453136017400716767328911934588735303200200711627098570329769140300538808882147822043418638970908759113328*y^20 + 7626117849714052546383203251895108706545341700678606378043761789315084492286784846738993109824925422179307864777941182781355241719319179275230336972948095043052328554102903095931521428788968976370647067400287978330603414433413829555216361735824899209129251870565554428964091904880739946936710741716757514059790433357598134116310973824196969973591729697064160935697/704064394520027206497169814036228609399552892577428489800577336325411229664437754082574536798606175932931073604138914932207038346652025806227998627015170906631179383598326020870576386288370015638123777390852837809332480015261628252125798837083654752306179704026101075150993367901883102954800301067440647855494653710450808213323221733065127958456363138669992*y^19 - 31636049295415854571361902464179478242200066044683305078728904769782221837837949988819776111471363701754388825751120286868935963253179076592558993523745004829623120205134792568532962364164063063812327573279608709374101250994642930798626603410986095139049823203339847569735738555456299340216266832220702599117057957045663916796695669505855750562022459832609183851765/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^18 - 517219125820641298943701373737336929398237842102649073091682269028312672622269303831853998824830802507462213111398705092803322670098040800204756996040482222535576754218722804892517891627223510528732764033300221386847910694506145669773914471098019955085980822751648473643372888342211989047324591478964130996249374016607850374639743841604106678844742750185957642491/16001463511818800147662950319005195668171656649487011131831303098304800674191767138240330381786503998475706218275884430277432689696636950141545423341253884241617713263598318656149463324735682173593722213428473586575738182165037005730131791751901244370594993273320478980704394725042797794427279569714560178533969402510245641211891403024207453601280980424318*y^17 + 24756310903393828880582591600337382174406205386991231558394403988432591033176065514067936682428480616092614989046835521416662071020163536874412560365115868032992540298136859644997945191089008235069085359363105625240257977626057376226245944387365180391542994312912393420756609544650014833372355333465619478506376918084111905948668258387943525853616126162019875443/681572501955495843656505144275148702226091861159175691965708941263708838010104311793392581605620693061888745018527507194779320761521806201575990926442566221327375976377856748180616056426302048052394750620380288295578393044783764038843948535414961038050512782213069772653430172218667089017231656406041285436103246573524499722481337592512224548360467704424*y^16 - 486689276856372031851703253503410145446762233344929683769910158654975935187018906726075603624231792279481082472381592605550378612477894367085128639489347286395810317741570743891539369398940134282170143597274453432213303966577564719727019360894775575320215822162872559429051163411369405661279566227156851228134235507279628789088435820635630668947111244526778984025/11448201536911011487758858764816725356090290936218349427651664005291239506738825269635358321928555706226521522018518941987106314579707736686634124016506844010263079408102862127976851809566992124197134591721184354623292357971733792717492664017620402476523247219936602847983631998404603300078053675893343867569018759519525336802003605415693137535875823393008*y^15 + 17491986419271684346964268864677559651555027161505944034885430108709503979284024765807171789511165616854596207262617436034308245789779756090370803188808649652318453438195652910721491039544044783222223313170842939080664901735057382352174382482570686286648488844203085189319565886888231477894951356572449513159327829370567628473696454621986504725949401447241673474069/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^14 + 2043784974277036695308983559300515623226331147969575949833247176151148615431226928746146594853961636787423101656264534281364457624819911958917547538373751298895216105384521263492494829732742003142096694282023286773064269645567093673360925562115583072142785873876214455186280436674675848741100837773971364555797287187616884509247674935423746478582695026489307197859/128011708094550401181303602552041565345373253195896089054650424786438405393534137105922643054292031987805649746207075442219461517573095601132363386730031073932941706108786549249195706597885457388749777707427788692605905457320296045841054334015209954964759946186563831845635157800342382355418236557716481428271755220081965129695131224193659628810247843394544*y^13 - 712939536015615856132160033157802696838831590050296565094084836964414147769733641764002952612696879716067882749232147805129486519249529910664837246659435149229820677622589977179583788536234205352245035289885893432749308255299694620741379015886979994082417288512124550957394350771141343386439291713136245160577455366818988932285922019279387696025736325361897659395/88008049315003400812146226754528576174944111572178561225072167040676403708054719260321817099825771991616384200517364366525879793331503225778499828376896363328897422949790752608822048286046251954765472173856604726166560001907703531515724854635456844038272463003262634393874170987735387869350037633430080981936831713806351026665402716633140994807045392333749*y^12 + 1768088883839158043840778340027261187376063271840261253317016335127022980486690712605472713373707284109078844766663155584777686615256163681602923259325649290143976778209757503792799340113104791375273186244368672317915777951141040335915833875366390835090922426320003776576789970917914599485198261566825328435020442801585217161603706436911531894164156094040840661407/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^11 + 64961872677791792356102559065043418298378903672616109413243315368701295724721588719546730358848309446244742878593670892099985271116020871655144124699838730278961890361094539392540790470931480285366748000144725454635213114052649962302148787893839697035155300564772767610618041287486372069680587625858551141996607725097948037876057902130900159209039581079259985290/88008049315003400812146226754528576174944111572178561225072167040676403708054719260321817099825771991616384200517364366525879793331503225778499828376896363328897422949790752608822048286046251954765472173856604726166560001907703531515724854635456844038272463003262634393874170987735387869350037633430080981936831713806351026665402716633140994807045392333749*y^10 - 407578604971538766180455567908821736636498548788805199122744176820454576705491799594001185249324598624682632029038161287687681588448316467751161344620616387147963626408377528435070198222883853136486537660666994871343035522396053878081505707179462846138599579871213809192997838094294344636049828111751887023243956225820374563140151452048842225732929863139016959057/469376263013351470998113209357485739599701928384952326533718224216940819776291836055049691199070783955287382402759276621471358897768017204151999084676780604420786255732217347247050924192246677092082518260568558539554986676841085501417199224722436501537453136017400716767328911934588735303200200711627098570329769140300538808882147822043418638970908759113328*y^9 + 7270418482241671150535942284636363140096256254756576416151410860681044572416016167526033139708857412456022110444411510833975746185225567389767605315304293993662587312178179223890364153048574400729193186988734718268251544765192755433358964420197413032648745316512983087847979020525702173047201311489130260592745204795985693219224725048675294264644358275164220/112975673061621823892357158863322947592996292133733711457088789525900389869133144108243667650610747100919620283077489559083285999141852664670731487005001750101280388895751928894508406015463738067734880839353792973256174585247372954448940763331780287597268887038848054420891105247413848356033424433157998693115316705784789507914509263970655962525090362431*y^8 + 21350546172724793244721270663615166088226916483736295096522771419425180755174329356012506743979529652232605111979796295615210418291568024209213722878464769275339641815128320105699628587178615965335789648873589594490906886192092003260309166575079679612799147153731317150470746466830834812111152577827136823210325875432216588419066804499648209643793279477925273729/352032197260013603248584907018114304699776446288714244900288668162705614832218877041287268399303087966465536802069457466103519173326012903113999313507585453315589691799163010435288193144185007819061888695426418904666240007630814126062899418541827376153089852013050537575496683950941551477400150533720323927747326855225404106661610866532563979228181569334996*y^7 - 9574266503738237429331865688316005577862412728760627283538673356744626453911461657014267885474297979403994928345095485892133723500827040290452085919314776894883052419709131434593474863268725540214317046032021943316242951110928878480384836945185589741761151292198152424991351670250596168162786379336376855877821945300416426713853370150198304557259185212799684013/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^6 + 1214866091249074624287823900880596997814847333518813177651495652996265488121107444271119397752831562238399734458013056820980641927076154583234925118752735069432917066915429443413039838297567909989366555901758453923819580600579498844497686936745303340251626356445872568195833847428522915794127212599436939042553637230672045130977753947354350383598561977038001369/234688131506675735499056604678742869799850964192476163266859112108470409888145918027524845599535391977643691201379638310735679448884008602075999542338390302210393127866108673623525462096123338546041259130284279269777493338420542750708599612361218250768726568008700358383664455967294367651600100355813549285164884570150269404441073911021709319485454379556664*y^5 - 188080712224611443040938172778541617070484161948430441502614465537612441244218334866667370319993045980803706039568208638637615858893411201022232575827062775116550804677551722145747193602471464459594907378751577334711190151738069881966500042450614917540951319017746135703513711968561283679986017047148086493707920779041395750637757261749002323263470341081151711/469376263013351470998113209357485739599701928384952326533718224216940819776291836055049691199070783955287382402759276621471358897768017204151999084676780604420786255732217347247050924192246677092082518260568558539554986676841085501417199224722436501537453136017400716767328911934588735303200200711627098570329769140300538808882147822043418638970908759113328*y^4 - 413007727888034903328557014318574331779242664740110151336192617472416846646267781353822623346128140821490862949715169108225914655239902143189475786742056836483837073293509414253983888118410332540692969361805953510403211908441708148317018562335420407269243339532446954369938326013306740872681716693334230743478916169218627580872471673370771964637296165925483337/704064394520027206497169814036228609399552892577428489800577336325411229664437754082574536798606175932931073604138914932207038346652025806227998627015170906631179383598326020870576386288370015638123777390852837809332480015261628252125798837083654752306179704026101075150993367901883102954800301067440647855494653710450808213323221733065127958456363138669992*y^3 + 65760890113838222809205412596238551893725658953508122632380773930746483002627948285108652036884545054882724411560325184674145694082779754836013447386990479828434344745262683520139503994784114055302000557269945288478725151129294630054492160789343883764855236936662325283591654493997054234554901757784590679272067199967845414530403740574965057926095290244497395/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y^2 + 14807552366713420901247010201477795576639996964532285993865341732267039898884555429978874026623944304283949581915211777655032000797102645290063675759953065029404911704412735344993453406337721533771100527387748898067935214877315261822635611738968570233025481151410816011898658127565507965774089612359381712936665089452792997069760050535899569273539383526696985/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984*y - 793782194755944861662891937172994774969655383262889735632235081045746504816344983729192850089641538191440857982628776131641797061804345724407966009648343214198398621035564752198745400906408078704897028716181838690630730313907630572572035835851486298493107006979879493182878196969233195608643577815357166442933440266009538630901680171116919793702523935868623/1408128789040054412994339628072457218799105785154856979601154672650822459328875508165149073597212351865862147208277829864414076693304051612455997254030341813262358767196652041741152772576740031276247554781705675618664960030523256504251597674167309504612359408052202150301986735803766205909600602134881295710989307420901616426646443466130255916912726277339984

# 3 Loop Invariant
33879372390967043627882977625554377155571255509901901852730449485517564373748635011861526648615998995157880026119109400770839470760554120264069436414331746487089111623426886060849672351225798376748873146296258129857298669874810906836634888590664620949747773579767170567378976309386708091651352878195253485761659504705374420723396719398806920472402611431065642777437985386517379787493250706334785343618475045276225372222641535102867/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y^38 - 18387114688442216628212291644035148570536727236783357049813908926309938902275017831887835099169475681420548810627784253031244935669245296378941351765985618798445748755076291572032708821992803311480970416642842881773465440432007923608691602216705909118772397643608894833318437659371988512657870220377623501008255537578652895833505678574812371922321327685220296641747041394127314317946518816716733258413141134952419099775613561344995/30326779921567543295239795128025225774320057533729688730807890009534002849343486674181105091025305635896009449852209052571087065384727961656073859708447188919799348891126515125188952581464079261941504458632630265291895938920216084039522004496804624368416984741092058411232518493438170928059799168283798216455098443057491101335024792962043096366973375365232343630347096463184751476350340940253283063507732299091723467623154388289216*y^37 - 13700526520008811938613714700961034285109449515769394342982592904051762035912879172252333803836946794889895284302898794612465933298239903264841058211288777766824345790852998630998591647005096337467533161521307768178521960083773699666763861097776356299707553566883635064098443759432192986626417806998357767691163901906327928097361098820541042538439049069521141263410022320010687533518573055656171583332627571555765436860212892928987091/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^36 + 38063877440770412743855830906228244687678136953810241705373451946249474682672272452980306606989274064294452740562064025266900492983274126481219743473457122254927890082934537256190536096293633370030230289500418286051358937450190023139901797518679251444037611531209016118557309698855473204964769625182827390073080496749561802700248103566710785000466293407691317555814356276078450814556963029346934698982928110164094463800795208062755513/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y^35 + 948063307816093979415466225271131425465032330124949532238846275863384098823503619724682449715085063232502659817165445075343604358509111457164166494108135756635305308949215520426350040521723285672117275451728615180374454786064604398185951104451649223836497099885550186407773575488311553374918226270043198313031112272580815683730795566244833876304557394649749084577313114838889266371165188080074088640115491304978918695831870409472798293/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^34 - 2965461384754568863461523946784525808038823497785922849493848835310513229695886135844477193522362088171693363700612325807548850635630192442310098157786184602573363574776851705311958419932100113099288463062869073206530575946999732480879807650268014679803064552552183958259916435231410175741613003780536080116550052445538460421615142327104470054388242050947557689297560420868296889197960374203389278593504740511581239574346276785927777055/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^33 - 47001247433285409073887425780512191080624673667555092761152086380754051183754545858723818548571791418227453244065244688735269094565184121343915039448974018178493489311813086401058991217090136069397561301416496021188933289981944359570468371641226775578932406812759623104128468230628255313486033874126359231994660251608928963118091678302469173739727906540939324198250906903083620080897054283565404196855058775332555102672310623301951357551/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^32 + 65086550129702212533720683226548552735786587802837906683005606342283938398597559282216911641604489658312386722814521946474279504646085548286452862378138628984377667528624492307427315722333249904750185543560020080384428572404886036211943241684608983200636096540846310597105351376750047258655158160027708134061494006584794848910072876619564835631785090714484798246662931096698700632858265702482584843988641661690785772784212184218820481963/144052204627445830652389026858119822428020273285216021471337477545286513534381561702360249182370201770506044886797992999712663560577457817866350833615124147369046907232850946844647524761954376494222146178504993760136505709871026399187729521359821965749980677520187277453354462843831311908284046049348041528161717604523082731341367766569704707743123532984853632244148708200127569512664119466203094551661728420685686471209983344373776*y^31 - 9672259614862244943416537584112011176656504138922066310315126136261633431538547550238589389949826582698728827964325060795436483196184374272807740865009925030001332768237052272534020895877237325823433105513375662549940471389048772850326516588797083108240329548799741731710711885306700132442181614275423096452455978611839677893163936163971799303555997375402053195195134555612265413515294500444260130891948133230929073900644354080041438109/26191309932262878300434368519658149532367322415493822085697723190052093369887556673156408942249127594637462706690544181765938829195901421430245606111840754067099437678700172153572277229446250271676753850637271592752091947249277527125041731156331266499996486821852232264246265971605693074233462918063280277847585019004196860243885048467219037771477005997246114953481583309114103547757112630218744463938496076488306631129087880795232*y^30 - 1830142245545304566821810393753964822498343201438277329299297272354958641090144561585895162817918658664368233003545886490749948641191536421829661266273201065650571388169288492299961994887588794950692830955208227178740025678016737364792999041187894919275860431493988912087901511672173106633461144079022765824129885191029850576580497870543869219861281999771898525363759899372523795309245397398321391025345198717523091266677204799032645167553/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y^29 + 1546173007384349495419520478768219220170228411860136432161454527641349375234481718525607258133191920697014028203320626438906537638779561220589754141256696332627552338694736174716547692538864873276448792989401338639081152410143280095071108099874521149283489946694371981598505338928578570728647831293851353476019630420688318652495699051868070622940835567762722476879605526437001441461054902715617800661081551066059664515956495398080361689401/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y^28 + 7216716623073863911058223174278857560022930165490875703382977717801502296472592755645861789921536739822108488981099787734489005555868669114442734442187965341197698750857538126319784158420027643307468809237781906592237683584001829030052974176422207567917013362318420577518174071832244352450824352066479585871177925207975176691327094014095759275353052489056174259683536402072110339640922259580378143574329917883156989322187077603393543012319/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^27 - 1511293573198548751589234087022629705119718962397784583751495105198453127981242638885231339128129263269447638486745982157322128028678080756125215864728562710388465779429393758964521108307495105121534223918236467535679291457473466522085260820890832697553642796946349537181800408355427849101278723126730331938748218143746876099844417479641061756121251206057488523245730983837387207428917563681029930546833903811857021120230904285621097251179/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^26 + 509409554208144818987827729204803156668302106731426322150409236829133251162137759612690823135304041218801068924691103625845864328760738856322995570673686458327020153292366258618520687350871031165681690514944823982443192862358782681365343163721162934874257069693961948185447389195266539183447291547677415703713708773838997823032524431963892045144014751091835823470573381368912097427988169078263912466390495362244332876714158798511451967187/30326779921567543295239795128025225774320057533729688730807890009534002849343486674181105091025305635896009449852209052571087065384727961656073859708447188919799348891126515125188952581464079261941504458632630265291895938920216084039522004496804624368416984741092058411232518493438170928059799168283798216455098443057491101335024792962043096366973375365232343630347096463184751476350340940253283063507732299091723467623154388289216*y^25 - 778180931988208470702058267838347260091166866483558089845876946712394373629250480951880760555802518386221753752244344748410777598934071189774394313108407894672992838574812919751997814363061614232561464423974268704693415083515912076965183404664035216370951424465027479834570779905843558174084474395414842467548951962563960563810747848599674532501463145941339353237776736482596048924384415514696248903090594305302843588705225229286420399439/72026102313722915326194513429059911214010136642608010735668738772643256767190780851180124591185100885253022443398996499856331780288728908933175416807562073684523453616425473422323762380977188247111073089252496880068252854935513199593864760679910982874990338760093638726677231421915655954142023024674020764080858802261541365670683883284852353871561766492426816122074354100063784756332059733101547275830864210342843235604991672186888*y^24 - 719259136399243031493679339000554778144140569199420312072842891596520418531177321519898768993989563933271793020054188797781078321884877119670298493200489253528034697855258650904204172129528228862357821133932393590929434367405142249267338053488734909940580377060067569095595988648010359461282113122107861362019059368979868045383052538175749831735125595140267404489109052642390865335740885205181770166770450706208205914605767706931622250619/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^23 - 4195201656813689530039802353317148708874207719946978682843405151877142898720920495083305541033107313281161391636108704090877021161409936933699009106882029384279499402290230320551007081683308396238092231107615931513592518684313961899837139129252078259233119255131368927752712102738162273163953328685552679614055099560256958317648968017052200687871065661186647228244251345632508547858632960562417968293434708622615880575766653095436114487293/144052204627445830652389026858119822428020273285216021471337477545286513534381561702360249182370201770506044886797992999712663560577457817866350833615124147369046907232850946844647524761954376494222146178504993760136505709871026399187729521359821965749980677520187277453354462843831311908284046049348041528161717604523082731341367766569704707743123532984853632244148708200127569512664119466203094551661728420685686471209983344373776*y^22 - 36637060399365757515127196715949808010505232475124491726909076363444163404120657702157786871863599294700731031994444489179063258875933438801046350824791401423248149278062229541136672433168708935639208660367200693774923443958841869532130417832021115453603508445867883604044836794637967457195091190821157462584985475697695064939689297496900960989895627597499669708884406624246380031421351935000905615285113393188552781057728120427281262416613/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^21 + 15341096222881237115033264421393684775266858674840723561342627915204676470543814600770878664194671553914787215732076674322055924034585218733161285858252357477046012023613341477583303801500414383436714571088404723890908048641384984920659110540873621156506015875687889630207718039288156407521507430867620656008440483657514935103019932120113333178292949456386215762449453096284513126314114719004811861958624680526868243662184273081775457361463/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y^20 - 7012544906070716880803138103473934462743282028929858849427702914692101259058026183482318103534992350687739426069961691862423228802516953257962806547911625677692617259295952706422250079954976845418989300671886511370344688609892907100732469024234589889240796647017658018236040766463752263305182159328410281528898427161535743703646636113012630582781160795986983852283301937325236165771738379228767575383724730325658367208102819323395329419935/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^19 + 1618608192965033084747864856158367860462590305805129538343016601249977510404739226117758649006959668831932548736118867697246228967842250117375840802944401639576318344851854905010918077942068261060334020549690585191071524420309539849514286839789232490892935054776485957101663390084654999110659488533700453942138859147195461547729831257928670667307735935618859058221600711456394730349071718354457649636954657563897108844088519378863666202055/72026102313722915326194513429059911214010136642608010735668738772643256767190780851180124591185100885253022443398996499856331780288728908933175416807562073684523453616425473422323762380977188247111073089252496880068252854935513199593864760679910982874990338760093638726677231421915655954142023024674020764080858802261541365670683883284852353871561766492426816122074354100063784756332059733101547275830864210342843235604991672186888*y^18 + 819748802766565096198823490125039674366127575287591322585212316009339710319258661315021500358021665013021698567226305514464136829861822099815938234496951019287024889241915990434461901693997942283322603743918919621599466874723829648764838991141524409187548921978092309923207396667914790294255455655186575260150328447691830397581314289960416116581048514967472639887554276987387710734439652406313383497728566632712142956802823486207637762861/26191309932262878300434368519658149532367322415493822085697723190052093369887556673156408942249127594637462706690544181765938829195901421430245606111840754067099437678700172153572277229446250271676753850637271592752091947249277527125041731156331266499996486821852232264246265971605693074233462918063280277847585019004196860243885048467219037771477005997246114953481583309114103547757112630218744463938496076488306631129087880795232*y^17 - 20752316643721235850882710886597114515375424476131646576613220996968738198657077140789155573552841018909081543721083767939886074690036794622275728484633095388263032398634659135877570332245907761658676944540761877780221662000179787003836531249374962935796804429934018189336145749608579761860493833203967311743020099234009746279669169782686306821093002688432369845867711739888395589684401362396203925124484646002198501519132928200674215579/557801373194369140957943956856223900979749364124747420992594298336056199552300335730339783862033695142327376134745374635867041860900127077894872540620035420596503028975221478585275991333802038699795338542129695102174271867845213549613667072061266082284533117212729051126251550218127054823945967277243142413017299533487251621844599289718120843148590640793237685359723942691684683495311208000786426143898270748056869201200322727488*y^16 + 24899380419767663771376646649321276132147779178536293645703580607417521980982002970887446894802446046778320533880392285267743174327403723795569039855810642947579131805822162570332595437478227234612690455036637464701136606612012779208837223106741904751679862992138493308057728178842711210122077497432664451045947718844446421097238126325675270197737369850730495750395162505061447341254631234771071975102036060743414573945331743081717987241209/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^15 - 7857094473894818430418117220634409550209834646273634347974065230125991210249311193140755951272832966780171934538905175060167185055162498615136591462668311893017890940905257813757763044022271977654881953510211031059047343756906625230820085404976079085899918938273951744500531645572855260657172301969030191325781523257862117530067240529869046507050344038412646403823599277134492036445167355350709854871527324472577218549641107677918092545539/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^14 - 19891833274897017376194822541981754859618961309399177738865526855008436555748872656961285561518305435363224564115629165696617985616182236437098778643819993953474079546423174287956869082763356239158541046240539573860688099505973565278973069858244541775051830120186260776161069233468806950094520042883322774568432673086827861051491260967474543888014391913096213391737856826422265288340094383382174191852933842237876787639856705521090788565/1277624874744530648801676513154056074749625483682625467595010887319614310726222276739337021573128175348168912521489960086143357521751288850255883224967841661809728667253666934320598889241280501057402626860354711841565460841428172054880084446650305682926657893748889378743720291297838686547973800881135623309638293609960822450921221876449709159584244194987615363584467478493370904768639640498475339704316881779917396640443311258304*y^13 + 4956980537176121378267712373052611007668975972325609349422778265466776404331707995872883703557712611185086051738288534324157049056640139685682624411919870038176872671708645658251239875198375263956702890469991178857717004493632059066973321310144983680300030905935207654619474362167504196025908694368109641133981641319132028916355491291662503673425893782609235241795443261625384010842578099107262893880553201507391263317148893886581977083497/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^12 - 209774264837518822567079323439728042452602782458705913822404271206701700765240221292209615592108758214033507987937288041241475268589730960760902078534235464156250076639721593925837815114254761461131365605075734999903873007915005863662038384537449256483422868860675620057832156581930385020686465991869303498071044340479280140749273776706061800546621481075942392481119644425906673630771155063608069436167702728550795685010491074332036277127/144052204627445830652389026858119822428020273285216021471337477545286513534381561702360249182370201770506044886797992999712663560577457817866350833615124147369046907232850946844647524761954376494222146178504993760136505709871026399187729521359821965749980677520187277453354462843831311908284046049348041528161717604523082731341367766569704707743123532984853632244148708200127569512664119466203094551661728420685686471209983344373776*y^11 - 406952771562274520689362140188255262046497818563236832287112059375063493654906631740512090759224810309514913841893309720620647190570716754063239745254461254462149887858860533081626777824612836513324265654394097453178147172337504881840245361750309657961705798329114088380764232514682646676592244047313785164792774983723746239458427548008357600615614748222081621371771964147584044295952881439516303895108964266227601407488623747803905967935/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^10 + 127940980558014226807443252929548679410174008021342586176539525014590761668434518663580956723254741984605335639053622868632103443991100353417164136879915107825168693165547321969402745660136779016628242233255124651705131785899436490646177776526541120804034661741810226854305157262613732725992021095834287511727254433247630082161954916167999653067589163911785583566107872439682251569080449796626449072825129563517356228240134695078259660625/144052204627445830652389026858119822428020273285216021471337477545286513534381561702360249182370201770506044886797992999712663560577457817866350833615124147369046907232850946844647524761954376494222146178504993760136505709871026399187729521359821965749980677520187277453354462843831311908284046049348041528161717604523082731341367766569704707743123532984853632244148708200127569512664119466203094551661728420685686471209983344373776*y^9 - 2752224420693074005753677141510427987035373848059731321844783523077520296625799903510121623310166518461542644171394166395429278041647513657902013805605805234916059014410536511033567677585253743779746164690602909792479842643081563866608037731507455871531904388387729272557005463505701952175332473215981020950207268705604650453547766353680620995752144387531020410507374128539812786737371299811344540080468689850716669934430116215210262153/30326779921567543295239795128025225774320057533729688730807890009534002849343486674181105091025305635896009449852209052571087065384727961656073859708447188919799348891126515125188952581464079261941504458632630265291895938920216084039522004496804624368416984741092058411232518493438170928059799168283798216455098443057491101335024792962043096366973375365232343630347096463184751476350340940253283063507732299091723467623154388289216*y^8 - 17399260474122905900926928513032218525962406731041160244746219611138431415160340499001583492805134412069282815638967856887727217511715149368111549501292229850538494320114745520245941266099896864700647058348872956819934294384375267220108546873979170842293475761923429670538619556256968952809053909688470822870382499909057219850992669162045643526456762583907010102860877999636222682207218203160206915445235339674605780164860663343645873097/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y^7 + 4836472993541387852906249524837872665075873496309968460716327438126992467676777059645455068562114359033864849109266114583412105200447386307263970984319232431943399840801502001294686729488405278569449156707293249112672866177059821100464224635650831529888783887651999194299307168240262583329624319999273542912434751829069734351445083414984658764515086648874234899246603697682605087510287639201022738270952690428040508595867100350206647499/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^6 - 2997037968841661322019487402253777910119954716262691744214591637632490322903109255625125778903136021048908430164444458798852988481140430645993180488472932233237712273592265557595222199167806274275704869979788961890581732130492736981757936674913136429279879806334596768430304549483194246867255371240758608313289218870260663549335310865887074213926156646432196521546963410673288420871686855460800136823258284634871340894380645870760100501/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^5 + 170999762045145502017015133013833187698076883796259724956313596467767971705540360240761703819567140892362253047074951779578396002623860954939437406575454567230447740423503825228906896823842050528956846997579009549976399522799740604981857995252475072861261762044342698055211797212102213393798325685301793730920834811890287023519373416097828803764036038036860961838984955257666158659031945752953855978963074457962692563663331150798134687/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y^4 + 336900320328768351748337984531305895417678277845902180903070549857024851467856465685247578920397907303359390149582372351806687483717148378554279521188921275655803943384447347376571238155654918338446432942291794691219319701256579990536219416344057376406436492664564218753776621904180481793540546900316853730331510957148059118949606094794102711388521391632977956740011057269179860693819145844380981398835775224515233913826452609216142857/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^3 - 35870087654380587253988680957673238432074821986502663281745566812524125044356900751259031743868001089840170320641391455297561794666665268754466364280839779617151860799831441350398021835882248787299072306017084716902131288327177879820259648243333701149387838317497299266624286247636015495991224605526006393535367992479195799266559150069259269103383494213445669988216174864842868275985514469364215532790105539967027912689922679192742173/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104*y^2 - 2997516831335423599333306999595874756401416433498136846104549693187474460661803967885620260313827589086844216737464064659805565147938236718570091673549566863103053534398577927918900154185903164120045366302147143318008321554020825822473177719782985661399655339148551723221659679818247371234605624924617334356558166916988890376232451642278797444991991759570947463308527546082156033602864949944399498719758266564869993008240844144148195/288104409254891661304778053716239644856040546570432042942674955090573027068763123404720498364740403541012089773595985999425327121154915635732701667230248294738093814465701893689295049523908752988444292357009987520273011419742052798375459042719643931499961355040374554906708925687662623816568092098696083056323435209046165462682735533139409415486247065969707264488297416400255139025328238932406189103323456841371372942419966688747552*y + 479106449392510677617308901260088433105806648447903196650675475457030099254400818410652871004967882963302829103239871901842935162933911579930122049572257759136336626712661698792656836212076271246506186740754134918767540268900996989042356149980651650319368900516940281375330755454062158728814569487783308535081045961653657353417998970701648889812096288826507762152072221956805922448127922673535829109800940189111968744670084966735961/576208818509783322609556107432479289712081093140864085885349910181146054137526246809440996729480807082024179547191971998850654242309831271465403334460496589476187628931403787378590099047817505976888584714019975040546022839484105596750918085439287862999922710080749109813417851375325247633136184197392166112646870418092330925365471066278818830972494131939414528976594832800510278050656477864812378206646913682742745884839933377495104

# 4 Loop Invariant
-260692361651772607764877399022292002605231603416165135106275394196331908966545365486406016515397505207713009350100240044148691402247157748928633947493394346294461345136894602792191496106954451938279330000931577967695411928093126691853028871349474692879896537590270966216952865128883999461537480016325164975455159080170251994680568235475840082081709641422943920873523252853812122507971520065864134626853906453639190242943698210200160343699564182408761470877443396064795888088216764752648835037423351860534446353758364522830462520444575052364031078777328951796817135052034220868726885/7815197637329756564612502425636216493828768904349790961216457521576642115722469655459141890490430891983092608207385889916451316525564003315414234399902109170390257265931146647200377078763087541234680721324461302585989701791948814797961685545422026635368341188856398108306908151581722011072247195359297101282848903531362286886058092459736597698384703431774164699334666065833603087221586767378087458087049129610406351374795309906629589849929736600182835391333308111868546416971059574237235298569159257466158081117791087846235082115139360264378728514376238425952664449051798816962929664*y^38 + 352598196270436090876478323637958732296239119199658469676082323674346048054847239211103783608810754416498796592089926018985677953730649061333208395006699399823731394018776735566654126824878549987731289686112743433427344554111677056115209974613920426422725876127558801012081545266521311826638770248677990276686596818141952054987636843499609339200279826978311053616092402606709412066604344508232285783961036817987738960963098325783788248898447180114589802617457610955693962169584814917849704990058701423612727951187621410161739847556310775100140620140850400911342571105651025251945129/2056630957192041201213816427799004340481254974828892358214857242520168977821702540910300497497481813679761212686154181556960872769885264030372166947342660307997436122613459644000099231253444089798600189822226658575260447839986530209989917248795270167202195049699052133764975829363611055545328209305078184548118132508253233391067919068351736236417027218887938078772280543640421865058312307204759857391328718318527987203893502607007786802613088578995482997719291608386459583413436730062430341728726120385831073978366075749009232135562989543257560135362168006829648539224157583411297280*y^37 + 263674679294848927886740165155057602978952158453368258638671785113498408766275290112000949536832069515878757539449952473484823977560277520345748873128986814629032222036754423955205686075179759474198311830601113695119267050233295513552598680758933899489542816983989101533063373737109567097658430440733242768404942486504835653021283980612967380541489818430126706230362987274990184013707298827755000013848779930954002564974110441932758648092393775296141829259194868635700328807282740232125805969837600179702760487324384310221919086127338780190284731002692296774319458687024208845199169817/39075988186648782823062512128181082469143844521748954806082287607883210578612348277295709452452154459915463041036929449582256582627820016577071171999510545851951286329655733236001885393815437706173403606622306512929948508959744073989808427727110133176841705944281990541534540757908610055361235976796485506414244517656811434430290462298682988491923517158870823496673330329168015436107933836890437290435245648052031756873976549533147949249648683000914176956666540559342732084855297871186176492845796287330790405588955439231175410575696801321893642571881192129763322245258994084814648320*y^36 - 1460247656872479849693739351120007130302753631036935353462366809502752482898241129346005154845247571203528283968932646541665737129206232823492639244752009110195755103131813409311725839923886301839031474228287610321634367856292547479109929315567145171416357215238139345235228476086261205542779691795862794329562214731433885113937192440971749723482311252259294047984889975977828904279329710900668057069196134763147417489505660666038136121900371659448451799101885350698592233786689905044896626247359655606094917409625205693002376686714489505951483986271290145254016125950136414322930922603/39075988186648782823062512128181082469143844521748954806082287607883210578612348277295709452452154459915463041036929449582256582627820016577071171999510545851951286329655733236001885393815437706173403606622306512929948508959744073989808427727110133176841705944281990541534540757908610055361235976796485506414244517656811434430290462298682988491923517158870823496673330329168015436107933836890437290435245648052031756873976549533147949249648683000914176956666540559342732084855297871186176492845796287330790405588955439231175410575696801321893642571881192129763322245258994084814648320*y^35 - 6087910956019541623381595750679641921911493772038986251088570294098912785682850799082940224609556626599326014559117696934592028522375733837136839164416928608915756560904364689203067807539172455857296059956838185443450185290431783915270510785046600356293351560914199480437167508508597163634547932176880221279088456342889887665539664381158827701944327834363837180697722524399691358409622627921875246305867551469918189771694692502755510606397838173125741130282261277163210387843832355941118737949023787613361488303789952915956072712623493971680424791371375640655461142464114318140270529463/13025329395549594274354170709393694156381281507249651602027429202627736859537449425765236484150718153305154347012309816527418860875940005525690390666503515283983762109885244412000628464605145902057801202207435504309982836319914691329936142575703377725613901981427330180511513585969536685120411992265495168804748172552270478143430154099560996163974505719623607832224443443056005145369311278963479096811748549350677252291325516511049316416549561000304725652222180186447577361618432623728725497615265429110263468529651813077058470191898933773964547523960397376587774081752998028271549440*y^34 + 11352796882351137950747024529828324188857547438201209074146002806426843211895223913685187495330918182137580420409304824517938672677067429276705376958745867750107165950860600083720953933550722327310251724532935972081739489361475035820214312339875229528672778268086456609712656689638842635730194345983805727894187196665278739165001300583719397114241083406854286551378649434922244059164941321709949285145442525757584803809527184427235860441221273960166799353275168009107354545291763146831866983133817613750934190545291195540495755182481906114576311830176938346125738920882561353784978940553/7815197637329756564612502425636216493828768904349790961216457521576642115722469655459141890490430891983092608207385889916451316525564003315414234399902109170390257265931146647200377078763087541234680721324461302585989701791948814797961685545422026635368341188856398108306908151581722011072247195359297101282848903531362286886058092459736597698384703431774164699334666065833603087221586767378087458087049129610406351374795309906629589849929736600182835391333308111868546416971059574237235298569159257466158081117791087846235082115139360264378728514376238425952664449051798816962929664*y^33 + 150872532232305989277036252636507050608245651270179277763894966428697708369109181180532790561135759384823415585942757242817564107220219018505751632849917883706689461230401042084967327551361052361281028989812263139689182197897792192677359114063499123810730683870360269562127784683974595515582533709264417119247598246384278959346985752392079029922782010505058445962105599311278492752356473766631006754785810497745494292443601999582543841040327350576829700078757649240718042397462401777051166212442266639293367087435753974153619927787330006114509451697144601359970965688910499818397618465497/6512664697774797137177085354696847078190640753624825801013714601313868429768724712882618242075359076652577173506154908263709430437970002762845195333251757641991881054942622206000314232302572951028900601103717752154991418159957345664968071287851688862806950990713665090255756792984768342560205996132747584402374086276135239071715077049780498081987252859811803916112221721528002572684655639481739548405874274675338626145662758255524658208274780500152362826111090093223788680809216311864362748807632714555131734264825906538529235095949466886982273761980198688293887040876499014135774720*y^32 - 998823976094158046568483330253177423817278674874878840161169558745048960346751787605384290021985852105258608446023986616066868843713995361361467610024294189122413930674542219046599216492886079398377118519634618711731084492075424586870084630528454904000796962335353293408216413222261732366661196325853769760198167378539295272316788278142986954211208487188899342973110179446517953085831238483245628264966370106055759839036493060240895086346655578385325879084397539294584210029689670913264811264612545225494457486862431898435658055014271733496139113679809113098192237995370980009912698502439/7815197637329756564612502425636216493828768904349790961216457521576642115722469655459141890490430891983092608207385889916451316525564003315414234399902109170390257265931146647200377078763087541234680721324461302585989701791948814797961685545422026635368341188856398108306908151581722011072247195359297101282848903531362286886058092459736597698384703431774164699334666065833603087221586767378087458087049129610406351374795309906629589849929736600182835391333308111868546416971059574237235298569159257466158081117791087846235082115139360264378728514376238425952664449051798816962929664*y^31 + 364040901490841353945492911664010919570158172003269000287737486526471253429187201363081110673308983953381661977971231261899768665186264005145195427296208563457444332353348912527749921012087348113981589125623271957435636847390909357231766848291385714828976155833209887652294646272522864379456388065468063153599206735895252178980830270732579428229178017369592025650128855962303597687669985297538570746056876203882298406364209061251952865996059504093028595635460275469772688115382720638773725013140794231624004090799750982466742465779682202399209394192628966037100502320987939887437804603297/3552362562422616620278410193471007497194894956522632255098389782534837325328395297935973586586559496355951185548811768143841507511620001507006470181773685986541026029968703021454716853983221609652127600602027864811813500814522188544528038884282739379712882358571090049230412796173510005032839634254225955128567683423346494039117314754425726226538501559897347590606666393560728676009812166990039753675931422550184705170361504503013449931786243909174016086969685505394793825895936170107834226622345117030071855053541403566470491870517891029263058415625562920887574749568999462255877120*y^30 + 70524190397609252418850852870390557012060375243547125887728253124284380293670547687872529190281425639531662135960199064447539947802013763122091186578911042686163092200111892134190269071229203911307282304178260680773684014305587691505538047855874738971544895758280989052639454620575142652147299773582973422685406926050193015398423088188347020614421477851818470496107534123871417560896828886421772997315878876391562749230794459377727397493871879868877708860535915639355867876716483642977945360003739198559352510245592873852391712865022807407695059943705357623751268930979852581591121006182473/39075988186648782823062512128181082469143844521748954806082287607883210578612348277295709452452154459915463041036929449582256582627820016577071171999510545851951286329655733236001885393815437706173403606622306512929948508959744073989808427727110133176841705944281990541534540757908610055361235976796485506414244517656811434430290462298682988491923517158870823496673330329168015436107933836890437290435245648052031756873976549533147949249648683000914176956666540559342732084855297871186176492845796287330790405588955439231175410575696801321893642571881192129763322245258994084814648320*y^29 - 19464229534751933360874463629736325726172878695762327089439039639436271555267263076777426750866966151155978152927817432232485274778648959394458223620925231036136415184595503265793997754769477633163752891752773869464342060098108274748788582608971644775776857477084237489927588639617274714810355660072010016152403901565580308463922813355246291143111942262918032721412442246304893853626525676183920346358715385582744228287985404280995166187425884446877308313536883196456546712775288670125379934709245746115747792791581822235888182707667471953594750407678822938655686752693230823556542374501349/13025329395549594274354170709393694156381281507249651602027429202627736859537449425765236484150718153305154347012309816527418860875940005525690390666503515283983762109885244412000628464605145902057801202207435504309982836319914691329936142575703377725613901981427330180511513585969536685120411992265495168804748172552270478143430154099560996163974505719623607832224443443056005145369311278963479096811748549350677252291325516511049316416549561000304725652222180186447577361618432623728725497615265429110263468529651813077058470191898933773964547523960397376587774081752998028271549440*y^28 - 4679900477406376809124326028078269275871243544958559148864999571735483929199138799390666178515516219764189883440222879998066419946172747996074799099176050633449898452262214903333254663787673864890786249582279345176782325392298338774387085167944459079041793760331853569149139005852561919352392342490047759682226029662342394318888551563622617849907337329919234429177681673360072787391393531381993064077792309364834451109125398882814760985158617507171813215934330110441500700144192440365308059736256408818940690278010179180279250091709012168138269717557569477091629160626220519535619436734581/1302532939554959427435417070939369415638128150724965160202742920262773685953744942576523648415071815330515434701230981652741886087594000552569039066650351528398376210988524441200062846460514590205780120220743550430998283631991469132993614257570337772561390198142733018051151358596953668512041199226549516880474817255227047814343015409956099616397450571962360783222444344305600514536931127896347909681174854935067725229132551651104931641654956100030472565222218018644757736161843262372872549761526542911026346852965181307705847019189893377396454752396039737658777408175299802827154944*y^27 + 9158818960563365821773027603040877672376707043604598296290775795610235574864298797717261705796019760400310435467397878649718894562954541081804492711724438185442684053760083068333675124179105077537062454858644840898524387193890166366902165344869564172767257611591350405673140831250213342349078637824725876924570995248319868584138864886551642950229511052208342121784038013292835201624513496406869585027464277414669640911734806398629443684578679108070927432009222586218342964483485313154629625298135209190275370430932927871797572496484792669552639474244366663997825247877807135118913873329291/13025329395549594274354170709393694156381281507249651602027429202627736859537449425765236484150718153305154347012309816527418860875940005525690390666503515283983762109885244412000628464605145902057801202207435504309982836319914691329936142575703377725613901981427330180511513585969536685120411992265495168804748172552270478143430154099560996163974505719623607832224443443056005145369311278963479096811748549350677252291325516511049316416549561000304725652222180186447577361618432623728725497615265429110263468529651813077058470191898933773964547523960397376587774081752998028271549440*y^26 - 1619904175563561828269573751221512925714178869205930405672372362968428747769377715263439330205854361228957037363060370225084782038445286240949836942805009680773613553807136366772593717547026695915037462068188167588546244438176879582140035750804052781629719836048349893123060061636888739298327142443986301513356285742548226230334541275039020074026788310984673057363665784204464448346279929158116456924201415198517675574261070948730449362953302753399412219345797614300582317981046961485166619671550585156585319674943392297903816155733021819926621325051864579813833061699514887832142413467181/342771826198673533535636071299834056746875829138148726369142873753361496303617090151716749582913635613293535447692363592826812128314210671728694491223776717999572687102243274000016538542240681633100031637037776429210074639997755034998319541465878361200365841616508688960829304893935175924221368217513030758019688751375538898511319844725289372736171203147989679795380090606736977509718717867459976231888119719754664533982250434501297800435514763165913832953215268064409930568906121677071723621454353397638512329727679291501538689260498257209593355893694667804941423204026263901882880*y^25 + 58143192630483941135585448717701056443287333250770935422548196287346951538589766469821363539583031686812848039316179168412599936648416286226607703614796007493427928421895358576981351807483103482801062744442894989756837227621027457955502716110409226511400938176867411393961291113065531914794847112724010412947068724445420879661372622722756635419222530745387796773524263903883965725024364982371701157532977981357129783428836321598589333081777242327435731679477427015349691193525439594942180994362074550263275491862782536989997670896611641747858619723315460103119696913209369310696303861149197/19537994093324391411531256064090541234571922260874477403041143803941605289306174138647854726226077229957731520518464724791128291313910008288535585999755272925975643164827866618000942696907718853086701803311153256464974254479872036994904213863555066588420852972140995270767270378954305027680617988398242753207122258828405717215145231149341494245961758579435411748336665164584007718053966918445218645217622824026015878436988274766573974624824341500457088478333270279671366042427648935593088246422898143665395202794477719615587705287848400660946821285940596064881661122629497042407324160*y^24 + 5856175550806749780270723394722977759765386773425735573529566460604935957669225404214413287740713417410305875409169454825466143959856207921841351077364077044541175174479006019188565506828407878512801708026497123292539742311018604191027109265232975352703141883057998158173457379752845156720815640807380567291140778184895777986979101813578990374240381774472607427967584330405265245318191075571033462953278600111509950217383670711095718557384823677199250151846181182070780268460375436786231249308280415013836691944631838189113992719578981770538525878396652381210271695027751344410193006570263/13025329395549594274354170709393694156381281507249651602027429202627736859537449425765236484150718153305154347012309816527418860875940005525690390666503515283983762109885244412000628464605145902057801202207435504309982836319914691329936142575703377725613901981427330180511513585969536685120411992265495168804748172552270478143430154099560996163974505719623607832224443443056005145369311278963479096811748549350677252291325516511049316416549561000304725652222180186447577361618432623728725497615265429110263468529651813077058470191898933773964547523960397376587774081752998028271549440*y^23 + 20098756423521657900176016596153533850756453139201609757631493689323321191508355043878945647438670335478146523564069456651973814722527093060446935142596997500863805971933525874125119900857339502012030036671078852443162389984906177818563284971634409313810511065081492156835073779410852462614839307721246543391625370409929947921274713980643093961219867507590658474656989459603957369178057248822473156184159612195771496740806132710983482177693298125247875395405265676046513821917266322735938381609242447199734460713642095902447603901778224516139097919868941426923988917313398055336666678713827/2442249261665548926441407008011317654321490282609309675380142975492700661163271767330981840778259653744716440064808090598891036414238751036066948249969409115746955395603483327250117837113464856635837725413894157058121781809984004624363026732944383323552606621517624408845908797369288128460077248549780344150890282353550714651893153893667686780745219822429426468542083145573000964756745864805652330652202853003251984804623534345821746828103042687557136059791658784958920755303456116949136030802862267958174400349309714951948463160981050082618352660742574508110207640328687130300915520*y^22 + 710290053983095657279352254354753118454542057369338896470525702087841223726578704595852198966788531600893869664045015027092582284246392740481477083252575034963150169732130701959239264324079206005291529835633549077435883002227976050930921841322180696993199206757820049690984675514288972685153352121630437850073762155238096714325854704523397112191743373948671631665144464987677761953053742332458771408158751592389110883806445465982370611961021578821904665970131907915617481483344991565217153710428186817572087122158491919422275648684372053653786971592082315418719280205126963340616651496289657/39075988186648782823062512128181082469143844521748954806082287607883210578612348277295709452452154459915463041036929449582256582627820016577071171999510545851951286329655733236001885393815437706173403606622306512929948508959744073989808427727110133176841705944281990541534540757908610055361235976796485506414244517656811434430290462298682988491923517158870823496673330329168015436107933836890437290435245648052031756873976549533147949249648683000914176956666540559342732084855297871186176492845796287330790405588955439231175410575696801321893642571881192129763322245258994084814648320*y^21 - 116353635437695716324610596115440870360161647146580269910265002211360312393936707152874907168052877477423969868225713554684018508050456561925704579366143150288395426869681078466630335521298546751790595657172877940110234656287722374063385689279244253806948095107674912817449656681758582478664693364720828493852639854037527479970642003030573452646290977599165375453756838791413715472862085750509181540418110468643956972803615716318549258406630952199708095840614244239362403457751718937589965581828978243051752703183291220709417662930474395668250356696898074449347780522211339239862070941350029/7815197637329756564612502425636216493828768904349790961216457521576642115722469655459141890490430891983092608207385889916451316525564003315414234399902109170390257265931146647200377078763087541234680721324461302585989701791948814797961685545422026635368341188856398108306908151581722011072247195359297101282848903531362286886058092459736597698384703431774164699334666065833603087221586767378087458087049129610406351374795309906629589849929736600182835391333308111868546416971059574237235298569159257466158081117791087846235082115139360264378728514376238425952664449051798816962929664*y^20 + 59893621680857491667408730513852708347242099929956704694391818224638104371902031638860288848351334094161314663436875235131387339366221522347436951895862864993595048792825281978565738825746014684003763690104221929420259708888671763946699503927933471572684506855972769685383530168495901002945779518426260876679073575410702980627603858575593338748584369027818133004216019910686045181597738149208190435862480879265234856474113824161473764263784852103378959411940431002877010246946849460004027347790798774012297584785792965257522861944687778580473545902001666355615581801649865177928069480512493/19537994093324391411531256064090541234571922260874477403041143803941605289306174138647854726226077229957731520518464724791128291313910008288535585999755272925975643164827866618000942696907718853086701803311153256464974254479872036994904213863555066588420852972140995270767270378954305027680617988398242753207122258828405717215145231149341494245961758579435411748336665164584007718053966918445218645217622824026015878436988274766573974624824341500457088478333270279671366042427648935593088246422898143665395202794477719615587705287848400660946821285940596064881661122629497042407324160*y^19 - 20055457240765630359399672486007290991032462311749969099381165854065434888635677671391355221955074995636206926799469347633824574699206350784526104963568643449858192961015851906612108419764422918507373423764038178762281914260498211149202536820305716343631904370724966807648903780029614890144089304897705493541552229373469203093272236941112227917476687756388146509160309321274923130654802201464802558994337239737340374332309692431006712797916891060491236452283325291040822627745397563269679300206859940821462423491149284732766498481223968105020874302235350917377767266099076834312788540160119/3256332348887398568588542677348423539095320376812412900506857300656934214884362356441309121037679538326288586753077454131854715218985001381422597666625878820995940527471311103000157116151286475514450300551858876077495709079978672832484035643925844431403475495356832545127878396492384171280102998066373792201187043138067619535857538524890249040993626429905901958056110860764001286342327819740869774202937137337669313072831379127762329104137390250076181413055545046611894340404608155932181374403816357277565867132412953269264617547974733443491136880990099344146943520438249507067887360*y^18 - 5360642202257412983756115829026056845127426256497966766331367933118107362091638000392516407905312416126831802714109581652829272830649853235481845904641746143797717784074635580481764042532620376044226881967859191751152405925300626248983261786922019729264622310316549638848535162252907856464095849591844124681243815768230201505225126032885407222601890469916431929245098185981861101608464799303790848370884203156827377168888847269984024130038274056520483726737726745747122042432129328924269325665442820075392237721046134075918155295642309221888330595138590650079842592188042074618353724301769/592060427070436103379735032245167916199149159420438709183064963755806220888065882989328931097759916059325197591468628023973584585270000251167745030295614331090171004994783836909119475663870268275354600100337977468635583469087031424088006480713789896618813726428515008205068799362251667505473272375704325854761280570557749006519552459070954371089750259982891265101111065593454779334968694498339958945988570425030784195060250750502241655297707318195669347828280917565798970982656028351305704437057519505011975842256900594411748645086315171543843069270927153481262458261499910375979520*y^17 + 198365082451120515609353988789198920197581386869555841215368956075163643845991817395884257562367548252514745128254979705435117171711632721983846471136583439494126801706066894633569491502340459464218103810377602447081260847742816486712999289917365332330682762051131803324250583189272006937445218700653888478092221602201485588231317987562557909905746742501266318220582418381968137236201879303807713911563383400862278827060538533449914153425516200979856235761221302682088905512246739101152324201928999062678653703910713480607200508285879637694931914268629323771158185371095770641400014178781/18913837457235616080862784185954057342276788248668419557639054989294874433016625497238968757237248044489575528091446974628391375908915787307391661180789228389134214099542949291385230103492467427963893323631319706161640130183806424970865647496181090598664910912043557861342952932191970017115796697384552520045616901092357906307013776524047913113225322922977165293646336074137471169461729833925671486173884631196530376028062221458445280372530824298603183425298422342373055220162293258076561709993125018069114426712950357807926142582621878665001763103524294351289120157434169450539520*y^16 - 1273766425265490272533383283943256026094915818532240715609661801333578767732131765320307852476999831730955664370081127450079729199001718318588086424020434496700119332118879539362799395641902319342115718009581534735335534104237072963025473318387437670122129335810959870518609624172148181890320120393663221387548353837198793575042500048749587714606020356460798683542675890983350888381837988086946484333108404987752542437012148215802913537154077740569028185341738697345529121146114348308813497142045246758265702922782649606365336136817421118336484642287919657037872271852299843970833498481057/105896986955687758328082688694257676068140500058940256927052269940062901297052434355814930765452993116302067861888697695344868787609268337607238948508158660845396439917766214731712426541505251236242286196808418734227502734308249523007610915249620957118812211231116505532613931593248265732686276359882074543128033923189190879214879301622447123284345574956289494570930434496390285734709847796451049567575191458135587417002646475699587938345931390246379883351399838914207946029418151412428662582237930317969621695363022870545190814568284014422475996129759328264941252697178845758305280*y^15 + 34851045189923762267206672667246316157723411825359793544972962064038796338507385371750392160048763695433526328437016001455415202178288144369667027893610345381553153252653834826682005763605598343130165194665882441343081190756814876728750173194165306486424191623609921949563742119272537059062532749452366021972041273416960110792365665883453614672665118873061008569722918652454292263676419844670773830110328515482527941770239449203197947496025058129122033404590360664276541262309485485480596667425028164112435304227153475077366646866825306722254267398418371452844782969581803616715939250198469/9768997046662195705765628032045270617285961130437238701520571901970802644653087069323927363113038614978865760259232362395564145656955004144267792999877636462987821582413933309000471348453859426543350901655576628232487127239936018497452106931777533294210426486070497635383635189477152513840308994199121376603561129414202858607572615574670747122980879289717705874168332582292003859026983459222609322608811412013007939218494137383286987312412170750228544239166635139835683021213824467796544123211449071832697601397238859807793852643924200330473410642970298032440830561314748521203662080*y^14 + 256018841591337462556896035335211485851510780342215553825799702613744095642384310448745611877351384544484202020552985375582636852424649122677273391509114813659902861624079890262418672564312183766042885059384979267238311674107575540128101275736772287338596492289438472380600442490088989515394301352391682473453443521010858681719848059758211517141598587301604566466811968912870548278188550992025746391671654716796498741377546720925145124832344399197162692980417406185711279059226815444143807024477166987028553572124647549688833624609788057839617136636701026782619009707498140790811837469411/55505665037853384691850159272984492143670233695666128985912340352106833208256176530249587290414992130561737274200183877247523554869062523546976096590213843539703531718260984710229950843487837650814493759406685387684585950226909196008250607566917802808013786852673282019225199940211093828638119285222280548883870053489788969361208043037901972289664086873396056103229162399386385562653315109219371151186428477346636018286898507859585155184160061080844001358901336021793653529624002657934909790974142453594872735211584430726101435476842047332235287744149420638868355462015616597748080*y^13 - 5288325338362890520326887287593928576796960874116453904574470510905448528829627564199575815424633326465236353400748482182126655514878092217932968428886492788034363830465107409545619375875869654506066751469299239264678136725625630687351903199452755706280077354744851595166978618728602889962681508343547958855817612510455607032210435555731237842151596542494753467081419481527224002849817662074966045509807267228677338057906820464778879023229436813293128572051979434985936331613891174807229504590232118553582040509588732025408554442421793516763325058229283808523390326152265016212943738174151/2170888232591599045725695118232282359396880251208275267004571533771289476589574904294206080691786358884192391168718302754569810145990000920948398444417252547330627018314207402000104744100857650342966867034572584051663806053319115221656023762617229620935650330237888363418585597661589447520068665377582528134124695425378413023905025683260166027329084286603934638704073907176000857561551879827246516135291424891779542048554252751841552736091593500050787608703696697741262893603072103954787582935877571518377244754941968846176411698649822295660757920660066229431295680292166338045258240*y^12 + 216894199676839672190310412909987245739222935538797775159257277750595628882506968932613135539748149009110190746509882924514470670362127944452518310532917082884890063742485777800269400150920377752365950833561507587623188107945578588005967139997350904385825010477490405438137295949700435800266723014137454444139383055901949354596102510932617276485867113756396996682290058153970956562886077894937180294536892699265904159338451542759095753415859027468929386262455560410463177279449777374173826597400774159042912987782966454284316739987574203285836732825122405813203028313140793476079122164611/610562315416387231610351752002829413580372570652327418845035743873175165290817941832745460194564913436179110016202022649722759103559687759016737062492352278936738848900870831812529459278366214158959431353473539264530445452496001156090756683236095830888151655379406102211477199342322032115019312137445086037722570588387678662973288473416921695186304955607356617135520786393250241189186466201413082663050713250812996201155883586455436707025760671889284014947914696239730188825864029237284007700715566989543600087327428737987115790245262520654588165185643627027551910082171782575228880*y^11 + 1498605470878224071098450118289010493022587695037097698394509346881380002254057323002173674179497246361443892156358791835936476738232955074375759496531451807591319444064751073383775461570129548013759254506047223112555762191500252418949734509194029050323897824181032866418739163282050085567369866822373666053422569623354593825740374453773768282588903404770951716516803596670768055672392593738664167847383220518795357221960275259207739034730843441986463188026193316516959024668964500746858710462766152348060466016636562224259394689413626115507215556239611130212906337320609938643195745808429/6512664697774797137177085354696847078190640753624825801013714601313868429768724712882618242075359076652577173506154908263709430437970002762845195333251757641991881054942622206000314232302572951028900601103717752154991418159957345664968071287851688862806950990713665090255756792984768342560205996132747584402374086276135239071715077049780498081987252859811803916112221721528002572684655639481739548405874274675338626145662758255524658208274780500152362826111090093223788680809216311864362748807632714555131734264825906538529235095949466886982273761980198688293887040876499014135774720*y^10 - 5051478304757564725047712894724878295193373579695069511390872732390257793038572932704775738195348172479306260941244010264195921485342169177788379606127497922675234847254108756298580113576710701681745513553749460773757896819110263658122813617929825774817390669551913775382189391471055091362033954871845676348392134566169839724802329769347229936523150692739768898676716388821922965894468096587778655644218191111758322672723898151172761759514028571012053302496271064341334420159776868559072530677070984142332194994999229468799871157989747334856306147217262533705645208690245263447423994335753/19537994093324391411531256064090541234571922260874477403041143803941605289306174138647854726226077229957731520518464724791128291313910008288535585999755272925975643164827866618000942696907718853086701803311153256464974254479872036994904213863555066588420852972140995270767270378954305027680617988398242753207122258828405717215145231149341494245961758579435411748336665164584007718053966918445218645217622824026015878436988274766573974624824341500457088478333270279671366042427648935593088246422898143665395202794477719615587705287848400660946821285940596064881661122629497042407324160*y^9 + 287644137393261287576153549661243334049136059229056630412568704464115098453501509977442887575829816468664144865798206883480428256489005340470578627717380702279398570571959803444362831371212719682748684875547808995460807333703887767456172280919299569407406540557269324840397593607399516397267558344178224663855836941008711632463603164261592528364304814223602104575540127896939976292996658635061002805157474379768875704322375771491191757731993263583446244530823450062813800162859906077022847982727848084216774129248044208800001283162322413889298921116905085813363750399208730494458541207/12540432665805129275694002608530514271227164480663977793993031966586396206229893542135978643277328132193665931013135253396102882743202829453488822849650367731691683674472314902439629458862463962186586523306260113263783218536503232987743397858507744921964603961579586181493755057095189363081269568933403564317793490903983130433340969928974001441567239139560598041294393558783060152794587239053413764581272672673951141487155503701266992698860296213387091449507875660893046240325833719892867937370281221864823621819305339932983122777823106971082683752208341505058832556244863313483520*y^8 + 5192044785943601813070538090817271418509761523790288536410200616858248331998585865858104212466196723369977381572322250095557536591191063016283803612380777352161715396933261044506436013582082239473726702541875858689962544539189662883769153314291745245418621119609507373556057041098467756345159221303490800338004226880137230371828297901169955950585417462627962347119302943018506774368556370766509276299914395052452029002400706679114638072529121156449515061743296353206179017162950084972114823051698191766748395856884382080842909471668817876765174895997699322361837724659356984102576989291/271361029073949880715711889779035294924610031401034408375571441721411184573696863036775760086473294860524048896089787844321226268248750115118549805552156568416328377289275925250013093012607206292870858379321573006457975756664889402707002970327153702616956291279736045427323199707698680940008583172197816016765586928172301627988128210407520753416135535825491829838009238397000107195193984978405814516911428111472442756069281593980194092011449187506348451087962087217657861700384012994348447866984696439797155594367746105772051462331227786957594740082508278678911960036520792255657280*y^7 - 34663090231389569356125099332313091190268415308050769527449947176648372444391116846296830761934818817565852835600882243168618442553068101146824724941949119111804058618115424554948195755941203240620482304070884501802253354117244943027367396198262696931542773507643721090115593165786121249263270819836506204239211551880677844824286042447126083815917368051248967322220377822659889386128349395605513156515423967650350703981713788397374839326090718736638406309760468866256234681739681725946514426880254984492042461398407016132251434507534003216847024120894095802391091520831290993157084333611/13025329395549594274354170709393694156381281507249651602027429202627736859537449425765236484150718153305154347012309816527418860875940005525690390666503515283983762109885244412000628464605145902057801202207435504309982836319914691329936142575703377725613901981427330180511513585969536685120411992265495168804748172552270478143430154099560996163974505719623607832224443443056005145369311278963479096811748549350677252291325516511049316416549561000304725652222180186447577361618432623728725497615265429110263468529651813077058470191898933773964547523960397376587774081752998028271549440*y^6 + 14483361049935470763983648264499116566206776616694828979337318754884856199603902713644235219577054412332481343545362720800879845397302754911979968723689572476536007551131356019921669353519713372201788584048189056638687185800837689731315286648600721751066964648475157151300625425792541564758388227398362904978189053884910239118126772054446478844814862301607852456737316095195513041285219600603612785581722809157506472358644526007099955538960206493144550011119173017325255253470401201936280200730863024772672474979544790947889905070823583524071205922352139508910315194578563147651717004573/9768997046662195705765628032045270617285961130437238701520571901970802644653087069323927363113038614978865760259232362395564145656955004144267792999877636462987821582413933309000471348453859426543350901655576628232487127239936018497452106931777533294210426486070497635383635189477152513840308994199121376603561129414202858607572615574670747122980879289717705874168332582292003859026983459222609322608811412013007939218494137383286987312412170750228544239166635139835683021213824467796544123211449071832697601397238859807793852643924200330473410642970298032440830561314748521203662080*y^5 - 2902436070459642555691959845643941371719772913341180682600900004573764890165978120519585230701118578669719353996538306223354170058069688276907215157185393907341660396563933407981219679976317624363075459473920655242898292281280189858280694045949642561180591289154068680128764279669800604957202276700694589672415726451991656231799089340728071956413320728473194802258290450029048087923440791891552829181657113132696933118457606042284458549329012666975575859395446382213367718160146463644597691458892777632776194309617975692550238849403715548590876820035856506744968522999920412166968924197/19537994093324391411531256064090541234571922260874477403041143803941605289306174138647854726226077229957731520518464724791128291313910008288535585999755272925975643164827866618000942696907718853086701803311153256464974254479872036994904213863555066588420852972140995270767270378954305027680617988398242753207122258828405717215145231149341494245961758579435411748336665164584007718053966918445218645217622824026015878436988274766573974624824341500457088478333270279671366042427648935593088246422898143665395202794477719615587705287848400660946821285940596064881661122629497042407324160*y^4 - 7036677988370350368515457712162784973827418753873174448336724543389297470777878913120925581677265995778839616867331584644096039285044516018367478715518886701840565171029785951760837474188458065880272014627132007920816175906204086377407375189480825628567182693915530120581667600441530466040624380678184808801307544252275904991359319871659076403440210552886503905907368178106628592677903816871601352306260421424728102214081039064494040421839608868351812617522657230713161644939293049283769505372970529443783636421501490295494255942027459377700723743084902162108510207503175867017595073287/39075988186648782823062512128181082469143844521748954806082287607883210578612348277295709452452154459915463041036929449582256582627820016577071171999510545851951286329655733236001885393815437706173403606622306512929948508959744073989808427727110133176841705944281990541534540757908610055361235976796485506414244517656811434430290462298682988491923517158870823496673330329168015436107933836890437290435245648052031756873976549533147949249648683000914176956666540559342732084855297871186176492845796287330790405588955439231175410575696801321893642571881192129763322245258994084814648320*y^3 + 245138110059021563710947928826870033750620390640383805476432202213512128010513721513070172746979161867193152142750808419785010277381826744195513200016503013345897884598130373201956223530720699970923967032577230591452636631212981928170847243304313924080247735793832991038948439899691099719200355456186073823269902986976752154593094619492756396862260902182027224847262896184478250711419361706308115528646195641955260954299860993455231099986264647496322599033656498022319916092704268220039973551104349625429432715489305553961131966487870619606120846845588646498240669830799458844180852577/13025329395549594274354170709393694156381281507249651602027429202627736859537449425765236484150718153305154347012309816527418860875940005525690390666503515283983762109885244412000628464605145902057801202207435504309982836319914691329936142575703377725613901981427330180511513585969536685120411992265495168804748172552270478143430154099560996163974505719623607832224443443056005145369311278963479096811748549350677252291325516511049316416549561000304725652222180186447577361618432623728725497615265429110263468529651813077058470191898933773964547523960397376587774081752998028271549440*y^2 + 111865161842726738808938425858684272355643047499978473632685806662405372392291489400657577697751444380924376775326734777175528238026226548157101896518435777529759360428780517723686075792121241147115027100683832445917239255578019726403692019522169732529845092693007812277940028113028141201559939697761259623257127327489434344752345746563739153331292512647640817696358300911108873499571535400655189654565219747256141301938596511434879998638662482297597985911043618711933118665022400017172774108402753856315312409737527836595840539690334579036160317480712875583029479376664316488020587/33920128634243735089463986222379411865576253925129301046946430215176398071712107879596970010809161857565506112011223480540153283531093764389818725694019571052041047161159490656251636626575900786608857297415196625807246969583111175338375371290894212827119536409967005678415399963462335117501072896524727002095698366021537703498516026300940094177016941978186478729751154799625013399399248122300726814613928513934055344508660199247524261501431148438293556385995260902207232712548001624293555983373087054974644449295968263221506432791403473369699342510313534834863995004565099031957160*y - 1242933704282471928021638559634834190345857771840039579251484147367860243571306132724525038177532858453593767744569292969259815547259180691434007180129961283543662487075206069508440147977210376468749789565306873499823004533483317539858899309994729439792338531257816847011834967248313703475887666530921533733785161343121257126935757055874220876951729214304841328423872795594279844901515642062210985770419685757975687959000801234218471541369449652673230104659394445226252922958113123724002222512954252982334895524050270779882171442868752076952944224662715374191279320027042207884451301/4884498523331097852882814016022635308642980565218619350760285950985401322326543534661963681556519307489432880129616181197782072828477502072133896499938818231493910791206966654500235674226929713271675450827788314116243563619968009248726053465888766647105213243035248817691817594738576256920154497099560688301780564707101429303786307787335373561490439644858852937084166291146001929513491729611304661304405706006503969609247068691643493656206085375114272119583317569917841510606912233898272061605724535916348800698619429903896926321962100165236705321485149016220415280657374260601831040