# Manifold: Census Knot K8_215 # Number of Tetrahedra: 8 # Number Field x^18 - 17*x^17 + 68*x^16 + 112*x^15 - 150*x^14 - 1168*x^13 - 8387*x^12 + 4186*x^11 + 52710*x^10 + 12267*x^9 - 174159*x^8 - 336156*x^7 - 58113*x^6 + 415894*x^5 + 186350*x^4 - 194773*x^3 - 63053*x^2 + 35371*x + 961 # Approximate Field Generator -2.17538867220615 + 0.110964168737347*I # Shape Parameters 17107224106178157430736425540029860532934939916249321/28409204724837696980227644383282845187199165538214455664*y^17 - 130826889282585654732337560745946120869429907096715481/14204602362418848490113822191641422593599582769107227832*y^16 + 334289791744391993682072610653294786492122886087559243/14204602362418848490113822191641422593599582769107227832*y^15 + 1946980224667815313412865448764853769615944565508753533/14204602362418848490113822191641422593599582769107227832*y^14 + 33452019164544134966082094576080683288489157354805717/1775575295302356061264227773955177824199947846138403479*y^13 - 1449960882807123126364926704082632571335088519535904651/1775575295302356061264227773955177824199947846138403479*y^12 - 176491466375735826838609882822221522722513846491171279435/28409204724837696980227644383282845187199165538214455664*y^11 - 176191887534836256861645542347957114116654706001292624043/28409204724837696980227644383282845187199165538214455664*y^10 + 998519826332255336808990248142076105354121359485147514369/28409204724837696980227644383282845187199165538214455664*y^9 + 817678950045636808777109397563301900604879167041333119377/14204602362418848490113822191641422593599582769107227832*y^8 - 2484284271923766434894577545944205469406644990384334237209/28409204724837696980227644383282845187199165538214455664*y^7 - 10149617049138233995695142272938672744840854631489228022115/28409204724837696980227644383282845187199165538214455664*y^6 - 5461891179345155094379447363966556213446907211997071306739/14204602362418848490113822191641422593599582769107227832*y^5 + 727075626260737651609495727421692570860126308277716757103/7102301181209424245056911095820711296799791384553613916*y^4 + 5476263264384245709644528772561153702499793890115458264865/14204602362418848490113822191641422593599582769107227832*y^3 + 1503301967732795638435616476733592131822874266119949470209/28409204724837696980227644383282845187199165538214455664*y^2 - 1378459466476761115492590587692259096346609507308659942555/14204602362418848490113822191641422593599582769107227832*y - 102206476282128511901932104253565414826911366891555235751/28409204724837696980227644383282845187199165538214455664 251693233687534522928305288426425255799289593101629/979627749132334378628539461492511903006867777179808816*y^17 - 2206173022254529906159803038118035786302246544426061/489813874566167189314269730746255951503433888589904408*y^16 + 9801882625023214578496212945192218778711056881504903/489813874566167189314269730746255951503433888589904408*y^15 + 7612479408489233438633498560150771143635072622951425/489813874566167189314269730746255951503433888589904408*y^14 - 2167354337208811845941891638302444736966568420529017/61226734320770898664283716343281993937929236073738051*y^13 - 16596255520456836875011456620539264416700618525230407/61226734320770898664283716343281993937929236073738051*y^12 - 1987677032865761094000812717447272592946294520650557095/979627749132334378628539461492511903006867777179808816*y^11 + 1951238553646405050847852642047179688023452772061784297/979627749132334378628539461492511903006867777179808816*y^10 + 11047721522386802838875865845314405680347533691447747685/979627749132334378628539461492511903006867777179808816*y^9 - 902278765683342130889591317077893019314690929964905059/489813874566167189314269730746255951503433888589904408*y^8 - 36412432027767427194410543508357559516233428299932538381/979627749132334378628539461492511903006867777179808816*y^7 - 65379233152096329424400627008147982573281500362558283343/979627749132334378628539461492511903006867777179808816*y^6 - 298079122405650279624692282554877871253712634559479175/489813874566167189314269730746255951503433888589904408*y^5 + 16005074258308189053500838209523464987545872414672218551/244906937283083594657134865373127975751716944294952204*y^4 + 2452080631119881382653242226741195699367326411517982941/489813874566167189314269730746255951503433888589904408*y^3 - 19078768135067946357859011752609005556610090018857935019/979627749132334378628539461492511903006867777179808816*y^2 + 674997164282487018722873859868232797446949554589462001/489813874566167189314269730746255951503433888589904408*y + 990411275095356231151265932546520639636230176983356813/979627749132334378628539461492511903006867777179808816 17107224106178157430736425540029860532934939916249321/28409204724837696980227644383282845187199165538214455664*y^17 - 130826889282585654732337560745946120869429907096715481/14204602362418848490113822191641422593599582769107227832*y^16 + 334289791744391993682072610653294786492122886087559243/14204602362418848490113822191641422593599582769107227832*y^15 + 1946980224667815313412865448764853769615944565508753533/14204602362418848490113822191641422593599582769107227832*y^14 + 33452019164544134966082094576080683288489157354805717/1775575295302356061264227773955177824199947846138403479*y^13 - 1449960882807123126364926704082632571335088519535904651/1775575295302356061264227773955177824199947846138403479*y^12 - 176491466375735826838609882822221522722513846491171279435/28409204724837696980227644383282845187199165538214455664*y^11 - 176191887534836256861645542347957114116654706001292624043/28409204724837696980227644383282845187199165538214455664*y^10 + 998519826332255336808990248142076105354121359485147514369/28409204724837696980227644383282845187199165538214455664*y^9 + 817678950045636808777109397563301900604879167041333119377/14204602362418848490113822191641422593599582769107227832*y^8 - 2484284271923766434894577545944205469406644990384334237209/28409204724837696980227644383282845187199165538214455664*y^7 - 10149617049138233995695142272938672744840854631489228022115/28409204724837696980227644383282845187199165538214455664*y^6 - 5461891179345155094379447363966556213446907211997071306739/14204602362418848490113822191641422593599582769107227832*y^5 + 727075626260737651609495727421692570860126308277716757103/7102301181209424245056911095820711296799791384553613916*y^4 + 5476263264384245709644528772561153702499793890115458264865/14204602362418848490113822191641422593599582769107227832*y^3 + 1503301967732795638435616476733592131822874266119949470209/28409204724837696980227644383282845187199165538214455664*y^2 - 1378459466476761115492590587692259096346609507308659942555/14204602362418848490113822191641422593599582769107227832*y - 73797271557290814921704459870282569639712201353340780087/28409204724837696980227644383282845187199165538214455664 -23512494218162806970147209394333262781734638446566527489/71548092285629173677514008109567099348009594974104516685376*y^17 + 197670192332737398926718061725585496578294994674874485153/35774046142814586838757004054783549674004797487052258342688*y^16 - 755815956735401665639428394875912301070823716946776899443/35774046142814586838757004054783549674004797487052258342688*y^15 - 83140451797262573199021723529401587293202734615249626327/1882844533832346675724052844988607877579199867739592544352*y^14 + 127726377496598239872955979863473572650476750443574641869/2235877883925911677422312753423971854625299842940766146418*y^13 + 1793370055240924114316699862903423782559921678163474256747/4471755767851823354844625506847943709250599685881532292836*y^12 + 200382953617878536287965182628012795074815106877882755846163/71548092285629173677514008109567099348009594974104516685376*y^11 - 75038154905026792570693905407664352214570674580363694923517/71548092285629173677514008109567099348009594974104516685376*y^10 - 1356735250110639431305763279931038208554803868010077866559097/71548092285629173677514008109567099348009594974104516685376*y^9 - 199163980366490754480542082331104368014145855261202112398689/35774046142814586838757004054783549674004797487052258342688*y^8 + 4587396205734544433188516754458886444996600499738901074827313/71548092285629173677514008109567099348009594974104516685376*y^7 + 8462513913087733171326036840303562051070561665340443083150843/71548092285629173677514008109567099348009594974104516685376*y^6 + 493636290613440456772718237580947986595739483871139202406139/35774046142814586838757004054783549674004797487052258342688*y^5 - 3129057178572252146594992157366018771538612037816504702325979/17887023071407293419378502027391774837002398743526129171344*y^4 - 2781624022346920678013166074552193214557472330509900429717985/35774046142814586838757004054783549674004797487052258342688*y^3 + 229480883961214875726430186999096274047994013743801430102505/2308002976955779796048838971276358043484180483035629570496*y^2 + 1040409110960179091370028683909340981809795886186512368108291/35774046142814586838757004054783549674004797487052258342688*y - 48344541561757360379680134604512190452870204123192439667343/2308002976955779796048838971276358043484180483035629570496 -5958994949388679265920504815907458734628272321680585187/3295467748081172849706406748460810041715103202432876857024*y^17 + 53325496523805573695173150709289943164111808460674031379/1647733874040586424853203374230405020857551601216438428512*y^16 - 249190551908473392062557321464653541382293793859288162793/1647733874040586424853203374230405020857551601216438428512*y^15 - 131175970666994622063834118200810798470677430444718696271/1647733874040586424853203374230405020857551601216438428512*y^14 + 20093526026625717507169411693367753789160775209248832621/51491683563768325776662605444700156901798487538013700891*y^13 + 383435966536972716218808068154369500915575304057439355407/205966734255073303106650421778800627607193950152054803564*y^12 + 44322742040337336276135638677067147202971016557772602430521/3295467748081172849706406748460810041715103202432876857024*y^11 - 67636656433353096892384054852585420589032507716281933210839/3295467748081172849706406748460810041715103202432876857024*y^10 - 276158615727872104831140055461987090374964055366150666966315/3295467748081172849706406748460810041715103202432876857024*y^9 + 87150532023834686324652898464353354183305120144649768682205/1647733874040586424853203374230405020857551601216438428512*y^8 + 1004448656344515056897110588637915482422693748896603905799411/3295467748081172849706406748460810041715103202432876857024*y^7 + 1191061159948818986852491378445038942054516752020313420950577/3295467748081172849706406748460810041715103202432876857024*y^6 - 532595392031803717796547935930504863441898350822601184164591/1647733874040586424853203374230405020857551601216438428512*y^5 - 627767636554529938017218654730464844377023856671403410073169/823866937020293212426601687115202510428775800608219214256*y^4 + 188674412094462712731540585591835726540220477786488543722333/1647733874040586424853203374230405020857551601216438428512*y^3 + 1139789773672627242908022971303184631090587917854852583338309/3295467748081172849706406748460810041715103202432876857024*y^2 - 86794769156116922799068146104552370035845107281698878388743/1647733874040586424853203374230405020857551601216438428512*y - 2035078111644376236180860919156016831960889052296732459635/3295467748081172849706406748460810041715103202432876857024 -42025512212413666397531788949168425474132727947912243/30368460223102365737484723306267868993212901092574073296*y^17 + 173918468561232041703958028146486260347892452858181609/7592115055775591434371180826566967248303225273143518324*y^16 - 640978738092983657864364905027561988556602635033759119/7592115055775591434371180826566967248303225273143518324*y^15 - 347413122183378532462196267125477030460611629891044339/1898028763943897858592795206641741812075806318285879581*y^14 + 1261979997296432259431454777523134566407601369312886615/15184230111551182868742361653133934496606450546287036648*y^13 + 24613402037228812266851768548954934807265019645261577121/15184230111551182868742361653133934496606450546287036648*y^12 + 376441371237922330140474350952965497911729519607867689975/30368460223102365737484723306267868993212901092574073296*y^11 + 9789938549316325839413637371800431536628381731831818465/30368460223102365737484723306267868993212901092574073296*y^10 - 2077907491477825142591672565055856863896145328270945106781/30368460223102365737484723306267868993212901092574073296*y^9 - 783192103671667999691000354718562307250982084207018461107/15184230111551182868742361653133934496606450546287036648*y^8 + 5906571003363807452672951970095631982958079995589939437487/30368460223102365737484723306267868993212901092574073296*y^7 + 16828824249647753878673634676514900825309824069672230898551/30368460223102365737484723306267868993212901092574073296*y^6 + 6131279363789440465049439549493293161569849505546400178121/15184230111551182868742361653133934496606450546287036648*y^5 - 941103313311915085176664705943259507749996506821513660927/3796057527887795717185590413283483624151612636571759162*y^4 - 5329055445064987249389398321082829418730407696463474568397/15184230111551182868742361653133934496606450546287036648*y^3 - 5322998411354441593658430032391863058102936790609334629/979627749132334378628539461492511903006867777179808816*y^2 + 119146194339577206319684713285722087716042125065755871707/1898028763943897858592795206641741812075806318285879581*y + 2625010540761628111538160964513806426712429582981729269/979627749132334378628539461492511903006867777179808816 -30393845031359259099298761457401579445947316945111470091/66932086331717614085416330167014383261041234008033257544384*y^17 + 250911045122105955329015834592332262907267442158123736687/33466043165858807042708165083507191630520617004016628772192*y^16 - 913605960700677777717192526728571474319545284266236886877/33466043165858807042708165083507191630520617004016628772192*y^15 - 110275995982742691000924484474494705141592904002102854961/1761370692939937212774113951763536401606348263369296251168*y^14 + 249010938743524456993020924124288425803884781763492296429/8366510791464701760677041270876797907630154251004157193048*y^13 + 4546784076797055405234309979078222970260576620236528996729/8366510791464701760677041270876797907630154251004157193048*y^12 + 273415584522018093298775469312136638373590776145094722938841/66932086331717614085416330167014383261041234008033257544384*y^11 + 12507520472925672604836687543328895096210363547239597042881/66932086331717614085416330167014383261041234008033257544384*y^10 - 1550871554049039613431907370255298242399796966629058111428523/66932086331717614085416330167014383261041234008033257544384*y^9 - 597996843336135154034299753287934467844076646897518929453227/33466043165858807042708165083507191630520617004016628772192*y^8 + 4488754945798797179186149369769112952366281975523987622463211/66932086331717614085416330167014383261041234008033257544384*y^7 + 12532743961576798338672322957941705249912850941648861034536881/66932086331717614085416330167014383261041234008033257544384*y^6 + 4316408584688549782665767317455430027693024176042951103929865/33466043165858807042708165083507191630520617004016628772192*y^5 - 1786156855862498953146385960767702287245212881883764303732037/16733021582929403521354082541753595815260308502008314386096*y^4 - 4713975003572413574271021570416431660252924417660127597376387/33466043165858807042708165083507191630520617004016628772192*y^3 + 11770673814761772353586195243084725439572763246686100994883/2159099559087664970497300973129496234227136580904298630464*y^2 + 1148467048599981621352909561528215152827851777200699354418917/33466043165858807042708165083507191630520617004016628772192*y + 1333591469442169282297913765918366376966699961862979403539/2159099559087664970497300973129496234227136580904298630464 3798362950839820722011662720250933995715994687336333/121473840892409462949938893225071475972851604370296293184*y^17 - 19057207350295309857208967095363929485808865237113053/60736920446204731474969446612535737986425802185148146592*y^16 - 99433407897617094586639862858295414610931836990579801/60736920446204731474969446612535737986425802185148146592*y^15 + 1186571567058311004048396128614029899893990606331736897/60736920446204731474969446612535737986425802185148146592*y^14 + 23171430288080362884208475282074886646147821654353791/1898028763943897858592795206641741812075806318285879581*y^13 - 461957246178237923451343730394196361911029534391168169/7592115055775591434371180826566967248303225273143518324*y^12 - 60387708445287752964207163000734358670662969529249491607/121473840892409462949938893225071475972851604370296293184*y^11 - 200643575706456312023888788479577623718768665894835547495/121473840892409462949938893225071475972851604370296293184*y^10 + 348776550810379156757462369999562521658483548257131145733/121473840892409462949938893225071475972851604370296293184*y^9 + 613914262375564585024106948047970008082808401762778950061/60736920446204731474969446612535737986425802185148146592*y^8 - 533128358321177601334405736017458255885524578306921073405/121473840892409462949938893225071475972851604370296293184*y^7 - 4977912624644010766077906642845790595360057224834951557599/121473840892409462949938893225071475972851604370296293184*y^6 - 4032474859138823175033100379343428029602794615818592502239/60736920446204731474969446612535737986425802185148146592*y^5 - 188957643118216003696754424649865663939916150540720667185/30368460223102365737484723306267868993212901092574073296*y^4 + 3156163609845767623709187923724988724126901947335396434605/60736920446204731474969446612535737986425802185148146592*y^3 + 41130367711795059573022313254380069214621574410268165739/3918510996529337514514157845970047612027471108719235264*y^2 - 600594278712556673546507872505432874923187417635615898519/60736920446204731474969446612535737986425802185148146592*y + 694049968972869596240878380788415232273921648304201059/3918510996529337514514157845970047612027471108719235264 # A Gluing Matrix {{8,4,-2,-2,-2,-4,2,-2},{4,2,-1,0,-1,-2,0,0},{-2,-1,1,0,0,0,0,0},{-2,0,0,0,1,1,0,0},{-2,-1,0,1,1,1,-1,0},{-4,-2,0,1,1,3,0,0},{2,0,0,0,-1,0,0,2},{-2,0,0,0,0,0,2,-3}} # 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,0,0},{0,0,0,1,0,0,0,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,1}} # nu Gluing Vector {4, 2, -1, 0, -1, -1, 2, -1} # f Combinatorial flattening {1, 5, 6, 3, -2, 4, -1, -1} # f' Combinatorial flattening {6, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 1844357675404297613647219406060611540376378201563647623/242947681784818925899877786450142951945703208740592586368*y^17 - 14224193222279796830883092465040934711040075202419694935/121473840892409462949938893225071475972851604370296293184*y^16 + 38227777051657977591530775304695829015091922556435045493/121473840892409462949938893225071475972851604370296293184*y^15 + 199159036924339723304730394028262970570644733382378350787/121473840892409462949938893225071475972851604370296293184*y^14 + 402768005302650014582459102963556654616867536290175358/1898028763943897858592795206641741812075806318285879581*y^13 - 151967147665429332172676802078984248994188025542308665575/15184230111551182868742361653133934496606450546287036648*y^12 - 18774560761681128239942620421057407274909921828822918144997/242947681784818925899877786450142951945703208740592586368*y^11 - 17336609402421953379454130485636254566416761715529316868757/242947681784818925899877786450142951945703208740592586368*y^10 + 103976362172992565997548729945573487976106599842238171035887/242947681784818925899877786450142951945703208740592586368*y^9 + 82183721541060582014763335703575952659358477927178580687079/121473840892409462949938893225071475972851604370296293184*y^8 - 256140250135432693821147039579741966224111386839801176849111/242947681784818925899877786450142951945703208740592586368*y^7 - 1045886453149383058268553620144252676355212008547928142908221/242947681784818925899877786450142951945703208740592586368*y^6 - 569870126390536072436475181897908964192454347692747608292893/121473840892409462949938893225071475972851604370296293184*y^5 + 55057079367673102734900999638396912029365764689494385374845/60736920446204731474969446612535737986425802185148146592*y^4 + 507246434200814358069194534786726668396742715572637343246439/121473840892409462949938893225071475972851604370296293184*y^3 + 5330464134477456330485488780885743982881437134855851010081/7837021993058675029028315691940095224054942217438470528*y^2 - 107694746654457499139646685538213644187548845052268559031781/121473840892409462949938893225071475972851604370296293184*y + 166274729533842505201510784126739497340350621848160149001/7837021993058675029028315691940095224054942217438470528 # 2 Loop Invariant -880231502010282575232220569323170834090025215205933283799062398450234145077847752276001446877655903/18765953339324913406064954015004558628881709614919529374525014063353766105974365521357504606221206930624*y^17 + 11960629908061338102616078517690617224441010123806659397968979666741437200238749164813474236586356767/14074465004493685054548715511253418971661282211189647030893760547515324579480774141018128454665905197968*y^16 - 29120317906486528416920632750586414541606739089024669671111550992625899546144839335257474303275546037/7037232502246842527274357755626709485830641105594823515446880273757662289740387070509064227332952598984*y^15 - 1540210106853502577248019846057645556239610501230065601476309942820495439544555829081585927268744081/2345744167415614175758119251875569828610213701864941171815626757919220763246795690169688075777650866328*y^14 + 74881283290770074625374587163086454307620789108458769021269709158830740546280295158250211792380918909/9382976669662456703032477007502279314440854807459764687262507031676883052987182760678752303110603465312*y^13 + 1278351863122931035805048696917157948799258794269021456828040119703365885084163495236773048295818530003/28148930008987370109097431022506837943322564422379294061787521095030649158961548282036256909331810395936*y^12 + 19250736046206561979828827123228458139320202082210561838791643358941808378480947779889889206750493064837/56297860017974740218194862045013675886645128844758588123575042190061298317923096564072513818663620791872*y^11 - 10860093318555729178402543542858943212079502748280389625664507672431499892443163489079519229205999026299/18765953339324913406064954015004558628881709614919529374525014063353766105974365521357504606221206930624*y^10 - 102884946439929399509530952401741735619822516938857910947937947453869850760393423620205954601929111890031/56297860017974740218194862045013675886645128844758588123575042190061298317923096564072513818663620791872*y^9 + 14382751649437389581156483524428485442018556544927951946013416479401545473801932964754335140017828821303/9382976669662456703032477007502279314440854807459764687262507031676883052987182760678752303110603465312*y^8 + 364131356827256726754746265116655210028289847994257743754936099449661440280779573286974291190956157093205/56297860017974740218194862045013675886645128844758588123575042190061298317923096564072513818663620791872*y^7 + 154181178219377481368050459561504121039117884844701075413942163863780532345253909945207285375989526336323/18765953339324913406064954015004558628881709614919529374525014063353766105974365521357504606221206930624*y^6 - 186083956595923310833552636941556811455434526010488757873608999388978078363525246125122596115472314701737/28148930008987370109097431022506837943322564422379294061787521095030649158961548282036256909331810395936*y^5 - 26896097955512052781592577565291721209640239457134171960650473284220719502836105230935084970166079503591/2345744167415614175758119251875569828610213701864941171815626757919220763246795690169688075777650866328*y^4 + 165183700637512275961167027059484589696888986926734861365736241987632859458174535968225655054700955104269/28148930008987370109097431022506837943322564422379294061787521095030649158961548282036256909331810395936*y^3 + 71103981527668702674402926267706050516678203629105283732565707431037476086694123172575520214744461840989/18765953339324913406064954015004558628881709614919529374525014063353766105974365521357504606221206930624*y^2 - 28071758297616990650215867001371867561818864550883648527406089434683421537776083088859974801662476670399/14074465004493685054548715511253418971661282211189647030893760547515324579480774141018128454665905197968*y - 15501800410019327937470635664186967792442701652694156954738112304512895129263855481446686782949484985393/18765953339324913406064954015004558628881709614919529374525014063353766105974365521357504606221206930624 # 3 Loop Invariant 50275048913352765335149298058821660067890367308185201543834227118581652251107069057139761452911422765973297655507380448555057/1273084138080546736593629697409445748120618513724142617108019358759497357978621887095672042055779189983843074267248388727473925824*y^17 - 460100972178789843739333691144869073691162080385622002659084803380115932239587208929168945340204563985395756847759594223349847/636542069040273368296814848704722874060309256862071308554009679379748678989310943547836021027889594991921537133624194363736962912*y^16 + 2311567770156709922447813434015796833197545462536524533496101564965644873795486295658886440496209614678273208011103578822318613/636542069040273368296814848704722874060309256862071308554009679379748678989310943547836021027889594991921537133624194363736962912*y^15 - 218510113521100170539994486663783382538947122739577584601518069244085383384077126548060794863119315490035166073714972637540397/636542069040273368296814848704722874060309256862071308554009679379748678989310943547836021027889594991921537133624194363736962912*y^14 - 1866307419173727441404743883551559268409011728180851719769456658940369409693722985372605661464921128077871430636600763472749123/318271034520136684148407424352361437030154628431035654277004839689874339494655471773918010513944797495960768566812097181868481456*y^13 - 21926745027814844864566661940218542783749245087161016087196859522807350173013733038641210875359933470926658137839518726175251247/636542069040273368296814848704722874060309256862071308554009679379748678989310943547836021027889594991921537133624194363736962912*y^12 - 91832584586768416288383498384429068268703654286208593634043026960226532328067949404879492275555427900253952950344559064418510813/318271034520136684148407424352361437030154628431035654277004839689874339494655471773918010513944797495960768566812097181868481456*y^11 + 334716549879011391715550121782024206013128678797441356628404869104516898783170500883249259569627340814747389625844805250223351985/636542069040273368296814848704722874060309256862071308554009679379748678989310943547836021027889594991921537133624194363736962912*y^10 + 107139225461619311070206680777384750735323149841034393329341433341902683220295751392842981455793295188183964018003653319735891547/79567758630034171037101856088090359257538657107758913569251209922468584873663867943479502628486199373990192141703024295467120364*y^9 - 1880747889788583072798231021448348413543290351808535408211019347569620361413608216732333050926405040047571744818654933922127066743/1273084138080546736593629697409445748120618513724142617108019358759497357978621887095672042055779189983843074267248388727473925824*y^8 - 2613097812131954279443038082830591502681030426451479227700010203177986162923715581449374950904964809191661002528818569250244021153/636542069040273368296814848704722874060309256862071308554009679379748678989310943547836021027889594991921537133624194363736962912*y^7 - 541483885641697005756020323980547685689596587890944454863359739060989940905633868009805712510852701629256335834805093109239641901/79567758630034171037101856088090359257538657107758913569251209922468584873663867943479502628486199373990192141703024295467120364*y^6 + 96721575275067971471769440623038789406412548743082477137933625266140316000325238659903480593485534742616679838692013423525091677/39783879315017085518550928044045179628769328553879456784625604961234292436831933971739751314243099686995096070851512147733560182*y^5 + 12372909107417130788686984667831732553516254197172060147473518371236540298891132049172655126050072610018047236690637933949688667023/1273084138080546736593629697409445748120618513724142617108019358759497357978621887095672042055779189983843074267248388727473925824*y^4 - 3080755221954567750665951966346914072043439308307440455346974760121851683966860652218078383192836187324871244799753089199730888481/1273084138080546736593629697409445748120618513724142617108019358759497357978621887095672042055779189983843074267248388727473925824*y^3 - 131215191936133039924768524421859756872058398064282963719690656296810269369636662975674078627509571602733723318660854051579956519/41067230260662797954633216045465991874858661733036858616387721250306366386407157648247485227605780322059454008620915765402384704*y^2 + 352096292969866641914341574872057616131371067701725013746620630242840568195481798387425022272250382527401974274042903590165385365/318271034520136684148407424352361437030154628431035654277004839689874339494655471773918010513944797495960768566812097181868481456*y + 3217766031193153157343894084419085192721353778684226769462008904025630461008596203501283476463521114343999334563889132517033487/41067230260662797954633216045465991874858661733036858616387721250306366386407157648247485227605780322059454008620915765402384704 # 4 Loop Invariant 57653620059615830899655787601089650534069285110870834734789367623262855128415027067092475654058441337543982721049281951314487696916187056757547219808819117879437510686656579201/146324790534451766415700934911598469369208521545545724379712652432601952952795913266929870482165105859833889088896875772988608579206199611458183081563177023591379060204813839254016*y^17 - 1215496044130523361175317471479581508423634014353055642044335907145647586219008993173272440188504110902078206779768725692903474038671423555405537135793565872615061316511740483871/182905988168064708019626168639498086711510651931932155474640815540752441190994891583662338102706382324792361361121094716235760724007749514322728851953971279489223825256017299067520*y^16 + 1509030278701815907775701161322724020689956721426155514453777140889601745622803073677340083606721488273611293839792266929990513883559423751931100219416690527916208585673271994429/60968662722688236006542056213166028903836883977310718491546938513584147063664963861220779367568794108264120453707031572078586908002583171440909617317990426496407941752005766355840*y^15 + 75578733269453626471978634175852573902828914692076505466953527364009843868667931413054641806938556982266888899655161862014262184136885825013046493138465016108645128928100438436901/1097435929008388248117757011836988520269063911591592932847844893244514647145969349501974028616238293948754168166726568297414564344046497085936373111723827676935342951536103794405120*y^14 - 699841909615865583364169138095472644557800469968760816327976837960476704405927462328635417394132755071947887626224857798210158109107968935371613825600965821819239125445452052843753/4389743716033552992471028047347954081076255646366371731391379572978058588583877398007896114464953175795016672666906273189658257376185988343745492446895310707741371806144415177620480*y^13 - 2153043801622189912068313736429015749932625993936129917285212494211595195528578288242369624848952902222939864223343081806351962799416381927777630286644526228988233846221740878417267/4389743716033552992471028047347954081076255646366371731391379572978058588583877398007896114464953175795016672666906273189658257376185988343745492446895310707741371806144415177620480*y^12 - 3191425008240153398090251952237039465158182416533660008982968803429299053770964631313908958055552232261525594484347354802811553297446232673610476377553674434868985966009985392275733/1097435929008388248117757011836988520269063911591592932847844893244514647145969349501974028616238293948754168166726568297414564344046497085936373111723827676935342951536103794405120*y^11 + 1672972890835782371503922148906706691346067612361701625441595388845484750985371451645597533845994596709851689236063231650810942664528206980089981368237399586270938869911957171523005/877948743206710598494205609469590816215251129273274346278275914595611717716775479601579222892990635159003334533381254637931651475237197668749098489379062141548274361228883035524096*y^10 + 41643157957202612921931996805625274257171329129734917416161480267783642166706972369529330225705554195325654907780476857103436244936780733547109413624641646984337442775990486667528749/1463247905344517664157009349115984693692085215455457243797126524326019529527959132669298704821651058598338890888968757729886085792061996114581830815631770235913790602048138392540160*y^9 - 10478727427444915870790977554048341018713446440842982926872116727194191747619261556254594325458916270236667421201911286360031899297067160872756995541511483078833847396701258992642313/1097435929008388248117757011836988520269063911591592932847844893244514647145969349501974028616238293948754168166726568297414564344046497085936373111723827676935342951536103794405120*y^8 - 13219880666623856666305812037909880267911224228202244458207237163019953893060965780169128942465403423193488921822836929256791223515741694499207154267403750094874738637649510441332091/109743592900838824811775701183698852026906391159159293284784489324451464714596934950197402861623829394875416816672656829741456434404649708593637311172382767693534295153610379440512*y^7 - 33511461501609770516078643204176111069350778501879333866616404233664204544905410428585082793387532423643671891749464619970014554052122230227696141340220715398605926134931836618370103/877948743206710598494205609469590816215251129273274346278275914595611717716775479601579222892990635159003334533381254637931651475237197668749098489379062141548274361228883035524096*y^6 + 564039400245872061493363590676681990749512387658099828372469573713235036709857305396988014215750420684016071082285344279182754352925101304434921655028184098117706602473363449628183273/4389743716033552992471028047347954081076255646366371731391379572978058588583877398007896114464953175795016672666906273189658257376185988343745492446895310707741371806144415177620480*y^5 + 2828466473640063123998209025399048832114758160120262326306978767765055428670340383880224269137980513097745139605224374768339578170234424074289239012301667569728289169666586266510069/60968662722688236006542056213166028903836883977310718491546938513584147063664963861220779367568794108264120453707031572078586908002583171440909617317990426496407941752005766355840*y^4 - 23641827174809751677001885741740715170084794484544063483938283410391971554555322336556463018203219463074838394260583569259402434993835893790519482389606349163327921824907859175602001/438974371603355299247102804734795408107625564636637173139137957297805858858387739800789611446495317579501667266690627318965825737618598834374549244689531070774137180614441517762048*y^3 - 1859022160624014498823735964183816385478567287054694744413917156897226491644656420932490419231189332233653415893305786341453182873535586945665216987770122176580825762436619817433723/141604636001082354595839614430579163905685666011818442948109018483163180276899270903480519821450102445000537827964718489988976044393096398185338466028880990572302316327239199278080*y^2 + 36262604769147372445036635181653074072003964810141128482701553066076509610538636719461799885925038419023418673657786621969078461264178715586701554115283268770149510007396742407208239/4389743716033552992471028047347954081076255646366371731391379572978058588583877398007896114464953175795016672666906273189658257376185988343745492446895310707741371806144415177620480*y + 1972714853383094685311568445063720753777197103873740294888278142895955249881409753864109251859667261784377454030847980680996839790487268821728015673982334360442595354404373029207/8850289750067647162239975901911197744105354125738652684256813655197698767306204431467532488840631402812533614247794905624311002774568524886583654126805061910768894770452449954880