# Manifold: Census Knot K8_103

# Number of Tetrahedra: 8

# Number Field
x^28 + 5*x^27 + 11*x^26 - 21*x^25 - 116*x^24 + 336*x^23 + 2498*x^22 - 1138*x^21 - 3014*x^20 + 19583*x^19 + 30409*x^18 - 16551*x^17 - 9746*x^16 + 80226*x^15 + 148984*x^14 - 132749*x^13 - 112172*x^12 - 34164*x^11 - 215665*x^10 - 410556*x^9 - 338304*x^8 + 15248*x^7 - 252384*x^6 - 4832*x^5 - 76992*x^4 + 1024*x^3 - 15616*x^2 - 1024*x - 1024 

# Approximate Field Generator
0.400885524380667 + 0.459021543813592*I

# Shape Parameters
-151911379316710087234708148576694343265182023418868193259186710845584299173181362900743/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^27 - 251599172421816135447475253863481336770785290458000633098169222905694066444750330243353/234991053257905601129352813632357627100497707641629225079574702475613670370240767576500736*y^26 - 1641606050086571745819858215532970843826435603411208172409158734617861555961158875894937/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^25 + 3278691112734323172238239596365641358926065074054235681909128803595261814343808886835199/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^24 + 367304372432160256484402205859488241349101112533684405054331080773557536223166964082449/14686940828619100070584550852022351693781106727601826567473418904725854398140047973531296*y^23 - 4299684401804362809739152957935568332808234031002782264136381480139790040567215933479891/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^22 - 189325497395621679348298156381828441406175942282880598868760226902707511531842043135608163/352486579886858401694029220448536440650746561462443837619362053713420505555361151364751104*y^21 + 92762301746119956568959481071791451161523169946035752294449259697366053409086695419807711/352486579886858401694029220448536440650746561462443837619362053713420505555361151364751104*y^20 + 234285907581523362270509623436204787114678966594887658407380250194758245232941050905723401/352486579886858401694029220448536440650746561462443837619362053713420505555361151364751104*y^19 - 2972657301896446826883774205633502457941970799795503304021942528938073016078583030844920145/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^18 - 4538133542681690271718956330692544871368654162360517350620740761567392798488612910248546703/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^17 + 2724515740991997168277650409624287351119310100864172906432774413980708425412624152789500285/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^16 + 7001964874075107574350819646244824507000410529923036806893262928109078167373879215119191/2865744551925678062553083093077532037810947654166210061946032957019678906954155702152448*y^15 - 1991047249633847361863725836254656580255190880901126970918826686555864515348961306565565967/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^14 - 2794502970761381753547684905971765564232501555216631856854011550795772871616288158154653501/88121644971714600423507305112134110162686640365610959404840513428355126388840287841187776*y^13 + 21034494296648743014243964980742287454739648968634511881990468102869455545119730487311137747/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^12 + 1493278174826334768528866757899971890717633861707172457694400835702147469082535845151428033/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^11 + 57509511764854423095820631238136663227603826704227265141257401148107584769675516621394481/7343470414309550035292275426011175846890553363800913283736709452362927199070023986765648*y^10 + 31503788181897002776746940508616049633845227894377899468353073511600033104349090209047307727/704973159773716803388058440897072881301493122924887675238724107426841011110722302729502208*y^9 + 14695757971613162305903092052102579078238050169897592554625253285572431328915035648833591963/176243289943429200847014610224268220325373280731221918809681026856710252777680575682375552*y^8 + 11956982619120250884940649608752146683689538066381070964692146087580939096191665454183138441/176243289943429200847014610224268220325373280731221918809681026856710252777680575682375552*y^7 - 1034328559729305841379057640661102049846504351198731342883601999728585599356660003228180431/88121644971714600423507305112134110162686640365610959404840513428355126388840287841187776*y^6 + 2013100987220450290590433187390615139977032231812183134885556427377590448739805039312808899/44060822485857300211753652556067055081343320182805479702420256714177563194420143920593888*y^5 - 57794957249263539918620085569898203680204208895158274868917527890260333989085971446037213/11015205621464325052938413139016763770335830045701369925605064178544390798605035980148472*y^4 + 145626180308453167777860989101374917156137134234889636313584336172292966260543460735694777/11015205621464325052938413139016763770335830045701369925605064178544390798605035980148472*y^3 - 596241889792600448840263086673252190540292871813996594029694056702893850180930491158923/1835867603577387508823068856502793961722638340950228320934177363090731799767505996691412*y^2 + 2538107016722696759656433873731615334119111703672920162755194624957775575602375371174083/1376900702683040631617301642377095471291978755712671240700633022318048849825629497518559*y + 1644670579253435479256991764430576940709555466586133855447339034883551770270561543336965/1376900702683040631617301642377095471291978755712671240700633022318048849825629497518559

-9038182029602625266613601400626449424158298009813552205369254586846323768057867267077/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^27 - 39506808154134152788164279892043759873350765823953700992338223729910550298120359184637/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^26 - 69221646984172280470752753852289050180390270795712923206597413513028150863516040415625/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^25 + 261407125369292857174537533320946094697985529100925159378433543320178931317328970341019/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^24 + 474690114941327710274412105230315109470505683960832863679674625498231301619470800837033/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^23 - 1866679908547707994704740065322958951310804477119128683852505155375146771583275273634135/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^22 - 10442011197772056714297165645070843751393686508332610716428353155401351925735554176205579/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^21 + 12528272204904351237753350265568315895966779371345302245119577923237400715331562244328129/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^20 + 12663941030242305571524436368715263883845594857724712571961280300467508442969398494769941/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^19 - 195643019619182235538008546555085052298292148300550765124867908979904501853950787142961375/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^18 - 170004335719937826865435951035965186248792535091458757666589122589054470180786537348039805/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^17 + 354736907942998758328033403044926045024649280026648933063200953922751656648148978877645733/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^16 + 337475008615638267884244842091054596032075724960562935016266594644513776798826368235829/716436137981419515638270773269383009452736913541552515486508239254919726738538925538112*y^15 - 201545447865092996185539651412064572864791797139354931599168690136881173397148230142809335/29373881657238200141169101704044703387562213455203653134946837809451708796280095947062592*y^14 - 58699954547381046814801292545835750987693566922829399844109440186857386443563159064187361/7343470414309550035292275426011175846890553363800913283736709452362927199070023986765648*y^13 + 2178466506755235185525340435951254185106369460101746382474504365313756622348420337773084989/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^12 + 71865950137753032936078628400812190082479040443346396728874055353095302472884841761491785/14686940828619100070584550852022351693781106727601826567473418904725854398140047973531296*y^11 - 284991571859356906598177599578128482716805794502533386080119503997065087167714665251719315/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^10 + 1426555119214271735138005065973277429048990946503414428492351208448327995720008799891357865/117495526628952800564676406816178813550248853820814612539787351237806835185120383788250368*y^9 + 293901614226427317436005003103408145573453772707613982525568266283152303335916053040375191/14686940828619100070584550852022351693781106727601826567473418904725854398140047973531296*y^8 + 264750291836177845383661137373452454079660158164818847926850502895059514027382638651738223/58747763314476400282338203408089406775124426910407306269893675618903417592560191894125184*y^7 - 705797896077538612447927484273012541393094736206208354641440095692697757855873029101442615/29373881657238200141169101704044703387562213455203653134946837809451708796280095947062592*y^6 + 106588456387580956084427683237371421588864473279766740337256720360634946529624418324279455/7343470414309550035292275426011175846890553363800913283736709452362927199070023986765648*y^5 - 7867034383623130723199464389085353436777769417766805207972177367695814556207719053174433/917933801788693754411534428251396980861319170475114160467088681545365899883752998345706*y^4 + 5169523230656829314189955289377764550115480471065524127291699221317147488370416179578087/1835867603577387508823068856502793961722638340950228320934177363090731799767505996691412*y^3 - 2159809660780070305288405350241817890101862673614076047010415571903580627875875495645405/917933801788693754411534428251396980861319170475114160467088681545365899883752998345706*y^2 + 144607557900122735970990875301462561965549128759450371321178948282433828081868760804666/458966900894346877205767214125698490430659585237557080233544340772682949941876499172853*y - 71653821217712404782568513463713007368969511705735393436428416677596421552819307519595/458966900894346877205767214125698490430659585237557080233544340772682949941876499172853

-2082385573282039789965450504571063601222599066639749268853078561545883659894403190209/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^27 - 1675148247536645127848186988691830266847614816096503998035987051467144258428535190885/104844312875329685215356698527226781871132231249983294949245108183646789278810574468992*y^26 - 2600611375431153128678204394768243764257074033147257685195144010763796602136771301865/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^25 + 24561384444715963279152459939963365636498661806200739218187917730966248110613901402611/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^24 + 78964974602309361015201287413463956168520286689193434019052867563259813177231503289703/209688625750659370430713397054453563742264462499966589898490216367293578557621148937984*y^23 - 324935586233376926516431087142083854053460453123797663372232353946683192117548517430/273032064779504388581658069081319744456073518880164830596992469228246847080235871013*y^22 - 2557054095456208858806412152797201553918148009772769186510477493738236451460282993483339/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^21 + 26396372831929675590288762831840784698470601853748245422180426476406239844789237523907/4914577166031078994469845243463755400209323339842966950745864446108443247444245678234*y^20 + 823782794779915562608487303404488540246153896483808511748769317049047310846452387148847/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^19 - 42364962537972442352836286873361208324659783929714678453198709766732703184053780051410913/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^18 - 7147924370209789832528004710731785220347297467811997404989407926410071241000582971761383/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^17 + 25715573285072692872259973419504732618775057894082391166543127158827366178084566464673447/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^16 + 2478300939478264481791222972525168807250375615577794949707552611567908929680502139464117/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^15 - 4944916927116141993048428684380201378131662943028723791751736369762645365197674866082951/17474052145888280869226116421204463645188705208330549158207518030607798213135095744832*y^14 - 142353883678741595409143844576640655622684679636752040366308765359604623009751901806924475/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^13 + 354780511275477997905607614494684054608498739455101613530746429017635432445892354940250685/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^12 + 75277989900838482514302171404592916161318270667495629684889309777483056453437667372436195/209688625750659370430713397054453563742264462499966589898490216367293578557621148937984*y^11 - 106525983672316310475417003870758166066699549399888398171851304300081908898730588262043/3276384777354052662979896828975836933472882226561977967163909630738962164962830452156*y^10 + 404086891455272863001041154687853351369112368942323191387524395846337365584951400552113745/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^9 + 776677039732352746651888736225791885260734721697777462555494545576698714940770129910367509/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^8 + 125415136204112604441160537111185248389599856785094227190446265287167885818982672137718135/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^7 - 64736559560221116612852535014287200566554482193415634730114719416427047375711402027875837/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^6 + 14475989658589876907722230546670266733446778763003390562291418112030024746587995622060251/19658308664124315977879380973855021600837293359371867802983457784433772989776982712936*y^5 - 2397379350224574252953099291043951431597944701006989735047459614381688410174798615247675/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^4 + 3179819140391949426876857266944810862917200148180867918665680616554430501501969934079459/19658308664124315977879380973855021600837293359371867802983457784433772989776982712936*y^3 - 18286933896432800312285408387056463356578477047240747643570144685203478836520861548826/819096194338513165744974207243959233368220556640494491790977407684740541240707613039*y^2 + 68276540583634659583939955779813370691186516433730939091893788946024314019561053936514/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y + 10545322648944491421786614867052401449422748365822186399484049342680838092155566962660/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117

-3514365007886909072004639339328768030579176081192570900825591770602702549519616173578445519/63154281872670160987998592370597033337511515645468201045617632573838880158115790056390225510208*y^27 - 58013595005542259925272308104946452790827098733801260464829021781099639573037577724777169111/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^26 - 89655676777110019126457510288135374459036680580901318144208246601320318684772891057273233457/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^25 + 445628236118868667774219703051241151992583550990573663924469135457458670118635791485891952177/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^24 + 1398401177903627629817581880526277914191315324785546113962273850886026135882929614605066657017/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^23 - 3128728772485438678540965628337325005298003907139441793724615343371474231116632071456574612381/126308563745340321975997184741194066675023031290936402091235265147677760316231580112780451020416*y^22 - 7842182947887771391190862055905255765226509138845266362055379604333694757025976852861045074605/63154281872670160987998592370597033337511515645468201045617632573838880158115790056390225510208*y^21 + 24095882445627998291138374443774131814894468590799325839568035724782081458233393601118377684189/126308563745340321975997184741194066675023031290936402091235265147677760316231580112780451020416*y^20 + 18331722523808382520445337195461171848779564051836271416005266951892414753940547982117137618497/126308563745340321975997184741194066675023031290936402091235265147677760316231580112780451020416*y^19 - 161627047842999917812468575237745239166467653466883140474672363549071437176754486036308790233599/126308563745340321975997184741194066675023031290936402091235265147677760316231580112780451020416*y^18 - 197786108250576158636519057235285102797381651092784537184371538395927434254370438661714086867925/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^17 + 684564311676253036992172728085385715279835843218597744582267457839351799990541160246348414756367/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^16 - 106039271858214640091849773418845730561413662145839995890221995412647165452029847036962955957/6161393353431235218341326084936295935366977136143239126401720251106232210547881956720997610752*y^15 - 351426581541664755825873877713509730488437391946412696271346590098669136677427471180593473223489/63154281872670160987998592370597033337511515645468201045617632573838880158115790056390225510208*y^14 - 570776511115414922562949925223030044129231469249494344834051868217926430519142519069834552747323/126308563745340321975997184741194066675023031290936402091235265147677760316231580112780451020416*y^13 + 501466952839706556462850181319308851766937444025578688335681243326395842049290278625099312725043/31577140936335080493999296185298516668755757822734100522808816286919440079057895028195112755104*y^12 + 293855314706524966846100081532592351720942467720153541758166936705466056645904210143523900986199/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^11 - 917719678322808068845653166018419430189100232151684344519335132854713733022211517395994319366583/126308563745340321975997184741194066675023031290936402091235265147677760316231580112780451020416*y^10 + 590897021471479311897759925149673175640406766310966460745130381651070625241404185135849208047853/63154281872670160987998592370597033337511515645468201045617632573838880158115790056390225510208*y^9 + 3359144202443755417448892716616842245842446588964383524127148841967501563795286886121151602400699/252617127490680643951994369482388133350046062581872804182470530295355520632463160225560902040832*y^8 - 395264439917212696557238268110019446873904381942349439707139349929983766177314709293855820790987/126308563745340321975997184741194066675023031290936402091235265147677760316231580112780451020416*y^7 - 1283871877547297965873993777852118930127708339685636427993286425123913817809042661796928345739205/63154281872670160987998592370597033337511515645468201045617632573838880158115790056390225510208*y^6 + 478485237683669102854516017732393499145031808653245119066536029000563778287977668182132954991325/31577140936335080493999296185298516668755757822734100522808816286919440079057895028195112755104*y^5 - 50842028678342237093393312233750653737621373845603656885850212817389984520891434258937004426973/7894285234083770123499824046324629167188939455683525130702204071729860019764473757048778188776*y^4 + 4551356255292597733575060691561302882041708352699562580834103596262594289106880819623670945771/1973571308520942530874956011581157291797234863920881282675551017932465004941118439262194547194*y^3 - 1393973231135202490405377535180185765823542650117505197858117794204061740215448997092620761575/1973571308520942530874956011581157291797234863920881282675551017932465004941118439262194547194*y^2 + 483411299671898903317065156183181750031913014407782024267413185999815547043326727667055199598/986785654260471265437478005790578645898617431960440641337775508966232502470559219631097273597*y + 692986929888435765046444270117183676160608746897338571657824065671772842353379828535321110483/1973571308520942530874956011581157291797234863920881282675551017932465004941118439262194547194

-71426182185517214365330299923485541409565100760251023946619808104566954497368551909/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^27 - 8700894666609944497398046265861455603828864691686449301716020559917357101080135031/4368513036472070217306529105301115911297176302082637289551879507651949553283773936208*y^26 - 8688064167448314049760495446610084992659058431712672021470986593301384156164463125/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y^25 + 1016247772491812706303458284513661817104648691166550050715807716031167358393983475977/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^24 + 2490049360935320289005956545170266845798030852581296007676399589046072423512626295363/52422156437664842607678349263613390935566115624991647474622554091823394639405287234496*y^23 - 4886117000069129177270110758570426661701702808001788970988007816124487492939406399025/26211078218832421303839174631806695467783057812495823737311277045911697319702643617248*y^22 - 82416289713214411289118178829044970129315331063226945817406922300012871254966740449147/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^21 + 48612460215077433537242495186839905833268479242825257504253981157958552994082415797503/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^20 + 5946649672334072249820647727439396826231959401804962493670139004508536372771262170955/4914577166031078994469845243463755400209323339842966950745864446108443247444245678234*y^19 - 1545012077831485746395064947141618507272498791773297467791627957233884523672280568538045/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^18 - 670482919095468015202612431086062422362036975870891150038933099846545867168822941025371/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^17 + 1356772718439556023834764444808043229637921456862671209720131345552341578091880840647109/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^16 + 28307480408066715571074008904005075216701921247063032952518994713288552208260409092481/17474052145888280869226116421204463645188705208330549158207518030607798213135095744832*y^15 - 352371785076523471673469938012221919002862833598822620670215869721568793401056494691925/8737026072944140434613058210602231822594352604165274579103759015303899106567547872416*y^14 - 3609768336847544109559336736796334263875585878432153425184583047255245137805354979438939/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^13 + 16760291311406878386381570735497911911616449995423478726935084777626587206459548381393205/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^12 + 1204173849529811853847202946049632363139885936910990797297604564888888883907169866053001/52422156437664842607678349263613390935566115624991647474622554091823394639405287234496*y^11 - 650692316399063826662405966175972497458083392247318129055199432130205676015678055336505/26211078218832421303839174631806695467783057812495823737311277045911697319702643617248*y^10 + 12858863627839111271233040929168785820031794046973376144462553314277498192224060550920877/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^9 + 19204241168830824546338611221656463728343575709368538940480522370564771592990250523570831/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^8 + 2042631285483765823840647373758876171961630561827139791392627135464065612196324328187295/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^7 - 4851346997763185624516924943822113018212334463397489569913008294345983757084849387524777/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^6 + 1986662706541763906078345136129339229772463443585794060817234527501335501681718477603763/19658308664124315977879380973855021600837293359371867802983457784433772989776982712936*y^5 - 311262679476802075275139028322613190354573302127609215572302685850713816332480254118321/4914577166031078994469845243463755400209323339842966950745864446108443247444245678234*y^4 + 55742838506679774775141996286901756076162963782273905542165090836509597491272904182869/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y^3 - 10508886355116689140580669154597113993358310473144861157746420379304788943457941461708/819096194338513165744974207243959233368220556640494491790977407684740541240707613039*y^2 + 8176203282092139626462182841663300029787676993731516472757007818946294856102509099228/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y - 5590359198575872129547381397975761820818686016075361904657320630795005909559267605513/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117

-71426182185517214365330299923485541409565100760251023946619808104566954497368551909/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^27 - 8700894666609944497398046265861455603828864691686449301716020559917357101080135031/4368513036472070217306529105301115911297176302082637289551879507651949553283773936208*y^26 - 8688064167448314049760495446610084992659058431712672021470986593301384156164463125/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y^25 + 1016247772491812706303458284513661817104648691166550050715807716031167358393983475977/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^24 + 2490049360935320289005956545170266845798030852581296007676399589046072423512626295363/52422156437664842607678349263613390935566115624991647474622554091823394639405287234496*y^23 - 4886117000069129177270110758570426661701702808001788970988007816124487492939406399025/26211078218832421303839174631806695467783057812495823737311277045911697319702643617248*y^22 - 82416289713214411289118178829044970129315331063226945817406922300012871254966740449147/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^21 + 48612460215077433537242495186839905833268479242825257504253981157958552994082415797503/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^20 + 5946649672334072249820647727439396826231959401804962493670139004508536372771262170955/4914577166031078994469845243463755400209323339842966950745864446108443247444245678234*y^19 - 1545012077831485746395064947141618507272498791773297467791627957233884523672280568538045/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^18 - 670482919095468015202612431086062422362036975870891150038933099846545867168822941025371/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^17 + 1356772718439556023834764444808043229637921456862671209720131345552341578091880840647109/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^16 + 28307480408066715571074008904005075216701921247063032952518994713288552208260409092481/17474052145888280869226116421204463645188705208330549158207518030607798213135095744832*y^15 - 352371785076523471673469938012221919002862833598822620670215869721568793401056494691925/8737026072944140434613058210602231822594352604165274579103759015303899106567547872416*y^14 - 3609768336847544109559336736796334263875585878432153425184583047255245137805354979438939/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^13 + 16760291311406878386381570735497911911616449995423478726935084777626587206459548381393205/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^12 + 1204173849529811853847202946049632363139885936910990797297604564888888883907169866053001/52422156437664842607678349263613390935566115624991647474622554091823394639405287234496*y^11 - 650692316399063826662405966175972497458083392247318129055199432130205676015678055336505/26211078218832421303839174631806695467783057812495823737311277045911697319702643617248*y^10 + 12858863627839111271233040929168785820031794046973376144462553314277498192224060550920877/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^9 + 19204241168830824546338611221656463728343575709368538940480522370564771592990250523570831/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^8 + 2042631285483765823840647373758876171961630561827139791392627135464065612196324328187295/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^7 - 4851346997763185624516924943822113018212334463397489569913008294345983757084849387524777/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^6 + 1986662706541763906078345136129339229772463443585794060817234527501335501681718477603763/19658308664124315977879380973855021600837293359371867802983457784433772989776982712936*y^5 - 311262679476802075275139028322613190354573302127609215572302685850713816332480254118321/4914577166031078994469845243463755400209323339842966950745864446108443247444245678234*y^4 + 55742838506679774775141996286901756076162963782273905542165090836509597491272904182869/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y^3 - 10508886355116689140580669154597113993358310473144861157746420379304788943457941461708/819096194338513165744974207243959233368220556640494491790977407684740541240707613039*y^2 + 8176203282092139626462182841663300029787676993731516472757007818946294856102509099228/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y - 3133070615560332632312458776243884120714024346153878429284388407740784285837144766396/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117

69859721868372472389270180334016640367348844874564690395073027255503208003449272069/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^27 + 504376692114067074625147833425754327928766204733858996256564174241209529468188166135/104844312875329685215356698527226781871132231249983294949245108183646789278810574468992*y^26 + 1558002927746150128242110535214643493522043004979490075522393845831829814284941711031/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^25 - 7497253435571982877245065425467083229550349243009677086135213665886383834731678156585/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^24 - 71595471684702264301510092740164380067686323048137057435310324406035212190172503837045/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^23 + 1772013662898410543831563157728059211450745701736535578325294494824853929064214000887/4914577166031078994469845243463755400209323339842966950745864446108443247444245678234*y^22 + 771422359509458099924377183865405207870059338795806895753776734377673692025600352788327/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^21 - 129985513545044713806898846243284983823107044960668182212925580122245201851602731052735/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^20 - 62810217274398040902252974273121835137764780810470962780297539924086919316655736801399/19658308664124315977879380973855021600837293359371867802983457784433772989776982712936*y^19 + 12743480536456390047701635356575582256367503340282166604370578715867604189448145825381141/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^18 + 1429909339239149123394447133437073608327759848284547709794955563383156118967834143944559/52422156437664842607678349263613390935566115624991647474622554091823394639405287234496*y^17 - 7912871141645185067414412357678947550738208502957138975612688816806245048684234784859401/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^16 - 7457708362246100861070759056627186654626835549423624064285398454501135268237411625313509/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^15 + 13236073733386425220620126390013294550493358776004546517087498641151867696508170674076077/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^14 + 42959808167676926104070052825801677212041323088736307206506555313567892617998027098543819/314532938625989055646070095581680345613396693749949884847735324550940367836431723406976*y^13 - 108536124209213610187059015045755075629174230258371633666449437677502930853688984473454905/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^12 - 70772131478710264841028899940409543032229587460449390452126999635180242932230930261270793/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^11 + 22084120164093490545783204598229649545799259100298834921055938076115075586483227969779/4368513036472070217306529105301115911297176302082637289551879507651949553283773936208*y^10 - 12949192400107047905697781516250517678045245661021759584461308573144202986981581218153397/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^9 - 228158140668983013326624143845994516868379562744162114119250986217793075306767089077191477/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^8 - 12110996114170967162474922548752599839871568846837841701642476689285443473540250419270389/52422156437664842607678349263613390935566115624991647474622554091823394639405287234496*y^7 + 22712087731887873021321613304234602351300164127326789466483201831808706076666669577015429/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^6 - 432843993623567402047882264924766766160197716884304871649834106897984437140201544264711/2184256518236035108653264552650557955648588151041318644775939753825974776641886968104*y^5 + 1508193374701284877881372547315694419816769623154883415190233107164019191932235662838147/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^4 - 964662733526710325512118826975702996818052235593156335723879436306012465468634211139419/19658308664124315977879380973855021600837293359371867802983457784433772989776982712936*y^3 + 46611617006430246718582622483747105502594465446656039206971829615373788676994378481386/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117*y^2 - 6568681951327010027102940963214336672802729926234125470025805932296286362146766857390/819096194338513165744974207243959233368220556640494491790977407684740541240707613039*y + 5051743935864284720805105035898150108962107650054827451770633198506562154813390177169/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117

-33199007190494559938371817230368954485092059775634841443138843992514280853110801011/419377251501318740861426794108907127484528924999933179796980432734587157115242297875968*y^27 - 146568443365712262865454079160354466204629001969224455136308856289891974137955336339/419377251501318740861426794108907127484528924999933179796980432734587157115242297875968*y^26 - 757257567437907184420946415018217859525251239496711419266798701941370568918366819863/1258131754503956222584280382326721382453586774999799539390941298203761471345726893627904*y^25 + 2987505538653824857951492874199068687713939053311531256300597460928349868488114936881/1258131754503956222584280382326721382453586774999799539390941298203761471345726893627904*y^24 + 1368130336559582816774533639507378000382435149222900941608597252075879891714856396373/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^23 - 5125661246694511755610646896839689775915702976600620349152147106329364921506911873315/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^22 - 117575555888215883687100785622657879425585054063646271457795433596138916159834832762081/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^21 + 136123419570774645742292451557683737555945928422193357495708159724163565287072806275541/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^20 + 179116154540377764731687155727313900804027910578007793510972441556277798113053681933231/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^19 - 2128221414322828207739668127895070444222070520943932106946598151075740246371917740342511/1258131754503956222584280382326721382453586774999799539390941298203761471345726893627904*y^18 - 228799793563116294034540134921933808803755537939588637154670852347300034903699484600781/139792417167106246953808931369635709161509641666644393265660144244862385705080765958656*y^17 + 4257076850279397342235820161708710838001623565470059857783111862687057888826533484324075/1258131754503956222584280382326721382453586774999799539390941298203761471345726893627904*y^16 + 916338779085068121456063398477427927713534222927147793019550285479604174974668432649039/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^15 - 4363141232755028376306889573842815374453571880956545133619585028705397358085361474683169/629065877251978111292140191163360691226793387499899769695470649101880735672863446813952*y^14 - 698019961727132101669313037113660377486592639518034131081289491886400597496138533532849/78633234656497263911517523895420086403349173437487471211933831137735091959107930851744*y^13 + 25142186192795312827194095462691387329602617407771214454677449716216476692307249580506133/1258131754503956222584280382326721382453586774999799539390941298203761471345726893627904*y^12 + 1504448504617126826969455041432532182178199941188229295266281799238793563839783834668199/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^11 - 176520124730597735238502205369834016419717683927185967033609220442738479684007118032481/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^10 + 3552809405512816664967817083432423410120019053471672612770638796612477139097285653577635/419377251501318740861426794108907127484528924999933179796980432734587157115242297875968*y^9 + 2886769741887870708524992481181887469543870477933570014628873354501026378861163462160943/157266469312994527823035047790840172806698346874974942423867662275470183918215861703488*y^8 - 25164445939403820952153039909720603670011896806736531630616123916924223549229574901745/52422156437664842607678349263613390935566115624991647474622554091823394639405287234496*y^7 - 1352181286287100607447079125536450175776419199172430402080780136783469596022956035927245/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^6 + 37007568957940075210767975449575804688976987199561826244010695850555174219601576789423/13105539109416210651919587315903347733891528906247911868655638522955848659851321808624*y^5 - 536555228631444375996711800883728054760688540781512168260342905882468667395659146277555/39316617328248631955758761947710043201674586718743735605966915568867545979553965425872*y^4 + 9335909790052217001781692656796092832842064109441457389151786308410476630447592333695/9829154332062157988939690486927510800418646679685933901491728892216886494888491356468*y^3 - 19632145870847600400466308480528852719023482978860619315720586632799455552256440818015/4914577166031078994469845243463755400209323339842966950745864446108443247444245678234*y^2 + 188583644382717062536941788794245338684897337196743267418566124338455108010666167033/546064129559008777163316138162639488912147037760329661193984938456493694160471742026*y - 76071485786119632330742975286208966029831008870440870456209304610947431141535670589/2457288583015539497234922621731877700104661669921483475372932223054221623722122839117


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

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

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

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

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

# 1 Loop Invariant
513532558089319814973702337143814166190626994813931103767924000872754922356635285955/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^27 + 605611615327320978744156181063123172392549695262392399242772141701504397000546921273/17474052145888280869226116421204463645188705208330549158207518030607798213135095744832*y^26 + 148898601706248060160653438555597684647946125697396997688182059948995729445772184567/2184256518236035108653264552650557955648588151041318644775939753825974776641886968104*y^25 - 6557089181345791910209468407165330553154563155608395757646692450485438163640905473037/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^24 - 57951722762387397959085975182206460386144184017913623110284246269744877655887513245699/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^23 + 96722441152443517966913036762312012843410054309455037866128992443538978248377740557767/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^22 + 625688898431385639523021681339812529690120994477236001170593043246058029421494759436391/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^21 - 251811192163960711390145047864648754242404501703304688957665549398305505453297987136955/17474052145888280869226116421204463645188705208330549158207518030607798213135095744832*y^20 - 110017443791046425122686665957508886974576422819624168597057019778078370517160180905345/4368513036472070217306529105301115911297176302082637289551879507651949553283773936208*y^19 + 10823390999270004597935357627114302122123615771713375569633946337753589952184130842882355/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^18 + 6616415758402166223936953167673628011648612072273891592298128016387127723112584215621185/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^17 - 8095016179842546778238357221199721385942753492425963120598236184068726058347712841345079/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^16 - 6338322617430083680837797475509849162496277895589915543560657693946431346615159740355891/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^15 + 23665537860379865305758254509587813502001461467805002115676290609564324025250005677255385/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^14 + 33068185580926174233545972886798450443151738060313605847456555876002657133852701344282347/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^13 - 103122746926971538899720469800624135606192860659420260480254938226837142162557954467251363/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^12 - 57492090395492919983740756358913622929629829926006057928748914593104488486407569573854389/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^11 + 14842226106123602253795806185625561465109060416938590460679924194078547683461310900109829/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^10 - 92311328465521866476727914192463283129500400243133717126036125101729538434329810338013839/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^9 - 182034160684584624308922365981532394656362136256208289797470112817740158661963461859809025/69896208583553123476904465684817854580754820833322196632830072122431192852540382979328*y^8 - 42350468748583558289731540190789805795327937726615557555228145070611379716291058343620617/34948104291776561738452232842408927290377410416661098316415036061215596426270191489664*y^7 + 13435109131100750215334385721817106551734671129685397650550221731002858852452846174215555/8737026072944140434613058210602231822594352604165274579103759015303899106567547872416*y^6 - 3324649158303003340680784692316508491503113109817129021317061309200702782815672901262717/2184256518236035108653264552650557955648588151041318644775939753825974776641886968104*y^5 + 244016185658740285044728674056342592773532083388844013803280085519058336282381279870271/4368513036472070217306529105301115911297176302082637289551879507651949553283773936208*y^4 - 32788658274744785882735494810732337190227671870996439529106364914137209225354976366264/273032064779504388581658069081319744456073518880164830596992469228246847080235871013*y^3 - 21762940959947460659295868716941679065456558307060194169170904312213667209260362725483/273032064779504388581658069081319744456073518880164830596992469228246847080235871013*y^2 - 15417365951555173671843640134846948194492467981901152573722712142554655044147383729799/546064129559008777163316138162639488912147037760329661193984938456493694160471742026*y - 6897669084011534894924191913975466069105570031980485487814317246336582179019596476177/273032064779504388581658069081319744456073518880164830596992469228246847080235871013

# 2 Loop Invariant
-11875220746035331979537202713456398624114265646060484434198982517354264715462099952354603249866784803309249257595433488785086413826053442246337932055182370135233074713249/90384277198970511343787425770667166707798306681001227851514762425653180262255613017846038697832669846134530216715027048821991934543114081730508124692532525793091312539510784*y^27 - 109448257582195302259649882162690677348349731270228812072992224712584705354655620041040274656128232474295993108602887096006535897479184696567182744848356224081153379172851/180768554397941022687574851541334333415596613362002455703029524851306360524511226035692077395665339692269060433430054097643983869086228163461016249385065051586182625079021568*y^26 - 23157397066275066541222602970076113960002923595144923372793784794433606520733194359034387429013487358848796302334439444981343708557352103994683519093266382251736943952635/20085394933104558076397205726814925935066290373555828411447724983478484502723469559521341932851704410252117825936672677515998207676247573717890694376118339065131402786557952*y^25 + 630787521336964337905788929431519345157111490366640746197320948110397595412678547703032987000376052273755036081312347341146814091587360556310158462316874260134139338688263/180768554397941022687574851541334333415596613362002455703029524851306360524511226035692077395665339692269060433430054097643983869086228163461016249385065051586182625079021568*y^24 + 2618101588430305895080463604034982666476473526121699801451340867836920046325820660975645844866392397182734740478264892528506536569084991389753202382761053303415259063567445/180768554397941022687574851541334333415596613362002455703029524851306360524511226035692077395665339692269060433430054097643983869086228163461016249385065051586182625079021568*y^23 - 2305249619236584950107720066819810858021540220511275472352684110403539962027896877955069885884848735998513605444591623427440262130417936004457973075376689295572638701789535/45192138599485255671893712885333583353899153340500613925757381212826590131127806508923019348916334923067265108357513524410995967271557040865254062346266262896545656269755392*y^22 - 14228256807474221835459043053064986609990884120891565842584280730282198135558916851122823176667664273595982338553559580481863766083884609345958297453602004570370759777175693/45192138599485255671893712885333583353899153340500613925757381212826590131127806508923019348916334923067265108357513524410995967271557040865254062346266262896545656269755392*y^21 + 26322705885775166296579361261958620745535726787929613746910745705123063746926142911512564362778795450472654940549334653436714323222469975630493874789557404256349810159633249/90384277198970511343787425770667166707798306681001227851514762425653180262255613017846038697832669846134530216715027048821991934543114081730508124692532525793091312539510784*y^20 + 38163940252360111851751767547301613135585039029980985050636849128861914556595107176924764642183945902364752257448301791121959053185703149677135491839942696302729728618304631/90384277198970511343787425770667166707798306681001227851514762425653180262255613017846038697832669846134530216715027048821991934543114081730508124692532525793091312539510784*y^19 - 63199331891114979294383977128730726215826325172371699078563698669134902644620400515524743697377415681520578936934311046998524793064818126872721496972634956163040771705636669/22596069299742627835946856442666791676949576670250306962878690606413295065563903254461509674458167461533632554178756762205497983635778520432627031173133131448272828134877696*y^18 - 560867213994321112549566893606958542578307175695658708896243244066463003989001704328458543449920189155715185594595177115305815899597800278528156199502277210894264140934590089/180768554397941022687574851541334333415596613362002455703029524851306360524511226035692077395665339692269060433430054097643983869086228163461016249385065051586182625079021568*y^17 + 89637424386012638940967901185526141410419535496534551802874517530238605889543524621511399901371340215447073047695036265914641182579682629915132193831814910615208808939074853/20085394933104558076397205726814925935066290373555828411447724983478484502723469559521341932851704410252117825936672677515998207676247573717890694376118339065131402786557952*y^16 + 26485869456130377085973916831521286705259433722757073596652979064124022084883769459962655176402927127113095143321056378219070450680635156839597343119175898524985068152479403/20085394933104558076397205726814925935066290373555828411447724983478484502723469559521341932851704410252117825936672677515998207676247573717890694376118339065131402786557952*y^15 - 364665358101444239136583617822342627387859826300343469802918512288254986420034269304193982935450270148874824308514304780384441478193163873199693940619226018935696479112615907/30128092399656837114595808590222388902599435560333742617171587475217726754085204339282012899277556615378176738905009016273997311514371360576836041564177508597697104179836928*y^14 - 1437226615054060345948606347198194240977018562292389681283504026695733663874664742223007264353873861084948449343182052437924637962789347897096622976275645750130812124674792129/90384277198970511343787425770667166707798306681001227851514762425653180262255613017846038697832669846134530216715027048821991934543114081730508124692532525793091312539510784*y^13 + 282804871519053018939731673442082036424480365834162499390344882814877974272097852325835197474082772938067506546320533702832721998458290868043923019626964615521574806465840209/10042697466552279038198602863407462967533145186777914205723862491739242251361734779760670966425852205126058912968336338757999103838123786858945347188059169532565701393278976*y^12 + 751171942069068268572801382123463635271863539806309435441858035972987667329151064290303571076528118568254362439603800891007951467299209364238496200202543945041674597271319695/60256184799313674229191617180444777805198871120667485234343174950435453508170408678564025798555113230756353477810018032547994623028742721153672083128355017195394208359673856*y^11 - 40902933871276598887613908198467998856270388570137741458089600809159583650116185336394586008471280094097796805277526320759486248487904957753161706112422400320038123447760991/5021348733276139519099301431703731483766572593388957102861931245869621125680867389880335483212926102563029456484168169378999551919061893429472673594029584766282850696639488*y^10 + 2051619928113635537105679611052431152600701314488895667771216667840253445252452684095472247839405569914926818342715360593799133303576799085117019027782484385037840536713642803/90384277198970511343787425770667166707798306681001227851514762425653180262255613017846038697832669846134530216715027048821991934543114081730508124692532525793091312539510784*y^9 + 7944282635587014810145093533956486754991070201111580010983698248214832552213696519018371174994241356186561886765454544693150972659676047578296357632179901110858151341252341761/180768554397941022687574851541334333415596613362002455703029524851306360524511226035692077395665339692269060433430054097643983869086228163461016249385065051586182625079021568*y^8 + 268281809914257151903914909741989221539340943918186994643467559237836986445528627263563355842519331403463859904976996347856619599161705140630900512953359367248900864958635273/15064046199828418557297904295111194451299717780166871308585793737608863377042602169641006449638778307689088369452504508136998655757185680288418020782088754298848552089918464*y^7 - 350757724735423436330781377682030061209967653082591324260125192338262019924953512206466111734580526791420055943476563489873319594922114801359042684714975047409000409640815133/11298034649871313917973428221333395838474788335125153481439345303206647532781951627230754837229083730766816277089378381102748991817889260216313515586566565724136414067438848*y^6 + 160077533768881581438956218236873574864462541271020465868105030485554224679906861333851483172393707700706135215807617979412111208123500353635223554683138294921392215973911983/5649017324935656958986714110666697919237394167562576740719672651603323766390975813615377418614541865383408138544689190551374495908944630108156757793283282862068207033719424*y^5 - 3269941785816062784693056556458777978633466889367016948597610404925125085392777334331400420851438623734059661580736321239662721360558013212805068023719683140212526875967325/706127165616957119873339263833337239904674270945322092589959081450415470798871976701922177326817733172926017318086148818921811988618078763519594724160410357758525879214928*y^4 + 332358473247038392495122183594266434112535317095927888793661741068920601197637239835160629199385685502703928451605078769097825619360648265819109475786843730965336955077515/78458573957439679985926584870370804433852696771702454732217675716712830088763552966880241925201970352547335257565127646546867998735342084835510524906712261973169542134992*y^3 - 1879614950807545037764314710369530816260883131270272977148230042314769223631723629326104681451935304358097649364511908802831968284509608572908809250213087106380343434283679/941502887489276159831119018444449653206232361260429456786612108600553961065162635602562903102423644230568023090781531758562415984824105018026126298880547143678034505619904*y^2 + 1216565074726559168577416293684774829171789375703904593729646865139017539537737767187644180200727099947335722703552766760580493988754246597703591355730988060451963453194847/1412254331233914239746678527666674479809348541890644185179918162900830941597743953403844354653635466345852034636172297637843623977236157527039189448320820715517051758429856*y + 80435232123544545399301054544767755772200426316629229978589762234603878727062400538425624583932960209633017740524909849910666921506643792961811975754156276874924957713675/78458573957439679985926584870370804433852696771702454732217675716712830088763552966880241925201970352547335257565127646546867998735342084835510524906712261973169542134992

# 3 Loop Invariant
-324974416122866342591330987420804472224409870841448674213829279085806145824393821542814053043759098854571582553674543557779579304703331890453212816469443456502306229422446268115298890759762665881002393077523771297/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^27 - 7862794643541879793885994123080287718765682620517570152363679825421020096364025873422970370474248061037460293976967294183544421411345876168226746638165144232449861850132958462127319908505165938522945298719412139/340481683759605668115058119787776400729467512503487408242532062776532301116800977858377285621952398260698013074465422473065636947228472361709344246637401028274100961643836100143343110167600675772842906397298583289856*y^26 + 2026670742723143559050239629049992455299153776859516545228170350908459629268644917033849754242105048788714931189207521315851592592753626366972847526775962314604682291667129957412771078343675742678980861945564318907/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^25 + 21173665970519798471022579507518688429695498943723821138728732748565674215574220514562324830493224994194995427880497048196811684434366857532752759146802255371096261681315899591289703364302306167917098121412233600791/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^24 + 4216618574234193885825026548028825209983195904797413881978552534768279777558289359858085873467438239174363499159736893818865852591252945431597080129149451115186569895330696766738526577057588126966960833786892978637/4596502730754676519553284617134981409847811418797080011274182847483186065076813201088093355896357376519423176505283203386386098787584376883076147329604913881700362982191787351935131987262609122933379236363530874413056*y^23 - 19514952117754528987804519950718305089230393914368037706525205613939054295324401243315561957085803947163173749351888033434842508060941376982782318363658472721977128975795461629974474872878489330500559341857410815217/2298251365377338259776642308567490704923905709398540005637091423741593032538406600544046677948178688259711588252641601693193049393792188441538073664802456940850181491095893675967565993631304561466689618181765437206528*y^22 - 277170272742989415122344004512338456626291715870730835716706914273830178826595499990434792526703542675799775274819868739240301510015998256043371917728713089981956474629748134958781174110583498616132406628249663823969/13789508192264029558659853851404944229543434256391240033822548542449558195230439603264280067689072129558269529515849610159158296362753130649228441988814741645101088946575362055805395961787827368800137709090592623239168*y^21 + 1523382566941632765997054957971673639631108186081831940505739266293611904397256567043872531267800719334209415318271488511547008116550684815268032280003147872750784691297607466114180192568637959372553924608163165472659/13789508192264029558659853851404944229543434256391240033822548542449558195230439603264280067689072129558269529515849610159158296362753130649228441988814741645101088946575362055805395961787827368800137709090592623239168*y^20 + 772688339922271705115698550314460061257684965248046379137654054964207337320570666970599622948828423517041596704903811113335985396778558958517828528405786732349207249421893423427050562245456013103418221963149035485421/13789508192264029558659853851404944229543434256391240033822548542449558195230439603264280067689072129558269529515849610159158296362753130649228441988814741645101088946575362055805395961787827368800137709090592623239168*y^19 - 9652651734986709620030649515216432720421609097722221604262737674785460507880009291660032511627928766789974100059943744066886226279906086765425384464994337754112092039816022478050227488687780837590231539537820145841219/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^18 + 7893364640631309887760819019187886797549154673477026053604020795838007968539982255488831239259307937429906454985237891284853872804631539616028537965027094632823175154635097833944666115995362552834717624421914251460277/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^17 + 49187396182614778119099350255497759360645392792495675175407163882282125548310792469343588053205327956822496394197831974609668382339351667949873359724548556410773507574856090856584674270651544687200072359458707880707917/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^16 + 25859021445053569948409056686241168822750509032566132032495579614676907763018382308271865642749567653009262305260844036560845002071441412250620078573656912133879376391293293989819107798635642829883800362742453002893/63840315704926062771573397460208075136775158594403889045474761770599806459400183348445741054116074673880877451462266713699806927605338567820502046244512692801393930308219268776876833156425126707408044949493484366848*y^15 - 2052368105718866696168688497068034204059367409562425146896720828935861837960289570271942035846963545086258452697394853017107850945945855103966109727387761291492839776823298006830436426935673433171417799791693951997601/1532167576918225506517761539044993803282603806265693337091394282494395355025604400362697785298785792173141058835094401128795366262528125627692049109868304627233454327397262450645043995754203040977793078787843624804352*y^14 + 9801473659371444630718806807495310420988177089011942735029412279522271006111681080242676144530864086257315474161087043396074664572380774278353001061422756936635881414778407648903026867698585979228660508576283118496169/6894754096132014779329926925702472114771717128195620016911274271224779097615219801632140033844536064779134764757924805079579148181376565324614220994407370822550544473287681027902697980893913684400068854545296311619584*y^13 + 271063754783087400261990424420487777781392808613658150034438781252898929353868306706816116702423846326728287539894280600871158698252989871439683962536351906824721996372736743306692212019513903365829935571771633927346885/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^12 + 8588043238572669853476157401415401783202383050430421623334445410764872310890194710606435782603902448630297424233263552788968578516759986940243424806247798987280269410639099166370024466982071227446966906235061042258519/4596502730754676519553284617134981409847811418797080011274182847483186065076813201088093355896357376519423176505283203386386098787584376883076147329604913881700362982191787351935131987262609122933379236363530874413056*y^11 - 4253319179981113513061679561593981105767849062717009731320615245471172262028730905838362747047165778518435054207236504841700981575246806991792413704337311033334705174400073088358055521505204513850503928306881656768675/1149125682688669129888321154283745352461952854699270002818545711870796516269203300272023338974089344129855794126320800846596524696896094220769036832401228470425090745547946837983782996815652280733344809090882718603264*y^10 + 71161493165553382878718674896964244583592087627430100378278037816179852826871193333282771490646869719135556953208786435566812569904656651262884850690358393645173761200953587026440106214391832820937657379625935742437417/27579016384528059117319707702809888459086868512782480067645097084899116390460879206528560135378144259116539059031699220318316592725506261298456883977629483290202177893150724111610791923575654737600275418181185246478336*y^9 + 37969134005252123120536334994465511804910104847351063185523190012800061041976734060341266087787429160467503254691047710813332654729948325926695634413769723951579234943787854006833058903921370480888515677213059156555393/13789508192264029558659853851404944229543434256391240033822548542449558195230439603264280067689072129558269529515849610159158296362753130649228441988814741645101088946575362055805395961787827368800137709090592623239168*y^8 - 59400939540345895571509619142756059356841922276374709074556411562576116371380744538180122389262067642715808108656916563860951663309077163374115855147004259105360835140492152132384138052236459745602637790842094572600163/6894754096132014779329926925702472114771717128195620016911274271224779097615219801632140033844536064779134764757924805079579148181376565324614220994407370822550544473287681027902697980893913684400068854545296311619584*y^7 - 24987828388790349970426128548531533859807565468718506754613109904949719358799911058881071090899116612940230002296570970948987550674132104582430962130266172179130773343451973462951613453568522762913601722514919881595257/1723688524033003694832481731425618028692929282048905004227818567806194774403804950408035008461134016194783691189481201269894787045344141331153555248601842705637636118321920256975674495223478421100017213636324077904896*y^6 + 985413339659682360056562532006957741317212789741438525412257510769623177564821119185493862092663042310783364153342543299149025068409355039172967232150430725419164249640724214544619920420045394649164754707901890137337/430922131008250923708120432856404507173232320512226251056954641951548693600951237602008752115283504048695922797370300317473696761336035332788388812150460676409409029580480064243918623805869605275004303409081019476224*y^5 - 1947616458303300716996068338432229032411274462009897771902214430991600952968246675641915486206764491419213217552333246923639445626738668959278064427825788138045504043836652979629908699382393143759421330636670048289059/861844262016501847416240865712809014346464641024452502113909283903097387201902475204017504230567008097391845594740600634947393522672070665576777624300921352818818059160960128487837247611739210550008606818162038952448*y^4 - 923165343432832010573361189281388499239026279704642862032881274446379475228220258783894766694810365975460238722197721308998293584095033436798922486523385919645555982235690055845282676710342640441309367368170269039205/861844262016501847416240865712809014346464641024452502113909283903097387201902475204017504230567008097391845594740600634947393522672070665576777624300921352818818059160960128487837247611739210550008606818162038952448*y^3 - 196705493112226352609615885312447350260305747870583019393170739300907771558583193382089353583918792901140077047149715347620141538885735781873970070863441014813276747503963953824240517281076614618758298445596977639547/143640710336083641236040144285468169057744106837408750352318213983849564533650412534002917371761168016231974265790100105824565587112011777596129604050153558803136343193493354747972874601956535091668101136360339825408*y^2 - 11560490681134959924286084104350283949462221082165852627573129126660392929795391220539709638916552487880146736894707507991741586259141642426074156276312126500362434647723678206864891636370662284595355804466785609875/107730532752062730927030108214101126793308080128056562764238660487887173400237809400502188028820876012173980699342575079368424190334008833197097203037615169102352257395120016060979655951467401318751075852270254869056*y + 7608549465693154445588219071677896419723884930006704878831350149358061036506486810256334524663146609975098108756640188951592086585905533167516357870988982077527245296664879100694907441886202868503206940319175704013/107730532752062730927030108214101126793308080128056562764238660487887173400237809400502188028820876012173980699342575079368424190334008833197097203037615169102352257395120016060979655951467401318751075852270254869056

# 4 Loop Invariant
212912916208916680485775361149760376421844841481389157571485841567029549100563374259641018361794632276129136014518817464961040255575941413365475715039500775547276553599809048843366199853551685698248378238872426843276581875661660885683566683570446723109403160671092623427285155911578743075642539065143047/356630139500968410008882183139486279820674475904777354841464215605790215035758670933228759688650330374893510557303292874040218401809991504763211137485287741321365249534856094527120137917692307332863631956354286462481717942710998970802230904776182948506600080072040957602197167789108126284799540259309486080*y^27 + 75828389516280669151728426845772183690723246478927598107445204704458476630396388082005101148192289152022076392233310043230418034611026181868124557351012410767901448755178040372906182496650207401460294457772323638221638099724898417260917462171128565008619333240176377765301008163994809997091311894608767/19812785527831578333826787952193682212259693105820964157859123089210567501986592829623819982702796131938528364294627381891123244544999528042400618749182652295631402751936449695951118773205128185159090664241904803471206552372833276155679494709787941583700004448446719866788731543839340349155530014406082560*y^26 + 1057850261593214006585369883512089086159900478611014073884256429761699401193286621874451985961449889554203856793325106814890449556153371235995793760078738938003455900873497967709373411573810539111987815712664611900834290287930775845266628714745828450176491890816299126540721750105866161166088774172048521/89157534875242102502220545784871569955168618976194338710366053901447553758939667733307189922162582593723377639325823218510054600452497876190802784371321935330341312383714023631780034479423076833215907989088571615620429485677749742700557726194045737126650020018010239400549291947277031571199885064827371520*y^25 + 636325325694933375530101294719738972696164835352700571458628722980291175604446085387177332437275006957553680552056411763414358448398262434211409542616061101717841516315737768061251314481214395681876023942080120020228214619837728539440018256281673725901435183041531401077649160808960918296709824324703481/178315069750484205004441091569743139910337237952388677420732107802895107517879335466614379844325165187446755278651646437020109200904995752381605568742643870660682624767428047263560068958846153666431815978177143231240858971355499485401115452388091474253300040036020478801098583894554063142399770129654743040*y^24 - 7847292104986560656765131639816286761752226633812774564808580623696930785406344834571343242273505708200942553095444034766444853272368869091775098678858772377439139171639971158653626539155149027007726261455985091338724490037871291288526602043420349036521084276303559721423285113704934372481353293929154053/118876713166989470002960727713162093273558158634925784947154738535263405011919556977742919896216776791631170185767764291346739467269997168254403712495095913773788416511618698175706712639230769110954543985451428820827239314236999656934076968258727649502200026690680319200732389263036042094933180086436495360*y^23 + 801440796179916503456600690710331707534258556596031372983624785206939291631689807729413110267037367355096369983190059728269457686804788436046293646149790408855889478541678252876812475910435297795761327398094347144103738350460903297331761966770414237759753899007328163105831597801080214156315030767456607/7429794572936841875185045482072630829597384914682861559197171158453962813244972311108932493513548549476948136610485268209171216704374823015900232030943494610861776031976168635981669539951923069434658999090714301301702457139812478558379810516170478093887501668167519950045774328939752630933323755402280960*y^22 + 295424607982115486288570616862098181841170347234005313838135770888927599467227549015354245972212257047184360858103698723956760596764731415125505552772491640984683374576503815751705791018235495571312627479833477137108042009581203917261441393320968266429944468437562237917985010400034021812489236975351850309/178315069750484205004441091569743139910337237952388677420732107802895107517879335466614379844325165187446755278651646437020109200904995752381605568742643870660682624767428047263560068958846153666431815978177143231240858971355499485401115452388091474253300040036020478801098583894554063142399770129654743040*y^21 + 36502714363456587077494805721227816905455985034232610456431940491648242906302352784087915891645610041668529635806111091036043738218721515234273010036509221884344476400666924919073140097997164365539381427456747347941532078360625157544853229019575738657985609419089185682901557862324435822440283355433228397/22289383718810525625555136446217892488792154744048584677591513475361888439734916933326797480540645648430844409831455804627513650113124469047700696092830483832585328095928505907945008619855769208303976997272142903905107371419437435675139431548511434281662505004502559850137322986819257892799971266206842880*y^20 + 2327370960542426363373958074572899419576065174533603247242573146456610148261795682015139081008398208399350997949097875627757054712394862281298450644322634780842037858704114123591236777599558160927588586416761224949879292628592210217431042811713618936348118718445759868738814918717625421606978126760899/10513860244721946049790158701046175702260450350966313527165808243095230396101375911946602585160681909637190759354460285201657382128832296720613535892844567845559117026381370711294815386724419437879234432675539105615616684631810111167518599787033695415878540096463471627423265559820404666415080785946624*y^19 + 4206922064075299181290947783809704861012852520097178912760477188768495138134854702633739288447091792235196282817449374214854975960990708018777050607651774944209018790034551103964344654062569669758768950257765385124959618323234906398877515563094724114979342442332111889184504162746086364297880675997591225903/356630139500968410008882183139486279820674475904777354841464215605790215035758670933228759688650330374893510557303292874040218401809991504763211137485287741321365249534856094527120137917692307332863631956354286462481717942710998970802230904776182948506600080072040957602197167789108126284799540259309486080*y^18 + 3129201845286886922965223244797432326682726353027964296870746269639164064271139790502207254851854874543829772808479647766083613401342337061256274572719518045928650992010696771435296417000876000484371618526745057904845800733267315611473732697932067866391673841514931410358389791450850976744402069972632078827/89157534875242102502220545784871569955168618976194338710366053901447553758939667733307189922162582593723377639325823218510054600452497876190802784371321935330341312383714023631780034479423076833215907989088571615620429485677749742700557726194045737126650020018010239400549291947277031571199885064827371520*y^17 + 1349495745336375121855714993877868278881440835219427474427448935464144370890514276934396328403195749244502555421862448962089598541518750602195058619459939171332173267717171912809400598584114827901533938069597153831175251727029020193184521837904263722825316115453538492643880289954798911156232858788666239737/35663013950096841000888218313948627982067447590477735484146421560579021503575867093322875968865033037489351055730329287404021840180999150476321113748528774132136524953485609452712013791769230733286363195635428646248171794271099897080223090477618294850660008007204095760219716778910812628479954025930948608*y^16 + 554505285129622057655427553764715499278298999824328986041387727712331537592989207530142451058384859492166222737572670435569104849625944202973669194612261667972714862420655432603361076795755040860700728340955628096308531249132607277892327269116729749429458702272720120559125955737201913597393413905755664827/13208523685221052222551191968129121474839795403880642771906082059473711667991061886415879988468530754625685576196418254594082163029999685361600412499455101530420935167957633130634079182136752123439393776161269868980804368248555517437119663139858627722466669632297813244525821029226226899437020009604055040*y^15 + 1028569975635830416073357667681315552297240215245631904052246605467314756732950541671942400041214307772145297331686111600883301364768290630826961873807931534565940709116519976838550662595412147225008811202880767108951310901164681286508084572415981666723277444032528832198109940732495722213937028866856977939/9906392763915789166913393976096841106129846552910482078929561544605283750993296414811909991351398065969264182147313690945561622272499764021200309374591326147815701375968224847975559386602564092579545332120952401735603276186416638077839747354893970791850002224223359933394365771919670174577765007203041280*y^14 + 8382675535028500306456672142522897119948252071633860784375882100531921146741116652826709205580646206691818903459083546503853011795758030065196408278720320830519308450517907067914160386781098719299676050321906706947694897669374291077198480344985061351342571545508889599514799451039639092964175646215493563869/35663013950096841000888218313948627982067447590477735484146421560579021503575867093322875968865033037489351055730329287404021840180999150476321113748528774132136524953485609452712013791769230733286363195635428646248171794271099897080223090477618294850660008007204095760219716778910812628479954025930948608*y^13 + 86070392659472283382350495241123050315855911705561384936897610797945063344959586242459675743238604838388683554340422557194998016980312019913535368134545198872079172319056443217420790002789002585954605052664888716689444198428528421309172611187267148024562309596730362156643959503372233183563707101691855833101/356630139500968410008882183139486279820674475904777354841464215605790215035758670933228759688650330374893510557303292874040218401809991504763211137485287741321365249534856094527120137917692307332863631956354286462481717942710998970802230904776182948506600080072040957602197167789108126284799540259309486080*y^12 + 5782645791505243409596296815138626288535204956714515865970683369956393152731831250558820009590894379511857273297227098983610974072465993722531966211112995333662325307398206821702145182020035514670505011775192270149512802224822991132004507656731490979236235284405117537388114414796509508907582698650517814427/23775342633397894000592145542632418654711631726985156989430947707052681002383911395548583979243355358326234037153552858269347893453999433650880742499019182754757683302323739635141342527846153822190908797090285764165447862847399931386815393651745529900440005338136063840146477852607208418986636017287299072*y^11 + 283607705801539872781472369570260961910725396827975869486569074330380115159158080422077229632006238130764083845398647442457640605472112675081435412984365270633966238765310812869208011347414340090412661783335919969764729956886205763519968144663148498597773562450586874285384616902168513422987988807371210531/928724321617105234398130685259078853699673114335357694899646394806745351655621538888616561689193568684618517076310658526146402088046852876987529003867936826357722003997021079497708692493990383679332374886339287662712807142476559819797476314521309761735937708520939993755721791117469078866665469425285120*y^10 + 109043830136744814086560582018094079903718789189727259704049300553050682250289225051956305227942852543130769054813260268438083390047268123675178909867802872799651166186371057844113670705865020316663091286985096771882560190302897301321616805160709341433478481006188923430308833312867130729947220164039029915409/356630139500968410008882183139486279820674475904777354841464215605790215035758670933228759688650330374893510557303292874040218401809991504763211137485287741321365249534856094527120137917692307332863631956354286462481717942710998970802230904776182948506600080072040957602197167789108126284799540259309486080*y^9 + 62324703687499998412771854128823889626394255380159246174328832988876676457682464086521863463052276993315702040599227532505628447169698288925540010993815590804346782316271113970239131625506299470046370509613434726632555770840461218377007665238371839078042088057244487111190679183398667097909099074279307732489/356630139500968410008882183139486279820674475904777354841464215605790215035758670933228759688650330374893510557303292874040218401809991504763211137485287741321365249534856094527120137917692307332863631956354286462481717942710998970802230904776182948506600080072040957602197167789108126284799540259309486080*y^8 + 3578014964685319426819054870623085792372814399682530844512200474194943242989690961095929922155964346178807861578350674301458758437680943907273540733867762789685605133445856544573844066019552940796774645051726108231190803212934764271180178995338018510708099469476749152059852492606549110787248518957199707923/89157534875242102502220545784871569955168618976194338710366053901447553758939667733307189922162582593723377639325823218510054600452497876190802784371321935330341312383714023631780034479423076833215907989088571615620429485677749742700557726194045737126650020018010239400549291947277031571199885064827371520*y^7 + 7802637444925419393708065349089281665630536451049785500671441865865339642528916598619148259174528573859613129120355114087825106488120443689810357562452307568699531650377023853971466726899462161692169344899410041531423108523302916322670414114287176094369441410571399212982626148390608585860054480345507577921/89157534875242102502220545784871569955168618976194338710366053901447553758939667733307189922162582593723377639325823218510054600452497876190802784371321935330341312383714023631780034479423076833215907989088571615620429485677749742700557726194045737126650020018010239400549291947277031571199885064827371520*y^6 + 813258036282894965977617829032605722085000688894470869358267014266750561286534765330382762606656806371017333690210954329652863347928835802095691840765453724823548292094184409160895308729541640690958594721851452977891018447944751748800583151005889353605873654845259908297556170402170119199333120045986002807/44578767437621051251110272892435784977584309488097169355183026950723776879469833866653594961081291296861688819662911609255027300226248938095401392185660967665170656191857011815890017239711538416607953994544285807810214742838874871350278863097022868563325010009005119700274645973638515785599942532413685760*y^5 + 592215592467029148688291165945445476937205172710797265426649013851289518455517348385265285186996126293739045956809199898926733727095676774518060072236313900532611745942374959147226021593806243741054469311367391128283075252608275963870213947675020181772193400324792281102145367956406181275608918932700676403/22289383718810525625555136446217892488792154744048584677591513475361888439734916933326797480540645648430844409831455804627513650113124469047700696092830483832585328095928505907945008619855769208303976997272142903905107371419437435675139431548511434281662505004502559850137322986819257892799971266206842880*y^4 - 9303646762075111031929476340775118736689031584736776207642223509248486551391209632571827009809652764284721215276449861176119248827046244142039200468701081341182693665911815734242427995922869289778053190294343802955179671957379393642783532231185264614785711308498742201858945821724917014660189133386313361/5572345929702631406388784111554473122198038686012146169397878368840472109933729233331699370135161412107711102457863951156878412528281117261925174023207620958146332023982126476986252154963942302075994249318035725976276842854859358918784857887127858570415626251125639962534330746704814473199992816551710720*y^3 + 1436067084921477670679341079305950614631251815945125488419971278186735436302255953748253694021018532684037754905979634693993479670708662480007446549820224491226060387701731699349148202810120891001254034227290228072055855856828589952535879300765730378549934104932205586184851848271246383325596674208037813/464362160808552617199065342629539426849836557167678847449823197403372675827810769444308280844596784342309258538155329263073201044023426438493764501933968413178861001998510539748854346246995191839666187443169643831356403571238279909898738157260654880867968854260469996877860895558734539433332734712642560*y^2 - 37478668469898419949932345324279905872905019487599272258034836279196872602902297051458434474323936517155579038731440236484283733162836085480734808230210617702145979734101125938142215258082244344583320906829200116498525152631535383174339671169769581564943862006474041239961271488827153061732221375481203/139308648242565785159719602788861828054950967150303654234946959221011802748343230833292484253379035302692777561446598778921960313207027931548129350580190523953658300599553161924656303874098557551899856232950893149406921071371483972969621447178196464260390656278140999063358268667620361829999820413792768*y + 548216490534896103883233565607358487935700171534513785563613893118118314794448745625847920837672045857362285029094983295995638429022234055004254213093642166501682722148490687013545329055749031442914853065798434999548371459730727812740501044015962032452233926037788904112827000635732476083798411279926787/1393086482425657851597196027888618280549509671503036542349469592210118027483432308332924842533790353026927775614465987789219603132070279315481293505801905239536583005995531619246563038740985575518998562329508931494069210713714839729696214471781964642603906562781409990633582686676203618299998204137927680