# Manifold: Census Knot K8_296 # Number of Tetrahedra: 8 # Number Field x^22 + 9*x^21 + 43*x^20 + 110*x^19 + 112*x^18 - 150*x^17 - 511*x^16 - 82*x^15 + 838*x^14 + 345*x^13 - 167*x^12 + 52*x^11 - 2467*x^10 + 2950*x^9 + 3111*x^8 - 8058*x^7 + 5263*x^6 - 767*x^5 - 565*x^4 + 234*x^3 - 3*x^2 - 10*x + 1 # Approximate Field Generator 0.634314514360356 - 0.736556422288467*I # Shape Parameters -y + 1 -12365202383784153966736653766635988864/1897714808267504683439614510526320195*y^21 - 113750832279044257829385516843924418209/1897714808267504683439614510526320195*y^20 - 111026763919611387821436117328803009883/379542961653500936687922902105264039*y^19 - 295544193882112725023672765170641874959/379542961653500936687922902105264039*y^18 - 1712808532752273154622463813903254863848/1897714808267504683439614510526320195*y^17 + 1426125795159456776154896197226611573349/1897714808267504683439614510526320195*y^16 + 6506691723537288735167405038981749760687/1897714808267504683439614510526320195*y^15 + 2407446624633137702023741239938002901992/1897714808267504683439614510526320195*y^14 - 9496191305344885233507833982160110388398/1897714808267504683439614510526320195*y^13 - 6055615175480675112409157912241193505306/1897714808267504683439614510526320195*y^12 + 269915955580605569722044527526533259451/1897714808267504683439614510526320195*y^11 - 884688710011705549772362355831993881006/1897714808267504683439614510526320195*y^10 + 30369747474159891645580033189744492794066/1897714808267504683439614510526320195*y^9 - 30497649775108781811957288528170197189968/1897714808267504683439614510526320195*y^8 - 8533541469422744984641484789905034832802/379542961653500936687922902105264039*y^7 + 89024291355659516252980018038144119849217/1897714808267504683439614510526320195*y^6 - 49671088653180872099256629353525576679503/1897714808267504683439614510526320195*y^5 + 5328440479329363798513504478478261148637/1897714808267504683439614510526320195*y^4 + 4218411714318295284368106604157212780734/1897714808267504683439614510526320195*y^3 - 1153536262835371061555029347299427023163/1897714808267504683439614510526320195*y^2 - 87597125037874788351109535778180735179/1897714808267504683439614510526320195*y + 26851405412200664869894262916324853002/1897714808267504683439614510526320195 72301089158078659535492215883350873241/322611517405475796184734466789474433150*y^21 + 678024529456313953667178922421073557771/322611517405475796184734466789474433150*y^20 + 67162053471043174580611340732107488237/6452230348109515923694689335789488663*y^19 + 915763897721165196372542983353497444101/32261151740547579618473446678947443315*y^18 + 11244767138275902222567222211108192289587/322611517405475796184734466789474433150*y^17 - 3714235110602953139140805277537497979293/161305758702737898092367233394737216575*y^16 - 20360771091669521622135958958365574223859/161305758702737898092367233394737216575*y^15 - 20550990758842591333145596083684168830133/322611517405475796184734466789474433150*y^14 + 28186548330552873919572166887595085237366/161305758702737898092367233394737216575*y^13 + 23749380260003414340713264040162346600912/161305758702737898092367233394737216575*y^12 + 366953406418008420751069722020522739478/161305758702737898092367233394737216575*y^11 + 505777058932970844368967514388118610857/161305758702737898092367233394737216575*y^10 - 178012034367386508387837090346756833176439/322611517405475796184734466789474433150*y^9 + 72556562982900045414254747384902710659546/161305758702737898092367233394737216575*y^8 + 5933779624798649824217939587350078896949/6452230348109515923694689335789488663*y^7 - 488482384486914698770637136136015047714153/322611517405475796184734466789474433150*y^6 + 173575255843005586600788962402476533643767/322611517405475796184734466789474433150*y^5 + 30210369364751055720497918898102311996751/161305758702737898092367233394737216575*y^4 - 49778939184571641337839683403610581282621/322611517405475796184734466789474433150*y^3 + 4595461858395215893325956544489907874257/322611517405475796184734466789474433150*y^2 + 1363200296248446447224249308942518780553/161305758702737898092367233394737216575*y - 21178178043050686518491969493457309689/161305758702737898092367233394737216575 26940278570570334732356677703911668412/379542961653500936687922902105264039*y^21 + 256486903917491527261534960057261005822/379542961653500936687922902105264039*y^20 + 1291919842660619412445174895221761752160/379542961653500936687922902105264039*y^19 + 3635676011281230811617561136623193152366/379542961653500936687922902105264039*y^18 + 4908532552578289583471239274113340845908/379542961653500936687922902105264039*y^17 - 1489465846113070732749710133589581476135/379542961653500936687922902105264039*y^16 - 14545810343310305089665929329081411437642/379542961653500936687922902105264039*y^15 - 9776840484400107449021407425618158615093/379542961653500936687922902105264039*y^14 + 17503187189382526013035670038171617785216/379542961653500936687922902105264039*y^13 + 18410506674981365468795744301499984024840/379542961653500936687922902105264039*y^12 + 5059393714058862730437413603573273045179/379542961653500936687922902105264039*y^11 + 4021355134013598893869117249779899637993/379542961653500936687922902105264039*y^10 - 64366565583420117314585261808163968847103/379542961653500936687922902105264039*y^9 + 45964350182478814456102568861987967870433/379542961653500936687922902105264039*y^8 + 107820519145955770917124147531724784166176/379542961653500936687922902105264039*y^7 - 161046059481732732265193156901787870082002/379542961653500936687922902105264039*y^6 + 57850552957070112226442638459344991881054/379542961653500936687922902105264039*y^5 + 9697053098503957949336453750990992875744/379542961653500936687922902105264039*y^4 - 10335295042393597146654169051076781099767/379542961653500936687922902105264039*y^3 + 963702845237916945856633300859064115808/379542961653500936687922902105264039*y^2 + 423159087323102948791648055846991026408/379542961653500936687922902105264039*y - 53144532633345464051909373840420726246/379542961653500936687922902105264039 -371134221503558734608345463498121903/3795429616535009366879229021052640390*y^21 - 3816490550143264527109397239264957103/3795429616535009366879229021052640390*y^20 - 4087111730291440576309353542268630447/759085923307001873375845804210528078*y^19 - 12638554428253400509630702723988828565/759085923307001873375845804210528078*y^18 - 103839228977352858438978391988655355811/3795429616535009366879229021052640390*y^17 - 13662734294644401678816432801692412011/1897714808267504683439614510526320195*y^16 + 214390677044152390066026676959643745909/3795429616535009366879229021052640390*y^15 + 264721201995610048761345445635500660299/3795429616535009366879229021052640390*y^14 - 87972585207664638669706126758075388963/1897714808267504683439614510526320195*y^13 - 425525409419596762992374225075717745017/3795429616535009366879229021052640390*y^12 - 94522674967280883952975240192860367909/1897714808267504683439614510526320195*y^11 - 48429869020053893382967029958846080531/1897714808267504683439614510526320195*y^10 + 805259980342191270378785303063603647217/3795429616535009366879229021052640390*y^9 + 6752835367950184604836835208814265987/1897714808267504683439614510526320195*y^8 - 429290102590575462219958626552830369549/759085923307001873375845804210528078*y^7 + 1338406773869762997183117099726766510589/3795429616535009366879229021052640390*y^6 + 1036246885332692954511086259848190782139/3795429616535009366879229021052640390*y^5 - 1383525039007497898403072020323247413521/3795429616535009366879229021052640390*y^4 + 247961190392633778897053915400753473939/1897714808267504683439614510526320195*y^3 - 13777345574181474492934807720528409011/3795429616535009366879229021052640390*y^2 - 38811205664664538452530356828409342863/3795429616535009366879229021052640390*y + 9498750816591917967453848367428348799/3795429616535009366879229021052640390 20747818830309467857405006552325071319/6452230348109515923694689335789488663*y^21 + 196354133383361910761458805348160900206/6452230348109515923694689335789488663*y^20 + 980886333897282010962185309238470167256/6452230348109515923694689335789488663*y^19 + 2716119434579315162412673854502209699091/6452230348109515923694689335789488663*y^18 + 3482570286127763831228514605164235579507/6452230348109515923694689335789488663*y^17 - 1756251731066072427964159651293387124294/6452230348109515923694689335789488663*y^16 - 11686420026997396798073564159515704342734/6452230348109515923694689335789488663*y^15 - 6788849549131031276364273679941309705974/6452230348109515923694689335789488663*y^14 + 15414776374934179904444924187594340430170/6452230348109515923694689335789488663*y^13 + 14520988521644269857710030735861972385041/6452230348109515923694689335789488663*y^12 + 1394512171109302152758138004059109129244/6452230348109515923694689335789488663*y^11 + 943975437682212461885487215924772598267/6452230348109515923694689335789488663*y^10 - 50496459621944006092932926999890085294814/6452230348109515923694689335789488663*y^9 + 37591696015027374972735120629389800489409/6452230348109515923694689335789488663*y^8 + 87793116662356112278984455466947802916663/6452230348109515923694689335789488663*y^7 - 133422824033637049784917960523564089676670/6452230348109515923694689335789488663*y^6 + 40479903400663069144952038709481952651055/6452230348109515923694689335789488663*y^5 + 21297895610671005105098435898129164280998/6452230348109515923694689335789488663*y^4 - 14827672909393277874262262512108307696821/6452230348109515923694689335789488663*y^3 + 1216442604290112699712373418701022940777/6452230348109515923694689335789488663*y^2 + 900183733035943290878416535631845485310/6452230348109515923694689335789488663*y - 142623678099909728588542597395495120749/6452230348109515923694689335789488663 -5569526109237008729600827762102168886/1897714808267504683439614510526320195*y^21 - 106158246030623975600250103856847801157/3795429616535009366879229021052640390*y^20 - 107027633341593744143292917939584714719/759085923307001873375845804210528078*y^19 - 150779069994107202093709880544283397479/379542961653500936687922902105264039*y^18 - 1020346370959728327486522754855533140317/1897714808267504683439614510526320195*y^17 + 606822488407891865935479969815362687097/3795429616535009366879229021052640390*y^16 + 3019201714978269540971859039072246064498/1897714808267504683439614510526320195*y^15 + 2054326360948028746846081474304834056443/1897714808267504683439614510526320195*y^14 - 7227005092950249024447368511890781268189/3795429616535009366879229021052640390*y^13 - 3862018554806151413810737346382326074264/1897714808267504683439614510526320195*y^12 - 1076288117704433274432554907358756464066/1897714808267504683439614510526320195*y^11 - 815975580406267713118076354786590938474/1897714808267504683439614510526320195*y^10 + 13323008994456697236743985349270310002804/1897714808267504683439614510526320195*y^9 - 18706185306985116218505129667239774242589/3795429616535009366879229021052640390*y^8 - 4489509987423348196052079072913813548293/379542961653500936687922902105264039*y^7 + 33093085529566123488151029576115810367518/1897714808267504683439614510526320195*y^6 - 23017694014247403748619007365664529591259/3795429616535009366879229021052640390*y^5 - 4450322632802321691430921437252692012869/3795429616535009366879229021052640390*y^4 + 2133852584516594035150608058285981681951/1897714808267504683439614510526320195*y^3 - 370212106344834536549571261558414081339/3795429616535009366879229021052640390*y^2 - 178046494952007625169334198801595736147/3795429616535009366879229021052640390*y + 11528639886329894942772680900831987678/1897714808267504683439614510526320195 492580962958245540739320355861301119/379542961653500936687922902105264039*y^21 + 4516858058391829415793555617803178591/379542961653500936687922902105264039*y^20 + 21973857125623064583496608299129076437/379542961653500936687922902105264039*y^19 + 58146889247247316084388338642580507212/379542961653500936687922902105264039*y^18 + 66144724794834656367976870467306275348/379542961653500936687922902105264039*y^17 - 59861995310341959934098450558029003196/379542961653500936687922902105264039*y^16 - 259103406421995497055995567488812856063/379542961653500936687922902105264039*y^15 - 88352482688057163862344910419568118260/379542961653500936687922902105264039*y^14 + 384883968827492469347931041338016672951/379542961653500936687922902105264039*y^13 + 233871192719881355696218540196285264340/379542961653500936687922902105264039*y^12 - 21186807019325186868317085080438498006/379542961653500936687922902105264039*y^11 + 29558549398104453264459733750608519033/379542961653500936687922902105264039*y^10 - 1214058855645419586629372747974025960980/379542961653500936687922902105264039*y^9 + 1248788277386082197562787575125652646671/379542961653500936687922902105264039*y^8 + 1679916078402862652368516190108647111250/379542961653500936687922902105264039*y^7 - 3602538589100853128960807424499200108466/379542961653500936687922902105264039*y^6 + 2053294667432286542384565770057628571436/379542961653500936687922902105264039*y^5 - 239657399456390495973181260528965206503/379542961653500936687922902105264039*y^4 - 164694248352243806645333747713147679442/379542961653500936687922902105264039*y^3 + 46495908144325301869544298259110367174/379542961653500936687922902105264039*y^2 + 2977284516028099573069617319083378541/379542961653500936687922902105264039*y - 343318981282546585677250346004026593/379542961653500936687922902105264039 # A Gluing Matrix {{0,2,-2,1,1,1,1,0},{1,-1,1,1,0,0,-1,0},{-1,1,-1,1,0,1,1,0},{1,0,2,0,2,-1,0,2},{1,-1,1,1,2,1,1,2},{1,-1,2,0,3,-1,-1,2},{1,-2,2,1,3,-1,-1,2},{0,0,0,1,1,1,1,2}} # 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,1,0},{0,0,0,0,1,0,1,0},{0,0,0,0,0,1,1,0},{0,0,0,0,0,0,2,0},{0,0,0,0,0,0,0,1}} # nu Gluing Vector {2, 1, 1, 2, 3, 2, 2, 2} # f Combinatorial flattening {-30, -4, 35, -4, -8, 20, -4, -1} # f' Combinatorial flattening {38, -8, -2, 0, 0, 0, 0, 0} # 1 Loop Invariant 3535320719417126580767380131924649034/379542961653500936687922902105264039*y^21 + 31553822594035602120208254891735842718/379542961653500936687922902105264039*y^20 + 298969759751322573349065357347657390415/759085923307001873375845804210528078*y^19 + 751984788849590229809918341464734711375/759085923307001873375845804210528078*y^18 + 358967376193663774793204928949906669670/379542961653500936687922902105264039*y^17 - 583190563831497183556945411405900802150/379542961653500936687922902105264039*y^16 - 3603913967778553062041091508666188628179/759085923307001873375845804210528078*y^15 - 156902173052103211133431842837177656171/379542961653500936687922902105264039*y^14 + 3064194673288475648545002556686903842964/379542961653500936687922902105264039*y^13 + 2138413953950974810009482521844804189983/759085923307001873375845804210528078*y^12 - 768030844222366865479001787962515686568/379542961653500936687922902105264039*y^11 + 106794855067313050167885431985340218182/379542961653500936687922902105264039*y^10 - 8787239149015555267843079624888436297408/379542961653500936687922902105264039*y^9 + 11036167053404174320874501399111132297542/379542961653500936687922902105264039*y^8 + 21145149785126855036775996985073160220093/759085923307001873375845804210528078*y^7 - 29494913462052166683405256311571654378729/379542961653500936687922902105264039*y^6 + 20049593157700879484093705858452962173617/379542961653500936687922902105264039*y^5 - 6616806965247716144498256545248059764173/759085923307001873375845804210528078*y^4 - 3941321914596238053649901391572351464639/759085923307001873375845804210528078*y^3 + 788693418010608873271081295221046356775/379542961653500936687922902105264039*y^2 + 74913845169974571976166447371246193893/759085923307001873375845804210528078*y - 81634654716555213996160048928881809063/759085923307001873375845804210528078 # 2 Loop Invariant -43903436565058727603632183593373487633626639756004983409221894299212341856986691961022748848247582669/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672*y^21 - 107416284487060757984693075357388191876034086749476083949666400940346386896466341713468330405130790147/156695398464271763514824496425010822345890948725239944646285837375515106119920487631201840307051567668*y^20 - 138545317694428178347521158923403584168563260966710735436856819904662401719989982332335500230353996009/39173849616067940878706124106252705586472737181309986161571459343878776529980121907800460076762891917*y^19 - 1621468787606167023027711003910174032779997637834703025841526738137548569307674273985458213673142963831/156695398464271763514824496425010822345890948725239944646285837375515106119920487631201840307051567668*y^18 - 1197133293243106893937500514036102754980365909183801626195409496218930118938422623394313559503903546871/78347699232135881757412248212505411172945474362619972323142918687757553059960243815600920153525783834*y^17 + 309271146328041281065041164179605877267086324637215197232660898017010278474982160226118007247757075859/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672*y^16 + 8140563055965537529118614633808938019994033301329734203040817894221146990436151424681114171680590101615/208927197952362351353099328566681096461187931633653259528381116500686808159893983508269120409402090224*y^15 + 2803991597091502036456867272985410587430153707926896649508597909954102411409282114261319828057835260793/78347699232135881757412248212505411172945474362619972323142918687757553059960243815600920153525783834*y^14 - 2006690320972795170425160678267543175455770597339257093803898785312258398292323655358846740075557237701/52231799488090587838274832141670274115296982908413314882095279125171702039973495877067280102350522556*y^13 - 18881798478925875785078565982094898993532332199239825196154272854531436944812268104236287630780522016867/313390796928543527029648992850021644691781897450479889292571674751030212239840975262403680614103135336*y^12 - 4200696459627118379483725470167723072288257600445051229627326120718311006742683772343141106696200543511/156695398464271763514824496425010822345890948725239944646285837375515106119920487631201840307051567668*y^11 - 2960899227627659142494748888744211748100374307314887897156506325655370658229250209567031609116567624273/208927197952362351353099328566681096461187931633653259528381116500686808159893983508269120409402090224*y^10 + 34561778513820187017781353033055780799323071646968266036266050950288394827433538408811793675052480565847/208927197952362351353099328566681096461187931633653259528381116500686808159893983508269120409402090224*y^9 - 15475692135859904335286171581075523498784264483845468897120683473467182036025636547793894784253160961295/208927197952362351353099328566681096461187931633653259528381116500686808159893983508269120409402090224*y^8 - 194869089347169046843608688635533813615182991758945374891024189182924571186171448850002171789924877755319/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672*y^7 + 214559669090265564393467145055685223792917678832974581448656792475578778623500156356772582219051629461847/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672*y^6 - 25532526080602301438367770573324576872283605632860434523829661877407548996120533414259663147431687071241/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672*y^5 - 37629420935432651706831230926406971201999257877771887693480148294896795513175068092005556210726008703441/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672*y^4 + 998383660536178478764997745521509762902602822011100370758881486543891654828611346241045246236737028985/52231799488090587838274832141670274115296982908413314882095279125171702039973495877067280102350522556*y^3 + 1452944285846062993696734961615194622650188372430546313657785149005414791239331532044182837415640803859/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672*y^2 - 20899950468433110449025239245930877437663363921490237992448530503899006724294505319178292119161462105/20218761092164098518041870506453009334953670803256767051133656435550336273538127436284108426716331312*y + 91504023713201336342686595007173344583124149389872267152623374702969707230654352619147291482206612410053/626781593857087054059297985700043289383563794900959778585143349502060424479681950524807361228206270672 # 3 Loop Invariant 3703965877627401401837583049576749014175766725842945513500918403435642234782620956916645136484904454953937235211629610070111516252493/77505407292819060779821012065153126800531582107427476896504169382377103247646861577364796228088571375917928190240967769281160157473952*y^21 + 69390215200555985041523589617476075393457898486282560135286543367222817132683411753623412322671972266062921673049507475963490225422799/155010814585638121559642024130306253601063164214854953793008338764754206495293723154729592456177142751835856380481935538562320314947904*y^20 + 172060099309047704570843784495312041398606099818261117218468436285628706056990991283207297025009958691150257956905791751292442762782211/77505407292819060779821012065153126800531582107427476896504169382377103247646861577364796228088571375917928190240967769281160157473952*y^19 + 942157273718122275587109783021326136236077224077185399579557192349895900997216597823847968840982411312582083848598384739914441691534435/155010814585638121559642024130306253601063164214854953793008338764754206495293723154729592456177142751835856380481935538562320314947904*y^18 + 590048014948501453546601102241169595767978190801918768130915517068400576904607312874869946281997008652837153342587010552019192548034395/77505407292819060779821012065153126800531582107427476896504169382377103247646861577364796228088571375917928190240967769281160157473952*y^17 - 166685599952726678522343496795579365206009324128582195896807372239596919600530819498001188135161251593858526056123800692358367023260775/38752703646409530389910506032576563400265791053713738448252084691188551623823430788682398114044285687958964095120483884640580078736976*y^16 - 1005117683090487724780329490971075509725205331471688615245447215127850698712958826745816310386414769585243170464661493329174938698020801/38752703646409530389910506032576563400265791053713738448252084691188551623823430788682398114044285687958964095120483884640580078736976*y^15 - 1052020642698182445972479915232823787280727696742928020322980208540273552105996019601763144639707908200427207725775914992213079273422375/77505407292819060779821012065153126800531582107427476896504169382377103247646861577364796228088571375917928190240967769281160157473952*y^14 + 2689203611583552855396424057507410142449499456023487585232068580586262327996715066848442619314936480839868845935373157207063445397737255/77505407292819060779821012065153126800531582107427476896504169382377103247646861577364796228088571375917928190240967769281160157473952*y^13 + 566362650561263944964604904549522808875566308517902293345423917260186341372452713604440069028031296184991514691156584999541296261258721/19376351823204765194955253016288281700132895526856869224126042345594275811911715394341199057022142843979482047560241942320290039368488*y^12 + 66203619789976842341821263600324222042033233411630731834885035767909937365928071830851353017557712809072534302961780683816259542202107/19376351823204765194955253016288281700132895526856869224126042345594275811911715394341199057022142843979482047560241942320290039368488*y^11 + 609192053881130506489804100267846728633036960255516858154624064104500502681490205976657759826506776270375095257739118972369452217598709/155010814585638121559642024130306253601063164214854953793008338764754206495293723154729592456177142751835856380481935538562320314947904*y^10 - 291717310036870673989220932511751396207100110916914043307106631027760402366342214955414457324200661322001765877423335926275590991160761/2500174428800614863865193937585584735501018777658950867629166754270229137020866502495638588002857141158642844846482831267134198628192*y^9 + 490668834610148887004073630280871527573549660239995859396400555761711269983382756724153645881263104007715771155413488028460915818066671/5000348857601229727730387875171169471002037555317901735258333508540458274041733004991277176005714282317285689692965662534268397256384*y^8 + 13447130021715475612985129323174900090484752181097701463170892761684886520914538267325242474541098557614740000137653868894530568997823/73534542023547495996035115811340727514735846401733849047916669243242033441790191249871723176554621798783613083720083272562770547888*y^7 - 3057108129109295579094058525319458414970598339274171648380097586236109351818265990790118773379646581151015692845206075440977333856947183/9688175911602382597477626508144140850066447763428434612063021172797137905955857697170599528511071421989741023780120971160145019684244*y^6 + 2670534598328455564368507074413784214484924493827510827483945577882973755223257441003439195477964595834916959350794805192084967032337193/19376351823204765194955253016288281700132895526856869224126042345594275811911715394341199057022142843979482047560241942320290039368488*y^5 + 148011736870464565729856540827648919365003643615917049160208519831489565320897643629858470873014563770296313375227064957115993361329547/19376351823204765194955253016288281700132895526856869224126042345594275811911715394341199057022142843979482047560241942320290039368488*y^4 - 384553338999318427250512303280655146071884739183751163468556618254244832801975069566839023075827841912957376930223094788785256537509199/19376351823204765194955253016288281700132895526856869224126042345594275811911715394341199057022142843979482047560241942320290039368488*y^3 + 245894096804989006504757110134273462327810140949248252520605410887862285319989732611063365510760569437833929966001428494145726584094881/77505407292819060779821012065153126800531582107427476896504169382377103247646861577364796228088571375917928190240967769281160157473952*y^2 + 107116900171958061239310951241990570540415599486960283014094284615399571101027187775092416116108565002822842323294994957905702136622741/155010814585638121559642024130306253601063164214854953793008338764754206495293723154729592456177142751835856380481935538562320314947904*y - 2800694728752023609547491628178510456146079135431494743209277741292885487608527312061595604602232469563676313632835263695506335076281/38752703646409530389910506032576563400265791053713738448252084691188551623823430788682398114044285687958964095120483884640580078736976 # 4 Loop Invariant 285274235003875055331377626242766415120525916943677912658565048292515838809913033212549707856301073300645670938034392123521264519424829999519884398206418226876430899388540065673833076857278794741569/15058037328059535097398410185149050915702247065697268085931021952139320525974988515422433542058726828347171195299220429413447041912682307753357592767491547091362991670855452785107070508383570370763776*y^21 + 20369735230310954025857904229888277136646489545245533801182071013484251249639863739211764568815401212956825455866927436657986983910589726626442156891330786754656849440150395779233154057106738415815463/112935279960446513230488076388617881867766852992729510644482664641044903944812413865668251565440451212603783964744153220600852814345117308150181945756186603185222437531415895888303028812876777780728320*y^20 + 205704397575979242197685528578829291064811807390024387805181826530636272671269903961581915068816008549867061070772050965456405986509280172693567926492953763039222703233534315273564264643096907120505507/225870559920893026460976152777235763735533705985459021288965329282089807889624827731336503130880902425207567929488306441201705628690234616300363891512373206370444875062831791776606057625753555561456640*y^19 + 582282335725374832139880460468502054049412177616820042323328963309901247852300942242481142669261375992118667714184966927250790143469038510978991509273547685918399653372151897510662464146028329305789747/225870559920893026460976152777235763735533705985459021288965329282089807889624827731336503130880902425207567929488306441201705628690234616300363891512373206370444875062831791776606057625753555561456640*y^18 + 201016188344256263902101315288404014719957801688601149318549140135541151621495523278840545164001133144242521983075017392666708515873983286769769396187745446430030337547314988672483568384863621192003083/56467639980223256615244038194308940933883426496364755322241332320522451972406206932834125782720225606301891982372076610300426407172558654075090972878093301592611218765707947944151514406438388890364160*y^17 - 83429423021264409963261739598489700432441369367882303553398915651029556255531462836842379515414576486503411922557302899140624267214928436830844269181736751712953039565847490196765668529488044453658029/112935279960446513230488076388617881867766852992729510644482664641044903944812413865668251565440451212603783964744153220600852814345117308150181945756186603185222437531415895888303028812876777780728320*y^16 - 368762570020644122629070496505280419533218386915166738088854314692756708741678252852886254957920896332580701406142614805014489035569639529901330757107397509195339823147562265217019664250671596391313383/37645093320148837743496025462872627289255617664243170214827554880348301314937471288556083855146817070867927988248051073533617604781705769383393981918728867728407479177138631962767676270958925926909440*y^15 - 392519474715866133277196050032864854416155837260261104418824605016182167486735719809019347879882036075950013280182302730969616168653671735436069432601313522136770670110443331842316062938733554872393369/56467639980223256615244038194308940933883426496364755322241332320522451972406206932834125782720225606301891982372076610300426407172558654075090972878093301592611218765707947944151514406438388890364160*y^14 + 2511196195061738246724022655279765480007666055142120798874446255030257264586250415005559744581868346599752802924962440323632465230870917264924418623403973982381797337336797801196093186200066331500815717/225870559920893026460976152777235763735533705985459021288965329282089807889624827731336503130880902425207567929488306441201705628690234616300363891512373206370444875062831791776606057625753555561456640*y^13 + 113211668852277688721864179857492165345494523685665526926394580885896759946761361062556867070254708144046253165451824602181631103266811571596028966168948375138783878310918773788552545614423396807993341/9411273330037209435874006365718156822313904416060792553706888720087075328734367822139020963786704267716981997062012768383404401195426442345848495479682216932101869794284657990691919067739731481727360*y^12 + 549195187564502948193824166869408062177355201279995926573819545615732787566101899137137038730647280539749046710037282304456087687558540499802126364604423121269817031332555427114496947456624440012786667/112935279960446513230488076388617881867766852992729510644482664641044903944812413865668251565440451212603783964744153220600852814345117308150181945756186603185222437531415895888303028812876777780728320*y^11 + 55602601908413422201534888661905269109336872185839624356174077191106447339463796935872331755782582492059219854656418285492079936690666526874829726470514812807132811119909784232543710392012193845845767/12548364440049612581165341820957542429751872554747723404942518293449433771645823762852027951715605690289309329416017024511205868260568589794464660639576289242802493059046210654255892090319641975636480*y^10 - 2519374523786866993273132692143397982049748632240880613579091012467667359177119185090517219274204374509283659084715916148611533239285979426395471892220835504423237834748146519165997313414659960984984031/56467639980223256615244038194308940933883426496364755322241332320522451972406206932834125782720225606301891982372076610300426407172558654075090972878093301592611218765707947944151514406438388890364160*y^9 + 1480220553435914100045106244508490367327623726801836013860461076164417349668058485993557667484156066119613468170703004964000255216912825962633804642736259352782977247621041822579303856152780272312486753/45174111984178605292195230555447152747106741197091804257793065856417961577924965546267300626176180485041513585897661288240341125738046923260072778302474641274088975012566358355321211525150711112291328*y^8 + 15933179654352484824197879559359086925294906192498380651700390596883186094179109286334824649132680815094250754221953615955348193833148434524323554669774763027821085537610580655046844164918475569302308017/225870559920893026460976152777235763735533705985459021288965329282089807889624827731336503130880902425207567929488306441201705628690234616300363891512373206370444875062831791776606057625753555561456640*y^7 - 4963975437494301095339940729880099481188549393993670606435532036457785759520411706056004049365105647660153881140658773197903796625196938862736954196735627221665560672708229733689841742334927249183405673/45174111984178605292195230555447152747106741197091804257793065856417961577924965546267300626176180485041513585897661288240341125738046923260072778302474641274088975012566358355321211525150711112291328*y^6 + 3727710819325582611403704716437520169785727805631859870224002078600275709416401789186624587169147005817002797467998110743584030367780355261776252000308775597069743874911404721395109378372237654193936741/75290186640297675486992050925745254578511235328486340429655109760696602629874942577112167710293634141735855976496102147067235209563411538766787963837457735456814958354277263925535352541917851853818880*y^5 - 204834503136586907084824197043794560521056054976670218067810452877041254869854676115432753537443402805150014868529251466675959885116062468046566051961874657090775636271733901179880157766352587895762699/37645093320148837743496025462872627289255617664243170214827554880348301314937471288556083855146817070867927988248051073533617604781705769383393981918728867728407479177138631962767676270958925926909440*y^4 - 2835211676743692916471521162480346356095007098375455437169070251354489931381754278804744238546584287634979036302865574668424636790764722479781511478679786492543706077519066397353928999679745471660067/941127333003720943587400636571815682231390441606079255370688872008707532873436782213902096378670426771698199706201276838340440119542644234584849547968221693210186979428465799069191906773973148172736*y^3 + 199978143288465884885504916318193940313643393130595735950488068650504886793427299154266765010766577470789048400485247523101855309621112930803648059767664185899496617265648220983399300814413772263842001/225870559920893026460976152777235763735533705985459021288965329282089807889624827731336503130880902425207567929488306441201705628690234616300363891512373206370444875062831791776606057625753555561456640*y^2 - 143655009032828785392307807805687159465582808820503660772184491620267378729553792506499849526888897341304259741712356176383566380293560294772024842529164335836615437471852716500402053143133581089403/1821536773555588923072388328848675513996239564398863074911010720016853289432458288155939541378071793751673934915228277751626658295888988841131966867035267793310039315022837030456500464723818996463360*y + 1495470652958365248656487227165916971083234874693933288021142177096660166397683402011206845787267948217817028084282870759537219117387617586843268928488001865399723564685668529797254809649479221290063/112935279960446513230488076388617881867766852992729510644482664641044903944812413865668251565440451212603783964744153220600852814345117308150181945756186603185222437531415895888303028812876777780728320