# Manifold: Census Knot K8_77 # Number of Tetrahedra: 8 # Number Field x^26 + 10*x^25 - 22*x^24 - 498*x^23 - 1904*x^22 - 1778*x^21 + 6811*x^20 + 19675*x^19 + 3771*x^18 - 47691*x^17 - 46941*x^16 + 45125*x^15 + 82673*x^14 - 5837*x^13 - 65837*x^12 - 21805*x^11 + 24796*x^10 + 18138*x^9 - 2958*x^8 - 6276*x^7 - 559*x^6 + 1000*x^5 + 189*x^4 - 67*x^3 - 39*x^2 + 13*x - 1 # Approximate Field Generator -0.815687937924159 + 0.178571757617088*I # Shape Parameters 15734420174984264458820690057803149220713623928/480587315325858177266361782446681347234087665*y^25 + 161865147674012122616442293635447846397871693104/480587315325858177266361782446681347234087665*y^24 - 299740536184689886488098043276695662155134007574/480587315325858177266361782446681347234087665*y^23 - 7922876873086509542319550653150643589027993532506/480587315325858177266361782446681347234087665*y^22 - 6446759661579116501406053686858986365267306306052/96117463065171635453272356489336269446817533*y^21 - 37190493639572834882326196754200448780393390560299/480587315325858177266361782446681347234087665*y^20 + 96703795676652643415200251964452940311646445749061/480587315325858177266361782446681347234087665*y^19 + 337739260042593108048301488806284543007373891475053/480587315325858177266361782446681347234087665*y^18 + 156084027033535581515398363709583046352718200271122/480587315325858177266361782446681347234087665*y^17 - 707732804939595164272509059891718874667948843586982/480587315325858177266361782446681347234087665*y^16 - 944429378204861466784509488006825506047558168679864/480587315325858177266361782446681347234087665*y^15 + 441030256680476106802237225282951031458279524218863/480587315325858177266361782446681347234087665*y^14 + 1434771981194077023928776421932128200298015015975923/480587315325858177266361782446681347234087665*y^13 + 322928381174015728043307592159783419514306116709453/480587315325858177266361782446681347234087665*y^12 - 949787074718429883377461884739129276289884340632707/480587315325858177266361782446681347234087665*y^11 - 622492056480411837816567298825733678450010882368981/480587315325858177266361782446681347234087665*y^10 + 42479244681822750721625622434463062117467049631315/96117463065171635453272356489336269446817533*y^9 + 350749453287946526135687238215979538983398294264149/480587315325858177266361782446681347234087665*y^8 + 55865691374129384728441590928209933882531377480573/480587315325858177266361782446681347234087665*y^7 - 83609103342985219810726716429780958750269137233489/480587315325858177266361782446681347234087665*y^6 - 33683127588866400830772175239649729696295362496419/480587315325858177266361782446681347234087665*y^5 + 5982731674179048844028663282500637920677943696453/480587315325858177266361782446681347234087665*y^4 + 4817159002521736181873796325388879203013208244091/480587315325858177266361782446681347234087665*y^3 + 362070898346825853481211661146515659615583432902/480587315325858177266361782446681347234087665*y^2 - 515266410724156787347787092112890565365837451851/480587315325858177266361782446681347234087665*y + 52747208846185541753941723489705482010294850996/480587315325858177266361782446681347234087665 -557124508690902431063792540098157959937536825/96117463065171635453272356489336269446817533*y^25 - 5742579521143165159728411874041300556689898078/96117463065171635453272356489336269446817533*y^24 + 10429403956000909357919453936516597657844656947/96117463065171635453272356489336269446817533*y^23 + 279978048418229796524421068582934936559986082572/96117463065171635453272356489336269446817533*y^22 + 1147517249242472282392396727320319804116007883417/96117463065171635453272356489336269446817533*y^21 + 1374810149135721737982848168226121968811291291651/96117463065171635453272356489336269446817533*y^20 - 3222276828001288982834981487959297682503595814997/96117463065171635453272356489336269446817533*y^19 - 11692621530960656809952514468082178746628736767265/96117463065171635453272356489336269446817533*y^18 - 5871345655188719766485458596428726674370908709639/96117463065171635453272356489336269446817533*y^17 + 23322495659740383019203459660346574725947059270647/96117463065171635453272356489336269446817533*y^16 + 31613299354735842007806421330137902496042284664076/96117463065171635453272356489336269446817533*y^15 - 14001665068608975290734759588012292697761990278705/96117463065171635453272356489336269446817533*y^14 - 45651373646882226489190393192508881437400973696610/96117463065171635453272356489336269446817533*y^13 - 8888368944521868308736786126952693869591794423262/96117463065171635453272356489336269446817533*y^12 + 29906141190843861116793071687218881833252542170260/96117463065171635453272356489336269446817533*y^11 + 17074345435463638206436391519397412595608336330823/96117463065171635453272356489336269446817533*y^10 - 8162675090783903818210963091113850363906984876765/96117463065171635453272356489336269446817533*y^9 - 9983612876102269425588971297930988630386854771232/96117463065171635453272356489336269446817533*y^8 - 298062538066855794432468746937388876089955502659/96117463065171635453272356489336269446817533*y^7 + 2924516339287377669711784917219055099423427344745/96117463065171635453272356489336269446817533*y^6 + 680406511889605048889849358888220447814448056635/96117463065171635453272356489336269446817533*y^5 - 410224061085141846521901526400873134538482873982/96117463065171635453272356489336269446817533*y^4 - 159018759407086424397311895161675066594779424308/96117463065171635453272356489336269446817533*y^3 + 10335685629557833321974661764527591423347325119/96117463065171635453272356489336269446817533*y^2 + 21831908760936400327840781349123835937344048734/96117463065171635453272356489336269446817533*y - 2923025878698389783481172585219725590787519606/96117463065171635453272356489336269446817533 1818835403108723725289702662657936124061159592/96117463065171635453272356489336269446817533*y^25 + 18781857901170037725896088578388666678100802488/96117463065171635453272356489336269446817533*y^24 - 33870001620158256034662546337878833558637608046/96117463065171635453272356489336269446817533*y^23 - 916651531053016393118120692047765105496325166012/96117463065171635453272356489336269446817533*y^22 - 3762263610066355778485414817500663187931763037958/96117463065171635453272356489336269446817533*y^21 - 4469693243832647183437871120393846120129720705118/96117463065171635453272356489336269446817533*y^20 + 10887648225416954557322818755686109383792348352357/96117463065171635453272356489336269446817533*y^19 + 39256112619528163916675337171321619852933550372791/96117463065171635453272356489336269446817533*y^18 + 19691133133283065665504732126525446113308907305774/96117463065171635453272356489336269446817533*y^17 - 79914811796112506128817904687145686895765229366667/96117463065171635453272356489336269446817533*y^16 - 110865454790586119871210780421543314253234733790191/96117463065171635453272356489336269446817533*y^15 + 45653945212902082126837484948825979596190808534324/96117463065171635453272356489336269446817533*y^14 + 163834234406148904825258616815157311873544725585135/96117463065171635453272356489336269446817533*y^13 + 41938220458751076459828587190784753362189646658128/96117463065171635453272356489336269446817533*y^12 - 105035075503629720503180679724176350587582630809764/96117463065171635453272356489336269446817533*y^11 - 72404393608296266456396564483289590615223574851232/96117463065171635453272356489336269446817533*y^10 + 21629890884937164506599311143955372233412109200854/96117463065171635453272356489336269446817533*y^9 + 39241979812813829027183978574520480493275640969264/96117463065171635453272356489336269446817533*y^8 + 6937888656252901638805541953683633166288597722359/96117463065171635453272356489336269446817533*y^7 - 9073975403380883982337723400684324052061633567700/96117463065171635453272356489336269446817533*y^6 - 3794966487653113704870750614454822690444461620338/96117463065171635453272356489336269446817533*y^5 + 626452619667366470720601535967826942406425624016/96117463065171635453272356489336269446817533*y^4 + 530448532594467805389010022846514231339734287389/96117463065171635453272356489336269446817533*y^3 + 42245442800498071173616690226099614877750849814/96117463065171635453272356489336269446817533*y^2 - 57268775818278379328421535813199521252190881741/96117463065171635453272356489336269446817533*y + 5789036518268253251474524502905552536391774387/96117463065171635453272356489336269446817533 417005600298643536925408441401737874332423667816/9131158991191305368060873866486945597447665635*y^25 + 4297404385435801692794187239352518350884562137938/9131158991191305368060873866486945597447665635*y^24 - 7862901735387272485799209846309255506475159429518/9131158991191305368060873866486945597447665635*y^23 - 11056992624020912410111626938653470513590311057748/480587315325858177266361782446681347234087665*y^22 - 171624888994044607970457005542363900981674340081624/1826231798238261073612174773297389119489533127*y^21 - 52784649773160932615692761452803868320332843138747/480587315325858177266361782446681347234087665*y^20 + 2536812409572772412414197442694242540844036932356007/9131158991191305368060873866486945597447665635*y^19 + 8984522396052073572303540660262037151066379349552541/9131158991191305368060873866486945597447665635*y^18 + 4313939322422659707727695935813534457458561545592609/9131158991191305368060873866486945597447665635*y^17 - 18596349113968894863602299464518949666267689222209869/9131158991191305368060873866486945597447665635*y^16 - 1330963538949601724812583041105298644895778128521357/480587315325858177266361782446681347234087665*y^15 + 584959835118374890610103281291719288777578286493204/480587315325858177266361782446681347234087665*y^14 + 37953301114528400537487706886713419605102606164917456/9131158991191305368060873866486945597447665635*y^13 + 9200545554780421662934346638674205421942315234761436/9131158991191305368060873866486945597447665635*y^12 - 24704545157808605114961402909426837074281438066412579/9131158991191305368060873866486945597447665635*y^11 - 879651008495468256998461537019724300521534752142818/480587315325858177266361782446681347234087665*y^10 + 1046308285739799173410440283681213806542404647826906/1826231798238261073612174773297389119489533127*y^9 + 9199256589953588467418791177003045760714745767422568/9131158991191305368060873866486945597447665635*y^8 + 1596867565249714196146867829627060082604385149250311/9131158991191305368060873866486945597447665635*y^7 - 2133122386401309882197497366986948728493851313024913/9131158991191305368060873866486945597447665635*y^6 - 891765493706445054814875824022278701901957011168268/9131158991191305368060873866486945597447665635*y^5 + 143122577972180924506416502542962079835707895549036/9131158991191305368060873866486945597447665635*y^4 + 123136394248681867265545966717537383512370349856352/9131158991191305368060873866486945597447665635*y^3 + 9925651547725750161803536152244353116984933281934/9131158991191305368060873866486945597447665635*y^2 - 13238263018871881205981611489188746196851193341592/9131158991191305368060873866486945597447665635*y + 1355457182438919772574511667047912071097128976577/9131158991191305368060873866486945597447665635 -7325579930992582300517920115421315197262213932/1057292093716887989985995921382698963914992863*y^25 - 6771389414468215822916910345218817333712573759/96117463065171635453272356489336269446817533*y^24 + 13521713356157279701287346865763610965256151852/96117463065171635453272356489336269446817533*y^23 + 3673945885952834972404448994887757256898094218481/1057292093716887989985995921382698963914992863*y^22 + 14563552179999030249021852582755389135852154036558/1057292093716887989985995921382698963914992863*y^21 + 1402672463124490644578685409193547142418864844484/96117463065171635453272356489336269446817533*y^20 - 47487537503137894657177897502737077144231143412451/1057292093716887989985995921382698963914992863*y^19 - 152386492199812401502003069236044783545794306849889/1057292093716887989985995921382698963914992863*y^18 - 52866687325600902648305416995720741492416974928571/1057292093716887989985995921382698963914992863*y^17 + 342373705766280623979679317312107446820616728482066/1057292093716887989985995921382698963914992863*y^16 + 403088275312445898003162054072641203362536056241814/1057292093716887989985995921382698963914992863*y^15 - 24152355233529405181784236717107317699287364796470/96117463065171635453272356489336269446817533*y^14 - 656434266571498679993654159504040923102489488781500/1057292093716887989985995921382698963914992863*y^13 - 67958201865232564967646067588906411380429617141975/1057292093716887989985995921382698963914992863*y^12 + 478236823918329122922391664549120680979779020437148/1057292093716887989985995921382698963914992863*y^11 + 244763443208931150036287765944922583101628644915083/1057292093716887989985995921382698963914992863*y^10 - 143802234505179217762249819477140099737574046966604/1057292093716887989985995921382698963914992863*y^9 - 161557270162129404966158413293666374105226287035563/1057292093716887989985995921382698963914992863*y^8 - 5897079754350997478633538363806203151440576011078/1057292093716887989985995921382698963914992863*y^7 + 46736847761235695540886052944314310987863864303467/1057292093716887989985995921382698963914992863*y^6 + 12814721060137354055917949586212041937031193716637/1057292093716887989985995921382698963914992863*y^5 - 5366317577847297220075824548710230166561841937507/1057292093716887989985995921382698963914992863*y^4 - 2534095540342677779165738044433161822896835251029/1057292093716887989985995921382698963914992863*y^3 + 27687431181916308075143229284247360907956492420/1057292093716887989985995921382698963914992863*y^2 + 308285182738870932320138125548080125998264869719/1057292093716887989985995921382698963914992863*y - 35135977429312408812909097464060892404847659842/1057292093716887989985995921382698963914992863 -2282092361960854742908184994944573905403497839/96117463065171635453272356489336269446817533*y^25 - 23474833369632024019469383714484558391266789712/96117463065171635453272356489336269446817533*y^24 + 43473162136976968868090332091215361073973532136/96117463065171635453272356489336269446817533*y^23 + 1148872447674527505744313782645792786692294800506/96117463065171635453272356489336269446817533*y^22 + 4674416463284382195079269106494033798243755705555/96117463065171635453272356489336269446817533*y^21 + 5400178281039852309543672889419125088366083135672/96117463065171635453272356489336269446817533*y^20 - 13982584868181597566812741928559153475931164654495/96117463065171635453272356489336269446817533*y^19 - 48889694638484086333141145360597605627277341666676/96117463065171635453272356489336269446817533*y^18 - 22648706448120817156552167375601195553154043092435/96117463065171635453272356489336269446817533*y^17 + 102211360717395660225027951130834383024703175666593/96117463065171635453272356489336269446817533*y^16 + 136330069708913497210152352682068830930540507699942/96117463065171635453272356489336269446817533*y^15 - 63672064219173122672823238500280566566365674416872/96117463065171635453272356489336269446817533*y^14 - 206541994984479962150639215542089502305485992376415/96117463065171635453272356489336269446817533*y^13 - 45958542521348634536900484279259995238980954052691/96117463065171635453272356489336269446817533*y^12 + 136596908456517411580481462103030039428565629370319/96117463065171635453272356489336269446817533*y^11 + 88740441691352545048950010540940086939158318914521/96117463065171635453272356489336269446817533*y^10 - 30899827558510475755927387050688973826164209606642/96117463065171635453272356489336269446817533*y^9 - 50044207725193736499867853552099758511615135728638/96117463065171635453272356489336269446817533*y^8 - 7623017845283313050025316532993323353659281171371/96117463065171635453272356489336269446817533*y^7 + 12047439852933627511921482234772161396191397700587/96117463065171635453272356489336269446817533*y^6 + 4708022072560684702386494103550538888548790279463/96117463065171635453272356489336269446817533*y^5 - 915607407522697786933981639364726150676982600808/96117463065171635453272356489336269446817533*y^4 - 686410445498655839239826537710885664214644125175/96117463065171635453272356489336269446817533*y^3 - 44641432422092834199280934925004555053614148475/96117463065171635453272356489336269446817533*y^2 + 75451416338458604248591494759440900684898623212/96117463065171635453272356489336269446817533*y - 8120694244217240532969567571700863595328415691/96117463065171635453272356489336269446817533 -1608395487954634488790616322543233805889225052/96117463065171635453272356489336269446817533*y^25 - 16538978371845912739873138399814514687795642480/96117463065171635453272356489336269446817533*y^24 + 30702547232192054420917709821625890685382954492/96117463065171635453272356489336269446817533*y^23 + 809634311771477289793727844771512542909309549148/96117463065171635453272356489336269446817533*y^22 + 3291498423112933191961115386535024286476444747583/96117463065171635453272356489336269446817533*y^21 + 3792512270059653721241651647207342668173772310161/96117463065171635453272356489336269446817533*y^20 - 9875457537229153000523535456312603133411040326463/96117463065171635453272356489336269446817533*y^19 - 34432071859347187340595247598870453525722553466176/96117463065171635453272356489336269446817533*y^18 - 15826940172871609335619391750742129908000524102629/96117463065171635453272356489336269446817533*y^17 + 72160445051939957726491062286909366841408394326199/96117463065171635453272356489336269446817533*y^16 + 95887384512120428865357354561024576012306678059724/96117463065171635453272356489336269446817533*y^15 - 45302388214773820238353745514451035302952420891982/96117463065171635453272356489336269446817533*y^14 - 145597645579556461622024073769823298436838533870550/96117463065171635453272356489336269446817533*y^13 - 31900791340746226791926520985431066976954757372632/96117463065171635453272356489336269446817533*y^12 + 96569078554713191358940656292830006759916598802258/96117463065171635453272356489336269446817533*y^11 + 62321360452442469296193162346846783626264274986791/96117463065171635453272356489336269446817533*y^10 - 22056039318677809421631311214988900582886774705811/96117463065171635453272356489336269446817533*y^9 - 35272933735258627141129681610846795750523606455889/96117463065171635453272356489336269446817533*y^8 - 5255065167902968487567628218409538778040852266182/96117463065171635453272356489336269446817533*y^7 + 8530610065100552770776318925761010072984815273620/96117463065171635453272356489336269446817533*y^6 + 3293123255918786334023331948217728047179996875969/96117463065171635453272356489336269446817533*y^5 - 660988390664545055189338320152995856416249490837/96117463065171635453272356489336269446817533*y^4 - 481603772889221430683480301568042614822478250132/96117463065171635453272356489336269446817533*y^3 - 28544560287165065318830820846292937807973326052/96117463065171635453272356489336269446817533*y^2 + 53166387105073695807439996312091770855141811528/96117463065171635453272356489336269446817533*y - 6138481490961531691838836390754444665298939640/96117463065171635453272356489336269446817533 -10444248687434924376688220711771933113848973786/96117463065171635453272356489336269446817533*y^25 - 107319775571316141056724548058803722874082715407/96117463065171635453272356489336269446817533*y^24 + 200190747912053547945906656161836945092397849702/96117463065171635453272356489336269446817533*y^23 + 5256208557839501826426897136398101376054417054813/96117463065171635453272356489336269446817533*y^22 + 21334195260575531647525502552563744290939353186002/96117463065171635453272356489336269446817533*y^21 + 24455877669840207885071502080075235467393909833383/96117463065171635453272356489336269446817533*y^20 - 64362573687272925707829484506597659512603846477304/96117463065171635453272356489336269446817533*y^19 - 223177322594496089899149068551451408508613565952022/96117463065171635453272356489336269446817533*y^18 - 100964992831663275703576468156815574584211144501882/96117463065171635453272356489336269446817533*y^17 + 469914202870121592442572011382650331349062655117302/96117463065171635453272356489336269446817533*y^16 + 619511046291440635430447423091474766613741958348166/96117463065171635453272356489336269446817533*y^15 - 299925820834418129728271150272955321060282276899553/96117463065171635453272356489336269446817533*y^14 - 945044743861794751286816549392092632880499998238838/96117463065171635453272356489336269446817533*y^13 - 199708761582455205094092273891720561847583941901980/96117463065171635453272356489336269446817533*y^12 + 631165292035480619477608803613939240097034775802710/96117463065171635453272356489336269446817533*y^11 + 401157186034556990654118976056795022209200129730885/96117463065171635453272356489336269446817533*y^10 - 147624695746797230834053862389470537936163706388194/96117463065171635453272356489336269446817533*y^9 - 229459543587024936904044970823054511404513397153829/96117463065171635453272356489336269446817533*y^8 - 32443918768206486164842160535984103628785151820970/96117463065171635453272356489336269446817533*y^7 + 56298078928309768920285528357222608431938305321390/96117463065171635453272356489336269446817533*y^6 + 21274699452850293685276257632828895808866381014417/96117463065171635453272356489336269446817533*y^5 - 4522197805057695651132133234985534266600780101915/96117463065171635453272356489336269446817533*y^4 - 3189751466480066996842153520578384622663853081433/96117463065171635453272356489336269446817533*y^3 - 181154187153938796414836084295239255994792242464/96117463065171635453272356489336269446817533*y^2 + 354165056414066203505972361703753855013094089482/96117463065171635453272356489336269446817533*y - 38694370067597569399609626315013771246805128735/96117463065171635453272356489336269446817533 # A Gluing Matrix {{0,2,0,2,4,0,-2,1},{2,0,0,0,0,0,0,0},{0,0,1,2,4,0,-2,1},{2,0,2,2,4,0,-2,1},{2,0,2,2,5,-1,-2,2},{0,0,0,0,-1,0,0,0},{0,0,0,0,2,0,-1,0},{2,0,2,2,6,0,-2,1}} # B Gluing Matrix {{1,0,0,0,0,0,0,3},{0,1,0,0,0,0,0,0},{0,0,1,0,0,0,0,3},{0,0,0,1,0,0,0,3},{0,0,0,0,1,0,0,4},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,1,2},{0,0,0,0,0,0,0,5}} # nu Gluing Vector {3, 2, 2, 5, 5, 0, 1, 5} # f Combinatorial flattening {0, 3, 3, -4, 0, 5, -1, 5} # f' Combinatorial flattening {-2, 2, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 151494728071473670061637555930731963775415491450/96117463065171635453272356489336269446817533*y^25 + 1554939752755344554720655200422997480117597604887/96117463065171635453272356489336269446817533*y^24 - 2922446667053817247013085139109180879855866690685/96117463065171635453272356489336269446817533*y^23 - 76216269789229674591492999744300622823291142229338/96117463065171635453272356489336269446817533*y^22 - 308564594923004597094586334278295437254438316632084/96117463065171635453272356489336269446817533*y^21 - 350792589666450079734643329375035343709808496727391/96117463065171635453272356489336269446817533*y^20 + 939292325188117105034209176476361429992519279894044/96117463065171635453272356489336269446817533*y^19 + 3228614447547387929532190470603299130509302203743180/96117463065171635453272356489336269446817533*y^18 + 1423175297293638357744507974337446294492949501065954/96117463065171635453272356489336269446817533*y^17 - 6849915594910010221243975970006191425911660461398840/96117463065171635453272356489336269446817533*y^16 - 8918884349611269606406187634755529837344930854577136/96117463065171635453272356489336269446817533*y^15 + 4484502037732801773261815747561525335432936702058804/96117463065171635453272356489336269446817533*y^14 + 13708940981407455921375110176908115719813498216226359/96117463065171635453272356489336269446817533*y^13 + 2730033128067776904892862642256617068715534233880125/96117463065171635453272356489336269446817533*y^12 - 9256620718126181392389888647262682250985050151511955/96117463065171635453272356489336269446817533*y^11 - 5743454981341654366352840786884348896419061542681974/96117463065171635453272356489336269446817533*y^10 + 2244645321953801102916150386679323879576658759756726/96117463065171635453272356489336269446817533*y^9 + 3339857500545234228196544356123435360176204749130069/96117463065171635453272356489336269446817533*y^8 + 431001598296719028999444379609357685728339945444867/96117463065171635453272356489336269446817533*y^7 - 837837141540349453889102604353819558060797219466342/96117463065171635453272356489336269446817533*y^6 - 305232428806706939123213023902893808283915920258460/96117463065171635453272356489336269446817533*y^5 + 71389240229906845922159278882082495433090544440248/96117463065171635453272356489336269446817533*y^4 + 47466882936283420747913638509641669519621176562086/96117463065171635453272356489336269446817533*y^3 + 2299807522151012212083867849321477570392275007055/96117463065171635453272356489336269446817533*y^2 - 5321762400820837174079069116712725285660221426753/96117463065171635453272356489336269446817533*y + 569235407437806824677948485775897200789453306426/96117463065171635453272356489336269446817533 # 2 Loop Invariant -4741501885886869950391972990494484903373059153248944361170159754529183556250282436728354997415761761765817682460712232498678349859/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984*y^25 - 8117455311687423198864110668440630512786277300304306172857710790089817205790561760458650410281822754452691045639744414068264048331/451627553735469656326488854107639153739824739162853317237871351383300598213074998861116589118869763211940865652180783494251282664*y^24 + 15174461116679898607734959891711084542048026893183281193601909040154875665375693133212140787533005309817736415284098446310382799675/451627553735469656326488854107639153739824739162853317237871351383300598213074998861116589118869763211940865652180783494251282664*y^23 + 596461335360657372681214291738364263436080238687550359676036724223760357395511536802606771771576990292778835648921526426177044660509/677441330603204484489733281161458730609737108744279975856807027074950897319612498291674883678304644817911298478271175241376923996*y^22 + 9677132625403798918595947011502467907163750557066955436032212609733551948187887299647449176276066101278062748037307844789665212386001/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984*y^21 + 5535882321787252022506776682487226914261774512435549816616162781370439906371279694346839342185474602004981760515636844984621567509613/1354882661206408968979466562322917461219474217488559951713614054149901794639224996583349767356609289635822596956542350482753847992*y^20 - 29245509290650254508733694267280747498870037762589392238460646609251843004529695823439375682082315634271694905951072832671061252382819/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984*y^19 - 8433235509789704461604442455761415023176130274283211717042680438802236158577586125531617984158831376665088002401071872853949825432629/225813776867734828163244427053819576869912369581426658618935675691650299106537499430558294559434881605970432826090391747125641332*y^18 - 45507224010780723651923306860358017491394856133355005912443355407533655299728469821457004072785142677293747086260471201650075318020275/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984*y^17 + 71125922379022628906150368259562202304814229607390928928123531975737599520252928770925386775636006021437739599531258421174690222197507/903255107470939312652977708215278307479649478325706634475742702766601196426149997722233178237739526423881731304361566988502565328*y^16 + 46735086320716630710462616571515113909627383234989069784194432066624502602171597934522188717855141692613210848672582713483058638481161/451627553735469656326488854107639153739824739162853317237871351383300598213074998861116589118869763211940865652180783494251282664*y^15 - 22831765030800924062668216654716016309719185619153179910220689018783046571760907873179674477525915412355383585456373489777758990763919/451627553735469656326488854107639153739824739162853317237871351383300598213074998861116589118869763211940865652180783494251282664*y^14 - 428272195487505775758950822512486657743811030013435498641156315906078823515071100138494806911150413841674844320553876202655258130360559/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984*y^13 - 89143925832641365390514815499579849846634394451205489689972506482846585222626494192926509381027451454919349900965743276342986770116561/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984*y^12 + 95539040479020066929557662199993698665815755464540481081524612274823229753084101303752093670058129117065222965365462657711354263278945/903255107470939312652977708215278307479649478325706634475742702766601196426149997722233178237739526423881731304361566988502565328*y^11 + 60324147869466846690459711795130447749045164497429484232226152621863078664386930495044784018794261745232574513035218205114014646963715/903255107470939312652977708215278307479649478325706634475742702766601196426149997722233178237739526423881731304361566988502565328*y^10 - 4226964595957439814177410734057471523487278131190464699140475132272507486379300289643012876179624961521767251062373326660221847594167/169360332650801121122433320290364682652434277186069993964201756768737724329903124572918720919576161204477824619567793810344230999*y^9 - 17313277872315883340913301943600909591708342153670726848180674052390426832218167188611720240226012983398645888093912409017901143406073/451627553735469656326488854107639153739824739162853317237871351383300598213074998861116589118869763211940865652180783494251282664*y^8 - 4776639886584682658593416550889813981253376378823760898139735862139800194641371554811367064419045347412494031134341953686263172016663/903255107470939312652977708215278307479649478325706634475742702766601196426149997722233178237739526423881731304361566988502565328*y^7 + 8541862964183671951746915410939706295360568151090828022859905269367696798490594164619621935671964526015089440301828635266927000485645/903255107470939312652977708215278307479649478325706634475742702766601196426149997722233178237739526423881731304361566988502565328*y^6 + 9571748570653501387805405671755993212082129760474155534681244997304747731175027532717436240582557354458991310596070732256657239725423/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984*y^5 - 348939933403499208449042732643423592477552522691812253265191090585660937929231874403616747099274376229249615161487594663545452577119/451627553735469656326488854107639153739824739162853317237871351383300598213074998861116589118869763211940865652180783494251282664*y^4 - 482580962623759109872160796932915472451823070500397433683987274904400639586602760018232050034749162445713416696791712397516484612813/903255107470939312652977708215278307479649478325706634475742702766601196426149997722233178237739526423881731304361566988502565328*y^3 - 26097687095426629379983049848306475970124704926380820683659399465702404036243186507259358428209045996659893586472837876446963328733/903255107470939312652977708215278307479649478325706634475742702766601196426149997722233178237739526423881731304361566988502565328*y^2 + 26971276322704949907732862041530188646422664378617684326164425124939032873750282544051290802569480116577458761042622555035598310255/451627553735469656326488854107639153739824739162853317237871351383300598213074998861116589118869763211940865652180783494251282664*y - 20497313923144770604193827765572388514808558834037075689773723080445294026471256805845718555716888814888603001994850489347041170865/2709765322412817937958933124645834922438948434977119903427228108299803589278449993166699534713218579271645193913084700965507695984 # 3 Loop Invariant 1140261083644245543939342046759870591518572491477002934395698215706489070131678868091656168457435884589032371452743579236829482773895558407747695065518410807813920435276347/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^25 + 366717656503923608016837022337209437189510180909272555869163871611983565147202085259398475372286312960793024658049702960106087906935840980490648322972939417334721008862003/86529563099745751843071721474327820845919139380292866939568909111553619804196547740889300365734267705820134494867655583901681385211373605085557266172387763089839539226534*y^24 - 21662921521149326569531769960301477015085765469011067772946884498202255273434689527961856470069333248273594372491171345517637898327697995242829093313946857954176308448835215/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^23 - 71767854321263442059363152041696518491399070374104636254007082662150472627271414377917488252449269057816095736746782915240415260722809847120535518429608455146935918839432087/346118252398983007372286885897311283383676557521171467758275636446214479216786190963557201462937070823280537979470622335606725540845494420342229064689551052359358156906136*y^22 - 73077581439184671786144791633341188331453636399524460185469721055922230768031189137091619619450180808182505061898617507497439821474454952892225488115751248052234767655105963/86529563099745751843071721474327820845919139380292866939568909111553619804196547740889300365734267705820134494867655583901681385211373605085557266172387763089839539226534*y^21 - 1355055436284515167456532301455846927334072421223383885755124616832306318064302519764249450203078629921818871431111720516166645062199022560455387976881425708298142861212221235/1384473009595932029489147543589245133534706230084685871033102545784857916867144763854228805851748283293122151917882489342426902163381977681368916258758204209437432627624544*y^20 + 6973123619325552651940050947996216817560192983401077484071091330702502589772726083279157897274148759385191857719791075113090219244333509569014882251254327232109314443692039515/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^19 + 12233661935452479510830403443853563032320202714026075452343304470834040238339342907125806658196670962995713350140123984524435061482361156677392934980903008535429347275542771361/1384473009595932029489147543589245133534706230084685871033102545784857916867144763854228805851748283293122151917882489342426902163381977681368916258758204209437432627624544*y^18 + 2862731109169156075300743845040679492351728479746731302391534779972460197088945546997981734279968796591570686243999351421335380027780499742063007124598643225660719988754682815/692236504797966014744573771794622566767353115042342935516551272892428958433572381927114402925874141646561075958941244671213451081690988840684458129379102104718716313812272*y^17 - 51012472324532833816564853079864628205274876223094972688846753489692908721302812878605854216430685017438744904034833977005035765587986693343860443929289651377663807904789482681/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^16 - 68425117243960841923620708455936464728364921858115284348548065228275572903233421370203552488942950169474658004829282543731245351522598402839530553769364069999134968405457945921/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^15 + 15699289642931004963543800744046984066308881698081074097485237948024640352219233024878031931124227710000389565663251525741450607773623620740795138941779505868991691454682956593/1384473009595932029489147543589245133534706230084685871033102545784857916867144763854228805851748283293122151917882489342426902163381977681368916258758204209437432627624544*y^14 + 103404336030825220951734742226029305185037973333180420190653019295423283929527192598246757330104082205227691383727719721138841164354450354648107745856340084329896419582845515073/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^13 + 23654234114689012773662878323842782063318669077532796733766906206697672140628252245971941139805969487909785503879998860418678072265190733653203469796559152939976388786398884865/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^12 - 68069489531547197489396116248138178898608790550330952530063252941305895542488644304226699717604452164547574435327709337477108940446703237314300429853859229431286676518337468773/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^11 - 44817595637207928807137737823343986946244318111414960914732979270359282676834397483824268497573815148060983808287381270956453381062260125091696235229468593715263365175837018879/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^10 + 3769804294127085420531059137240189308384464451156159041940265902617734148534443598246367733849632197224360171978143592834749894089270518649275684391036192445586884544813376919/692236504797966014744573771794622566767353115042342935516551272892428958433572381927114402925874141646561075958941244671213451081690988840684458129379102104718716313812272*y^9 + 3135983833238573896206477810817331412367293269312284734360121069442815400480040792337296858560598330540600355304006048044775182601609195118171688080524160679161399945966638577/346118252398983007372286885897311283383676557521171467758275636446214479216786190963557201462937070823280537979470622335606725540845494420342229064689551052359358156906136*y^8 + 1002528544842429777922899396292685470834941765550303929516613386882848085770356193141256380630813655601513363710181999362071288666888795624866426648863833820774159488054403547/692236504797966014744573771794622566767353115042342935516551272892428958433572381927114402925874141646561075958941244671213451081690988840684458129379102104718716313812272*y^7 - 5962624735425149598729939735412615357198200064175381810588873749644193118932125581969656276829402176411595022064198546430374242652095541991085797669853173005852286615453277415/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^6 - 2390196904908123945343345906838815937207241982940299924492385113580736861700265902510114927632261938803923206406967361671498499711050457457622063990537590099976891565977960619/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^5 + 432794692857607692903757724384424047281586664608122079495854150174987941455216880238230640562972884307123413436158928547527427656924865716727575944405306150703823435293413927/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088*y^4 + 170790218770490241401450121901501409457786391786037232682401018483200685716917508171130648705327981514979651116533348365977744412268150378964581711145810240587300776952508701/1384473009595932029489147543589245133534706230084685871033102545784857916867144763854228805851748283293122151917882489342426902163381977681368916258758204209437432627624544*y^3 + 1525106712476035320719240564824814418501541123308551383219646997904116394373469032004883874938843819734528739663812230412810078208019998542685122614465970503105884399980789/173059126199491503686143442948655641691838278760585733879137818223107239608393095481778600731468535411640268989735311167803362770422747210171114532344775526179679078453068*y^2 - 18534059027521581060053474847649816482222402096584715416937196061190488122271652268184499926866429647535500636112620977011113283521406130950576052172739666921942738498006177/1384473009595932029489147543589245133534706230084685871033102545784857916867144763854228805851748283293122151917882489342426902163381977681368916258758204209437432627624544*y + 3929000074384529916157339943976998132814157200348285355747425586899031672476562932560230962561126325217294923582073240432906122329150214720522015431921214541673481644781131/2768946019191864058978295087178490267069412460169371742066205091569715833734289527708457611703496566586244303835764978684853804326763955362737832517516408418874865255249088 # 4 Loop Invariant 1328101924712706242894296430147271959819148919286858059406104477338071932507480042444323864894080032413678194315520409746691994397616122503612103843121362914624353686366552236008800853171450697453205025535213192126451621110553296019099169966713312782851205/4878922143257966630056487094305509927964446875466515622933194811751259493077194179995237626141425241752597365987304928373548978213277869744838699005253500363817351622209331816371511327994909110408857627877671460101939280823110541525464628734673055033689664*y^25 + 273167687536480844640041226144303917310394040687859338211817356050394733747693077004823827707455906686581480856062983284274252520625754884426546876471314019046301020928995102970661415950435960580696945312921676796235587893598216329158325790382984766120357511/97578442865159332601129741886110198559288937509330312458663896235025189861543883599904752522828504835051947319746098567470979564265557394896773980105070007276347032444186636327430226559898182208177152557553429202038785616462210830509292574693461100673793280*y^24 - 135127087749388860687230689438838044086170850565728645941492924950014449813908178489077034322338461117445544585242429346738708206128868011037824866080232253717365824124710524876619198272627102029012848732820041925196047055291087668988390765108798118205523693/26020918097375822026967931169629386282477050002488083322310372329340050629745035626641267339420934622680519285265626284658927883804148638639139728028018668607025875318449769687314727082639515255513907348680914453877009497723256221469144686584922960179678208*y^23 - 10697464552214353630945021592015897335529876889731884012437095963099706738402645399954490489404548206704676059820132021818177820452881560243920671585620557601747443559236102297470973141569034534430189236183878314436093613933460078968871194294972230542865041321/78062754292127466080903793508888158847431150007464249966931116988020151889235106879923802018262803868041557855796878853976783651412445915917419184084056005821077625955349309061944181247918545766541722046042743361631028493169768664407434059754768880539034624*y^22 - 10195414413763710923644277734490679882738850469830234858620572924903309277011331729537847347229879402731097763134551836881607226869354349726024596010264033245606470343577798582548149968964019622711817303439910225049467063958462697334687989267954836316896375871/18295958037217374862711826603645662229866675782999433585999480544067223099039478174982141098030344656572240122452393481400808668299792011543145121269700626364315068583284994311393167479980909164033216104541267975382272303086664530720492357755023956376336240*y^21 - 37610030934435982253294898228308027963597121165139426761035130591796234923002969040451723332433844335906449278833220179891334099266326285154883707436504611475137851066410319926919648925718987928570468477085967496862397648804727563016055227096548340715510396787/58547065719095599560677845131666119135573362505598187475198337741015113916926330159942851513697102901031168391847659140482587738559334436938064388063042004365808219466511981796458135935938909324906291534532057521223271369877326498305575544816076660404275968*y^20 + 217519771951213112323003273845825770820918557275237064330250354400927689771775107759610771267397765271783634876768423115767027267323924181187630737698393813216431650170948424162367977600892710274510586845303270613165765313541591370777636827364412281446291837107/130104590486879110134839655848146931412385250012440416611551861646700253148725178133206336697104673113402596426328131423294639419020743193195698640140093343035129376592248848436573635413197576277569536743404572269385047488616281107345723432924614800898391040*y^19 + 6830235351171546305901470925160467673472544689851183888901431625561439463988525618852916355518013501781094221008348393879022185397818906334985671625584496477803227207407013706761133987058264200044556105802026130740742914138546928203188712392752348094322029756259/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^18 + 3146724596636258827816520878579406628676067868275704887869710417288353395405920833586320591484897141697086401816863730966270526543940048913867921520424693613796286496283063852511514521572977438120145974068604709153911509518859820945008936629119416047105751324039/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^17 - 4771156614113034598315612372729567940795469961586043776379618108203129452662652444022906179605095353190516717183187448834516221652502955709019772176683906233836098739304630112445377329577321938794838442130345667520104515474374715817571479153231004440230035251229/390313771460637330404518967544440794237155750037321249834655584940100759446175534399619010091314019340207789278984394269883918257062229579587095920420280029105388129776746545309720906239592728832708610230213716808155142465848843322037170298773844402695173120*y^16 - 19055804741353667101555980658256627940919013188248619543505565188054221345073716997301810624211981171203655622443937442410356333389894673196176444783172203807199358715652719224346099730888039655932198572252537127749811873194048953656718229980358474142379073898099/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^15 + 199020477311730036367966732695253939443007118132748771828805592987086885944817115786938433101071275850843037476751488458615787336892813561217193301364209995692533450340073925683631135412945261140549541838835824102415947364347622799186518622830047520005570720069/26020918097375822026967931169629386282477050002488083322310372329340050629745035626641267339420934622680519285265626284658927883804148638639139728028018668607025875318449769687314727082639515255513907348680914453877009497723256221469144686584922960179678208*y^14 + 7236173958726974511895111149206313103179590393041271320948361078729806330410934062930822040842289884545671892745305089532167312033181565338390312896439629349741518136167748878443647815474263991916660429676732266246476980228383617656250031406221247187877113136923/292735328595477997803389225658330595677866812527990937375991688705075569584631650799714257568485514505155841959238295702412938692796672184690321940315210021829041097332559908982290679679694546624531457672660287606116356849386632491527877724080383302021379840*y^13 + 35673957098938824385856408880336693690810978155615134938647943663792493039090777933783145292265147611854433099956195367795285284447142152285424235842403742755574765672646524825343898415728866643299744377583330383149303336826642238399469607483194576853751368839/6505229524343955506741982792407346570619262500622020830577593082335012657436258906660316834855233655670129821316406571164731970951037159659784932007004667151756468829612442421828681770659878813878476837170228613469252374430814055367286171646230740044919552*y^12 - 19185622557099304965318686885353099969018488210992040650509336627227650791710639152753202185190333528243896814534528594857910807122758387332057836358481550180340356251321971712673809731206141534781190881842999036475423543679788074719578162322723146037912105422343/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^11 - 12470130321745381268486008393895000902167090171360889423792593499877919132764693945794210118845338526579975209849988212536130102760214288762490983491231719493047381706541141399444585330611706702456673811676157312109000989209850740158140081289668968931009410102083/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^10 + 4342430681992647875455823902537758209851432020169976870461056946948567226254904207866165733896366768364046480175007373993641277686043155933870270692861386343865300826045545738020078947782385238407838607829836357408275957277253698604973273799387767686753184399951/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^9 + 7046361207408490901968707806374092185326431107642914902397520883425216447935662349985224574762709759853629857021147591438768340586228237200173814897263739536214343497747011669125430858269854252861925877212447760715258145529129263111581893711687500690458278986063/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^8 + 1083092801204858431431154561569564371506990213532463093498794777243613642608855669408949738428061953866368467367076022058364861142548751175014254508130233725864207114106781237465514264777847496222474689536477246239924845449465112292295625697341703322419146959679/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^7 - 1694066992669188041231842216005686687726362387766346044782030018340787169468266309114150712488735146066065567805130687476183601086710885831603174792042288010059652938664073328738114743124221879681121224387850001102745802841892705159459160215639699982754654016301/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y^6 - 133428539589568963762935096454378206803522755933703077727554969950835257793048157464609325368924207594249483025802884960059919929546325281866521444306581168399826434194573785391494355936536314730654664235683365047410245822913919728450927216796527482750936406737/234188262876382398242711380526664476542293450022392749900793350964060455667705320639771406054788411604124673567390636561930350954237337747752257552252168017463232877866047927185832543743755637299625166138128230084893085479509305993222302179264306641617103872*y^5 + 7049715214438366279709496747306805325132927796364016769079260387919402482722702868356394631711266197865248595253502718902916152621664688045187992604128963740853834108713877209925482666114780813578412954351914224956867060794715072818903290819148906736170872929/65052295243439555067419827924073465706192625006220208305775930823350126574362589066603168348552336556701298213164065711647319709510371596597849320070046671517564688296124424218286817706598788138784768371702286134692523744308140553672861716462307400449195520*y^4 + 6444794924760372486678897598653248231448428129971817851948442017036013594023556311233164967231877648526227253654127834605448048097814400940862572999574128878051353987134532066951408102466592263964084129488696105210443189437780584366829079688592153484041813549/78062754292127466080903793508888158847431150007464249966931116988020151889235106879923802018262803868041557855796878853976783651412445915917419184084056005821077625955349309061944181247918545766541722046042743361631028493169768664407434059754768880539034624*y^3 + 35887767550764535226638094343511166772233274567101633038366218705840161143924183586263213885257844923890816976255734328399457875435607277897994304911562343721389065925858245273669883622232368394633840047259028733283662653929282563256795386628746890294730763/6505229524343955506741982792407346570619262500622020830577593082335012657436258906660316834855233655670129821316406571164731970951037159659784932007004667151756468829612442421828681770659878813878476837170228613469252374430814055367286171646230740044919552*y^2 - 10557017522388333100778181599155610173558596024697146562358161883500940273137179283363926784131499170145772025793717450836086172361622692095037636191465858930522606628549659514938843468649777361353480316819999809416443087122958344653661771218891167341764380333/1170941314381911991213556902633322382711467250111963749503966754820302278338526603198857030273942058020623367836953182809651754771186688738761287761260840087316164389330239635929162718718778186498125830690641150424465427397546529966111510896321533208085519360*y + 373999116340336806222909315329900678397444644508209178006957742952898944641245185286661563239733613854090180637751973337993429845170553068422502745410543322142478744467509982817800168199580380904488650596737343627282527290784193675990130222875169744100585561/390313771460637330404518967544440794237155750037321249834655584940100759446175534399619010091314019340207789278984394269883918257062229579587095920420280029105388129776746545309720906239592728832708610230213716808155142465848843322037170298773844402695173120