# Manifold: Census Knot K8_43

# Number of Tetrahedra: 8

# Number Field
x^37 - 29*x^36 - 24*x^35 + 1158*x^34 + 953*x^33 - 8585*x^32 - 74406*x^31 - 79897*x^30 + 990250*x^29 + 1435880*x^28 - 1174130*x^27 - 9163508*x^26 - 9946185*x^25 + 12959991*x^24 + 12323228*x^23 + 23267914*x^22 + 32355718*x^21 - 67169357*x^20 - 56972461*x^19 + 55563238*x^18 + 43942426*x^17 - 17384312*x^16 - 25292576*x^15 - 4154453*x^14 + 12852014*x^13 + 4629051*x^12 - 4443565*x^11 - 986679*x^10 + 703463*x^9 + 474*x^8 - 14666*x^7 + 16147*x^6 - 4401*x^5 - 1441*x^4 + 213*x^3 + 66*x^2 - 3*x - 1 

# Approximate Field Generator
-0.267525113334202 + 0.661663664080662*I

# Shape Parameters
-18281024667680451892603770106623336243791391540605321311892049480214422996005498582347390818273898758835474832236369029639289297640580046751316819566090561367759/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^36 + 197293414951818227844484410079123438800962244351614502722392853344242550155809111754221741817845201080541493362511944099998845565983345848373958922307305354105521/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^35 + 2175121156129775229336213614277581968325950006831979212764560151530667964504354540830740331523745312300094641499849634524322121269791936060533379872108644589983053/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^34 - 4336555769189552171819763476783658712043168251544586970346237432969989875544268049962179447601051033650646016230419054812998159972699229742900136664492089930133210/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 - 173776737320019080026460395314834314743906048686719201563318824021831764981865706454727252835286427552146178751385090370583578033271573479906838571832998461767377119/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^32 + 2480257938572875297897816463032121426552444965880252261753155680607627340321293934996889984697202009121542173089925475538197451200110996540888955159898546513615037/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^31 + 624765951904882029969503231821846915635882920706968720319035945284990583909238306341460710666196379128200845203000487392794520996879730063690208062138382415864799074/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^30 + 11710831645520133166233952002289027400404084027235763977416293524515503943312060882195629281214785165458352321615943365452253424650687144850928496651173759156394791315/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^29 - 5752282511580434368894017528458142560267516773046278055362126181583766555524923501827676211577684092451752538901312138139366096458526926963843789413410836639407235761/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^28 - 158502640824045882759631687688364594768564824430657506684148090550369107349649028349324607648344207301041178760074572899222400608638314833095364084539015738845783822779/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^27 - 192297852872557022416609909066656912960590735596599440320008854792952039339776805606372645482522940205255476141893094325261070829842935984106016536495001983218329186079/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^26 + 293094811285590496337695625031132790866413586171191418118836489398665403478471614674329239604511905319268518307657930946778649948628039083284864931604963806196984535935/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^25 + 359586323554316448342022605502218209770964498350846356317739811242295555074733619052282438788374829770100587797324691149009455165306479095092271748327454812426572302803/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 + 1297614845863687330136845974225850326089186206494784147586365881799572163273908792507137662341426755986028815983333634122152952023629981459571496613124623542458103777307/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^23 - 1734570527940460427971294628412793105747642871648336615207719212305399650642514865350283096915786785997125766736508160677898299379602689104917273337779357383437185136543/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^22 - 2287825711723507168982140356153371865726948075156121389179144333658480691629663450437280161511871567791979501611446263210911233028348743919843620129715127034378364936259/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^21 - 4047534217941637460057365015550156496566825826957046746158506929638907925967083641369444215747923669254487986306153601898508987985298823416896510915097051439296217693615/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^20 - 1853509505844249726069468444695583219180452996315878018005090674357855005716947352477121139369915155106277389559306852769190412576308039196646466198170674482483887847311/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^19 + 9369175219394851443072641531858972011149176213136391167017207617778031961246697725279088251735794680675274641139166106879563579859785865037488011089742584693721319725673/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^18 + 7838454143975505612169804817900156923005530201016297769878608051054561397060062194504740572904382463537942970452661121286237592600946939763776429273614932474308629712489/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^17 - 6886733087576673651655573899912604028242050272506482991598801062897987453409182918815927314299567002202659679869924926139792026050131445637726788265531854312283009847211/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^16 - 6330477189795093474326173128659790775890506652328657565587725765327504907898942063724985140371839791090820534899601667835502852570191141090702530572008560865127068921925/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^15 + 1715051991430958747989556553867610880431125191456002140346381292663788771850874737363731099032657244785418128003472521277457221345447492284950638451078265545976993552733/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^14 + 1762755275312425076825072817814648932640855877067895033774103695809302138188661645787378380534825698570051038240338998888228294706622313420206314487420038027624974810733/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^13 + 216860396736710232349984529725252528513387336755131221080337343129977390321461676764890493921559074408669015802848227749207067439524073896556078251451866301492858618364/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 - 1580904893179934322454466525808723037594136135951195639974402006844365486194099956806829174479570032881319236382612679245424235754598409713251431506924005375477468312225/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^11 - 185596336999937285385913266263325184381014607338504367873558634242713503824896018440983023031531493829545290250940365368049963291346709243908177891309120833307216628819/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^10 + 464419160237472599188631146034550117786369614540314749523563110612800847655019009769515353854686647501766541054968197211957173511534086726673899737924294061950974224941/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^9 + 82013397095045409069943985563387214292570837882845518734318720594400988778439261175693877117077216513224040900601978503604550106869158620446126772809542040475542318831/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^8 - 14431537667955453851019420102588582915956441601891162828760559253155997108002530755722764412006177198789073042171398466600113532480328395020470039209616040166638083601/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^7 - 1094893002968309560788003471827457864950492444330361533499053472450518380959932167164707914628578374998148481471026165295188713477863820072522260645114632714840612031/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^6 - 615731650109633647385029911503867656667383205564750640495054680093746500399416777696753560546614698572506570659262168064855889617805130924369440648461207328915751907/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^5 - 1215341640987317841442223326611877339835560540280820178733089238730433487272544501545783595680751213100813491069746683897191843354793825295308092670824190065771390585/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^4 + 288914914210783160882947874455140650832019955978415165317256763326674854203883623073898624883034557442708665748474459617751347790478515513107959840075140796188018597/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^3 + 35747237057529128986078735449686457681170699615645735070307095051812859961386965229834536878358984511623721973112803033324724881576478844254149756751586683945696560/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^2 + 339690202176602374061520357835469528508910245224327867176977858947159680281885084638194161825972053014049465290762602658276414591484754324982902657934295662488381/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y - 3273767515368685683457547903681801437623380467669262245671145957972656038491026250029217659023178119959620876627861503144942754900642821940658020228204849855900097/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524

10027989786801538465807908086073598312406177742361495470805632908516396617997519427085343338007183775794794598088743043640573904853920081749264829058102926905194/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^36 - 287389105589666431502947575074678697245502835504323415789032434386107338711104135749761977182040570099527077226203624938031395884660392392154796326612051134669567/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^35 - 339349439586583295035119092774990335847254586986868163657953037739295260568811133035576686613627477653061398833514093719810486921678279745462536547842777334419313/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^34 + 11513634877307650986921856895290897454131091687939989781154655591977346286563093066248163982201869151308525878675197339785354928319799175729294606694616285357267107/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 + 13502770973060825324724471399272635767523954615818212039077143777348491179503095665458220289721433334127882997859953351515747952319917742204396099802849518319747861/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^32 - 82162293596507015834112010843740501488927373815679081752935968729254093834261691307836579438235900373422643810360818720170969679844290286281395450288051673675547776/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^31 - 774838256659104474427048545087435009130716315623093791415820453507903953474466264119678262196791749687037108854347555015077529250092586513659950930081602995408561848/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^30 - 1060721107429752125921051166511118790776783362130213141777062730043398359741569847108867292517987918278336425625443238750186048249253171499601799701760390663158369855/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^29 + 9612733311032984399530749095140272943763536102690365491720446419506341149163779069586712623147051493546990726194046740433891870575877968285207346700516392396995856196/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^28 + 17733330704950301758580679216761428283643114835210997853916767042964335624326264468218755252244694338325291177202659747384399047396022312172473108736249063553772168571/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^27 - 6296406884945025261538784985130484378203074531015233116278739909164794067538747191478367614893280151628822477367465413238285403466384346962007050119362138093796586359/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^26 - 94961619015963577180886937809774344860974515461651249117314598691253969190931845110659755467711321611764404152517789575743544037152428130394013026275479789564314283702/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^25 - 131614608928282916953225193775144228428354533330488621786036193132099941559373225762875533571980802555880485060393045760340541813439189978613817210761231768437904603930/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 + 90454814081253395246532136331588778567217074155005452327290243794283009016467487315991075970889529842290114940171130276461985853095911172105276107269104532860356429836/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^23 + 161055882338208514405256434494320814869451317790030968857668480497195570490035774568998374966254888412037933252752671694427263985203316418192667884675380179206165697710/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^22 + 281864690044382235149352338824944952452731338671396278257258935469498403225569717342604174706142484853961301859798752745515659039099719362365171694508121995215595100449/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^21 + 413061365459982946289181246342097121897422223192677700148470534420504982146451300721278407005260689705282270963896702430887966870455491342373356029081126277471966021756/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^20 - 547506685325559679505082915627919277988919826359898779092420924931795996955884111518369861572269708024467680241593160962374470291602628968007957171728667096808065422161/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^19 - 779834192925553448695592559648542210092458996505848165769002508601512591193352537462348352422700038905924541991870791451030424117869207557794203194485369766419091179835/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^18 + 326688565514036695315855998572625287197996253285362658674029621922337620453848945865843803264882529730252606611043473643641939448275272764225524926472718667311373824219/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^17 + 588807933838394468718533670385779377989266960725520474421383069207831165442195986436471950173037461770298901367313209118145810337647698122039049306337157951883630158639/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^16 + 79775677148109747277262548751779304747747760261002665049884091499388290958432523003623835176501906337773030591313827500663920142640620711389318535667466218470450271/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^15 - 280313607461256859627226809075526134575339515525630445307595632171894591572411827957599570514064100791070654815020264003988489545205326691423562983813369192883404549028/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^14 - 131212061464329304082419920024867512768796423614504332519934598221329321058550049773985821946429768392527606112454057636783118069964204050093845940189704012614868552509/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^13 + 98033380779719779462191733796413566286415868451881632206338097750422695638766964015768154410370041376125849011777134105723517349671688291917741644580261728150409560583/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 + 83983183788694772035861424719532586894729472396281830541717771023439867599002812334265030707214649057054105104431878560902822424299230683096336511341999451592855045205/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^11 - 22207882284326878621111701559046599929948061822817950553545590849392330572799119442623960840604205014095083837432334208634284454455163129548821426175027293289672058741/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^10 - 20585565938617999748887387010635855162111721479433187557083329308322565625785645003819959777408015273255466831696172552244028274753187887363695508899485592384912164636/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^9 + 2035115487599764558176583666339014333164850033075236020989562141997172136202094252995038091379152899463446692107068337484617493293909431780892337908673531831290680900/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^8 + 1302693033898900504190793862114849090599281156215819677389362719036583110022886861395035860129956325044702633755093480989617908532761305345883216691700537361054785196/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^7 + 11809678246695144874265230245572456977852048115256051314228470170287807130164325469942072962968314851533058575861353325465553543859300018195045279608567162181279097/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^6 + 175730785336732425319202305463296783413790191399161602990441221306845246383691982049570167248882134342324154442657675561528738978198433832500044655382602271497321860/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^5 + 15716330135260812929024482572214576962377369914387732135852013520341479113641403690866144112725079673175296368077859613527298645696871849664747424966811879191765973/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^4 - 19056102928406338602378508089509551871412303006075886448931912955591800490784989057463276736141258057806633927601018365760981851787582658368634444222417239912632668/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^3 - 2428743121585797310462785994144925553236551897961722466360602195850708900923329551705065195005898115680600170133900327694217297281359212847465359839510588771952955/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^2 + 335306242061167863827269678045894552277330664436057678810308562291285411238734967459717217150156668212692841502371382557629134205163186168301508798480892884705861/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y + 111471396048396688166925068036703758897346738368147877300585603546771613772776726331370124044929684516970291204487416844100899326028468428847197054769657897849078/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381

1613413404908192143402778716067897990005460009968285173885995435244132921242414797019195963789837501149384132979140806150539153675952516462105758453325727054549327/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^36 - 23252061743817043096258293900152502851517572398159214055972804492860794744076569853653738225931874167153115618794819694414498590680881957196510005764625947351386265/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^35 - 23465008892266304820087687727127804251217774219309925215246667890848389799409926504870274258895285531858273178373558946457316298492948826383947515205256299803919987/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^34 + 116248258253389226534691456517856100919826394592632943330871897335749034600958699137059211034522710727063214482898785118647789130578735457118254335402458155012945965/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 + 1865808677598754537458787034068230049470465781647228646108272973147001830282752775536200603074793638014578800763187898899207286635127737018921056067318885050543787495/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^32 - 6759348830653769180516513076526266083706189990049609043156766623558142219690547335899355582594484463519416136560303655015283656605834313256733181670782521427520146495/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^31 - 30606909181933143600112101742717049049853594250753301257610519376974572077591689861657587993569651529699328098866667516137351368718764753302465257622057824071975413711/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^30 - 150542053729577751238050664374460157771777127142263942058189188601032119293920685927796778882585791006180373166415883883338395967218676029245500664583430597638322219979/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^29 + 1570870078922801963584908330448701494503929061398449430550597778117612876925160864973511021614687494288894610283604110664976004020076145466618343069585732073384499344753/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^28 + 2593527139977989397812558891632623114791370397384056453857599120993956557684017194019772381766785753061529015994586505542971860758868993729481105986866356972510170272215/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^27 - 1434087302407070992294974489573135022374245836046173173007201101710972705167000037426410058945899245732119459663561968780506473900703140586490078334582732844690404068837/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^26 - 15030188027557213589741957346578230785753027279693664891160938502139775641290989895294469723090959831272443555404646156482954427841860801975129217708582328934458383082919/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^25 - 1168660005696919685700887753489698406631187972708582072399641623052077149196386575899747273062585703750863992644785827703026374223497389411136149696522245030514654339845/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 + 17579517774475116470659137471827179938736418570027222095072982704364869684597517126533425921961449677093534262691995952146425450357278179245125201527669667618661414484617/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^23 + 22924961108816156939364048124054847644967214941713662798141700344054464049431787464689094446590724525381762892062140901760384954093169924368774440383980249549724770381003/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^22 + 41583968245611523086107998191544031839153806873912811975959656218727777063485973043679967090707915960924334127997707743028318820844935136800427262244398342127567286767835/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^21 + 59625174358527631749394645877330310340811901807579304660096926945269582607503672856876125281692908861377169590441231325876892808540293376740281211257160904106878967290319/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^20 - 48865626857263276171627933513046775343103186137265604311577942379977763437667811024929360852888881117524527793922577621639396471589955145538873009531935155490573044722049/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^19 - 109002370130082002696564457550205125679015665869775221588670311497766128207367570201313121724533764048655842391499396825979581503242300085145807698160347234900345894970129/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^18 + 70347824899016626887242440503569312292675639786423236128143914947602399213716126140497878119029737299750122259650204671456821482863394010461899364366650962092843538731387/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^17 + 82920322886179025719168251709820097259625703767292127431359429939570995062841528015240508265940795613656861107852867696101016060742643165537729506395426567549969882544107/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^16 - 13493098045824800026252292218241334968873316867503826290070233717747301567821070943846217148690392909429428994427712567360546271078648629712746204985448736534458978972867/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^15 - 42861999170319548423076691815435770940894308724081364312058773369563370988625960803008192082253306622066742635115201653897047242869700517763640953264731436774716483765101/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^14 - 7070080279642443167161108256148875728247705018786144962936701378176617547823772326704330120317117111860203183693114585021253403030616689696017685056716872029598202467239/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^13 + 1131599909429867756831768717484080489665592336911759895500471359808889701081714729820175503962983778893953024768983746144093236923618532198460081461106676936525710249522/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 + 10556557273277253699215453541928455268645121418718198927782629347800970491294435513166461816661793174896083959078346767364025302165472076155072543413636942472232940556549/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^11 - 661172928808159930575199127672501494089404720457804768435319624623851177744890233893272953684804905867086747054381065749202390421880382035350467154199460767178622167489/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^10 - 2465182447305507343200876004205684862016962962529975379619148664192777285118376611442756589914740308115106769135779430749358394026536594629472558706962916422556066119649/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^9 + 353907043061242280168211265384927921301711935432450674002760075006982789983744899488631080621845726413919005867205033280420851487636323517009265629279126603868678225317/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^8 + 26413769683471826293439382883572291661879769303595146484822525530592730432809650022939410086617056202879182241552583581260055943055233414431946279872635888687711283311/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^7 - 3561992425214324278984894593743474275713763520957522288678893833767033210812779687957553718735919382587411208965860586642630287028912596976254966086033141700911550361/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^6 + 27550713527983907902559260929023027758197039093079624330382831738542638563812646620194614236796324305535025150043980696137021651364588520041417383705970246431439004735/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^5 - 1206064074806993905382745932871678941395408982539302129851914499797082683772615005526903647693880465093682535326954703984758036346743205593070784512965991987766454975/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^4 - 2681729624626971073820045771207279670573453309975330257643196885916526525421587842279808372937861400300653687915538391376673831300675582511456846614740786565179523089/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^3 - 18324530822037172081424289693480663878931111316002039260581921506988811769954934789665405608338413290860296448506762573951768947737520981570583680877079406617470341/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^2 + 33034640327401024105191173025678868045891915435641399317628517336880625040924623002166472942683796965322341701439294664565206903864706811177764410848912500829519057/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y + 8053049780529709347201244325860755768596627532215230330287791040002281432742512082256366760158089967662473585077777121561148780148089723734714169944433802308692769/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096

359906457049013394859267367918018872469302397068862591355597648973001866025157209707050953739879708013957160836457500339765210394050460549438678670774614087066167/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^36 - 5181659779890744825409223720995289497494906331315680139717361134715011132386393405914207925320235581813562776828722473747671349386271381641984316438044720636763953/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^35 - 5388204118890155854945680104337092145211230135370746830926514222229484887089823266759725085941552100128623660556058912204789686845301947117483483200721545426370539/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^34 + 25925804457667743117689847462115946849321368895020899610506959846112942798950485018437630203299763509607705334674682611400401265230324095336295236200703716455407510/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 + 428425312903647497814981167656264027391292385289883531191491052477450053751788465838868414307674950464687159630420512921774019900035858861627472422305396878512780319/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^32 - 1505977282369777162521628938899864710484720261424938665946401635484487964744636548499817074270912583795628503751929190821138703786587883980484942655141072137233115359/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^31 - 6851361429429693070287192524036605822544143727636985219358140575220654733063731903173971546794455106760129790539335288068519806685971706846682937302038834544391280943/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^30 - 34311280657150935927282345977930744531790471070704407106149102255839262577584587213993191422996279654246608490669341576089481540301047833273299503796076704366509180691/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^29 + 349991296931777646455539453873258513171186806258916902890043625625161411991501853281126330758399148109982141182318517481662699633231149749735552067572217405165920735545/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^28 + 589340768029305529473926017109222406300297120444786696226512794250401003774677999133547609510012368070017111074374004102154325690517369658860587478382036568624975876847/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^27 - 3071738328302654750709497858884010120401090947766209392818725202069656887799990296561240535302007825766254452234065970088463833262685108856506305741770622504086486761/13628499085818021065026436819598035620478470384624496897308893246715365051891909305647198591732259308339333273108365617182748133490923948842682071969513376276496*y^26 - 3373408045116981868966838290497333838399433704697372101963269855355098609056544444429258027910456922356466178791738335722863763917030166256994343153237431262360225998719/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^25 - 266323554256855060898879882987363691028302143164731071196352272356039501701110484927809477528576762921404983256271362659185887773349707897492449988972905123644651985109/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 + 3867959320529432107570439543303990301167458459301221889254900780810188952219962744216372242298549550249337242593542306928429661959869165688979641648706076918405001086977/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^23 + 5308413404593290160231758170915089153008067622060646920621297249053999863376625551204625152595812684312426431832861905297725997456160721314523758244012965546654953656659/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^22 + 9341204464933846731438622480515540497338015434563248430360142733388630199433511733010130590581858984103150362904794505039900077304474256276143769881367133482931483864883/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^21 + 13469881774202838201650754547940104888458242686467133162774282349225261718982518331177963201735591115976488606383658387953492221637476023833314616727844672726457456383079/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^20 - 10798893919305592048468883427400999982214786399256503134667724316706384634830772459197018256029623674943472548895772310017355745348601196051991293130724874576835894364609/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^19 - 25208093456957949301200375154614380138498872738205203031043168168446893894610393342007304623676208205289205476335398053588557552404744524908020779910228587784383873841929/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^18 + 15441642895955863780226036543645620206403817105137118529223740066729647050685198275371949514434796709481573798481611124904306641544975116494063074242416941340410264875603/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^17 + 19422538838360770052807331770136305071326898653630670324969483404300979863195665041925088568516564699614423376624588360511432290442114489171343049181024607822961703361699/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^16 - 2815242375146071868865756836654206008278041941379810822152394332337453914004311709223158297255628276254515423223280281156264208360419594117752168292710144473485113042203/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^15 - 9999083901516840930263078782291437041396641849204820595146764840265203958540146386280328809518721222830236473349362227051392197216160697100871373511420589973824949617141/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^14 - 1676853028823763215828698311856498052757928241196097242183159608812483590008318208644653148233665820982030183211687735574781822256265443353420023330810766355290941661591/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^13 + 258155805605713832304640995883104985970996053480869518286571881287599249923131865265702254920338941350767150741496568494911559758384408419596529585918890849307403887152/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 + 2526246066727222691583902885671072883431115910345205837759253062426822586671326453448532247065105477753942837275168745474366474446964521684981473169345519684872998533453/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^11 - 149176575954320093888449908133747622686211065391611469389042668901309174076705644286755814595593364264517467965384295129800986545235488377362917973782611866129755710497/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^10 - 626490007570445189467016184275058471400204458755007556986161187500679251649101175657874181725405967166884005680167964350775620156287592903264280477427256966250712874921/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^9 + 83742585260909528629040234135277086073066800725627708406343661219535797295877400081354085151738561730435649293474093664323801893745054601721384810550955418217620244269/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^8 + 9174333173698404586559476246739353220309160993331547405990536068293711852809795784928001690605799650354403577597492282537517701335664267445368304581511397286669679863/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^7 - 2193118892497618673943501704820913436884705065410212232094578420189756244929636815516824454362130417354476202315966148564686029732406569581977544390711932745930185865/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^6 + 6146830907990949821381724652318631757509581153664082717397427871492181198125872362140594332379498350472102044755851901891302641197991515714433201296816911817175710007/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^5 - 176681680588069926550118599404139886789811955716354451603960356465863338306751049412575436019345457041279296083344840792965978290791860196879328503502424874269331823/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y^4 - 739164876649765229875312019634568840568355872459844762868637881312239717124415487933263349066904208045495521939544571205917510499762310733540823961878205769118669897/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096*y^3 - 3325426497682362534302895770329483447927886441813454837949001177902044983533355072954889775631030512251137579346092306927521627769669760156699124172271223728559149/344119601916905031891917529694850399417081377211768546657049554479562967560270709967591764441239547535568165145986231833864390370645829708277722317230212750981524*y^2 + 10459903504967849783866184274696877390441016833807725560221656283744192422310672890543447805905920968613383132673589072947571242015915697454032310698824120281096721/688239203833810063783835059389700798834162754423537093314099108959125935120541419935183528882479095071136330291972463667728780741291659416555444634460425501963048*y + 1878667336225903854445432820316306101801639986523622213022774022169331607531960804697690825843533433709343385213766167990293073115672053034883184553207441702023801/1376478407667620127567670118779401597668325508847074186628198217918251870241082839870367057764958190142272660583944927335457561482583318833110889268920851003926096

985318671846386719329267532665574356718617500781409623933958427666363451325742628853980438802944992013203574388018631539451665888522150419076778002627593828978631/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^36 - 14121052010144074102580048809740768665542952692682383589699557635957811933280193909401132981555581569203919994059733592049212263323218417870448110226822728755326197/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^35 - 16642643050064710922993338222055933874389828400253683997288345665598804499784391412096976754410105808316064688743909532759193158150110442988594580764728105346674208/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^34 + 566614393084396390504213635496643992332385122783945095674152767599945060606687373502705968560912057073394130272074859003493781452843427599426320833074820802876328534/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^33 + 1322677217140348440799074282388372680088514360696098708508121883794597734414625161996026039162906812348910121125653248069161741706344235652156834226626507084810452431/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^32 - 4074868929049543280420639558140763192753120860738785519314694456713089107571406695931106984298826919879830640376586038888288782353489904607037757773169193286834344223/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^31 - 38063697724444493874054612673517490701685772933367258434191857443468129114769333406618365656123873633660179693813438329445010055913567550789157270060789371153725010055/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^30 - 103358288113023769389324474818168739889844108172449577746351925790167816808799635252259547275476486156682702919968723575440192235610912351301492543713982978195861508463/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^29 + 949277617177943126245398112627312820750369597334678029265224486883112272851136402463074392868807320565466342804121266108025626426949798804885490053481840942191157929741/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^28 + 1741426224908398002070627210274000080230500088393568002392224295770377252140471479872604874713377300996490671307663250448133813231883179695798421843888805894136986934979/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^27 - 688260247482037630969022564407582151744906381850618196733909401565043944992004011009858913713365001653104555100102269270443125604125914580841673048581819851120175805887/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^26 - 3130082075671439525070129332402118128375084819654723435007904471191661963226911490824241537996119885152124259550820453836175573256905442878542902610096501295850234241883/516179402875357547837876294542275599125622065817652819985574331719344451340406064951387646661859321303352247718979347750796585555968744562416583475845319126472286*y^25 - 710467308975978541228843733559141525162191978062495440468888129796365371685186333912308783322493010986042962386762277632402659368220148938888763448981034293790291912858/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 + 1052513248824081751840886345872065367889474265365994712533147903278504026134061101603045403669513328998875458535995913233793388424858864507131090593725517017275970841917/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^23 + 16173778196968278390695951279843325163829637102329055841448340764932740976517892029610133164837905033678913560120100511635649227901956199350004216871481918573781403623841/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^22 + 8870488736427353795712989370369287774968571674164298181221341649017205117898162586806286266765665199420752699083628745386809203301778869613804896356551521377116404179465/516179402875357547837876294542275599125622065817652819985574331719344451340406064951387646661859321303352247718979347750796585555968744562416583475845319126472286*y^21 + 40023831903332479032169102374069042094112705836463619100347390309391603481455859186754718303353126509762620681234275771513187458533832779641719778653169808570682318138433/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^20 - 27605103758182274580546836774067044699990512706302958812012567073565512179899929075298724322780465647516401007597782159554229934214562320284170496461982766716487057083706/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^19 - 77760350123132985616656293906892911352765926477129365379305575887916624726025715965015687630588519901294081940144086299619990288991049632386033057657489943287607804906665/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^18 + 37347400401421228998616827153672701339027718263164375982701746923597703479494374358117658089282630243815178599535364509918505177167144687202707335886780787566832056518497/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^17 + 6616143128851665153822937353020151838931602569059092850742925378959987555592278426052844420507122372671670038949045886983996504175293377828561601503024568816926617194139/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^16 - 4520982547094724957763191244940196838507292784916874452634023631588770724365550416527215404245605048904878080434619829563255287438083149924489345298328103217402475571517/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^15 - 28932605263759616492156189741562939770261272034707784542785115378758328753367580513497186460267955216483712077893309244547034847102315563350377505139264446357713520525515/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^14 - 1868858895574367002172671291408335210438017353387432249998970156985614599580926532090556762385683020800401427409577743166229030214958099066498589536705523269368398598976/258089701437678773918938147271137799562811032908826409992787165859672225670203032475693823330929660651676123859489673875398292777984372281208291737922659563236143*y^13 + 5412332511008267006086706515148812884030007817449867913518962114634836347257559184929463979157726744437465017065821965962018121416945860278260036692348197721173946995970/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^12 + 8128218613333165547282819234679259919474750523895753786329841357210745506571338183998497289570735053945183697925386409836745139052232968430534009741473345288157396240619/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^11 - 1512911113282280100410669447039467168493667130322530813840398861090645314511037445206653970849161659185828036048026327957759527950718472240128256154878043807621275047644/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^10 - 2061738764628560998674375239660439151727416776806717932495448142665269237182207056279010036874699218338784293668198853051724003389379275308177763857882265333036659222343/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^9 + 81971342725037921924359221867781610983958890387400274716855812053203294840920552029772524919237303455379765074818664753704350070268069032316105420965087010933492842987/258089701437678773918938147271137799562811032908826409992787165859672225670203032475693823330929660651676123859489673875398292777984372281208291737922659563236143*y^8 + 5672627405888907880311714013996387070061279028945441923256826295842165868492890855599111424564533988575344734446199486629585746748861143934236815790358466138140830267/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^7 - 12134235862679129684687127991059360198621339277941258703794142635934757137856678822676519608671238735967865421419478049677700754590313616220694042397595356577601987540/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^6 + 25367548731032526705428179026881507527444341216948862703279362486276093653038046081510069747859858128483322563865303566561993577921658693993132574589116342742536438311/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^5 - 990137742272098013101064004207444246301360153926408721869377709142043579326916144629345577918675988347086242652519005606796427122051986399544963131071435911663801733/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^4 - 1830008924008844912099610636324177930233308173984840855724114764230292245495281183300473239046476169755764218889628059654918958232652903295339872149123173748091599707/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858*y^3 - 25723307362313406263403714286171890642502103786851428462031351365126142594489006672050284218936437519581209461301236448583555139163337168900683290794271477555941167/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y^2 + 23542213806209312774127340260837720104488548653600200199522158360197958821228975586245128279364118754502034615533628820747517588420331031881249817012983009343300891/774269104313036321756814441813413398688433098726479229978361497579016677010609097427081469992788981955028371578469021626194878333953116843624875213767978689708429*y + 2566323562549470521817410281428482589455671059392933608461601586318923880792916968303283672420431152883506416122732711115634691204238598597266966259734237452271061/1548538208626072643513628883626826797376866197452958459956722995158033354021218194854162939985577963910056743156938043252389756667906233687249750427535957379416858

-61245889236048118036647429564671195672053102478015700609010484983609182718627444848163455518546299128640634466229050990210037246685680754921413830442432305098405/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^36 + 1766979464920062738107034146386358095084651117035796897918014362502778392496878301851576237979852238412518943197819984610096468173088196726579977107925847647831101/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^35 + 1732157388295780717168409840953035465160913255723747552940314077075808701084951093992781413452668055096951609687103501392801419647579869779081760887231881998666751/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^34 - 70612826920208793191523256542549888564896053040474282924723245272120336133955257600022517466402611628399727481705298749274937872095349580990126085850113290353137453/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 - 68873430078654429559527951886625643679208528430330226470477248208558291502833857074907819962368683709227208068744708227447247200462158785663431587902644437752634169/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^32 + 513465755092736954016118119424589236382560375515369467004360131524697517390570271989844715127664990031177041349035506407743283065986223752631328980474370126842162891/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^31 + 4632002066051852156206281902134250800445570464368874661968179119768100393014849707037966924618086493768455530335085761361329119726042846947111833404288277335033240563/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^30 + 5600441856503621779532355010241803064889468936692005622918633515854005011527062789436202232949077744113076693794980316820438186768212089464174915249140916687677804525/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^29 - 59679957770222093304051542185441360645019378208111015515792185444447328155063236914542508412210833108332860671338252702556444308256217393478027800053273178000508464894/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^28 - 96710808106117327770899192294791680419947462635450602017558694811726189247272277770279826113744786472031175921733039945775022778454322019778503796768900164477038626364/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^27 + 55726128605778947116081634217827183574183094485521691510331182379422825858841643795725296175857079126293593618101074896188890829886064597801141241795037888741542474453/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^26 + 566940986585088811518611611125006779281172390806603451417885316092085386242511665592606141308362343744382215153166155521705389849880023242159224282492792790224232528052/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^25 + 695737296615316312239798862613854237518752696995180402985422757263223074889750206873531622775547416190865315609447645572717310152810695883664158863160539844636558093744/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 - 673658939634641967107362294417766078878236869986878451675821431100581118172577188288226844014632499664491389717785543434266457104022261813571757712037044482626809689376/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^23 - 836984306212289763326016696622211976207633935315799684545730962557703603524998417748898451748629701161670149415494640418415026809067625260617624752517307110103572259546/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^22 - 1571323325231631729992233480906541005352386733940987216302887294311329408859766913763502356306475641431757654692157264527259722222941128619382349765461115633344315004891/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^21 - 2238260495822756092209025319912912382521878231216410144487438502597584474768853334629059237639226750197908201157212172340717553167045305694689913210764612682332400032161/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^20 + 3736463853660076933464878259232706149838425721446700981646623102623004237810060038150274415315768020518658327860165851445721699646091770581362754001091255071968622130909/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^19 + 3987294785799919844598708403719434365619980608723042513759752809037047688931322917640803103040401969546387972759097794312407156685050764789362243638839058454674436763466/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^18 - 2693880767839887074931587530562655696190841732654918372461074732293310882281596195609713106861059536725298279239784917940748553416612010054470972548676352045367586077989/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^17 - 2990850745822065867905570071948198375737166838725358316723738378317153579330975805938859124808162727858597544287489376160270581337798542002016903334783736718975713996738/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^16 + 529499048325545264717018034806275886102542022052544239787925258129743078816977258490298415076009335235802658716332385625557728070111702379114658993105914491111245887521/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^15 + 1551581784187245267618229401068590711839223120102223113530246922627491644755797200188740314991507571915215116921987363410250786386077168445046411444454657841912879920583/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^14 + 509949353473989977876545404430179582640663044344067040509095551473695949522750968411090671827876614003728318916930492233079501186451760500878285837144027581576034931016/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^13 - 668920712358066954523515367326037257119695933999035325039774017192976043072064421584129521935944794845114065626512866644990465183236859883321966051752184413959795026185/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 - 373458669155698165467739826108015864395216424498169779086629012717889573030308686889868637700686631687742042547490474322200760943521566877305038130306044115365243100026/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^11 + 196052425993100991794871789489587147994340624150233400158555617530692835130493988630737691708738329304092595005315192914392032800851529365298358729884606484237231900776/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^10 + 81212487504043299522211154520472769873489632526719916110289157823464089411483069620241300128663628831088214010843832670201861198807709822404847183867519205221828377167/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^9 - 24326431144469744950848970604043178361805860753522688426819783612469607031938990602433936590739512464185754324567838518913951806780943293154118478321142531801716936368/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^8 - 2050054257024488894756760152373500200110875852112949791002203244325909462896686003279327778019483399927673180102109056904131861210079811808266526680162148851611002134/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^7 - 325122634695721179105735167323741462147369618373534632126772190110781717629091429140525215784243290013002108088503924203349545695130427606859511544610547731360137043/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^6 - 993947531206568492362221207705206242922517976741853641394639936260090924904684389460093850263464180291824514205737079600423293880207152881525394945492405853302323379/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^5 + 112475741498825831467797756619058463883521210452864792838657416523600728955705131977178028786348911203057650783782775371243118042729208714372527806222259673553368893/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^4 + 76404413247981820096987576332646230737375330758057085255787870487767990643413271271964485008627267604929548493890033108536971025350768923464163530606766040996749048/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^3 + 5150550447882074296641248326753803100585383188290198870078381961743040739329232559556577770080879791427854988408402523061017736096259796888315976114066853436581606/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^2 - 1860816362715485634897291010739088658134997536867304697215540925122099514136298483299127405375089134430259616649289280067110398992522424923854719763294071169236536/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y - 125017849796534897037653772187317922370849660416579593829982591976017655292754988787559977723318781037831279300240230798107865407001427413994184668595069164325517/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381

321726779826022106143310517001178741235858633824593966689658744435907425719356440443266120831572878381086218171496400136445300727505009361524272553191741771761168/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^36 - 9281253807097443415489367142837586446559075782188997825580458749997040795989929664012956621596485365238076810717750813068348246328963673684555017840789450282138839/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^35 - 9121208059185026433437366487432133959754052386374634682581397833004045498260229069822971637885787067573776097426295224530464182086589609542616961864822227071955698/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^34 + 370924295819510040317695975965297945293778215297084626984470600071120736352178777969909142577345102933458924559718834723374396610599086578574692975047612390544089679/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 + 362663728891861049561887067363968115092700469351258521694010025648859558065147875895729070540262443086766007090776067070517839361599461094704900915099460371719971198/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^32 - 2696961289720034196142378051043769292822059955958889163730730297452146455520176407617719490124033855603811456173029585519327998991438477298271753382704607463113159720/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^31 - 24338510615114701982697140465241050922730740775742264061421781363503686124754992728424571726601619692830940837951659235395728349970430685054089665462354853633290718172/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^30 - 29471750850260411388074071745946848214186637830959252941377515966548967713815029138170316271531916293999840938829553827235390826804098653688434417128460322466228434644/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^29 + 313465094083110010587650026029564458262897364536488444696244332462499328191837828445448839769977626424164055497736511621648520804829675280662070383660069437834894493038/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^28 + 508774630884207390506614097192946359222416918508112307375458540107119335036967899668896907797351077937411791767946319288157279860185054814844691364105776793409132413202/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^27 - 2891443154595128716368757336277858633571944330790444047505268478394389523866532079075521634086404549067213582837117194994913566371788858427810751004461521332810490172/851781192863626316564152301224877226279904399039031056081805827919710315743244331602949911983266206771208329569272851073921758343182746802667629498094586017281*y^26 - 2979268301914738579990952098785114959792565946387930445017302541144823288700356989884299270095339365371658661275128792952757493940202611203599608624516210117632038157416/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^25 - 3660718146844542082715339231220162189210035763098696885170070261308128409706250162056785283898242140920201051465439681488751954261854037417129508988134671100186747691522/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 + 3534321075408498136771429920643124331404808095885052819903245716196587677460086469712805164769400765610383767211433170050824621025397381828013041774666239792328754841208/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^23 + 4407273652201018983000997082992780708773130965022980862430673503969965324295385764241170923705359822388059966063749255712716797593348670989563979643924385560594229413972/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^22 + 8255405290748022559935323705753653543539212668558637468477168088756024239031122463242433359045207378680472847634788554341724881429595273500181184223717264084383899032813/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^21 + 11773778910168277956336001379421128035990202130096727696785991264314264259710735035784127703588279450198471673141896095571045179240861761475291862136306564166718814195712/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^20 - 19607948952932153056725208742184476337090867824316085758061341604738566871158229723602502757451562171999353525149463940482689340719008174428543613454487644590148017029570/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^19 - 20999630189381934622129887744271577758873918628023643313696574375335750551729599427277430982849709659608362643474684704780577617570526688757276217570715101614064256210300/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^18 + 14143581984770903901785609998025705820265494333183162642935050806088398447310931715659742471808204775224173845028335749741262921204248059467434234377422857581545003855397/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^17 + 15755694750814350116289814937949083540602538445937627615743370608061592850614034697384912297859661987056166934197353841630338668199263883263893676445041687863315689039270/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^16 - 2787261012157234935697919678822494247434989132747912743723127813173968375506329915962076544172248226669437919645331124411139834626617331583735947791214455634854918206233/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^15 - 8167204075716634978971962959671770133959402607222013232192697593977488692392882268892082825539570152566031032906135427577883276283672679250352549002475690681158826825461/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^14 - 2678199199668447904928079681049631626421297727455767769272696044797454569176002401716234123839137719882289608994167791171083957992061284427885064185966216624361969758406/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^13 + 3517644211296155177637120810582239823816544101956391852385565773799071066602614245267472006435867489613260478709293089437338763938925810643547342172506851099952278961685/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 + 1966355467839702024333527927005889984271725458448847642521698561457332943963817335921041215848258784060966403006356918858829368522752393703544511112844056716560504904342/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^11 - 1033371228678204544313528924776325736884296516199409673362755511138421564261570871293102323158580906244380897417577876598740059722825350236157195656847164403564845552026/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^10 - 428793266087003002262696841919794194554610862524384193882128245435423722601844175764495384623360998206332692821713005996292405603080650755529705494473498523242746305517/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^9 + 130217413821397340499051562023777390766624196748098690167682996312873416991879411636672357021055871921820686246621571319279255424961963840318025854967371959892169878637/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^8 + 10814550203008810693201115585989864031798193060617562817801978861844983065619797198043804551311561532827672001604559078651401893755010095233487748737075281389241019678/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^7 + 1193530307201384491924590125036948917545273345034170401971613723695962457980687573171824560646594824528008797101774170108420373550358182179070024864185906822509005763/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^6 + 5319973599935663308807923266127754892178977531785627146761035229017595857126029871912331482143238686224611757637970033382580834003115156496912925444254263906963982439/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^5 - 593581004090410854613096108024531526433572099977662118310941040887023398179351901077304016069942570599001406032939500211305937963289330423278549804089153346314092143/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^4 - 409137960856974794097421942980443359345139524437273132567648896984101498305415222709281005093843069833099445808958251316298058898994181961979190738461190964147455759/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^3 - 21007671048130493194961637634698401585590547335700379485820632088273780945105158075137737815660411987335464840237624560911343308891245520694594727228628106796248923/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^2 + 9134216519755937551021333905393903401700258845141658387890872085563434567568599888947574471044277868576122094877741234005377780274792728424344578526529643930548596/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y + 807515833861333402667432972374267139712856242878247459993536977842230816278307391835428963167776888692490965131096177267646373871308314798772534168391532814370040/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381

-616352486006678730907292259489029313500000369907383247291003691566796447682382453912334459463193760226039589003738853145010169465136154281972295682330722822924767/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^36 + 17782429955336896612201157818803635347570415188098501888081893865620423735805615352103712071234145183998237479709056351834690367036112648068886214570108277747837422/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^35 + 17423580280729444511594219411137941384843517329333227176923718450105783746519122463473155384034274067715326327012974865396226805046679175471565534339528805858783436/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^34 - 710644533420446879970254920089352059833268531031084993839548596546964897726378344593911430982324554620809570087392218830342946747947231690682822345039630115532796646/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 - 692764926907416417354287244457815975253433966036171695369519447427692768311392861811487837110386020863215482049439699416674610226323640742137786132871852661874713964/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^32 + 5168379101072737203861601271435272604017931931845660755339780638205285327282589882093471670396399039760310102900211321479949468492041851693742787760750859970001134143/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^31 + 46612001523385858070318139583974500385644299208095090178274579113352378172639172526427138839034840489247766327361010130269096297593235360964720940643370251752103496858/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^30 + 56331629308499815564810491888801429255865791362432507393099561644215869552362442821180601051607536543007579882785239017552626689414674128645478076051610237971317456470/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^29 - 600663918084153366018550998819650351584915083419983679938518087711076814200328455275091984671253818931237967664048769277664016776330735385917333798589813222451946982683/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^28 - 972975115859767452509572322079617618185214248652033638769765633756531773808919750621287156332672223629574618042717674986775420771003947533066386073552902296149051236526/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^27 + 561946434959958332993949928450011114632002779329724892525269227189732320095543395751357420911824655805103254242999444337896001046396381134169697178817760617683813615440/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^26 + 5705614385007070757632005741776448158657073209722162154959549326970305945467583783914515035298099129931685016002732680097771668088416950785597950668759350129415967113028/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^25 + 6997303054634497616617397155366415948279667536984853752152329102590220221473366721505421803265077564669201024092624830914071220046959449895992412759342029054967901819587/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 - 6788196089783148438272751163182305639489504174571960977465971700871237036558542901932295579371124465874382400577232401701354041801864963229739965372357415015198973849151/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^23 - 8421568831844607218821779373758412888407301101349354900240390638682276332279489742274393760917170979261194299604042139207534594307690219271530168420023449536229551995779/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^22 - 15795346720359990360529955486680095002028773748859619906830329592125174923998283815571168203059720094508404565433763375241597605100708490435535788002606148621117540492128/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^21 - 22514307196732746424023345439612791082966324549619764602877827233984700924366753972520294708360377899418062031213000337791195461119059453651697142386157791953648433544386/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^20 + 37621444049024715383435068674020111388083142407617254618464142065195283833884309286230141485622405590618517221771798871050392010117603384789461173493871227223785817418825/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^19 + 40115698570986955974484372309500163643111668739798968042357437924301692246988872093157025751910805446395967050814775947298116044620112210052246862761890458313681702462346/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^18 - 27189930251717763553772401513528293216367389683989318722777525218556945707868931841561459059789911892349173252112161648908891099614176861894203803329411567680695296775906/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^17 - 30093080905424079445455485127232611103532278407802501890918724324564902919679977941235331367255562135215962456036530371775102628803322974354675857429148755104874730914211/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^16 + 5409151003251159557476055406296490200270900639512857483980956393639523216949949931135632394148420805142572536591508009626946345253189128707701320855792858987277765319720/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^15 + 15620172634838268171992199858959306984447558187983632674773879558941281353870977351789222941555448262501241111557139217335250543110051013327667281598788930216773876820240/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^14 + 5091429239785455821451653855495523345918095083990252618181101442047668759458356250793007431287682452656514479816732447444682650467401654606712575575144649664253315626462/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^13 - 6746835584487696779464208351678249951814551588992733003408278708615007977523622652259746645989859567309393453526282775435148442722486225893058764834136511109400672244565/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 - 3746951254632736522262187925246236371131955318230154924080870306217407959294484807048170810401724686359270432773264634206313045386489616432671095981947855529091556400833/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^11 + 1986847897576949851595863328641901338740920088471774907057068213189600425055459952183343313084590446229942410965336289077202393640327799780964274536438373931885355939983/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^10 + 814733510904219903815556502148922918910742768971055284451883484942858275610183033368639376363571723661578125843869033167373672773616206925305734294980687550553155816066/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^9 - 250630026990731216200271276422421178438322831069269509512709611782038044970280416762850872626383840392405124772919343389198467642909644173269891778979471502253595282837/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^8 - 19809995179630824369922207245537823886835863032273900591820869873457929365245590680342685704541569263049953341001431071223744283269500440509649668095631402433321742114/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^7 - 2375844821458003948605431794454337353675033913849393381747898304710789986857481191123541043266302957606416558661504678070798454692773440001156578078915759814656300986/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^6 - 10176293543757113912717356583439907935664529065242478935524612187704804102307121584752477257298532176726782438554697542534111304361486326062650855506582441254594983613/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^5 + 1162419456188233789541721237153752051540699833368872059392636313264561292059205015249214619094153227872930218976817317089953081964314290069764429254389017865538324755/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^4 + 776299128142044659753231095398032563621256437052164807975096500044379274626738004258774705889418393204740774523881202550702772670911099488288218204735692888356969892/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^3 + 39251186133751485749632647564317987560844913360356865569380154203188366226346581246413603732813168449247706688155096510065267797604902390065730633369293390338589085/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^2 - 17187712128447343433278733777340841463345774441947523674141767331594350077150200600057109565527519576295119651897338616603078195581579138602873044565086917393846153/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y - 1358886793586571617154130364953316952974839306060959281021560386659464277270726199272204248011267879331903995118371576046666153499895767327534391506798539444221029/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381


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

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

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

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

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

# 1 Loop Invariant
-17354353301971223984842793473316601362363980769673265755043195578631048087446238250446035414733858428280985104900015716654076058348209223498224590239943017942373081/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^36 + 249751073499055000846851349618810568557491785236986380685605284989140798018298316177359068727040846173463021212695711673648342890143206658933906807545040110857436489/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^35 + 262605030521147685929953660929066216659229058196335144006176542424500124633724271656718345761397943325434016155800967473262606933280368205952001975456753038050313747/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^34 - 9992208954955833209244183055155255621541512445537588378581835203463642077508953695359803858009125932021361230837892653172870870446619872073476325132398650489989702382/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^33 - 20885239376176383518411365632130578107098382676224506385793567583099230587975987746359670724201708613462718071293521716631307712831469726643870980506801520769273583769/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^32 + 72268407051232765990711407065685654649203806401008331419471392025264832826343944827786533737266755024299084821105837180723506884384610166792686177669033442719909050306/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^31 + 661359757548531525574752352150382163446935288246534684414039577988729792382517042034486355136678593830231207907613996726823806213388748388988722429931720347454252217728/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^30 + 1673473910271266362795271188086133272981998651916666007301547739531212587983954274892569730706933408853318391349022788625560160648654477457579019155542219355226555694967/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^29 - 16826609654447505953676293764135200005683305462861874637878002988089078864881423175643428927977112355443455895586146956180967726814144618594465823203126207865588194495827/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^28 - 28580463924408899992871161525531885884907263303190096766074087016382675441088650782458755378012730650523691680444714715665275742903023761209937498498746489625721794787939/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^27 + 14243593773282494338630846679885972772055292445196966582603269248086100607902954170388593176741429307917985864564202573242675064244682198432928158673587340218851110331853/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^26 + 162191172321995451780443203652221660509956238079618876847646640190472855995312606389450745639463950688501228879143056812194396402006202715020260099076635068822157636686483/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^25 + 103848240601344124509840984719172199410405728647985596074996666470692879781940566740454082618993374601417835739483692683409031085894012730732088972767619912038029369967367/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^24 - 180454639420358488289112389495573228004647260527932153489860324211195032756461464419822331304531221597375556116181193797162963286865146953983296896403886080824597698170707/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^23 - 253438108997517158045263820610566856922213458465845651437620413218790759086125684583843157655097079991596135874031824668453094588002355335779090273899350299174756796108177/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^22 - 457177547677855772054114374985956204617758912275103994441317347575569896910786362820121701521482184529332684853458507732628426446054751763524275432284150467292169727502197/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^21 - 660155607923151337289726213849109997460922971706768512310572909783916736889741514682001566096030840999570443875078008474141364612350205917710624513887813738075150819400121/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^20 + 511638021200146233995346263149119444075619273907933405937234834828885618483996086208023740809743525920081415445224377383751893036309123562252627010316317653072388608703549/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^19 + 1212216872001531090146829346102249141360681525853135478608807837591819308423824929030553536826899291039102170414610985173322627064989586339562048507263750908042906572742111/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^18 - 708333810962976275672932387509168607191707552591555927563918908772303366994162756453721204140191179478789099954680347482850051507053530510815562999025354443591675448619949/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^17 - 919311249427840807851173646714682882067870593421700193533270880360611281620062777738167229959507006430995121453669596874862242252657525593666565867040208875902792482203079/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^16 + 109628236327307171179210007119375398234320861594524964238940138510370488354065833616849658821482562472599188256200519378931546944150592848052881071361349629540918998510657/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^15 + 465771010233528647243069741514115090380958883546152139867979919362361134905670937885411618030621827943891635718313729174164712949717193274027562762988522943998274777612131/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^14 + 84963543648465077328871528582551841002545356070492308829231330046147851805725094336695516291652578482093539520252077480753698919807106325053374846547277710883781279503996/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^13 - 94289778413187624477330068474636520719957256317118785158485524062509571296351793441548747350730538101772331786614865061311872497789105222780776567587669784868533174989924/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^12 - 120900779853742931520053190871281335749493232713779484617183548370574831740487278353206517656359636115030946934240151871595511087784675392894796211026810380829341640509809/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^11 + 26242304734076158388790031975252106955337257637119957506044295246493999082233848970602800979278133798242875050541448238029392615943195665442000556294061375006791648414568/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^10 + 28732900534911444621421419079432149525258747544641518744922709325103069899172403494472170682771217666545248235295359468255890429734228936112689103650965733165314045990161/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^9 - 3295039212608790434429243762154701104507418082701171935424712475666552556674530571903526010699798649130958641886177911755289489746512035591376892006980801897845923703610/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^8 - 752744225074303245420815476802208583571847440903893617673854327552368714723877049258996380668575283069646342398186914181078422103653880349462735701362348035031062807798/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^7 + 10484054217019943960792219288401819404090057249641973165760693909811809453726842102723790903800162906390916668469153676451596509193186039674605559948008790208712253971/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^6 - 275628514937814626988667590099071302247373297247660255257360869737641535665322086247210978940535540042090792916744775595155737050645740822687442392023977748891134323029/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^5 + 8347603032662150451581135841352594154925311481845836620341967418483727846085907573216848975469713708795506525769107969486864696655760166833558851077304835603032495710/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^4 + 30312266373937314334382770572332974424237630524493740296195132631547986751059420764697933117994274934367926282741582289335498983586150418484855176214210009172912605653/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762*y^3 + 1013389711024978897238809736787648216459959525496657897486057528283750331891826596927581888112807622703676601306844418707127191389403153510923401681771421403977536553/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y^2 - 437102069396164242894628187083895490849197025062537033682599148958301423604722747674429703893481321881626096427090773802585862500160582645432578718956177241563596653/86029900479226257972979382423712599854270344302942136664262388619890741890067677491897941110309886883892041286496557958466097592661457427069430579307553187745381*y - 108072122349683505223672682879978370329590186299929915295512982840484313063149029298697467914129071544694477977887901115604050927543837065161536807923452426284502455/172059800958452515945958764847425199708540688605884273328524777239781483780135354983795882220619773767784082572993115916932195185322914854138861158615106375490762

# 2 Loop Invariant
-1158835786717633351328977371504326296684498498866834286890192687049972978672207361239568536763759021957845628097357643678531216501465841211782252884641064064042705967115158303016135716378419429138578122958206024197234363460857336657455705764888894696513513078581762941844198941704232237560655/22981090546916097356690951394020489912351105059543845939477757147291762516931960684162168153913311768331627038696441060261100941631375468643928462206410684459131164972575634217249228661385343640653315463196549797492121759493705373791687356329182215844201049378970582777022198015028852413145534*y^36 + 88880890241826774130410001903490401624420200760575093188785913585460788939898965934057675927655819093802284630207570108966985882839720290596301320819239885529627182812474659159165002128594078756432176212642340525062930646747416279528908048695311578855276391127703295408700431165087220676756357/61282908125109592951175870384054639766269613492116922505274019059444700045151895157765781743768831382217672103190509494029602511017001249717142565883761825224349773260201691245997943097027583041742174568524132793312324691983214330111166283544485908917869465010588220738725861373410273101721424*y^35 + 95277564165602891549472043242045920911297240472450517238394483994386925533017886523709483619893415558845174831527466949291901749824479165039094663432072238182706579474123551900603967583093721366088881078192511160537976606230217649396059569475472028691363729333562097124098290142913034549998597/61282908125109592951175870384054639766269613492116922505274019059444700045151895157765781743768831382217672103190509494029602511017001249717142565883761825224349773260201691245997943097027583041742174568524132793312324691983214330111166283544485908917869465010588220738725861373410273101721424*y^34 - 10663086302301302379079935511316962387460443088837725182405398701536650835511149066162129343242885264225500945822204887638997374526612855215075580657827554317815085833238445233250942639009865955477924240127205921135969254470114898700026395033104945686857749769128310065914428281195664343833939013/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^33 - 473785471706694622905729515233129082285247116302949896317411312233955482856062675423551809750066191140671634900418415560130493709214189749456480392084265370782105506592361450033430049140465677063174720783251243014606638141151824604277270366359451313775224081908459898917095093111720656798191351/7660363515638699118896983798006829970783701686514615313159252382430587505643986894720722717971103922777209012898813686753700313877125156214642820735470228153043721657525211405749742887128447880217771821065516599164040586497901791263895785443060738614733683126323527592340732671676284137715178*y^32 + 25569954459136681584192188802357493470096180259638115413040476043699379750171322985012888608486219402759030882888461631079959808419886491096777408221732713278986223567008724928160271781153418168500308628769645579920777035098897707814182559204567913310433544908129823207913435630666108559649529231/61282908125109592951175870384054639766269613492116922505274019059444700045151895157765781743768831382217672103190509494029602511017001249717142565883761825224349773260201691245997943097027583041742174568524132793312324691983214330111166283544485908917869465010588220738725861373410273101721424*y^31 + 707944848136127367726410312295906815107084620076395693139650927042909233196422250393404247672515004199051214163324756556234271646217899904813414578917278636284188205254087916949179518224515989456977018138847289361030433587340924825380833077056495551703794100082776589054647110766775035604158270519/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^30 + 151756197166101648836093165572185961956978942935578599999968393729486214292561958479681092409669246799689800434183222594250055637482518413731729827476569587503602484381566971815949708773764498847065440335193150370771092538516269608334035785379577215219813466629316034042501108024150896452533576181/30641454062554796475587935192027319883134806746058461252637009529722350022575947578882890871884415691108836051595254747014801255508500624858571282941880912612174886630100845622998971548513791520871087284262066396656162345991607165055583141772242954458934732505294110369362930686705136550860712*y^29 - 8952706757998070467082877673460292635800843614190858483679664058559369358861173963556642400009132478128208229739542937875097283169710316178669727930232063474099715406779903322272503790820342770418651670148280152310920743083149587441296947724226675019068761474345881848250183871476275227493264966467/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^28 - 15432992413942946213341043165144113261870414731506219778903310379927588476786038994668000814519848589552239476934399614780645079941928559722647017555158921102493834041848894159420092040523193286858245918515079509054873847214599438560173903809816158057646233505046229560859530976818222962379011234159/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^27 + 1765670232921474363633764797066674326865631037478410764171570563822639654181079174195958692347158638560093566531236504483069363848118330075905473078607363717101659754224996111482698003303452613931249757689442198443392104370506393385545922151013737428677118027919714391891151829144767940112880744497/45962181093832194713381902788040979824702210119087691878955514294583525033863921368324336307826623536663254077392882120522201883262750937287856924412821368918262329945151268434498457322770687281306630926393099594984243518987410747583374712658364431688402098757941165554044396030057704826291068*y^26 + 28814980578738565358714080113315446268794699225542855024315671379836426232530656985189662570411015742390330053503246236529292122746962358585698408327283342757517309196084528849403882194557537019307325958016123074076427096711443196361741885946397222619658816943373724141241525094320436991839320103887/61282908125109592951175870384054639766269613492116922505274019059444700045151895157765781743768831382217672103190509494029602511017001249717142565883761825224349773260201691245997943097027583041742174568524132793312324691983214330111166283544485908917869465010588220738725861373410273101721424*y^25 + 56494875526551745993876023681173883520892693879269276453515896719983495863989363072865468787130985649861413965089913426096673439619142730889934355762894259850179843559662681685367156135051408506941083400806591891748086489880846837330491116841344808709374605496427461509217435385336856307329136792151/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136*y^24 - 91926844844473187230080460658142044936482475546582642659950260124904990621168542244162536945741750969835921819917871657540987043603587889728353750672981244407468067153366973296670340597592025483027132243484550616748105739689046353589409325030309591600765306313677402558504314848367236336690263435293/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^23 - 134864615814894691204800703456036782219043627360777680965809462745195080643230284727530286348474287110540248378899967254876698301422475124109773167113672399746411243827226654967254344197571432078235045043213750257372491161308098414675530759560669350724383613555779145596969842927027937011847477814439/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^22 - 612516986570766040252943471147145107376948101591437593487386118121346905552559244586658448521173738111104396729544823087215134395170332798498025783198337377220083965101176077145390525529807356994558676497587911755644816514757283391912470999154066773487284487304429400066165887525326455314647051191/450609618566982301111587282235695880634335393324389136068191316613563970920234523218866042233594348398659353699930216867864724345713244483214283572674719303120218921030894788573514287478143992953986577709736270539061210970464811250817399143709455212631393125077854564255337215980957890453834*y^21 - 60153641304830644406473012202970422350189326575816638974850530492698384029454126187973269322681134843134572611459544877288436765088189175918956912345388466453629465511910243134859089483134191320958981743739149039953221659985434106717750649884982109892494104130599186541107453914821995844677279987537/30641454062554796475587935192027319883134806746058461252637009529722350022575947578882890871884415691108836051595254747014801255508500624858571282941880912612174886630100845622998971548513791520871087284262066396656162345991607165055583141772242954458934732505294110369362930686705136550860712*y^20 + 177834500364825866604483438376336865617467259479764019059430974051167458037421897649935551551222592568138532719159180598274618539146615876868850166362669913116699670708754567180105922763743566615409309808943357672646053565731609356451532695386711556727534768683849219647602199462540699321619556126555/61282908125109592951175870384054639766269613492116922505274019059444700045151895157765781743768831382217672103190509494029602511017001249717142565883761825224349773260201691245997943097027583041742174568524132793312324691983214330111166283544485908917869465010588220738725861373410273101721424*y^19 + 650882749955051680769723355462841689666372720679354140834569248295544076004356747673028006606175633520658292882084580919930299452399181704580032325568724538261000899505977792010110538178570564601986111938387086674395114688443603788039053215058141732275378714197853047429482182488816922185490620207921/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^18 - 174791079589230585999944878242489022868238301525564903532781181184703149102818796645952073890563582317685044371205630785613151770889662237030204104276781193031146328861196664673024491151558319412712511301915860723862475781696554544990220049477552046504128461796344120187092495339111714866152199810855/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136*y^17 - 483946327948165758107636130270232828091938309002005411526149598725220421688758692886031877951251147509201857533648454859181994918399830294514832105653077429484019745836842412288427077166216874911616349551399746862270055977801554125434128934709999949189317964347004352520352687956074511012745143695937/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^16 + 3079100160424752602658798151679585657782111198407749401118296071433342369264108656816081210579877463833094568822215147040017797869410017875573281163606402642344561356242474356018029831420855727414232504150375761805649177795680454504584084266634465974850446613723699137166326714258355344494815159675/15320727031277398237793967596013659941567403373029230626318504764861175011287973789441445435942207845554418025797627373507400627754250312429285641470940456306087443315050422811499485774256895760435543642131033198328081172995803582527791570886121477229467366252647055184681465343352568275430356*y^15 + 59601542956126152718205297801944396045549878557478371026564998255131808158684948937483424482349479151688402304208705171078487887103398846957519533756362569650708655339715633287593884952175699701176488706449957845712951752470320404868304483362414117949503710850520800108623185393989409292204719173883/45962181093832194713381902788040979824702210119087691878955514294583525033863921368324336307826623536663254077392882120522201883262750937287856924412821368918262329945151268434498457322770687281306630926393099594984243518987410747583374712658364431688402098757941165554044396030057704826291068*y^14 + 49181316909591947599367560256242958440918089354747562090115865274943159512076496704948824720088677501427237768935934368696017110247127550931689121397427238265825764684813740058493643444442284601074014949439809265602055105729605836789676185074417110710970725719678170714485401151044449875127603921693/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136*y^13 - 92657278283748053540037159563555216688088330777528333286962281956792882897401653887393868094548161151275722773287276594887988616198627829930702665204002938555952624935081576110564990854036478986685438550790689074370786547480048694553615435969448272356999134927403885222449927943452305617916410836159/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^12 - 21586159139019659121554434535638968113802352066165660256315984776448632205262390579833439593894357819748430330232911015534523031249738971119884283269758815970547323580525863554542216785563059297379071122712602646505179972264585535783078148355384154488577163347016106421682325877587812727862844210607/61282908125109592951175870384054639766269613492116922505274019059444700045151895157765781743768831382217672103190509494029602511017001249717142565883761825224349773260201691245997943097027583041742174568524132793312324691983214330111166283544485908917869465010588220738725861373410273101721424*y^11 + 11977127482294416328419216066217868104210231610814707956962969266116321562324586991534155489658202662049684654148498883241897137511500089731254633249222350593022826717266970824336812660302679511715975493167670774624310394664685846103955093501408595580021128056502063983530167296187754737950171605847/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136*y^10 + 7233521725519276329055278193289560788764774223864142869335724623979048121106352009101552925361495735300204204659164264289046858143633349999807366255998432122539674046225893086407759633411924246611527038050055041357079783810581263937746168728451274665503050884652073410740341905929760608648933938187/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136*y^9 - 35573283147819353741823088708817633736745738595686126596751151270197812956251726146843480893801644850027486704330566325560204303023179852410905972280889650128428506033776723014735943765143650549301549462109703016541704112834106564050707489645364172954244344628016751325702932682397238987342251645/2703657711401893806669523693414175283806012359946334816409147899681383825521407139313196253401566090391956122199581301207188346074279466899285701436048315818721313526185368731441085724868863957723919466258417623234367265822788867504904394862256731275788358750467127385532023295885747342723004*y^8 - 93291911817796630274230272176405669315869603541699673448142800116933672046500150374739330414619429134667315297041537730726980554634602980843711299809664923611666694778435129301199681243634478575136992594423558737033602464492891672285469589163618876507718297890460722575949615135635256730161748885/30641454062554796475587935192027319883134806746058461252637009529722350022575947578882890871884415691108836051595254747014801255508500624858571282941880912612174886630100845622998971548513791520871087284262066396656162345991607165055583141772242954458934732505294110369362930686705136550860712*y^7 - 84708544627337516113161003164847814748294684373967980447768472060769591262566351752162248376944952645573547352302746099524331207675293682310388782168251369010549557335859766963632014253362574337540140538315380172482113252011504321669539063958643578706433226289774291398570230648865501045156203037/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^6 - 75215091895221898427673399147716295452210265021101497634465870165248129656241771009730127725566077614233559862347207957601132611382292054340864130707954796559151780395858792140523670199146949307174879196424776998506632598179659571130941481416799994386244648888889477667364727698600707994403634497/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136*y^5 + 1551381709585382002808302884078866166401400212613051213727823059595955064103400341750960259107739112252815075031189522094079147628435794161472544080184014999169993693272100501230661985319246631265305713653085415335348659821255952527296637251509724118379452193322189278426877776919353307566591861/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^4 + 11720468800444400081805768640766146368879909548859615986253364062897000038701996558042342793591608218703503011567334152164089503115709645719405618323551094071513707689626258664526476400762468448247177181647608547940745677186394237579589326700336852026265191727190122696504034975107578858115750729/183848724375328778853527611152163919298808840476350767515822057178334100135455685473297345231306494146653016309571528482088807533051003749151427697651285475673049319780605073737993829291082749125226523705572398379936974075949642990333498850633457726753608395031764662216177584120230819305164272*y^3 + 374268551237857679726645293004898676164448005659628227084290992475996885021181153181903985458504190172303018664151568923885641023146077644814065156149914867505759108907772908991346741784301814765001117721274453942146892779641379076146131006464051439860769329158045908016286682594533643906240/39759672226498438333375348432561401232441358234504923770722763230608585669432457931076415491199501329293472385287960311870416854033521572048319138765416409098842845973314246050604201836306822907704698033212023871093636262099836286836829336209657812879240569859810696846059166115966872687103*y^2 - 114800786657925911282301827128274024468776270754048203271763507882465032343391297348478089061828478733634812352019077133852707318557404895739466855199571219476347362487030654987114211806951121459695811210328715321706047437247934384334276048568530278630723610364122484099909825937584378528824285/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136*y + 20960617146429591583774562035464723859233459746943243734941707652440563097034536888935593323504330972549983488766935330961031206911708487213301614483737116313848941544833353597243611453907124961879808377351610472561537806142661452607976611523155239767372908062776324829021138503269177903362431/91924362187664389426763805576081959649404420238175383757911028589167050067727842736648672615653247073326508154785764241044403766525501874575713848825642737836524659890302536868996914645541374562613261852786199189968487037974821495166749425316728863376804197515882331108088792060115409652582136

# 3 Loop Invariant
-832396263543738527622599666380278109903458554756174202558578185472529504997965338750538115165830510720395895066325720793877130165490306351849777481963193021937633761760931384438909097127782650189764613595595280309005791811484503406974904347843513466077971245932844629813569167616534675747437170783742114243420919756866104599597056116317516586313749141492535/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^36 + 23945764837264427794532416979316408090833503031427465224670328228105235912684002929886958726694417017107849721658869252730001936029425389791692175102405426935689148431499709706776366140457941060916320464643829967253156476109787336399066238558134645231575195821362794359462300942159129889477427791038621885793053043826758127052008366954069638407099069181767335/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^35 + 12774306321499765477180520676843071086176559764718968527135489561144177959859546060780473154958114121040528690625429398028752055594126525708907578995655463562568632151426808405932429082510466796573697381098184990447976204237901827206009492903308349835945676837963720752363106745373409565600409262468920399712726344901519562339390639975063287239433262332099287/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^34 - 957912987453129886625085637631377225438878036101549864654537277712343252953879144819321275958401008240748663730376448587149288197206483173144004162484780993025606391230222795119530758462642100778077236924088237429095065392000880749269109278475003797020113717122165662753621760189117157279645239707312671105833947082344759012790328665343754770300300542215864583/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^33 - 508099515610009493067977214474731252386084140581516242480946312717003472594140467908446203370551317785784447600358933679893317704371701487995461574788861961515316240482874075947108534459920367017721470653764432664184236407761293591025457079294734156860975665131480613293628072116966767885143147941067146921849573317791085182434193833876233994405087547231278443/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^32 + 3453703162254023908404393436343188031399446256901085995317645777781925704027886880699190868162503421124465623584927919945004533367725946140999696148017949618132385447328403984376462500410531915117092304327526450583165887451976580244395884983813916017433268004917850827712404735116898030050843277686242649523019543962091985902989093258180731000613086246847944623/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^31 + 63542337090969800113500760300060228369815295130825617852688474163148592797097596742115509798765439342548069634456465832092429477160074404927143934242130158756454769262838131118661773994427762147172813090622084761774687199574851332439559321153678018666165547650676106827659276712139250035395738539243809286738111099598245434744614486332796362255519576750089216023/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^30 + 40655812061538539915173157267686284619999822886899873882042426633725916295516219117185080018887603467750973975799618613454136511150272505690421069971009794288513553173419638865674199335938685227122044051449045036068557793234392338000599978391978125689521653571670333893008435698478712101289486159862173631923020311464518209451854070838403744255870588304639910051/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^29 - 805225378453647510960479144866943845855872543336870640116286676649693583505537791721753302296676285381796312509572528837267950007379897490602255321026644817012995356973184047580288103700638006181854389792083910955828454160145546634785103066601802127798059839126981457174197257635142547993621867788796308522004182805840755380404788713048045384085423190389988652431/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^28 - 1382554842651640228593530295417572126119629986966123219970821999696089234387922318593773397505451960095436578595983083521148840217794891069277351869406692958031488288728478465291012588662956006730791487415361202365246317058820320693220664584167739857506647631379693398092050600279186457910771406713580299820533729219410551909604181972111782470217843437369781792209/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^27 + 163404875372861693324436722740122213639647164232138216412251253343774330130905414158691150039265777431495033834983385225891473775169105750925524047419463007482347305875218607202641054840505598758254697825343760149363056927379460498499776068982764769774028905128714886880949640381957651567362429824726092743803935180176281645422030008477502428676942149232644208185/12930768829943707055065803570889486255550779509233965887732927317126913410597338563853801748555996248810729763324111214912254487189926773058995064329779775904986675077018787424339364259634695658182856174715898810926467216530822631491656107046451231580018642567315961182568464606511500348823873426111900713540903639746769443783982087387792816462340757726768688*y^26 + 228769631436594632460057452767409705015503542272164580097460429920313238389101856623615463159317939884629859857067459844086442227898738099653965201892763206623255678378113462096157317758319022446525652426159925686332247805141922495766265004794325807974911551970311359838551037198244356614023140087242738620753944012201504279435859864372570214207690071642675685701/1521266921169847888831271008339939559476562295203995986792109096132578048305569242806329617477176029271850560391071907636735822022344326242234713450562326577057255891413974991098748736427611253903865432319517507167819672533037956646077189064288380185884546184390113080302172306648411805743985108954341260416576898793737581621644951457387390172040089144325728*y^25 + 10093158301520294086514547974409710989236873256083523873753114314863370571312163918461328967273172921866110400761964972503173613680300279740517697761973640600039792546644933830165507001820920283487943889863224844503912652344363841557269454103140387846569184470422476911686074823900129603392599500375723248546596128880365974399963302717673634571784719655361473700605/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^24 - 8422852843788517991610264476922460266292368385365595544623410186435373626798791693886566403348430933044634037533002599220479447996099018691480253635691520290463925511073148451953500728919477147848862569399732374425729981799192541168328478115297225469396513331149418572724238951545430916856246551768955113199165329273229192620750779983610093056352650555149553133155/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^23 - 12209275258475607052939896494883969331511849948266440147504335608077848157182144136829508177079346977300433417971809667196190871868352239411504355657490934729784556209754746673352194912463510865325403484153941709636897946175771604654552240334749027304123102104646111399368339428675694445408931316252765327827433598709447792940141704949445789846614418133018061961467/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^22 - 22244651749684797225516311253518162047864536111823091581168543484666195538725589432313689785749107140556594518868769146160739172186830606417513322268089067207778333720533136317523667146741935203489918718378215183972280342679602603681780177787217640050845636897709930950696742053763233943239978464450241586787553273244333809360334420493628765831687050533572244183521/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^21 - 2007420224165886329211789982657275080520679604899239410829475287082794999213387622213394654923900463685145855028524390522881010692535548898709893817262967173478076206872373488108701876199985478951870700065639260575881506457745770043208798206134188792153097575273318538943874719618500827786962947425417631791535115956128469880013324635493032747946367179363104417317/3232692207485926763766450892722371563887694877308491471933231829281728352649334640963450437138999062202682440831027803728063621797481693264748766082444943976246668769254696856084841064908673914545714043678974702731616804132705657872914026761612807895004660641828990295642116151627875087205968356527975178385225909936692360945995521846948204115585189431692172*y^20 + 24202523720638231571607710253652644174602211149985470430906456657478810693609324492378119069038101243217997688805187001697955898103305990053300335283495420424722319041308776068714977512551635437879203092042643084297262279186604656429595899874947290011227397492358559372759279919023120922747783547341148072735690357242546014999948081300537431355485411551958132437907/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^19 + 1832917209055806377323589633935394017020909617445003665314837768353301922460863813470694900048370503374977057116320372744418148606034738750857723927714564924766034586797166249965466842214600037928906842641014427284704062225532221283862736998933765403141446480628006549871069360570631522957682850482111757742673749147690989553842168592914759977683489582593232574753/1616346103742963381883225446361185781943847438654245735966615914640864176324667320481725218569499531101341220415513901864031810898740846632374383041222471988123334384627348428042420532454336957272857021839487351365808402066352828936457013380806403947502330320914495147821058075813937543602984178263987589192612954968346180472997760923474102057792594715846086*y^18 - 8109517551809048646756669631460722190342710630702959310064258417655952261375726005467550555590083108819959569146637066591616459369056006469720829267253984452463971537763174913800458058146112113373317705162658127469319166610854519466504263423975178320431505124903459130674169306518409294082379364763390207198081773455536532523269565018124158496334702275022535609419/12930768829943707055065803570889486255550779509233965887732927317126913410597338563853801748555996248810729763324111214912254487189926773058995064329779775904986675077018787424339364259634695658182856174715898810926467216530822631491656107046451231580018642567315961182568464606511500348823873426111900713540903639746769443783982087387792816462340757726768688*y^17 - 5511736582911860214809709318866043711730360640666386643277604520401717805160439431726703959433431920423385085825307138967991214017632012090070050123328703897743465949576952421998906946682486128996446287176018155308666607425071534756678823027871179780745979717911008230496323713351192580701947962935523982965121329758962753138409059263288379257917566150163880342733/6465384414971853527532901785444743127775389754616982943866463658563456705298669281926900874277998124405364881662055607456127243594963386529497532164889887952493337538509393712169682129817347829091428087357949405463233608265411315745828053523225615790009321283657980591284232303255750174411936713055950356770451819873384721891991043693896408231170378863384344*y^16 + 218703415557122979206011174027462778911638337962930297127388056333639077264557306733436289115113418219954992597102491302221615139760904300827569023278588813322805255541301783820659193627924913229647503201426604114089744113093724715990438631253594580210488618194226716596243773255816221445993132209911147514407799832174750456299465418406767753784350007848874438/2796446546268102736822189353566065366684857160301463211014906426714297882914649343393988267421279465573254706601235124332234966952838835004107929137063100325472896859216865792460935177256638334382105574116760123470256750979849185011171303427000698871111298133070060809378993210750756995852913803224892022824589887488488201510376749002550349580956046221187*y^15 + 10986983642542065719113254145182683178025486077856651261863167631736003511787510556200805331746962449329173592171973982898146359968969542744555407666779882322925967019311901481369469294098180207796508100788730225899730231710060298332083295728087639429026367906057833421760375960600503915553747526402087957000043455865297754209037813668728693649076710354318130079355/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^14 + 8648145907824122536430297366415378276119538988207839130381007569334285800223692441494980558485781656791062105679435188060936089574289512142069121510205820268362042007236171238577924786333357609228932091910115176090572353604909036522594107061680892192185597490369794261033659383716923089681441616120920698855545789925901393626299822406917152277789340435258709813229/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^13 - 8657384898571991060848421613719272528864964926119673928716911976164725481252009227172575890839110148763470278066308669421813896833665559762048478187424190309307680355869436300858745383351273545278427232638098358381149838027036695857148989940602175062568832818770537544635248214751502213617626307032123875264076338064124752136346804851278312419852872141392104156685/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^12 - 5885175167174805939515078941690656872840156305637981933987727045499697069735878342027621245560755256592132015551276320478135839671856296955201178061886930795545444179236324539518318076357770728795773854086923234427557245487799114321243596292114932525373943078142538137622303737822532168925593298007257125305517043279823132428612891687181104234232323812994875063781/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^11 + 2301227892396215732471575102044511500551732580262271616695906203671617478939611061077912717398701265676656575566716144475864719729338863137263845477642525603719013753033531170718457800301921607593362106154346294488363814884977954685896064435440772194945796068210534278544135108148294467255202484186950568501854116211975777823369286898418378033474356276611001275663/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^10 + 1361526177027936967666170780099967421956490124083630112808529706016411700912615233348910812217566367714235061959487704493168787350011031653337973451708127992015782362550935045867605563224049192550163729029945334974949845983436510714178271217260491606121593549249497370235018269550364062916812260303802039878334339433897044049860739204855320539380720824234742852257/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^9 - 128072376739885317304152554356109997850291043434416247243244580108214920775786717397088962905746470526836474070666729519534217367263445729101874036942642711744439062238687878298747009033372589695216361634662501564950846523004281782423421232708327458789782037971838255448718869761078652761787432584719628702679548586566999569826685669296811007399390146079932571125/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^8 - 15727610267757292182122474052922068483903417772247868236021145897285071307297498549797213555871151299303145022443251765821818305396615630433552620339310277745236495696850811744385128087362472437266967164622030853805194187726744932295180956619493680789906205463864108129325947782649286608631992159349235526154212976726324073448788389422622897958629362550749986389/12930768829943707055065803570889486255550779509233965887732927317126913410597338563853801748555996248810729763324111214912254487189926773058995064329779775904986675077018787424339364259634695658182856174715898810926467216530822631491656107046451231580018642567315961182568464606511500348823873426111900713540903639746769443783982087387792816462340757726768688*y^7 - 4347232542253836376426667635096219606589670578299721185010851829186521169486477407811644474048262943997602613823865874447137572943848724394569536992734630657629941166881331606565964023238819910661932043934536308293885271940869846300581850284474962567271398363230313781928377422050348020652288007762442537077398842859822563420397595878298869597530816148560722021/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^6 - 13740052884070679294805592411976421654101514283554174013790949471727337541115055036705521205489004472282643286912836920080439124503123465254393442104595338987163951369212911420620106792820188408983055802223359900583458618261204788898270489675057899750372901481794041097908228319852707856175300324288861964420461690977801353455468040843427100046694258114844605569/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^5 + 395532716768636327620102926351327826514578032593625177710715307728190915366103239427549342153916081219087323054936637016820048378378321563262626025912475711447792075734141869549766394865722724896986925349904136383733605567983490922082171703542217946145396971442609202618877105244656407692190569401052455968020759253835403727327739395020712965303948897208049729/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^4 + 632140625326609994238775696004871475523345916287872605300476583200716927442081055052459656292116782012962285757075255054832702065281430496351850778157600542141291336581845450671038964221939380557162419828544672011983908519250353144678834145823469287579593401066772627613665512890860108770039197529138749119613196836304918403520212655196524626523111957539899837/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376*y^3 + 139956136460937130833712853522072015901136683573703020347648211897564752975490690850905427622032720704211568306176111961787013164849684363600066964967535162074807293916365806135229047361367602429995927106499428971789656923971388545523510035459926435805561082908771508114825820980393968476253617479435286950962627900888177814179491985424033345813682079582864515/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y^2 - 25199338954619856014700336102672451544639730448639797611573500724033627586334811705476402019604797077957603510216677992737124334808768284986673025261202942164688296210718664312953033907736808909431727472431653616185017026673855036826244575827034402026122884048749125193827471717388076366700865563738470120714396460019904644020459990379093162504675361474192727/51723075319774828220263214283557945022203118036935863550931709268507653642389354255415206994223984995242919053296444859649017948759707092235980257319119103619946700308075149697357457038538782632731424698863595243705868866123290525966624428185804926320074570269263844730273858426046001395295493704447602854163614558987077775135928349551171265849363030907074752*y - 1597973800263194204845722649481037820271693118503941233066791404465682231517045393981600885782437920932056157407259828261707716263028610917384527175909669749831930084492302519347497606621370957620004728072040043892494616810734830287871420314031866638074645148423278978839007204696800373448613333301978301525730471480659222970592377042477288556359862876872797/25861537659887414110131607141778972511101559018467931775465854634253826821194677127707603497111992497621459526648222429824508974379853546117990128659559551809973350154037574848678728519269391316365712349431797621852934433061645262983312214092902463160037285134631922365136929213023000697647746852223801427081807279493538887567964174775585632924681515453537376

# 4 Loop Invariant
-5972174322033163481112039888030097968893308276542223337950946807003576999988369763530163407370606575319355983364708127521129057317159604689345021340942882338279584499836316590022464990886791000122836264662579559440148751446234447669303797887781957658580771993868717465280312978411768574216749640076792769476601500871918516119453313693580108283454949756755196582352948342112161353782375786806868761133482592756616352761944901657074479994306788152807074024882902942686959360163979228854441/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^36 + 171610476832997414116746878854565739704375865733483186986771523938184136637078454134384713898232591550336773793099733199725710145087211704481359080421140024062410866535644199806008097201566784154092690674099556715544826208486786913345044392113310680114202965467150251474473706735547443596819842142305281080767996609799783448820901960735606742732447458036520442110168952522174618984393282305293454160946718780223393621296013002866109096382402156080394244517957049348886941133578450608196383/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^35 + 11108505381234276948585416874768020308478818277648545002330144991322940609888416774988809653706304068319559488551033486328766541038138930033327072865242690604795138037345370425492031129665860546512119827331157690773350746756952908910655767615528343962267802878872023855091307108661169071629099471634006614172774530681241204498507398016867380768276000473385126019043913064747257638992712378789825725089730107068270421258589132026009187947723515812389953281867848978390829356567182724681387/41876308303473653328956366466213588908884274661833758855379153081331699325619152383775170731001143273878503885831494477325710768137550195480734327344931486830561796332193318080103377523389514126412817740556613837242824018301802203022619183700218183239582878103162735290371244179429424377937709421973053072368094786278261323362029371710239497702700029919990647320862338973978493902300965893133460487962159224363275462833193438457770600338027039739179720283611920864048438464729717688171520*y^34 - 2288930722000399333060322294029690827724624142065495724943247157216711128555804088676297339101207962761864919186552474555809726053142398948035078327793861076788631905986873783888901047790056551395209276345353522111029882803273063950189375508300236048801044063205414992165613627832414910966584044570798452720154224106279269539085339606251566671401810199327619490302723643192739941545438942677975649232248684057850039657664802553291327474242143083994445080676878820866618199872675660667649549/237299080386350702197419409975210337150344223083724633513815200794212962845175196841392634142339811885311522019711802038179027686112784441057494521621278425373183512549095469120585805965873913383005967196487478411042669437043545817128175374301236371690969642584588833312103717016766738141647020057847300743419203788910147499051499773024690486981966836213280334818219920852544798779705473394422942765118902271391894289388096151260700068582153225188685081607134218229607817966801733566305280*y^33 - 313020474449591508617228507957301907061009642226994149474561717470858887366303216212035069515059246750635359743105051015592649365734978309212138384844068225990999086155982712059583742966677830771126309706680954316708418620531433697341520003034346393866105783084917559325552835672601321786427637252496352095400050153948786713889351359305354605537533940474890489850436522795540338136012716727526425169055293244815207615714422539397531293230007688497844156827967584379831826260741181628696921/29662385048293837774677426246901292143793027885465579189226900099276620355646899605174079267792476485663940252463975254772378460764098055132186815202659803171647939068636933640073225745734239172875745899560934801380333679630443227141021921787654546461371205323073604164012964627095842267705877507230912592927400473613768437381437471628086310872745854526660041852277490106568099847463184174302867845639862783923986786173512018907587508572769153148585635200891777278700977245850216695788160*y^32 + 770668778500895377002728875104889320120448470277297492577997856649087351845199422437984699843438551504109649670087426730348194025834737250013789914884449123108643103906863756577143716626535179171365520817155935994431481993959260425225944432077046371972753763228780134107768676379538825428787281273618374779742958913443996022093262826809540462253625928638444373899199599493425998566653110596270348374214131010977497302344254850617234597004500949995037593359759589816398269817968650124867217/11123394393110189165504034842587984553922385457049592195960087537228732633367587351940279725422178682123977594673990720539641922786536770674570055700997426189367977150738850115027459654650339689828404712335350550517625129861416210177883220670370454923014201996152601561504861735160940850389704065211592222347775177605163164018039051860532366577279695447497515694604058789963037442798694065363575442114948543971495044815067007090345315714788432430719613200334416479512866467193831260920560*y^31 + 76248334041689298113445654024696016087496606521167762566154653424164560695547469728885219967912053269032353301692833587662749822206298690627084692945641119142163568097403523791047033702457911877066610582120549196341226127582258337389881190894785454956334408961805785482467439485076888630154520561266638947262462995583606829211723986783127269130061885515326042716320533571493492895796955989115714878876378076124196666468675589648836393550955454458408608585775805879978427874673520819605608787/118649540193175351098709704987605168575172111541862316756907600397106481422587598420696317071169905942655761009855901019089513843056392220528747260810639212686591756274547734560292902982936956691502983598243739205521334718521772908564087687150618185845484821292294416656051858508383369070823510028923650371709601894455073749525749886512345243490983418106640167409109960426272399389852736697211471382559451135695947144694048075630350034291076612594342540803567109114803908983400866783152640*y^30 + 33227152603658607351365281732319602435134022056711265587937243384914160208120739954548244124740453644453330707306076401976868528438997778504091699593332001817480428963164266931907034001230124728228193642950306193033571763318302615041871036835118201214835706348520522834722921729568151872660642829401061314211871704479543121947861882204656232388577822251733679597569590374751015355881374320867878007712360579317064072176471339918518497947384216834130717867345632526989623800685838394123368237/39549846731058450366236568329201722858390703847287438918969200132368827140862532806898772357056635314218587003285300339696504614352130740176249086936879737562197252091515911520097634327645652230500994532747913068507111572840590969521362562383539395281828273764098138885350619502794456356941170009641216790569867298151691249841916628837448414496994472702213389136369986808757466463284245565737157127519817045231982381564682691876783344763692204198114180267855703038267969661133622261050880*y^29 - 359896829066950185923878316354362414292423735539194880339191492607950321666184320214718599433636181660169805435824034804560480256618398323195439617449252000809064078057301220737628362451581901626776899709974288678346192362568477023131254234906364715381589408753557674278275954585757747368074102368940315251898582203294987590875555444201686146622576245314222238402996680928207630907723579793144306556223651797160353380064123836108487733719043043871803131616068048462052546583604980948929516509/44493577572440756662016139370351938215689541828198368783840350148914930533470349407761118901688714728495910378695962882158567691146147082698280222803989704757471908602955400460109838618601358759313618849341402202070500519445664840711532882681481819692056807984610406246019446940643763401558816260846368889391100710420652656072156207442129466309118781789990062778416235159852149771194776261454301768459794175885980179260268028361381262859153729722878452801337665918051465868775325043682240*y^28 - 10105426221165050310811253686689802052477432980564789728379642019937515795558517969897522516061361325832675886849025028055232353308340310269990399832394268009828281345846390210521551745532190603026868293385844154101744442113458529100963199781469125737613499545701923528818895841179293453004952450147588791165428581953563200627078729712178200132959883247011635403906776830355330193024964560106631398201312036019626955427822536108316801182960911342671533869658971652650269682096215355698761465821/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^27 + 2184760575548384285318268320298276683907046921809147278258903253236759459651389373063446666236454024125431346947605894707625857022185585699729398580474850838805646644902128927865348364774950838565083599172921791606515622615139687321112220188976618850873076504229514504531695410220018424534481679133024216704528694507538426582764853944062166518541822522025751707633891441111552848577514301443439387206930162306474862781143899427384106486299366932315019874067652021603187387763362666527326578069/355948620579526053296129114962815505725516334625586950270722801191319444267762795262088951213509717827967283029567703057268541529169176661586241782431917638059775268823643203680878708948810870074508950794731217616564004155565318725692263061451854557536454463876883249968155575525150107212470530086770951115128805683365221248577249659537035730472950254319920502227329881278817198169558210091634414147678353407087841434082144226891050102873229837783027622410701327344411726950202600349457920*y^26 + 3497076801058421485558997156747557537650163811376837187781021260960835871678136865567397838198324596582064357650109159460785077930123924616286095510514818416796932499929316912150880913034834953374972707916749924701860248329884460023362895634989574408590655445785798447861596454947548687832769863756722200011549523184516314869399520902486714476595348173724600585362889280729327226887016610719737593026654947927952047963518161909875454383428110127934341154845893999011715266778233500212723313651/44493577572440756662016139370351938215689541828198368783840350148914930533470349407761118901688714728495910378695962882158567691146147082698280222803989704757471908602955400460109838618601358759313618849341402202070500519445664840711532882681481819692056807984610406246019446940643763401558816260846368889391100710420652656072156207442129466309118781789990062778416235159852149771194776261454301768459794175885980179260268028361381262859153729722878452801337665918051465868775325043682240*y^25 + 37104108302233243254789658290129591922475781605180968982203279002890353417545037454414032505063099896144720233582770624182498566911242472790321007917906161861738584776624224043311942988045003360514646048647514519183750652128885689370009158485042849697086817548522084392458905627804365400627671877145349444506676313723795397661018378953373343295136831675441288661522006879146280960252933784992158372860825332183362878808786436135169775107317030301074901270417038494171059346722306041315013299919/355948620579526053296129114962815505725516334625586950270722801191319444267762795262088951213509717827967283029567703057268541529169176661586241782431917638059775268823643203680878708948810870074508950794731217616564004155565318725692263061451854557536454463876883249968155575525150107212470530086770951115128805683365221248577249659537035730472950254319920502227329881278817198169558210091634414147678353407087841434082144226891050102873229837783027622410701327344411726950202600349457920*y^24 - 19363697880948129148649698401349699444389921120821227009078642554680241029850945438654854534588118131001277988026681718536276778744302629495950424172564027922855215650674991666607652854695034945285409095198422123931445667040271742010080692886397745468040011041916127783126839227780417887407588845233508142459531665367472530355996873482335791106378334115811459383107915257251308334264756444984534687379790655759277605186862416624039633477512444839319338092917488003235831399160369828553490795473/237299080386350702197419409975210337150344223083724633513815200794212962845175196841392634142339811885311522019711802038179027686112784441057494521621278425373183512549095469120585805965873913383005967196487478411042669437043545817128175374301236371690969642584588833312103717016766738141647020057847300743419203788910147499051499773024690486981966836213280334818219920852544798779705473394422942765118902271391894289388096151260700068582153225188685081607134218229607817966801733566305280*y^23 - 17901565487682812224645084267063146309636620077757631632518057572417822388872319692955357490211889142741041995553321147681178873921832791256358874135311717681449786089842206443235070436556033342416135543675863258737428130096183144743129149800443399315236444637099251657455040300061977750051898610933314224819535357483890563433405716195393976299565305408152293235450226590262602988940095141457732027569850180502216976839505797091555911722319719773699073722767280057253038677780060916249666849401/142379448231810421318451645985126202290206533850234780108289120476527777707105118104835580485403887131186913211827081222907416611667670664634496712972767055223910107529457281472351483579524348029803580317892487046625601662226127490276905224580741823014581785550753299987262230210060042884988212034708380446051522273346088499430899863814814292189180101727968200890931952511526879267823284036653765659071341362835136573632857690756420041149291935113211048964280530937764690780081040139783168*y^22 - 33492098447791263215303338481795769408776882533624780958609309673904809728927657737370758556600260963460085059263134158190280163896249557766381037669043066955973018632058264705945009083288751338487891749545337348645732423624573734984693659609815969304504795138242120492908094691816323176856102387947371086288781376003177361625610821036848210355738410005052732425887589499373423309734044837242082110331773179008875785800899582202843550783550202173217313187624723632220612617341810995410822501/146843490338088305815234783400501446256401128145869203907063861877607031463598512896901382513824141018138318081504827993922665647347020074911815916844850510750732371626915513069669434384822966202355177720598687135546206334804174391787237236572547259709758442193433683980262201124236842909435037164509468281818814225810734838521967681327159954815573537260693276496423218349347028947837545417340929928910211801603894981056990192611819349370144322517750669311345432072777115078466419286080*y^21 - 39268019746070527993941761482757538121633480681686167108812045766220766901207392182411539821164666256725982366436721841743347811490224562015274598616422685780961344841728048476795191809938440762860618342228743389862058993481613000314619222201026933222639626461141774752832657905120814185071305154893174253094276161878224781919607018351730533090549994149818616448795049214198928330204704813498640873250404424999669232806855602396443391610847112673714417680243318872119814141505964888920464539819/118649540193175351098709704987605168575172111541862316756907600397106481422587598420696317071169905942655761009855901019089513843056392220528747260810639212686591756274547734560292902982936956691502983598243739205521334718521772908564087687150618185845484821292294416656051858508383369070823510028923650371709601894455073749525749886512345243490983418106640167409109960426272399389852736697211471382559451135695947144694048075630350034291076612594342540803567109114803908983400866783152640*y^20 + 67954403641411107670634962438424556542530338585293622647379025174743285519051013734646061177601363708986709760178126848075968051417412220325408834137140584607230150101984072393702640020768735380284887590986868031965494071791220455733130407553420465577937898314478435278019753124346061415919930038413553281728101195845062282211361453665326960273369871318987256269452291430168838640201179322865448919125445020331280011544414059397807422371517286201787204104845102548841674431937066056922280394329/142379448231810421318451645985126202290206533850234780108289120476527777707105118104835580485403887131186913211827081222907416611667670664634496712972767055223910107529457281472351483579524348029803580317892487046625601662226127490276905224580741823014581785550753299987262230210060042884988212034708380446051522273346088499430899863814814292189180101727968200890931952511526879267823284036653765659071341362835136573632857690756420041149291935113211048964280530937764690780081040139783168*y^19 + 431884401054844424651044355648837949469540492514962677977159085494768107486356283934178456942241362482118102737914370325076675958238368021799172909807719093911533266837282185204093141069959091059456023082433038815580695249546011713697290606622713310529585448579347567736145346960863761307221506769094039438899521164756554888109601086388847010649515347093876074160166439507511455185465871267741367493874887864349845141386633259369579561010080407841490212556671454363235162594778289275729925403193/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^18 - 73104431104152200507891267497231258400239554380066489904222879718620220162182717415189761944563653893559416942812634859790855286134908905546570981809721001473440730754124025924993297857131145948822641031315523566462051146599729864579625078930962327386400529414551677982292041895720863836678110806129208687802703128976214995247106011807126665208410913148915814552164020019669376866374928691623896739138021714841544603622743361220071280130938970884426933189967515461108200697268507210910731413139/237299080386350702197419409975210337150344223083724633513815200794212962845175196841392634142339811885311522019711802038179027686112784441057494521621278425373183512549095469120585805965873913383005967196487478411042669437043545817128175374301236371690969642584588833312103717016766738141647020057847300743419203788910147499051499773024690486981966836213280334818219920852544798779705473394422942765118902271391894289388096151260700068582153225188685081607134218229607817966801733566305280*y^17 - 107903348614720654842812670555121343361902782547545787157713799271872394976526442624710929572795377009368307959282688248552303917138187515115158248377045880013221413902265251629137522738155915175860397367654918184085999918735926876420209007037680101754676180190374341757697575440458878368643425612617887280675946381944026064318972650157142645891835712540957282481832857046592576723872318631862969401109086103452167725785426731213464972449291767690279693512285078799067455826957427238466144376981/237299080386350702197419409975210337150344223083724633513815200794212962845175196841392634142339811885311522019711802038179027686112784441057494521621278425373183512549095469120585805965873913383005967196487478411042669437043545817128175374301236371690969642584588833312103717016766738141647020057847300743419203788910147499051499773024690486981966836213280334818219920852544798779705473394422942765118902271391894289388096151260700068582153225188685081607134218229607817966801733566305280*y^16 + 19160529645369450461496690706207778068023096512721294730817588520009530006068920877040740948508977708261861902582770449266181862488965758696677859841527712986071950117748178463435133060964985986278996114442295851762387164291561943692698039493546177335542284795765634052531502530778780163591587830480823327112170127224851736502328436246411004248470272976631363455609036036679164157044941756293368193374746403324083575115595247362240725546715071267627484402871330012534286655561545922521361286759/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^15 + 158570650866889245673762178183548779258937178988349013767253733836143093320035674443585539631022761426035133348054375279703345734288522760037461168852674108420544702593080391500708401797308188065324008058004128212009885209063237673884484440749653899452898249847125645652668826717452203887855393625200267512562005617859504268579163777830382396702846189724160297064731170758553530028312975230762703173592951392382115290144823676273850904845250140440801376577316507346528768973680363008896881607087/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^14 + 66883918083369898476823601265721479508484700342619771051092693880424661141637698435432263118773354849055172671922157626379315883699954340445790136325442700732583373800404570250597979073896445238825095200481169253612675393613735123647302694148869823411773665347159096022642015224600490406274707746206859503698501322203941997137153195512859816194506224051923456536494493142766056088666388714952744533590127075163890707325053239470548090122880920144291465767568691656101599593407535096950669163159/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^13 - 3009052167516826075271426747177527828711327513161370866082104081991124995410168447715779208955297352909274726336628044243520697234669317367666275458358365849402939083418145733319130935475663440863259704513265294647000580193063358292765137437694576561776610427377620469222955993212848971055840827600127121964052634003924119767450588984052389115314299202412001174527390088749067150195395418651157042788634294005790219455135814212845015605061837753889538176441351556741112671836136432423278190891/35594862057952605329612911496281550572551633462558695027072280119131944426776279526208895121350971782796728302956770305726854152916917666158624178243191763805977526882364320368087870894881087007450895079473121761656400415556531872569226306145185455753645446387688324996815557552515010721247053008677095111512880568336522124857724965953703573047295025431992050222732988127881719816955821009163441414767835340708784143408214422689105010287322983778302762241070132734441172695020260034945792*y^12 - 22065938571092362674827058553649663229286429886464496914392863669217202896638365569030170613660231380408320750083730474935899678499049072985002098555763465519005151872064696811877319665571284643913960443105187762793632408036084072472673203692379716036956173864085536317906403256654391164961409085276552994629329366933408039790328091861813588559961419339762706641873081624834110152185649366395918018229445775700026330607231013918615320502116634830051816897792294931890615592021562416605720877059/355948620579526053296129114962815505725516334625586950270722801191319444267762795262088951213509717827967283029567703057268541529169176661586241782431917638059775268823643203680878708948810870074508950794731217616564004155565318725692263061451854557536454463876883249968155575525150107212470530086770951115128805683365221248577249659537035730472950254319920502227329881278817198169558210091634414147678353407087841434082144226891050102873229837783027622410701327344411726950202600349457920*y^11 + 3044949838654819013794987611513188067577450066088012258208728242170805389483636346574339569426059174029866703610805238812117217075482917907728512812629437195095137815558229112944725692680347399817326794300386092057613355379780187014137651439470488136094406906970657071580687146827895777456410977371613717495624050294529571079246192628908769150481246945766468156356826699070949126956113958791748929557355511314390568996453474256094742577689746092782420023695080673057051955169474644366335185733/142379448231810421318451645985126202290206533850234780108289120476527777707105118104835580485403887131186913211827081222907416611667670664634496712972767055223910107529457281472351483579524348029803580317892487046625601662226127490276905224580741823014581785550753299987262230210060042884988212034708380446051522273346088499430899863814814292189180101727968200890931952511526879267823284036653765659071341362835136573632857690756420041149291935113211048964280530937764690780081040139783168*y^10 + 53570287266954761752951988349218643663900991022147468783162070157374031310850984750398926357966763824140093100167059529601795756774067123508336605358207326073837479496335303119024614022531535891847876974589338020251204579946919823630379978474539250800973269519817379621197723057265849376439269582214048464656804987940437621726727418762316046315810872859936175724279106564286747748654399901767203754523293517694751823355775096630784041986518818048013906743493335502095054837845470869702355889/3707798131036729721834678280862661517974128485683197398653362512409577544455862450646759908474059560707992531557996906846547307595512256891523351900332475396455992383579616705009153218216779896609468237445116850172541709953805403392627740223456818307671400665384200520501620578386980283463234688403864074115925059201721054672679683953510788859093231815832505231534686263321012480932898021787858480704982847990498348271689002363448438571596144143573204400111472159837622155731277086973520*y^9 - 1562436626362511538674451529557519720634634270317002519782030587278247902197799863180830718862444032002090888091693002074874919165026116513150300899147467868078294286282907350833479932153694183339161644730462371052522610734787558391676156974908121921239487904141994227300136829962392476641699121400566574659458116008709008360844773137169579970085748090514275563141435656392396011988777813273201798384379593475183599161006477335778345470620323918534051258346439966175842205527094498125384207419/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^8 - 513513085536954227304217799593738419288893270042567206877168858191366979120084076673904502197239710776068180810655445288804875755270985578625943255577648161150533687687670316027418202441264772217219698970427502639767832710933570504506760763524513438708591784317411010047626135331031143378548828366664916332575397288545449366913037070572532057089026684632889403683170141272008314145491726406844083592474965818060052195283933897526970464491194274899291814217582245953916628479119132083589596979/711897241159052106592258229925631011451032669251173900541445602382638888535525590524177902427019435655934566059135406114537083058338353323172483564863835276119550537647286407361757417897621740149017901589462435233128008311130637451384526122903709115072908927753766499936311151050300214424941060173541902230257611366730442497154499319074071460945900508639841004454659762557634396339116420183268828295356706814175682868164288453782100205746459675566055244821402654688823453900405200698915840*y^7 - 12386145471881844821016913722392075236117929799168048681687407078110611986955507855573611953370390883046183334084931818643004218403646711154533275376148481634027597992040084067435865905785118677065899230313732809116076596646580164768323263111263840329261241479636567505809338269111786330126695128300187573051563641025032564682411329700151639085200920847082289779745880176191967205356758861180597781205999489587935663007240546425366045050340542635570875298421173290975301883518306253862359431/237299080386350702197419409975210337150344223083724633513815200794212962845175196841392634142339811885311522019711802038179027686112784441057494521621278425373183512549095469120585805965873913383005967196487478411042669437043545817128175374301236371690969642584588833312103717016766738141647020057847300743419203788910147499051499773024690486981966836213280334818219920852544798779705473394422942765118902271391894289388096151260700068582153225188685081607134218229607817966801733566305280*y^6 - 16438787154146394268521051532970426887027806629844310899714610818191666196367683362711037109109765681290614435218376277555196925249189978817826567453346706258031361541373841382375534622575298202099316691710995756443604675141289751497522267360522065219216463743859909150328975963877085893712108823284722366414603835896079688490046171185359610919736531212801389828154078142509157900560259766594185246669611736212464156408523050479242211167215308755863095513211675532120852902290710045528126501/118649540193175351098709704987605168575172111541862316756907600397106481422587598420696317071169905942655761009855901019089513843056392220528747260810639212686591756274547734560292902982936956691502983598243739205521334718521772908564087687150618185845484821292294416656051858508383369070823510028923650371709601894455073749525749886512345243490983418106640167409109960426272399389852736697211471382559451135695947144694048075630350034291076612594342540803567109114803908983400866783152640*y^5 - 197039751996283760267110074325036301752073444715112214198760011372227049348386758729774170313862512181255194346945280494976884441064913165874877521599967959801185356462569410007007594372441954958728634838861029099386357900231982965208969991989523107972306608158909981207592905537143799038741020557575265739582630491112809122790505810360013239732800088370438180891568936256354603415674304762642465751719955768796945185717627153787574000250210625168837206767426017398788036026098290685766141/237299080386350702197419409975210337150344223083724633513815200794212962845175196841392634142339811885311522019711802038179027686112784441057494521621278425373183512549095469120585805965873913383005967196487478411042669437043545817128175374301236371690969642584588833312103717016766738141647020057847300743419203788910147499051499773024690486981966836213280334818219920852544798779705473394422942765118902271391894289388096151260700068582153225188685081607134218229607817966801733566305280*y^4 + 2321405921457874546095421526623496987457455320123273528134086731784224168224869739908624782799250863166642018742776374335460409028782135564529224200471413077396861843995196224823551910462654920981727867660786745734174671995312613124381106709429876085219503390146763342806473051001416639661134226786401291568295489514000356524874630388043072170824609121660873794431442046299923182199366507095491692915100092962256903031475925656433268881403986796005133055465821097330647717009950350286959863/177974310289763026648064557481407752862758167312793475135361400595659722133881397631044475606754858913983641514783851528634270764584588330793120891215958819029887634411821601840439354474405435037254475397365608808282002077782659362846131530725927278768227231938441624984077787762575053606235265043385475557564402841682610624288624829768517865236475127159960251113664940639408599084779105045817207073839176703543920717041072113445525051436614918891513811205350663672205863475101300174728960*y^3 + 310560608973739087094370037777630715522322886685600458512919869439636746821301002069043576121675429725704909670668250648945069643067858928027195911170460059158946552663865299065195867810979273170458158593101073752717473875715403728099493787133858097556811665344968571519433785375580086885345997859431615364761675063716833953316058075748517378685526123301453973867530332542781061128598387593487790722764795433897441211862039768438284278090242042935911351689330919476147608670516350780143519/177974310289763026648064557481407752862758167312793475135361400595659722133881397631044475606754858913983641514783851528634270764584588330793120891215958819029887634411821601840439354474405435037254475397365608808282002077782659362846131530725927278768227231938441624984077787762575053606235265043385475557564402841682610624288624829768517865236475127159960251113664940639408599084779105045817207073839176703543920717041072113445525051436614918891513811205350663672205863475101300174728960*y^2 - 2034720208121109980110826569550420211246165422412140437348923096154117226452162913297350820271170885379354203902726925292798413008891251985552794583958672730999036700221716111921733608154150065629964451521563788157935605047877461952757548467298745702288328707185553562037900435252883383591374827764209298234379245130669752718228198279201773810652850018724582366093278279348900429011454809735024250027529805574157387164985011625501174490932880480150860896494914315443637220096841743475553/8375261660694730665791273293242717781776854932366751771075830616266339865123830476755034146200228654775700777166298895465142153627510039096146865468986297366112359266438663616020675504677902825282563548111322767448564803660360440604523836740043636647916575620632547058074248835885884875587541884394610614473618957255652264672405874342047899540540005983998129464172467794795698780460193178626692097592431844872655092566638687691554120067605407947835944056722384172809687692945943537634304*y - 2828232097641830307840103734708700613401496121890759672142579140728609333778491029919162937711355711710295352903547882667941839299528229022302005693708906174593036309377228330437563157864108574904906119940107854626568263649944270513889678053526371664367820366347532092731636762401659710758118175923944891729968896928111366323611840310642200315577838982640699372631282943103544670934538548600885527498144065808732395488947771085771026740275711314137800842024462048024616648453950707274429/59324770096587675549354852493802584287586055770931158378453800198553240711293799210348158535584952971327880504927950509544756921528196110264373630405319606343295878137273867280146451491468478345751491799121869602760667359260886454282043843575309092922742410646147208328025929254191684535411755014461825185854800947227536874762874943256172621745491709053320083704554980213136199694926368348605735691279725567847973572347024037815175017145538306297171270401783554557401954491700433391576320