# Manifold: Census Knot K7_59 # Number of Tetrahedra: 7 # Number Field x^22 + 10*x^21 - 67*x^20 - 232*x^19 + 1409*x^18 + 2120*x^17 - 11772*x^16 - 11204*x^15 + 50545*x^14 + 39544*x^13 - 125140*x^12 - 97316*x^11 + 188204*x^10 + 169633*x^9 - 170141*x^8 - 181985*x^7 + 56799*x^6 + 106239*x^5 + 19964*x^4 - 31740*x^3 - 7167*x^2 + 192*x + 29 # Approximate Field Generator -0.434822848962585 + 0.566225366667062*I # Shape Parameters -667676120302593882762951936148149540693388632681443928/1660634161144948901382695341902160829744656505829603268225*y^21 - 6962733732320214464428705351884760653600746390827364533/1660634161144948901382695341902160829744656505829603268225*y^20 + 41772565488475746900620101420609717548312833679328028418/1660634161144948901382695341902160829744656505829603268225*y^19 + 173030868147351054818887623042853674485884901276795443539/1660634161144948901382695341902160829744656505829603268225*y^18 - 867679694397330909517170889147371610254489208613207413313/1660634161144948901382695341902160829744656505829603268225*y^17 - 1794094068136811616278444689554452002225487512194653815273/1660634161144948901382695341902160829744656505829603268225*y^16 + 7112570880409976044463053842154567523223555620883749072318/1660634161144948901382695341902160829744656505829603268225*y^15 + 2123321311435189289660106478244328362154915705982123308706/332126832228989780276539068380432165948931301165920653645*y^14 - 5874149585439436768843264597374198692873429202840264389326/332126832228989780276539068380432165948931301165920653645*y^13 - 39584455224356264565001413995473005412612685411505998104137/1660634161144948901382695341902160829744656505829603268225*y^12 + 67243250513422099840401443291374598317954885053733713989858/1660634161144948901382695341902160829744656505829603268225*y^11 + 96111559846817828181548499557508474279128209806795506129306/1660634161144948901382695341902160829744656505829603268225*y^10 - 85579258579977437154310070323232059338567655035265741457856/1660634161144948901382695341902160829744656505829603268225*y^9 - 31085122176644566164511946866413386686095506233838973234351/332126832228989780276539068380432165948931301165920653645*y^8 + 47023820986759028863296420064090704625677057521216469276418/1660634161144948901382695341902160829744656505829603268225*y^7 + 149751693615806757443010409995971814177265552751483459382898/1660634161144948901382695341902160829744656505829603268225*y^6 + 29631086904127485071401933470521177232758283999552816056826/1660634161144948901382695341902160829744656505829603268225*y^5 - 64773532289910524918483658578894523778430180376740583276941/1660634161144948901382695341902160829744656505829603268225*y^4 - 47295994802590615844163063805342777985342951176163420909708/1660634161144948901382695341902160829744656505829603268225*y^3 + 1052504989242001021446019365455553756790736115261083257212/1660634161144948901382695341902160829744656505829603268225*y^2 + 10551158604296444063403135837016918015445136825115348459938/1660634161144948901382695341902160829744656505829603268225*y + 8422293446651908449449582753997323948858114463553689986162/1660634161144948901382695341902160829744656505829603268225 -1754891714628002420579482234757276937481768401872898538/8037469339941552682692245454806458415964137488215279818209*y^21 - 17140149372793624534746384138290168127016299155510912581/8037469339941552682692245454806458415964137488215279818209*y^20 + 120336024745991138435458729492786139618307559395520158303/8037469339941552682692245454806458415964137488215279818209*y^19 + 367639200239631023817209401805463652391109624815798430092/8037469339941552682692245454806458415964137488215279818209*y^18 - 2467960187666416197114355217003052431867811153838016918241/8037469339941552682692245454806458415964137488215279818209*y^17 - 2927771704273213052641262485448346022730376278424574025107/8037469339941552682692245454806458415964137488215279818209*y^16 + 19487368313910559242208668593299549948128560601162194468276/8037469339941552682692245454806458415964137488215279818209*y^15 + 13894042075215177466140012654896177077985484987052904464085/8037469339941552682692245454806458415964137488215279818209*y^14 - 77371012097385155070283827007303953331728562843598593433000/8037469339941552682692245454806458415964137488215279818209*y^13 - 4366563795232879706557523914466761241683007704860919902672/730679030903777516608385950436950765087648862565025438019*y^12 + 172688338709707198140146199715932524498287262273466476327673/8037469339941552682692245454806458415964137488215279818209*y^11 + 121607476952120561018993859615912876984316249659666561108280/8037469339941552682692245454806458415964137488215279818209*y^10 - 20471694352381267289027755901593859482159843227659198292371/730679030903777516608385950436950765087648862565025438019*y^9 - 213356323117608619765434228104834616203225529580687281679752/8037469339941552682692245454806458415964137488215279818209*y^8 + 160225358538191727759752146437715167041551961291945347776130/8037469339941552682692245454806458415964137488215279818209*y^7 + 200060356109601983697512112073382028961356458286746174527395/8037469339941552682692245454806458415964137488215279818209*y^6 + 18378206743933814720087222821755507628888544951303619991131/8037469339941552682692245454806458415964137488215279818209*y^5 - 9013098873946866947579844860230442523750485067498749179578/730679030903777516608385950436950765087648862565025438019*y^4 - 43355844858562202056525225915749173177941355656020951408781/8037469339941552682692245454806458415964137488215279818209*y^3 - 8845588772078517499963955603971880696455584951754534397320/8037469339941552682692245454806458415964137488215279818209*y^2 + 4755082375400479617924783131283415850966599849396907643764/8037469339941552682692245454806458415964137488215279818209*y + 5585723187038645083462457499383301582809660623471114723856/8037469339941552682692245454806458415964137488215279818209 184273108217505226701441347796598533426709464667266857183/21189691896209547981643192562671572187541817014385737702551*y^21 + 1844478402058097088696315447441463178541462015179301093042/21189691896209547981643192562671572187541817014385737702551*y^20 - 12327236326552104021575863813426743810779670833467807399702/21189691896209547981643192562671572187541817014385737702551*y^19 - 1477673797624716293128007306226049018656729448381257348204/730679030903777516608385950436950765087648862565025438019*y^18 + 259129798011474440825937711340663174884357874444177825910866/21189691896209547981643192562671572187541817014385737702551*y^17 + 392758980666413340644128090737761080902858695216695359444852/21189691896209547981643192562671572187541817014385737702551*y^16 - 2163380071212657580842978440427025262665045399617498360473356/21189691896209547981643192562671572187541817014385737702551*y^15 - 2081908112906947810270545884050849293972834448375294200611943/21189691896209547981643192562671572187541817014385737702551*y^14 + 9277019907169550346089372088514998775757933236059469737741950/21189691896209547981643192562671572187541817014385737702551*y^13 + 668886515801104980618520950125951771143945138779398293037395/1926335626928140725603926596606506562503801546762339791141*y^12 - 22920011100166043426844177402992757627679864171345537767051088/21189691896209547981643192562671572187541817014385737702551*y^11 - 18087614516454315599503409118465561059510071088947797760664147/21189691896209547981643192562671572187541817014385737702551*y^10 + 3122731915371236615653728601064880422225258275787399005316057/1926335626928140725603926596606506562503801546762339791141*y^9 + 31427672083044894645660548061049845884208099458191498005109697/21189691896209547981643192562671572187541817014385737702551*y^8 - 30846661528133370500293072817078378280508222531826029510853784/21189691896209547981643192562671572187541817014385737702551*y^7 - 33560373467935959982247959217496009258575197535340031200151022/21189691896209547981643192562671572187541817014385737702551*y^6 + 10012936686823220910164182891392606492497356408442294250002217/21189691896209547981643192562671572187541817014385737702551*y^5 + 1764806600123364085465860551369628115560427194512696427858401/1926335626928140725603926596606506562503801546762339791141*y^4 + 3821596697251926258866104729671226278729320082519889273556346/21189691896209547981643192562671572187541817014385737702551*y^3 - 5689889926963259470531045643971877847737614424939546789153103/21189691896209547981643192562671572187541817014385737702551*y^2 - 1299060823695097858218479499890913006603183734843616984899071/21189691896209547981643192562671572187541817014385737702551*y + 42463404256126562044234506374013749742975940826104151480821/21189691896209547981643192562671572187541817014385737702551 -3705226050937747798646774764982992613119435873408336191268319/2842152450048156244421643996469830010288529133467585545041985995*y^21 - 36489922740930678776971704135227629043274563930287136379006194/2842152450048156244421643996469830010288529133467585545041985995*y^20 + 253331444746322766416618449354376177169252359926963949798493424/2842152450048156244421643996469830010288529133467585545041985995*y^19 + 816191699157505448477590840665808083320864828895493121252362492/2842152450048156244421643996469830010288529133467585545041985995*y^18 - 5318397756200852109553418350018370424302390199890011868294222849/2842152450048156244421643996469830010288529133467585545041985995*y^17 - 6919150128163116952855103697319239416146060670126404244773627529/2842152450048156244421643996469830010288529133467585545041985995*y^16 + 44142427850260657230930203648775788271978310386717282760877278004/2842152450048156244421643996469830010288529133467585545041985995*y^15 + 2225668632320738299647072543023545348269038320911826946620257095/189476830003210416294776266431322000685901942231172369669465733*y^14 - 37662417872820945576314213996217355338726880934670796044593398694/568430490009631248884328799293966002057705826693517109008397199*y^13 - 109237125922887800113386273719353087197763057922898232104814757681/2842152450048156244421643996469830010288529133467585545041985995*y^12 + 155142207679572523861958362853588543201874479784133752049218068173/947384150016052081473881332156610003429509711155861848347328665*y^11 + 86130971829263923561922007694651216291662259882274806351123216326/947384150016052081473881332156610003429509711155861848347328665*y^10 - 709262306223627994919074587542781795670672586143589758788533362003/2842152450048156244421643996469830010288529133467585545041985995*y^9 - 90107575734998871709576562198720680456662643314002597111911365106/568430490009631248884328799293966002057705826693517109008397199*y^8 + 678515753935400868169674046554713665233101406486855472998982173134/2842152450048156244421643996469830010288529133467585545041985995*y^7 + 157449055869010864654245370775103611101134149536145044353076823713/947384150016052081473881332156610003429509711155861848347328665*y^6 - 294919317034883976294799205349627881887199148420614796154378357907/2842152450048156244421643996469830010288529133467585545041985995*y^5 - 91441063255284406415246751777603885634000054416455347991323699301/947384150016052081473881332156610003429509711155861848347328665*y^4 + 8895202753866106368083511135599602166820328539014995345801099291/2842152450048156244421643996469830010288529133467585545041985995*y^3 + 34493437182326822802712269055175344933987479529833400487980024352/947384150016052081473881332156610003429509711155861848347328665*y^2 - 64329907384836824236328161189335690445967058665254011238811513/20745638321519388645413459828246934381668095864726901788627635*y - 213165644353235290515371074742546752616483303932068375568617313/947384150016052081473881332156610003429509711155861848347328665 981458574237297477883525267073369616880073555211534463138792/568430490009631248884328799293966002057705826693517109008397199*y^21 + 3266539078294292489787720233420633253479959911624503330479529/189476830003210416294776266431322000685901942231172369669465733*y^20 - 21914833886859516326474354052433941584417381627326600560845326/189476830003210416294776266431322000685901942231172369669465733*y^19 - 74996000238189063251301549278101342924674440607653552551851087/189476830003210416294776266431322000685901942231172369669465733*y^18 + 458774779632398647978876185936553050356408002233976589595893951/189476830003210416294776266431322000685901942231172369669465733*y^17 + 672567598024631365098383467556903837490207797321027612282698917/189476830003210416294776266431322000685901942231172369669465733*y^16 - 11380399657786361378541204286198903644897288888424171985893292228/568430490009631248884328799293966002057705826693517109008397199*y^15 - 10393099438224009484411654103604319769675478372372406771233889133/568430490009631248884328799293966002057705826693517109008397199*y^14 + 48150117278443142663445537784984315738284179300070767117154233951/568430490009631248884328799293966002057705826693517109008397199*y^13 + 35613773014397994866980249474105263208290527331819188462931543200/568430490009631248884328799293966002057705826693517109008397199*y^12 - 117018964485647511137381145679534271226752691835474271833378528681/568430490009631248884328799293966002057705826693517109008397199*y^11 - 28349332130038981448248959795686770109636818839950898416205873209/189476830003210416294776266431322000685901942231172369669465733*y^10 + 172446940777743175975997395899051498925785756190006243514165920547/568430490009631248884328799293966002057705826693517109008397199*y^9 + 144426360171777157461465179459529980184745390629231152040194933654/568430490009631248884328799293966002057705826693517109008397199*y^8 - 153378100893154178577416420401897525618705651124964813746239297961/568430490009631248884328799293966002057705826693517109008397199*y^7 - 147755704301948403280725475471606528399017009338478964930104905969/568430490009631248884328799293966002057705826693517109008397199*y^6 + 50523839421622236946537447540846611960048442316666801328097290307/568430490009631248884328799293966002057705826693517109008397199*y^5 + 80276552150505472375987060594787161050369165758119008380002774811/568430490009631248884328799293966002057705826693517109008397199*y^4 + 12511028361327912510126681335204741178137503367736718892838681016/568430490009631248884328799293966002057705826693517109008397199*y^3 - 24958198262266821423946124468996349647535909531826709575233965308/568430490009631248884328799293966002057705826693517109008397199*y^2 - 8444612382491960139313418878492954845888763707010020253356662/4149127664303877729082691965649386876333619172945380357725527*y + 634424060493171712705010246803283751792017837107442106640162756/568430490009631248884328799293966002057705826693517109008397199 -18580627343493499653055295080063910062866520285194336681321/4031421914961923750952686519815361716721317919812178078073739*y^21 - 183265396940329228482218009320130919932942261562254572849437/4031421914961923750952686519815361716721317919812178078073739*y^20 + 1269620208672859672360698433119846816288284594858074331879725/4031421914961923750952686519815361716721317919812178078073739*y^19 + 4133553648889868142267851341829917850491429648514764564687892/4031421914961923750952686519815361716721317919812178078073739*y^18 - 26723660238148053740826322468635023192705746473405461896017374/4031421914961923750952686519815361716721317919812178078073739*y^17 - 35653102433862853831308593936568553801133205110350453675250105/4031421914961923750952686519815361716721317919812178078073739*y^16 + 223161278077453211140143160971126144104843078433450836737897084/4031421914961923750952686519815361716721317919812178078073739*y^15 + 176867867881678185137066028841230224477335520974303727976289095/4031421914961923750952686519815361716721317919812178078073739*y^14 - 959800863686286064502473356278715234598781269235805637362859551/4031421914961923750952686519815361716721317919812178078073739*y^13 - 599333696860577943577487539443193372704253680200521554516113436/4031421914961923750952686519815361716721317919812178078073739*y^12 + 2392900436874434729698542630253437845489842618486441223788299563/4031421914961923750952686519815361716721317919812178078073739*y^11 + 1467431768052247447052538003227538028368438926051701772695361408/4031421914961923750952686519815361716721317919812178078073739*y^10 - 3664822537529244877132555621671494003948819630039212609734647440/4031421914961923750952686519815361716721317919812178078073739*y^9 - 2621911874436622131742564290639091535468122113714716862889419128/4031421914961923750952686519815361716721317919812178078073739*y^8 + 3473065884688155638160625454773382222387861625317921668393129020/4031421914961923750952686519815361716721317919812178078073739*y^7 + 2862710872610972491810403818757595887815335128193878807156793710/4031421914961923750952686519815361716721317919812178078073739*y^6 - 1404825587636158344318416179632914409144673348826842079591305048/4031421914961923750952686519815361716721317919812178078073739*y^5 - 1742461890670034636154147052794086790907156121632149601904019106/4031421914961923750952686519815361716721317919812178078073739*y^4 - 150935408803506946614558151900555795345037304115690763674794546/4031421914961923750952686519815361716721317919812178078073739*y^3 + 591829437098177899325977876198880376483985389694365397410064400/4031421914961923750952686519815361716721317919812178078073739*y^2 + 432485053899510699566544785839430512801240025393828367570836/29426437335488494532501361458506289903075313283300569912947*y + 2807289943917203886124029027881538513023901755505901076889357/4031421914961923750952686519815361716721317919812178078073739 -1768743721256226808923222851899622714745111923131938920247848/568430490009631248884328799293966002057705826693517109008397199*y^21 - 17516317886196207105554543043462233779079499477950574829882106/568430490009631248884328799293966002057705826693517109008397199*y^20 + 119973213725096731360057927762232299681266114900892861403153845/568430490009631248884328799293966002057705826693517109008397199*y^19 + 396317097346207868338414158979696345393324133694007737684608071/568430490009631248884328799293966002057705826693517109008397199*y^18 - 2516931792965510963461010836225046336761459792804034085276111518/568430490009631248884328799293966002057705826693517109008397199*y^17 - 3444803669040264390429084852813214723794497164757545043860403135/568430490009631248884328799293966002057705826693517109008397199*y^16 + 20877866786735316932301594052384829536626655296646194320659050857/568430490009631248884328799293966002057705826693517109008397199*y^15 + 5713077459276580692714326354672254557434321614965911501047621027/189476830003210416294776266431322000685901942231172369669465733*y^14 - 88865316337464758530658965410032383679562638102475864772083987601/568430490009631248884328799293966002057705826693517109008397199*y^13 - 57428946592921128579529962169584887356822395359610009167955752705/568430490009631248884328799293966002057705826693517109008397199*y^12 + 72779984841608656163451282047818224991991544937473444249825774030/189476830003210416294776266431322000685901942231172369669465733*y^11 + 45627704504932893707693488166269539235279012585347823704446342993/189476830003210416294776266431322000685901942231172369669465733*y^10 - 328233297615562867269338966610448598352339995825540026884281983294/568430490009631248884328799293966002057705826693517109008397199*y^9 - 236441804124131730966958019039402221123533892274033600183126705276/568430490009631248884328799293966002057705826693517109008397199*y^8 + 304221780700378994437104382324632335344990080475712848256354133716/568430490009631248884328799293966002057705826693517109008397199*y^7 + 82078201333838341012706129777772583547464295101318250134160695838/189476830003210416294776266431322000685901942231172369669465733*y^6 - 117624343536157168773919507869818505346390416972452697819965318120/568430490009631248884328799293966002057705826693517109008397199*y^5 - 46326699430967349075981347590469739306157419421295193237768190106/189476830003210416294776266431322000685901942231172369669465733*y^4 - 10960770848080824140955104605722796305794150151022337871072996929/568430490009631248884328799293966002057705826693517109008397199*y^3 + 15633179186782259973067508881979149844909892978855737836890907478/189476830003210416294776266431322000685901942231172369669465733*y^2 + 2102869073542783014136567391449164026621073538507524221820178/4149127664303877729082691965649386876333619172945380357725527*y + 158408454457271540145089131025150536148942155153497743116216651/189476830003210416294776266431322000685901942231172369669465733 # A Gluing Matrix {{1,0,2,2,0,-1,-1},{0,1,-2,-2,0,1,1},{1,-2,4,4,0,-2,-2},{1,-2,4,5,-1,-2,-3},{0,0,0,-1,0,0,0},{-1,2,-4,-4,0,3,2},{-1,2,-4,-6,0,2,4}} # B Gluing Matrix {{2,0,0,0,0,0,0},{0,1,0,0,0,0,0},{0,0,1,0,0,0,0},{0,0,0,1,0,0,0},{0,0,0,0,1,0,0},{0,0,0,0,0,2,0},{0,0,0,0,0,0,2}} # nu Gluing Vector {0, 1, 0, -1, 0, 2, 2} # f Combinatorial flattening {12, -11, 3, 0, 5, 12, 6} # f' Combinatorial flattening {0, 0, -10, 0, 0, 0, 0} # 1 Loop Invariant -13037447661470362904182554674111810584241073650938522101399843/189476830003210416294776266431322000685901942231172369669465733*y^21 - 129244751320495295954476216663978976414053986020435280447264530/189476830003210416294776266431322000685901942231172369669465733*y^20 + 882706043171616508543073935945873382146969213089688922970059158/189476830003210416294776266431322000685901942231172369669465733*y^19 + 2926886440266024970187068620477320117407178094384039350212974904/189476830003210416294776266431322000685901942231172369669465733*y^18 - 18503390563117631624061469752127106226346325967692659119423228987/189476830003210416294776266431322000685901942231172369669465733*y^17 - 25498793214929766816868912804388577050422586031548079189555971201/189476830003210416294776266431322000685901942231172369669465733*y^16 + 153237149630741425389413840400800796767187120449344243497467767300/189476830003210416294776266431322000685901942231172369669465733*y^15 + 127088652618553833632210078358344576399535045192098511570360224033/189476830003210416294776266431322000685901942231172369669465733*y^14 - 650628784441131557260936094953430132563544695376876609415555301108/189476830003210416294776266431322000685901942231172369669465733*y^13 - 425556459134670256135739810725769340619796433282807605487850990483/189476830003210416294776266431322000685901942231172369669465733*y^12 + 1593155542300658360238488005467493600958347177555681748255717017463/189476830003210416294776266431322000685901942231172369669465733*y^11 + 1010950429550753631353231475135662244109782441233265382696924683362/189476830003210416294776266431322000685901942231172369669465733*y^10 - 2385171932514467230566568033348236491128573243086355525147339116737/189476830003210416294776266431322000685901942231172369669465733*y^9 - 1738631936442418872469876426182939904323362248728438402711411844596/189476830003210416294776266431322000685901942231172369669465733*y^8 + 2200324148951208360679349621945016482035963434818393383582719613408/189476830003210416294776266431322000685901942231172369669465733*y^7 + 1800440862037531980083261423039850329691347814076214276601012176133/189476830003210416294776266431322000685901942231172369669465733*y^6 - 841468419986354755165286396154001883711906555636159732468236912997/189476830003210416294776266431322000685901942231172369669465733*y^5 - 1008891676536625250499543701134720329379006487006355950903108480455/189476830003210416294776266431322000685901942231172369669465733*y^4 - 79823207965412403572116227757911310906554552044691530810482561009/189476830003210416294776266431322000685901942231172369669465733*y^3 + 347171428937775445839367638057919431414033084311570499080155018972/189476830003210416294776266431322000685901942231172369669465733*y^2 - 4604794526880197386754054558645529723621049742541740545413011/1383042554767959243027563988549795625444539724315126785908509*y - 202308965208006185964249240857821605195617085471793897971696067/189476830003210416294776266431322000685901942231172369669465733 # 2 Loop Invariant 18761522859116778749643015424542253057069747570270651225313723312127739322464947179285570181756563358302813041221543542886105/114436877636509415541735499192726188046229873329085188304336876382343943035960282890454226542279827655798685105897190091331273704*y^21 + 3357142174894407724629346370598885834433419763802334992789059239242198900370156164651790838626689546065178480182402519052180593/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^20 - 1423191706213927884730110540362403112534540003837953216068795568491549802178574146596697358462850124122370658673000468204908429/128741487341073092484452436591816961552008607495220836842378985930136935915455318251761004860064806112773520744134338852747682917*y^19 - 76433736408149617132124863424787437871649366820544712122381896520845388054432951301500838709724973951281944543158453115581456721/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^18 + 477147644500482394707727032675961335525797800278787051688905484919897017124042905777105398241374976329913213413812337440896220349/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^17 + 673337504592462864628759397276685040666824334576891991509921614574713765665418942245778463421465305903908110437716379671035538571/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^16 - 987501206051289059828907869349234258962258488033117777774719620016303052787476905113820285134431680679310846876662299809381478101/514965949364292369937809746367267846208034429980883347369515943720547743661821273007044019440259224451094082976537355410990731668*y^15 - 3396166124254334538884099849282624418916621640397125615974341640247046609725721024485436014490881799210472015883832354421432997947/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^14 + 5584242588757409769835416373631848198463611689761401720464872985623105652328718666486707616420705268338515395578247720584189850389/686621265819056493250412995156357128277379239974511129826021258294063658215761697342725359253678965934792110635383140547987642224*y^13 + 1431307790151787469511598178888569568214558026738662638055155060959261162257928931995562787203282934329449232079456122774688237627/257482974682146184968904873183633923104017214990441673684757971860273871830910636503522009720129612225547041488268677705495365834*y^12 - 40912741869753003342456332222466725896818202894348659404555480706625505353346270524810900430201142081634398444262944108890817300395/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^11 - 3019382052426788878706045269194037937093749030025027893869872681873500131377271797528874537876778120620412907211750412235750907313/228873755273018831083470998385452376092459746658170376608673752764687886071920565780908453084559655311597370211794380182662547408*y^10 + 20301968437987357507194450017542680466028857268318378289545021686519614752757815307030473386237054252293141597589570446940231440739/686621265819056493250412995156357128277379239974511129826021258294063658215761697342725359253678965934792110635383140547987642224*y^9 + 11593646711432874653714242701580496556461939629133901507925243611147541431582052670181212356612855330831240225413035520281968212719/514965949364292369937809746367267846208034429980883347369515943720547743661821273007044019440259224451094082976537355410990731668*y^8 - 55543691401953649102769226669797303855093888877912071656499936419189781821350594377426369902640177375841540955774727552552053509785/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^7 - 47659429645402928956061602244350817201651625349890580562575980695717745462004607867295482420446705423341389110270595718454816090627/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^6 + 6873386098377257949699349660363222825678500512260654877241865929276552569393207160258811468508443895575407668864149564540158795205/686621265819056493250412995156357128277379239974511129826021258294063658215761697342725359253678965934792110635383140547987642224*y^5 + 26305932555330429463796199555655259266386618066048316950700797736462927928122085509263518001246936474765641302156369396101369151369/2059863797457169479751238985469071384832137719923533389478063774882190974647285092028176077761036897804376331906149421643962926672*y^4 + 351467254464718498931576503570412557475066972441918235163193280036551859693288152734305277366373850104039896840768676391815671981/343310632909528246625206497578178564138689619987255564913010629147031829107880848671362679626839482967396055317691570273993821112*y^3 - 556733017119892291818776861196142294300442941578158947588817237458922227491118922909683086945011175940743930661762423176805451738/128741487341073092484452436591816961552008607495220836842378985930136935915455318251761004860064806112773520744134338852747682917*y^2 + 544158488074276281332056050418836809815118650930275549710931149152227612482436283023067946054658088136906939535359403552793493/2505917028536702530110996332687434774734960729833982225642413351438188533634166778623085252750653160345956608158332629737181176*y + 2325398528165362700069526729811891707776436606148398496442555928053993327921623033462662769376246525450396164196294877214433881031/514965949364292369937809746367267846208034429980883347369515943720547743661821273007044019440259224451094082976537355410990731668 # 3 Loop Invariant 41929621655703142154978271555140156746094144214695486620542823546942888115161324831692414965908240810415660739864087658387906800341141446615558022302561169975/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424*y^21 + 437618392466292529596452038206963580881440725421877330593164392573273864662256081439326018033824268031792686742405759504391800061694501098561322621284849490115/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424*y^20 - 1313245230025305374283979238295231230607767013624615113334575189758925061581854282869731565999571326621685377944093998671017389175133332920935852887738992516711/377317716142767536320183409205594357166153483857142911892709004937604938258421194920930934365080730158770276548693498419226439075821883135857045514363732031279712*y^19 - 10959281822784747182689888830406368699073198937224079884390922377958175013050938761213601612288890515512221979628611407038902168550549272364320551299499470790985/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424*y^18 + 54860338572896009265128946076014003131456111946824768283491926067450541102739361757080247344966009217528320330356404555813114349140922283726801560420589874095245/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424*y^17 + 28699536308061832402268112974175291992102078784916146631872758020656292385419831320595883703693899612232817979197727695634238812722199487797724388284422455336195/188658858071383768160091704602797178583076741928571455946354502468802469129210597460465467182540365079385138274346749209613219537910941567928522757181866015639856*y^16 - 151833475721919038524227597836493226606095772616557089728881474623778173659949794693853352557119122668532029061228186309902806107924527299013153096528225336011613/251545144095178357546788939470396238110768989238095274595139336625069958838947463280620622910053820105846851032462332279484292717214588757238030342909154687519808*y^15 - 343064530084290161435935549629917277266230053453334601527073765687744050363469782675094898925051181913777996333381670342773048824833426600266240686454025640773849/377317716142767536320183409205594357166153483857142911892709004937604938258421194920930934365080730158770276548693498419226439075821883135857045514363732031279712*y^14 + 1921363692189635174908325503172141730579069513966881611515103253527513246193491934097216984201289561653284995658606236685301856991886358534262655366250749346105141/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424*y^13 + 861762892973488575748230826354233050682584138466211695603384190678310632642312939638735838761010700224205307658983008751939184558456389172193630373336251590713539/251545144095178357546788939470396238110768989238095274595139336625069958838947463280620622910053820105846851032462332279484292717214588757238030342909154687519808*y^12 - 4559578529315337862186602574091902211197068112880348799187128324602383925734161755425637540674506679270177611357172555604295347670094817310144429266635376107031845/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424*y^11 - 2121734995558049377304423374484946615369242046734948573224558260660151493552387797455101737175060657419597529986142624467258503036565200982851992006549416722989027/251545144095178357546788939470396238110768989238095274595139336625069958838947463280620622910053820105846851032462332279484292717214588757238030342909154687519808*y^10 + 3107159562168867502404369064289159295087936268260953632897075668101277191942424567614881704776423759074782656194010920439039472698356623425605828537473776803835327/377317716142767536320183409205594357166153483857142911892709004937604938258421194920930934365080730158770276548693498419226439075821883135857045514363732031279712*y^9 + 3505528622322869546189238392174592622827267798622305306488000338350231750845713851778893039239556358181186718804747342240148413544722677826335942444252822113086823/251545144095178357546788939470396238110768989238095274595139336625069958838947463280620622910053820105846851032462332279484292717214588757238030342909154687519808*y^8 - 1401303002583670964147143775118146651948822561366300680713600312129953929279202763630422366993982687809417832540120575141885490796175761442580662824070171575829177/251545144095178357546788939470396238110768989238095274595139336625069958838947463280620622910053820105846851032462332279484292717214588757238030342909154687519808*y^7 - 5334412655991075381528329633042405244974386586187239956799736916053028917978751192123498419797961390117399789010901015830253868769474101782702331352237327436882689/377317716142767536320183409205594357166153483857142911892709004937604938258421194920930934365080730158770276548693498419226439075821883135857045514363732031279712*y^6 - 383762610307452637489329718704140072755933714791557697045268846633042862194882807608856121114211227166107712534526374810881296969198002729344686729737524622941825/377317716142767536320183409205594357166153483857142911892709004937604938258421194920930934365080730158770276548693498419226439075821883135857045514363732031279712*y^5 + 5454897746863945567284556824500463117548305194958198986267318867352757143753052408070370245896433347481164876988468769153122652584758259349513157646171724225215497/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424*y^4 + 1325420972040517224233630148934091644026508004180282749514182626287841848173431948708789666057625822074476919847658049330216002878359622610796401468343642289778053/377317716142767536320183409205594357166153483857142911892709004937604938258421194920930934365080730158770276548693498419226439075821883135857045514363732031279712*y^3 - 15248200087441901916819131589015073215872388788705227446145045032069904731135134266348638623876053787012081049954967061722963553383913292058693950112722179281018/11791178629461485510005731537674823661442296370535715996647156404300154320575662341279091698908772817461571142146671825600826221119433847995532672323866625977491*y^2 - 6003362843806668352679188264264631823349354638862812451492181708535612515202218266181411676683342573213571314409557201562427189354458397014466597652531617185799/5508287826901715858688808893512326381987642100104276086024948977191312967276221823663225319198258834434602577353189757944911519355063987384774387071003387317952*y - 100459401347555901668814505260967693761584510534921592563081283493282454779504054779176339987022059207341989445238285235654203266713320891596724533218029677131911/754635432285535072640366818411188714332306967714285823785418009875209876516842389841861868730161460317540553097386996838452878151643766271714091028727464062559424