# Manifold: Census Knot K8_101 # Number of Tetrahedra: 8 # Number Field x^20 - 7*x^19 - 3*x^18 + 113*x^17 + 366*x^16 + 535*x^15 + 1102*x^14 + 2986*x^13 + 5218*x^12 + 5801*x^11 + 6917*x^10 + 12993*x^9 + 18911*x^8 + 10969*x^7 + 2446*x^6 - 439/2*x^5 + 1411*x^4 + 886*x^3 + 96*x^2 - 56*x + 16 # Approximate Field Generator 0.139747345675930 - 0.148551404835065*I # Shape Parameters 11032735477954748591473143951434176503997347/7362345429650788848255031674244566701721955000*y^19 - 108016082982701801663801725177198040734900893/7362345429650788848255031674244566701721955000*y^18 + 1466944079595136154514787908577029964397191/58898763437206310786040253393956533613775640*y^17 + 1321465495121191849620059033726903649523676711/7362345429650788848255031674244566701721955000*y^16 + 63588921384910540979231404791470457924943107/736234542965078884825503167424456670172195500*y^15 - 1050134307818599506681227298206561184266056339/1472469085930157769651006334848913340344391000*y^14 - 2594624971873687642165797576459717988809759883/3681172714825394424127515837122283350860977500*y^13 - 2037187351888731965193267473228469898050698383/3681172714825394424127515837122283350860977500*y^12 - 19027524899016583359568009157796630019930403881/3681172714825394424127515837122283350860977500*y^11 - 104368885636066997709648941686620241707065490109/7362345429650788848255031674244566701721955000*y^10 - 126441867613008272867870848145013621660862929393/7362345429650788848255031674244566701721955000*y^9 - 111947956468819037101685176727289543501435323513/7362345429650788848255031674244566701721955000*y^8 - 233494466346386134612847624773063071935302944527/7362345429650788848255031674244566701721955000*y^7 - 508669732682084231192439025172534421305836769633/7362345429650788848255031674244566701721955000*y^6 - 207034795361790775923416004923095783372730166221/3681172714825394424127515837122283350860977500*y^5 - 3745849266722451045740199791917900228804225393/117797526874412621572080506787913067227551280*y^4 - 42482762270616802997937122449782039258854380883/7362345429650788848255031674244566701721955000*y^3 - 4486389815083808192364884297985417903321775939/920293178706348606031878959280570837715244375*y^2 - 3056267647165770823261376848702280814367333311/1840586357412697212063757918561141675430488750*y - 1296088853915483242623288741768308670390060113/920293178706348606031878959280570837715244375 25381156924378892849595495756153828663579361/1051763632807255549750718810606366671674565000*y^19 - 179135921641608987702479272558040967812859609/1051763632807255549750718810606366671674565000*y^18 - 3156144048425884858249800486294159844271961/42070545312290221990028752424254666866982600*y^17 + 2976655301319839174130879757992663116591651843/1051763632807255549750718810606366671674565000*y^16 + 226672584875886436428043423521850922768347369/26294090820181388743767970265159166791864125*y^15 + 2312958236895081398164171716232677840870730603/210352726561451109950143762121273334334913000*y^14 + 2988945378788344209259417721295945112182561174/131470454100906943718839851325795833959320625*y^13 + 35651415599504507921833837472617529274778755621/525881816403627774875359405303183335837282500*y^12 + 59225186645104860476863799055302348225164443647/525881816403627774875359405303183335837282500*y^11 + 111872619120309743231692595672102898219120247133/1051763632807255549750718810606366671674565000*y^10 + 132081325962942456366740049191662606899599381691/1051763632807255549750718810606366671674565000*y^9 + 294789068768170138021715553306052694849749301931/1051763632807255549750718810606366671674565000*y^8 + 415818066308199491752495593088237492635351063449/1051763632807255549750718810606366671674565000*y^7 + 140519483853637309216580473213588500082823661671/1051763632807255549750718810606366671674565000*y^6 - 8164385081381432314156037966214466470600591412/131470454100906943718839851325795833959320625*y^5 + 352906990607767820778128819195008103303764557/16828218124916088796011500969701866746793040*y^4 + 19316677328733367412584065875432703972526456873/525881816403627774875359405303183335837282500*y^3 + 1730586225558499739961536984066699150772589197/525881816403627774875359405303183335837282500*y^2 - 790957282416581125434047288076268560414644643/262940908201813887437679702651591667918641250*y + 118687738446708805226031219068926173533878831/131470454100906943718839851325795833959320625 -15162358716166002750214826667874353872567369/1051763632807255549750718810606366671674565000*y^19 + 104463018844115871604024509772084348272128711/1051763632807255549750718810606366671674565000*y^18 + 2439450891382630234811639039524650628042771/42070545312290221990028752424254666866982600*y^17 - 1738215736928794187347953400777691170870053497/1051763632807255549750718810606366671674565000*y^16 - 572498054917762980790239886476381747258174799/105176363280725554975071881060636667167456500*y^15 - 1658766514541497912190829059490343499056556307/210352726561451109950143762121273334334913000*y^14 - 8305594393933751581719075848587147908601131359/525881816403627774875359405303183335837282500*y^13 - 23101350889560837305444784003618329422375081409/525881816403627774875359405303183335837282500*y^12 - 40644094164876552676938003565481081576130575613/525881816403627774875359405303183335837282500*y^11 - 88460020911696964873672126743132199923904979057/1051763632807255549750718810606366671674565000*y^10 - 103781418844987579506249683095602720130829436589/1051763632807255549750718810606366671674565000*y^9 - 200733257462527493971834499680859409313165930649/1051763632807255549750718810606366671674565000*y^8 - 295403226399372576836656073465539309848311984671/1051763632807255549750718810606366671674565000*y^7 - 165627505334514293591047021660602761740429619209/1051763632807255549750718810606366671674565000*y^6 - 10510814635750527023203746229287380535654589683/525881816403627774875359405303183335837282500*y^5 - 131475829490707914891776028534936928481963989/16828218124916088796011500969701866746793040*y^4 - 25130119014243244584653491416258901576695052159/1051763632807255549750718810606366671674565000*y^3 - 6781230102901708057307465741461436180791869913/525881816403627774875359405303183335837282500*y^2 - 345114275940549455279492942163892192121230053/262940908201813887437679702651591667918641250*y + 132229201886808462489786259355142140256460226/131470454100906943718839851325795833959320625 -3257029962396609308547048932930146146406006131/1746979394092851468135943944417175041651452465000*y^19 + 20178229248514355292274751618293103101147787489/1746979394092851468135943944417175041651452465000*y^18 + 1105775293362421847342638799017061806178644001/69879175763714058725437757776687001666058098600*y^17 - 356422428079772575359481972065036620835283648603/1746979394092851468135943944417175041651452465000*y^16 - 148997290992952954812801143515465288051992579921/174697939409285146813594394441717504165145246500*y^15 - 551331143504732517975165563971176678339308353013/349395878818570293627188788883435008330290493000*y^14 - 232363607309828162470880602963305884911507704981/79408154276947794006179270200780683711429657500*y^13 - 6355484929159136871410892439001494056573222309841/873489697046425734067971972208587520825726232500*y^12 - 12577334527903545312667311620539439495343641291687/873489697046425734067971972208587520825726232500*y^11 - 33597286979577708812500596192298710158952963755443/1746979394092851468135943944417175041651452465000*y^10 - 39013023077195638442938797462878959524679612584811/1746979394092851468135943944417175041651452465000*y^9 - 61274207175616802819131728156122101889477887294851/1746979394092851468135943944417175041651452465000*y^8 - 97289773956555195314149349662299988719786324756629/1746979394092851468135943944417175041651452465000*y^7 - 89645035184366204535811365041892984863571400041891/1746979394092851468135943944417175041651452465000*y^6 - 20574297040629476615764407082912229214724416234617/873489697046425734067971972208587520825726232500*y^5 - 1327002473713943031921697800816316838623810857/508212187372465881639547329284996375753149808*y^4 - 4373822338170362182314355228254192018795570257091/1746979394092851468135943944417175041651452465000*y^3 - 2399304445611517355234096560042721942005925518681/436744848523212867033985986104293760412863116250*y^2 - 462755243735847317608493566577397273100847601236/218372424261606433516992993052146880206431558125*y + 194622726762737179463241918072668661504677090873/436744848523212867033985986104293760412863116250 -4667904155522732945069387386631156883080039/262940908201813887437679702651591667918641250*y^19 + 32018470333938023966922822253806030671197541/262940908201813887437679702651591667918641250*y^18 + 747652392281301255797100023125222459681277/10517636328072555497507188106063666716745650*y^17 - 526264881202350980164685207428716440783806507/262940908201813887437679702651591667918641250*y^16 - 178189585218842561242357090151419816598898979/26294090820181388743767970265159166791864125*y^15 - 545610759707111236968031329640591020047573127/52588181640362777487535940530318333583728250*y^14 - 2738711678886212636041994915327582483048111429/131470454100906943718839851325795833959320625*y^13 - 7325979732402831625600772858193081240185436779/131470454100906943718839851325795833959320625*y^12 - 13133241678676288679846160087888434844362564353/131470454100906943718839851325795833959320625*y^11 - 30366973122656881543589979656211587613077161567/262940908201813887437679702651591667918641250*y^10 - 35963971040360662102689821949410019503396580559/262940908201813887437679702651591667918641250*y^9 - 65170620140696189333083450609419585880270359719/262940908201813887437679702651591667918641250*y^8 - 96716179465514336502668410076831980261743349351/262940908201813887437679702651591667918641250*y^7 - 63247037278444129143595481409526633955789189129/262940908201813887437679702651591667918641250*y^6 - 9205153583649315337751759254015271450414485273/131470454100906943718839851325795833959320625*y^5 - 21733339556330775284257388170580995445182787/4207054531229022199002875242425466686698260*y^4 - 6908940144168052836382353175746732294231109779/262940908201813887437679702651591667918641250*y^3 - 2948063796796460861347956983349714254963865578/131470454100906943718839851325795833959320625*y^2 - 537215788572425975293437875357328762953676836/131470454100906943718839851325795833959320625*y + 100331297764614846469585596475203984295142199/131470454100906943718839851325795833959320625 -9413259968853720786946152962087074842046131/1840586357412697212063757918561141675430488750*y^19 + 67139013918740404356097825258082604322039389/1840586357412697212063757918561141675430488750*y^18 + 30039379668751598570799932540233244565249/2944938171860315539302012669697826680688782*y^17 - 1062191815028971726972232125641218420804037553/1840586357412697212063757918561141675430488750*y^16 - 330236574475216492435396904765618562283451911/184058635741269721206375791856114167543048875*y^15 - 933150762273125718977704615400242038964845153/368117271482539442412751583712228335086097750*y^14 - 4985237099027422813430830646950141922963404091/920293178706348606031878959280570837715244375*y^13 - 13544541962929758004908932003928797442006609341/920293178706348606031878959280570837715244375*y^12 - 23073277329917993175769331056010376598449767037/920293178706348606031878959280570837715244375*y^11 - 50243140467005152288699799653080672222064448943/1840586357412697212063757918561141675430488750*y^10 - 61470511795171397253580199221183133876518897361/1840586357412697212063757918561141675430488750*y^9 - 117353195200681947162202687745882057011553364851/1840586357412697212063757918561141675430488750*y^8 - 166318024967478643685757830017194533469640113229/1840586357412697212063757918561141675430488750*y^7 - 88870963341125191952438098535236975035832959091/1840586357412697212063757918561141675430488750*y^6 - 11113182135399070737647095555457606617311018717/920293178706348606031878959280570837715244375*y^5 - 9482685790646040069577481232093413367722247/29449381718603155393020126696978266806887820*y^4 - 13874146428785048311275125232057350245518139591/1840586357412697212063757918561141675430488750*y^3 - 4015716771079462043135590774730249750472462162/920293178706348606031878959280570837715244375*y^2 - 470216189139831963429058262041459355420113044/920293178706348606031878959280570837715244375*y + 595804605519305268733499503956353371126120671/920293178706348606031878959280570837715244375 -338969325436750520950864460813632442802849/262940908201813887437679702651591667918641250*y^19 + 1984734056669738925717870052735608878250231/262940908201813887437679702651591667918641250*y^18 + 27582661919775869513306805446332807758623/2103527265614511099501437621212733343349130*y^17 - 34906873140937432518576279209890582338986937/262940908201813887437679702651591667918641250*y^16 - 16880891171349163656166500407351090089329794/26294090820181388743767970265159166791864125*y^15 - 71110736525392777488161758012356291540415687/52588181640362777487535940530318333583728250*y^14 - 329376575056680465256481581240121996879384189/131470454100906943718839851325795833959320625*y^13 - 759782441216396969561013764695258084140567189/131470454100906943718839851325795833959320625*y^12 - 1578530031104077482584721028258326915200492798/131470454100906943718839851325795833959320625*y^11 - 4641197854337981075577384611491889493028486997/262940908201813887437679702651591667918641250*y^10 - 5500815325971571375741019055651540065851754269/262940908201813887437679702651591667918641250*y^9 - 7847479779711547653461668850241940851287358979/262940908201813887437679702651591667918641250*y^8 - 12624869050152911520360920157012067815225907841/262940908201813887437679702651591667918641250*y^7 - 13732257002980700881921728538752745829478883689/262940908201813887437679702651591667918641250*y^6 - 4070388960781500355439447052538163420454251893/131470454100906943718839851325795833959320625*y^5 - 3084883367283305881840893928470177758656861/841410906245804439800575048485093337339652*y^4 - 549303915377876306903074584664656959914648689/262940908201813887437679702651591667918641250*y^3 - 616984243474920112797907648670036211202580798/131470454100906943718839851325795833959320625*y^2 - 452164343899685571802920730760143553241848476/131470454100906943718839851325795833959320625*y + 80317384273889092294702981945863607977803384/131470454100906943718839851325795833959320625 -338969325436750520950864460813632442802849/262940908201813887437679702651591667918641250*y^19 + 1984734056669738925717870052735608878250231/262940908201813887437679702651591667918641250*y^18 + 27582661919775869513306805446332807758623/2103527265614511099501437621212733343349130*y^17 - 34906873140937432518576279209890582338986937/262940908201813887437679702651591667918641250*y^16 - 16880891171349163656166500407351090089329794/26294090820181388743767970265159166791864125*y^15 - 71110736525392777488161758012356291540415687/52588181640362777487535940530318333583728250*y^14 - 329376575056680465256481581240121996879384189/131470454100906943718839851325795833959320625*y^13 - 759782441216396969561013764695258084140567189/131470454100906943718839851325795833959320625*y^12 - 1578530031104077482584721028258326915200492798/131470454100906943718839851325795833959320625*y^11 - 4641197854337981075577384611491889493028486997/262940908201813887437679702651591667918641250*y^10 - 5500815325971571375741019055651540065851754269/262940908201813887437679702651591667918641250*y^9 - 7847479779711547653461668850241940851287358979/262940908201813887437679702651591667918641250*y^8 - 12624869050152911520360920157012067815225907841/262940908201813887437679702651591667918641250*y^7 - 13732257002980700881921728538752745829478883689/262940908201813887437679702651591667918641250*y^6 - 4070388960781500355439447052538163420454251893/131470454100906943718839851325795833959320625*y^5 - 3084883367283305881840893928470177758656861/841410906245804439800575048485093337339652*y^4 - 549303915377876306903074584664656959914648689/262940908201813887437679702651591667918641250*y^3 - 616984243474920112797907648670036211202580798/131470454100906943718839851325795833959320625*y^2 - 452164343899685571802920730760143553241848476/131470454100906943718839851325795833959320625*y + 80317384273889092294702981945863607977803384/131470454100906943718839851325795833959320625 # A Gluing Matrix {{2,1,0,0,0,0,0,0},{2,4,-4,-6,-1,1,-4,2},{0,-1,2,2,-1,-1,2,0},{0,-2,4,8,1,-2,6,-2},{0,0,0,1,1,0,1,-1},{0,1,-2,-4,-1,1,-3,1},{0,-1,2,4,0,-2,4,0},{0,1,-2,-4,-2,0,-2,2}} # B Gluing Matrix {{1,0,0,0,0,0,0,0},{0,2,0,0,0,0,0,1},{0,0,1,0,0,0,0,1},{0,0,0,1,0,0,0,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,1,0,1},{0,0,0,0,0,0,1,1},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {2, 0, 2, 6, 1, -2, 4, -2} # f Combinatorial flattening {-2, 2, -6, 7, -6, 8, 0, 0} # f' Combinatorial flattening {4, 0, 4, 0, 0, -2, 6, 0} # 1 Loop Invariant 655720968488653387448063334834284710179284173/1051763632807255549750718810606366671674565000*y^19 - 564907932074639884437174274501520893924510839/131470454100906943718839851325795833959320625*y^18 - 48712801427966237565193438673530871054474573/21035272656145110995014376212127333433491300*y^17 + 36835958967034664729745021983642199342239688737/525881816403627774875359405303183335837282500*y^16 + 49617788409626922157754932141416285999259823371/210352726561451109950143762121273334334913000*y^15 + 75948098836026497134646120235939021354076211759/210352726561451109950143762121273334334913000*y^14 + 767604365651026093495996693972452561634820998731/1051763632807255549750718810606366671674565000*y^13 + 1021923901945213664834400431458873607948527809853/525881816403627774875359405303183335837282500*y^12 + 457104504001290654663997729142819119500068741549/131470454100906943718839851325795833959320625*y^11 + 4238232282251521727728978726611944704155378189919/1051763632807255549750718810606366671674565000*y^10 + 629747843042199758781518229843155435270509379011/131470454100906943718839851325795833959320625*y^9 + 4550771924278126445621810659216863544127702303779/525881816403627774875359405303183335837282500*y^8 + 3367237163299493876696509201546579284250125050683/262940908201813887437679702651591667918641250*y^7 + 1104432360699049969211928190584873780702334338441/131470454100906943718839851325795833959320625*y^6 + 2741859610590167730176971279716191735292548362147/1051763632807255549750718810606366671674565000*y^5 + 2062101146173051880869621992648286622395460201/16828218124916088796011500969701866746793040*y^4 + 2137386861468152721595411101143845921991928979081/2103527265614511099501437621212733343349130000*y^3 + 115259963020910485412896083997619671655318215999/131470454100906943718839851325795833959320625*y^2 + 121705054443144036606732025250914972574403171127/525881816403627774875359405303183335837282500*y - 6883052404791118704011140416992497406024775659/262940908201813887437679702651591667918641250 # 2 Loop Invariant 4975757027585233945296494211464876806442392606432152150045528872286892058178475732737392062698036885739/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200*y^19 - 290184858136874596652039543935599314122772216525258813104105661207901503536791824541612266523036390032707/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200*y^18 + 1894360849693036464224699139961471982146848795260321765245011714022523692459864533465590415028412482646821/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200*y^17 + 84814660951647202462630370429658997382819933814197987627387244520821053853341246552981226806835851048081/44795750473551890441378568962475110884634456035688024340600979205893284424027687099296033401801098291499640*y^16 - 6755792355759904226357998239842611366233789261137337312439312054426657463660824761809020369482119685664111/55994688091939863051723211203093888605793070044610030425751224007366605530034608874120041752251372864374550*y^15 - 19246578728222153507014382984466786727350728204948813128068500072203986159927721149609384176568565086811723/55994688091939863051723211203093888605793070044610030425751224007366605530034608874120041752251372864374550*y^14 - 92409245839021324173386496211470445314875900574506775549071805098666342654547140844664691243805707222459983/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200*y^13 - 218540627384703271230996307477870446066738670235840039274207692084195278779323206835732901026274167486165927/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200*y^12 - 624803394126041516745465111354690260023479405252079604725628722015229871802148885572706780495520221446539251/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200*y^11 - 123777934787925078878364023183046504527965221106180752046210905902883718439906981841159951167443421835897086/27997344045969931525861605601546944302896535022305015212875612003683302765017304437060020876125686432187275*y^10 - 16681579754224921948212763439537115659466992225250790089360349589510495780727134356951135179865548307290297/3929451795925604424682330610743430779353899652253335468473770105780112668774358517482108193140447218552600*y^9 - 611377884334762487236543726663187101592818874195925753990274358715181032484808813932413460057480078855562923/111989376183879726103446422406187777211586140089220060851502448014733211060069217748240083504502745728749100*y^8 - 261245767509956597293603927462892388009528082354605940171706816686588453860865833114477076961272012408034473/22397875236775945220689284481237555442317228017844012170300489602946642212013843549648016700900549145749820*y^7 - 1741354457421447813123293419815522807466703313705789781881246735526348678204258038550948819942974743768171609/111989376183879726103446422406187777211586140089220060851502448014733211060069217748240083504502745728749100*y^6 - 1069982382357805233396830195796158661937891438556706635137120872214249586816358423719322013786222018641122941/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200*y^5 - 37010066910298242701600409456395788313848375299997092592662894725673005788070232440250803845719289893129157/89591500947103780882757137924950221769268912071376048681201958411786568848055374198592066803602196582999280*y^4 + 17367165986704970158015323825661433055852993178202206367544903369323688868100366284159794466490013082480357/111989376183879726103446422406187777211586140089220060851502448014733211060069217748240083504502745728749100*y^3 - 14908392482322718072696053410686512814776835261869194112408191052354315942149327645352526038522805244628963/7465958412258648406896428160412518480772409339281337390100163200982214070671281183216005566966849715249940*y^2 - 10010205718890974896809832328580117577923287373898314063417315490059530958709467768052162028096506115234003/44795750473551890441378568962475110884634456035688024340600979205893284424027687099296033401801098291499640*y + 1316026521139247589262405203333254660422391077562758469943572450332763877992116437544981985697127501240127753/223978752367759452206892844812375554423172280178440121703004896029466422120138435496480167009005491457498200 # 3 Loop Invariant -2702774630873923399713429213140472060557720176125360930964581281654630302702807844235503926479145564845208594703638510824510414271170242020689/3482214742672980673617780085802856470752278393169800984787431989578792931969016683611179394330115382246038123457852836599549286478840047353285000*y^19 + 9789516098980890101378496762729009850121110207811779814490273239860736628604624652416535666882034086835823404801467509771838394271833834802333/1741107371336490336808890042901428235376139196584900492393715994789396465984508341805589697165057691123019061728926418299774643239420023676642500*y^18 + 71552107263013596016467710970910501071686950244112256296843589424584553211009075061604491204412479734995322560603598549862262044670583016513/69644294853459613472355601716057129415045567863396019695748639791575858639380333672223587886602307644920762469157056731990985729576800947065700*y^17 - 154122635885989912075922821653688087896339506107628815415486685882499923108937262538732336551657221532639308628638950204100905065498492418440391/1741107371336490336808890042901428235376139196584900492393715994789396465984508341805589697165057691123019061728926418299774643239420023676642500*y^16 - 19221731642357293812929710527187208688119601159354284251699607739004326052867860209637195324690039548522928259507534289602652671580046060267629/73309784056273277339321686016902241489521650382522125995524883991132482778295088076024829354318218573600802599112691296832616557449264154806000*y^15 - 239069935640945017956089034929429371270170436820380612078586125997177194278800131590090078733056594411020219542521799108883543613822244628809767/696442948534596134723556017160571294150455678633960196957486397915758586393803336722235878866023076449207624691570567319909857295768009470657000*y^14 - 1310988895652504345093270269508732175036375784410914670315875957109613860268127915877908031388685525327614903428883806767101679430152315390955629/1741107371336490336808890042901428235376139196584900492393715994789396465984508341805589697165057691123019061728926418299774643239420023676642500*y^13 - 14733672857922186429752459113760073521761295320332400334626902134781379319982332348552336512301045928617567618570173033256237424349730283367315591/6964429485345961347235560171605712941504556786339601969574863979157585863938033367222358788660230764492076246915705673199098572957680094706570000*y^12 - 24227275516706858807766793717672737363687126105984157264103030124393355849346419134314058057843603504321686941078506989926886344350971763743810887/6964429485345961347235560171605712941504556786339601969574863979157585863938033367222358788660230764492076246915705673199098572957680094706570000*y^11 - 24365032759987261357094299445828125911140333285710508748569258689919063534296931624809375523896055192386001387320271119666753887535081971130601909/6964429485345961347235560171605712941504556786339601969574863979157585863938033367222358788660230764492076246915705673199098572957680094706570000*y^10 - 14996816923690532549451669625969141334511067031427702603110374491110845989366846336527734292079437757532894743045499716854380413416893523280522759/3482214742672980673617780085802856470752278393169800984787431989578792931969016683611179394330115382246038123457852836599549286478840047353285000*y^9 - 30876508348034558520453084235178610668373362035250884862994263909505753486004205844537928011905178564970655943523200806557216706056348472310971119/3482214742672980673617780085802856470752278393169800984787431989578792931969016683611179394330115382246038123457852836599549286478840047353285000*y^8 - 4491190112832527994583120589796020208779965464828392782731936700869759016252794266437102278306672136777652412250439190762445895082763487097355433/366548920281366386696608430084511207447608251912610629977624419955662413891475440380124146771591092868004012995563456484163082787246320774030000*y^7 - 34165645628970468997123116335834065400160112195087130322800497552501683570751977383413676781391215435898881908270247824059477710999459499520476083/6964429485345961347235560171605712941504556786339601969574863979157585863938033367222358788660230764492076246915705673199098572957680094706570000*y^6 - 168863716753601730395892453190671063474319202703701505486984259562853336490379308152944980330716644511702647778464323481532532463983056285545567/6964429485345961347235560171605712941504556786339601969574863979157585863938033367222358788660230764492076246915705673199098572957680094706570000*y^5 + 6535417137147698965465835848343236060142016036016876431027110304565139301665918321962031626539289109910388619894470625863199707844067548089571/55715435882767690777884481372845703532036454290716815756598911833260686911504266937778870309281846115936609975325645385592788583661440757652560*y^4 - 1970772715767821053654126154975853118283176764589931185739693824067065587503818575734881535191481085649355418979864146502555082372037990992228027/1741107371336490336808890042901428235376139196584900492393715994789396465984508341805589697165057691123019061728926418299774643239420023676642500*y^3 - 1469473948390978822014803186473872149758486678652689005963453327340369854852792892478055601065517839243060718306503850712680858833997962437135481/3482214742672980673617780085802856470752278393169800984787431989578792931969016683611179394330115382246038123457852836599549286478840047353285000*y^2 + 120892795467212313636795283416169850648664537827816319754528784019054049053280299991761998290208445678044115842255844445079337383411879310576357/870553685668245168404445021450714117688069598292450246196857997394698232992254170902794848582528845561509530864463209149887321619710011838321250*y - 7662747335535746891351530719327502352439445419376582652541250619484570480348554113555337626542610278429073097160964138890348499530170542153369/435276842834122584202222510725357058844034799146225123098428998697349116496127085451397424291264422780754765432231604574943660809855005919160625 # 4 Loop Invariant -173598014041013380284401979010211449748151077234870523599940479267479029146710405238716086448264838366398824216818477184094109581861416070070304423729550610145468324614643880344302930141936697713163992272447/444933874425059323191932057721782107853685750811840571718283122323201194619478817004711153373530422344300888359450681788166696989548604207122047396152358512139912564924107439396579343081214256737572697259880000*y^19 + 912957795686333319515120320385803277450694424016398267959881789508900512875254858960924075757044733028587336640448752363793122955467324553817703882961946713121337228739122270389164653197149928978433330912267/296622582950039548794621371814521405235790500541227047812188748215467463079652544669807435582353614896200592239633787858777797993032402804748031597434905674759941709949404959597719562054142837825048464839920000*y^18 - 16236136292327909820861357329476993993258943273270910687844976280940332941108143414598930535982225643957075978919996254850016418792674873862702340314594452633450623330472615580572424381603018300209236606383/11123346860626483079798301443044552696342143770296014292957078058080029865486970425117778834338260558607522208986267044704167424738715105178051184903808962803497814123102685984914483577030356418439317431497000*y^17 - 38820033808216291285276955352829927818548724742461504840829447866115296402702522351692050314195311170283994371841429600656222780259647055775676860628714462795523364655169309411133024818094579867407470138217367/889867748850118646383864115443564215707371501623681143436566244646402389238957634009422306747060844688601776718901363576333393979097208414244094792304717024279825129848214878793158686162428513475145394519760000*y^16 - 1024251072607387234221773754464421503831024787444464985429802266877530753503300210353192279021083685297107132361623613367877135803715480876309608529201550501274424211868171753869825115005587082653824006079567/9887419431667984959820712393817380174526350018040901593739624940515582102655084822326914519411787163206686407987792928625926599767746760158267719914496855825331390331646831986590652068471427927501615494664000*y^15 - 37381530668896741451739795827790106793172419847040472863841771491979340462413972654556839070295786268720365910532153548393824473380632705328836618544825965152645133273311789928176237559470822939892210483451447/355947099540047458553545646177425686282948600649472457374626497858560955695583053603768922698824337875440710687560545430533357591638883365697637916921886809711930051939285951517263474464971405390058157807904000*y^14 - 551011581355954618565884878775529698851636990084278713374214302587724621512172913793539683318855715646854977668939152707870093820746137917494747077059697300426735151350957582263455468786068642998336416899003881/1779735497700237292767728230887128431414743003247362286873132489292804778477915268018844613494121689377203553437802727152666787958194416828488189584609434048559650259696429757586317372324857026950290789039520000*y^13 - 85388975613039945961634060152110300179946037750090716388964952928251047081946305852441590965236792074208771748530878618965315045064999851039697524013640200983586394625625681561246991676426477156283354374692027/98874194316679849598207123938173801745263500180409015937396249405155821026550848223269145194117871632066864079877929286259265997677467601582677199144968558253313903316468319865906520684714279275016154946640000*y^12 - 352328577329715821100936519525669299249146057809404507945322218328318678506558732725517042762597038706807070471127528002042392559625282786591456460155174000106214772905594179163943627554134604927044580278588557/296622582950039548794621371814521405235790500541227047812188748215467463079652544669807435582353614896200592239633787858777797993032402804748031597434905674759941709949404959597719562054142837825048464839920000*y^11 - 874194209870429492870102766221511299226787116701777782704142417489267756207761550392938223831177389452350749522927892334133281819776850722984129106317564552161296788730810977127697918590848535917272805954344857/889867748850118646383864115443564215707371501623681143436566244646402389238957634009422306747060844688601776718901363576333393979097208414244094792304717024279825129848214878793158686162428513475145394519760000*y^10 - 142660997475686916704144206198292794157263617115074035635736706099945421342719108199530807399120797436486083016489258755867282399410867445630250103885014100590873899426602153830204931262810448469994412413869777/93670289352644068040406748994059391127091737013019067730164867857516040972521856211518137552322194177747555444094880376456146734641811412025694188663654423608402645247180513557174598543413527734225831002080000*y^9 - 1030734567986095671843565476667609240005894786106560958142773775921064969869334497218898656103828149567504389833975173796127611017452429156321022925079290278770438262291907503374503900568539045791784685427242983/296622582950039548794621371814521405235790500541227047812188748215467463079652544669807435582353614896200592239633787858777797993032402804748031597434905674759941709949404959597719562054142837825048464839920000*y^8 - 2317201370029649424204434495558085698028986740475959241667131806607269439939743731885640848131059034130993946258885872261633575355942542880394057939450371005629128053549314740167067264314761328218108285731749329/593245165900079097589242743629042810471581001082454095624377496430934926159305089339614871164707229792401184479267575717555595986064805609496063194869811349519883419898809919195439124108285675650096929679840000*y^7 + 41995172843516919250050767648353144011462392830907008759232975492688179034041533795182119105784767979144868166356180581373447845066473506106215651052387042096314339654531579899806977532431752728405173752219623/444933874425059323191932057721782107853685750811840571718283122323201194619478817004711153373530422344300888359450681788166696989548604207122047396152358512139912564924107439396579343081214256737572697259880000*y^6 - 6204856607651606079128546673562515042855822411924461443920028161648124194775890110772008125918813091805709263499722841248695075037532272406511580817573158559438560522599549530605967838095079543586157162665817/111233468606264830797983014430445526963421437702960142929570780580800298654869704251177788343382605586075222089862670447041674247387151051780511849038089628034978141231026859849144835770303564184393174314970000*y^5 + 161500026807275105330049462433887404149770071226618622046142088922195915462371294378682232759522563021764811852108964760155878874076348479714543371815088754236333284656705367497590024823900314663540954303963/3559470995400474585535456461774256862829486006494724573746264978585609556955830536037689226988243378754407106875605454305333575916388833656976379169218868097119300519392859515172634744649714053900581578079040*y^4 - 134635552389534588518625042279926200427894900424626751270108769404654240445436118704054243142047980507262908542497306619560555163250267655040223156537131530118046709693458285789653773123902664414719485343544671/222466937212529661595966028860891053926842875405920285859141561161600597309739408502355576686765211172150444179725340894083348494774302103561023698076179256069956282462053719698289671540607128368786348629940000*y^3 + 25690413672085369985041693983529229245589066170594004456197868299918368061065509607079061807412777549613826231549288473924975722818597563354988530968149354111607720065641041795305014055107112081570616195359369/148311291475019774397310685907260702617895250270613523906094374107733731539826272334903717791176807448100296119816893929388898996516201402374015798717452837379970854974702479798859781027071418912524232419960000*y^2 - 8245521767434590323527460786913821864606452370985242604669415439303119497759110330549826147450298024924087761254661594967185033312017857880109835419819347320036535257045677332938543917005789638567413719767433/222466937212529661595966028860891053926842875405920285859141561161600597309739408502355576686765211172150444179725340894083348494774302103561023698076179256069956282462053719698289671540607128368786348629940000*y + 46067886629730354802117850344487903083222191824283651874782231244584960319459626959320074309403374329365136305657031772222600012311356098709875625787538654343527495971822773943478007109690605649025621782899/27808367151566207699495753607611381740855359425740035732392695145200074663717426062794447085845651396518805522465667611760418561846787762945127962259522407008744535307756714962286208942575891046098293578742500