# Manifold: Census Knot K8_256 # Number of Tetrahedra: 8 # Number Field x^20 + 7*x^19 + 254/13*x^18 + 77/13*x^17 - 25*x^16 - 561/13*x^15 - 985/13*x^14 - 3353/13*x^13 - 3654/13*x^12 - 104*x^11 + 6748/13*x^10 + 15768/13*x^9 + 22785/13*x^8 + 17250/13*x^7 + 12288/13*x^6 + 3340/13*x^5 + 3592/13*x^4 + 228/13*x^3 + 964/13*x^2 - 24*x + 180/13 # Approximate Field Generator -0.381391290212884 - 0.700088476028135*I # Shape Parameters -1983027303334400811585840806527554474935220605/207872963230064789335910000482234805033910670194*y^19 - 1611868009688595409342712744981074331344197922/103936481615032394667955000241117402516955335097*y^18 + 13326954630432462887152767996305743545675720973/103936481615032394667955000241117402516955335097*y^17 + 131838611858296165792699289637205537611034901951/207872963230064789335910000482234805033910670194*y^16 - 31451588657805924148975988670801181454456594858/103936481615032394667955000241117402516955335097*y^15 - 67968663720426391435674984113242936205498525059/69290987743354929778636666827411601677970223398*y^14 - 193334525057045496717471961934281318279574837/103936481615032394667955000241117402516955335097*y^13 + 53506675137187772594431323012794852163391756777/207872963230064789335910000482234805033910670194*y^12 - 545360646435567904466561464063886695959807264253/69290987743354929778636666827411601677970223398*y^11 - 484617982359766965333791730144547753559077807055/207872963230064789335910000482234805033910670194*y^10 + 13532513162379619022512401228910759045137086573/12227821366474399372700588263660870884347686482*y^9 + 968323985838117487304243938771574897587728015397/69290987743354929778636666827411601677970223398*y^8 + 704268866486095650228256184117574808103384686050/34645493871677464889318333413705800838985111699*y^7 + 887631661871667315863850542114889287331758478714/34645493871677464889318333413705800838985111699*y^6 - 227633021742190847808497126138078655734056552738/34645493871677464889318333413705800838985111699*y^5 + 675570397456530464515137129239139089980514611121/103936481615032394667955000241117402516955335097*y^4 - 904821039111224779176396743712343753718263776442/103936481615032394667955000241117402516955335097*y^3 + 270266741696699056806721065033198011780155581500/34645493871677464889318333413705800838985111699*y^2 - 347280466036494099919516353426378541952041257574/103936481615032394667955000241117402516955335097*y + 80488419548113170245519443268493210577552628041/34645493871677464889318333413705800838985111699 44591324546959222358491769903106351231905144629/1559047224225485920019325003616761037754330026455*y^19 + 262878453136075153967340320292470694653605951273/1559047224225485920019325003616761037754330026455*y^18 + 1083741990469481587587477386618414641069752791479/3118094448450971840038650007233522075508660052910*y^17 - 1132215039231954075730170830185636189017965175803/3118094448450971840038650007233522075508660052910*y^16 - 192495941219869482281665385507630690515641758501/311809444845097184003865000723352207550866005291*y^15 - 69185247741663898136205658310610177702324428129/346454938716774648893183334137058008389851116990*y^14 - 785351015365240188633177450395310883709587399477/623618889690194368007730001446704415101732010582*y^13 - 17984921347214962752706467857451633085053061235413/3118094448450971840038650007233522075508660052910*y^12 - 743469672206280409092608940150477231634005180023/1039364816150323946679550002411174025169553350970*y^11 + 8360172807335886033198606317991264022727939565443/3118094448450971840038650007233522075508660052910*y^10 + 19041828138353711029827623558166003377865427015189/1559047224225485920019325003616761037754330026455*y^9 + 8858388738030984371112816603853207347836638864718/519682408075161973339775001205587012584776675485*y^8 + 1948549085657506420083276711056926821334766078017/103936481615032394667955000241117402516955335097*y^7 + 124275275504712315059048794758218753563587752605/103936481615032394667955000241117402516955335097*y^6 + 12151794544502385162241976438961623899087340584871/1039364816150323946679550002411174025169553350970*y^5 + 6665763844867303432156676948216867557059462151/18341732049711599059050882395491306326521529723*y^4 + 12781865715595461870752643060846303430552136452561/1559047224225485920019325003616761037754330026455*y^3 + 49240281909377899618454203009262981295964274231/173227469358387324446591667068529004194925558495*y^2 + 3427781922617390718163446420607746756079136432917/1559047224225485920019325003616761037754330026455*y + 258608090957336747904385139698194504877968760131/173227469358387324446591667068529004194925558495 2726054668201139118185407824177246889221107753/61139106832371996863502941318304354421738432410*y^19 + 302204268813133774483667789566924235695428187549/1039364816150323946679550002411174025169553350970*y^18 + 363496396578761097112014550293661205472247905733/519682408075161973339775001205587012584776675485*y^17 - 297613377403980154027557787333489948887358744849/1039364816150323946679550002411174025169553350970*y^16 - 1590944948940895777116252194755749128451470515723/1039364816150323946679550002411174025169553350970*y^15 - 406248261174247671272412685796834201058244376351/346454938716774648893183334137058008389851116990*y^14 - 2098292068637727906802157471417933994221275614481/1039364816150323946679550002411174025169553350970*y^13 - 583855119704503728994510483305057098061637711819/61139106832371996863502941318304354421738432410*y^12 - 1011936118939399400811401887094447715675272342884/173227469358387324446591667068529004194925558495*y^11 + 180846740135032956329439196563644209366272044452/30569553416185998431751470659152177210869216205*y^10 + 13835455639856505544723369530431891413013930866946/519682408075161973339775001205587012584776675485*y^9 + 1459164098267663855760297871415892834882134804053/34645493871677464889318333413705800838985111699*y^8 + 2919792863108309531855297400535512946705456483585/69290987743354929778636666827411601677970223398*y^7 + 12235406727137985118070455304306877620819854883/2037970227745733228783431377276811814057947747*y^6 - 879250261686213206254550316676248865187572038934/173227469358387324446591667068529004194925558495*y^5 - 7943465217465493459012179713124931872882952470319/519682408075161973339775001205587012584776675485*y^4 - 1693185272548949200954406452021961912801836022581/519682408075161973339775001205587012584776675485*y^3 - 462601540778955154838946436279639296719902896088/173227469358387324446591667068529004194925558495*y^2 - 613080948351821967765455742996324764627293508794/519682408075161973339775001205587012584776675485*y + 18378246294583256429006407585703004078273769251/34645493871677464889318333413705800838985111699 8961216330344372382615215998536850711898608037/277163950973419719114546667309646406711880893592*y^19 + 61707777959740687920541981160312022152316902101/277163950973419719114546667309646406711880893592*y^18 + 41354550991518613729513612832239753810264279433/69290987743354929778636666827411601677970223398*y^17 + 17334466865360532844047578398327494841940741623/277163950973419719114546667309646406711880893592*y^16 - 267576904266761933947089117875123798566593109083/277163950973419719114546667309646406711880893592*y^15 - 348171573721004811055986445571528118624524150101/277163950973419719114546667309646406711880893592*y^14 - 583011752901284451990218011003583058854319430777/277163950973419719114546667309646406711880893592*y^13 - 2170665997666415414094869038422227086955337330323/277163950973419719114546667309646406711880893592*y^12 - 263517788283355201674602324731887426371775973863/34645493871677464889318333413705800838985111699*y^11 - 23672852497395811986066545545086504429410448247/69290987743354929778636666827411601677970223398*y^10 + 37205222544040197905443369758597719917258752354/2037970227745733228783431377276811814057947747*y^9 + 5188688647677894874359499406648535318767586566429/138581975486709859557273333654823203355940446796*y^8 + 13232763322231040233138188385310532539389536795065/277163950973419719114546667309646406711880893592*y^7 + 997957054623026605672928740443231157501396488080/34645493871677464889318333413705800838985111699*y^6 + 534640079676086894557279259315085138426434326930/34645493871677464889318333413705800838985111699*y^5 - 31240021430259849575514765619507843648372627821/138581975486709859557273333654823203355940446796*y^4 + 346210245948852407389332617505229853990230028853/138581975486709859557273333654823203355940446796*y^3 - 13663083347659489902159114154520093813250284566/34645493871677464889318333413705800838985111699*y^2 + 3413313409778673038365085181491926608797583789/69290987743354929778636666827411601677970223398*y - 2732477599898642883717528705885408044651483070/34645493871677464889318333413705800838985111699 46583555889416538853333210031689867523472912673/588973395818516903118411668032998614262746898883*y^19 + 311436039689604674629597177082174717315478950020/588973395818516903118411668032998614262746898883*y^18 + 794942741962223747403247932923840962542989228910/588973395818516903118411668032998614262746898883*y^17 - 81184425205686598075490487159391090267896720713/588973395818516903118411668032998614262746898883*y^16 - 1382517086625807295045677512437690620902467667107/588973395818516903118411668032998614262746898883*y^15 - 1433916854884330724726211385712485898868460887486/588973395818516903118411668032998614262746898883*y^14 - 2660720156742093522665494068072183903716414754469/588973395818516903118411668032998614262746898883*y^13 - 10865144855405469390226516632667855809631206719032/588973395818516903118411668032998614262746898883*y^12 - 8775464890585315819263091676727207763862806619516/588973395818516903118411668032998614262746898883*y^11 + 1587907234613138116235125734766906231271642056988/588973395818516903118411668032998614262746898883*y^10 + 1481426797683365117286029826221764047067590748074/34645493871677464889318333413705800838985111699*y^9 + 47536693616462584771881368936097045110481835987300/588973395818516903118411668032998614262746898883*y^8 + 58372261697359729782655761820947988826592092592105/588973395818516903118411668032998614262746898883*y^7 + 29743194036003761276306884828844830155731411321005/588973395818516903118411668032998614262746898883*y^6 + 18705020995619875703335755005846850493631701322516/588973395818516903118411668032998614262746898883*y^5 + 1041147935915309112306902933142625348732257177461/588973395818516903118411668032998614262746898883*y^4 + 5986028884667500615379347390871716535268843407327/588973395818516903118411668032998614262746898883*y^3 + 626168093588638049633413328399231934170818583226/588973395818516903118411668032998614262746898883*y^2 + 486726155748301476751306838137750215988821734588/588973395818516903118411668032998614262746898883*y + 192577547584662289281340613653296226528112670345/588973395818516903118411668032998614262746898883 8776114903220991671619354317623529429545099295/277163950973419719114546667309646406711880893592*y^19 + 14816080378836811657009168123648459342138496221/69290987743354929778636666827411601677970223398*y^18 + 75056099161962580977975993050503305892749954597/138581975486709859557273333654823203355940446796*y^17 - 30187903970439395221482196130194381383293264283/277163950973419719114546667309646406711880893592*y^16 - 162971712076864691367750160826315181539771307209/138581975486709859557273333654823203355940446796*y^15 - 276827505719216967912589518032712322200479004333/277163950973419719114546667309646406711880893592*y^14 - 91499085413136021131379692638811190685656019883/69290987743354929778636666827411601677970223398*y^13 - 1981266331386649048491035229529608707300365658819/277163950973419719114546667309646406711880893592*y^12 - 1708873391833406566138326905716950163522377097973/277163950973419719114546667309646406711880893592*y^11 + 1059589844196710930858634568978440046870090750423/277163950973419719114546667309646406711880893592*y^10 + 335380985382672154846706067910222302838869611011/16303761821965865830267451018214494512463581976*y^9 + 8634930978637339772621668444135871094037079524607/277163950973419719114546667309646406711880893592*y^8 + 4535925307779984669466340954061624519075599011609/138581975486709859557273333654823203355940446796*y^7 + 420645065836504549109639457337902762525972530463/34645493871677464889318333413705800838985111699*y^6 + 89844392638459141152724726497670110053227601599/34645493871677464889318333413705800838985111699*y^5 - 461893935341828374138599554093836175809723101491/69290987743354929778636666827411601677970223398*y^4 - 69476694762746579623995347094711662149084547499/69290987743354929778636666827411601677970223398*y^3 - 17596856101301536614413264206683399083364123562/34645493871677464889318333413705800838985111699*y^2 - 28109442798731362349750302254139598398570642809/69290987743354929778636666827411601677970223398*y + 2448249672899132824987412231179423078154733107/69290987743354929778636666827411601677970223398 297979016896832084815307214056118163300688856223/3118094448450971840038650007233522075508660052910*y^19 + 1057799263913920302940469055245370230114425151318/1559047224225485920019325003616761037754330026455*y^18 + 2935203800598996221258911166953716633369200256547/1559047224225485920019325003616761037754330026455*y^17 + 1365143999629800769599159689520142968564577749977/3118094448450971840038650007233522075508660052910*y^16 - 942705460029524460727316969596103714668274493484/311809444845097184003865000723352207550866005291*y^15 - 3971797664168679209315043884714610996011496829397/1039364816150323946679550002411174025169553350970*y^14 - 1951905102822539727332367231838686716699706817078/311809444845097184003865000723352207550866005291*y^13 - 76849864860792748664769636512693063987160053902253/3118094448450971840038650007233522075508660052910*y^12 - 28185875112635283424898632516629506791604576236163/1039364816150323946679550002411174025169553350970*y^11 - 6448588667669981119796684378961387665080314155807/3118094448450971840038650007233522075508660052910*y^10 + 9526076527511210255989965917777702162430174543749/183417320497115990590508823954913063265215297230*y^9 + 119324945058870766059182962593923898274118780588071/1039364816150323946679550002411174025169553350970*y^8 + 15956365046869282878061005559198156501839422307779/103936481615032394667955000241117402516955335097*y^7 + 11067034532516978339223050530898655875528006890175/103936481615032394667955000241117402516955335097*y^6 + 33628680964595152546792178359578968262316759553498/519682408075161973339775001205587012584776675485*y^5 + 9704465783644480424762059480992205327947284203756/311809444845097184003865000723352207550866005291*y^4 + 31033391295591306442141539711012007595525910508301/1559047224225485920019325003616761037754330026455*y^3 + 5395120783408402297649804805802679553624101692708/519682408075161973339775001205587012584776675485*y^2 - 1113858288330452565457980451490144783112229729078/1559047224225485920019325003616761037754330026455*y + 544486262595142160336352910907420056557450862978/519682408075161973339775001205587012584776675485 -14589592878853389921640139073673801489724048948/519682408075161973339775001205587012584776675485*y^19 - 26499340868735017104190974501875544118494603662/173227469358387324446591667068529004194925558495*y^18 - 545598107158142887846219693579245196235309165471/2078729632300647893359100004822348050339106701940*y^17 + 371276807137970796458262758563266484444480237129/692909877433549297786366668274116016779702233980*y^16 + 34272610774311460852612156863727765052958493235/69290987743354929778636666827411601677970223398*y^15 - 361137547111562548894159726736987381588777824331/2078729632300647893359100004822348050339106701940*y^14 + 418223198824795959899650627967926220010554548105/415745926460129578671820000964469610067821340388*y^13 + 10662656709569223313544681200656147755662410814997/2078729632300647893359100004822348050339106701940*y^12 - 3933523866400817604268983495397351278062392376809/2078729632300647893359100004822348050339106701940*y^11 - 7997882152198518472050475731058408497836238940367/2078729632300647893359100004822348050339106701940*y^10 - 107605200861347706364389196671390049784027343978/10189851138728666143917156886384059070289738735*y^9 - 10373285356128380597938960827768709659634516113731/1039364816150323946679550002411174025169553350970*y^8 - 594609464608132304176924560808271039498701328901/69290987743354929778636666827411601677970223398*y^7 + 597189493447785996971456500858859576134250959627/69290987743354929778636666827411601677970223398*y^6 - 6963758955957178449524997694909268834751251618069/692909877433549297786366668274116016779702233980*y^5 + 321407514672967505254108761070237104055639657405/207872963230064789335910000482234805033910670194*y^4 - 1681228725881734697453170105498637098148993573599/173227469358387324446591667068529004194925558495*y^3 + 1582859606302929961391010919428133235042848173362/519682408075161973339775001205587012584776675485*y^2 - 3097547227511907628585551611966524010655428551543/1039364816150323946679550002411174025169553350970*y + 245000831814671729071811779775571714611381729657/519682408075161973339775001205587012584776675485 # A Gluing Matrix {{4,2,2,-2,1,1,-4,1},{1,1,1,-1,0,1,-2,0},{1,1,1,-1,1,0,-2,1},{-1,-1,-1,0,0,0,0,0},{1,0,2,0,0,2,-1,0},{1,1,1,0,1,1,-1,1},{-2,-2,-2,0,-1,-1,1,0},{1,0,2,0,0,2,0,0}} # 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,1},{0,0,0,0,0,1,0,1},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {2, 1, 1, 0, 2, 2, -1, 2} # f Combinatorial flattening {-4, -1, -3, -5, 11, 6, 0, -7} # f' Combinatorial flattening {3, -2, 0, -8, 0, 0, 0, 0} # 1 Loop Invariant 742701444343361200040255139415615025710441047263/415745926460129578671820000964469610067821340388*y^19 + 2356462795788381604770280060630938513633725227975/207872963230064789335910000482234805033910670194*y^18 + 5208067890598062835094525736806803979291354737541/207872963230064789335910000482234805033910670194*y^17 - 9482544254992219185704356303406693037766616101721/415745926460129578671820000964469610067821340388*y^16 - 15849574524286863308797277156297769215566337416393/207872963230064789335910000482234805033910670194*y^15 - 4962856035576801026281002728207791580723936043181/138581975486709859557273333654823203355940446796*y^14 - 3941544379488117555807630915292187284780214352221/103936481615032394667955000241117402516955335097*y^13 - 138604960199858724999233906542503913761145293320659/415745926460129578671820000964469610067821340388*y^12 - 16496054150528533160124164110961711332952789350901/138581975486709859557273333654823203355940446796*y^11 + 205752540696629106035003316321384671489233595801495/415745926460129578671820000964469610067821340388*y^10 + 30021704240067751294690665320587886833558866070963/24455642732948798745401176527321741768695372964*y^9 + 196911795561069040032579785575740115770698547924313/138581975486709859557273333654823203355940446796*y^8 + 27763976908630246560684970665136039303121908517081/34645493871677464889318333413705800838985111699*y^7 - 76813055816073252862360009060197515771804981553725/69290987743354929778636666827411601677970223398*y^6 - 49549693504265254588377379695834428031982329077506/34645493871677464889318333413705800838985111699*y^5 - 105486195455574315673137093374760466468079258374309/103936481615032394667955000241117402516955335097*y^4 - 6079822390090960429146554820691383791886417699631/103936481615032394667955000241117402516955335097*y^3 + 4379566602863250325271116527498228802969664234551/34645493871677464889318333413705800838985111699*y^2 - 3297130413900278137588153544258523550867364434111/103936481615032394667955000241117402516955335097*y + 472487765021074361974907212687508470670193197837/34645493871677464889318333413705800838985111699 # 2 Loop Invariant 133313919621766484977895960455411842499791700774064480045974500222871732286008871957502897420697321/27351929499301442372106203926843913927190330571565654207463266802614041813913338952902311193961027580*y^19 + 2926722284033950192459856889879141623196504236968457964413773021602894709313853648569356598494662791/87526174397764615590739852565900524567009057829010093463882453768364933804522684649287395820675288256*y^18 + 1212761141061408556028450692974934294390304688351819320280622520444256429537237441974186680240557721/13675964749650721186053101963421956963595165285782827103731633401307020906956669476451155596980513790*y^17 + 813957047191693156225246367465429006353050038284062273837080847269407203086437429894262677931307787/218815435994411538976849631414751311417522644572525233659706134420912334511306711623218489551688220640*y^16 - 17159245453044313993779680642026296703076771065744391653592509871266989347848390726415681824751261119/109407717997205769488424815707375655708761322286262616829853067210456167255653355811609244775844110320*y^15 - 4751029294633175904447514085095181327852381018781358185885230607966658076377084068047551414516415959/24312826221601282108538847934972367935280293841391692628856237157879148279034079069246498839076468960*y^14 - 132567660890736150318721504020597761053912658539311540695700650514090222497380553985897383820726644557/437630871988823077953699262829502622835045289145050467319412268841824669022613423246436979103376441280*y^13 - 499103447040884141777046904919716596909030312805033295284208224958362804850256946410121612505839442921/437630871988823077953699262829502622835045289145050467319412268841824669022613423246436979103376441280*y^12 - 154608849368258721135695797063429958619345478506144068919048472506202215753369404880852660200002579381/145876957329607692651233087609834207611681763048350155773137422947274889674204474415478993034458813760*y^11 + 5998922373452755614250654313555048182930603119257531554288518222948077885029479610024028143621109897/54703858998602884744212407853687827854380661143131308414926533605228083627826677905804622387922055160*y^10 + 75913307902577026336204419109107367404545476092701222631637823742940149907855946507111044968365286893/25742992469930769291394074284088389578532075832061792195259545225989686413094907249790410535492731840*y^9 + 10431490386612679739244298991279912799864491064242451964078619870695776031433156817096112631256880771/1823461966620096158140413595122927595146022038104376947164217786840936120927555930193487412930735172*y^8 + 6245097804520973775568376600542009676485616241388822768908986868171339513242047086265158529111413955/911730983310048079070206797561463797573011019052188473582108893420468060463777965096743706465367586*y^7 + 32418290439549791723906417662381294918920194883172262897572982056651261682909737033245903158407139249/9725130488640512843415539173988947174112117536556677051542494863151659311613631627698599535630587584*y^6 + 46070110538230600322891949408188114843984101577686648485543082402894001381347928164712664444801673639/48625652443202564217077695869944735870560587682783385257712474315758296558068158138492997678152937920*y^5 - 505929233510418575344714492552133848866442807815873468089786204654152223550867296802351834299321951567/437630871988823077953699262829502622835045289145050467319412268841824669022613423246436979103376441280*y^4 - 7723428598528475946119059863512508563398399106398457528740774866505105167505807729070164014175230241/54703858998602884744212407853687827854380661143131308414926533605228083627826677905804622387922055160*y^3 - 2391571152216830536412615518062158271255929320654158999440198850932883248345894338537289478178347129/24312826221601282108538847934972367935280293841391692628856237157879148279034079069246498839076468960*y^2 - 1862640680356853731331641222487451399585717749095678441766890105567212284129822924147430771091322459/27351929499301442372106203926843913927190330571565654207463266802614041813913338952902311193961027580*y - 58714920569539291577938270534806603674860109133384894052113523734898595786190775246874254410879365161/14587695732960769265123308760983420761168176304835015577313742294727488967420447441547899303445881376 # 3 Loop Invariant -265397257522427654269619997585501549370150547142334054425993048006862876624321603027603575436014389243190459158779242657848617/193219540658354096167258134967231737045039460832826114835206939230411822248822407492863846184290125913905171906949521559144582400*y^19 - 93855009099700665174790534960927170642741702149012614445316572363758021426712018483451284065149513513062170898749359750162659/9660977032917704808362906748361586852251973041641305741760346961520591112441120374643192309214506295695258595347476077957229120*y^18 - 2601943079781773150762553882677685288006675414350964161227238476612501475417290478136945499580641003690249152841619774574952717/96609770329177048083629067483615868522519730416413057417603469615205911124411203746431923092145062956952585953474760779572291200*y^17 - 570772075795291844201784771748809585847172906564851756993944080083564945693079361801355516889885993724932359728921539505290359/96609770329177048083629067483615868522519730416413057417603469615205911124411203746431923092145062956952585953474760779572291200*y^16 + 4358881462305102923386137907077015815843793637429458619592726141030885249280445991084962347227456463344953663293722247923922281/96609770329177048083629067483615868522519730416413057417603469615205911124411203746431923092145062956952585953474760779572291200*y^15 + 4102667457849252149894179649488859309149112355381564646094672655687239477349233060830856987339871870124106158438562843490814423/64406513552784698722419378322410579015013153610942038278402313076803940749607469164287948728096708637968390635649840519714860800*y^14 + 17582474272516745480335443702272856336573675738339568667432224093108397003994282748539850158376001129395904168376899709788121829/193219540658354096167258134967231737045039460832826114835206939230411822248822407492863846184290125913905171906949521559144582400*y^13 + 65005741026899325677844497304537538758739657860149341968617684341900343800542500395663138303365728671865231884989950430283399877/193219540658354096167258134967231737045039460832826114835206939230411822248822407492863846184290125913905171906949521559144582400*y^12 + 3006161687616099521206653441478199987872325981360015115129943585201078177499281592323135402410299354270717920855394624451732559/8050814194098087340302422290301322376876644201367754784800289134600492593700933645535993591012088579746048829456230064964357600*y^11 + 5008778914908578315485339921953640290228172783848218060328388830092918957772045745238806213115106241683699340094282942080742033/193219540658354096167258134967231737045039460832826114835206939230411822248822407492863846184290125913905171906949521559144582400*y^10 - 2427091794601548467051869615039773075574013391317790815394756559112137996092655245506287426405634080366286859003493434090123479/2841463833211089649518501984812231427132933247541560512282454988682526797776800110189174208592501851675076057455140022928596800*y^9 - 2248561029639210666059055591972706920675980088845476943947966667858323910437492187681218816769844446836215738034839827501039733/1288130271055693974448387566448211580300263072218840765568046261536078814992149383285758974561934172759367812712996810394297216*y^8 - 28099248854358505139417438953408556130601420987036849977102670468066424831051448488662124230971681301090489090562368234969139777/12881302710556939744483875664482115803002630722188407655680462615360788149921493832857589745619341727593678127129968103942972160*y^7 - 16439512568138319175792307741571218238058030034662975221047598190050383487706701849723493521056231839599766810379710791281743947/12881302710556939744483875664482115803002630722188407655680462615360788149921493832857589745619341727593678127129968103942972160*y^6 - 34084416616689099916455758466878152315236633575551551530998710351253490277305599587941777595710308980756286301295181071333117189/64406513552784698722419378322410579015013153610942038278402313076803940749607469164287948728096708637968390635649840519714860800*y^5 + 10090938869188703870150425586195795276781893637498015571802195848980474346343195600583034676362571945778071885592367500439976137/96609770329177048083629067483615868522519730416413057417603469615205911124411203746431923092145062956952585953474760779572291200*y^4 - 26606671569413425676494981699087563342841328851890767239146065917323805480266294029447759993317744465358320212689389881017389/12076221291147131010453633435451983565314966302051632177200433701900738890551400468303990386518132869619073244184345097446536400*y^3 + 1044693352531081426141323142012421720234563126289047971475368710954407825697013781823618290018473028301786539703398830918648987/16101628388196174680604844580602644753753288402735509569600578269200985187401867291071987182024177159492097658912460129928715200*y^2 + 2384769022994881157845116548581930551000852621884568953721923574929541887683049214314839337378942354835262343277711311546662219/96609770329177048083629067483615868522519730416413057417603469615205911124411203746431923092145062956952585953474760779572291200*y + 69533443331563524663151152420253461705843330041837345789864907964923318642181925907413451640471544343577717676672139909858619/1610162838819617468060484458060264475375328840273550956960057826920098518740186729107198718202417715949209765891246012992871520 # 4 Loop Invariant 436977187134485703150156389673228065831667036736044520730583745340064816092144375994690164593342415200696038230355539000591149157145182570346419093070625611154602204437836741571/1055660836195088597215991062965429305626985283303793730995706347507630383498541646968904903715789383566680397874589524798705478403176553668997986378702818337429544115793955263744000*y^19 + 2712611180658301456274409745808170142536730488065906229073470225004452158937551208134141344607135195934871020100386315456355656297049982453141075641430124668087679917723788839481/1055660836195088597215991062965429305626985283303793730995706347507630383498541646968904903715789383566680397874589524798705478403176553668997986378702818337429544115793955263744000*y^18 + 2885964547746751107629939743012099917342955891028129533613101388504559595927628947011157803544323483882154067847127258427101515300709005167695828384655401148690703831097041185699/527830418097544298607995531482714652813492641651896865497853173753815191749270823484452451857894691783340198937294762399352739201588276834498993189351409168714772057896977631872000*y^17 - 3034360381841591668275227735047789587373201201187863340143317810377477737324639783462134295725608120019302887821108527392635054807291434498981947391865060367796435750424901893139/527830418097544298607995531482714652813492641651896865497853173753815191749270823484452451857894691783340198937294762399352739201588276834498993189351409168714772057896977631872000*y^16 - 16304884164799143734566398429204008931992549245937519638990778716835923900663902911860126543047248309916357219317217370606778056545585590270574646332971711867404854105818871746279/1055660836195088597215991062965429305626985283303793730995706347507630383498541646968904903715789383566680397874589524798705478403176553668997986378702818337429544115793955263744000*y^15 - 337031769654086727714461912232059273958280470963259163726476690702470423449007357855632683550706237717783878742870968578393372108674916492306238031050603297761543416172868345933/87971736349590716434665921913785775468915440275316144249642195625635865291545137247408741976315781963890033156215793733225456533598046139083165531558568194785795342982829605312000*y^14 - 6006692397791418966504203460106704816614112275088207768371175429849691375263193709237779757826798387880046167059715406290896495575164938966219833531949822157286211698593445283619/527830418097544298607995531482714652813492641651896865497853173753815191749270823484452451857894691783340198937294762399352739201588276834498993189351409168714772057896977631872000*y^13 - 88120182069300941381040030648352087875131842758660741914090647670706155236071521969952310620055389248169214307884971690576558365296234701620932715658224383324039432207691573442979/1055660836195088597215991062965429305626985283303793730995706347507630383498541646968904903715789383566680397874589524798705478403176553668997986378702818337429544115793955263744000*y^12 - 1316943540694975965197418572563812813272483397186688578332072171889006663579847590090566019508230470035590313022383341883783007097370602252763360755808607681251033239992860215611/87971736349590716434665921913785775468915440275316144249642195625635865291545137247408741976315781963890033156215793733225456533598046139083165531558568194785795342982829605312000*y^11 + 53271847545305463995845723558191208991558681617588123273196661231700976944643048283864897853471382424676189709871549964414943558154721866951403815059312005419696539398419428123227/527830418097544298607995531482714652813492641651896865497853173753815191749270823484452451857894691783340198937294762399352739201588276834498993189351409168714772057896977631872000*y^10 + 26770414407048241121613899564550508609639713507277674254991931686663596455141323348983986976905870622185258341053135408528025185595904682592734979345655680167015280673344099807671/105566083619508859721599106296542930562698528330379373099570634750763038349854164696890490371578938356668039787458952479870547840317655366899798637870281833742954411579395526374400*y^9 + 19434632003923213910173300577526513135363680275037497322974476081183553689076593221866463160210086825263192702423199001991845183414120576690071685001863929113251977573615406139897/70377389079672573147732737531028620375132352220252915399713756500508692233236109797926993581052625571112026524972634986580365226878436911266532425246854555828636274386263684249600*y^8 + 4835737866598521698068280564977877817691742853631186458207316435755753268833476000571538750668588677594559208036672126221924160683656867738160064319480453131473271392040790424061/23459129693224191049244245843676206791710784073417638466571252166836230744412036599308997860350875190370675508324211662193455075626145637088844141748951518609545424795421228083200*y^7 - 5958893564196626717655139712724705954737741096569169700749065962021155549308374198895406959401233882805368485482312338501108524955746694831933417862426904545888580979347602508643/35188694539836286573866368765514310187566176110126457699856878250254346116618054898963496790526312785556013262486317493290182613439218455633266212623427277914318137193131842124800*y^6 - 10377462984965640606569899430020939597166545874851115943721481611407222062929500128393183186091855444590347004222466419823815358915519172297397170694601577022793162511078757714887/87971736349590716434665921913785775468915440275316144249642195625635865291545137247408741976315781963890033156215793733225456533598046139083165531558568194785795342982829605312000*y^5 - 290796625924079411687409041460953154683423004338706676097180347524944942805391222043535839812957031071504755413890583201345742881320630580050282260099701825922060721584733456262461/1055660836195088597215991062965429305626985283303793730995706347507630383498541646968904903715789383566680397874589524798705478403176553668997986378702818337429544115793955263744000*y^4 - 52024310845632981303778405431383732762711516516542426771350979251213156307765561576353225194639973756524052959266321544947435724766498671712592084170345926692350870297267003282739/1055660836195088597215991062965429305626985283303793730995706347507630383498541646968904903715789383566680397874589524798705478403176553668997986378702818337429544115793955263744000*y^3 - 17824404621647934654787091843257179940246048328885629869241986778150606392605982789725023090888786372694826068445023876429852128467805495740894757986173721585818510251083712040041/175943472699181432869331843827571550937830880550632288499284391251271730583090274494817483952631563927780066312431587466450913067196092278166331063117136389571590685965659210624000*y^2 - 17260735280622267920210760479052718617913755563118131123340825940624823742973758412674137827744713059040474475777634765580906167049044708926046502517876036053474017467086485351/13195760452438607465199888287067866320337316041297421637446329343845379793731770587111311296447367294583504973432369059983818480039706920862474829733785229217869301447424440796800*y - 6196755649117255005741268527423820900154168764355133533323804608544432183214241293014460397351055185759041663981156420652763965967844632933629107428584042255330365442486608219/351886945398362865738663687655143101875661761101264576998568782502543461166180548989634967905263127855560132624863174932901826134392184556332662126234272779143181371931318421248