# Manifold: Census Knot K8_174

# Number of Tetrahedra: 8

# Number Field
x^27 - 9*x^26 - 7*x^25 - 23*x^24 + 283*x^23 + 306*x^22 - 462*x^21 - 777*x^20 + 7767*x^19 - 5282*x^18 - 14010*x^17 + 3679*x^16 + 47691*x^15 - 46713*x^14 - 110298*x^13 + 217074*x^12 - 50041*x^11 - 190890*x^10 + 251395*x^9 - 105036*x^8 - 67390*x^7 + 111948*x^6 - 67961*x^5 + 22293*x^4 - 3764*x^3 + 157*x^2 + 33*x - 1 

# Approximate Field Generator
0.307511881525001 + 0.352293631773120*I

# Shape Parameters
23455228318433231991035707665081538870288122/1281602105376969091162643792692743273533877091*y^26 - 39032700246474114405047427011187830588912971/233018564613994380211389780489589686097068562*y^25 - 133535575793534574070302376020198171916556035/1281602105376969091162643792692743273533877091*y^24 - 501329199335465818448819436522573657792654960/1281602105376969091162643792692743273533877091*y^23 + 13482955873802592735717001809330642562204668811/2563204210753938182325287585385486547067754182*y^22 + 6221448943149921216988244922764304948573713278/1281602105376969091162643792692743273533877091*y^21 - 24672717622976629182241305373420436064631113961/2563204210753938182325287585385486547067754182*y^20 - 34738037547040338419775229756814068313126269177/2563204210753938182325287585385486547067754182*y^19 + 369839058851369257797363363859541700447683356643/2563204210753938182325287585385486547067754182*y^18 - 301141097879822568161973205312018979902944748613/2563204210753938182325287585385486547067754182*y^17 - 321020643030595930821345271578940456681210691378/1281602105376969091162643792692743273533877091*y^16 + 271920601506374065705587727824366072499394197007/2563204210753938182325287585385486547067754182*y^15 + 1123819007356759834899549771602865603134439508839/1281602105376969091162643792692743273533877091*y^14 - 1253197933996443070383828714266307426071553969781/1281602105376969091162643792692743273533877091*y^13 - 4968058877149630721508429161668715039591473855111/2563204210753938182325287585385486547067754182*y^12 + 11020235871615782459027889674458394748178339968805/2563204210753938182325287585385486547067754182*y^11 - 1776688724842748054737164492187499246601009120161/1281602105376969091162643792692743273533877091*y^10 - 406436052843813454932209442512753745168303574874/116509282306997190105694890244794843048534281*y^9 + 6536154730552631985713266901602863744540638379555/1281602105376969091162643792692743273533877091*y^8 - 6354834830205550399275585219365506355889446125133/2563204210753938182325287585385486547067754182*y^7 - 2736687703748124341806614267908471718967925901913/2563204210753938182325287585385486547067754182*y^6 + 2876620290509928143944566531707961908321480095309/1281602105376969091162643792692743273533877091*y^5 - 3848268377237110595457063752568271449899671585139/2563204210753938182325287585385486547067754182*y^4 + 711220111733970809306523915505354736590253620599/1281602105376969091162643792692743273533877091*y^3 - 13681731906429014249686514856272700561388362280/116509282306997190105694890244794843048534281*y^2 + 16122803959275149796313745639409794842977108319/1281602105376969091162643792692743273533877091*y + 908853817366407978842161994237185577749099601/2563204210753938182325287585385486547067754182

-1654350393387530203483125591148300969318654581/2563204210753938182325287585385486547067754182*y^26 + 1357823999738603481393654703242261072873497043/233018564613994380211389780489589686097068562*y^25 + 5575546525500748082963178720457520324376269693/1281602105376969091162643792692743273533877091*y^24 + 37782987896326125531971283844370525950495943293/2563204210753938182325287585385486547067754182*y^23 - 469183819727341979222622181168014321632764556343/2563204210753938182325287585385486547067754182*y^22 - 492748264502781649530119429082049454049303632975/2563204210753938182325287585385486547067754182*y^21 + 388376389815669398221590256478021828861182921489/1281602105376969091162643792692743273533877091*y^20 + 630378769019567169462073639474404708547981747738/1281602105376969091162643792692743273533877091*y^19 - 6442038771493993714436605848102833848505558199902/1281602105376969091162643792692743273533877091*y^18 + 9108117836724303792595232736304867420388816853485/2563204210753938182325287585385486547067754182*y^17 + 22876307913479475582636616326675677600251405931197/2563204210753938182325287585385486547067754182*y^16 - 6728396383333915480257109592992480179485751586255/2563204210753938182325287585385486547067754182*y^15 - 39312852004769164434304077419814627727638280712732/1281602105376969091162643792692743273533877091*y^14 + 79527307941025218065106345282516314386051190459931/2563204210753938182325287585385486547067754182*y^13 + 89982571910932460121507064511971342730882927517788/1281602105376969091162643792692743273533877091*y^12 - 364084516171354362112404433734594999653469098371105/2563204210753938182325287585385486547067754182*y^11 + 46902791953560590685763488690555261776926566928313/1281602105376969091162643792692743273533877091*y^10 + 14192980415639097474246341595905644251819816123944/116509282306997190105694890244794843048534281*y^9 - 424837010308222051513148965722007704575565847037723/2563204210753938182325287585385486547067754182*y^8 + 93419328690478943212240056697529334051217739664513/1281602105376969091162643792692743273533877091*y^7 + 105131838180180110013452248368118495966494686088457/2563204210753938182325287585385486547067754182*y^6 - 187937905542695355561335557945778468632252668935701/2563204210753938182325287585385486547067754182*y^5 + 118184547666029796446805831363445605992508044169959/2563204210753938182325287585385486547067754182*y^4 - 20364350848512660710853191278018672479460219079686/1281602105376969091162643792692743273533877091*y^3 + 347700686553572968387433298004223378258905594731/116509282306997190105694890244794843048534281*y^2 - 560731113703280555439954044648282664533572739377/2563204210753938182325287585385486547067754182*y - 22347955063238197122315653229074342301561384535/2563204210753938182325287585385486547067754182

-149069764027039902695899241770411774113948411831647060809384539571/1491130818460749461442497217110493894737382003504759885245013024938*y^26 + 117014298394918822870893169856472559098601073353490346635927764577/135557347132795405585681565191863081339762000318614535022273911358*y^25 + 764127742922014178384396157106406933147048249017497512763571939431/745565409230374730721248608555246947368691001752379942622506512469*y^24 + 3848705549126289102524239262305471042455562738146947383657335471055/1491130818460749461442497217110493894737382003504759885245013024938*y^23 - 40793925829734320542017580322215709587100412736813578309564293522329/1491130818460749461442497217110493894737382003504759885245013024938*y^22 - 60914655502696771130707025392681014851093107092470887683748531816385/1491130818460749461442497217110493894737382003504759885245013024938*y^21 + 25470699277921678057929266081545991893506558331476165855261746976645/745565409230374730721248608555246947368691001752379942622506512469*y^20 + 68073509488495033741255592544848940838899247493626907990722678354503/745565409230374730721248608555246947368691001752379942622506512469*y^19 - 556796666033768672607888084451634328456624933523674948749358111604662/745565409230374730721248608555246947368691001752379942622506512469*y^18 + 372608879745429839412396063560756181431255690659873984104341211617229/1491130818460749461442497217110493894737382003504759885245013024938*y^17 + 2338465719690683128694039436858850864686751876898868658079598087430005/1491130818460749461442497217110493894737382003504759885245013024938*y^16 + 160655490751693073795698350335310292592271589030489601835733151659973/1491130818460749461442497217110493894737382003504759885245013024938*y^15 - 3556011645085463663446767516331868463555629652278824364567280941555556/745565409230374730721248608555246947368691001752379942622506512469*y^14 + 4365646698628246989084529387337144962755448195260247151611651837017457/1491130818460749461442497217110493894737382003504759885245013024938*y^13 + 9360128150061572780361970463178669209539778741488463146941414073153138/745565409230374730721248608555246947368691001752379942622506512469*y^12 - 26581622441090919598619810160874778962027149461809077824505287141746607/1491130818460749461442497217110493894737382003504759885245013024938*y^11 - 1449500121824647717304869080856873818048080477262315837343698856598884/745565409230374730721248608555246947368691001752379942622506512469*y^10 + 1376617858467450468067521463080148871080477102507053980898821896085763/67778673566397702792840782595931540669881000159307267511136955679*y^9 - 28948901143293715935619642791329534361150388852715255627494918524918203/1491130818460749461442497217110493894737382003504759885245013024938*y^8 + 2643817424359791239921475183510220131507858005941255669501645844137193/745565409230374730721248608555246947368691001752379942622506512469*y^7 + 13791743225234737593112823592544438722008747875584682033019591861513337/1491130818460749461442497217110493894737382003504759885245013024938*y^6 - 291323463451324364337752272008771927181500505915514259820783502502535/31726187626824456626436111002350933930582595819250210324361979254*y^5 + 6169449353350502735614993403245675640554510366742640069594982710750811/1491130818460749461442497217110493894737382003504759885245013024938*y^4 - 667482555793172276027712801263323382811792618741806654250944352785233/745565409230374730721248608555246947368691001752379942622506512469*y^3 + 4152791419017786830053171709988044200377889403615203308393492657099/67778673566397702792840782595931540669881000159307267511136955679*y^2 + 13892253116385932947746748269380995787402365972496091624684294197097/1491130818460749461442497217110493894737382003504759885245013024938*y + 1119236582283291300383746598300198724425282349391295478307039071365/1491130818460749461442497217110493894737382003504759885245013024938

-24561885684973040455251206311703274082230027927475861242764861541/31726187626824456626436111002350933930582595819250210324361979254*y^26 + 20183480049005684557225823487278547622989612242585223546143279255/2884198875165859693312373727486448539143872347204564574941998114*y^25 + 81911477591337432156476200782237198764771646398749307509565965230/15863093813412228313218055501175466965291297909625105162180989627*y^24 + 553560595683258467327097648337148471762249645349015349092572511553/31726187626824456626436111002350933930582595819250210324361979254*y^23 - 6979003347303791780852513503595625051158335111409311990676454287715/31726187626824456626436111002350933930582595819250210324361979254*y^22 - 7258666314347332561003948642928520952360214421148807223843033782997/31726187626824456626436111002350933930582595819250210324361979254*y^21 + 5894408337403823605063339330308188681806197329515612641714310169462/15863093813412228313218055501175466965291297909625105162180989627*y^20 + 9436121424825148030523527292891373298468869478218870189665771718429/15863093813412228313218055501175466965291297909625105162180989627*y^19 - 95837785413184909453433295590789032160300033659411964253764262764405/15863093813412228313218055501175466965291297909625105162180989627*y^18 + 136697737794125994792904510099293511113919883336383664161187238613271/31726187626824456626436111002350933930582595819250210324361979254*y^17 + 343028632110248041677731737509347336740515278335959971114184486558007/31726187626824456626436111002350933930582595819250210324361979254*y^16 - 104885102534624048873009577792075728466618406402561107755890227586461/31726187626824456626436111002350933930582595819250210324361979254*y^15 - 588071498505329340259681200385982793982391857518159270896885143833019/15863093813412228313218055501175466965291297909625105162180989627*y^14 + 1191577399773249503591426430991042923578941867494296483419937879189025/31726187626824456626436111002350933930582595819250210324361979254*y^13 + 1344947812097576117684789015206857847047982848825706774322151332445234/15863093813412228313218055501175466965291297909625105162180989627*y^12 - 5451606030733690653679767264729436481371487701488228760220643679961959/31726187626824456626436111002350933930582595819250210324361979254*y^11 + 685138518544609133172464276213773313184928181403747127707040230525105/15863093813412228313218055501175466965291297909625105162180989627*y^10 + 214949815280340537128262432341139478806380655809062831376592595574415/1442099437582929846656186863743224269571936173602282287470999057*y^9 - 6341655338842427180855554485556413175611394436479633478816012553310949/31726187626824456626436111002350933930582595819250210324361979254*y^8 + 1359915556880879940627974251201235281485456122353802667624457495029524/15863093813412228313218055501175466965291297909625105162180989627*y^7 + 1643630428774748005534160732185276167841154280252628893620607549499883/31726187626824456626436111002350933930582595819250210324361979254*y^6 - 2824563369820454178486940335254200635940622045913292127326258128677709/31726187626824456626436111002350933930582595819250210324361979254*y^5 + 1730102394171001003600965798168645486085923713681105615699006946425647/31726187626824456626436111002350933930582595819250210324361979254*y^4 - 286320859643426547683649156323860797421254924463292856949967079335519/15863093813412228313218055501175466965291297909625105162180989627*y^3 + 4469597878766765231417311850168771908261116038130326429987379092240/1442099437582929846656186863743224269571936173602282287470999057*y^2 - 5001271617531201182101641229855253619107570853384158585991535938177/31726187626824456626436111002350933930582595819250210324361979254*y - 565924732233593859955282239128124360416593140927112446462553508721/31726187626824456626436111002350933930582595819250210324361979254

78562312534213608622457355035479774673900296900644545174882513630732069/102791880262188621323725893346231454231602727685198194319517919742592753*y^26 - 64171032754699469077879526751325675626268163022517503908356873080829546/9344716387471692847611444849657404930145702516836199483592538158417523*y^25 - 559926492956977270450548234709086583515632696932713269745894811108690764/102791880262188621323725893346231454231602727685198194319517919742592753*y^24 - 1820816041778596460959782170521579079054905307597377157385944077747634729/102791880262188621323725893346231454231602727685198194319517919742592753*y^23 + 22201552429166754025537522256251881567339273609529379021980612825381360818/102791880262188621323725893346231454231602727685198194319517919742592753*y^22 + 24360404582688250439813859514729489459428901900546072088619877430002086232/102791880262188621323725893346231454231602727685198194319517919742592753*y^21 - 35755987851645079046365043261946320759120600112027096691721910257023712050/102791880262188621323725893346231454231602727685198194319517919742592753*y^20 - 61393306600320929768476485933613461371767788483325945427373429746329088523/102791880262188621323725893346231454231602727685198194319517919742592753*y^19 + 608959360371340311729047364717277299420193599656302404523092211190784214428/102791880262188621323725893346231454231602727685198194319517919742592753*y^18 - 406361327502805068373036967536272495112178586428275910061301793124954597469/102791880262188621323725893346231454231602727685198194319517919742592753*y^17 - 1102046384996949899969346222549525638443908230334520881932728219733088130305/102791880262188621323725893346231454231602727685198194319517919742592753*y^16 + 269278762542262830555608812423852134516629457314714846247918384552539230418/102791880262188621323725893346231454231602727685198194319517919742592753*y^15 + 3741540190030599388623319034320822605221727814439158687085102469090799364750/102791880262188621323725893346231454231602727685198194319517919742592753*y^14 - 3611694734792772563882358876119457894432449015268918154675303870560572461819/102791880262188621323725893346231454231602727685198194319517919742592753*y^13 - 8688884653942394156569287652067457135846589576656549356808868906141311075427/102791880262188621323725893346231454231602727685198194319517919742592753*y^12 + 16895767280052483272967774992477415645481208570082851976472941544809999356041/102791880262188621323725893346231454231602727685198194319517919742592753*y^11 - 3748576709921253564342498298954796507074711492461837749023825518730491918645/102791880262188621323725893346231454231602727685198194319517919742592753*y^10 - 1356405136838287162643084481279332157189502909052731210018495605705507911960/9344716387471692847611444849657404930145702516836199483592538158417523*y^9 + 19508335140112282440205583304303725714414451580703262924117200158759223789853/102791880262188621323725893346231454231602727685198194319517919742592753*y^8 - 8083291042231137330100937861855568845346088838984164242615331993594660584362/102791880262188621323725893346231454231602727685198194319517919742592753*y^7 - 5272600906987481399617059176267345125105288241598384825644083948010336826129/102791880262188621323725893346231454231602727685198194319517919742592753*y^6 + 8666875351560261812494597423155884387001585441211132438335168322309416908310/102791880262188621323725893346231454231602727685198194319517919742592753*y^5 - 5258309367558636345111338861256004583395894745246760521565616296376952978115/102791880262188621323725893346231454231602727685198194319517919742592753*y^4 + 1736298326808703575197149162106291187808218081273282491488900232170378014583/102791880262188621323725893346231454231602727685198194319517919742592753*y^3 - 27541023458580532033755354331286699938031260311950296461190841740655617651/9344716387471692847611444849657404930145702516836199483592538158417523*y^2 + 17108769137428233835155402307567523656190308401717840266455526403371123975/102791880262188621323725893346231454231602727685198194319517919742592753*y + 1664539916716297934722628359781039848010121625126486458144032848889696563/102791880262188621323725893346231454231602727685198194319517919742592753

25162205440205406317461693287822219151295888796318238908556428374528383/205583760524377242647451786692462908463205455370396388639035839485185506*y^26 - 20419461233554624980546537614084628724761852592165692754448117877606265/18689432774943385695222889699314809860291405033672398967185076316835046*y^25 - 97691381489334615774658518543948873828613261361266697834518364448421327/102791880262188621323725893346231454231602727685198194319517919742592753*y^24 - 568272538951799220840496813632638258354971009470230731758714390032778961/205583760524377242647451786692462908463205455370396388639035839485185506*y^23 + 7098781214552982106043634703086365904051135656508522529621545138341200161/205583760524377242647451786692462908463205455370396388639035839485185506*y^22 + 8296597561018497979943165266192044658023353821008856986530815272518235397/205583760524377242647451786692462908463205455370396388639035839485185506*y^21 - 5900315959519483679704957393589670700319433278511809036369559755806344146/102791880262188621323725893346231454231602727685198194319517919742592753*y^20 - 10637372535324261962718595565363572982621793644543353098531321041387946451/102791880262188621323725893346231454231602727685198194319517919742592753*y^19 + 97375478858914852818303154810117923141535361548698484262102547307878946504/102791880262188621323725893346231454231602727685198194319517919742592753*y^18 - 116391416625674197380105734974956973189853918305391938397845756207697867899/205583760524377242647451786692462908463205455370396388639035839485185506*y^17 - 381983234753753175306705472952238072655688547280759146726720406069873056135/205583760524377242647451786692462908463205455370396388639035839485185506*y^16 + 78531466721471791677384683122606828890829563294195176416845747076901499043/205583760524377242647451786692462908463205455370396388639035839485185506*y^15 + 618023853585593066177993400166217501729735024759953891955375501136545100616/102791880262188621323725893346231454231602727685198194319517919742592753*y^14 - 1077526507185914278429314573262186788103150624154909590662866708252263977387/205583760524377242647451786692462908463205455370396388639035839485185506*y^13 - 1493612298886682726431115967299830092990495104440304220863311321874533035161/102791880262188621323725893346231454231602727685198194319517919742592753*y^12 + 5364511906768329588394653802225641671225816870722781457605236184400070545925/205583760524377242647451786692462908463205455370396388639035839485185506*y^11 - 304570491435399115682499171153671154707420283036341829710341409566032077834/102791880262188621323725893346231454231602727685198194319517919742592753*y^10 - 242033116379559672659669626250182915953460516195905862719952320983141746393/9344716387471692847611444849657404930145702516836199483592538158417523*y^9 + 6054802848667324808282221376991137123694923112031138329291303310435476365563/205583760524377242647451786692462908463205455370396388639035839485185506*y^8 - 952178336969480106408809555807906254487706319365621158287969997778580969548/102791880262188621323725893346231454231602727685198194319517919742592753*y^7 - 2219934804777914162943372858583148084852855524218067807016437993170986751631/205583760524377242647451786692462908463205455370396388639035839485185506*y^6 + 2812003570287402685185820203253877493828142502650257901599980023009277200887/205583760524377242647451786692462908463205455370396388639035839485185506*y^5 - 1428333292100046551906719783994603117013665998283433381561111216755488962323/205583760524377242647451786692462908463205455370396388639035839485185506*y^4 + 179406198829608760712098717588171490584732508484226984054350550478557099300/102791880262188621323725893346231454231602727685198194319517919742592753*y^3 - 1314025432888739291892919121670889066454320519313169091766351182996897627/9344716387471692847611444849657404930145702516836199483592538158417523*y^2 - 3483149145932799672598591684778931398419353064276236644896460902467391765/205583760524377242647451786692462908463205455370396388639035839485185506*y + 321090180571558256723630083392393760737855993872172461805938271007509167/205583760524377242647451786692462908463205455370396388639035839485185506

-23943841470866170239821339960548665055110385990936696402038458859168556/102791880262188621323725893346231454231602727685198194319517919742592753*y^26 + 18710209401797058620871460075434125601189974442163951854587902649502646/9344716387471692847611444849657404930145702516836199483592538158417523*y^25 + 251316402812303752672348302948926671539115422876219627991645444728547997/102791880262188621323725893346231454231602727685198194319517919742592753*y^24 + 648336508415253748823070515933197822967588343722886046112872497225790114/102791880262188621323725893346231454231602727685198194319517919742592753*y^23 - 6520430708149595415026286382806608212620718864932150016331699783960436051/102791880262188621323725893346231454231602727685198194319517919742592753*y^22 - 9978481421368211669633677866126927051488105853963419971954984297360510863/102791880262188621323725893346231454231602727685198194319517919742592753*y^21 + 7154389595765894492473216764533871919764388119337886797776889796662871072/102791880262188621323725893346231454231602727685198194319517919742592753*y^20 + 21744262087377860088965918953762584459857758565340192087853143287051353343/102791880262188621323725893346231454231602727685198194319517919742592753*y^19 - 177250913645347014052948030477686355330958867755193107193673208002483871247/102791880262188621323725893346231454231602727685198194319517919742592753*y^18 + 54308712849326258995347133698006657505719937351651155686103530451172393146/102791880262188621323725893346231454231602727685198194319517919742592753*y^17 + 360836412154318394683349388042947940801863048260556855863817192825567884717/102791880262188621323725893346231454231602727685198194319517919742592753*y^16 + 57939343065778448162786942065382276846772435772052577427017788626401538361/102791880262188621323725893346231454231602727685198194319517919742592753*y^15 - 1126044205509748479147888429939081642285591685000249784036611290914194653496/102791880262188621323725893346231454231602727685198194319517919742592753*y^14 + 659369849767791455787131188671666924068635466695447657826539211479521147886/102791880262188621323725893346231454231602727685198194319517919742592753*y^13 + 2929697798610324527675160135189073393280690230652827552698416993064867049224/102791880262188621323725893346231454231602727685198194319517919742592753*y^12 - 4018190727603360290391864494027228551974170734434110968535477387388901162612/102791880262188621323725893346231454231602727685198194319517919742592753*y^11 - 489800805065528034142224059175095877738483231130093308628640487290116158597/102791880262188621323725893346231454231602727685198194319517919742592753*y^10 + 402980871647732740403003911692070818549668932324786970226764600948145017804/9344716387471692847611444849657404930145702516836199483592538158417523*y^9 - 4191087412688263466452774381843527983122106659320734539251583614589976427711/102791880262188621323725893346231454231602727685198194319517919742592753*y^8 + 738397392228685641659233784105003300123567349057913114108391702662499648187/102791880262188621323725893346231454231602727685198194319517919742592753*y^7 + 1965239603012081540751640174268323207664982364130486669748357287260326534285/102791880262188621323725893346231454231602727685198194319517919742592753*y^6 - 1876224696800128692549778784037755775096843688453221962108052907692333904466/102791880262188621323725893346231454231602727685198194319517919742592753*y^5 + 829087169088689143450610127392917580603742406840504909659290999397805182624/102791880262188621323725893346231454231602727685198194319517919742592753*y^4 - 176138221114737253761878189196208961459904702769975032043229744208442041018/102791880262188621323725893346231454231602727685198194319517919742592753*y^3 + 1230856582939283827025147247567550949299921496064446925987598501929362114/9344716387471692847611444849657404930145702516836199483592538158417523*y^2 + 1636423481580970437954601506658567838250258383054155329756520249287939910/102791880262188621323725893346231454231602727685198194319517919742592753*y - 60143854761828910162670731516714875143899594510440635626215066131360867/102791880262188621323725893346231454231602727685198194319517919742592753

14698651792904842195469149100037763975367448363760498775369163635569223/411167521048754485294903573384925816926410910740792777278071678970371012*y^26 - 11404686606459480130074089075457477095605393070440316856526301218211107/37378865549886771390445779398629619720582810067344797934370152633670092*y^25 - 163630692794225994492021332073329434311198686707609663418683266840195659/411167521048754485294903573384925816926410910740792777278071678970371012*y^24 - 393048195256874453408301779738654905661680398306664296734483251544738253/411167521048754485294903573384925816926410910740792777278071678970371012*y^23 + 1998268729886913536692057386789649433094765791988241189196379332999845863/205583760524377242647451786692462908463205455370396388639035839485185506*y^22 + 3211256811830114153217421482459570548638559012924585089138546864248381881/205583760524377242647451786692462908463205455370396388639035839485185506*y^21 - 2236118657280842411409957494899799789931387250973383930885542574157746987/205583760524377242647451786692462908463205455370396388639035839485185506*y^20 - 7163453388579876740273425262902438118395985459720671694309606586031437799/205583760524377242647451786692462908463205455370396388639035839485185506*y^19 + 27057389939121238019942862764297387193526487322066336177909295719599299920/102791880262188621323725893346231454231602727685198194319517919742592753*y^18 - 6324650045892552311065998764627191945813832774672952692320701382633166075/102791880262188621323725893346231454231602727685198194319517919742592753*y^17 - 117817174560556340979232583919003950343310084536890492681242263818066404453/205583760524377242647451786692462908463205455370396388639035839485185506*y^16 - 22833923882619906240923154030102209159232839995071315588747037783624462291/205583760524377242647451786692462908463205455370396388639035839485185506*y^15 + 177217743241483629681803709167666094938751098654939179356568432656040461435/102791880262188621323725893346231454231602727685198194319517919742592753*y^14 - 87599296267786077983859600197531849783836664886463557616432859690612480743/102791880262188621323725893346231454231602727685198194319517919742592753*y^13 - 474536198357150432393770709475633057932389696235202763967388262666062285471/102791880262188621323725893346231454231602727685198194319517919742592753*y^12 + 2399885442898395757567967142783800955482621941983887757691574791388482304875/411167521048754485294903573384925816926410910740792777278071678970371012*y^11 + 623997274568691335270566778974220567505031232183123739689762757546878271863/411167521048754485294903573384925816926410910740792777278071678970371012*y^10 - 132749486802451260864727172211187210462643298571058502499498165569301460021/18689432774943385695222889699314809860291405033672398967185076316835046*y^9 + 1195067287302954302351457966524814762779411873663452300208622062630968099841/205583760524377242647451786692462908463205455370396388639035839485185506*y^8 - 30432502803220483486323912705445267773365431602019555774217852420665972116/102791880262188621323725893346231454231602727685198194319517919742592753*y^7 - 1400154209091508538002166966442732951784948101645675187843438894885984734515/411167521048754485294903573384925816926410910740792777278071678970371012*y^6 + 1105817870403066444690582835786578420006882111294118165867248742767559889349/411167521048754485294903573384925816926410910740792777278071678970371012*y^5 - 377375198911090432638970737521634116874560096267812330223458130658596370583/411167521048754485294903573384925816926410910740792777278071678970371012*y^4 + 38743826429729065227710646365386661513770824112406557254399568833511157439/411167521048754485294903573384925816926410910740792777278071678970371012*y^3 + 182500915528817925680742474251424433744137272789857565530551869605219571/9344716387471692847611444849657404930145702516836199483592538158417523*y^2 - 164231089546075040351164053128528487506094347571301161066517660449957315/205583760524377242647451786692462908463205455370396388639035839485185506*y - 5544835274641566422769929182208259663147414457924740750473722841431645/102791880262188621323725893346231454231602727685198194319517919742592753


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

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

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

# f Combinatorial flattening
{-1, 1, -1, 3, -1, 4, 0, 7}

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

# 1 Loop Invariant
-288255563760846194124160619178256307993276846101976429082698459843894667/102791880262188621323725893346231454231602727685198194319517919742592753*y^26 + 227973717130513169177449416551309058057376002086948991311847951564393154/9344716387471692847611444849657404930145702516836199483592538158417523*y^25 + 5531819774266296054020102415886420446572429294212397074568969316023447933/205583760524377242647451786692462908463205455370396388639035839485185506*y^24 + 7502819331849340723832831220740194486805101915979799961483121561311038718/102791880262188621323725893346231454231602727685198194319517919742592753*y^23 - 79246109913316834257346819906906544659970445591312321277823897925476321003/102791880262188621323725893346231454231602727685198194319517919742592753*y^22 - 223725394491357703008878219979834888976623266360021184792163574361116547221/205583760524377242647451786692462908463205455370396388639035839485185506*y^21 + 196428264938981882183029197964015027177452681690678394974129167819097037325/205583760524377242647451786692462908463205455370396388639035839485185506*y^20 + 250608955686485297847333342024759301512563008141834837350038773539007684857/102791880262188621323725893346231454231602727685198194319517919742592753*y^19 - 2162531899561648780050135802961277668687795456991344260593810773105683530465/102791880262188621323725893346231454231602727685198194319517919742592753*y^18 + 1757877028981913986239963423076110865016991277573362632630681784605929963403/205583760524377242647451786692462908463205455370396388639035839485185506*y^17 + 8532711638132989805275404306835136753608164090539969790330927518171025033025/205583760524377242647451786692462908463205455370396388639035839485185506*y^16 + 428896075953575458076139241362045782866443257913207254813301971825076856299/205583760524377242647451786692462908463205455370396388639035839485185506*y^15 - 13585778090076882471510864739757106156167889969611373614982794953230370581171/102791880262188621323725893346231454231602727685198194319517919742592753*y^14 + 18846640371917903139360548635393887597380398125148078208721505675950142432751/205583760524377242647451786692462908463205455370396388639035839485185506*y^13 + 34380318014750133590446001437235919324250999934001770516861611528844556553548/102791880262188621323725893346231454231602727685198194319517919742592753*y^12 - 52228501434550750305027170355669985748557534731535106105828913584588221507204/102791880262188621323725893346231454231602727685198194319517919742592753*y^11 - 987309227589436521955717896671120202041158262161775617941563864799361575561/205583760524377242647451786692462908463205455370396388639035839485185506*y^10 + 4928836987785234700627149921918969368436667367238294367295912759834006611178/9344716387471692847611444849657404930145702516836199483592538158417523*y^9 - 113562964878527211095240059298840717092103994764400982556208272509497702240687/205583760524377242647451786692462908463205455370396388639035839485185506*y^8 + 28718753599046762517047337948907023518204190160419175560174800510353040608761/205583760524377242647451786692462908463205455370396388639035839485185506*y^7 + 23063376711498619620304127364550528505735609261293583769492844197871437685514/102791880262188621323725893346231454231602727685198194319517919742592753*y^6 - 25512258180195855883992054097909984304927558178984347827848141543242257600989/102791880262188621323725893346231454231602727685198194319517919742592753*y^5 + 12532806873116854477059570677730649909656215281627225614478064789857813728165/102791880262188621323725893346231454231602727685198194319517919742592753*y^4 - 6101286175278399371928705427120035555960439267299764830446704536530769330909/205583760524377242647451786692462908463205455370396388639035839485185506*y^3 + 57537219261773335373615639084701266403220445871063659951337674576418105427/18689432774943385695222889699314809860291405033672398967185076316835046*y^2 + 10212717758908003380233308544773957087968605514214302039713653638585170155/205583760524377242647451786692462908463205455370396388639035839485185506*y + 3015854913868248877337481316804376917390329513013341224624707832349469945/102791880262188621323725893346231454231602727685198194319517919742592753

# 2 Loop Invariant
52921347108401042181084612153632164484523051713840113681408431233051412616077137179410717645510017026963529534317977020188834113744982995701093157346576394354293459/5814004281182069725798716508927144788233594873683359637716022848496796207158722731813550766058857632541451066389662457023514650845849744759236680022938720634750794636*y^26 - 42406441144344647029907217173546546051223268346913067835789765932740327630293711629142788803319566625830483411273499439972108679230612853951061007491348279060175653/528545843743824520527156046266104071657599533971214512519638440772436018832611157437595524187168875685586460580878405183955877349622704069021516365721701875886435876*y^25 - 455416882556896433132144629447615276589758613422284957343495330502324490275307392274237227482458142679028197054156389726568415533468074878805763049024083722628806631/5814004281182069725798716508927144788233594873683359637716022848496796207158722731813550766058857632541451066389662457023514650845849744759236680022938720634750794636*y^24 - 2630036390251707981952827540032542864964065915323675005884171151393178012083199755226176588303390543704376351159878621543739908651734532640925588708810144842634732479/11628008562364139451597433017854289576467189747366719275432045696993592414317445463627101532117715265082902132779324914047029301691699489518473360045877441269501589272*y^23 + 58849170374267725196182679018953480115494719713653460858171317737737089750077495177633829756278212535121770582100784699259354290130967101381490190774401163062827247627/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^22 + 75492768561723286824808320154434069349403500919463173203771134406745918686836559614374172244383868646413645482341721883808540026846734218884011338615589419221291413329/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^21 - 13682701886212445108045291199150052158974883884116145777007323240625291150508125030246833338641976528100683665145980016675124990380623272581168114631906734359592802409/3876002854121379817199144339284763192155729915788906425144015232331197471439148487875700510705905088360967377593108304682343100563899829839491120015292480423167196424*y^20 - 58860219031558444386550101317721213242328913366523558150937051913246962997885308620489491086704151752335250610437027150240133590562272362854317965276530060557130620087/7752005708242759634398288678569526384311459831577812850288030464662394942878296975751401021411810176721934755186216609364686201127799659678982240030584960846334392848*y^19 + 1610607621796114975266754893789025014267580608622181741576733681954994832199637786497335013330689739796738429003897277345118220952503606895945835804588681225688070765351/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^18 - 51586640360445095641815664435981023501785435521413290019998593057689252493560539000699365869809688010865605628435090699016055519693490480490840472696830229819322982163/1453501070295517431449679127231786197058398718420839909429005712124199051789680682953387691514714408135362766597415614255878662711462436189809170005734680158687698659*y^17 - 768426958658180294251687019764194027879439660896859105435553922702643724131453142379958227652862935465637058507719482065485474120375469666346996163044195819030359489415/5814004281182069725798716508927144788233594873683359637716022848496796207158722731813550766058857632541451066389662457023514650845849744759236680022938720634750794636*y^16 + 12901397811810825503284656830061740637997059985435541151784135263315200549204361789124017109865574725938869402085290487582596899100885666016432669607222742825746719511/1453501070295517431449679127231786197058398718420839909429005712124199051789680682953387691514714408135362766597415614255878662711462436189809170005734680158687698659*y^15 + 10043018053612724042910829827911249241238383872307660411087951620842508974949420782520170394262761510181715408060132407025328297911961199436571531744285188554836479063171/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^14 - 8078779962314500693816893519961438772866105788314851622361516524129088760405653982663811186611238541674801501086155731575215291682578408209611429252409449132244780958737/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^13 - 8186904197413036562474896299940721479293985666465851058596568892809772851886262144221718807342115456219694049132283109316258709204036627854305839958285666477973484409555/7752005708242759634398288678569526384311459831577812850288030464662394942878296975751401021411810176721934755186216609364686201127799659678982240030584960846334392848*y^12 + 41303831096335317188476279259471089162796515786072466335560581518588492317779349071189121028469564596744462502807432392452718798258970368635273209053838385098486328772747/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^11 - 308136109679446061144491259211419960066380252773689703064823803929306400153224956320803332654474816919019828889046166974355716287800174105949403751636198402661711799491/1938001427060689908599572169642381596077864957894453212572007616165598735719574243937850255352952544180483688796554152341171550281949914919745560007646240211583598212*y^10 - 1833048053293399738511219867484903087858838202897744252512438445788045365392968047111102751989717970603826510290778558425629751146259509394780114078726922368913048582015/1057091687487649041054312092532208143315199067942429025039276881544872037665222314875191048374337751371172921161756810367911754699245408138043032731443403751772871752*y^9 + 23041987147215218230474160996983480601393960448923512323229023809982185314104774182419991447827460079280870118086941395895763618807499313332725780019828229554945838694795/11628008562364139451597433017854289576467189747366719275432045696993592414317445463627101532117715265082902132779324914047029301691699489518473360045877441269501589272*y^8 - 910779834086182335924972148679565748930626043470191446291780322674139785817557279147481740686663482038869598780741972867391160668837483941328455708982610278999602275343/1453501070295517431449679127231786197058398718420839909429005712124199051789680682953387691514714408135362766597415614255878662711462436189809170005734680158687698659*y^7 - 2041993420665379708533503856148945346159898847799306910463885928378489940850926491008142146520946410192845961278544415109228626938623671202361943138649243391316166701485/2907002140591034862899358254463572394116797436841679818858011424248398103579361365906775383029428816270725533194831228511757325422924872379618340011469360317375397318*y^6 + 20709875594637180179142587404129500109890569526817375595034465886031810663903775774562342172257413646633935124985148974449749333712656420667123711995765607460585221710613/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^5 - 10948182458359552805560705819104916105056420037969072791656324765676971567972622704971859977305380483935091580751051255297344246673079684869168398431174261830330967229223/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^4 + 2914354666374598159485210761796334049635705296109093468893167752283984610072911585252259626161475901660903605203559649590475204856868523925600978885235836039810514558567/23256017124728278903194866035708579152934379494733438550864091393987184828634890927254203064235430530165804265558649828094058603383398979036946720091754882539003178544*y^3 - 229746905742699832577194256949586052554003783279153001747316823691461215718279052465880866777319950187694196282296416473292627294585462479679564089905770487187226737/17188482723376407171614830772881433224637383218576081707955721651136130693743452274393350380070532542620697905069216428746532596735697693301512727340543150435331248*y^2 - 3167904542233810836386183887779320412128729215245867957631945416536921237971919682259932691103633576015777548009367115380950265206472604748467266779057851971435446051/3876002854121379817199144339284763192155729915788906425144015232331197471439148487875700510705905088360967377593108304682343100563899829839491120015292480423167196424*y + 8379982057150885146494793468500268242134714882711178198903099025606032810607295556742379325643071304771449463012623110091540029080416554169850166887161954315026456261/11628008562364139451597433017854289576467189747366719275432045696993592414317445463627101532117715265082902132779324914047029301691699489518473360045877441269501589272

# 3 Loop Invariant
-1944827797988554791662984054622000494240488371941784472386899110222645101166586328836077548356657332218625967229290943381487881281481054443209137898257372453943098730526948005991408522741624691402242854638899319/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y^26 + 3033361023644268601710015886190557732399259252921307613647540618244644263950626876291334040654263735756795032981271732159675714555658756367822827804004570672477057432426892779380736859049335770240286484546913603/193530329258164229790782884051460521182764292853521379232056280365193903384635495055866761788661519048060153560889670246419543913054351619670881845630059288659668592549456602069131325534793033949164371321572846272*y^25 + 41286165479912204006012972739259800230002545653564470467193677483137291272215925171540510846883690954209724812276394543840735176916973847425327325187655145683468124855568680613092523877994838927903161213104550653/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^24 + 652351004224793330078581981213067035246637980763974729962648951727480661235047272969762288611766340584211671967138115758514535447867753847648298705704620452262056793128084605170117711759805357708945449937987067/12980692816096381266454949540036986176892726959687409582637921244006908153847502717161794998019979936150376153474307150674481603924377242782803050621528366922294844622219650138783198663919044960004927344739642128*y^23 - 1055822620083137089862142724983405213364603533064254047692396444547174227704321915291495345329650743282781973047626325541880103818580721147239586731897349493621201449370714739768705958419549031324658104699114381937/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^22 - 1635980948593672397410284880819603373148656763435393330908118309223159418070271853699494159325329462932436067031031338599255954611805985077579095972789539625950271365892049272129615461909623194260390935147540089645/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^21 + 1103147293136172796860832125863527971878690368871429569015707920936163477250570100522925918973566324727404371799433374047495511199452880174399211016339483745774260330710487718851816002131500722331876578566447688981/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^20 + 3491141302536954138268746910736754751359607657403620427109806819799736792695861005405802164255372421631150750252154400133315270819189702492380496466638137624594550417116132399674327974900908398643641668931994993715/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^19 - 3588361899531628459638341332471318090739703816341255443405691244743216050524632067510650782625295887873412584552930527089992574806780970678685691284779273432890609156208425123048331108299488521367679680987462440095/266104202729975815962326465570758216626300902673591896444077385502141617153873805701816797459409588691082711146223296588826872880449733477047462537741331521907044314755502827845055572610340421680101010567162663624*y^18 + 8462718302316474614355542321820643472123223281679475146813043948069803714638035232877322581597309136636492460633108727838723381373350388475905016518687264107929715468417679151137717563548553790994160612849998136597/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^17 + 14490985137181007745100907731810982141332520300499982157168185805652355113407377063645417674811452798168629180912200490848593378886469011934874833367719691658824407369937622574091415008905406026065791952207627822519/532208405459951631924652931141516433252601805347183792888154771004283234307747611403633594918819177382165422292446593177653745760899466954094925075482663043814088629511005655690111145220680843360202021134325327248*y^16 + 10391962448037682880061818988362751497760980861985049025109167913272077099562863961157326021393755051345281540609028226499641281298415111867490459853729036314071571566691039114109554871749031263259335648790550418013/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^15 - 90325909249624227737286712466429789554398471828133778644301286500057956265975736619645202284568338042495902179440044713990283539964432836492378388926970537918596318448391170724824767502451990892312613179551170650759/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y^14 + 104906619993293994250732694973594528940666660917743054463330893040028373377348351233133455796285650655065103652370394311846287847724857488802562674887133263528211822718047006404024435169154938471527369526297835630159/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^13 + 236171200077645195448743987651892848562863100444387848797120749846950131147908458039311201471970327605106567860047858578298846531373468638030842494676260920781605754343830103635039487234329092733184348629638754235011/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y^12 - 643616498711557036035696370422832606028749815462899061568875992863096358424173874679626118795348210663954309433360474702360238269577968669734813865969766753029545686728027029133902452429214355530680375467116524836375/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^11 - 37228381288229493427012705539977176434515132518381221721950203191947002553947048771909365271193360911537497345207266835643552451857708149050767609734213205579865934023101299919691796006633882743432002779219702424991/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y^10 + 63945736956190046849967964153795195060366848776079883787535083170663223469947602303184128618046263889050276159708404452124192507467406684648983846991520647170106810432267121121805506749048101686529725324409160717995/193530329258164229790782884051460521182764292853521379232056280365193903384635495055866761788661519048060153560889670246419543913054351619670881845630059288659668592549456602069131325534793033949164371321572846272*y^9 - 339924697720953241432298564144059253280879614231518661662163819319270770662341990045242324745203373620172458572951887650395110013529934297478910413157728084649930795758642728665134844269958618959509620703920209482477/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y^8 + 130995578764083756320215025113275762163901022946618208476420488452796846220602393062415369493476826829048237559010090863199839933313816389045343242029266865476680832113771424323197449176087413050681717474851049656809/2128833621839806527698611724566065733010407221388735171552619084017132937230990445614534379675276709528661689169786372710614983043597867816379700301930652175256354518044022622760444580882723373440808084537301308992*y^7 + 38258233873653264673993343106231649281322432645179294562346023818715209424618779252616866823863097219319157914113524447053696000029990735862758918964317308418294539404561071977974302699672823135224111232915462714229/266104202729975815962326465570758216626300902673591896444077385502141617153873805701816797459409588691082711146223296588826872880449733477047462537741331521907044314755502827845055572610340421680101010567162663624*y^6 - 151335921952518729534504484458020197145704250554208532753092909284305076439635695563365548188495789321108488339368719068876188906730884159904681295252624890951814839042046129176156766336020522210095983227452876819427/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y^5 + 71098161380141297841925402699021149029217654539547230807487975460237693566522722612028114858920565239490849697993465161477937807675591695674514806994846873488518078397969036792978920407596921532505425423079157735635/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y^4 - 810484191273625067964183161699066233043713725389391154712811995081238358486118984857234217355555309214802865442611268090436098964046269502446287873239550335701490779229280565781444865070530548028286698564507013587/51922771264385525065819798160147944707570907838749638330551684976027632615390010868647179992079919744601504613897228602697926415697508971131212202486113467689179378488878600555132794655676179840019709378958568512*y^3 + 183623103335218056739294779043483910180228118375374147221184914155840183369446741200934703215194641747660734751815928946572641804787816315701676803037509760207582778361257033422624955554323839553999161695621365719/96765164629082114895391442025730260591382146426760689616028140182596951692317747527933380894330759524030076780444835123209771956527175809835440922815029644329834296274728301034565662767396516974582185660786423136*y^2 + 27630724995996610596580216694249688453641421356174447191419579248399225497796167199234027188287304572019474867186664246479636684451293421386667118736432875973936897129319499077095327497503636924199204133265694939/1064416810919903263849305862283032866505203610694367585776309542008566468615495222807267189837638354764330844584893186355307491521798933908189850150965326087628177259022011311380222290441361686720404042268650654496*y + 10464362503801420897005587556049241140533661084041631815466060599956840454723557656765815127245562303472434131315469478450895772890925893966632540661617229132874428366459582398531511806387042774369343329607099859/266104202729975815962326465570758216626300902673591896444077385502141617153873805701816797459409588691082711146223296588826872880449733477047462537741331521907044314755502827845055572610340421680101010567162663624

# 4 Loop Invariant
5920659075898170347823541299934131456509551547728314936463259126489093665674554089860399046214199450811322451395866435291918473678178749370021470392147486416559619318992414529973381845626698667591061568982599621705168362755817130775220508017366049621387520503368981590771076218573788430383073432357235230099/1204088081639439515486386687742422854626763351960132113813053851329564933419429336219339301639920148977010792640744601544860900839984264159600558914303680593020561296046844644972231763163737432293712967446285109842586866468390221092669384079270180231019524353126651353522850662347330233197420360837271754903040*y^26 - 13935969833510818999678542823769095836962757292976894996514817347770515481478090675041994778497235819033803754701574474812050805270048731480478577314761022741867122510820049557746502935444459537675787425399855658511252618979004295838623475674591987397546354559678859885492490198639458542544661795332473336587/328387658628938049678105460293388051261844550534581485585378323089881345478026182605274354992705495175548397992930345875871154774541162952618334249355549252641971262558230357719699571771928390625558082030805029957069145400470060298000741112528230972096233914489086732778959271549271881781114643864710478609920*y^25 - 90502564683893258094524854902794096269235964331403276516851607310669574401433160664777381624826069051082949679763599838860351755173397940946926021767932557963935321566967333581143757421458565666528581751501815796180189948092019410570932485980925999011657129674504957021721943463350423977019252843401100959561/1806132122459159273229580031613634281940145027940198170719580776994347400129144004329008952459880223465516188961116902317291351259976396239400838371455520889530841944070266967458347644745606148440569451169427664763880299702585331639004076118905270346529286529689977030284275993520995349796130541255907632354560*y^24 - 474899058760601801650407634811103694191132158361158583527339077328609088309844817335014058991518298593091634314384634037340943859730166613727433529649050091941966198720642185440126435935667642740653172733578833110322897847194449468322392236521463580157998754168721252112028822276539499279341142890471110228967/3612264244918318546459160063227268563880290055880396341439161553988694800258288008658017904919760446931032377922233804634582702519952792478801676742911041779061683888140533934916695289491212296881138902338855329527760599405170663278008152237810540693058573059379954060568551987041990699592261082511815264709120*y^23 + 4850138516947262138065805873638340834515420875333027804355656571172545891918229724206310570578747750255509724788150553000616658143323280121526748138863270178962064278453874022854783339831573970954210875109674211576997600905117616307921054937261953163074023077018076295887840917391937933512953090294516466418601/3612264244918318546459160063227268563880290055880396341439161553988694800258288008658017904919760446931032377922233804634582702519952792478801676742911041779061683888140533934916695289491212296881138902338855329527760599405170663278008152237810540693058573059379954060568551987041990699592261082511815264709120*y^22 + 14450195973384443927291821746910239213683290192674206870076741943145351995076060009881939798140111550289014441525635348507716804315386699448894254464687811792707815382940207783067406828738632218801971933969873120424460556184862671331599242863176750569008524599496876318160377901678582487033699860121864135530981/7224528489836637092918320126454537127760580111760792682878323107977389600516576017316035809839520893862064755844467609269165405039905584957603353485822083558123367776281067869833390578982424593762277804677710659055521198810341326556016304475621081386117146118759908121137103974083981399184522165023630529418240*y^21 - 277792244513440817729336565589726122876591300658414922746372700933402319815337946473357396662675497928440333545796266163265719762573379073522719377079922059099318739092632344052458962191101113348887909595251955197792414672326197367814870088062750471404202534463393320944743550890614429034191898536088084472635/180613212245915927322958003161363428194014502794019817071958077699434740012914400432900895245988022346551618896111690231729135125997639623940083837145552088953084194407026696745834764474560614844056945116942766476388029970258533163900407611890527034652928652968997703028427599352099534979613054125590763235456*y^20 - 2637889969207698703675012132207059723695280107473247630077665023353690532717243217481256791758526183797622506376228640593916108758714355160419578228125277659687131421245199718576185130733131883390476404313514076752243624277649202342048742352502340230363258531901903018112184742329060554610098890769293990625327/602044040819719757743193343871211427313381675980066056906526925664782466709714668109669650819960074488505396320372300772430450419992132079800279457151840296510280648023422322486115881581868716146856483723142554921293433234195110546334692039635090115509762176563325676761425331173665116598710180418635877451520*y^19 + 16528269385488290717314902813361903669757047193017496191763152199568452284460605112840545927338008792796846605427607200513172513426681180668602102877600818656688609498690500632862891864577303529419610635631857408362690859049150842372374085571686619510359753011061078010210948877500591898918916898901068792956237/451533030614789818307395007903408570485036256985049542679895194248586850032286001082252238114970055866379047240279225579322837814994099059850209592863880222382710486017566741864586911186401537110142362792356916190970074925646332909751019029726317586632321632422494257571068998380248837449032635313976908088640*y^18 - 1245786597285954689468689099984792825582266004456951790569649187114623349245114675902058584463951673484527627994530635590534694764175329287907265760596727531256200438329319009110541291465605659560869980488050157531469942360682928418827254404372781164057407723953579971842786389824819179087353068767968528684747/100340673469953292957198890645201904552230279330011009484421154277463744451619111351611608469993345748084232720062050128738408403332022013300046576191973382751713441337237053747685980263644786024476080620523759153548905539032518424389115339939181685918293696093887612793570888528944186099785030069772646241920*y^17 - 531455722499140726939955133917583100463152807358611973667122747648780735104144054212773337237419495091658591685996636745356158030174397908472816226647743886463786862378316164943618751502899873183459037767409317362707468138353141673539944976755181093691874749377506555986564663364258943632623357483421447423434297/7224528489836637092918320126454537127760580111760792682878323107977389600516576017316035809839520893862064755844467609269165405039905584957603353485822083558123367776281067869833390578982424593762277804677710659055521198810341326556016304475621081386117146118759908121137103974083981399184522165023630529418240*y^16 - 62915181637385734526891276552193557594726791933898731346372066194042839823168078510878972011442384595348537732632254858591421749455784220254044452325775183922671765393483594369653676899498421740780485449909682559375418500821810376906799912652966659160568452448666927124858493049824509485191961142710511681635349/7224528489836637092918320126454537127760580111760792682878323107977389600516576017316035809839520893862064755844467609269165405039905584957603353485822083558123367776281067869833390578982424593762277804677710659055521198810341326556016304475621081386117146118759908121137103974083981399184522165023630529418240*y^15 + 104566627975206565184869815701875486628002277332430902772168051986612417644415743758040263613788362047095782762685398536750071827922098730280139389014586185495347551368907196842748267472265581908260987266799011532645897905289053666554524993237960857493599629021151878359367816552922750854588003131965376928501067/451533030614789818307395007903408570485036256985049542679895194248586850032286001082252238114970055866379047240279225579322837814994099059850209592863880222382710486017566741864586911186401537110142362792356916190970074925646332909751019029726317586632321632422494257571068998380248837449032635313976908088640*y^14 - 130364484996567153177777036009034708869154637362748438001150849055742696675713798485323805025828636760495634805486049743988176709963866147918241464994501203958512794714658557606314968763815635810404368055891278056737991082361219133534616874931807503211417775796048835620382184650248050811614381406968181600348099/903066061229579636614790015806817140970072513970099085359790388497173700064572002164504476229940111732758094480558451158645675629988198119700419185727760444765420972035133483729173822372803074220284725584713832381940149851292665819502038059452635173264643264844988515142137996760497674898065270627953816177280*y^13 - 538944989680112014040682633478067168096196811111227245022351331536573041239750564910748724774014934850504460502038210211166186953578614932158445696682101378081032419997548460461547558794486103664517274537666556151447376243205749939143333617457273407332810634969031779072269047397998913606347327710940084393098799/903066061229579636614790015806817140970072513970099085359790388497173700064572002164504476229940111732758094480558451158645675629988198119700419185727760444765420972035133483729173822372803074220284725584713832381940149851292665819502038059452635173264643264844988515142137996760497674898065270627953816177280*y^12 + 2043707203422499663071369039068485839062234671410994040038182080470239845664938574191570881051753224469753441376585021407770608412152530811429785483887149378450831296995982421774650014438596894272425790664585713083257929405617628029720711069940830731510365416572674246717880729336256135364158944130631555559524841/2408176163278879030972773375484845709253526703920264227626107702659129866838858672438678603279840297954021585281489203089721801679968528319201117828607361186041122592093689289944463526327474864587425934892570219685173732936780442185338768158540360462039048706253302707045701324694660466394840721674543509806080*y^11 + 32908843359592485279937729763249902008588271477978910610246579631098740577923866257051155696119570884356435859785916724271951664196380004806955285377811487558280818976804197260193762640642052024290941591433295942997575543932455030257450627533689832705372603028335302415167701739552014848496206037118603413291903/481635232655775806194554675096969141850705340784052845525221540531825973367771734487735720655968059590804317056297840617944360335993705663840223565721472237208224518418737857988892705265494972917485186978514043937034746587356088437067753631708072092407809741250660541409140264938932093278968144334908701961216*y^10 - 25154486918729016286391149622925729020149424918850075253295936370584374722682839863259792500938538482280153517251338761474937505603118876684668421893366740532344812652860306845150940496404675103232111490051654731312119142805318193028003304148411989913002492315427884296224736541700737730555696736524482890988071/27365638219078170806508788357782337605153712544548457132114860257490112123168848550439529582725457931295699832744195489655929564545096912718194520779629104386830938546519196476641630980994032552129840169233752496422428783372505024833395092710685914341352826207423894398246605962439323481759553655392539884160*y^9 + 432946699618820563691951495183874470390594546057840664719705494719484723700654192233326503144177403562288845589106027339902937909799342765252700388182236741991336207139170675133253597110175453897735705723915562961602693916425716323819530661468885525192207368953025217314433659627102396814409700656563356791652981/481635232655775806194554675096969141850705340784052845525221540531825973367771734487735720655968059590804317056297840617944360335993705663840223565721472237208224518418737857988892705265494972917485186978514043937034746587356088437067753631708072092407809741250660541409140264938932093278968144334908701961216*y^8 - 73556850574053542397401370556578483286002436517332695848416621623527713668760173785442698928977053437557394311971294638152385013812605455166865761827512101060028374595822693308116152593417863617927268677444605337193511941927718332791516524060781641947238735976003860356363995032644134480374603699582192742730141/401362693879813171828795562580807618208921117320044037937684617109854977806476445406446433879973382992336930880248200514953633613328088053200186304767893531006853765348948214990743921054579144097904322482095036614195622156130073697556461359756726743673174784375550451174283554115776744399140120279090584967680*y^7 - 2906824217731065587546478353240979837535387551439123736142872686346165349102542465311744331986182350686692571366762874181511793573856655242264961285606051586230093861511492843548389865511115480941443607765086471645005114280000659729287074187858512107053140721286073527421730891107819650872027473655897866745984941/7224528489836637092918320126454537127760580111760792682878323107977389600516576017316035809839520893862064755844467609269165405039905584957603353485822083558123367776281067869833390578982424593762277804677710659055521198810341326556016304475621081386117146118759908121137103974083981399184522165023630529418240*y^6 + 183003391245236916713364647374599914732624645548839809150527228792676030719579882554797164741895083817704106938435411981975250372088203812849675929937510935422866517818263989268247618176887148832636562927167664635227495175752041359995351004392244652716000414101672576700862293295367808295024821015800075909196679/451533030614789818307395007903408570485036256985049542679895194248586850032286001082252238114970055866379047240279225579322837814994099059850209592863880222382710486017566741864586911186401537110142362792356916190970074925646332909751019029726317586632321632422494257571068998380248837449032635313976908088640*y^5 - 133306589024823305905129309980322902559195289002050987407980284561799413981217640173178725194929368625465265326372513931233749707119833883989547034071544462253006854110673008542299252460635162708894302472600480665893067540939128556114388611442508820083033641089425301486630999262194990614277060274380302344073025/722452848983663709291832012645453712776058011176079268287832310797738960051657601731603580983952089386206475584446760926916540503990558495760335348582208355812336777628106786983339057898242459376227780467771065905552119881034132655601630447562108138611714611875990812113710397408398139918452216502363052941824*y^4 + 295111596764084740314647449694442827909164611687439704796371622980960617801058846239310023232206962476245172812497322102007125320080864960359920044382831179382002260193465473479159307630437053297204279538784383209672621404341222863124895055662621179396132463223801853471008702331349801690975817900229090557846901/7224528489836637092918320126454537127760580111760792682878323107977389600516576017316035809839520893862064755844467609269165405039905584957603353485822083558123367776281067869833390578982424593762277804677710659055521198810341326556016304475621081386117146118759908121137103974083981399184522165023630529418240*y^3 - 49661530150653836093659897448374180739925484969881204304791525244344994670927317585732028479676205905587641783779249932105353971568397918965958521405407857101511039108950258963045479125129890483741438224630978023357506537474402640915181889038129189617492479139095966237948415550315695273160689030365565166233/16018910177021368276980754160653075671309490269979584662701381614140553437952496712452407560619780252465775511850260774432739257294690875737479719480758500128876646954060017449741442525459921493929662538088050241808250995144880990146377615245279559614450434853126182086778501051183994233225104578766364810240*y^2 - 522700058760388278390633215539716140558168017322012807386039191841778314260489622415589491857410534028905868855652676926051483007376453179495077860929167316285240872114145233680146359552097354586476515736831372441037883487982203909834267397204448963473803484619489657028671546481123240078863495676334174980689/1444905697967327418583664025290907425552116022352158536575664621595477920103315203463207161967904178772412951168893521853833081007981116991520670697164416711624673555256213573966678115796484918752455560935542131811104239762068265311203260895124216277223429223751981624227420794816796279836904433004726105883648*y + 116308150837795106437474722057875557914986903129685676956269212761474783332899430091046334717748294754338865152466763503295131814941017285969629057190837870215186586893435110383787360173145255677867473802649684894259664767797441853747026405653596247127471961241920387526591079772903672088011641136384020349263/7224528489836637092918320126454537127760580111760792682878323107977389600516576017316035809839520893862064755844467609269165405039905584957603353485822083558123367776281067869833390578982424593762277804677710659055521198810341326556016304475621081386117146118759908121137103974083981399184522165023630529418240