# Manifold: Census Knot K7_37 # Number of Tetrahedra: 7 # Number Field x^21 + 10586/1189*x^20 - 61041/1189*x^19 - 245163/1189*x^18 + 254695/1189*x^17 + 244946/1189*x^16 - 36704/41*x^15 + 1512922/1189*x^14 + 152013/1189*x^13 - 123116/1189*x^12 - 385912/1189*x^11 - 749043/1189*x^10 - 143003/1189*x^9 + 294516/1189*x^8 + 223761/1189*x^7 + 71407/1189*x^6 + 8283/1189*x^5 - 2278/1189*x^4 - 1199/1189*x^3 - 239/1189*x^2 - 24/1189*x - 1/1189 # Approximate Field Generator 0.641192778853323 - 1.32175910167878*I # Shape Parameters 4389372331381093543578474241342529573339495395730447300299538206475521365/14818051611300348172252176743836333735476524755094300340242760073579*y^20 + 1551663061515975869684730099986965213135028523436047977325142615241604339077/607540116063314275062339246497289683154537514958866313949953163016739*y^19 - 9675116009439805332789281737251011757765489917896596212520041659399583241240/607540116063314275062339246497289683154537514958866313949953163016739*y^18 - 34384277509531365211365296428635349276843345030440038019628808024715073979985/607540116063314275062339246497289683154537514958866313949953163016739*y^17 + 48204860812079092324306004240434927301858750194782905659763727641234888106776/607540116063314275062339246497289683154537514958866313949953163016739*y^16 + 23471602204288859906455730809670252492779705276526082941276340567529165548644/607540116063314275062339246497289683154537514958866313949953163016739*y^15 - 167626620150878329556230198180230577172384568610386380965202861561049813333041/607540116063314275062339246497289683154537514958866313949953163016739*y^14 + 276147047655177910855103757718902357473631061179082131606565309540564053894438/607540116063314275062339246497289683154537514958866313949953163016739*y^13 - 54898006901901336564738338909864461908555673819348290273984048461685570333993/607540116063314275062339246497289683154537514958866313949953163016739*y^12 - 2733809482990956889758179468374418481887748834522839824972200506604213425258/607540116063314275062339246497289683154537514958866313949953163016739*y^11 - 57830970043083642488627573846464196301333826746710849389784668511484434185121/607540116063314275062339246497289683154537514958866313949953163016739*y^10 - 97071162844864632030136231237396476653165899810608369679950943155337654878466/607540116063314275062339246497289683154537514958866313949953163016739*y^9 + 5561059292875169521048535525386437624980586617485901492631194714868477224392/607540116063314275062339246497289683154537514958866313949953163016739*y^8 + 42893146621747896658065774553100964414709032620997794028799680420928302503055/607540116063314275062339246497289683154537514958866313949953163016739*y^7 + 21842649533481536901552460435759271452957352384787863306236320036627593860437/607540116063314275062339246497289683154537514958866313949953163016739*y^6 + 4719572929508820585861663447859575917656713906841526050881396781383133549028/607540116063314275062339246497289683154537514958866313949953163016739*y^5 - 54730820653014593471369855245993623987066395650916306501249679243641110979/607540116063314275062339246497289683154537514958866313949953163016739*y^4 - 327109493890572380254306966782847827024714124863367111954202080674522698478/607540116063314275062339246497289683154537514958866313949953163016739*y^3 - 90139839799116773856083495898346885328445129975280266944918908936300368266/607540116063314275062339246497289683154537514958866313949953163016739*y^2 - 11151450256988350557985018575875465163328364472029919190609479542141623937/607540116063314275062339246497289683154537514958866313949953163016739*y - 549620948215860047664345954994639910071121438987301802411996175850157110/607540116063314275062339246497289683154537514958866313949953163016739 668561789375018593687734189894950420223226115021064444064697965280776192/14818051611300348172252176743836333735476524755094300340242760073579*y^20 + 237256986193050013361890053766763841389698646520892788272302575661156812863/607540116063314275062339246497289683154537514958866313949953163016739*y^19 - 1465957526792445585385185290270018664203566823755535922118109315062222770093/607540116063314275062339246497289683154537514958866313949953163016739*y^18 - 5288311113644781142947106199344232998848139233095255861321145144964844102929/607540116063314275062339246497289683154537514958866313949953163016739*y^17 + 7178893093517886117154660082831137673423324949170042182178123821065130904364/607540116063314275062339246497289683154537514958866313949953163016739*y^16 + 3858900397256117629281976466199548029917869191151515834775714584554156256234/607540116063314275062339246497289683154537514958866313949953163016739*y^15 - 25478154940061180915977210655071308718334940039027405634123028874781557136303/607540116063314275062339246497289683154537514958866313949953163016739*y^14 + 41193645612849205307043996778640906777410043116048643179971237237591686024501/607540116063314275062339246497289683154537514958866313949953163016739*y^13 - 6751960983951050412071980031519323383825053534208406609340639101936652199885/607540116063314275062339246497289683154537514958866313949953163016739*y^12 - 1070296475638229106626459318872952531391105035821985297382588644275860925406/607540116063314275062339246497289683154537514958866313949953163016739*y^11 - 8672138145327420108904093273105776087639073978601005098512175059014539203075/607540116063314275062339246497289683154537514958866313949953163016739*y^10 - 15110650324323062877691892840099639551676132215745796321309580554425979355251/607540116063314275062339246497289683154537514958866313949953163016739*y^9 + 427683952806734802838118139592921307199066808219403451062533169256513621758/607540116063314275062339246497289683154537514958866313949953163016739*y^8 + 6659680922017789471292772661864669715080945310973897583880311343420309947684/607540116063314275062339246497289683154537514958866313949953163016739*y^7 + 3516533190561048732177054857798404664863295551538802519270209034431622076141/607540116063314275062339246497289683154537514958866313949953163016739*y^6 + 785765432956329683328582989656898687992397595383480741306771761643251162055/607540116063314275062339246497289683154537514958866313949953163016739*y^5 - 47828836251913068456770521347500070109760905486155710844105091308209443/607540116063314275062339246497289683154537514958866313949953163016739*y^4 - 52062473982163247160548642772252018547455923673417287525338703739675420333/607540116063314275062339246497289683154537514958866313949953163016739*y^3 - 14869445829177106226233788692509111677780546775491064422604616719120490495/607540116063314275062339246497289683154537514958866313949953163016739*y^2 - 1888554902285466937034753067278050685270089328536919158643927408657288810/607540116063314275062339246497289683154537514958866313949953163016739*y - 95566001582887784595931290966853580671161628453236524697283237516527345/607540116063314275062339246497289683154537514958866313949953163016739 3334575620005938349387999095604009381086088502165171524237946682085440531/29636103222600696344504353487672667470953049510188600680485520147158*y^20 + 590253713132535262710259945902344693063939003092094329811313131880501116379/607540116063314275062339246497289683154537514958866313949953163016739*y^19 - 7335801724824147696636011058884749131916379118633082762358338284725675735797/1215080232126628550124678492994579366309075029917732627899906326033478*y^18 - 26218218114822758944195423863914601716694054114031604749585506198815765545527/1215080232126628550124678492994579366309075029917732627899906326033478*y^17 + 36321044739543446183552624184486173686442814121882332241919730257529552251145/1215080232126628550124678492994579366309075029917732627899906326033478*y^16 + 18381333002707018916558590426845672728528377749917315925881191283809227688425/1215080232126628550124678492994579366309075029917732627899906326033478*y^15 - 127283360954089409978212967620162003795740691037696603587768678518765880253077/1215080232126628550124678492994579366309075029917732627899906326033478*y^14 + 208165258433970535414911320604343839329107250362523727372304237382937315716373/1215080232126628550124678492994579366309075029917732627899906326033478*y^13 - 19292081888433250657859286408948299755874503948684269399009010286368192965404/607540116063314275062339246497289683154537514958866313949953163016739*y^12 - 1762849726156471406470107367255908689768962393827096263038567174696413318149/607540116063314275062339246497289683154537514958866313949953163016739*y^11 - 43537898481326866470408655102876059387707527560016652198063962515389988149811/1215080232126628550124678492994579366309075029917732627899906326033478*y^10 - 37204698622736420356891002704875555327273013451613365680705497520893685728849/607540116063314275062339246497289683154537514958866313949953163016739*y^9 + 3493035162410981230181942762260487933312961762820910793749460296172501825211/1215080232126628550124678492994579366309075029917732627899906326033478*y^8 + 32858318373456595679793987337666687489107894859856857900211537705073207975985/1215080232126628550124678492994579366309075029917732627899906326033478*y^7 + 16924116172906329944039683786153374475843339563518795675220581068249642580439/1215080232126628550124678492994579366309075029917732627899906326033478*y^6 + 1847409486919067422953217823998828833636469880769809764463895871530006792630/607540116063314275062339246497289683154537514958866313949953163016739*y^5 - 14844363303137442623775592581529834606628936145902583459364606718073291124/607540116063314275062339246497289683154537514958866313949953163016739*y^4 - 126347976235909420538523230005845523358225218735342824806909153823603764373/607540116063314275062339246497289683154537514958866313949953163016739*y^3 - 70338279026581730456239610850852126123901823565431426266268433816850277439/1215080232126628550124678492994579366309075029917732627899906326033478*y^2 - 8761753971937411956445620323634850362975768059766215136647582511343852985/1215080232126628550124678492994579366309075029917732627899906326033478*y - 433376498786126460740398813087818125732678632715141895484758054654131767/1215080232126628550124678492994579366309075029917732627899906326033478 -1310165173884759313339446878792739637657305015152657648866782065827533782/14818051611300348172252176743836333735476524755094300340242760073579*y^20 - 477570727480484747648293089885567050398164067498396525385915198544109747601/607540116063314275062339246497289683154537514958866313949953163016739*y^19 + 2766441834757544997370727223029063400863801798560090396934060161919713890589/607540116063314275062339246497289683154537514958866313949953163016739*y^18 + 11062978807750392372693980136086484648432493277296564967217189649404466965826/607540116063314275062339246497289683154537514958866313949953163016739*y^17 - 11793623137930994453375322562055596872874138130277829718840758056098061545337/607540116063314275062339246497289683154537514958866313949953163016739*y^16 - 11392360876399829720809745533238267377104619439673175173686376028297015006181/607540116063314275062339246497289683154537514958866313949953163016739*y^15 + 49029820584325487152564264472048739348265895701358234711709365342442499653555/607540116063314275062339246497289683154537514958866313949953163016739*y^14 - 68780413201228491810899132010903066940765788858569856849640512904900874862843/607540116063314275062339246497289683154537514958866313949953163016739*y^13 - 8486425997023244031824599519543702942322343999882181075325829794408633639016/607540116063314275062339246497289683154537514958866313949953163016739*y^12 + 10185786713247879963806904776846475365252880093822878211978715462650676185827/607540116063314275062339246497289683154537514958866313949953163016739*y^11 + 15658914596247394086986963576355193999275216288461835257289944649423787210185/607540116063314275062339246497289683154537514958866313949953163016739*y^10 + 33896140169619142928856549315647892896023132673105707852016275679104099635968/607540116063314275062339246497289683154537514958866313949953163016739*y^9 + 5140927309418823910306539974573533529503227753860112723848330464689303944962/607540116063314275062339246497289683154537514958866313949953163016739*y^8 - 14629500241222213178483100781644217962385680389644149790839612162464681375693/607540116063314275062339246497289683154537514958866313949953163016739*y^7 - 9601763611855295616540580229034116952066154986035196873838240872155867605338/607540116063314275062339246497289683154537514958866313949953163016739*y^6 - 2532755031616020992968287017339897220075423244440746698624796604062358516867/607540116063314275062339246497289683154537514958866313949953163016739*y^5 - 130622576806357310325903769708362999553395132265793307080097948832103062292/607540116063314275062339246497289683154537514958866313949953163016739*y^4 + 132879197800223562434600310205772304134062295630144865438870679567713793423/607540116063314275062339246497289683154537514958866313949953163016739*y^3 + 46092470142442854489068823415507022700982374916531954916070788983290824044/607540116063314275062339246497289683154537514958866313949953163016739*y^2 + 6618759584511952229417369405836503663032856740478004951536661554092085475/607540116063314275062339246497289683154537514958866313949953163016739*y + 375923603825783302395653216276670375701663795114347873260077384691207076/607540116063314275062339246497289683154537514958866313949953163016739 273457003927971901769126676137118233194532521139466957016022932884792586/14818051611300348172252176743836333735476524755094300340242760073579*y^20 + 97313551056667736517426620349520751436573217783974023479784199627533503249/607540116063314275062339246497289683154537514958866313949953163016739*y^19 - 597433128141490106496854346134883091171372320905506455256567628322519582646/607540116063314275062339246497289683154537514958866313949953163016739*y^18 - 2178805101414336562864526905340324111470989453351534175172363139573469556413/607540116063314275062339246497289683154537514958866313949953163016739*y^17 + 2893352317938426542562123801594209853502550502595337074368846251324416256695/607540116063314275062339246497289683154537514958866313949953163016739*y^16 + 1676384225515151821409894669680797153354787262114535927263511391454629657442/607540116063314275062339246497289683154537514958866313949953163016739*y^15 - 10436389457591492012111229478200925611676135930321290308203607326343401711316/607540116063314275062339246497289683154537514958866313949953163016739*y^14 + 16596590231947765369829769053987222733409681494378435428452942348872670031339/607540116063314275062339246497289683154537514958866313949953163016739*y^13 - 2204954458437150545723061627890315894480514820242781642948772785533303207417/607540116063314275062339246497289683154537514958866313949953163016739*y^12 - 806644109971564518433228594789535621913859993822095679502463361577406579602/607540116063314275062339246497289683154537514958866313949953163016739*y^11 - 3398806103384651639201953833356994368708140353116776228686888711883313492802/607540116063314275062339246497289683154537514958866313949953163016739*y^10 - 6317339941026699102208352851922544832812623494013558965310102870746879190017/607540116063314275062339246497289683154537514958866313949953163016739*y^9 + 93338936066256068616130178205296214958295000223753124092841023478868173881/607540116063314275062339246497289683154537514958866313949953163016739*y^8 + 2790987423594437638431943631047510308198587787266463873439293885644267182885/607540116063314275062339246497289683154537514958866313949953163016739*y^7 + 1474369896607021083523257573744663807356780786313595054886301797955570138987/607540116063314275062339246497289683154537514958866313949953163016739*y^6 + 327959318414877331386929049278571918387264223590104084653789506526988667171/607540116063314275062339246497289683154537514958866313949953163016739*y^5 - 700648687389015858005476038178753299958403686517777050922002857054200698/607540116063314275062339246497289683154537514958866313949953163016739*y^4 - 21986898163887398259788109689130657391312043383222487643622516634368020618/607540116063314275062339246497289683154537514958866313949953163016739*y^3 - 6205210452925433183690163406511681192331140581341744332542951565592604019/607540116063314275062339246497289683154537514958866313949953163016739*y^2 - 775147862097246737657192792294472363369174089212451684782757637980790665/607540116063314275062339246497289683154537514958866313949953163016739*y - 37574288678028385498257854032704451159363510595452162272359666610497358/607540116063314275062339246497289683154537514958866313949953163016739 -23392873077126438807997580265815185347414889823019973143963700345329253625/14818051611300348172252176743836333735476524755094300340242760073579*y^20 - 8304419644687048935072568527440877251669438581033734956414298549226063368212/607540116063314275062339246497289683154537514958866313949953163016739*y^19 + 51271544876973148879982866242797385622417782882855047355430327974141935829452/607540116063314275062339246497289683154537514958866313949953163016739*y^18 + 185208902454205038558317867693335169300019323352599203686253053890286027205464/607540116063314275062339246497289683154537514958866313949953163016739*y^17 - 250781943301088350209635276335739820897375217523467890194530393847152185359848/607540116063314275062339246497289683154537514958866313949953163016739*y^16 - 136175014396820958225480078428891309497336134206731142081172877294998751677758/607540116063314275062339246497289683154537514958866313949953163016739*y^15 + 891911831228606169194324788843680339811732136506337522825267284780713554606573/607540116063314275062339246497289683154537514958866313949953163016739*y^14 - 1438743541535211295366418321954360980630514300262683992779653242323687354772920/607540116063314275062339246497289683154537514958866313949953163016739*y^13 + 229686048503222101521735638866292425592424430040439345376025647480859818158996/607540116063314275062339246497289683154537514958866313949953163016739*y^12 + 42885653011676701524249467348096277095762373548782535387901769982480397583383/607540116063314275062339246497289683154537514958866313949953163016739*y^11 + 300875259759186800239187185786636075681791979171807156611504130254943988260149/607540116063314275062339246497289683154537514958866313949953163016739*y^10 + 530551671395517799294662685893613313549110858949847350743086773634423200248997/607540116063314275062339246497289683154537514958866313949953163016739*y^9 - 14486932878806662685570903997652819989943834616015434495197065839142984183448/607540116063314275062339246497289683154537514958866313949953163016739*y^8 - 233970298463585902301757180415894143991335234393210418984325566482046791309288/607540116063314275062339246497289683154537514958866313949953163016739*y^7 - 123238692121277806090221912267979884864077502602175657109437410906911577649008/607540116063314275062339246497289683154537514958866313949953163016739*y^6 - 27456203774860009965400706745601597370147820385695449113291817687038123168099/607540116063314275062339246497289683154537514958866313949953163016739*y^5 + 31555403630918634139172336665771356147191113774580028912026156427326860499/607540116063314275062339246497289683154537514958866313949953163016739*y^4 + 1828826739698549032895263262030301053784994799890753964706421408535760022739/607540116063314275062339246497289683154537514958866313949953163016739*y^3 + 519754333697624635113209280306752335888955665911494515128429519237695640441/607540116063314275062339246497289683154537514958866313949953163016739*y^2 + 65696285395107725595022523785274486039672332261464692941768111757219827512/607540116063314275062339246497289683154537514958866313949953163016739*y + 3301768514595176345531618892057786261673042148080614374058422063431385326/607540116063314275062339246497289683154537514958866313949953163016739 3055323542015507965318875313817444126527409317621658728966122799923938990/14818051611300348172252176743836333735476524755094300340242760073579*y^20 + 1081389639748550995474915001187046871008255165191502564661933598725869026000/607540116063314275062339246497289683154537514958866313949953163016739*y^19 - 6723696523314185349844188465386154344573185523834501543756352222378885165072/607540116063314275062339246497289683154537514958866313949953163016739*y^18 - 24008858044422597823251723240966030676833016576256678353333226083838082016042/607540116063314275062339246497289683154537514958866313949953163016739*y^17 + 33329319840058250378570004106394512540644024680633063136400094906971446231211/607540116063314275062339246497289683154537514958866313949953163016739*y^16 + 16774003939105846399412599464606309369268761683341587989947939343482351988010/607540116063314275062339246497289683154537514958866313949953163016739*y^15 - 116665215159860894892727826400713340389897627177262660304521632366839019044232/607540116063314275062339246497289683154537514958866313949953163016739*y^14 + 190979676555400173935308357624009039879259419475996237544627238732543113903795/607540116063314275062339246497289683154537514958866313949953163016739*y^13 - 35736637590987261536274145365103753986274103531696237550915124695745845376971/607540116063314275062339246497289683154537514958866313949953163016739*y^12 - 3195940875206072981227900495770138479018700919149696056816013878815078213799/607540116063314275062339246497289683154537514958866313949953163016739*y^11 - 39830641677046227829370851400474184338888599308898482538502949107140793715334/607540116063314275062339246497289683154537514958866313949953163016739*y^10 - 68128751889817109324500057872062291461840127120960424104225410121595230289499/607540116063314275062339246497289683154537514958866313949953163016739*y^9 + 3355807003369752836780885486334314782549078370080505430409096337840953112677/607540116063314275062339246497289683154537514958866313949953163016739*y^8 + 30092595225467295764708416518449834688474290183049914660864899758982719267151/607540116063314275062339246497289683154537514958866313949953163016739*y^7 + 15436348969237158913049231010505362703167417669462757584403180613143779188876/607540116063314275062339246497289683154537514958866313949953163016739*y^6 + 3357494118895103525888693388540787264926398077932676684229644176365520594763/607540116063314275062339246497289683154537514958866313949953163016739*y^5 - 31602853875788866521799481976599899113898187979236585304666765301882187353/607540116063314275062339246497289683154537514958866313949953163016739*y^4 - 230878169800713643917709814355499421113051062624824199811920780646667191989/607540116063314275062339246497289683154537514958866313949953163016739*y^3 - 63987074225873198820771607298784019030440057890395759249264052670835787212/607540116063314275062339246497289683154537514958866313949953163016739*y^2 - 7943289258263227322336366619208140368235042063757707944360542208656033136/607540116063314275062339246497289683154537514958866313949953163016739*y - 392524409246784204072813348137114256880982127648834220087091310316205324/607540116063314275062339246497289683154537514958866313949953163016739 # A Gluing Matrix {{-1,0,0,-1,-2,0,0},{0,1,1,0,0,0,0},{0,1,0,0,-2,0,0},{-2,0,0,0,-2,1,0},{0,0,0,0,0,0,-1},{0,0,0,1,0,0,0},{-2,0,-2,-1,-4,0,1}} # B Gluing Matrix {{1,0,0,0,0,0,2},{0,1,0,0,0,0,0},{0,0,1,0,0,0,2},{0,0,0,2,0,1,2},{0,0,0,0,1,0,1},{0,0,0,0,0,2,0},{0,0,0,0,0,0,3}} # nu Gluing Vector {1, 1, 2, 3, 1, 2, 1} # f Combinatorial flattening {-2, 6, -5, 2, 2, 3, -3} # f' Combinatorial flattening {5, 0, 0, 0, -2, 0, 0} # 1 Loop Invariant 99012502184408080302506202685713618651690885209628259448650347744826341676/14818051611300348172252176743836333735476524755094300340242760073579*y^20 + 34963085613462656734409999702143013879115657319355273951345744708719855488216/607540116063314275062339246497289683154537514958866313949953163016739*y^19 - 218571851014505839579930697796070072418231979637348813236019312392661128663169/607540116063314275062339246497289683154537514958866313949953163016739*y^18 - 773532537512728524711423353580354164866549767022889436181349125569383482858705/607540116063314275062339246497289683154537514958866313949953163016739*y^17 + 2189069361125221914612959273276569848645570478628290481155982637706333814193469/1215080232126628550124678492994579366309075029917732627899906326033478*y^16 + 1037153102515500640950605867183922718747663853082093894783286053810461071876949/1215080232126628550124678492994579366309075029917732627899906326033478*y^15 - 7571094330259870560660254726066232618653127519171288166147501945099670916370617/1215080232126628550124678492994579366309075029917732627899906326033478*y^14 + 12531099427343605728396867681290159179995715876205281475841374914096047799896843/1215080232126628550124678492994579366309075029917732627899906326033478*y^13 - 1299968549778262967753200928424752699636089942681900147234760471525183078086747/607540116063314275062339246497289683154537514958866313949953163016739*y^12 - 92592469821237259343165318409290684778026551653568282672745774091772625246215/1215080232126628550124678492994579366309075029917732627899906326033478*y^11 - 2605548261483050181226751045214385297678084768510019040195061285362289222410849/1215080232126628550124678492994579366309075029917732627899906326033478*y^10 - 2178951089746975772199625522515606655535269860963409513880130249811489647186296/607540116063314275062339246497289683154537514958866313949953163016739*y^9 + 291647691742011896031271183828843159844737022910175434701883377857338484130813/1215080232126628550124678492994579366309075029917732627899906326033478*y^8 + 964210919788811062799771661759278231657480326210161292918668525200527336890992/607540116063314275062339246497289683154537514958866313949953163016739*y^7 + 966920191366023993040279649006568252980035948699789900556055438239065765147249/1215080232126628550124678492994579366309075029917732627899906326033478*y^6 + 205580811723662577719751572687470377934526788110502046528821664704935510517151/1215080232126628550124678492994579366309075029917732627899906326033478*y^5 - 1777585346296159136130794986660565695172138025323942260647806937620855713664/607540116063314275062339246497289683154537514958866313949953163016739*y^4 - 7282220558340980752650087083172071100020755807663118024893784672505008819985/607540116063314275062339246497289683154537514958866313949953163016739*y^3 - 1969797806661446318491504632913789975607981999702248045683849570590025185494/607540116063314275062339246497289683154537514958866313949953163016739*y^2 - 479562699665651183583674620596977057870193306301913932524950850822459983645/1215080232126628550124678492994579366309075029917732627899906326033478*y - 23196832775556745594249529669743675349502408250601715265079578252575046065/1215080232126628550124678492994579366309075029917732627899906326033478 # 2 Loop Invariant 1048991160423817765559913752076167807244651616907457096348817379070455615614375891103947803136026766864144735502251176423108173652775561492793/82361759156532777137629268779282848828942973731806703652992943770544026308799102124510766757120649479005320960467440586776859408357486468*y^20 + 1475669969240711321055452951363522441152978868913202172140467375115028228966425809840205464694462210201833815670139722412744907905023074733687541/13507328501671375450571200079802387207946647692016299399090842778369220314643052748419765748167786514556872637516660256231404942970627780752*y^19 - 4656506346340088799413594571091124145350508634667903308299971723176755892033127286204755410213383474921713056655904867161240772629621309362653817/6753664250835687725285600039901193603973323846008149699545421389184610157321526374209882874083893257278436318758330128115702471485313890376*y^18 - 2027916556025985623466653262308371457597480551040969339887705138946887586405228177307307023424692431001431083030089365012718005887487382931912517/844208031354460965660700004987649200496665480751018712443177673648076269665190796776235359260486657159804539844791266014462808935664236297*y^17 + 23726622731360778482698532914835794009276366102903508963459208052630287655780483360207584715103442411023134741679413610777852434587643280651001659/6753664250835687725285600039901193603973323846008149699545421389184610157321526374209882874083893257278436318758330128115702471485313890376*y^16 + 6707763948713158041680202565877903628597872413558162023821978762727373988993232159360220569257917220762784807053616399000239657481524738594299401/4502442833890458483523733359934129069315549230672099799696947592789740104881017582806588582722595504852290879172220085410468314323542593584*y^15 - 53591346890566414791978093518263531488718606521730906551485505534263120204845647971614938618399568765823115148293120159424132579339691587100595611/4502442833890458483523733359934129069315549230672099799696947592789740104881017582806588582722595504852290879172220085410468314323542593584*y^14 + 135592090203212855828721905720323470319542499329765228065759213390083181741872849275470021246090163484246183308045827606966651759092264112188482023/6753664250835687725285600039901193603973323846008149699545421389184610157321526374209882874083893257278436318758330128115702471485313890376*y^13 - 65608008389874132769023292946162416932536050095205258902046656461478697197909141118639708143943167315208403787885948115447887074770476638829391127/13507328501671375450571200079802387207946647692016299399090842778369220314643052748419765748167786514556872637516660256231404942970627780752*y^12 + 1162247251379139925864183483325212700077255686671913504327557637472303590946923160836577538049465898556529015750003609533976063681299332823462027/6753664250835687725285600039901193603973323846008149699545421389184610157321526374209882874083893257278436318758330128115702471485313890376*y^11 - 28076725647584525860875462516422130937354628852649419167515423545171561847004136786762223487142753111542666896724517099200539882449312949202792741/6753664250835687725285600039901193603973323846008149699545421389184610157321526374209882874083893257278436318758330128115702471485313890376*y^10 - 15029181334036123105246095198539524410788627402711787254554790650591661939439629881619492180625830967414127844505331970076146470052356511931026499/2251221416945229241761866679967064534657774615336049899848473796394870052440508791403294291361297752426145439586110042705234157161771296792*y^9 + 8912446479598826168861226640975974195257442698960801767129957332451661405074684809117674723447067980981769422742017023565936851511188785244048595/13507328501671375450571200079802387207946647692016299399090842778369220314643052748419765748167786514556872637516660256231404942970627780752*y^8 + 13350719545341562693079613810419943854493892014427935343700496803232549976168324547985773417642693327655644278765190980955897687878549155437862697/4502442833890458483523733359934129069315549230672099799696947592789740104881017582806588582722595504852290879172220085410468314323542593584*y^7 + 4814156311667508854044917423920310075748205027431610181302400187730023298339674303709159588798904237673417272367944421302044985901603619502446897/3376832125417843862642800019950596801986661923004074849772710694592305078660763187104941437041946628639218159379165064057851235742656945188*y^6 + 1302918143948346746800812336356043482894891277783282101426221339535140566624753579295594331706307780165423116184305995856301380908315296864877389/4502442833890458483523733359934129069315549230672099799696947592789740104881017582806588582722595504852290879172220085410468314323542593584*y^5 - 22399307402792951448677922913375939373183021666356346375396324266692403462367232763230770943541328569145471932411744244393440500007569818618357/2251221416945229241761866679967064534657774615336049899848473796394870052440508791403294291361297752426145439586110042705234157161771296792*y^4 - 294626887408686041832993517783229656488245362959711397189433978712752604077619171034663350457461604629265194528509927524404999329399292776043653/13507328501671375450571200079802387207946647692016299399090842778369220314643052748419765748167786514556872637516660256231404942970627780752*y^3 - 25315844486020119936316990019518155979618200479430654523900826439107267183880773132954343467616364798630474959193229986363972213882711443616005/4502442833890458483523733359934129069315549230672099799696947592789740104881017582806588582722595504852290879172220085410468314323542593584*y^2 - 2950074680339880020208688330822933045652038532321479422509113237670635771161564340159136934248645193243734933705821713524258127960089729719879/4502442833890458483523733359934129069315549230672099799696947592789740104881017582806588582722595504852290879172220085410468314323542593584*y - 126486417621565767035186839944639233422142116397498076046361055935446885536696261735315933502802505564681524764513278758399669778058501678231/4502442833890458483523733359934129069315549230672099799696947592789740104881017582806588582722595504852290879172220085410468314323542593584 # 3 Loop Invariant -24248579496624850321991756524293068640556330942419519314963435216319541108336744423267606874743596397595688110525953424963862761390386777127980960046353139263716105282925477141/4726840836294350336402014135167218450377578656919886553961650259179515386204157450176008661833107436869419469368207904372214932818805519275385974581913296144338816880658592*y^20 - 4270730045272851613814680361899351805974293689274793501379102752391775585211615935761103488145729927820085748711999970644222649974962845441668387844213642654155567154866414631279/96900237144034181896241289770927978232740362466857674356213830313180065417185227728608177567578702455823099122048262039630406122785513145145412478929222570958945746053501136*y^19 + 53705011056706077190006264576203212598382730026790250147508605559122782003762012544322640737662162457887195642247926552088967606382920543117940533307400083137222670249355379227195/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^18 + 188250361901859776955402194006803659366202799512494177926381801016673099130245285226096747470587887513365063518851202694461174638741994801213134053497311990632582605845764038845161/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^17 - 271732485170002174457197170277605519512318762558773305979091144495252725441195191523499721323716018532753020242216818592189176395314000879952301071286904404033075808557427280994865/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^16 - 120199340539909908616416304900088353686346112659017235480996534105458347949924512367598995687362345218282018706244650650250264852342853378455503193574864004272985989739035202142139/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^15 + 1855590415069358735490290378489956907972555465953092585631395907202176746621482405885302620636165110101104898564599390842847050461849857366644921614048303714891042376967912759110391/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544*y^14 - 3108861653503877693406166997893560435830158943691396066282890826519454658773102805954207089627571799146032979148163744525024261206794526427862912400085169269158104651276129687271701/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544*y^13 + 713896921684408823939685631605631052554799292862328940624619207897073525305477732899960542258414010246307191205661981665645714365854441534608678005011015593528748951738333493285785/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544*y^12 - 3394920161699795988173820935811924508571705295693626390276056556836425740157467001561914262798406737605053517944962291448718724778155632511602721250724055721491724126583930622935/96900237144034181896241289770927978232740362466857674356213830313180065417185227728608177567578702455823099122048262039630406122785513145145412478929222570958945746053501136*y^11 + 647919444220108557673981551114200047046368279308522736721802260210986590695803964805959560148492643466375842333920890211488526025783157298524851794424496129923098934546509008468671/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544*y^10 + 525530970015723983676209973162780275428309370901909481396131597920178554966415107978804515735485417010624783239562697729861808549272770572494629131982891091615187280163403316504285/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^9 - 44696362105063806843635740924898459901111854122946163327606180708785896575587508612664131547334080767709743445651791208002130564257213434455185038771897030970791539710756711720653/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^8 - 232657717924366107480999840900330563801595960954329745650932242420483797455947998141621894224144344867489804772465507878287974259462705662009330856523854704631862786366203755292959/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^7 - 228734703061758493443884375355241362008513797426517241945669743478187441099841460183941352848722398898384568425361291915088041900218480490454461231789190385912608794590902000137213/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544*y^6 - 23885405573311498382329178892765372283564019523189354153549755721170077546029846725225160299760156750992274481491787969868126867215097518177116658815820142768533466170519152229135/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^5 + 1133861050580655515559240209353541675162418910180510443697841050580789833506425860324805004025067575120516212446072638654033624178633196641176436028871718588034795833427736227429/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544*y^4 + 1731280856773159309615658703892114579740663333348306583956011614401785755715149087647645170313142939337127705406668037169703208331154914854289688108531223798938299656281133524461/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^3 + 460474519578181796840748765668492333590280999750029987791336232811022389041632023782297620932188635562217199339222749389663948847999073948249868521734659778699936334574490682581/193800474288068363792482579541855956465480724933715348712427660626360130834370455457216355135157404911646198244096524079260812245571026290290824957858445141917891492107002272*y^2 + 110985339492663284369737988659828192054409343282873839514480350276556579454973950388364505287018846218131804386163688167068636416152587599896637272844667568657810123272290829933/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544*y + 5326410144114624903376615288939578449699972889559514691522724750416537035049480631858647467945214244995912653172029142896487999735844910525120803915808501070372324538836771757/387600948576136727584965159083711912930961449867430697424855321252720261668740910914432710270314809823292396488193048158521624491142052580581649915716890283835782984214004544