# Manifold: Census Knot K7_73 # Number of Tetrahedra: 7 # Number Field x^36 + 6*x^35 + 2*x^34 + 57*x^33 - 1176*x^32 - 6093*x^31 + 24137*x^30 + 111979*x^29 - 254728*x^28 - 951210*x^27 + 1588557*x^26 + 4806199*x^25 - 6604530*x^24 - 16592890*x^23 + 21963510*x^22 + 39124832*x^21 - 60024886*x^20 - 56509703*x^19 + 117902234*x^18 + 39002511*x^17 - 151632149*x^16 + 7282969*x^15 + 123130133*x^14 - 36576059*x^13 - 61372738*x^12 + 30742494*x^11 + 17637815*x^10 - 13332814*x^9 - 2346697*x^8 + 3342883*x^7 - 73120*x^6 - 484475*x^5 + 65158*x^4 + 37524*x^3 - 7568*x^2 - 1200*x + 288 # Approximate Field Generator 0.359451622819046 - 0.330196418808731*I # Shape Parameters 26997894873789352966226459375186651073936719247535768899892879949334719410543807736759382092037482786779401158584028582967530011/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^35 + 29184244174207477706121980080352013975258469291636034226955216447992546881950684465138996114904986432043102087537325158571489355/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^34 + 17353137814181943012376318346018708050808315579209812487057965699114879896264853855723254654977283381221889941114984972141439380/7780918586334789555096342022607801618773729545161547734479275559799322196598700354770679485938348109127690168003805723045387047*y^33 + 535021597253192281469844202690556634502234766837964748286341273398901228516746906862034147651509703242926699003743546939293882093/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^32 - 2580730593116675812585535637911334110869170201082455801769138211718053500893502851204113696661912289858927059281116006908636540969/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^31 - 59853426193737909307423171617856886442715312068999258153786638871279593227347565876002741937941282439080353668354793005075365283703/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^30 + 564713492298806238167872298859808611524386463143222872423192606378637191106130307312560241755508176651822703851433771759181109771963/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^29 + 3298829361265674208539023798803220615478285777208635766496191318115324410209560829466353430086879949184623939433489077557017157824503/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^28 - 2640860846598046830133507887749229852665510672266872465334432134941339898584954343986335860802154515980663282409368665658103521036755/31123674345339158220385368090431206475094918180646190937917102239197288786394801419082717943753392436510760672015222892181548188*y^27 - 1177862474835320920941770315041155625218947318019590713938305104976955367406073288847122559950496185621810708729342746677795428231311/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^26 + 9746990375866001309665854052658711707579872170654631665530395346812862775937801308850148384238314005714833719145504519486975547595709/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^25 + 144131123354915332692696605103297425783110808910441948626310931760673370944447561684144370562966656291965088177047492324586731839507209/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^24 - 9072757906156856852008179453429745369186874444974868191952850871208375894649236224773437391066949125694867094206717008103631424413419/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^23 - 62700722502138891099875500898834514879933578982172936138514676383511479097885437193624195006322997196362723202197056761778489552481702/7780918586334789555096342022607801618773729545161547734479275559799322196598700354770679485938348109127690168003805723045387047*y^22 + 58637835954616562990950964296228357778479212573974037351289788379079676274160062767588860170514154882907611752351254115980617095455757/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^21 + 307348217744355418392911078557519672869767113918361001408639138327232028488446858306366817432549752308085611819527248378196303630569095/15561837172669579110192684045215603237547459090323095468958551119598644393197400709541358971876696218255380336007611446090774094*y^20 - 515824450906861857978963123352606640092305447662670435728547170109107325344363876065253342665622869774875600112385845054047202961397587/31123674345339158220385368090431206475094918180646190937917102239197288786394801419082717943753392436510760672015222892181548188*y^19 - 2030134270117005195420911568033855259387764036961623314849933835248674541020731871009049812394388690187555535468526746755602077237305517/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^18 + 1108768136455476556769382319325065749338142120853360166431618610000881330077803268128590494695150869940890219658145223771057939377447433/31123674345339158220385368090431206475094918180646190937917102239197288786394801419082717943753392436510760672015222892181548188*y^17 + 709266678765657999090368302088792280354842226290593245372195582384840276195163925279637829772230862193133918759237321765833721566730621/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^16 - 3093511617020742835536539018881387062680836402088735210293641100176242217864788283113413155932520047285850695743289311615545529903216475/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^15 - 1287394918214572782268994006092340397335852416761531832085573984300344353158578714420228935797355547622377020336986416634963790859834079/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^14 + 2729701002897277860454613641056877299945805532526550006552945595701742066255804007982813289549286039293648463158708147323754140448996885/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^13 + 307559057902178550579654803664174664996580131712307126103190124550679425739419703700214167348081085120211392729570515445685460459918601/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^12 - 380040765532075091806786573047019030105065826934940376470743607044242476808917956044268098630537577066269957275384607546011172489297231/15561837172669579110192684045215603237547459090323095468958551119598644393197400709541358971876696218255380336007611446090774094*y^11 + 9684162702409314214079519462546367319319600833044908428309337562314566646868329063952433086684913903045106892811751104689133069754545/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^10 + 531187487058353172032918525817091242765496332700735452223769089073618056752920592026892483372988180676921933515986084102055955205916145/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^9 - 55986918703648877992105313506843639156835582933033484503958959569592979332337421466894120034256787530585738914557275462246693816798091/31123674345339158220385368090431206475094918180646190937917102239197288786394801419082717943753392436510760672015222892181548188*y^8 - 114438159710261687979349494466084243728302189256588937486108229294322235034164782942972458359702329336254629697115842218573237746046981/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^7 + 36522924884382273833063598377297660840865625437269358302526564217663517703128342633784460611309761585760169377467579768465735368359181/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^6 + 7313473901238195683388268391396451079433424763958735036277621682598998023670447346347635101928826967711709415653034959570541625310967/31123674345339158220385368090431206475094918180646190937917102239197288786394801419082717943753392436510760672015222892181548188*y^5 - 6048570162975406940288308920537650143447697541355065887856366425807059877383785053235565245544672110661630786602677771506432111910339/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^4 - 510521335511627590694117562547366674532909074862654874555536601577190021690401559239145213507586208937487715141161793203090693632363/31123674345339158220385368090431206475094918180646190937917102239197288786394801419082717943753392436510760672015222892181548188*y^3 + 83391271627810307501200505138928089907866913908159473243956511775710100617231178549004138368694867240424609424825166617125835903717/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^2 + 7707110684699508600285148990772127316537635760952579687827935919021255515607002981696173552522509498213976534379935180113102455865/15561837172669579110192684045215603237547459090323095468958551119598644393197400709541358971876696218255380336007611446090774094*y - 661724116128051472867389239722657856677112123494195715825365734807994610338330493261547828032552940809305253955011778725176095290/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349 30087176708140879967133691093789850525295402123293121720109725573241103589746078036011336263335400767471942678415893570911015705/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^35 + 84977221289172113825939310845110929483298304986736266651905062219830582281729392522795750832274557903438845926005452862796884485/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^34 + 3192915540541124995755491311192184678512121075011534110699916975750764218866367570394587085937891558317026929899338891622841075/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^33 + 1749367634174300371157041917265604446184012133175613942552924144130179864140154971868656596256245471049087251905872820500266443809/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^32 - 8993848380639701723645815195081712266643630579618874229363272520349111177655933693722691889338517869098310328035140931793750760807/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^31 - 170327298128114041375439392442447025781135575351469376598831271581605909262967562875064156462850790642372982064016326688959726482489/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^30 + 779174862871196689008492310675438971315236972885571538743721886833907490154415141325038351686621252195944666762423181661786952232317/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^29 + 3058204162630310869702502804122003505839921804909774807546509886517311257977948048553160689144738255193547108851476410765814723123467/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^28 - 537870784489348747419366536636590434578027238496397752430924945628850523423558421503990031002741073889042735514850728308048952196338/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^27 - 12461989026859062699197506559532526994350064488504728575900976812200750696905626841902917989432493624486830796366023055370871312422371/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^26 + 55233132169214313268997440491313877688984415376695010756696873634109289805030243538706406485220479441314713690735584196443062888961501/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^25 + 119606746804059210719239147626921361540510204675640402077746819399575785084928722640307558513088597668381675704174184975199816102962747/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^24 - 116492474644087764320497421779641571907281256451139262221443765181216607206209872165679384051137659061961285636126642210680100889408813/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^23 - 194920196263932957657604643971151055590217414074248649941061747767020479927284188444093976277347257123371751229615236196769831693302519/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^22 + 383646354829848900138053464075141095782900702316664236446610808188089949328637735747128999274560657798051218149450929439450810994549955/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^21 + 50954961417353841976410965446199609165342971803383064742609787230857005785852532252417120523514650086678914802655415405965558948062201/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^20 - 996445500128795741268658315406225626057459616202733142972868749664635324950547393941179666646018469928909125166292531273449404737227455/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^19 - 788599618577312658202078765276304282634678617522101302926957488718987898096864284300540374097911336679457206834097517392459659770358071/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^18 + 1775346801913473246767364663052608456761936444187072348470470266392848486246871039347547012176559446384561150834809636449102618143150995/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^17 - 371479870619656019019844763302981169307340896873675501893083385096078103165978830153327086995057125668575722600638575760319999723912917/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^16 - 3902616209093088211177937007090874029795619298151475739556834663195414455590913222989207922548137306681773429264693700710965321365419129/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^15 + 1795741413636361147531300099921354851896150312904997139121355129584636689012700464795609714199655836208954430616138159704414506582490721/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^14 + 2430812730755703677341725493548106766363155966204067934250662502633269227598914045016436509132398352093027628114835699662209677294534805/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^13 - 1942861448080252017513374542802237687233970690146385072488405827964382688401087744468789540915370304540767310663224811943799639880701651/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^12 - 347080232525777314664455266065970922329419918990012033999507002456629870803764325667403848451108671155024682389579244760891017513012345/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^11 + 519163029883266817822479468880756096733643167259858006993547156534199683613415986821567757250386515160372027769524438599523595171249121/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^10 - 31186913957797342646541286007571511432113795177466513412159939517005160840588088585792963409805697748899719132939224419457607004564497/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^9 - 146396164520478336515238266548017059200465710135270331233175387563118278086149668669950673637299008916904799585379159764836611089812477/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^8 + 74533844325932507066261300892309281649022499461105493432306420420960075290837635346247177846648113502056255300813112225349544485534539/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^7 + 40389915191018912924157633074074172798020708236052936476057395978855660075132234005777039942709786813025844333179754391005187575601231/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^6 - 1189613770089265888688428125758298925355300979537836889355462091217632936319568794135161904036613871729466569916378829794063287850617/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^5 - 1686754411602387610636913322001958146903443516417057669321453023131609868567084762639715916724909145922518543061833053160615971803327/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^4 + 1002792446911581484537101766321488667266343745154977789004397860763375245369891372756256377584501136626275611812931415958456766723493/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^3 - 17819580622995964773456061408050269095609004476720512564941658406953333588413509015640422653613263521592194655587012390190334138265/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^2 - 9698340739631303592992391128294656026238588234411664190326840440112002799613598619452531433354702090902228194219069415411482490359/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y + 728607574794546182683846522594492587754614451784566747007816381279616825331445534444514426268199764721203979140291329151405835949/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349 54642564390160126969497252438137700340876829092040381797692173546757263623512574617536860420743280138557916572552935176880355343/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^35 + 175298534886842601799983855760476501247923560197717222181842109274618483728862996470109249083345843010645490686530974320836977459/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^34 + 128200671853401959885977275743640898253722132993543683954837009143339308564166453136297662352958375685203216397612247632107780019/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^33 + 3228761935700897929911487115866832423092154053933992061863328956715039844180662932003193055258115570741719977408692075056931404943/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^32 - 15727975718615434840815381072470822216496484999419156929698100107522734339900374508821980394088897150023968512277902765819321743523/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^31 - 359049779982816172145640603517159620926694487526424108584779422039863781235577867499461323655757082300368379640769576172837343402771/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^30 + 1168075716458793917597318916916898661369218192317589068881363244303879936140526965751802586304537793985340647634772903336282504792395/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^29 + 6597403435132722836202992751267834513328527373906210081705710670879719836669608290783625978746909807244692260858978193793391318681969/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^28 - 2786464147045584113613264033633341782434721246379275553636297705846207925820438016566362784200490393064137657920010325648998056187345/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^27 - 28238702026105012162227045206551900508735190645173529221799541265590666806217387877314067701712579485507522675989416995983473723800995/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^26 + 63021505431024075697303780291447951926429171042009462211619220876733267010483762565689801303892238033464619902357541874159771406594235/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^25 + 287687050796239925043232933574421901684208494626047319454073635304463245812255888940596730338487067912632248173239972851239089320411365/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^24 - 119753968063852850724114571497246778584817775468164423386894313973554054267067032847224690200000433280609431464804833741580892051970445/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^23 - 500260665146327939753862241359097566493500496795158078080737769630092754676635405428226977234474749030142970854789901511590329276555263/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^22 + 388572997956676031596487971554669989737436653469018741724264099597234152796305787001247263209102502649630356733650200068885522422867777/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^21 + 305171686808952522929432821877241466195515780937764141313307888177050946191666990082802324095673640391275799373915777805291775888755603/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^20 - 1121096508400600003581779519917192042397580202354254029222962535152116016164762629963851784916957127597733869118408966115033324610356629/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^19 - 3974131814617951914940901541578000924101178245245820276741878597649929053496018796036948407856179401706923905827892573283220612478066353/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^18 + 2364291827624891294753272899118959611708992801167288282042548378236088531778519915361184495286647526445093639879781335896778485417749433/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^17 + 4030072282871631415932717477803360935988697732512240933413691370312163990903543374775138437804923120843832543409229881598303860965911241/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^16 - 6489744623971940215010967278588749300750920699277250280661001015999915865973353860189061043988976699675225972164397680571985714149733447/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^15 - 2249459402409086457042012491688200951365194147081391115818219038028396138589297670794218525155170909025710573772887757522004050581801365/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^14 + 5641102825101717213130395215444812513831153190131690007265412655915603356430644535125422781267401351783869984744054007327156905035157111/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^13 + 343463813218305360727247644536524926232156304884214813114404321954557101745828216086236372171664915580954031461379171384825261805971671/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^12 - 1546071448777429974614286060659230558085444845930431276220735578571001886292477756092459858550224346740466575585461640964798573892527857/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^11 + 183280683443909956357544258933726679395685774252786214855735922437488896156176566881787745031573711992351117078492266760035391327377837/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^10 + 1060937392528655030283785461747141590422773659357313060564477247429639845036316273317501727484117992847736108795153304539864588304791777/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^9 - 131699737856332330769444114029722614406488957310680445054299567146619618279557439291002361919831630667637041081102222934708639836842439/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^8 - 223674465355544906007414173218255860960539564139722740706425793516395436511895861651464596046391483159066122896096432244746072010988207/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^7 + 80072864866802288720974478987293764589625613669141655938600287659181282350980128456821146055304934080858078766638107800486705757477265/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^6 + 6967517142859796135827082561585386288769867321932471552618504489836795752235070935459698028076579803847493646718108998058704070828485/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^5 - 12872193243258762210412942511900122958690289167916977031402361627326008271222333709241910625450233583039502365864704366105939980922389/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^4 - 947078344687418661931986369862901641664422395574504539583207018527717513263060732330213096928840346296210589259434995976239709069813/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^3 + 262927680615369871545846653181497565719201246552528343507850073060523984523077688990162273020665259025179888766009809150081838695801/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^2 + 3522632176663416995273454433617569012157306755447119845296277769210029526577885497000121959886255767116208691439422011630133556570/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y - 2090585231010813634304363421994544575576176865807938882837728028202753942668444609848709540161899801151850020836815271254757836531/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349 4262118883250868441539618420954354609956334994607234532321273469301442829981853433225865842154310987287929034155248064673122517/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^35 + 13868011464976054419633885951364950468829684431919277299698287999836830878857136258700947576404910275164172074902420166225757159/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^34 + 11302134222244031526180197546941586840625101226445923298596327392643438522914469694949135372747446064503486429228840053140281145/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^33 + 254422830222794409654889194871803595560229640012110560731698685035183298447468138437273586637702726915504059305994102225365977293/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^32 - 1220785087197465709129790405932717674648650908269885111997536849271266859476119017193053847725689408669622338037772603861116101574/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^31 - 28447528902810317221066731984095692359793428048528745878597534900814962776550366842103359058199308793195309172318829337108770509149/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^30 + 88432964829964680450431705640320938144333890840804760830594521622563581125747954485237917334367863341203998051116548360079993926833/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^29 + 522144737514405763176039262432069734125516571831610534840370489953840252542424458560653610438438855622456893107258797809138640358403/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^28 - 205143817262392983873058443117226115443782645822450128398853535347661153390578266314224802516477204371185512483337050593027080420574/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^27 - 2235244447084296973474338181482070499141274727469296706876335494249060381326149769088015359037102986180783001018307872331903931202605/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^26 + 4500436680531915093978241635800494637065473474528168801722878687732129581879299896457377298691368192610711601932183283732728489037297/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^25 + 22767228251394750302705468545944799005808400442511655194377207890870350488193206155009926430859847339824550798035738407509059083135679/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^24 - 8292543445536704955526251641424183429395260184111246526446282618372182723663566296504950699138804223540717745704132401767406495175829/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^23 - 39564936426979741710739245337390661118957827600368693058452687104739517479737291048142627145887514150981187158838602472824863009200167/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^22 + 26703930708115511797778309720096075562338933802653072896289431134669639791114166835618844051001608992363952304034897555022618791654393/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^21 + 48457175313595820770413428723619273059959332059573071669874107312512848900052850430034759028667997279893176118173513836804144603893013/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^20 - 78657994047587643107034053498572920746937620109515562253337364986187990901344733717006298197176256494783811815444816054848913050985289/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^19 - 320620546505909496646922947355517790940785134974307896790941102835562515494457253571703536378177342812526583748305859363784907434420015/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^18 + 169710052010828408714204586793388277692554183188775740886903389782998773603700364356061875599598000100195729390874372777213268999327629/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^17 + 338440903649625476841266772512532695243707218449536915234885467722663365759055570334859754595790013293042357254765475808232281772910427/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^16 - 473817488745463462550732199289440740940734909062295711104581959369688582421374232793876382785776433769769001342941783014345019823766269/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^15 - 209565836987275249878974212806388727796085420769029514281896558415368875360981861379629696838932332065149760541454985227006954223968883/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^14 + 417570609106472116184962642653041855026121255229190536417595849201835411907379723863801477843708358289226836648780285624741912988390229/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^13 + 56446632375792067750942505540719876296091558380005257442920984536310884398247581667127665358962206282246041015646846878786292080279253/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^12 - 116126300750261597292642115928177966304414591153221019684533003944158489758650105794985060665832731602991394320575442030427819346220753/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^11 + 6332372705552620828544922288613238700564744929961102909266141111295852870520653558917526984953013255201373030855726629044930751384783/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^10 + 81308532607333306814397943163332500396682868733259209687028820983420871006184365264273456268612329924925471739189483985814910635450023/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^9 - 7625172524597371801779704976998427358862738238856135020786506254102075258393664453680852388004248290081007048924275190592891870535649/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^8 - 17695261121718242618349342691244330714305555158823482168454292503071314605964172490268990461938326340727350359737344162191968857422589/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^7 + 5160841245044699821905131939076458769676819125463413358582159977643073154371666474274973382652828311693589793419521734433356392244675/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^6 + 579309944575535112601531980460304661327106724543575903365526371580126800639445753702455509238113150365809083022020649499349745563774/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^5 - 870363205371835388444203267403451043849047541313968639335073594563588222726747996115338713554930427706984812528053767273425705662727/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^4 - 84110393579842287986664835525131770155299068338466860032371565227262744035873327075345145425870552733561671883962009409949051247755/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^3 + 18257490504046759792478375037191655888060903983034808326522065975561443958293974720689143662386281016479740265810153058096382731395/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^2 + 1314684504646108455728089446535833468437667809459445930101712472783317647574885921707522952719382482407105983792469072402489940936/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y - 597261880862229259806913524691515658794357972984235880141450614433845559985412382431914640678603259988639479345661049068303948974/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349 3833747729900707478705347372786867808698861853715251332161433910704973167085329154570386825018272873198278499249793726805010499/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^35 + 12963935297955670802897461663591858740720687451449930056470843419225780031044079209521277062889784740644789442099326317940274973/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^34 + 13023330003235968334234893705685345548410106015932746449815119958661978812348424954539355531498665434349078077194770120746587119/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^33 + 229950457111926588212271829989989575433707719593860742780254018992285329792717039261143154456869550836144581900413855747299214539/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^32 - 542028050724687959968095129077025837234774912322794407334648760838881635937401212034804168723524181710990178293067572851491522279/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^31 - 26749748799597315072083231643410199886809394805257589212400206810146388684785262290205876145889738816782062233475770219248195129247/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^30 + 73774631479355405746447917912235292763643198782492811396878046635666627811528862334670991315936287189388566569873322057014118355411/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^29 + 494158416574708388233560424243995312313942796967608567874547642291914528397215778350399008723065064357959436194550345462509677900025/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^28 - 79120701867256596589329554789273288887386398358292532386578142881965692774752678146808832011545408153876939215287963202297481666579/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^27 - 2142823624803653200049944688615463677799759099385242506378215108016699767614604717330880804190741947350567394923264997635918031919391/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^26 + 3169040349843226192371186195711731673231219484110450370634703690449880021368987894790671335447542545865413747415490205815449465552559/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^25 + 22151969482614017430604245303900534248409576061574879375693509162976228285675046112036527616844436562515196009713432421142737144681173/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^24 - 5280119426388430282010353040968876494961848803283734476761674535322747283477140906242471926102211250171868965253774298241165498981979/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^23 - 39087748560738139327502450840064791813837131174474277385365175706985462661306957370315497978672613209802888280935140219638617400827275/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^22 + 16650436646014147477320710745680513610067888382073952167024789535365200301322331557106343195281381334098374448886496251418093721380733/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^21 + 24682517152256668975900057506309412733733474684177083784248259737245194365720750432642922598108249423368353024055851847908284982496647/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^20 - 54096319994690491332773670449780939039713768992951317354727779049906689300757322459276072647713488157774996237487330465342392230177201/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^19 - 349892049260683497008350658293437979600847534889204178226483401389602420393202580821502386558302599836656265374246756515396337513644885/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^18 + 131327919441087431898778451655775761868907636961116573293797719927746184564784614652440256035642410480303366001401181599903625235211811/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^17 + 419651931287821446807369870839925828374012306102992586718812696265026907392591201632898921297525430853913938111801725825820759235988821/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^16 - 409443572606697750974116429408404719333304785892415079440964475830517079328798264913251320524177493754444911606492967943112648866191351/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^15 - 326560269361029519228982969205726393631138865895724668097483152273076609132744805247824968281612835880363888122938495651327723620679213/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^14 + 403933816984996021980752983175426310716024935056680398175982275508971655588501301906218827505332088485243204221225392407959043804432943/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^13 + 151444187534263512117906680979747149880878758804747019949600946387461399788601668818531894310399342639592442948369758442574762419529847/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^12 - 127291044415014409660026111550000766908968223194407441572875117383283998710682936477881701443842777188989898895774287138523613094678247/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^11 - 15314708943579456581403368403617079435172233455712213204344915659262278576796141637371727807324647514825781548951926239860037765296331/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^10 + 102594524100766948963662438694232314958712703066620730147292703952668047593081719481712300426969596123113687903750746123504339154157981/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^9 - 2632241315884552391520744322051507148837970839770696452216215362139280069194778844944405333537694610875633382750931702634286955382037/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^8 - 26005215208344149106713814502372424803420831130037879401245139985401644351901005535525054236952548754483321010939934614879407992184003/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^7 + 4533621320264387818811312117929851804362088079077672533770094830888696441030596965524449577455521600115435487584350384677370408409089/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^6 + 497056679143081055622274644549231450607175044827905167561084132352305125168280913841251602983216214670648652112954112501447351114859/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^5 - 1039590442773231518390270373862653576973645590013545392571503934854518220327094165164592474571249831386776481127594215978632667549177/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^4 - 167375472100945888180803963172761234318944903573190709563634689971388469531578880208335526616534138844333724061857047206984868538943/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^3 + 26314790728366709641136083581735566600083619779878649532397196041342917161267991701369735172687867236139697386971102620538653977803/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^2 + 757549185263144454947143837776674203326704246373821239789593762223208286323373211323172514708384541242985228394882215130478466899/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y - 492563202896772550982763698553758169319121222528394398541607456799360541184343448590365004029991657183147056354400296434891371895/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698 -412212950985998928435745395018601839951114158387799211315025655843957377631547445623938703997666624559161726983270250219071699/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^35 - 1559163340730715090686968450235482017488378550521489611286273843481175164908911624158127256680654827445580604461042377365993035/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^34 - 2392818548323558604571894863688991708107875558346549393432270921918960079577309060262146357469764763370653909126753421188940049/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^33 - 25463520548285499053831038585893816586643343096410106380201532371933103586752453809109167772834350018746275236528477903898417175/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^32 + 111754600645790335484578629864716734560853628736434511375826695746594878695812615075314000632866186992932875472774286974306740831/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^31 + 3264706475999256984555612818619810490101554884157818108175330988162387344545151882376365475786172680442423204002661493330198662303/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^30 - 5919990401301026508381975729726224568021630692980372584867810169516529097659377504219800596996914310869589502465936002806850227407/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^29 - 61019995141784853987502455998015829371911638434547984478892511655294033805308697829966915330435505997162003154003720227283372623721/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^28 + 7845547018322903037080199595739165985283452695835885839359908202217130574515970560484901695156813302743018793969002144297792841163/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^27 + 271547049103894440933523844197611657390251284246938707193661054794259162278921482036050755912776457546464052097888011127812264732559/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^26 - 32844095080286575088878862889915890205334306008879470131863381944330101585480732605860755005168383676200057681163061783880910299423/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^25 - 2886697692735868112629812447168560752842518807897429858929971252719959664438540550758632550540977810132359094416343674067521327170213/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^24 - 198771293123406269773552488253640778911639547197005307600387432082471902633285201247413843708243747746954620861373488920230040825043/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^23 + 5231262032612962453633034096471668302669492175657445912975850863789311242966130791785171230692672058314354306246905406423562812626325/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^22 + 812318034507438249535372072712156111034977298242056230906953111000809799167066934011313483432586846625647664156831151748182967937167/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^21 - 6992255519729465045111008039761380262373472740001401443940939879402652143725991423041401392179916546265831774854231799734765301815439/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^20 - 174584788510976012828120163405795253989332515710045263798716850951741038030446787107808321325369074203495958851265185778279654160595/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^19 + 55773569548450816006653797361209714586934633862976837605710566736481918642755408267463177181353600373497909494650503047295102324796845/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^18 - 5847013078509770009277801139272899635863288435506983325469345593209226076015620651764547599041572031507318811788000416215729930777863/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^17 - 79725259474863797640867681327449069516077849144990003633277248619162085918777061070970621680661918410964583705713885205302891610699885/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^16 + 33774974723280356580609233609265155453707713558238400804870805467582550154882701300925210111901710091493865629363985616048031443119395/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^15 + 77226599280223767955664341399472930408990660013640566480756344909420998100540642632226672001746940195931318717521569196275289300842205/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^14 - 46659610293577207286340101376262592500538245325529185852726998108202535764729994542745299708700736802591948623298625036607292878233767/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^13 - 47527441547686950027490147038838806785439031972869455477137404459792706291618470545238997130863024464967545212235032649875407170879955/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^12 + 18662463175636806661952176808514882689167765013258260232242972323484987710934665053339506324442183847168531102266615050568870574279711/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^11 + 8374357326351856192357156496030342190326996734743025342894729039030808550022262469616889954971459031709927157634180758385078194249783/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^10 - 18052846287153995762124213590529766735137881701003716941564808638734986753842445759070274676278435582480296812187550937456954281083557/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^9 - 1214571167790130881230785201272227756576843262649179839876393358340141565747314182272908688837787311517262966155521897808257138998565/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^8 + 5243814338194877448666918554671645221904825460989416703698493637146112548580209456007844998604559143305406802821724047743281844828783/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^7 - 284065474002826867098575113491074273011325353100682270943613012984980722303836243652734487195333928812233001886496109007567860557073/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^6 - 219134494490819451295840918532882887544291642836809773495189408088360394729055021064216836014217461678720703728366199985555567769766/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^5 + 147760383239379569939753768375169308143130478167441317128097747126555401255401978432413038806550021826737226002981792001918119540801/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^4 + 37984554073114067582813537107616349995789023040906144981960337503481901039162390782225324321097635259067700258262059428868434749245/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^3 - 4398324411490115245822411931802737869957838019940737311615520307882185952850883664026107440714694916119078348989629406748678795461/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^2 - 641783100127103838303827537222695412740448541721931074588761370387328680458601042883215332704666661255639173103552502952200854936/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y + 165021745954408472478333473356019632586987794591181815628223208517860231253926862060811471934549973338024573021328426277510551820/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349 7257559833780401399952598754038959784910473340982045260539101517098243448099817316301086512889068875070572328402520451492681709/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^35 + 45672546849711017839832257780372746243321976156152945481337901671549393271659316632892686390609589778422919157135179240453323479/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^34 + 14270902203599372089422900555318655838614026652538683853416944525223534987474149833778392155127164469174512464457437262545924133/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^33 + 425890109855873229626591449769521570039009734519057302053652708836653684806366464759276120790428017094615735586547468241288627707/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^32 - 8408626205408624303019328267182873363257322718179726935546580503115676139893495990511042025189633964311126990572663687534474403529/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^31 - 46647551348336276849796275413317428140819357810781261706256153108229072939818346065401660866964158273131343766274896337108527399439/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^30 + 40187793989719029250459675221291346065534430592540475447499100386047939363370379206641498863297876294748010789845965503944825912639/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^29 + 106989347489000873854926771758091977260211156156329531399949845384509684996443948374618588573740087276215104071870878377393663400356/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^28 - 1582565119044733152437265764200067588878973431356043332304368590893554317218340951904923512609724725922330385258763019074526618628927/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^27 - 3648204637477916621147038831531277191793502364462136665422065695492104813268538370191698889883711070047217566126616036219123161352555/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^26 + 9230962872109439338850071039570578751987922031338354467201872924032073839960674340664707961522440824547790583266832493138231790217373/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^25 + 18496316638023347799620983835906119510579156998956796430935384452794381853604791694988640906771291507954750850842774202890616168556371/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^24 - 36109070568785952419449404865278547909239645775711026903953391646295179925815892582741262477565456502928180541188015483083321067024741/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^23 - 64027685653387491934659375682141280213993042995516953204579926558008613210901179448470672408714764238856105486753144192958751682755925/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^22 + 58926825140476178934984184695473122762247012654256498023715402815851835008089862930666068331939275611793011874862094235766769545133433/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^21 + 77123634262839366090419710956838162086002136624284052578698512802986144685186338163563206641439469979395213640949743047969743954293305/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^20 - 166002796177461248596634237374473222154660008219837425081929473998698596506223221071928423783270700047898743138848844730580409640139577/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^19 - 484497226821319833538247504672697388593715334825456182729527073419821395822649922494341317782063891817879044452249023726807445620770109/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^18 + 677997110105154726209874654818361248107705751152993698602341667327723575310643333525637986994159944251703217677427176356548333520279899/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^17 + 450447333079302155051135695639958695981370358707202346661478429361777194382008435324197077667608667577063989955872690462621236958994711/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^16 - 450152931804015261642311489578295219645087217412959573719053759434980704722991473589633803580030290373902339016962022930929068470726733/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^15 - 24092834169185306708919782754155664552708763531104157590100629934922900101134027018998994027737686740064177055718389217090135429589816/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^14 + 94249411127211026739325625995871523476586122298357605701558749308375801523864450956692537157552884566162336125074092256100530524327998/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^13 - 17803416998565872523289218205978441950881678577687903542356700364486420352505403651291838139478794423167387990330384207962841736894613/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^12 - 394019587544839496575576785917682316931366956980606214063540236132261452370323548713643443130262536819405551149990765523586332568481281/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^11 + 21373472719461349470400750403212636140267162958868091909788394090232071563170903738662391355254980559276954944552239842558237541529835/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y^10 + 126448223471049841107954672839558106178645905325471502742544784973739311987863841825664427541461145006891927917569983742789885869729283/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^9 - 44144245856954951793950102224202122207786506123411748008533090084349835456852017166412032554635242631624129615322192520182818589197629/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^8 - 24179332830526458759470942534865089830749257418405196733888695565096972888429524883199007028362318854700409393254706804396530847214205/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^7 + 5815776564823016960811790540059057027093738907609424086602245010294688139105753106912147507381267899079857604960864360735284438385187/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^6 + 2606063861906860222189058930864255879153439068001336971730337508583945307331199393474909861763364551073445921406065428873935167302903/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^5 - 1692999880662566002945437693017015979014469962508917870883306214150084185616159794050199331218244769415578479834911151196305003034849/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^4 - 144128144661631861358266459373671619002121012011163192317184316662938616085917423476489931989064029357837493043809742903724277992855/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^3 + 64076673439854468596615416738856255971553431472969593298409785050301709932272040651494226067765087860581650196979035856340366128659/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396*y^2 + 860510421607445304486435854701107296878967033391260134887718785531803637933559163594650958052326897483645412455481789917008155487/5187279057556526370064228015071867745849153030107698489652850373199548131065800236513786323958898739418460112002537148696924698*y - 1908284627596778394087835062324765750798413254240590902515280233410570272235159825907207226460590215485888948464424408447998397227/10374558115113052740128456030143735491698306060215396979305700746399096262131600473027572647917797478836920224005074297393849396 # A Gluing Matrix {{0,2,-1,0,4,2,0},{0,1,0,0,4,2,0},{-2,2,-1,0,8,4,0},{0,0,0,0,-1,0,0},{0,0,2,-1,-3,-2,-1},{0,0,1,0,-2,0,0},{0,0,0,0,-2,0,1}} # B Gluing Matrix {{1,0,2,0,0,0,0},{0,1,2,0,0,0,0},{0,0,4,0,0,0,0},{0,0,0,1,0,0,0},{0,0,0,0,1,0,0},{0,0,0,0,0,1,0},{0,0,0,0,0,0,2}} # nu Gluing Vector {2, 3, 4, 0, -1, 0, 0} # f Combinatorial flattening {-1, 5, 4, 11, 0, -1, 0} # f' Combinatorial flattening {-2, 0, 0, 0, 0, -4, 0} # 1 Loop Invariant -294104667909357135915774879456526026331870917381029317273444588696781897089405426773923558665589210145636815917878135268897735295/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^35 - 99341698928849297392722279292000211229288296922694775786957106225320226552916286006609897158745610884717442518501773829856096075/20749116230226105480256912060287470983396612120430793958611401492798192524263200946055145295835594957673840448010148594787698792*y^34 + 1473132369731413571459164107532285822188417862117935014348052248891679905642218764713796634613483761974991680972614245806753571255/124494697381356632881541472361724825900379672722584763751668408956789155145579205676330871775013569746043042688060891568726192752*y^33 - 4949287168029446466978142558342651617670539963603999541583918403830751251759454242101944029488724431225320548365661486979692341153/82996464920904421921027648241149883933586448481723175834445605971192770097052803784220581183342379830695361792040594379150795168*y^32 + 63302978407871842064229752596924886630608219766217436511162887800719502579137525923773630230317394556591241726198265565212643299869/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^31 + 375052877931593241995051270807687394374715390704337512229593951251550203966003044748895886554565089655592508132481702190001641898601/82996464920904421921027648241149883933586448481723175834445605971192770097052803784220581183342379830695361792040594379150795168*y^30 - 10693498018059674491502384310507928224562667456998823710964136180099200882383805271879068630813173971822670771182868278465580048582189/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^29 - 19921439185275513915039987361290262622299420525428666116772557514982916260589473650670777533191427494212618619715719996671574647150583/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^28 + 70141086328395759323710531306903216198807039587346857463786153889763024680730392796683893492626707043505744405858620998208319531548709/124494697381356632881541472361724825900379672722584763751668408956789155145579205676330871775013569746043042688060891568726192752*y^27 + 24798418036922348658650694234300117081447527503626417142924390010761944184885104027713815749787166143817486182903097154174569879295041/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^26 - 338750805549111634339899367351621076051945091590018001187887803914837129683181250814486265296415533645082967155860552306350500249639165/82996464920904421921027648241149883933586448481723175834445605971192770097052803784220581183342379830695361792040594379150795168*y^25 - 634411299361521184728357639127949693065264002670216135317438874104968801272159894170731327222148391786051128666576580737652631890318619/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^24 + 48701580545259886710868964392868947295623963174872634797869218607723688349217265335865724323324310611634452134764575422162800862491867/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^23 + 889712297101108297571000910169690809553510268757642065283852820472352577736581638423655824680803530759537632066160966843072111980553469/124494697381356632881541472361724825900379672722584763751668408956789155145579205676330871775013569746043042688060891568726192752*y^22 - 2621355369618192440996039790285386723794488321464769308087294187351994843901323561603067627704649655777781017042774786688442659564172485/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^21 - 338368256955077605920327088824984544642956722913259043252708901360865510698400268118033949824666103944341424721468645573758018806103919/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^20 + 19597319236364842964928860147997849180126119491373041168521969786089140956703055752349990156219219287093167277884179775267590332056421525/124494697381356632881541472361724825900379672722584763751668408956789155145579205676330871775013569746043042688060891568726192752*y^19 - 11351104366918226437573209826385186962645931959810771306362274329938020212386946900123152857570052340487544881943425463375394132355540955/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^18 - 4108100215117968863601276587679801431529134770196358059405658705014577248620528666466411125759856496124095336282737670815178157105183249/15561837172669579110192684045215603237547459090323095468958551119598644393197400709541358971876696218255380336007611446090774094*y^17 + 14419014329626543077284578297745335538084331063532709468135927417741991833513448527004934589325727371211409733764296249164872630136809761/82996464920904421921027648241149883933586448481723175834445605971192770097052803784220581183342379830695361792040594379150795168*y^16 + 67293326291158550565009525835150211400436723488896383165309749079305900313281834053353394889227583534088554827398046125102217269853695693/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^15 - 70367916619471424012642763922055287035690465677209995827543010451513302154244963067088456700723129394797718749617073000800556293882027949/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^14 - 36553081326860905229359141420564645241083455315587605546185920875520500715679617415305491395396318146173606829921037025643369096576346997/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^13 + 62622679980347134555173864832869017539590471830536098634866355545037453335514600737921541897643018252277038987106816264669928636848386803/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^12 + 1174917032144264317589296500986004707221180590155496803106461616233845147065328818270867712042000865343985681751231726143932797715616847/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^11 - 5338740936842832362515770898319852505266979898996522928323500056495047543276684886077703363219926536031081448013495516648898277533275189/41498232460452210960513824120574941966793224240861587917222802985596385048526401892110290591671189915347680896020297189575397584*y^10 + 5753975135403811724139789309438321147409237656467539868899818521372774033639505792188677525183320861232676940846763301043545020745318723/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^9 + 2304500731587692932375968940894779136531850738203798029181623301350182674364686376703993002940985773038289712154085049119462599079478979/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^8 - 3476095604866223317998622222229093398090254617438658523322028996832285764537126018624078753710288751418493899691519756413087751027088373/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^7 - 1328286645580205339450217745853672131411218808508509331958753205336247189203368758927312874583271182749282524917641275589667932969899579/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^6 + 423489872407865719771787275900051811137590831643591813253137477712951414977579619735404841321690044837556292081137047253974502645922565/124494697381356632881541472361724825900379672722584763751668408956789155145579205676330871775013569746043042688060891568726192752*y^5 + 48051253715587965644452937336903674032376374923418496090594538981205468802971352733437925779364372433392955081892645605647182979375317/248989394762713265763082944723449651800759345445169527503336817913578310291158411352661743550027139492086085376121783137452385504*y^4 - 24277894251310138092286776188563769455486977420299783138003615603088586490495685232384107750498504295550699931444619616867491506992717/62247348690678316440770736180862412950189836361292381875834204478394577572789602838165435887506784873021521344030445784363096376*y^3 + 89008145969269538219373398048249824530912050337297907557399495083852745672205211004756356547975914529491950545460737147995042203522/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349*y^2 + 134181795186755924291196858456522419290029929217558318965529353077393839222588942307210592024723561484422201979467852271871519272107/7780918586334789555096342022607801618773729545161547734479275559799322196598700354770679485938348109127690168003805723045387047*y - 7579915437159540579666961999417376562728578123684827192350139697305789849878345150635557074765707956966883652676955386228512574574/2593639528778263185032114007535933872924576515053849244826425186599774065532900118256893161979449369709230056001268574348462349 # 2 Loop Invariant 2280030365575119273570154976347459997116998832896015567373183133677344475421418111165582214527621498218303887139027233457084164304930164465050526332652707427361809389673071705017447602466011504417276627987844336681212334846624674126082173153687796049451869381806189/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^35 + 414621645113182266559507344666486341858354265169906727754954044978846063433559821891952980630193544301782088842496977408770690498850654518564357818708280021608532479034062977258558173689831735199373719979443569275213291430620100306597284877116632500445243190190437/1724803805562882774116085015645844411398655103549134552275440132894660927631868199989215948601425548284869176618971805090951904709042346557688681665750996524132093653912887407793763806673105796335567580848123543524244617332655726752965801846476313912281618235257936*y^34 + 6293877082991245054675947820526818313998214729721450135613050828003797228243128976126621110273550193607562680060297242752537178438273867084122268496264443408849948919779666204508536527254465468680067612069606221543670229700701283267486155542635916177716627470362553/31046468500131889934089530281625199405175791863884421940957922392103896697373627599805887074825659869127645179141492491637134284762762238038396269983517937434377685770431973340287748520115904334040216455266223783436403111987803081553384433236573650421069128234642848*y^33 + 15116929366097078776418304571035518496240262480128342494244483521848257488639042300176048521451741463634089761943224933531181364527090177734301970025713140907447521590793016711253143009405783827626105967294755829292221066746899573702516461031859567960878268576458089/6899215222251531096464340062583377645594620414196538209101760531578643710527472799956863794405702193139476706475887220363807618836169386230754726663003986096528374615651549631175055226692423185342270323392494174096978469330622907011863207385905255649126472941031744*y^32 - 144849011677567062215416239284489086182460116097513310779346305847808283865494554632178275089912866671394185961800496910357636880064723540160124454771912649517117293092973545816587402650997925645486889310824046234111706685736940748221949347641372958761879871427019943/3449607611125765548232170031291688822797310207098269104550880265789321855263736399978431897202851096569738353237943610181903809418084693115377363331501993048264187307825774815587527613346211592671135161696247087048489234665311453505931603692952627824563236470515872*y^31 - 5108315065544086500906192187935389006585218587338708071629807945015942694671000600172506789874631495143165070771572688606948916241328187446318897366383588071481460322021528149990442728288525134388768609515071524054781791655756296980886933855340275888304435109532699395/20697645666754593289393020187750132936783861242589614627305281594735931131582418399870591383217106579418430119427661661091422856508508158692264179989011958289585123846954648893525165680077269556026810970177482522290935407991868721035589622157715766947379418823095232*y^30 + 46810135417854991374844410710941299330099479663523069413848056840359299253574724787206021171529631612620853082567267197729058362747352619227705947024067084583171391304226123224490966828743519295027116990717534574764650718178421126764634914614604522838655995891201273355/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^29 + 281701222996898374982437066030215579114683797311546147817918607381638254668912266820340792896169533997932144014064484365551438380906998513804648378454361562183228897950777103208979878526943898290401465928946475893213456958762031476206746785288931916181042189346542719521/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^28 - 214948588043487092169615458095683351043121119490418192012703414935323364898187961110225221152542396846842354379833031489796423404788579301077732979333477436916906267041039501690288537388477612599879881194100320259175186138322133307495522768550771149739045635279956730229/31046468500131889934089530281625199405175791863884421940957922392103896697373627599805887074825659869127645179141492491637134284762762238038396269983517937434377685770431973340287748520115904334040216455266223783436403111987803081553384433236573650421069128234642848*y^27 - 403053178964782639748644010320513584618366082633666591444478610491211295613343473647499697014749149669250241835804543823391108521810911234434232886443817358538650410311613819823933657530324108829157030524533024210201198607129450883972404619753706409080712842449774941879/10348822833377296644696510093875066468391930621294807313652640797367965565791209199935295691608553289709215059713830830545711428254254079346132089994505979144792561923477324446762582840038634778013405485088741261145467703995934360517794811078857883473689709411547616*y^26 + 777342929269328250333582978588264883496550958507349695882245525870921948440548428682209229333237637428254836693749809761632013987464663020863775999591754507139651740319163136590711510181150760060496500927955037456295042866646561776003594100577647988844044484625664169283/20697645666754593289393020187750132936783861242589614627305281594735931131582418399870591383217106579418430119427661661091422856508508158692264179989011958289585123846954648893525165680077269556026810970177482522290935407991868721035589622157715766947379418823095232*y^25 + 12354919795095829511745425746356912866391422052409617177713092076270535220573912070281087555237769358557101815669782926112179033810172252032815443395912118091676007698085425012252856105169504524867445178105898772430187568841283154969506666245109362964401797235021173823217/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^24 - 708307080640299649844837201045465368475072432497583294885557050780326271802917510195289197045709335148608752021859555443572278350054000170922285448516616671644351402863936186433382697546563771275370155604841930407966836052301000828539876468634554660162571030232049793213/5174411416688648322348255046937533234195965310647403656826320398683982782895604599967647845804276644854607529856915415272855714127127039673066044997252989572396280961738662223381291420019317389006702742544370630572733851997967180258897405539428941736844854705773808*y^23 - 21542011616071848718286479372347089232168228897482800298964214285211997336628160202281973566487089781642111870903699633251046725152088041125849473834502513827550371335685891968869168769483940089267158555836030918093735591810693284935228931641919301445872772021738807314443/31046468500131889934089530281625199405175791863884421940957922392103896697373627599805887074825659869127645179141492491637134284762762238038396269983517937434377685770431973340287748520115904334040216455266223783436403111987803081553384433236573650421069128234642848*y^22 + 1517507157534207814125583216651665639602871103521148354302646180915863514193844199555866209801735147198152179333244939010470108411265546911833779507605885214596407492211748319432762418902653756432053925362537888370709256451494179193043066888652253995415489294203159865089/3449607611125765548232170031291688822797310207098269104550880265789321855263736399978431897202851096569738353237943610181903809418084693115377363331501993048264187307825774815587527613346211592671135161696247087048489234665311453505931603692952627824563236470515872*y^21 + 26546937270005513033601195459162854921386414683402039754623719876568357265159674482699746760558475569986290425730644951774397255602792935801598538864495266893047956588879234411517529361930638694191538702414685176075782223628414788114265990671050310800780377904336102881955/15523234250065944967044765140812599702587895931942210970478961196051948348686813799902943537412829934563822589570746245818567142381381119019198134991758968717188842885215986670143874260057952167020108227633111891718201555993901540776692216618286825210534564117321424*y^20 - 40697448337677604834428241401215643314571300196443117936416187249434474235732324766104621553069671475300635907499366709821083189960821342470589730541191543549427064288530811013951336900616567022718019623063956845191617412770697524834133152194820340002659722484609494047061/31046468500131889934089530281625199405175791863884421940957922392103896697373627599805887074825659869127645179141492491637134284762762238038396269983517937434377685770431973340287748520115904334040216455266223783436403111987803081553384433236573650421069128234642848*y^19 - 903813526397435352907885688933906232472440998609081497884494085534967852697075713295222693823772872380563811500321087344054788309961356694560689366180227422738321318453199914695135040005194442238501772428405764047315035204224089647593098981576088506620221176682813020959/315192573605399897808015535854062938123612100140958598385359618193948189821052056850821188576910252478453250549659822250123190708251393279577627106431654187151042495131289069444545670254983800345585953860570799831841655959267036360948065312046432999198671352635968*y^18 + 5577199121464684653053824706819920073843628080056761661820977365064841468445569529801105268790348403517185864092945745234484433733589027732885685485888408310919806668320893354279155508478471229044702006281101646777732770216045028918931110662694653352816374714563408959987/1940404281258243120880595642601574962823486991492776371309870149506493543585851724987867942176603741820477823696343280727320892797672639877399766873969871089648605360651998333767984282507244020877513528454138986464775194499237692597086527077285853151316820514665178*y^17 + 64337656166732993759877116934482976927813299634449646905938029449356343371334189709208830462956856284146363311328786693502101582132991855732530003189059703126344581941072234491734591531089406262619486017971632842691674758411963177527964905392423404951623774273995806312945/20697645666754593289393020187750132936783861242589614627305281594735931131582418399870591383217106579418430119427661661091422856508508158692264179989011958289585123846954648893525165680077269556026810970177482522290935407991868721035589622157715766947379418823095232*y^16 - 253554746031778111076205866087490347224637498758282032497281468542120814493306444383895470806634499307981462696022131275107483443344329206237511268430239614015005615281482956913285534065201825158039452584086262728686959095932332423568490398584433137026066207125751544405451/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^15 - 126115324489261311122692592517784531902246062068277836470245323460343300556471023067917535348218052073393293391267099451749707207072522198815846440159405964960374937180839870009987582970993542216519574902892823061385405014403567691175052691653771921734016182974138154335513/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^14 + 228053548034333592613850037620907804535464433349783738295148027024138967613355357148647100828950180356077883820609078186324540352626611898772636745939101269391868780320332377254094826765741017728779837101519566923795013740451366342162117560011880244975865291432366069610255/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^13 + 40147784780357919152849658016608110709639232531918523610996101751069436381411237354650182068141668176656698820974654789241965861044880948774806360379072705553164575515667720613966694842919674953147664763009574494632193667999167452102973001378257387400225091699709649951915/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^12 - 32517112776243030757150525595857594233885531661496263201984795750776338557741528730509614157961931177022304324260200069042271068793904776126136577008575911114399482904678973108534008338809930631625231861927561222657352807803575511732253776902905803782808833027203196523161/15523234250065944967044765140812599702587895931942210970478961196051948348686813799902943537412829934563822589570746245818567142381381119019198134991758968717188842885215986670143874260057952167020108227633111891718201555993901540776692216618286825210534564117321424*y^11 + 465560360069055409419077350955371892958953805964833792254022923976964610892013498761636140397312216052310209878413329658914568760449419673115757821576049076687161035421082637486260898234830583666019424282584812239012552138913298327633936439061105221382159339355268457379/10348822833377296644696510093875066468391930621294807313652640797367965565791209199935295691608553289709215059713830830545711428254254079346132089994505979144792561923477324446762582840038634778013405485088741261145467703995934360517794811078857883473689709411547616*y^10 + 46985774303218307372009793538460848756613354704655296553058945980251510253100508222765652442687799797925366977279379733680209814581468405720768998094908918067700253457588201495617100386612085345154003405617633721894136275608757737177399265024281838397208570920734638338215/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^9 - 1863299674650931959591330167624915806757877935498907956723155268284096392285862885749777022897281252032734408183448385829202828259449588550289816733403801300393897460663091270568841509714729663545983117305032284800221049195657671269171074880509146779560016486271081993135/15523234250065944967044765140812599702587895931942210970478961196051948348686813799902943537412829934563822589570746245818567142381381119019198134991758968717188842885215986670143874260057952167020108227633111891718201555993901540776692216618286825210534564117321424*y^8 - 10622163225760658130863653717515030873337093324816702072943465621086753153333456457593447730064483419995513465695953175055155784126627032507070623854851033813830343504746324824307307942778892770902778140860119756785988047502125694730380092782210308016240179479719530720189/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^7 + 2799526339975939929465887545765700088672512687616546069214003707631536068183133494415145285392701859244274866213829394186384721136291337742923055419682394141157852606196859281618998076407719983418676726898956922403403849264727676302024736990785613325572225950508806079693/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^6 + 726895877931437316151208494915692331374130574992534925285934192799971390153566518112328021526091576482670650392366620057532777198774684345617404775166045749318004407056900130810810484446335845225320979452118064114535150372612550014348660780278860898122627531977646023177/31046468500131889934089530281625199405175791863884421940957922392103896697373627599805887074825659869127645179141492491637134284762762238038396269983517937434377685770431973340287748520115904334040216455266223783436403111987803081553384433236573650421069128234642848*y^5 - 501717401227362030523921919102243789272910647453203807779514178531379336493714226932860998663989117390858678207574643344645977642323575263801113078137249099765955993183143119186450463280745127233011443742042834245811809157266435813775084622022358844774007184733948168043/62092937000263779868179060563250398810351583727768843881915844784207793394747255199611774149651319738255290358282984983274268569525524476076792539967035874868755371540863946680575497040231808668080432910532447566872806223975606163106768866473147300842138256469285696*y^4 - 27690483204858135601840508660125471269505514986407354222761696834289303197683557597394826462277627850433231468630911849112500903224261975903546373826729738010701401804248034724988923057679735533387858563854887353771893548207971359268270775392429522673943007306417817647/15523234250065944967044765140812599702587895931942210970478961196051948348686813799902943537412829934563822589570746245818567142381381119019198134991758968717188842885215986670143874260057952167020108227633111891718201555993901540776692216618286825210534564117321424*y^3 + 613778280207859167704915332159816712466425627486736090532265014428450158150777578370930363012003169862120675638888825471076859362196261898332638598266747330411108533912657772703576398906806952776802608348269736179270684250875906132934241288755916670079393516359641531/862401902781441387058042507822922205699327551774567276137720066447330463815934099994607974300712774142434588309485902545475952354521173278844340832875498262066046826956443703896881903336552898167783790424061771762122308666327863376482900923238156956140809117628968*y^2 + 454360422687207665220093683909843421073287925906845133174756364227682402929272708923110199569345819101602881037502733454410387550100779614725018552254874606971169092326014828803011263696200606894537135891123453682424616416462575920880479292830605724231647318616201053/7761617125032972483522382570406299851293947965971105485239480598025974174343406899951471768706414967281911294785373122909283571190690559509599067495879484358594421442607993335071937130028976083510054113816555945859100777996950770388346108309143412605267282058660712*y - 15568226474331991248279567395421111419864610695143599184961910427122335651694861828666789066479343655803855654995661588811359531053745219281391403331929412060894169985369923056729118445066742420379318014875278651830990581510018971627050971549172810957810330018833325/646801427086081040293531880867191654274495663830925457103290049835497847861950574995955980725534580606825941232114426909106964265890879959133255624656623696549535120217332777922661427502414673625837842818046328821591731499745897532362175692428617717105606838221726 # 3 Loop Invariant -1989586417064334806865529783418936243898280874897521873160707343432995498677215193150439165376317956374451088297304277227223542782486760422670828889959375586713405313061143112008420590776347383971767090855811128219832866170585646252502350904471671671829861521085816335352696668581643661731449276544972471413192007459462467452475819/527455726882163857411923583585762103668318234449136011179196523443460498988748432173203796685518351411435573254467724737769384642065020334439409379778568082155264391996243630855732931017735842746989910656869260299550909540509411562533541465976527073715330810385162955922438252070597489390020227013351636892577530553642569921206455208*y^35 - 14686134920858835508133424983480362668986652227453718782237767468833374765557070272805840364873949850064467601303422715382295034994603842334227921241470094866614768540180602057778859796286174562709071521606352504360357825443187052431713787874495747603908115612027585505241671310321090935283921864808392501344381926350542792887497433/703274302509551809882564778114349471557757645932181348238928697924613998651664576230938395580691135215247431005956966317025846189420027112585879173038090776207019189328324841140977241356981123662653214209159013732734546054012548750044721954635369431620441080513550607896584336094129985853360302684468849190103374071523426561608606944*y^34 + 1989964630563793880835061888190059240205080498583690586177396681961783812313788631473556416551620525531202262754354451234330443988014902711428806483892261183170440719466677497955463067457490058376374380172657763602156746216685282476167360095559415760186608673594958438031136034801271774274425568477114930949309348252695069960719161/1054911453764327714823847167171524207336636468898272022358393046886920997977496864346407593371036702822871146508935449475538769284130040668878818759557136164310528783992487261711465862035471685493979821313738520599101819081018823125067082931953054147430661620770325911844876504141194978780040454026703273785155061107285139842412910416*y^33 - 152841012341782174299467768635016583054867815929447946179577022685646847350624845379748868849122623815162893584821586875655948390019929796965409450671588136895059922204618597265039117211971577876842039097135299025637091131360972812199592619586372608309773648213689623725737479437955967835478828959870873231448366004306160206254019881/703274302509551809882564778114349471557757645932181348238928697924613998651664576230938395580691135215247431005956966317025846189420027112585879173038090776207019189328324841140977241356981123662653214209159013732734546054012548750044721954635369431620441080513550607896584336094129985853360302684468849190103374071523426561608606944*y^32 + 1595288454847384974380312703483432164142328623483339273808373418292200857430545723625343494134267622005592789088584678439511757975802381950624053922559241684921153631332539325464150823631435142046428637483253395809290596199860615552781109634487035967170889192002260412980958503279620568326288389736962271810444919066706118691278083485/351637151254775904941282389057174735778878822966090674119464348962306999325832288115469197790345567607623715502978483158512923094710013556292939586519045388103509594664162420570488620678490561831326607104579506866367273027006274375022360977317684715810220540256775303948292168047064992926680151342234424595051687035761713280804303472*y^31 + 7336566073439643882636335581240727914134598211257670674263148226019762358153572131935370360188164899994167295487227717011426585646095442446613264888207079546210032052179844180178014779373494206925849455878523312114181260003346405472551083558905654148062954310259402990388818856482913834044221737921674006639454110414884254475441895301/351637151254775904941282389057174735778878822966090674119464348962306999325832288115469197790345567607623715502978483158512923094710013556292939586519045388103509594664162420570488620678490561831326607104579506866367273027006274375022360977317684715810220540256775303948292168047064992926680151342234424595051687035761713280804303472*y^30 - 423724613074589044494263314465843437802460193677468478203416142737317769413499810189925187783527153828272805687871959732916270282819783897806316650961055555258652832749917432128149176114246169753668415266960111914166096335575206354833990026013164966293181374055780470969699419079425572816262143604237318249431244502882672405095764084635/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^29 - 1579652742816156245387637584848396390969081105655109690139531355456220112293217896279320074137759301603346409156297398885923248139323224555259413579581515488924928954657217236354265883068631300032968588944648375569031852815751006480767890716613877316982051200803459055861250664487857374290502069215408484715436821637088525518977393854065/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^28 + 594858930026454273299795248607613932456530266133163211098098859305897905688933685036760772389263022163789834667856293850151365615971329479721019797851525268639887718752416777388695782711258706137011966708902282011161874224340927258384464485076848089902857893466801234498270543762071919903953011398331390879372498977600371604603013143563/527455726882163857411923583585762103668318234449136011179196523443460498988748432173203796685518351411435573254467724737769384642065020334439409379778568082155264391996243630855732931017735842746989910656869260299550909540509411562533541465976527073715330810385162955922438252070597489390020227013351636892577530553642569921206455208*y^27 + 2136896821489873425356716290827603701957678522279227370634685136385817529699826807359026756811950810038031592549293565212633658391830136074324228079672362193839488032607780509112612687774408546608963233641661738610670694358148457645268543647515698359667079867643937732365877907048872974491386621843159363865189209129305746706082277955379/703274302509551809882564778114349471557757645932181348238928697924613998651664576230938395580691135215247431005956966317025846189420027112585879173038090776207019189328324841140977241356981123662653214209159013732734546054012548750044721954635369431620441080513550607896584336094129985853360302684468849190103374071523426561608606944*y^26 - 10305811984754070657029146012753262171473020800128922446541984833391488083621438154766868999387310171399456080276008157874534083543589963160904611279580099846887139642811024508569374189301771826774282204094363418609233113834044073743525212341560535552568522106399291970184174556529592868925542938294656076644807598011262752764182408767365/1406548605019103619765129556228698943115515291864362696477857395849227997303329152461876791161382270430494862011913932634051692378840054225171758346076181552414038378656649682281954482713962247325306428418318027465469092108025097500089443909270738863240882161027101215793168672188259971706720605368937698380206748143046853123217213888*y^25 - 61236521125340687067048236449181820759672054641347654566719743613994593385760205828589894909320182354799596143850212929876970500415620892916447055946301708505765428133017167404273774370020156842978953384935859626657466985521050143230987396308708794188765212489889357703346720971868678989683047322718113615658215774593694156555545540882807/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^24 + 43832347263380924111007872926180023060786370041548500966990864772489163095252741516816194666051318582908630937319915473050997604986013094182829285316622760442946370050571959502991452850649171972524826802486013914036532113699314536756327928066436403519455823829288570541068372023472261036411147081870826100503505627863709591670917395553847/1406548605019103619765129556228698943115515291864362696477857395849227997303329152461876791161382270430494862011913932634051692378840054225171758346076181552414038378656649682281954482713962247325306428418318027465469092108025097500089443909270738863240882161027101215793168672188259971706720605368937698380206748143046853123217213888*y^23 + 198596093085128063425018901276488066385110077668172330743085760451358022067761640283984499562828479836352272273145675294701787460605879894690784828784924262723051381665255615103557313678229402992845753172249236968985444574487560558950187494276496250698956299598157194053396729507072249108278736155189367673112192631980201424565932154181505/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^22 - 72183618304456489857678790677588367009865757910147054125444056758358983955306907088506598689803929719520543224677994319083557298851299408835157241553607701200018192885459141524952786385686322403881626529107275906239738920140724286412436646539481053209097772309653188581510404169922785734104577476909836053720499142006518534978280295581575/703274302509551809882564778114349471557757645932181348238928697924613998651664576230938395580691135215247431005956966317025846189420027112585879173038090776207019189328324841140977241356981123662653214209159013732734546054012548750044721954635369431620441080513550607896584336094129985853360302684468849190103374071523426561608606944*y^21 - 203381856144881104510268176850333227337046250326544173275122048810738609223967579704913577002592618331914696999920739168883031406272277096745153019190921723606860280834994333321063581525522742812233620606598524643249131077091791644096994913947345772674391779064926488564639087238589655634094068456514936106826217007819570717548227869417959/2109822907528655429647694334343048414673272937796544044716786093773841995954993728692815186742073405645742293017870898951077538568260081337757637519114272328621057567984974523422931724070943370987959642627477041198203638162037646250134165863906108294861323241540651823689753008282389957560080908053406547570310122214570279684825820832*y^20 + 1115704198184397510986518563943892376062095682157490001812500450984086224199602124367160589731611784855565276662272599224672548832538323146961292544277752283954480122336055426177806542608878448816378181531607495810570844107372397333393629485831629783120910510601981519584438443408691933570987194688397822812233353414279363763283030602422149/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^19 + 349019661461286912726695731821301345189775556758007543025209905000816504510544422102342905561016134649444908462637674965656292384414237094678518915721921669227624724637648111551816953571674944970043621500055448817139219288056386538342178595278134325967430583667691687328720458267384678737134747370089246846760940820960955410313453361387079/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^18 - 982230820649019682753124402882338192620530003693995800564315095945388634510833023283288838770367092938388525883694414014387667885640959547860432547586174253907685316646782100844911774044024207262867775834726219426233283822832058828092084124921865536151353691565571541693214730161371948165411092321327647907108743738394150412914505847011187/2109822907528655429647694334343048414673272937796544044716786093773841995954993728692815186742073405645742293017870898951077538568260081337757637519114272328621057567984974523422931724070943370987959642627477041198203638162037646250134165863906108294861323241540651823689753008282389957560080908053406547570310122214570279684825820832*y^17 + 54545138667207949076953124378119450510569119624579982556613749951479713048702905214155372267006361229157329546156035226809349774220818245806463068698403162414218003617621787237028380891269029269901648959506389644999454241890449993484041511979311271925903836759474303306665814731072216233973264291355145069227541019134020403384754371061655/703274302509551809882564778114349471557757645932181348238928697924613998651664576230938395580691135215247431005956966317025846189420027112585879173038090776207019189328324841140977241356981123662653214209159013732734546054012548750044721954635369431620441080513550607896584336094129985853360302684468849190103374071523426561608606944*y^16 + 2127224708603903591424244485083053289014640007840376589058064631294102945752942034043815986770892466576729515553840473668255902492284413691042446423206167921525919065173373156793152973902239532870299264955435506140146994687841756729474572303705788085589266285957289555683635574594408733260699245243686063450078880151074788250173388302918595/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^15 - 275676812783073793414665868724468164651876108932317848324312085951391682949463162022002309998064080695332624617692056813826602600165088079667084581666736651957376973554535939055212006452923990969851886618086666432479295878228533285632921342010662301353049501593580161412984383959501531035472570806157281633206139054404469516779316916550603/1054911453764327714823847167171524207336636468898272022358393046886920997977496864346407593371036702822871146508935449475538769284130040668878818759557136164310528783992487261711465862035471685493979821313738520599101819081018823125067082931953054147430661620770325911844876504141194978780040454026703273785155061107285139842412910416*y^14 - 1293983402324858190579018908206864692543315144669426515918865744238071267935220595225760540169967310839896152817867298581662432033745215530866220269464146204500309834882627056183538358939674708243211098516637859602581904992488574132843266396277826148771698744063351777247395249064591463112851556233997907819737067722096271595190051819816207/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^13 + 1131180328969879021278950020229278933144182197157512925146370305077459261550640791739888848860882190549660592161249360971627869496216078600269828798633749778399320559974610244489933647293318784684866914158580633375610021437820227747678676667413772097889856315227162929206787782900873266684540917484641289909158015542263019742796118696373759/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^12 + 173195338832726520957829857919958775219487459370844258753927889557831254159732197936264267290929323494980802099245165852814102896933015964188927864315704158732721941430793433157799927101018207750801788448095917875311571589961940077647978503990197172447231665995699968401680439489518408353228049392895748256366414153344382071752522881808731/2109822907528655429647694334343048414673272937796544044716786093773841995954993728692815186742073405645742293017870898951077538568260081337757637519114272328621057567984974523422931724070943370987959642627477041198203638162037646250134165863906108294861323241540651823689753008282389957560080908053406547570310122214570279684825820832*y^11 - 195894322266362833461986523105961665720023908622653820740679793872000976039297963483438535281730495173054304278446911367453220780448902547714285592699868272399369396511800629249487410207933976357993577331812346865321612641353903682996193254378174182146321991157569932772592056828365520778845285963844925614165039074788053474703992686329443/1406548605019103619765129556228698943115515291864362696477857395849227997303329152461876791161382270430494862011913932634051692378840054225171758346076181552414038378656649682281954482713962247325306428418318027465469092108025097500089443909270738863240882161027101215793168672188259971706720605368937698380206748143046853123217213888*y^10 + 3939543504938825683565146033279239713830987771981939328750437030730826968227623633121963437910790046383035947953066620338602850339954214116494761613720006286948030835688990530051162142755661768088125023144600402271755892148976597970348631420116817558943775867464316682562279781113398181004980636046550015904284368889035412921397507403323/527455726882163857411923583585762103668318234449136011179196523443460498988748432173203796685518351411435573254467724737769384642065020334439409379778568082155264391996243630855732931017735842746989910656869260299550909540509411562533541465976527073715330810385162955922438252070597489390020227013351636892577530553642569921206455208*y^9 + 20233401717177815445387350540484089464495140888072903106122293252662037587861543454959700117631834078178859702863518979238916234875222841148832855031715559903145557726724573207509951711464497911010856745263805982131543698216898517732280803737064403781355414963781281535277719084975084079293831225585318230129029019504526638850970088551683/527455726882163857411923583585762103668318234449136011179196523443460498988748432173203796685518351411435573254467724737769384642065020334439409379778568082155264391996243630855732931017735842746989910656869260299550909540509411562533541465976527073715330810385162955922438252070597489390020227013351636892577530553642569921206455208*y^8 - 43715981533448189842386016791431821490517422074340436512194416441030391337298512293451544559574221110583439830070513097641972624405801917243136425621416213630957123290532075467477295237849577291584860662388505603110127384737921806702236536908780012010864128368019590612386141671116751625815396138208074814115684119095416998118928939946677/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^7 - 21820237510045712421709042543931766416387334518539312576067301467689675730536603323086258614960160582667324050673786913264299550398781020048879930108923237264501767389728481702722662558670275984674941490155835709880129181754095374699647542553171634226718206677932311541548445939036949569238140271924265559614481647064983510744389098149551/4219645815057310859295388668686096829346545875593088089433572187547683991909987457385630373484146811291484586035741797902155077136520162675515275038228544657242115135969949046845863448141886741975919285254954082396407276324075292500268331727812216589722646483081303647379506016564779915120161816106813095140620244429140559369651641664*y^6 + 5319391276339305745192032961568546054712067149850072865077155993626600255692612253879082023675052213156324808602398332173923198564295052103043099665781709878079136588062325269747437983225676806898914877543672452686622061085022462022312236318879752311340050750284012187644662111767057844804294241680965639392381970524143264380650524301989/2109822907528655429647694334343048414673272937796544044716786093773841995954993728692815186742073405645742293017870898951077538568260081337757637519114272328621057567984974523422931724070943370987959642627477041198203638162037646250134165863906108294861323241540651823689753008282389957560080908053406547570310122214570279684825820832*y^5 + 439966233774494654209224529076225461687135063721104738469752119024990924171313743056202512346405018877430697284430979270715860673040493833797615508451302708811769579004518247197012596228958675076599006693755927563442676431815369013190106119455811172817246449125178632779780630371429666566614355237396486166635601265028409569198955765191/2109822907528655429647694334343048414673272937796544044716786093773841995954993728692815186742073405645742293017870898951077538568260081337757637519114272328621057567984974523422931724070943370987959642627477041198203638162037646250134165863906108294861323241540651823689753008282389957560080908053406547570310122214570279684825820832*y^4 - 273109567368175769995944629244072063188781771070252702289862563273225704955022095433744924971049133830065507027867367241603112831857326798257633742640164830039811649343717092691159585003497759908415620257335066033975455277159231770258780165660780681773237011419204332456515862836345410348186735836976257829623472879929585702175225031685/1054911453764327714823847167171524207336636468898272022358393046886920997977496864346407593371036702822871146508935449475538769284130040668878818759557136164310528783992487261711465862035471685493979821313738520599101819081018823125067082931953054147430661620770325911844876504141194978780040454026703273785155061107285139842412910416*y^3 + 799508446238300672154661599713561267050660688552878874731368998893313476898999104919431864325147131925673602772321056778402989353053112437124947600827783381840911445791795561753435607528250296530934522368646384830853516360820771599679715980905703398025786904940406909850325078473373691117517702504889065313593170713241480738800048947/43954643906846988117660298632146841972359852870761334264933043620288374915729036014433649723793195950952964437872310394814115386838751694536617448314880673512938699333020302571311077584811320228915825888072438358295909128375784296877795122164710589476277567532096912993536521005883124115835018917779303074381460879470214160100537934*y^2 + 2587262062366910141760928272253669001797742571038638764591449155329664697224078399709788916226872578240233785332331468813469495513688945083948452397396962982860418291235814592088725364161196900057087278337339078442974855071568141282259865667349843363954998980756017169260221942203932687909461932222051179907863214912853299626064711673/263727863441081928705961791792881051834159117224568005589598261721730249494374216086601898342759175705717786627233862368884692321032510167219704689889284041077632195998121815427866465508867921373494955328434630149775454770254705781266770732988263536857665405192581477961219126035298744695010113506675818446288765276821284960603227604*y - 63019551018956303182925656175680329509492181924129122543444478613182494892962879809458235940335386132181706337513195393275434931186222216162354270153731047335776474893908516769966291092840798909269975691853731262291206576789418302463729020539537641650178057292090460769915238248385391235300566135537916926756311060676700544307306165/43954643906846988117660298632146841972359852870761334264933043620288374915729036014433649723793195950952964437872310394814115386838751694536617448314880673512938699333020302571311077584811320228915825888072438358295909128375784296877795122164710589476277567532096912993536521005883124115835018917779303074381460879470214160100537934