# Manifold: Census Knot K8_243

# Number of Tetrahedra: 8

# Number Field
x^21 - x^20 - 17*x^19 - 378*x^18 + 446*x^17 + 9319*x^16 - 2960*x^15 - 65350*x^14 + 50303*x^13 + 349307*x^12 - 131814*x^11 - 1044541*x^10 + 78496*x^9 + 1881951*x^8 + 286759*x^7 - 2123216*x^6 - 617337*x^5 + 1747157*x^4 + 233956*x^3 - 818257*x^2 + 10767*x + 159953 

# Approximate Field Generator
-0.792665428336290 + 0.884836785371894*I

# Shape Parameters
5435555103409669778605850550507514316359120964093598605/79127486379811804861802487303578414181804840410673138387424*y^20 - 225734919034193771448600852167523479252855159549027887/39563743189905902430901243651789207090902420205336569193712*y^19 - 92791134185131655646417353569923833573471627378309064467/79127486379811804861802487303578414181804840410673138387424*y^18 - 2139712146725019318290798628202456137194653288559682093583/79127486379811804861802487303578414181804840410673138387424*y^17 + 461735019901009836285943207666457334126962621247230316769/79127486379811804861802487303578414181804840410673138387424*y^16 + 25533199157068890545197107869110496845693326910256942542021/39563743189905902430901243651789207090902420205336569193712*y^15 + 15366838664237766338894384903340247578060237715882750379951/39563743189905902430901243651789207090902420205336569193712*y^14 - 81687715583798193314813636552501010280314961711498331876431/19781871594952951215450621825894603545451210102668284596856*y^13 - 25924672663775324499205498012913881187165069052641486293105/79127486379811804861802487303578414181804840410673138387424*y^12 + 468175543299829542363921617659985134994407843360739613835377/19781871594952951215450621825894603545451210102668284596856*y^11 + 500001467111315664124813285682319480621237312185300094103661/39563743189905902430901243651789207090902420205336569193712*y^10 - 4746940806559834126898548158922102682780353710221452278706343/79127486379811804861802487303578414181804840410673138387424*y^9 - 3922168146995143545395968255505329974653884593734685692306969/79127486379811804861802487303578414181804840410673138387424*y^8 + 412039409052415197957495969582272395329069257451634002651313/4945467898738237803862655456473650886362802525667071149214*y^7 + 7588454673319584334260473950836310397352588111991685902035351/79127486379811804861802487303578414181804840410673138387424*y^6 - 4517730059685623370885117232430388231503949778271227634558143/79127486379811804861802487303578414181804840410673138387424*y^5 - 3729389734279820509923638690872259599404598900724281635108873/39563743189905902430901243651789207090902420205336569193712*y^4 + 2586404018149513502204266339449522355695935621090628815907751/79127486379811804861802487303578414181804840410673138387424*y^3 + 3560387198930511716524605440770857291392492007779239836359357/79127486379811804861802487303578414181804840410673138387424*y^2 - 544842919326534748419036445073836317967832585452726768049263/39563743189905902430901243651789207090902420205336569193712*y - 8224954089794166302266935924003995676423719938960657402803/815747282266101081049510178387406331771183921759516890592

-1025329026851291443923683410902587475598239538913968493661905/12656678828910037623059893251669278083622229638208400504483631072*y^20 + 34626753690816851440092825833521533310764512006719224407583/6328339414455018811529946625834639041811114819104200252241815536*y^19 + 1030425625322701492802869066557306062158952482404019474084327/744510519347649271944699603039369299036601743424023559087272416*y^18 + 403899869935780900193540827332395824494892488345459792681813275/12656678828910037623059893251669278083622229638208400504483631072*y^17 - 81057979329830994159909253315948200572040752509186921432452237/12656678828910037623059893251669278083622229638208400504483631072*y^16 - 4819598752952772651705818796921699012495455387659960981261028345/6328339414455018811529946625834639041811114819104200252241815536*y^15 - 2974274874048072020556849097970126134724393152664525488772836899/6328339414455018811529946625834639041811114819104200252241815536*y^14 + 15416752958205200568787409569961410094249411888395188133176017291/3164169707227509405764973312917319520905557409552100126120907768*y^13 + 352145015877645470299363814736588476464873542119005538294763637/744510519347649271944699603039369299036601743424023559087272416*y^12 - 88495823138781291022305901641261734338520212841976446186740372695/3164169707227509405764973312917319520905557409552100126120907768*y^11 - 97332210983711375840851624818458515660195429477888220847344245069/6328339414455018811529946625834639041811114819104200252241815536*y^10 + 897478014849897742446450389305203265882674774951512497862287736027/12656678828910037623059893251669278083622229638208400504483631072*y^9 + 758222382552924244457570220937957190244765223506173070791446931053/12656678828910037623059893251669278083622229638208400504483631072*y^8 - 9157203445267940368564462097620747101454797426950455666763894995/93063814918456158993087450379921162379575217928002944885909052*y^7 - 1465947044735977143065941872345263072497392099745353929161782911227/12656678828910037623059893251669278083622229638208400504483631072*y^6 + 848320701648916539695649377860831227214909391317820016091281764955/12656678828910037623059893251669278083622229638208400504483631072*y^5 + 724566147617048531703480247175652972642773634281085116291406370553/6328339414455018811529946625834639041811114819104200252241815536*y^4 - 478565517366687189365614004270200858505586580069346261354822992763/12656678828910037623059893251669278083622229638208400504483631072*y^3 - 717241761841549290875312131571640738988456726713119743706319491265/12656678828910037623059893251669278083622229638208400504483631072*y^2 + 100799983688072401674504920600619021456700707384374679777626617199/6328339414455018811529946625834639041811114819104200252241815536*y + 2080218093526224109722091057999894492538007180981067676182599511/130481225040309666217112301563600804985796181837200005200862176

-1305537137543596084708758653432192364092072586689947144031915302393/10525277543542157069278392590345663641783135782575623167704369566320440*y^20 - 304361462208253290999400057700213633201329338803959934113001928729/10525277543542157069278392590345663641783135782575623167704369566320440*y^19 + 2823608057702321307435383275938211234919782481042943106243228437438/1315659692942769633659799073793207955222891972821952895963046195790055*y^18 + 104156503733233976349135317398205422035900467805063178955672365813279/2105055508708431413855678518069132728356627156515124633540873913264088*y^17 + 1178698221668286376680521666055845047708767455834598636202332504066/263131938588553926731959814758641591044578394564390579192609239158011*y^16 - 6201498542217245755797232940706924108366530172158555785142072072831553/5262638771771078534639196295172831820891567891287811583852184783160220*y^15 - 2793174156323748575168807033796958837140079813183901143286875364353193/2631319385885539267319598147586415910445783945643905791926092391580110*y^14 + 9825774885518969397928028267471551267304598847507377875400925833545543/1315659692942769633659799073793207955222891972821952895963046195790055*y^13 + 31020558358458411884568179697009577812726219556586263126863971356883757/10525277543542157069278392590345663641783135782575623167704369566320440*y^12 - 92780589033108094324683561244066452974106089329359454240179696370582621/2105055508708431413855678518069132728356627156515124633540873913264088*y^11 - 373858091824082297854071965070424123280117553975439042630944749331573473/10525277543542157069278392590345663641783135782575623167704369566320440*y^10 + 287698641313689334234113543641463963391562790159642926341095275166398419/2631319385885539267319598147586415910445783945643905791926092391580110*y^9 + 259720229058187439439704417488725613108281532177864721208273981302044789/2105055508708431413855678518069132728356627156515124633540873913264088*y^8 - 1516896776994689294050981825635233998621880181962971750825709142870179673/10525277543542157069278392590345663641783135782575623167704369566320440*y^7 - 1189694380471265786420735803474261333017061463990323410287368337220680457/5262638771771078534639196295172831820891567891287811583852184783160220*y^6 + 859622784306984723802258584769805646168908392854359295359022542020345821/10525277543542157069278392590345663641783135782575623167704369566320440*y^5 + 459809999378635431385116239475892985905592488699264772432760255456637433/2105055508708431413855678518069132728356627156515124633540873913264088*y^4 - 45683425471761457673966258280995337066556940572911605259132412764902453/1315659692942769633659799073793207955222891972821952895963046195790055*y^3 - 249194238058704205461034257017276410782227108184134573797774059863957965/2105055508708431413855678518069132728356627156515124633540873913264088*y^2 + 211747003472264345114475223648445646356477761606549832774072121587677311/10525277543542157069278392590345663641783135782575623167704369566320440*y + 44693498809420029837474425844184204377620958766981048742977189086427781/1315659692942769633659799073793207955222891972821952895963046195790055

-1305537137543596084708758653432192364092072586689947144031915302393/10525277543542157069278392590345663641783135782575623167704369566320440*y^20 - 304361462208253290999400057700213633201329338803959934113001928729/10525277543542157069278392590345663641783135782575623167704369566320440*y^19 + 2823608057702321307435383275938211234919782481042943106243228437438/1315659692942769633659799073793207955222891972821952895963046195790055*y^18 + 104156503733233976349135317398205422035900467805063178955672365813279/2105055508708431413855678518069132728356627156515124633540873913264088*y^17 + 1178698221668286376680521666055845047708767455834598636202332504066/263131938588553926731959814758641591044578394564390579192609239158011*y^16 - 6201498542217245755797232940706924108366530172158555785142072072831553/5262638771771078534639196295172831820891567891287811583852184783160220*y^15 - 2793174156323748575168807033796958837140079813183901143286875364353193/2631319385885539267319598147586415910445783945643905791926092391580110*y^14 + 9825774885518969397928028267471551267304598847507377875400925833545543/1315659692942769633659799073793207955222891972821952895963046195790055*y^13 + 31020558358458411884568179697009577812726219556586263126863971356883757/10525277543542157069278392590345663641783135782575623167704369566320440*y^12 - 92780589033108094324683561244066452974106089329359454240179696370582621/2105055508708431413855678518069132728356627156515124633540873913264088*y^11 - 373858091824082297854071965070424123280117553975439042630944749331573473/10525277543542157069278392590345663641783135782575623167704369566320440*y^10 + 287698641313689334234113543641463963391562790159642926341095275166398419/2631319385885539267319598147586415910445783945643905791926092391580110*y^9 + 259720229058187439439704417488725613108281532177864721208273981302044789/2105055508708431413855678518069132728356627156515124633540873913264088*y^8 - 1516896776994689294050981825635233998621880181962971750825709142870179673/10525277543542157069278392590345663641783135782575623167704369566320440*y^7 - 1189694380471265786420735803474261333017061463990323410287368337220680457/5262638771771078534639196295172831820891567891287811583852184783160220*y^6 + 859622784306984723802258584769805646168908392854359295359022542020345821/10525277543542157069278392590345663641783135782575623167704369566320440*y^5 + 459809999378635431385116239475892985905592488699264772432760255456637433/2105055508708431413855678518069132728356627156515124633540873913264088*y^4 - 45683425471761457673966258280995337066556940572911605259132412764902453/1315659692942769633659799073793207955222891972821952895963046195790055*y^3 - 249194238058704205461034257017276410782227108184134573797774059863957965/2105055508708431413855678518069132728356627156515124633540873913264088*y^2 + 211747003472264345114475223648445646356477761606549832774072121587677311/10525277543542157069278392590345663641783135782575623167704369566320440*y + 44693498809420029837474425844184204377620958766981048742977189086427781/1315659692942769633659799073793207955222891972821952895963046195790055

2583133369831199417105494159816001849954218001958211224052244176041/21050555087084314138556785180691327283566271565151246335408739132640880*y^20 + 3314915175912556673271393692242391579841975303553421733927274287099/42101110174168628277113570361382654567132543130302492670817478265281760*y^19 - 90746489465025018346605697382252313980899724128778999033220445740991/42101110174168628277113570361382654567132543130302492670817478265281760*y^18 - 1047999498237447784585960200276356525733802182260730267425394422991947/21050555087084314138556785180691327283566271565151246335408739132640880*y^17 - 997666169428865329162928025417082086662583745125441369683580205696403/42101110174168628277113570361382654567132543130302492670817478265281760*y^16 + 12428266933356619980998346177783031117232732196161799031398868868185917/10525277543542157069278392590345663641783135782575623167704369566320440*y^15 + 31821814524176537564616151019615650411687324139626060428069550793406661/21050555087084314138556785180691327283566271565151246335408739132640880*y^14 - 77502914827879189218178401405656290651494518496055187724784392582717539/10525277543542157069278392590345663641783135782575623167704369566320440*y^13 - 124605519125279993379968979579787225411637449554243738710609769443749221/21050555087084314138556785180691327283566271565151246335408739132640880*y^12 + 379470438176941348640159406515686128933675239862400252252217614431406369/8420222034833725655422714072276530913426508626060498534163495653056352*y^11 + 2165801541723327840625055582657047179475158612075117064985387147286050387/42101110174168628277113570361382654567132543130302492670817478265281760*y^10 - 4552680846683752953280635394858646190717310229981677350107108047158487631/42101110174168628277113570361382654567132543130302492670817478265281760*y^9 - 694604180609042594557396198600797698829539983858008242859644086104540799/4210111017416862827711357036138265456713254313030249267081747826528176*y^8 + 5521226052462810584522989255562045025627640117788870451598175481840340057/42101110174168628277113570361382654567132543130302492670817478265281760*y^7 + 12151775851017385570746487536230497091188391750598614547204420086383001309/42101110174168628277113570361382654567132543130302492670817478265281760*y^6 - 130883881905529214461318106809435396837177684317382762009887395050444999/2631319385885539267319598147586415910445783945643905791926092391580110*y^5 - 11472114033532139243068702396731717126234948504677901263834143985006808271/42101110174168628277113570361382654567132543130302492670817478265281760*y^4 + 38054820306807788268967270512044313184706757292302066936195542605250979/42101110174168628277113570361382654567132543130302492670817478265281760*y^3 + 663330058972909612037034349582973201429495644069766056044941432604311733/4210111017416862827711357036138265456713254313030249267081747826528176*y^2 - 549290935207718573324989730713333936088901601509839151669901934342743389/42101110174168628277113570361382654567132543130302492670817478265281760*y - 1871548561049971379720756218440577636378583269343199832612346167020944023/42101110174168628277113570361382654567132543130302492670817478265281760

-3127161224303093468879866812441217438600335588349083384296716755332069/6125711530341535414320024487581176239517785025459012683603943087598496080*y^20 + 502159883385223938554251472819720737854789980623191034051131352374847/12251423060683070828640048975162352479035570050918025367207886175196992160*y^19 + 35532814552537053083470591401866122339742300149355881461290507152579963/4083807686894356942880016325054117493011856683639341789069295391732330720*y^18 + 410385520101949031600094769783744458394778316719988818283652913516225657/2041903843447178471440008162527058746505928341819670894534647695866165360*y^17 - 521725107166107032197217463304216929511239571497978097757453346987886811/12251423060683070828640048975162352479035570050918025367207886175196992160*y^16 - 14673086128949458122619253438197021766966169372518623551298075147445962807/3062855765170767707160012243790588119758892512729506341801971543799248040*y^15 - 17765206653994824655455148325343769074107766403234204100454610207482046207/6125711530341535414320024487581176239517785025459012683603943087598496080*y^14 + 93583005434275460438472619515592840249884127368327270556618786098426902671/3062855765170767707160012243790588119758892512729506341801971543799248040*y^13 + 4956993318308808056103238764679270100676873482659986416866717252725363319/2041903843447178471440008162527058746505928341819670894534647695866165360*y^12 - 429239547136768741686289345486854200932701304451696243628022720041148038995/2450284612136614165728009795032470495807114010183605073441577235039398432*y^11 - 1155994148449196323425471626659681470207409892021475882028137957700677995393/12251423060683070828640048975162352479035570050918025367207886175196992160*y^10 + 1803230510699508897213969786038281674737115799779026772434068082726908781019/4083807686894356942880016325054117493011856683639341789069295391732330720*y^9 + 149662725321439229866796071893776491502709712642538286884658022034727195821/408380768689435694288001632505411749301185668363934178906929539173233072*y^8 - 7481744030812319512914695471701468814083154907819326226695116511917737776603/12251423060683070828640048975162352479035570050918025367207886175196992160*y^7 - 2882820751981157586340183458350096467932732983692156273962008780641120698481/4083807686894356942880016325054117493011856683639341789069295391732330720*y^6 + 1269276413468062078640452909218826374813068064293592018261464324079623914679/3062855765170767707160012243790588119758892512729506341801971543799248040*y^5 + 2813610256157565468450826062125251083073440995519910234017087083379794963031/4083807686894356942880016325054117493011856683639341789069295391732330720*y^4 - 2940273455547588629679729601973356177993871906646575766709235388896294404333/12251423060683070828640048975162352479035570050918025367207886175196992160*y^3 - 135580066482851954010740089615936271646704297105875365177616626478041088535/408380768689435694288001632505411749301185668363934178906929539173233072*y^2 + 404936508817796232996845785261207528918303488929596076740826214071988947677/4083807686894356942880016325054117493011856683639341789069295391732330720*y + 10780439034912324783374453963540192857058475180199454932236462323710867673/126303330522505884831340711084147963701397629390907478012452434795845280

2802329179855337822662248230709339628919773673227704931911059284413459263/20202596627066383796427440760042719237929655013963823830525804302899840071840*y^20 + 243602683472588126022485304157004064169779751328681994171382021131252259/10101298313533191898213720380021359618964827506981911915262902151449920035920*y^19 - 946683158056517961409605979519571827830754205882875137551663484110280459/396129345628752623459361583530249396822150098313016153539721652998036079840*y^18 - 371705906693652794733995880143149551945045687852523881403516181686275498439/6734198875688794598809146920014239745976551671321274610175268100966613357280*y^17 - 38982586075109235275952263705133699328721122896544636101419233264278473429/20202596627066383796427440760042719237929655013963823830525804302899840071840*y^16 + 13267237397628464078928696255483127805564103907454362491109232124162103335239/10101298313533191898213720380021359618964827506981911915262902151449920035920*y^15 + 11233828941070355243060203965444844296958703039423719332251389241162042949077/10101298313533191898213720380021359618964827506981911915262902151449920035920*y^14 - 13992403839952657491138916502696924513898953823777420921212738717527093219847/1683549718922198649702286730003559936494137917830318652543817025241653339320*y^13 - 3307707444099818308631951119859010903584570225919908906814573676827583594267/1188388036886257870378084750590748190466450294939048460619164958994108239520*y^12 + 16425929576105785758468767755799223814627974246758414158298283376088261550345/336709943784439729940457346000711987298827583566063730508763405048330667864*y^11 + 124844007999633823512868169623784528446578822174382538374223372672555315784573/3367099437844397299404573460007119872988275835660637305087634050483306678640*y^10 - 2440786764326917214519173590252181084275195269806014210773197281765442026984077/20202596627066383796427440760042719237929655013963823830525804302899840071840*y^9 - 525975502258695989845935694660526536000336234109388766555880692392826258616167/4040519325413276759285488152008543847585931002792764766105160860579968014368*y^8 + 5932864898455408766633472267436435680825887620404180904641031336344960286382/37137126152695558449315148455960880952076571716845264394348904968565882485*y^7 + 1609808799099358253873241100402176221030771245212642941930093038697624870913311/6734198875688794598809146920014239745976551671321274610175268100966613357280*y^6 - 1873265985200432180466559941738018778362714691972837411921981526071644950470501/20202596627066383796427440760042719237929655013963823830525804302899840071840*y^5 - 2315941501181316245735232150942657317195358016770846588391859110874262305882059/10101298313533191898213720380021359618964827506981911915262902151449920035920*y^4 + 287371068972387934578069623750691445273369763394864575922687791680101785023311/6734198875688794598809146920014239745976551671321274610175268100966613357280*y^3 + 486447421237004631859289712268746850461222850086122602198138459416597306848515/4040519325413276759285488152008543847585931002792764766105160860579968014368*y^2 - 230986640155367060368162985941587264684399825425943497800639992514128973522253/10101298313533191898213720380021359618964827506981911915262902151449920035920*y - 68245939836576485024399415566161289383415360178513159321761316283250380529/2147156618882600042132792088430515382923759699645427126211691391529369760

148699100393941756671504463298858319831132057167681592956739043720209/14293326904130249300080057137689411225541498392737696261742533871063157520*y^20 + 1080060074791337158863884394789756772519973998092852389623256296399079/14293326904130249300080057137689411225541498392737696261742533871063157520*y^19 - 1667847436692175384354284493577428976138353794170521743333732435885531/7146663452065124650040028568844705612770749196368848130871266935531578760*y^18 - 76638768245253579014534477683308625643002742248462167173981560016817251/14293326904130249300080057137689411225541498392737696261742533871063157520*y^17 - 202841723292485598725020645598302497494869828482322608605672220543271801/7146663452065124650040028568844705612770749196368848130871266935531578760*y^16 + 879951160145361884477912232596740972631938209431815803369256260438010767/7146663452065124650040028568844705612770749196368848130871266935531578760*y^15 + 2714303112974426173199492401591881345869388853964725705948646403359041353/3573331726032562325020014284422352806385374598184424065435633467765789380*y^14 - 2310460331060106747952849201667621080730128042592691014380192701546278013/3573331726032562325020014284422352806385374598184424065435633467765789380*y^13 - 9418116483006953077131030243676957015217932952969045774000502054867173871/2041903843447178471440008162527058746505928341819670894534647695866165360*y^12 + 2527371401877691598975008389957733625156493954039166410660196248886148429/408380768689435694288001632505411749301185668363934178906929539173233072*y^11 + 378488625288424218953783061986867157526770881786417259506044184293777292479/14293326904130249300080057137689411225541498392737696261742533871063157520*y^10 - 78208959803089473116854317722254714027112756242515613094961568811236277593/7146663452065124650040028568844705612770749196368848130871266935531578760*y^9 - 29628749497797581452298898033963392238888010192610291200720162976506324187/408380768689435694288001632505411749301185668363934178906929539173233072*y^8 + 3073566846946625515612060678803734867656569774167516245837079636782274219/14293326904130249300080057137689411225541498392737696261742533871063157520*y^7 + 409837888288773578457837919023167211890137842694272772048395787316587117781/3573331726032562325020014284422352806385374598184424065435633467765789380*y^6 + 64987532137358214123072863717201883582631789718025392090538532886309796681/2041903843447178471440008162527058746505928341819670894534647695866165360*y^5 - 211890801923147613073924419979798265231780123042934293189385768979544062717/2041903843447178471440008162527058746505928341819670894534647695866165360*y^4 - 288561031417040745651781887676004273852070737835174970549837599484379279793/7146663452065124650040028568844705612770749196368848130871266935531578760*y^3 + 208418805124200686980380719282798007773388989226424503393563617993022473973/2858665380826049860016011427537882245108299678547539252348506774212631504*y^2 + 10678738952950992090460448997616088974393942302882356303978563539030198681/2041903843447178471440008162527058746505928341819670894534647695866165360*y - 1559753656648241315704251063300689010793352556649113033493839348670948727/73676942804795099484948748132419645492481950478029362173930586964243080


# A Gluing Matrix
{{3,2,2,2,2,2,2,0},{1,2,2,2,2,2,2,0},{1,2,2,3,2,1,2,1},{1,2,3,2,2,1,2,1},{1,2,2,2,2,1,2,1},{1,2,1,1,1,0,0,1},{1,2,2,2,2,0,2,2},{0,0,1,1,1,1,2,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,0},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,1}}

# nu Gluing Vector
{4, 4, 4, 4, 4, 2, 4, 2}

# f Combinatorial flattening
{0, 0, 0, 0, 2, 0, 0, 0}

# f' Combinatorial flattening
{0, 0, 0, 0, 0, 0, 0, 0}

# 1 Loop Invariant
-2272722499893739425057167119119503134953134772873708024968806912613353/6125711530341535414320024487581176239517785025459012683603943087598496080*y^20 - 703724935343648866539802155996613303632275528872973353412201541927067/1531427882585383853580006121895294059879446256364753170900985771899624020*y^19 + 13641101764099868608335713827270221960827682911728421324621908776305503/2041903843447178471440008162527058746505928341819670894534647695866165360*y^18 + 315063581853238092161490112471827550519982919014833922529328654867587169/2041903843447178471440008162527058746505928341819670894534647695866165360*y^17 + 957919388562354233813579892837224695962546728744311680855699693950968609/6125711530341535414320024487581176239517785025459012683603943087598496080*y^16 - 11167611056096917767573783785635822000603908911465231625107056677324185989/3062855765170767707160012243790588119758892512729506341801971543799248040*y^15 - 20343911066756540187774176619021535286197765667111934059676743748395633617/3062855765170767707160012243790588119758892512729506341801971543799248040*y^14 + 11415599236070624444344238184769322767802444816259615184558429057064137197/510475960861794617860002040631764686626482085454917723633661923966541340*y^13 + 196397490329029988393709253236209626516264713652504475640856246688031629989/6125711530341535414320024487581176239517785025459012683603943087598496080*y^12 - 29317149446789542504243407480556393930275647356482845073936269066393152303/204190384344717847144000816252705874650592834181967089453464769586616536*y^11 - 118376607705956417496169554894503155923679117162326376870918792389992849089/510475960861794617860002040631764686626482085454917723633661923966541340*y^10 + 2049262619476120108087080805381816924831706065175714486033109037206825574537/6125711530341535414320024487581176239517785025459012683603943087598496080*y^9 + 877130073603912380046769305095187566197012476063081275741426450853109922729/1225142306068307082864004897516235247903557005091802536720788617519699216*y^8 - 1070813619822044995775784309165469457726763899824096502715912546113616247859/3062855765170767707160012243790588119758892512729506341801971543799248040*y^7 - 2485614306685298848845052838412930585994853357165075724606202794980664543271/2041903843447178471440008162527058746505928341819670894534647695866165360*y^6 - 56994161057378833615268129283073028935984205135493797048540107589921795809/6125711530341535414320024487581176239517785025459012683603943087598496080*y^5 + 1729665474642452978658014171957509774980820002978118114309440271589373987037/1531427882585383853580006121895294059879446256364753170900985771899624020*y^4 + 411653638427534536183032184641297544126684954440755855349797595281714604949/2041903843447178471440008162527058746505928341819670894534647695866165360*y^3 - 812918731699558901956712373957508263801626826375404872518146723765653131749/1225142306068307082864004897516235247903557005091802536720788617519699216*y^2 - 43790544564931425131468046613923046997630357657777931612627905729328085711/1531427882585383853580006121895294059879446256364753170900985771899624020*y + 12033676025843202580678416636629316341786269876890661213868099336788802773/63151665261252942415670355542073981850698814695453739006226217397922640

# 2 Loop Invariant
389613871074412846800796228753858414800200458502393546480343402664637366743270347418576484339668093047541014084265856566761484928121367/11463639100190317398869790349366063906612555108286580069542045017447838659214770903842666532561539254149469512755851562007061825598922767360*y^20 + 228756583602246088546800486185005780843454612656375164715763060032878183421363068124705960608425145275572797152476552482893599573194343/11463639100190317398869790349366063906612555108286580069542045017447838659214770903842666532561539254149469512755851562007061825598922767360*y^19 - 189615077247509801278601527003309228005233751948314891902265149997803087150686268394000714400966556588062961952660929472334186352379301/318434419449731038857494176371279552961459864119071668598390139373551073867076969551185181460042757059707486465440321166862828488858965760*y^18 - 52572797227616731242990864724217495601748422154533898224590180044278449192236535675214235316737797619777624341735535310392199095701789167/3821213033396772466289930116455354635537518369428860023180681672482612886404923634614222177520513084716489837585283854002353941866307589120*y^17 - 8392258158450088063067817821478033919282395083520555677191017864038169317664309033025718526900715612108466564957871276844565542456913219/1432954887523789674858723793670757988326569388535822508692755627180979832401846362980333316570192406768683689094481445250882728199865345920*y^16 + 374127226456164207312136579749954386138881316059274382624653796338214492225557637124257572507698433089159681043368333828903516476246914441/1146363910019031739886979034936606390661255510828658006954204501744783865921477090384266653256153925414946951275585156200706182559892276736*y^15 + 575657735355536467166685453431403486688063013489217456003483629647630867644411659339178322088608931393709126859883473806545514761902907623/1432954887523789674858723793670757988326569388535822508692755627180979832401846362980333316570192406768683689094481445250882728199865345920*y^14 - 648772965840492300730822707865780613651657600039856050147269795433916294693740835162938670804350657091022417076794987465161819831830419431/318434419449731038857494176371279552961459864119071668598390139373551073867076969551185181460042757059707486465440321166862828488858965760*y^13 - 17518431817575779194526523071019125402388629077542794247544861866327623543577487649232229003229491853942094091420677293443707313975484959519/11463639100190317398869790349366063906612555108286580069542045017447838659214770903842666532561539254149469512755851562007061825598922767360*y^12 + 9484357866794663053661084680737404945500051293755306360019109719966476396884354417714620108982184609226884346058911008596543551790830508229/764242606679354493257986023291070927107503673885772004636136334496522577280984726922844435504102616943297967517056770800470788373261517824*y^11 + 2745998810326284750667766274259827837599950708664772510042203105325828145640607226826664010157785122823288228047886627627722466485225877111/201116475441935392962627900866071296607237808917308422272667456446453309810785454453380114606342793932446833557120202842229154835068820480*y^10 - 42785056750578642938405133413371096711286451315611565296707650725430197242339924210756837519550735347709836399997822311203659358421662061709/1432954887523789674858723793670757988326569388535822508692755627180979832401846362980333316570192406768683689094481445250882728199865345920*y^9 - 101087856375288344756836534855187651866816888236879716916131542949711185168938354961314191584848016315197282430761919134339097365485316812651/2292727820038063479773958069873212781322511021657316013908409003489567731842954180768533306512307850829893902551170312401412365119784553472*y^8 + 418733215946688917254213267929223228911474101546643982022465595536420319167451989477272432354086061262763112058791018931382058927783395498607/11463639100190317398869790349366063906612555108286580069542045017447838659214770903842666532561539254149469512755851562007061825598922767360*y^7 + 147899387531026945801400251365629554305426726071163809651548780349793675922621809257162409334729333669303806745632135070539365681405667037223/1910606516698386233144965058227677317768759184714430011590340836241306443202461817307111088760256542358244918792641927001176970933153794560*y^6 - 168213517146227563613634466690159672850278588696124258432953278542353488442880601559958295811869092491589945893127383496286634225675827091499/11463639100190317398869790349366063906612555108286580069542045017447838659214770903842666532561539254149469512755851562007061825598922767360*y^5 - 44128253905429646565477943767247724573463754347873022390304303750683571625957795868807401261650624109852398841301321038950130670377194021641/603349426325806178887883702598213889821713426751925266818002369339359929432356363360140343819028381797340500671360608526687464505206461440*y^4 + 421967816750793579799800220507608880817476656551050076488572198315866366089362706509210487768684585948105358639356923428639314322841602433/318434419449731038857494176371279552961459864119071668598390139373551073867076969551185181460042757059707486465440321166862828488858965760*y^3 + 96092572356286117292610454576038531940666179769749315162385623426100542426113417811371067797691947858270135430427537547477137772063222403083/2292727820038063479773958069873212781322511021657316013908409003489567731842954180768533306512307850829893902551170312401412365119784553472*y^2 - 43086205301559749879443184401589461695233952523911297755070406711535730535947131378109135434694653259546430275879863817225608429832504791849/11463639100190317398869790349366063906612555108286580069542045017447838659214770903842666532561539254149469512755851562007061825598922767360*y - 353597137216500497240326376701099478856039282305449868170339769493543973016686336099959415496431306162144020853299930110672329279060428517/29545461598428653089870593683933154398485966773934484715314549014040821286636007484130583846808090861209972971020235984554283055667326720

# 3 Loop Invariant
-74242188310820693515674242025745723089780300742717322004939190462571450248901955931741689726124676173235038078740200505359551836994762747913235176289342600952285446387/8048080971605376768897327985190520810482963529657930025812846210240480656434448903908329121983493222591404304332807745948024559176643681605319006526429943204781517023805440*y^20 - 17194291560534429913621873510944542465084743977567808704195968017198745126388478096565115306655070290807533071556976130097311911985746105425285796570789670839885432567/1006010121450672096112165998148815101310370441207241253226605776280060082054306112988541140247936652823925538041600968243503069897080460200664875815803742900597689627975680*y^19 + 1366380980446904754620153967061019795529176687801613111926363825112447317571298517398754986807395880079871908009635742607680398512623486995138036760296743158200855879651/8048080971605376768897327985190520810482963529657930025812846210240480656434448903908329121983493222591404304332807745948024559176643681605319006526429943204781517023805440*y^18 + 6323650826037876413932476435364893206001126151173338828583810885231786704138545491067172253073791186874636158844270069734630567840505300425899344685078448660611473677773/1609616194321075353779465597038104162096592705931586005162569242048096131286889780781665824396698644518280860866561549189604911835328736321063801305285988640956303404761088*y^17 + 9764099400343211622706611448250352919485506114656430188570457194145624702409502887468617309143674546063971090199422825103239921496803134811239605729998215179708942690691/1609616194321075353779465597038104162096592705931586005162569242048096131286889780781665824396698644518280860866561549189604911835328736321063801305285988640956303404761088*y^16 - 371541274540268766323483991979013760909143125741895434617410419540734174712970169854178998839262925822447824857467659971616665032966459509114726177294675103509263962415427/4024040485802688384448663992595260405241481764828965012906423105120240328217224451954164560991746611295702152166403872974012279588321840802659503263214971602390758511902720*y^15 - 871050472017763399161625112048258834691030521207755564541925914166833650013014215548622731071040674200969331290556548421785616335585515065081416074312175611764499672873299/4024040485802688384448663992595260405241481764828965012906423105120240328217224451954164560991746611295702152166403872974012279588321840802659503263214971602390758511902720*y^14 + 1112754854310163936920546532370314459020156982797342545413884272954535064604699273004141068422284201031862887192859746387330111182122344629652897660910674702055214824854939/2012020242901344192224331996297630202620740882414482506453211552560120164108612225977082280495873305647851076083201936487006139794160920401329751631607485801195379255951360*y^13 + 8994576051531193479554994496672327782722071633426322522837939971255289550323004437697749575705775337231171453420233973512419022533137528619476034892439006066223100775356543/8048080971605376768897327985190520810482963529657930025812846210240480656434448903908329121983493222591404304332807745948024559176643681605319006526429943204781517023805440*y^12 - 3012848396489949327577897513449526506935234841276816204293612981199071889272965616382192884920433529233082720654583141309004254697062306120270481329658794764090593281506081/804808097160537676889732798519052081048296352965793002581284621024048065643444890390832912198349322259140430433280774594802455917664368160531900652642994320478151702380544*y^11 - 943648413755879239952147887673365586339624989633689089508525779586927735452813892958680553495868457246523655497534562653557363247901778393812450262759932399611954421067243/125751265181334012014020749768601887663796305150905156653325722035007510256788264123567642530992081602990692255200121030437883737135057525083109476975467862574711203496960*y^10 + 66698644601381825647335491472049510605280238944674905482647436744501069967566883478416515676166437181804864917758439500478382331822617468583684432812200374470072558267444959/8048080971605376768897327985190520810482963529657930025812846210240480656434448903908329121983493222591404304332807745948024559176643681605319006526429943204781517023805440*y^9 + 35564421303755531601995089033450910910525312781488932331079413681061352796825118441056797134826754020412631833399711581191244274522237867066199999180576487501231892894869219/1609616194321075353779465597038104162096592705931586005162569242048096131286889780781665824396698644518280860866561549189604911835328736321063801305285988640956303404761088*y^8 - 30901971584710711874659526647222400597141477236905436175989613337759689055579381997795266500023646208462826068059617636828437969161243879582910340321731730230499037977038691/4024040485802688384448663992595260405241481764828965012906423105120240328217224451954164560991746611295702152166403872974012279588321840802659503263214971602390758511902720*y^7 - 294957905154861717183239084965490309179460093109942989272219697057838195755590762923216385379212868418083596216688256258709808902679698959807568877824878318175331961414093171/8048080971605376768897327985190520810482963529657930025812846210240480656434448903908329121983493222591404304332807745948024559176643681605319006526429943204781517023805440*y^6 - 22501267915887853157071014762423628144234001418031613455703388957691490105898982060452298843056703712939097815086649204206683387545213815882679888944883604025305131162747811/8048080971605376768897327985190520810482963529657930025812846210240480656434448903908329121983493222591404304332807745948024559176643681605319006526429943204781517023805440*y^5 + 3407671320625763206973072115932231567695896841203629788161389966610874673221275479573182916783248037912672800468204488101590065154392993153487929477030168929598410501408363/100601012145067209611216599814881510131037044120724125322660577628006008205430611298854114024793665282392553804160096824350306989708046020066487581580374290059768962797568*y^4 + 57928029050404419258685322825424618260134879099558570079798193288383402668279022502626164487557427167934990382605879953982487798305410827873864571567218442388227579920255529/8048080971605376768897327985190520810482963529657930025812846210240480656434448903908329121983493222591404304332807745948024559176643681605319006526429943204781517023805440*y^3 - 35021152889820200713809338075278328944308153396457038847330845630679248497273631170356101794070590772748676532731743980094664294440365018129373419119861112314609957131049591/1609616194321075353779465597038104162096592705931586005162569242048096131286889780781665824396698644518280860866561549189604911835328736321063801305285988640956303404761088*y^2 - 543910544183211410282690738414529635440543105164926030078441666987567421423306391313656724003967882892181520259913280688971992313034855154908532649712304563800673264476437/1006010121450672096112165998148815101310370441207241253226605776280060082054306112988541140247936652823925538041600968243503069897080460200664875815803742900597689627975680*y + 551047036680774662339428662459909464566368301726358276731444674208827227062947968807177908902039061091967468546645788640287222455659124502031581510601608535390389548585331/82969906923766770813374515311242482582298593089257010575390167115881243880767514473281743525603022913313446436420698411835304733779831769127000067282782919636922855915520

# 4 Loop Invariant
-22492339283448786624740273025456968858232976336423417757289353095992486949939666903621885010349109236227484782657313063822712561135975356495678657467474626815596936066536776487665648399645558854895625655027376110213021017608283888351147/677752010730125278893898196726195354523498177909513920734583009190847535517543759093578882479348466788709569431121155044103075617405344577328857990541867862854897241075474082928019639335400252922814137176220986257019286572915498595490201600*y^20 + 17069465266100167685959525174748551512138220728694107301480948290432459968542621411505304252778757137012260223302176118389752911597021630666292351066000842500298381366369155477435706127947283249964837666236197248583843815106891702855583/338876005365062639446949098363097677261749088954756960367291504595423767758771879546789441239674233394354784715560577522051537808702672288664428995270933931427448620537737041464009819667700126461407068588110493128509643286457749297745100800*y^19 + 40124496630857931295775791839458198634852193743514292462030936175077464089228094967999751557548493628636353191781925034486532861078226355839109683155478093237577538308278570434892504207892470823709146834467602330783143878709446345351809/75305778970013919877099799636243928280388686434390435637175889910094170613060417677064320275483162976523285492346795004900341735267260508592095332282429762539433026786163786992002182148377805880312681908468998473002142952546166510610022400*y^18 + 924147232236838827202192681149715275377593352298915539138943278886233096152955375270530176038310971358704142985048297929611086152306681385647735845728497426091136209165315433335931037329603728200325847951314430252102817974902198238448481/75305778970013919877099799636243928280388686434390435637175889910094170613060417677064320275483162976523285492346795004900341735267260508592095332282429762539433026786163786992002182148377805880312681908468998473002142952546166510610022400*y^17 - 14279029028016558723794747615471154826375654979528117467526316454608771535336070651147380555707621975777835222877550342333490384895604196970526298610525583150352928147574624224125992518714169595302593345205793717780232987276400459050567627/677752010730125278893898196726195354523498177909513920734583009190847535517543759093578882479348466788709569431121155044103075617405344577328857990541867862854897241075474082928019639335400252922814137176220986257019286572915498595490201600*y^16 - 100419024952936511338819209169427618806115964744795872973723443254149529302710313252444839899488456684386477132335817313565433086716875969621692792589078208039947991285658575710753988343390698640741567466289492870574299077439300723653311639/338876005365062639446949098363097677261749088954756960367291504595423767758771879546789441239674233394354784715560577522051537808702672288664428995270933931427448620537737041464009819667700126461407068588110493128509643286457749297745100800*y^15 + 84770269146124004063247591340969586116838521306357670051879104060982180739600484220136045776602242691506371692801575712272122344556901161991147415367583083357473233432983139975028520416444081569292083755038021902044089827736343748374490239/338876005365062639446949098363097677261749088954756960367291504595423767758771879546789441239674233394354784715560577522051537808702672288664428995270933931427448620537737041464009819667700126461407068588110493128509643286457749297745100800*y^14 + 37480025641646348565712473271406014772517691248960249763569673728366852577643365013903960104675532901639378721362657519687814262103093417636739448866216226466676628654079504598550078736258880196410802587757239322134801130341397012300686151/18826444742503479969274949909060982070097171608597608909293972477523542653265104419266080068870790744130821373086698751225085433816815127148023833070607440634858256696540946748000545537094451470078170477117249618250535738136541627652505600*y^13 - 1832718759253545228323220336427737495007540417072405014098980076229834439625070780685906180559723509921988576631220048834852592986583785059933847039976496689313308026800890191829269298507706533508767982403211760933338224709274449421152440913/677752010730125278893898196726195354523498177909513920734583009190847535517543759093578882479348466788709569431121155044103075617405344577328857990541867862854897241075474082928019639335400252922814137176220986257019286572915498595490201600*y^12 - 3100113583744748356717393954111997141230759015098960012593810975631888035472753570838918816165787056204801717092090405082980718685346236517744196602729126055873549388154661158348809531547051002584456205909590774305736495330038085719471721/313774079041724666154582498484349701168286193476626815154899541292059044221085073654434667814513179068847022884778312520418090563613585452467063884510124010580970944942349112466675758951574191167969507951954160304175595635609027127541760*y^11 + 55545005163273024870080096122765871806503597195740259342383581280868513426595234463565314321744749163063349530803286297692231356884794087306978726414233072275687529254595267234064556858298384750271085191814368971650286853545354534649046627/5945193076580046306086826287071889074767527876399244918724412361323223995767927711347183179643407603409733065185273289860553294889520566467796999917033928621534186325223456867789645959082458358972053834879131458394906022569434198206054400*y^10 + 19064729861792934102188817823672128137525003990906248583434724372825660435770543095872274129043226818277942881223530099133015991530626848436357085687420740308878844612470818865070640309217508432082111579123353410721081647850840319981933265941/677752010730125278893898196726195354523498177909513920734583009190847535517543759093578882479348466788709569431121155044103075617405344577328857990541867862854897241075474082928019639335400252922814137176220986257019286572915498595490201600*y^9 - 2334623428253571032736344848954442911720915811282701217392587370918823174861837622860958058847669603156304476978870199755175208843039785207135056117714586612806861191233161499751508507094451221311177563854981093815849564032030144110965247757/135550402146025055778779639345239070904699635581902784146916601838169507103508751818715776495869693357741913886224231008820615123481068915465771598108373572570979448215094816585603927867080050584562827435244197251403857314583099719098040320*y^8 - 8324982040711379872954865015428127642517592892290263947469334904494211167578350627561006618207549715114861735283836875614096710054931522849653027714794604763990010385836853651932133819985618439919853554863873741992496733244114511355243071923/169438002682531319723474549181548838630874544477378480183645752297711883879385939773394720619837116697177392357780288761025768904351336144332214497635466965713724310268868520732004909833850063230703534294055246564254821643228874648872550400*y^7 + 3883294344885095492622065303808143933381735434397949001897580200045773791276676548302199121918279455611436792480374351858813639162289075980489905971824252539670210910368783978012507016585562649810305879779849701495302381308800761462637280737/225917336910041759631299398908731784841166059303171306911527669730282511839181253031192960826449488929569856477040385014701025205801781525776285996847289287618299080358491360976006546445133417640938045725406995419006428857638499531830067200*y^6 + 37235753526925773411713254464939337344489312781469388677635448100305585911205935506894983942446386810992993705078540040987081752683680258935948509643445327866133098044378199764801041688423095388822414058340583332935984305989185448961659281489/677752010730125278893898196726195354523498177909513920734583009190847535517543759093578882479348466788709569431121155044103075617405344577328857990541867862854897241075474082928019639335400252922814137176220986257019286572915498595490201600*y^5 - 200556629228182427322522329906932812162444479718420485855576803732290864705318165641629139053193535944484382056605288369561647732722008358412961735419920393632221495356030939496088111719878389572238171860599789042011182287759867590581501573/17835579229740138918260478861215667224302583629197734756173237083969671987303783134041549538930222810229199195555819869581659884668561699403390999751101785864602558975670370603368937877247375076916161504637394375184718067708302594618163200*y^4 - 3498408698245590739043273549615769645273851832553817506981048550663133522729976040427678394199645629286060480135757688160457407547424008352663825412864756676877437301493669993729109703032465622421663598720867113196742176741799971718114586941/75305778970013919877099799636243928280388686434390435637175889910094170613060417677064320275483162976523285492346795004900341735267260508592095332282429762539433026786163786992002182148377805880312681908468998473002142952546166510610022400*y^3 + 2667680320838220064732723657349731032404261935020332210249015313726857761267671769922280327713919829845083493094610617770976230888685718143186573705590759350012549663507979938500393067501884784729058520463772771793921386835052460732646641649/135550402146025055778779639345239070904699635581902784146916601838169507103508751818715776495869693357741913886224231008820615123481068915465771598108373572570979448215094816585603927867080050584562827435244197251403857314583099719098040320*y^2 + 4308206562864463617343583270119022906992351527519548657733276561289636247400163356930203869682663336564528267104030865553538143434994968480618201010283024561438331451622880603532043111669700775326716418652637347359608628266257823001606888167/338876005365062639446949098363097677261749088954756960367291504595423767758771879546789441239674233394354784715560577522051537808702672288664428995270933931427448620537737041464009819667700126461407068588110493128509643286457749297745100800*y - 53674083581333072031683645018689248125899474398786581328581012314759475205655519959954130775106568936577111040225980847094925064201625956053944236454271591318268439122874053682062092683928036048778673401873875619597931353087327478887386951/6987134131238404937050496873465931489932970906283648667366835146297397273376739784469885386385035740089789375578568608702093563066034480178648020521050184153143270526551279205443501436447425287864063269857948311928033882195005140159692800