# Manifold: Census Knot K8_209 # Number of Tetrahedra: 8 # Number Field x^23 + 7*x^22 - 8*x^21 - 196*x^20 - 353*x^19 + 1320*x^18 + 4300*x^17 - 1706*x^16 - 16724*x^15 - 6785*x^14 + 29891*x^13 + 23867*x^12 - 26275*x^11 - 30096*x^10 + 10655*x^9 + 19070*x^8 - 1308*x^7 - 6525*x^6 - 314*x^5 + 1231*x^4 + 150*x^3 - 106*x^2 - 24*x - 1 # Approximate Field Generator -0.711313833659329 + 0.465270131603686*I # Shape Parameters -50977648656238992541987983210952/76302023526906674324433436645939*y^22 - 340956774902957811257232224890513/76302023526906674324433436645939*y^21 + 512779297686025459614084134269910/76302023526906674324433436645939*y^20 + 9822760597465750096261776920826495/76302023526906674324433436645939*y^19 + 14944131833400807260577651623543909/76302023526906674324433436645939*y^18 - 71696823211632824012952644325295421/76302023526906674324433436645939*y^17 - 196408137006534103035585474116557031/76302023526906674324433436645939*y^16 + 146534404319592723195353847907814025/76302023526906674324433436645939*y^15 + 801571948065387427471175157182059012/76302023526906674324433436645939*y^14 + 98069031524931300251368161700270445/76302023526906674324433436645939*y^13 - 1534891963170423190297812927034713294/76302023526906674324433436645939*y^12 - 731204948677093398652661572161890412/76302023526906674324433436645939*y^11 + 1534927896460230793976717832665240325/76302023526906674324433436645939*y^10 + 1034151872310341456570753491981201573/76302023526906674324433436645939*y^9 - 838012589714113463055028819136827488/76302023526906674324433436645939*y^8 - 688521897999753095239684911827345709/76302023526906674324433436645939*y^7 + 267836463283724504935012420540746031/76302023526906674324433436645939*y^6 + 237640528211936549842220495257356662/76302023526906674324433436645939*y^5 - 53350800038791165307300899062995290/76302023526906674324433436645939*y^4 - 43018787543502877381941290184283175/76302023526906674324433436645939*y^3 + 4532815761385841472899887221958089/76302023526906674324433436645939*y^2 + 3638256307403351143376644676829229/76302023526906674324433436645939*y + 332800250706453303021413459675320/76302023526906674324433436645939 34609108536987561534941482810802/76302023526906674324433436645939*y^22 + 244436791236620470509527742324552/76302023526906674324433436645939*y^21 - 248945152498499349623808185199203/76302023526906674324433436645939*y^20 - 6704675076588320763341503045236449/76302023526906674324433436645939*y^19 - 12687289202419824415068528316562710/76302023526906674324433436645939*y^18 + 42428605338893727098200344118142581/76302023526906674324433436645939*y^17 + 145796457855624515134651942768217518/76302023526906674324433436645939*y^16 - 36947086986221252898579106986566577/76302023526906674324433436645939*y^15 - 522431640248448898169453176508502827/76302023526906674324433436645939*y^14 - 255368714994315101985317277189582103/76302023526906674324433436645939*y^13 + 833597054313331146725114431318858106/76302023526906674324433436645939*y^12 + 704070264971106746516552783278302294/76302023526906674324433436645939*y^11 - 637556065703992650270116632879746409/76302023526906674324433436645939*y^10 - 723838108886700804807604743634957340/76302023526906674324433436645939*y^9 + 247500770136474486747991536221175921/76302023526906674324433436645939*y^8 + 375846489577099584128028165593033243/76302023526906674324433436645939*y^7 - 62912653934874136438965422387672533/76302023526906674324433436645939*y^6 - 109051381295808259454062319394431843/76302023526906674324433436645939*y^5 + 12256054383744714094162047513674487/76302023526906674324433436645939*y^4 + 16157851724494517596037290226705996/76302023526906674324433436645939*y^3 - 1268472301700926134106139982185841/76302023526906674324433436645939*y^2 - 965689544119291285712160623216363/76302023526906674324433436645939*y - 54119552782127733815707914905364/76302023526906674324433436645939 -9269970916336672850358272401206858/82940299573747554990659145634135693*y^22 - 146565612090043886349029863356427042/248820898721242664971977436902407079*y^21 + 173861498264783067748644269194678926/82940299573747554990659145634135693*y^20 + 4831699762179356719203298161222502103/248820898721242664971977436902407079*y^19 + 871790325862515377115393146442253777/248820898721242664971977436902407079*y^18 - 15562164566601842274835172859959472343/82940299573747554990659145634135693*y^17 - 48253385331691748252706513976834898726/248820898721242664971977436902407079*y^16 + 66135897622033060875610095385670111836/82940299573747554990659145634135693*y^15 + 264692479548448099021178939934027956989/248820898721242664971977436902407079*y^14 - 457875330702673688332270894529486241212/248820898721242664971977436902407079*y^13 - 649762471700384263560901613537645587028/248820898721242664971977436902407079*y^12 + 624367944525415515445935810923150871592/248820898721242664971977436902407079*y^11 + 856495583224520547477464568933619201886/248820898721242664971977436902407079*y^10 - 505542166432626260325490316859787253548/248820898721242664971977436902407079*y^9 - 647951919807131516368704315433412503570/248820898721242664971977436902407079*y^8 + 240315180468676281470465545163104322612/248820898721242664971977436902407079*y^7 + 285021055229585531339264784722345092957/248820898721242664971977436902407079*y^6 - 27004384284516358509011519496878722781/82940299573747554990659145634135693*y^5 - 18871192983504441279034829321162915576/82940299573747554990659145634135693*y^4 + 4781977560235590765060300618864317044/82940299573747554990659145634135693*y^3 + 1339125823145794341558681338803433666/82940299573747554990659145634135693*y^2 - 469898618060454881087885935359530381/248820898721242664971977436902407079*y - 22094860311887763277561346141849405/248820898721242664971977436902407079 571352364881694995615588948305165810/248820898721242664971977436902407079*y^22 + 3728243095489205342223048127583173577/248820898721242664971977436902407079*y^21 - 6308097417235239529597122111201575354/248820898721242664971977436902407079*y^20 - 108752422537141878992374839117644226125/248820898721242664971977436902407079*y^19 - 150228855106825714446983985784553540375/248820898721242664971977436902407079*y^18 + 819196219058520110388291820379942445851/248820898721242664971977436902407079*y^17 + 2054350748518634183925700716763273471840/248820898721242664971977436902407079*y^16 - 1914690001434370702667584457823532123495/248820898721242664971977436902407079*y^15 - 2834166357788133313422788214771935170719/82940299573747554990659145634135693*y^14 + 56189968309678904098969342116444548741/82940299573747554990659145634135693*y^13 + 5511242528865168540412083165258370076264/82940299573747554990659145634135693*y^12 + 5425667951068355145537593180188266951782/248820898721242664971977436902407079*y^11 - 5658602093590208522947841469684089707247/82940299573747554990659145634135693*y^10 - 2787949977276158684397252298215359656170/82940299573747554990659145634135693*y^9 + 3254678265217639978350386775346615848635/82940299573747554990659145634135693*y^8 + 5603997833048394084847869043148894407660/248820898721242664971977436902407079*y^7 - 3407583083251168876777191865420043079812/248820898721242664971977436902407079*y^6 - 612146242539015469893707005659920883523/82940299573747554990659145634135693*y^5 + 241366202864789940774596635541037742501/82940299573747554990659145634135693*y^4 + 99294042138261801774395913326664376483/82940299573747554990659145634135693*y^3 - 65258140235568817648855002282525644749/248820898721242664971977436902407079*y^2 - 7899633573105863923044033189198038493/82940299573747554990659145634135693*y - 818294569018618132366247489634360056/248820898721242664971977436902407079 -636787788517293580437959137373182313/248820898721242664971977436902407079*y^22 - 1481709645396388501036075212471368450/82940299573747554990659145634135693*y^21 + 5178120032513204820007554697019835821/248820898721242664971977436902407079*y^20 + 41563346594911043860059092213807587048/82940299573747554990659145634135693*y^19 + 222369327721256441918875390668460447868/248820898721242664971977436902407079*y^18 - 281463467318665635087926040458055918400/82940299573747554990659145634135693*y^17 - 2720576563756638075843259201559401742285/248820898721242664971977436902407079*y^16 + 1137067545702490828250963276115519180869/248820898721242664971977436902407079*y^15 + 10616405441627716804656205935394285415348/248820898721242664971977436902407079*y^14 + 4108540023673373363567696643627530937475/248820898721242664971977436902407079*y^13 - 6362426035368005274175313110303826999162/82940299573747554990659145634135693*y^12 - 14788605199150094285134266456830685194903/248820898721242664971977436902407079*y^11 + 5670745770177468425977632576038201105498/82940299573747554990659145634135693*y^10 + 18778815640510879124449102203484054583149/248820898721242664971977436902407079*y^9 - 7197184063230918417239675360277541262836/248820898721242664971977436902407079*y^8 - 11989578131521308042276613180192133441060/248820898721242664971977436902407079*y^7 + 373851677399685151926643426600279057329/82940299573747554990659145634135693*y^6 + 4152462356510689952288185887583952203496/248820898721242664971977436902407079*y^5 + 94369040575833969949599944375835394115/248820898721242664971977436902407079*y^4 - 799694377011722361067592213320802355151/248820898721242664971977436902407079*y^3 - 73186326523367255356352093557001876042/248820898721242664971977436902407079*y^2 + 72726791774833905700370052174159124363/248820898721242664971977436902407079*y + 13009316236435077601564986302079183730/248820898721242664971977436902407079 421074345563235585786088192742087717/248820898721242664971977436902407079*y^22 + 2772587421874583094408941895574662926/248820898721242664971977436902407079*y^21 - 4495394526351547363039473165529664641/248820898721242664971977436902407079*y^20 - 26831960996841730252521085181154485853/82940299573747554990659145634135693*y^19 - 115444502639081288293018791713583932435/248820898721242664971977436902407079*y^18 + 599012470742789794819232613778610230954/248820898721242664971977436902407079*y^17 + 1554431595132256366887221888501540942875/248820898721242664971977436902407079*y^16 - 1330354167289835902522330320831248482886/248820898721242664971977436902407079*y^15 - 6396050613100244609121464836809700278454/248820898721242664971977436902407079*y^14 - 262592618137099579542216862967593054420/248820898721242664971977436902407079*y^13 + 12334327363379934523714571804679265186547/248820898721242664971977436902407079*y^12 + 1622051742017600815506577437886526751780/82940299573747554990659145634135693*y^11 - 12447880205840855475920096526521043106376/248820898721242664971977436902407079*y^10 - 7180281105679229184454122548265235845995/248820898721242664971977436902407079*y^9 + 6907872068535384164936506176202452674842/248820898721242664971977436902407079*y^8 + 1589818776255799265914658053978881008489/82940299573747554990659145634135693*y^7 - 2279149188090388852311337547301858587756/248820898721242664971977436902407079*y^6 - 528188842723547554739359407962898765942/82940299573747554990659145634135693*y^5 + 154571944064896795163320944636166917883/82940299573747554990659145634135693*y^4 + 90456512333268486464462206423542430392/82940299573747554990659145634135693*y^3 - 41656662980035262663885377480392829373/248820898721242664971977436902407079*y^2 - 21759508354199169528445777579736930206/248820898721242664971977436902407079*y - 1293732779684001581188093188640223036/248820898721242664971977436902407079 22094860311887763277561346141849405/248820898721242664971977436902407079*y^22 + 182473934932224361494004240196566409/248820898721242664971977436902407079*y^21 - 10064423468352739957153635259456066/82940299573747554990659145634135693*y^20 - 4852177115924350805647956651386520158/248820898721242664971977436902407079*y^19 - 4210395150758579052060817783098447356/82940299573747554990659145634135693*y^18 + 28293425285829332149265583760798960823/248820898721242664971977436902407079*y^17 + 141694393040922908918019306989830858529/248820898721242664971977436902407079*y^16 + 10559553639611224101186857458839813796/248820898721242664971977436902407079*y^15 - 567922136722110135680766239033299784728/248820898721242664971977436902407079*y^14 - 414606106764606572859432673506476169914/248820898721242664971977436902407079*y^13 + 372770933428436940153952364018502268689/82940299573747554990659145634135693*y^12 + 392366834254736503235486087301721778721/82940299573747554990659145634135693*y^11 - 401636799740088831854620060266747995989/82940299573747554990659145634135693*y^10 - 1521462499171094671078950842418718894766/248820898721242664971977436902407079*y^9 + 740962903055790378047906460001192663823/248820898721242664971977436902407079*y^8 + 1069300905954831162071799186358480656920/248820898721242664971977436902407079*y^7 - 269215257756625475837515785916643344352/248820898721242664971977436902407079*y^6 - 429190018764653186725352568297912460582/248820898721242664971977436902407079*y^5 + 74075366715616317857880295802095455173/248820898721242664971977436902407079*y^4 + 83812351994447160431782505064105364283/248820898721242664971977436902407079*y^3 - 3677234544641202601182233311771846794/82940299573747554990659145634135693*y^2 - 6359432662497485932097546707446337928/248820898721242664971977436902407079*y - 60378029424851437573586372044855339/248820898721242664971977436902407079 54898266464364893059260195084697928/82940299573747554990659145634135693*y^22 + 1130009764231693862585701431157024181/248820898721242664971977436902407079*y^21 - 499666861209687790155390408404048840/82940299573747554990659145634135693*y^20 - 32235862739850433042907115038323266439/248820898721242664971977436902407079*y^19 - 53414929231090742606557999581842624315/248820898721242664971977436902407079*y^18 + 76502475805150465128518842312670451855/82940299573747554990659145634135693*y^17 + 683424037572008707483090632211502705167/248820898721242664971977436902407079*y^16 - 136548858962312697517028632120599909093/82940299573747554990659145634135693*y^15 - 2789484028965317805756760831585377386156/248820898721242664971977436902407079*y^14 - 664135222344144796199765242473545969219/248820898721242664971977436902407079*y^13 + 5378778437612333433750731205038916382792/248820898721242664971977436902407079*y^12 + 3236960384199470964082418904591832897021/248820898721242664971977436902407079*y^11 - 5432823294819079633075874786968251020770/248820898721242664971977436902407079*y^10 - 4530423265321100516295840870267955092916/248820898721242664971977436902407079*y^9 + 2969217038815138380494521347661616147597/248820898721242664971977436902407079*y^8 + 3141154070368881463701501628292514736886/248820898721242664971977436902407079*y^7 - 910107065760988772821089084675477390233/248820898721242664971977436902407079*y^6 - 391337449768976882918223816520891313867/82940299573747554990659145634135693*y^5 + 57925582570533908058437737086699790863/82940299573747554990659145634135693*y^4 + 77799507150274730342638519803838849892/82940299573747554990659145634135693*y^3 - 6008852944303528529793219559074376641/82940299573747554990659145634135693*y^2 - 21187833572402891947998861955182878249/248820898721242664971977436902407079*y - 970044599785045610098287121094930855/248820898721242664971977436902407079 # A Gluing Matrix {{2,0,-1,1,1,0,2,0},{1,-1,1,1,1,0,0,0},{0,0,0,0,1,-1,1,0},{0,0,0,1,1,1,0,1},{0,0,1,1,1,1,0,1},{0,0,0,0,0,1,-1,1},{1,-2,-1,1,1,-2,3,-1},{0,0,1,1,1,2,-1,1}} # B Gluing Matrix {{2,0,0,0,0,0,1,1},{0,1,0,0,0,0,1,1},{0,0,1,0,0,0,1,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,2,0},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {2, 1, 1, 2, 2, 1, 0, 2} # f Combinatorial flattening {-22, -11, 0, 11, 1, -11, -11, 1} # f' Combinatorial flattening {28, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant -35891477856795582793458014629663986017/248820898721242664971977436902407079*y^22 - 79037694381406313239876105350482643273/82940299573747554990659145634135693*y^21 + 380640241383041833441941725184551579338/248820898721242664971977436902407079*y^20 + 6886120910119687199169791150106489562994/248820898721242664971977436902407079*y^19 + 3319222202424937524163489521837177994531/82940299573747554990659145634135693*y^18 - 51330461483561959857638334943703092986931/248820898721242664971977436902407079*y^17 - 44729037449016181321509839318427720242718/82940299573747554990659145634135693*y^16 + 114281721168594262182191172597641397926330/248820898721242664971977436902407079*y^15 + 555986208340004653292740578807951190645832/248820898721242664971977436902407079*y^14 + 24363046239925152652444025827434965825978/248820898721242664971977436902407079*y^13 - 1085190817065751667592633692219600649211861/248820898721242664971977436902407079*y^12 - 430621673303360482702253359660064730696992/248820898721242664971977436902407079*y^11 + 1117237911998173136374412306119123930287676/248820898721242664971977436902407079*y^10 + 644488207197977843451949260823903884176089/248820898721242664971977436902407079*y^9 - 639557249854383102540943476742732682747276/248820898721242664971977436902407079*y^8 - 437503819168176687340624339146540517130497/248820898721242664971977436902407079*y^7 + 73250885384799077797737006672033218737973/82940299573747554990659145634135693*y^6 + 50055211010243819237504248737754565124067/82940299573747554990659145634135693*y^5 - 15820975273081802593403688143215687298797/82940299573747554990659145634135693*y^4 - 8680660252494427229952745293636516486720/82940299573747554990659145634135693*y^3 + 4747170496368273132366055398781529902421/248820898721242664971977436902407079*y^2 + 1994266152971007377678213548706582087798/248820898721242664971977436902407079*y + 31966603212649133847309507766385857914/82940299573747554990659145634135693 # 2 Loop Invariant -1676787996972679708363088339442763472600819159923798479333745016041294548754620815396475070805377836765134/46320194639562140283699737024882388991794538063656278188639503699435061251307094105018099624107239501296973*y^22 - 182996506527913228348629010455707793101634650055198419522850019429300925037155589500861398833440035261249831/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^21 + 41334803138530195304337893631040133417343590289807815872982645151113590588760051288784164721016476159110977/123520519038832374089865965399686370644785434836416741836372009865160163336818917613381598997619305336791928*y^20 + 1739620442174491995383722611577857382828685021661636912811090157343041759059884458953645572812479733855324533/247041038077664748179731930799372741289570869672833483672744019730320326673637835226763197995238610673583856*y^19 + 8535885529729911710793338223787713978283837569745096904125327251072221909034978607460383884676287492585610589/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^18 - 18530701275843221204200042677883079937742927924150044861707257656593999489399241028713332919391567138146284041/370561557116497122269597896199059111934356304509250225509116029595480490010456752840144796992857916010375784*y^17 - 18176625686143324036916444889962108293738967098761931955996758285955842047194409877831370790629682472490754349/123520519038832374089865965399686370644785434836416741836372009865160163336818917613381598997619305336791928*y^16 + 65759971362775035555188661283072351088770755140716603067153068216789470786010851552961513392324599013971070929/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^15 + 73334001729382212200965776809784636569642504176099057645625762128761555578741129772442228082041726635257070011/123520519038832374089865965399686370644785434836416741836372009865160163336818917613381598997619305336791928*y^14 + 52730383399384104273242987692321042658478041733929076202590599187835388024629309775047702431251688231823552907/370561557116497122269597896199059111934356304509250225509116029595480490010456752840144796992857916010375784*y^13 - 829000455660242056689370490340154404242454837134897865147476359548214415030820981548307173411745803596091230045/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^12 - 126351727206151992283019067587682427365804549222139328735243524940629548336867012997911872684845418563903823407/185280778558248561134798948099529555967178152254625112754558014797740245005228376420072398496428958005187892*y^11 + 800811710741163975545182030121988892939861522860470011535522246090691034688491476434915287667686670391049893829/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^10 + 114689607360381785407064027176773976847619295140827862237264199150533253639034306857020193318770746985387090895/123520519038832374089865965399686370644785434836416741836372009865160163336818917613381598997619305336791928*y^9 - 50251873287586025886144864003022153862667268226320297874698520698240696209883062110029051004354495306569463633/92640389279124280567399474049764777983589076127312556377279007398870122502614188210036199248214479002593946*y^8 - 458060656901815057525732643581296825346167545564069515932337213187030418225478838959214245915767958818443715283/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^7 + 208077482893544609757291731077097572209192706108162243825176892979972008338506482439835285561532144190518645/1458903768175185520746448410232516188717938206729331596492582793682994055159278554488759043278968173269196*y^6 + 20356828201059383157827229398595196004100685326692620375881725935765023661665256456567466991214823487936638357/92640389279124280567399474049764777983589076127312556377279007398870122502614188210036199248214479002593946*y^5 - 14427723381813126546630557411295506348067393257097717669291659093561977313802277094900094029904315604477537331/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^4 - 31571576552259275402478461556004524825637127855132112909751275916764525690299539977621546743707334568860632151/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y^3 - 26327226129408448876392475384111497907126102602632997081228629011870466514299860585378787856601194039994149/82347012692554916059910643599790913763190289890944494557581339910106775557879278408921065998412870224527952*y^2 + 2884879209861799596752313901781848062407685871158025497499769733674401684261225759437346326640052113715567371/741123114232994244539195792398118223868712609018500451018232059190960980020913505680289593985715832020751568*y + 1564516655299242171399949278150442321485429254444261066773255723907055895941750618677358454421070893654285161/20586753173138729014977660899947728440797572472736123639395334977526693889469819602230266499603217556131988 # 3 Loop Invariant -2658904279925721326945506650560166063378741451273504441909180323869424391601237378019839173550447086152829928739793290209535640355826014737571/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^22 - 4556840094760350618803598040428302373862835604972103739953052360548004730822381654117738516098142370517876867796631279643966890890303606330845/61538971959234506729619673972485321815049322333498972153627957302161452095892866114717184205645127305355064328015715050484371870529640487278512*y^21 + 24020105899869697386939613023497485765325109138073522524967201320518877792166314064469450928438207799624748775951782582190177571939536391840531/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^20 + 172786534851390595479507789353094727033252717908394007371877238379410159034542534140098630990001038397861822297524518948980398015666039884079625/82051962612312675639492898629980429086732429777998629538170609736215269461190488152956245607526836407140085770687620067312495827372853983038016*y^19 + 862185585272662221437830950982515192309037808561381063536293314909640325869776129341460343099560652451934082388130773430354410735654720105793471/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^18 - 57111121687363940120913038785220700000088619383568715416987406989264859328778928279944613250199931478827317859882008010030922098391895292846517/3846185747452156670601229623280332613440582645843685759601747331385090755993304132169824012852820456584691520500982190655273241908102530454907*y^17 - 10928425892326652884566349309027833472330656476012163739567299794989177698574283372274987149793229174009428565439456906175914660757396430112137909/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^16 + 1569825565859457817195223303298177856317976168445378222801103023565983014541489295135375163993459844368049000209619729086641488379243279173037347/61538971959234506729619673972485321815049322333498972153627957302161452095892866114717184205645127305355064328015715050484371870529640487278512*y^15 + 10978261999111844469068022262943412320082184720965111694973343678600376295570230779728617713095863068674541549392785995061554265653413642724372841/61538971959234506729619673972485321815049322333498972153627957302161452095892866114717184205645127305355064328015715050484371870529640487278512*y^14 + 11246303488406121084847143804357683782545151731317550701260181317688438117708205658322964260230977317295733995150598110974236295352973887757859155/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^13 - 5162402170392995796866727651366067711146113696700960770418223097743695176633351559966817381159889657606737650593505535378426812483328067469124277/15384742989808626682404918493121330453762330583374743038406989325540363023973216528679296051411281826338766082003928762621092967632410121819628*y^12 - 8522181018781821496455298305934733672243721464710927066533201195328440525711605562823341389570052723410283278913800318772547617815250694922197557/41025981306156337819746449314990214543366214888999314769085304868107634730595244076478122803763418203570042885343810033656247913686426991519008*y^11 + 80224380304536423874452662979659980917299424643496316597471511035584939827244087341379541067374387518968425541466012215387630340516016055895516183/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^10 + 68690226264581981948048449876900544495480666693602950657335407832489614957277264359720979921269586559255656633021419531618162391860092305353073381/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^9 - 41423575735975904953045859508344383018840758750944720092471348830804420069349590780956170806359283271360586668216082452218553036916836372857467245/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^8 - 236487584107184401269810152530682455669287190916468336194250858263785391647300395041361467186047847186006986895106685481165492734577807043237933/1282061915817385556867076541093444204480194215281228586533915777128363585331101377389941337617606818861563840166994063551757747302700843484969*y^7 + 2999177682432169349513026278255132251241888386513082249355075922924556182166841967625795202845579623258333233673709542870379124399206313624293299/61538971959234506729619673972485321815049322333498972153627957302161452095892866114717184205645127305355064328015715050484371870529640487278512*y^6 + 2680203103733810555421672094493673425757717944846938320924899224607438761839402426040854138378117089483862819535137299188410197493848907409182527/41025981306156337819746449314990214543366214888999314769085304868107634730595244076478122803763418203570042885343810033656247913686426991519008*y^5 - 751988597166334796707281962788200073460342960293806534865018785755648998864411249587131130735021069921926953378435411422107524552296642986615863/82051962612312675639492898629980429086732429777998629538170609736215269461190488152956245607526836407140085770687620067312495827372853983038016*y^4 - 511801694148275345465265264970625702689702316047248858281759808627380921311608035791321072502712752862172765866584493358846278429815701596190085/41025981306156337819746449314990214543366214888999314769085304868107634730595244076478122803763418203570042885343810033656247913686426991519008*y^3 + 229310308122104009140485941626609248959624524256692077509815789194500548877185626879540726905884642748135754237599497094865251723249375775701741/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y^2 + 266552635727232024341894087901404281959236363647510509915479249395551259115662283661534232566199942735822565816805579217997646272323832431628989/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048*y + 13767986016306724683318150487711336389895862270319804383330352361144835893319181936976878845794604153907236722589432030860714395014943391312403/246155887836938026918478695889941287260197289333995888614511829208645808383571464458868736822580509221420257312062860201937487482118561949114048 # 4 Loop Invariant 4163786740555436813315572002839957344828046404379126447796501819884785952088431146689111637183505800129537867429857358382980574465204555682396806341397190417454194019479846465103487104386333082718814914647173736807/229120397339593940496472104893057670696402738082604480177525350596850073363354843284182268450884544251189000092991229360832573288848017679837055207449720457692561924421176157049862368800671411513289231081663303426880*y^22 + 457546504779787308515675634760007161581901866945218186450472299426137200292969162867269365518140720912535746028073832162666366253739435421979691957207603178145058448283708939530385191678924029570496540061642874259383/3665926357433503047943553678288922731142443809321671682840405609549601173813677492546916295214152708019024001487859669773321172621568282877392883319195527323080990790738818512797797900810742584212627697306612854830080*y^21 - 178623575127689517459890431293452944333297826208193687167383817789708776482202195754825616552417673823424800055990516850683222632050168859462598244817138366680974037519707856087173060200995588782859078811131599935989/1099777907230050914383066103486676819342733142796501504852121682864880352144103247764074888564245812405707200446357900931996351786470484863217864995758658196924297237221645553839339370243222775263788309191983856449024*y^20 - 7796602724734140365674179529005836069307008954960921623427008426865751318870008863373086996892098393392107973786258437268999146524196264872406988936566889398457314036106306149243289070567208545897823314375644067744567/2199555814460101828766132206973353638685466285593003009704243365729760704288206495528149777128491624811414400892715801863992703572940969726435729991517316393848594474443291107678678740486445550527576618383967712898048*y^19 - 65383667152359567202366277660554817321625771085040727258050872044940023684486207498150143107876687088858056463624344094578787935930760840688819191557814938602655393226093759119081473917834019314751592664231344185230413/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y^18 + 273633710047824479828236735651338296600999045105208949468207533181137353358921216197815032707101949648274865893870647387083052286341914141397152807039986279640240092347531607527493873723003242387756828510932099039612183/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y^17 + 826107026707101307878427833561591008201263913943266704457153733034876818636568713969530494502116511449211744004951163060813325440894353442193043200736750426818385332865428241696651434074237837645316500413684430002065077/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y^16 - 30394398297093857618428091084766332302574249700404478623059409000887185758107158319142227717129288336541527333040764256413720446433130793953849175898316575918004087974090999860181864316207355691238553360430273631118215/733185271486700609588710735657784546228488761864334336568081121909920234762735498509383259042830541603804800297571933954664234524313656575478576663839105464616198158147763702559559580162148516842525539461322570966016*y^15 - 55177985472051696152499773517864951528970125786374724687440188546528991053860973701823360425111211130102562888416959731987017535260167031733753142303700821121089537982497445424998036649622021625589231715265227792521247/183296317871675152397177683914446136557122190466083584142020280477480058690683874627345814760707635400951200074392983488666058631078414143869644165959776366154049539536940925639889895040537129210631384865330642741504*y^14 - 927969114557895322868444672162278111826974775183979424889133175389541861718588750218384448196883223705758850376149167643972373820718129585051155138178330185614349338071900060055760057994820126799901216949964799627997763/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y^13 + 3090623639922083139155765565530938324896900157712200865181163201608831244103927487345639785861234639951009686203701303151078888902595814513271271299951201031431150945728585968543492845768566885915936128795151807776690911/5498889536150254571915330517433384096713665713982507524260608414324401760720516238820374442821229062028536002231789504659981758932352424316089324978793290984621486186108227769196696851216113876318941545959919282245120*y^12 + 337074833262889170424798102542099835244512298183299827496626080071336747105302314979139353157110434517759856063981610302111575393474167262687851652330241806818453020271105548801280914149985752310540530820899554134594283/916481589358375761985888419572230682785610952330417920710101402387400293453419373136729073803538177004756000371964917443330293155392070719348220829798881830770247697684704628199449475202685646053156924326653213707520*y^11 - 5875426006185500920285766185247870764494207153787806054971252851924106219560939033458317702876785803985437095131450815410346158066367460807938992269439929430504480193885497616889049250311622443423167590544379110029730273/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y^10 - 150324919862230192799129515264172483651121104255604383811361547710903428553907517864471045287128783467083424632253878745655004529278146708541020609071309299402166546055959620551462903689772885482389846028552797159987453/305493863119458587328629473190743560928536984110139306903367134129133431151139791045576357934512725668252000123988305814443431051797356906449406943266293943590082565894901542733149825067561882017718974775551071235840*y^9 + 712087799042220758023286935942580691875062677684463915079860336465840238628920906947041082921575469366353260685692612515217555776177987605752478826228894036201725516875063975451933591876387584714310332629702407303605197/2749444768075127285957665258716692048356832856991253762130304207162200880360258119410187221410614531014268001115894752329990879466176212158044662489396645492310743093054113884598348425608056938159470772979959641122560*y^8 + 3563853848187016657165012211691252987665210582954824819075501806068146869691728475157230676841374287644436737510168472191992208388974628547041803810149128069034244241711161153261833704077330783597045200320309438670799041/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y^7 - 602117801740483438106991468533455419082381438174225806406705139764333694022599310244826056517726886842249414870823818325378872673228058652184381654926612085585585056101299231120594393153003396820829197558975527723107/9621853956518380703263920415456490107985416822366592343413138082807352162240623340018153005811424430496125988157111994155698615804641162407855336795788785624884490264406347802618892128112185260400597630726017991680*y^6 - 1253147508922333113009507155840596378738074408120088383919675628072276087711019198003771367440377453256955904099203841853090101776994911162404198075022935071811738108692370187070063883349403286031278888440978685532015213/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y^5 + 15918229462602825268997964977625870927658631459729530487775875965172018741023886437600738589926585866880257644388127078465754728929359001849896646244040030362752662469021610549058186509416722478989725201805616153614509/2199555814460101828766132206973353638685466285593003009704243365729760704288206495528149777128491624811414400892715801863992703572940969726435729991517316393848594474443291107678678740486445550527576618383967712898048*y^4 + 119774950250776356469919398229749789205127586563809886364225002011668198877201193491790031634894294565747906980919033073232430970574386764328387884595220407093127285575825909209536999709386676399168434297040913346238547/5498889536150254571915330517433384096713665713982507524260608414324401760720516238820374442821229062028536002231789504659981758932352424316089324978793290984621486186108227769196696851216113876318941545959919282245120*y^3 + 1583245938735733840072430365199756221399861269493040224141062179367395129793815244073976215166641953901594408405235790565484078049936621924966870255042737611265348703917887306170824505634019467452246878035807078845991/5498889536150254571915330517433384096713665713982507524260608414324401760720516238820374442821229062028536002231789504659981758932352424316089324978793290984621486186108227769196696851216113876318941545959919282245120*y^2 - 21122191517983905116880665417371538791192310923530026479734193038222169641248749275923932870767691666719162501315572425880135415262773249125659129315819537980316978153945940132322358169782534820250132341092424242137157/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240*y - 2472606292081143531624112230371534301830913582180465365434899743106536085427726261997889521907364076561785588857269333078310363238692886118352317975556312444372812108463170606034529946633433240605767518735966154705673/10997779072300509143830661034866768193427331427965015048521216828648803521441032477640748885642458124057072004463579009319963517864704848632178649957586581969242972372216455538393393702432227752637883091919838564490240