# Manifold: Census Knot K8_214 # Number of Tetrahedra: 8 # Number Field x^23 - 3*x^22 - 29*x^21 + 50*x^20 + 230*x^19 + 35*x^18 + 757*x^17 + 1077*x^16 - 500*x^15 - 392*x^14 - 3284*x^13 - 1002*x^12 + 2780*x^11 + 2181*x^10 + 2205*x^9 - 494*x^8 - 4065*x^7 - 1872*x^6 + 1605*x^5 + 1319*x^4 + 4*x^3 - 198*x^2 - 43*x - 1 # Approximate Field Generator -0.351442177249386 - 1.23505224617543*I # Shape Parameters -y + 1 -2258677966001225883486767383800256193060832/6075101448916318986054749140728573958734473*y^22 + 8265179091805584968244567723961341589011219/6075101448916318986054749140728573958734473*y^21 + 59832659976151726350748705371717703250785284/6075101448916318986054749140728573958734473*y^20 - 7990470695707765007745066648760091986033008/319742181521911525581828902143609155722867*y^19 - 412850314298927368375265150781049775134311056/6075101448916318986054749140728573958734473*y^18 + 185190889534595936788861592092494736685549709/6075101448916318986054749140728573958734473*y^17 - 1883826495032965177707534537228822305931314353/6075101448916318986054749140728573958734473*y^16 - 1223077917472423617849279145945737099339066336/6075101448916318986054749140728573958734473*y^15 + 1737624766634473343821001410390333786993314743/6075101448916318986054749140728573958734473*y^14 - 598552230197117411012105294797384952546660223/6075101448916318986054749140728573958734473*y^13 + 7709362103030104548101906311521950686268321976/6075101448916318986054749140728573958734473*y^12 - 2903672390346285232757625816865449118395966347/6075101448916318986054749140728573958734473*y^11 - 3734132012227851180875494932892267438400750364/6075101448916318986054749140728573958734473*y^10 - 1993546473812434215135590463376318008841919264/6075101448916318986054749140728573958734473*y^9 - 3878292808673327546699933309674955900290579127/6075101448916318986054749140728573958734473*y^8 + 3314040814445296922808365470139013500963989099/6075101448916318986054749140728573958734473*y^7 + 6298609195929587553348136670336233690644906978/6075101448916318986054749140728573958734473*y^6 - 250868315601968721181825819969717382585714376/6075101448916318986054749140728573958734473*y^5 - 2956776544706752440492161597014544728104200916/6075101448916318986054749140728573958734473*y^4 - 551956025520453105100623698812323149688078961/6075101448916318986054749140728573958734473*y^3 + 373310151107098875141443553064630400850763913/6075101448916318986054749140728573958734473*y^2 + 112993911740535838298760098384936435798729454/6075101448916318986054749140728573958734473*y + 14804778597884989859701190791579745918934819/6075101448916318986054749140728573958734473 72350885347490820622708188169753219833077163/6075101448916318986054749140728573958734473*y^22 - 268540148613289867800416140147763672216447755/6075101448916318986054749140728573958734473*y^21 - 1913483061699564287351409381898870337825383511/6075101448916318986054749140728573958734473*y^20 + 263003517622518903717895927029264946752649350/319742181521911525581828902143609155722867*y^19 + 13270874046729283253347214345218975806502967225/6075101448916318986054749140728573958734473*y^18 - 7181327914093299758997141112450378257835254281/6075101448916318986054749140728573958734473*y^17 + 58449654662880761403275048081813008470576236794/6075101448916318986054749140728573958734473*y^16 + 35637210740603617748271080281393536762213327874/6075101448916318986054749140728573958734473*y^15 - 67332612503874279036632917400175371547868253893/6075101448916318986054749140728573958734473*y^14 + 10998361213404027919344286056815797805639120735/6075101448916318986054749140728573958734473*y^13 - 247321240847757479916955079866815377840089223803/6075101448916318986054749140728573958734473*y^12 + 100885078870434610327648856045370651484090664405/6075101448916318986054749140728573958734473*y^11 + 148797234581134248420803359196145722530561816464/6075101448916318986054749140728573958734473*y^10 + 61161404562345377042103773813825721770939064164/6075101448916318986054749140728573958734473*y^9 + 111041261292108668503321778456012509372095985882/6075101448916318986054749140728573958734473*y^8 - 124804940745839913095811562015699849439832210684/6075101448916318986054749140728573958734473*y^7 - 224393527415225048323408091881752460457399030013/6075101448916318986054749140728573958734473*y^6 + 17649980657180343486570438274655724716636048994/6075101448916318986054749140728573958734473*y^5 + 117610868012947957066777650857911013059230883830/6075101448916318986054749140728573958734473*y^4 + 23250593766294209979351272362422672427633009496/6075101448916318986054749140728573958734473*y^3 - 16209104538183729067469778942617883696376026951/6075101448916318986054749140728573958734473*y^2 - 4908356688100831562388219190895515861131787567/6075101448916318986054749140728573958734473*y - 112105843109254520577797645153276420276541400/6075101448916318986054749140728573958734473 4597723978227214710255324156048349885135691/319742181521911525581828902143609155722867*y^22 - 16916733377702613280111460957310425218101414/319742181521911525581828902143609155722867*y^21 - 121972333575397890373620946983112407497486325/319742181521911525581828902143609155722867*y^20 + 16479803986196662393649148086793852022914067/16828535869574290820096258007558376616993*y^19 + 848557828980333519687224696266492202890543199/319742181521911525581828902143609155722867*y^18 - 421105793880092460919614655863167554915076968/319742181521911525581828902143609155722867*y^17 + 3737416049010054479626274653192302571872798809/319742181521911525581828902143609155722867*y^16 + 2398691655523082721765509557963773203133918910/319742181521911525581828902143609155722867*y^15 - 4047215787913632029540004307465143437242408366/319742181521911525581828902143609155722867*y^14 + 773464655417140827443086480537870103972449933/319742181521911525581828902143609155722867*y^13 - 15663297857990054717610164280022715565600209264/319742181521911525581828902143609155722867*y^12 + 5979863295519657210181437522106089349330350726/319742181521911525581828902143609155722867*y^11 + 9118293162798094449640969879269963095591335355/319742181521911525581828902143609155722867*y^10 + 4017667180449989201714246654545368635785072699/319742181521911525581828902143609155722867*y^9 + 7312417558849824856461238694854654321773684942/319742181521911525581828902143609155722867*y^8 - 7445613787938119051455364123207089028611883834/319742181521911525581828902143609155722867*y^7 - 14020805135057673362382014479511395441086179285/319742181521911525581828902143609155722867*y^6 + 784686399987865209060135959434613139861069924/319742181521911525581828902143609155722867*y^5 + 7130197968537210572297352507795265838375433799/319742181521911525581828902143609155722867*y^4 + 1454705435363433530585535184411618798380242819/319742181521911525581828902143609155722867*y^3 - 967192640287775510131608061678942085009804290/319742181521911525581828902143609155722867*y^2 - 295742305787168873929121978177692550930581801/319742181521911525581828902143609155722867*y - 7127820357784656911604340287633881914942658/319742181521911525581828902143609155722867 -3185970966121315473081817486949851738569123/319742181521911525581828902143609155722867*y^22 + 11668623344402179353722967198736868719593768/319742181521911525581828902143609155722867*y^21 + 84743150894350804813728683236633841162497781/319742181521911525581828902143609155722867*y^20 - 11350634703627081393792565872392807628154467/16828535869574290820096258007558376616993*y^19 - 592243878810243406955119827577913709117868717/319742181521911525581828902143609155722867*y^18 + 284165163448799936919041543486431096606766598/319742181521911525581828902143609155722867*y^17 - 2581935793539441159304493573552180282595572351/319742181521911525581828902143609155722867*y^16 - 1711581299884847843858080278424479214674529103/319742181521911525581828902143609155722867*y^15 + 2799723758077432742137343885819645473572531798/319742181521911525581828902143609155722867*y^14 - 496086465243224478162144605296838559943611009/319742181521911525581828902143609155722867*y^13 + 10817531143440740543372795140264056349402161139/319742181521911525581828902143609155722867*y^12 - 3941501585499590125841841097150036801241001679/319742181521911525581828902143609155722867*y^11 - 6488574924341693655811182833981543307955949027/319742181521911525581828902143609155722867*y^10 - 2774685506340707937698530239869843283561446530/319742181521911525581828902143609155722867*y^9 - 5123724794730357226493323458943170332113601231/319742181521911525581828902143609155722867*y^8 + 5095487220531813077241142940267848304006692306/319742181521911525581828902143609155722867*y^7 + 9818709928128526686712511390761735944194979327/319742181521911525581828902143609155722867*y^6 - 452011510703145155708622764799789828751743344/319742181521911525581828902143609155722867*y^5 - 4990397921931093770089441708093708035467327126/319742181521911525581828902143609155722867*y^4 - 1045757078876482133443179871346408795810107338/319742181521911525581828902143609155722867*y^3 + 677516048186582331084014530062978014749049692/319742181521911525581828902143609155722867*y^2 + 209183189984427867518790099853710827017613371/319742181521911525581828902143609155722867*y + 5204024498972040116915386767580007226299058/319742181521911525581828902143609155722867 189824584699696803772290422500932432012390/319742181521911525581828902143609155722867*y^22 - 693059380489452647945485811463175655018059/319742181521911525581828902143609155722867*y^21 - 5050725232009835312904093707178457706302189/319742181521911525581828902143609155722867*y^20 + 672356424911544278694621473929284389269283/16828535869574290820096258007558376616993*y^19 + 35246605290767450281529322871232539532219993/319742181521911525581828902143609155722867*y^18 - 16281099007977583757984678355216994659040783/319742181521911525581828902143609155722867*y^17 + 155106183067215550320729337652840180801626017/319742181521911525581828902143609155722867*y^16 + 104570466586415981380512338363959930409814738/319742181521911525581828902143609155722867*y^15 - 159921133354773220423668576984843972118179909/319742181521911525581828902143609155722867*y^14 + 36821982672084724609464055232011480153252505/319742181521911525581828902143609155722867*y^13 - 641726582944837265066925640835433891077689887/319742181521911525581828902143609155722867*y^12 + 229811871851516885278550525251941227953930831/319742181521911525581828902143609155722867*y^11 + 370321200724990548034640323347410164355538525/319742181521911525581828902143609155722867*y^10 + 158067290592195373054572815048860411414681326/319742181521911525581828902143609155722867*y^9 + 312626804018281800288941370451787760229248812/319742181521911525581828902143609155722867*y^8 - 289643392210249567320958824478537617867668757/319742181521911525581828902143609155722867*y^7 - 568177525294253964528136634027621063783495414/319742181521911525581828902143609155722867*y^6 + 28051131210655316664807839544936082950402411/319742181521911525581828902143609155722867*y^5 + 284122068089972842608338721945288238496692859/319742181521911525581828902143609155722867*y^4 + 52142915432103261547507755009022566335974670/319742181521911525581828902143609155722867*y^3 - 40055379493904149666647573732153846744304870/319742181521911525581828902143609155722867*y^2 - 10384558333847748680745179402525643732653662/319742181521911525581828902143609155722867*y + 389819067384650398426840624276773441490111/319742181521911525581828902143609155722867 -13389477810887021871885070073223400660076047/7354070175003965088382064749303010581625941*y^22 + 92561997198658249345894935091765120918333295/14708140350007930176764129498606021163251882*y^21 + 367076001601112410272598461167262682171334073/7354070175003965088382064749303010581625941*y^20 - 44038161536007992522073646919874208384313738/387056325000208688862213934173842662190839*y^19 - 2695126165946532297238589798854431755555100563/7354070175003965088382064749303010581625941*y^18 + 32853943984377227676506449152649292962378602/319742181521911525581828902143609155722867*y^17 - 10499154845791624702613308508493710694792265261/7354070175003965088382064749303010581625941*y^16 - 9618472584985765351425119884680685292788401960/7354070175003965088382064749303010581625941*y^15 + 479167507476435329587498385126911846043416650/319742181521911525581828902143609155722867*y^14 + 334977823769028603891275689738063679750318921/14708140350007930176764129498606021163251882*y^13 + 44010533151363661463923632268027959422442704086/7354070175003965088382064749303010581625941*y^12 - 6637741597233572023111028350747918308287564871/7354070175003965088382064749303010581625941*y^11 - 67735374688197092749390830305632360224676757159/14708140350007930176764129498606021163251882*y^10 - 13798661516419406462624085887751764204490630277/7354070175003965088382064749303010581625941*y^9 - 23538412129403971200561631309627133088245460347/7354070175003965088382064749303010581625941*y^8 + 34499444545633682295006554577754372591296525189/14708140350007930176764129498606021163251882*y^7 + 92777916151623018329155914023717646296017072947/14708140350007930176764129498606021163251882*y^6 + 4070744746607440413214395880862060414361658563/7354070175003965088382064749303010581625941*y^5 - 22942285900174166451421795240673115104833832437/7354070175003965088382064749303010581625941*y^4 - 7142801404064548438906244608995778984841775382/7354070175003965088382064749303010581625941*y^3 + 6041396034259455124258904200781541670474997615/14708140350007930176764129498606021163251882*y^2 + 1191615497711124051586252388626420585657386452/7354070175003965088382064749303010581625941*y + 32953862304597035012721723292464969843381756/7354070175003965088382064749303010581625941 2245754653353671317933280650486082940694358/319742181521911525581828902143609155722867*y^22 - 34472860690374470531141249818100630623455157/1278968726087646102327315608574436622891468*y^21 - 233224844350218428993474506078674671304112539/1278968726087646102327315608574436622891468*y^20 + 34226709373671840754060611205817874766336401/67314143478297163280385032030233506467972*y^19 + 390944266745195530809904454611525253537146282/319742181521911525581828902143609155722867*y^18 - 551455605702895219620603203736737129619367853/639484363043823051163657804287218311445734*y^17 + 3713599057393226084892973501062038269325155661/639484363043823051163657804287218311445734*y^16 + 899156982446185310180634003529702336165137767/319742181521911525581828902143609155722867*y^15 - 2197310536575713146571398484236231649594859951/319742181521911525581828902143609155722867*y^14 + 2974182723553431839791597399919180237575036085/1278968726087646102327315608574436622891468*y^13 - 30575260840784792331797818494595078727787877971/1278968726087646102327315608574436622891468*y^12 + 16359237812847419785380291300038716445658501461/1278968726087646102327315608574436622891468*y^11 + 16644517825439536952775777129588222029170196041/1278968726087646102327315608574436622891468*y^10 + 3728509921127645076268760395256397761305425361/1278968726087646102327315608574436622891468*y^9 + 13340081781653671204195432556047694968910745967/1278968726087646102327315608574436622891468*y^8 - 16897791152731457495979222760752429841409974225/1278968726087646102327315608574436622891468*y^7 - 12470349521338300122859931589538040505973548995/639484363043823051163657804287218311445734*y^6 + 3314084230812311992934374974364628932624237325/639484363043823051163657804287218311445734*y^5 + 13793166983859941993485653257101577413602557819/1278968726087646102327315608574436622891468*y^4 + 6507974367721372109121795537123724682434981/319742181521911525581828902143609155722867*y^3 - 2514885718651221239418954901322387718745915625/1278968726087646102327315608574436622891468*y^2 - 162076855407753428366181734487517291878998843/1278968726087646102327315608574436622891468*y + 108373916630864542057993934660230742406044555/1278968726087646102327315608574436622891468 # A Gluing Matrix {{2,0,0,0,-2,0,-2,1},{0,1,-1,1,-1,0,-1,1},{0,-1,1,-1,-1,0,-1,0},{0,1,-1,4,-2,2,-1,3},{-1,-1,-1,-2,1,-2,0,-2},{0,0,0,2,-2,2,-1,2},{-1,-1,-1,-1,0,-1,0,-1},{1,2,0,6,-4,4,-2,6}} # B Gluing Matrix {{2,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0},{0,0,1,0,0,0,0,0},{0,0,0,1,0,0,0,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {0, 1, -1, 4, -3, 2, -2, 8} # f Combinatorial flattening {-6, 1, 3, 0, 3, 0, 0, 4} # f' Combinatorial flattening {7, 2, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 23370550753326485312441869719425258896632709/639484363043823051163657804287218311445734*y^22 - 92500720421781376045753245604526976007940773/639484363043823051163657804287218311445734*y^21 - 593599974950319424702665578722254695535643613/639484363043823051163657804287218311445734*y^20 + 92395240070103980327896601506765098074312833/33657071739148581640192516015116753233986*y^19 + 1902633927015230606856526812508994912502880560/319742181521911525581828902143609155722867*y^18 - 1590623084796527750134415300792661915240619850/319742181521911525581828902143609155722867*y^17 + 10018530438801694495392442810998470880206079867/319742181521911525581828902143609155722867*y^16 + 3360299065908964222860682552053382130981431675/319742181521911525581828902143609155722867*y^15 - 21887870583918563126837056148006140979541451275/639484363043823051163657804287218311445734*y^14 + 11090786882873478305123736540414277534981014431/639484363043823051163657804287218311445734*y^13 - 82337540049950374810009042265684520261675105975/639484363043823051163657804287218311445734*y^12 + 26782391275428717443108447770194423538495558748/319742181521911525581828902143609155722867*y^11 + 29745907555897212689329351202483630621540134853/639484363043823051163657804287218311445734*y^10 + 10434992733060017048310160613846112823643364997/639484363043823051163657804287218311445734*y^9 + 17473525432351265040604795807848937155586293535/319742181521911525581828902143609155722867*y^8 - 23298898807463354681429654653794893335658323146/319742181521911525581828902143609155722867*y^7 - 28140398196521205190104074756944055463467263734/319742181521911525581828902143609155722867*y^6 + 10441652383580564651809776861768535269348793753/319742181521911525581828902143609155722867*y^5 + 29007525439259870851590660022442952435680050609/639484363043823051163657804287218311445734*y^4 - 2161470925313726736255657182866735937869670971/639484363043823051163657804287218311445734*y^3 - 4311124882338924786639468509875613281051956647/639484363043823051163657804287218311445734*y^2 - 93675860592090187889979834566193887855485219/639484363043823051163657804287218311445734*y - 36996381773730767667323423494288003901347369/639484363043823051163657804287218311445734 # 2 Loop Invariant -83452895559650303806418501820670781774009758096553574766973622624646239606295681881895121126553110521327688009902417/649816547309200584271135389903628923014056655288426938679913944923927211477790241319949362868643412701879759177109832*y^22 + 602803622334362150398232764481654118569152242910246408188981501431977724723508945220886716756546075974489051984948149/1299633094618401168542270779807257846028113310576853877359827889847854422955580482639898725737286825403759518354219664*y^21 + 1489076481970121258670452952759469859279729212022207604980209445950722852090719336492722640514315243924147360975047863/433211031539467056180756926602419282009371103525617959119942629949284807651860160879966241912428941801253172784739888*y^20 - 582295879646342327521351881163762774651079481966423818984209342036352024273076198716047445027492154159002254614866089/68401741822021114133803725253013570843584911082992309334727783676202864366083183296836775038804569758092606229169456*y^19 - 15750170905170457818293793043869372749197862958654762372849184206098839400533460525081874811609845621387493118626626637/649816547309200584271135389903628923014056655288426938679913944923927211477790241319949362868643412701879759177109832*y^18 + 13184889879729505805159112662829383026303333268629704540023681411616863601727150346980854874365580185142501306479614149/1299633094618401168542270779807257846028113310576853877359827889847854422955580482639898725737286825403759518354219664*y^17 - 135307047788671065269680564624714039480643811707840888183854131399299959693503957058417675993730394367447560388756439995/1299633094618401168542270779807257846028113310576853877359827889847854422955580482639898725737286825403759518354219664*y^16 - 4041886041842828268841786492210162590750764273457875610762455146611994557562932411912425604213751439743503553438366827/54151378942433382022594615825302410251171387940702244889992828743660600956482520109995780239053617725156646598092486*y^15 + 46373234500969310170693862037620773001608678971228856946067699360971315602959196594816146686566823856742449187343494515/433211031539467056180756926602419282009371103525617959119942629949284807651860160879966241912428941801253172784739888*y^14 - 7920644682265014636142956009684686047954312361439334626638595326440755073833699880390554272053042083066855368220574473/433211031539467056180756926602419282009371103525617959119942629949284807651860160879966241912428941801253172784739888*y^13 + 564233411930967243309518781280193793944743210492483310684376542287837516917282179833473737675208332083073160036216173965/1299633094618401168542270779807257846028113310576853877359827889847854422955580482639898725737286825403759518354219664*y^12 - 89537294023571580120200346085752600125454048391765671031209883959590267912878690052524051753701479348641305571529204729/649816547309200584271135389903628923014056655288426938679913944923927211477790241319949362868643412701879759177109832*y^11 - 340921791548088927451376874912711773645300914500420704468227375549514657060920436663878027038250627045717552109020124353/1299633094618401168542270779807257846028113310576853877359827889847854422955580482639898725737286825403759518354219664*y^10 - 25851347077974872864749014687280266465149806979160369094255205040020520502087482971022322321499140580954429112183087227/216605515769733528090378463301209641004685551762808979559971314974642403825930080439983120956214470900626586392369944*y^9 - 93570456771530010814789389401384433397442893452515840000004810665286961333279863680677131979561570823037253811775463169/433211031539467056180756926602419282009371103525617959119942629949284807651860160879966241912428941801253172784739888*y^8 + 124870628670753749361112687058550523711013902067017379123627026882119003032750288330355962860415360492882875665988901243/649816547309200584271135389903628923014056655288426938679913944923927211477790241319949362868643412701879759177109832*y^7 + 516028045301290602778236015045561810307769258192555933820768642570341835344512419663896756654683159435662795129016069157/1299633094618401168542270779807257846028113310576853877359827889847854422955580482639898725737286825403759518354219664*y^6 - 790280687526187609792775745865205203843546765737335052925052264466898970591156688496920272758082243193488294861117057/649816547309200584271135389903628923014056655288426938679913944923927211477790241319949362868643412701879759177109832*y^5 - 127466659884440796828045423549837323248536382367590645998731230335727823788100289182158071600290550073207255656418166293/649816547309200584271135389903628923014056655288426938679913944923927211477790241319949362868643412701879759177109832*y^4 - 30649596030855361041562921568708701219762434068418327019933612778420137595120478788900531272641326179471967016908120683/649816547309200584271135389903628923014056655288426938679913944923927211477790241319949362868643412701879759177109832*y^3 + 2051040336034352493575502041118462070248734590335424276208042188394044693111197360382733762578023569395781676925929097/81227068413650073033891923737953615376757081911053367334989243115490901434723780164993670358580426587734969897138729*y^2 + 3893380256186768695972297950254644448939785003391576364672895945881051836805098312015395647588977741614136874530653515/433211031539467056180756926602419282009371103525617959119942629949284807651860160879966241912428941801253172784739888*y + 7040922484432017645287052918809451546003956229966917601492578485665341653258992992804062475472583766193369334436870269/1299633094618401168542270779807257846028113310576853877359827889847854422955580482639898725737286825403759518354219664 # 3 Loop Invariant 214992144326067461646307731645778982655216644027561341214695030974771798979266813921355174298044540427907617662952156051823549324715204573363481160146747/3986477366022380696473213944325064264294803707725997989199645560811011313797263962050736459285789997017833605766533617186986197798123508669546212292603824*y^22 - 1551574411190984152561460225402741165097521050453699526313660761605838397069950356562786692568893650619403688621098895424435577051762725644565384168195223/7972954732044761392946427888650128528589607415451995978399291121622022627594527924101472918571579994035667211533067234373972395596247017339092424585207648*y^21 - 397765879402465894693921096694453402706760574066627102514752078470287660395464822916469490290369675164592619473100396063340879236725342226570423882220037/274929473518784875618842340987935466503089910877655033737906590400759400951535445658671479950744137725367834880450594288757668813663690253072152571903712*y^20 + 375546708415583026333655654001364062967034200401541295463541418534742302184944837697935753666369885283938494714521484863993723749904215594983601550042699/104907299105852123591400366955922743797231676519105210242095935810816087205191156896072012086468157816258779099119305715447005205213776543935426639279048*y^19 + 40911250601045127838663097202640284809757659243157678847053986183552508692868432083097168239048601434874893670116656981946973831122521342665185150672670377/3986477366022380696473213944325064264294803707725997989199645560811011313797263962050736459285789997017833605766533617186986197798123508669546212292603824*y^18 - 35054068826565010233195719172657990094232274225228338354623222839783222891314167703767983430456996566407015701933442573590130079565176697299452453632812089/7972954732044761392946427888650128528589607415451995978399291121622022627594527924101472918571579994035667211533067234373972395596247017339092424585207648*y^17 + 688999581327401208244233055568377641842368955851541884843874838976402152732127352197030440078711612371719856418467229912703717324470656877086899481161541113/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^16 + 4341246622208271185360385039415881180663782561841533321233005058497297394981278213505436026068806435040931520328907433470081673348543107250509526797464579/137464736759392437809421170493967733251544955438827516868953295200379700475767722829335739975372068862683917440225297144378834406831845126536076285951856*y^15 - 754291794060144522335793429755792260116827653909206717251596887681192813089615138557498925477021236273716271653867492937302448232294265928607493259474518107/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^14 + 89905430397993766526813388810411797600968595489204059478470126039743371832508517574829763498898195388116416393634044691449331588876859285580168076135926343/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^13 - 722934115269779594512935417064367752868936503365514740459263173869560920618665502239723029519464538956064047598636872077582773383371823454651352530921895733/3986477366022380696473213944325064264294803707725997989199645560811011313797263962050736459285789997017833605766533617186986197798123508669546212292603824*y^12 + 888468515573323734849372387836249699505189264302529773411350296668839487797315183946996131740244812498709915972632369818603338085682192477866484637739629507/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^11 + 951988581501939189311454769456954338392714083806703241919110087905047879892402132769971739594172415719587750917830179058709675455047676796102277630445771371/7972954732044761392946427888650128528589607415451995978399291121622022627594527924101472918571579994035667211533067234373972395596247017339092424585207648*y^10 + 11928798312914582342719844703153806217604454482549840276854269877059681985164251291978191615265732420151432162282287840187846315103367482464215928789908754/249154835376398793529575871520316516518425231732874874324977847550688207112328997628171028705361874813614600360408351074186637362382719291846638268287739*y^9 + 354427219692086291868631804325967565955114561619577010439064366490997203610589341322595133471111514029822146809446873905913989337213299674073568746439452575/3986477366022380696473213944325064264294803707725997989199645560811011313797263962050736459285789997017833605766533617186986197798123508669546212292603824*y^8 - 1320919118352246235674142430091145166515324199164373429330729004042442151792940613505086198924680299946645333686598174535727588892006741643515758280200890111/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^7 - 2755988590397570769642634204335712598032901296594320629185276616151843563489549410748966135543881186123701940235005702401706420487091584530007850649254760865/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^6 + 31249013645026432943172989751641460317919420216741644403976295514817655250533719176227425118184270586746400702326563686695185845512969708166213238806256149/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^5 + 700546502407860537999379768126266260173871521422188846234329664766363658347866824960684254184482365354257557968442304538086961978431972067557900328782136715/7972954732044761392946427888650128528589607415451995978399291121622022627594527924101472918571579994035667211533067234373972395596247017339092424585207648*y^4 + 40872781712106858311288159232264391888847805218855519823485768000083872221208862826430410307253846646708945979862250501285965577654637243320326362148428689/1993238683011190348236606972162532132147401853862998994599822780405505656898631981025368229642894998508916802883266808593493098899061754334773106146301912*y^3 - 190413451745616903033721411992200334994070085651113532284183647435086696529382900550916786685537965738742207080806806227127918329244616297588422241112524641/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y^2 - 61892211280315892458498151591001693335487754504410938058948689704473350788525353274167165233999702900941828712299935736583993203984435321746833861314192927/15945909464089522785892855777300257057179214830903991956798582243244045255189055848202945837143159988071334423066134468747944791192494034678184849170415296*y - 65997268813003995597781646816149020156207337026449741462258714926947743542275194634852441195548897746965197283147889418972315996289970629315980416543303/996619341505595174118303486081266066073700926931499497299911390202752828449315990512684114821447499254458401441633404296746549449530877167386553073150956 # 4 Loop Invariant -17141278680397964472142756111678995621158259421463103657521810662495855379715993085185572336319209509033711179658076951388597227655009698158178206981589137654382122218216950867578826197058407127413328497692482472674087477829285163/972212904378680151195056148069140344901799173714388772037928794359400532970945849745438077482748174010936850164059944502943231127975905408565138924083784982173464871058599109808810456996576883647466286659057616245120712248904596480*y^22 + 60260435958220948980151580064239484183386732401239897760109931491838818078064192465193324320692683457445632385278179939519916163598289519986286257891524835580354775840146994208613800985360073056803417987191896903356453764128697509/972212904378680151195056148069140344901799173714388772037928794359400532970945849745438077482748174010936850164059944502943231127975905408565138924083784982173464871058599109808810456996576883647466286659057616245120712248904596480*y^21 + 29056548283299351597146555220089859645569894893984150597329933630635763906591765784485244755496811722856710311886968051186096433187083682976843897578543361662019687966348163165261232709750853004157426079393267140259085789151097427/60763306523667509449691009254321271556362448357149298252370549647462533310684115609089879842671760875683553135253746531433951945498494088035321182755236561385841554441162444363050653562286055227966642916191101015320044515556537280*y^20 - 57562044684116390427062757850262470095734880169177957314529308697730831064765967338180829227428457775528719330032389309987675803522117784529715545755661633458605252338386525068604005947088288277375296650071700538483940568029944329/51169100230456850062897692003638965521147324932336251159890989176810554366891886828707267235934114421628255271792628658049643743577679232029744153899146578009129730055715742621516339841925099139340330876792506118164248013100241920*y^19 - 1115242253173368511831208804935757769279963199346543113578431909087166802761338615003260692219476519825858038746676963355761376039218637144060682657546443584721899674238503178248677441245190176799075457768625816718002440338815107811/324070968126226717065018716023046781633933057904796257345976264786466844323648616581812692494249391336978950054686648167647743709325301802855046308027928327391154957019533036602936818998858961215822095553019205415040237416301532160*y^18 + 269963208953889723282209379719891051412526902261226640890699102478783516628638256718968861888983453059809091000291031905716118512442712218956651323180409649503650819744176176383847784089988804117967554784483493423431537165049036139/243053226094670037798764037017285086225449793428597193009482198589850133242736462436359519370687043502734212541014986125735807781993976352141284731020946245543366217764649777452202614249144220911866571664764404061280178062226149120*y^17 - 13786957330261021795283936465481761752683675664660156840653441464958926053139587342586873599475872465235384494087358743093192316992233339730473199580005212183729041570330986088679312643314193477991777837407967797133568569112951042253/972212904378680151195056148069140344901799173714388772037928794359400532970945849745438077482748174010936850164059944502943231127975905408565138924083784982173464871058599109808810456996576883647466286659057616245120712248904596480*y^16 - 11493497799248858345233246755957873051610054356581428752210929002098949367376491203469277159011881632219506035322937931708886291650253367933977089958439759860848280271120714042319316771445151064088919639073709826559770956458326430599/972212904378680151195056148069140344901799173714388772037928794359400532970945849745438077482748174010936850164059944502943231127975905408565138924083784982173464871058599109808810456996576883647466286659057616245120712248904596480*y^15 + 2692549504388353259595246195132605524685141058746465669602545500660542795758368810868837463075277566396466655627513640323645331439592224298913472412641147198626393660964259465554523671934163897515459609687173599880810358613670553761/194442580875736030239011229613828068980359834742877754407585758871880106594189169949087615496549634802187370032811988900588646225595181081713027784816756996434692974211719821961762091399315376729493257331811523249024142449780919296*y^14 - 451882929501597387783872556542619471840799945398595886229691092601868476160395333042868827358389782125543804037045863150866650398212287865313409566018118744508178727023155067140149172248328783480631354451167148418867220661344219543/243053226094670037798764037017285086225449793428597193009482198589850133242736462436359519370687043502734212541014986125735807781993976352141284731020946245543366217764649777452202614249144220911866571664764404061280178062226149120*y^13 + 5675285886580379125223801602349265945201046499219271211333437944210136523760687999892197759428328064311120330659457966198506469003056538923573260151933303583327528120234470519087071997988016509956132639551068321000073211394228443949/97221290437868015119505614806914034490179917371438877203792879435940053297094584974543807748274817401093685016405994450294323112797590540856513892408378498217346487105859910980881045699657688364746628665905761624512071224890459648*y^12 - 421017558159101474450877525996612862956457881820628845663841225767353446187858356905494701908516129166480675898016107356867634431054739247681678258515548284089553476943284718394959905445318741209154909344378844204424614565839494463/32407096812622671706501871602304678163393305790479625734597626478646684432364861658181269249424939133697895005468664816764774370932530180285504630802792832739115495701953303660293681899885896121582209555301920541504023741630153216*y^11 - 315185645779698229261380763581002301078679965693845270605767435782991677624776219832371694432821889478456329292821564410839196296659186088705645765453023303650577289507583244951546288956667725038386737127778451879164226981882598045/8101774203155667926625467900576169540848326447619906433649406619661671108091215414545317312356234783424473751367166204191193592733132545071376157700698208184778873925488325915073420474971474030395552388825480135376005935407538304*y^10 - 1788282473218929326526461341546190575419124265747466633415898810457603616757415386006152399559316456335576099588983070850722887213268033423762817066178195220028669381561978751912903144719411061303495610906960418634154241552510434233/108023656042075572355006238674348927211311019301598752448658754928822281441216205527270897498083130445659650018228882722549247903108433934285015436009309442463718319006511012200978939666286320405274031851006401805013412472100510720*y^9 - 15140916705995563174805990028780587620703000919520926421046357417234898938132228361923285795517899251355195544254880242456901611794679872352486012298956265838316090286795175775776235116452410757198497448681857828863871432558116304123/486106452189340075597528074034570172450899586857194386018964397179700266485472924872719038741374087005468425082029972251471615563987952704282569462041892491086732435529299554904405228498288441823733143329528808122560356124452298240*y^8 + 1487395634952692957841404470619116175408108341248887502336912053760916342880175666172935108024233236104719721082299662455510444859087726993947674192478097083860216173323673881382781952565479534822353641188571815395262345182089809421/64814193625245343413003743204609356326786611580959251469195252957293368864729723316362538498849878267395790010937329633529548741865060360571009261605585665478230991403906607320587363799771792243164419110603841083008047483260306432*y^7 + 27375463520781617879902570877546250455659432999802037825155784763384846114236150959215878358584428772124122954212116758220376251806741371991701770872950192146668421875399843326043112645890582812857346668987018479523328937355716112331/486106452189340075597528074034570172450899586857194386018964397179700266485472924872719038741374087005468425082029972251471615563987952704282569462041892491086732435529299554904405228498288441823733143329528808122560356124452298240*y^6 + 632247033338248187677428171027948187062685190172649575761832354235577330250652868558410172000684594353135528270891160173988402833227954532909071910405031711514316966444880262808999813853205128120190098783809282545485827971116613391/243053226094670037798764037017285086225449793428597193009482198589850133242736462436359519370687043502734212541014986125735807781993976352141284731020946245543366217764649777452202614249144220911866571664764404061280178062226149120*y^5 - 8829420339712343778925714109311217039144011865584800397292606619943408519150463811716738061111458165853991662597290270810844239757376130670469586233136657984322403226204712788063445287557150637075223265159328264866740223152437737163/324070968126226717065018716023046781633933057904796257345976264786466844323648616581812692494249391336978950054686648167647743709325301802855046308027928327391154957019533036602936818998858961215822095553019205415040237416301532160*y^4 - 6908124414579026052679870854753724299720955203189608437019089202061592307658269491315165811953953658934125936966913400277025938226102109128935022038577030709125211841964527145425621184866129159339849307504698630694797512857656159979/972212904378680151195056148069140344901799173714388772037928794359400532970945849745438077482748174010936850164059944502943231127975905408565138924083784982173464871058599109808810456996576883647466286659057616245120712248904596480*y^3 + 238011397735378355334182294471352883547818685201858139548778372377345876865482307001909835267198669774106333512370549142892628940737883348378595945145094772241781627395213841527726721439136495964561576675085661807049838739589496381/64814193625245343413003743204609356326786611580959251469195252957293368864729723316362538498849878267395790010937329633529548741865060360571009261605585665478230991403906607320587363799771792243164419110603841083008047483260306432*y^2 + 1204059378428085933951753541252327219625562076697818402517720015137801116183919261712918633384749985769210752683085299306906735340198684504993322538042936991312135003881555471034385495251568722920652661594044971028105277735452666521/972212904378680151195056148069140344901799173714388772037928794359400532970945849745438077482748174010936850164059944502943231127975905408565138924083784982173464871058599109808810456996576883647466286659057616245120712248904596480*y + 4187274705761241771344939197876755630985306424659583992172664509297543501612519943031624818565703827359611516786906124545146903995821322013278013760850980015744758123272337669198046225377736382429276156359598535954090707890593507/194442580875736030239011229613828068980359834742877754407585758871880106594189169949087615496549634802187370032811988900588646225595181081713027784816756996434692974211719821961762091399315376729493257331811523249024142449780919296