# Manifold: Census Knot K8_72

# Number of Tetrahedra: 8

# Number Field
x^27 + 22*x^26 + 181*x^25 + 675*x^24 - 685*x^23 - 22552*x^22 - 139557*x^21 - 533123*x^20 - 1452898*x^19 - 2947602*x^18 - 4459764*x^17 - 4823810*x^16 - 3149280*x^15 + 14112*x^14 + 2741443*x^13 + 3421299*x^12 + 2248176*x^11 + 707941*x^10 - 109337*x^9 - 214335*x^8 - 88787*x^7 - 9952*x^6 + 5109*x^5 + 2196*x^4 + 242*x^3 - 40*x^2 - 13*x - 1 

# Approximate Field Generator
-0.708143619542120 - 1.12613520764166*I

# Shape Parameters
-34433337317020821508806535528243604/304925294360472009173888784291*y^26 - 81919393603962014087369748800053499/33880588262274667685987642699*y^25 - 5797939217545808735026428201297275477/304925294360472009173888784291*y^24 - 19816125713186182939519440087948039080/304925294360472009173888784291*y^23 + 35361727338649840364241274933649100203/304925294360472009173888784291*y^22 + 756111073517580850910878437394348800542/304925294360472009173888784291*y^21 + 1453231033429997241149516438373796309076/101641764786824003057962928097*y^20 + 15776673663792290882283623441576173680109/304925294360472009173888784291*y^19 + 13553329743567314398120785225562402906468/101641764786824003057962928097*y^18 + 77272320486913834709529458023922463705526/304925294360472009173888784291*y^17 + 107351488312885102942526573975118651032182/304925294360472009173888784291*y^16 + 240125139586342509954770672356384926574/720863580048397184808247717*y^15 + 5209783555015676671248498216153537703950/33880588262274667685987642699*y^14 - 29603588517421110657032108931998215818079/304925294360472009173888784291*y^13 - 25818205390110874753703742626375599027217/101641764786824003057962928097*y^12 - 23820509149712759556763033450595811147170/101641764786824003057962928097*y^11 - 11335093498395760773155987904591303326702/101641764786824003057962928097*y^10 - 3326104580354341800985528014938086667327/304925294360472009173888784291*y^9 + 2029345493488344103656683711192103321719/101641764786824003057962928097*y^8 + 416336465969961577115339855682764967684/33880588262274667685987642699*y^7 + 247455608009421511244235980033318378024/101641764786824003057962928097*y^6 - 15111602923481631947469752782082700459/33880588262274667685987642699*y^5 - 32526666230233618002320112647453481118/101641764786824003057962928097*y^4 - 14805569619060879547875931353898654198/304925294360472009173888784291*y^3 + 1295631094716673769236320702268077271/304925294360472009173888784291*y^2 + 621376205042808754553344781559722677/304925294360472009173888784291*y + 52844538196408325518016697576496057/304925294360472009173888784291

4920114885486285857932096297882359900/166048763073408146329025436867799*y^26 + 103376429661569226382693947762398604207/166048763073408146329025436867799*y^25 + 786876663346085947658650445961812427741/166048763073408146329025436867799*y^24 + 86649500453942958272745306757043949501/5725819416324418838931911616131*y^23 - 6085434859364800792263020767624562178299/166048763073408146329025436867799*y^22 - 105684644298737350234302694385578370422990/166048763073408146329025436867799*y^21 - 20014192357308324498951566896585990981898/5725819416324418838931911616131*y^20 - 2018292876561141301019436587538927848669486/166048763073408146329025436867799*y^19 - 4982026964650611699966272036006823254441506/166048763073408146329025436867799*y^18 - 23814612495943857486049820584548272895704/440447647409570679917839355087*y^17 - 11575101072923252245304108048916486623114448/166048763073408146329025436867799*y^16 - 203653692529159048656770400455619666448800/3532952405817194602745222061017*y^15 - 2466284692649006403566703802820263936907840/166048763073408146329025436867799*y^14 + 5558142464526913914222271306777727924386262/166048763073408146329025436867799*y^13 + 688084386193462611553500606160652760382792/12772981774877549717617341297523*y^12 + 6453911332026132641801780737219312026166716/166048763073408146329025436867799*y^11 + 67928067207052856388587166562426009642419/5725819416324418838931911616131*y^10 - 545628282147877999340340022990275259087875/166048763073408146329025436867799*y^9 - 732124751211711139450150995007583183342482/166048763073408146329025436867799*y^8 - 230338409634929925234035291226902317155503/166048763073408146329025436867799*y^7 + 10742859298671091682569300733175830739848/166048763073408146329025436867799*y^6 + 24374640380029545698280097031306845162205/166048763073408146329025436867799*y^5 + 4520127710852266789029958105774178355839/166048763073408146329025436867799*y^4 - 450965673121916184128499029825331368995/166048763073408146329025436867799*y^3 - 15825708715444519979888258694407566280/12772981774877549717617341297523*y^2 - 7327293001218144493527057828278283958/166048763073408146329025436867799*y + 1816273053484976056542353407017492950/166048763073408146329025436867799

256201751327132683411854933816499539631/1537128408871139398245573361610931*y^26 + 612046749336875535815685881179874052852/170792045430126599805063706845659*y^25 + 43620218793764886661929515138830174990537/1537128408871139398245573361610931*y^24 + 151142874871283304160443610936720373980297/1537128408871139398245573361610931*y^23 - 251000218221308108178386404230345862256713/1537128408871139398245573361610931*y^22 - 5652376751395837590471965624896427175558262/1537128408871139398245573361610931*y^21 - 10976847016687653437964152331878009545193203/512376136290379799415191120536977*y^20 - 120135173996624223212248660487631140174150123/1537128408871139398245573361610931*y^19 - 104073839419075373719700566530743746800449708/512376136290379799415191120536977*y^18 - 599224501593954352491875276994353303404880573/1537128408871139398245573361610931*y^17 - 843314383238662933667296075754550042231956675/1537128408871139398245573361610931*y^16 - 1926071224927972344446507477439877945425235/3633873307023970208618376741397*y^15 - 44452415381100472978870532037765253329081819/170792045430126599805063706845659*y^14 + 203245410143257806143236271273826434711051831/1537128408871139398245573361610931*y^13 + 200238929290756214145167780323019773188219910/512376136290379799415191120536977*y^12 + 192171596646582400324029505394409940625414068/512376136290379799415191120536977*y^11 + 96053303013806195706036293316621239378553187/512376136290379799415191120536977*y^10 + 37578187335868850761677255852303450999681016/1537128408871139398245573361610931*y^9 - 15573858834258791225618412866498215463600836/512376136290379799415191120536977*y^8 - 3508428094879036091904752551131868351665904/170792045430126599805063706845659*y^7 - 2329875384591088724828469926381530520128945/512376136290379799415191120536977*y^6 + 103899341432180722590293722043128666789030/170792045430126599805063706845659*y^5 + 280444845827757250257341005804569975015524/512376136290379799415191120536977*y^4 + 142842235775319233991123923653641249236099/1537128408871139398245573361610931*y^3 - 9203237967099212078736131776826088150968/1537128408871139398245573361610931*y^2 - 5647715448293159613294715293552453280433/1537128408871139398245573361610931*y - 513988634304428856729662120178019698050/1537128408871139398245573361610931

-1260934148732718418958689898475763150065/3244439012583684452277862652498939*y^26 - 27147630586347873720856557856687589471268/3244439012583684452277862652498939*y^25 - 215464316063632814316383687152832480525696/3244439012583684452277862652498939*y^24 - 749828654294044115169419553931774521527775/3244439012583684452277862652498939*y^23 + 1216215937292894080086932914763830974974679/3244439012583684452277862652498939*y^22 + 27864333673640815730343456766833401284292885/3244439012583684452277862652498939*y^21 + 162870540820157298912625888006061334273168165/3244439012583684452277862652498939*y^20 + 595662255746144703382683485323132470243527669/3244439012583684452277862652498939*y^19 + 1551996581301450459656804181391081138524808631/3244439012583684452277862652498939*y^18 + 2987235572747614095732135695594973427640393042/3244439012583684452277862652498939*y^17 + 4219520981396318941561069132708819389145787529/3244439012583684452277862652498939*y^16 + 87227775659618970360277417540125439324277126/69030617289014562814422609627637*y^15 + 2044989064130882136187939901898163568105924162/3244439012583684452277862652498939*y^14 - 977906390412010819092338109228189299989429846/3244439012583684452277862652498939*y^13 - 2996468086011748100452149729801732675668632204/3244439012583684452277862652498939*y^12 - 170926904937246768398746268895577038358488582/190849353681393203075168391323467*y^11 - 1469761735087166275420684370240922486819748762/3244439012583684452277862652498939*y^10 - 202569027119955220281462148403216243086444288/3244439012583684452277862652498939*y^9 + 232754594365160055273401649575580197229442784/3244439012583684452277862652498939*y^8 + 160860751266378241081074977383388233173375108/3244439012583684452277862652498939*y^7 + 36421161079801746830909618768819626659106632/3244439012583684452277862652498939*y^6 - 4535494905818573875557063688725190513654549/3244439012583684452277862652498939*y^5 - 4307386707418043346106053874818305042781417/3244439012583684452277862652498939*y^4 - 43934776162119820231206367545636942089414/190849353681393203075168391323467*y^3 + 1049558035059287502620767823959769742765/75452070060085684936694480290673*y^2 + 29204143454284480022109674557360184574251/3244439012583684452277862652498939*y + 2688895738919016385463759629155795659807/3244439012583684452277862652498939

-4326275107204769141562021060404168464944/3244439012583684452277862652498939*y^26 - 93056409120267190630061856462775763968006/3244439012583684452277862652498939*y^25 - 737420985582015204818076138415739358182617/3244439012583684452277862652498939*y^24 - 5117232602919513031882838730463254994319187/6488878025167368904555725304997878*y^23 + 8436252592726215567070591550087391843091667/6488878025167368904555725304997878*y^22 + 95497098803954104549253123246220107838438311/3244439012583684452277862652498939*y^21 + 1113860825235280310292698487650123164684921681/6488878025167368904555725304997878*y^20 + 2033331935481614849007293428889934349444892554/3244439012583684452277862652498939*y^19 + 5288576181663718746025733597617494220877178705/3244439012583684452277862652498939*y^18 + 20317870366484646269684069926528409887103294997/6488878025167368904555725304997878*y^17 + 14313035147485668169894540800743626628487732479/3244439012583684452277862652498939*y^16 + 589426722323840421015083533673792705324238863/138061234578029125628845219255274*y^15 + 13667761650306887706171249863200588845939430161/6488878025167368904555725304997878*y^14 - 3410626956539003448102633944055268007591185404/3244439012583684452277862652498939*y^13 - 20374162730749423609823143310374200703233962313/6488878025167368904555725304997878*y^12 - 1153715452234859677865920741985462418437644503/381698707362786406150336782646934*y^11 - 9837241464805418693230809642828119803518368995/6488878025167368904555725304997878*y^10 - 1303702866824546895308154168418932465740613347/6488878025167368904555725304997878*y^9 + 1584528981652375871481112639435123092472643597/6488878025167368904555725304997878*y^8 + 538801494332599649603724073054961278855196324/3244439012583684452277862652498939*y^7 + 240029657035995737600692169297730646381497565/6488878025167368904555725304997878*y^6 - 15751833176065053109757898416310591860036493/3244439012583684452277862652498939*y^5 - 28752366620124869929340973739649374626982091/6488878025167368904555725304997878*y^4 - 144371192663641807864673931859742821076440/190849353681393203075168391323467*y^3 + 3618017631059284816988827391385293968973/75452070060085684936694480290673*y^2 + 96748286456613380441131659522116403528116/3244439012583684452277862652498939*y + 17659686680440217978444440142258436475951/6488878025167368904555725304997878

-62282855138490130743962951833572021075904/230355169893441596111728248327424669*y^26 - 4022623324253655185577081649638628516850087/691065509680324788335184744982274007*y^25 - 31924115514499959668980415737405909710997508/691065509680324788335184744982274007*y^24 - 111080420190930581796562002447506928650839978/691065509680324788335184744982274007*y^23 + 60109549720429808799019729114928020363401828/230355169893441596111728248327424669*y^22 + 4128819496724380036964969170247125986615053669/691065509680324788335184744982274007*y^21 + 24130512911803880892844150822363746462419200105/691065509680324788335184744982274007*y^20 + 88243355067700532539480798687407446822868980359/691065509680324788335184744982274007*y^19 + 229894352610604867422849273265477478646402521885/691065509680324788335184744982274007*y^18 + 442439591072539911256826263816448075029572003359/691065509680324788335184744982274007*y^17 + 208283788501363219615591689251196669827570708340/230355169893441596111728248327424669*y^16 + 12913764683486164639406665489342109838973898972/14703521482560101879472015850686681*y^15 + 302521435210040603733180081543725638006305053500/691065509680324788335184744982274007*y^14 - 145114268234798434001744804305948522235124837800/691065509680324788335184744982274007*y^13 - 147942693276495793269677681721429320274355056005/230355169893441596111728248327424669*y^12 - 8434510057810050774877984459860350650382205288/13550304111378917418336955783966157*y^11 - 72478438802858237126930926614129571263042304566/230355169893441596111728248327424669*y^10 - 9957049802110057672879945158800725322080057608/230355169893441596111728248327424669*y^9 + 34485220483495127429406824272790219507242045060/691065509680324788335184744982274007*y^8 + 23799746623786714974863063756197807953710751442/691065509680324788335184744982274007*y^7 + 5380366676951087106282286415620196996050842454/691065509680324788335184744982274007*y^6 - 673506909749537096278845985313347903452710282/691065509680324788335184744982274007*y^5 - 637084711135459203594331459828536207847726694/691065509680324788335184744982274007*y^4 - 6487508649049831284843151653026166751203160/40650912334136752255010867351898471*y^3 + 51934102750493822600347718200292520319116/5357096974266083630505308100637783*y^2 + 4315848393092163294192843614893849975800115/691065509680324788335184744982274007*y + 396947964977085967531716343018611750499811/691065509680324788335184744982274007

-11*y^26 - 241*y^25 - 1969*y^24 - 7244*y^23 + 8210*y^22 + 247387*y^21 + 1512575*y^20 + 5724796*y^19 + 15448755*y^18 + 30970724*y^17 + 46109802*y^16 + 48602146*y^15 + 29818270*y^14 - 3304512*y^13 - 30141761*y^12 - 34892846*y^11 - 21308637*y^10 - 5539175*y^9 + 1910648*y^8 + 2248348*y^7 + 762322*y^6 + 20685*y^5 - 66151*y^4 - 19047*y^3 - 466*y^2 + 682*y + 104

y^26 + 22*y^25 + 181*y^24 + 675*y^23 - 685*y^22 - 22552*y^21 - 139557*y^20 - 533123*y^19 - 1452898*y^18 - 2947602*y^17 - 4459764*y^16 - 4823810*y^15 - 3149280*y^14 + 14112*y^13 + 2741443*y^12 + 3421299*y^11 + 2248176*y^10 + 707941*y^9 - 109337*y^8 - 214335*y^7 - 88787*y^6 - 9952*y^5 + 5109*y^4 + 2196*y^3 + 242*y^2 - 40*y - 11


# A Gluing Matrix
{{-1,-2,-2,0,0,2,-1,0},{-2,-3,-4,0,0,4,-2,0},{-2,-4,-5,0,0,6,-3,0},{0,0,0,0,1,-1,0,0},{0,0,0,1,0,2,0,0},{2,4,6,-1,2,-9,4,0},{-2,-4,-6,0,0,8,-3,-1},{0,0,0,0,0,0,-1,2}}

# B Gluing Matrix
{{1,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0},{0,0,1,0,0,0,0,0},{0,0,0,1,0,0,0,0},{0,0,0,0,1,0,0,0},{0,0,0,0,0,1,0,0},{0,0,0,0,0,0,2,0},{0,0,0,0,0,0,0,2}}

# nu Gluing Vector
{1, 1, 1, 0, 2, -1, 2, 0}

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

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

# 1 Loop Invariant
260102361011136442299093448249120355743186/3244439012583684452277862652498939*y^26 + 5592213470290738126535157384284471282654625/3244439012583684452277862652498939*y^25 + 88565383447460385517903200414385120114476249/6488878025167368904555725304997878*y^24 + 306859733499770867696765905943853020893559823/6488878025167368904555725304997878*y^23 - 254877897097454925344100729209009912614598113/3244439012583684452277862652498939*y^22 - 11476806126327404690155549810518718209427806875/6488878025167368904555725304997878*y^21 - 33430181514834548693693352944889484547375146456/3244439012583684452277862652498939*y^20 - 121953047864889462174296642295899394745697205095/3244439012583684452277862652498939*y^19 - 633862761275369067859264272982579294739452067279/6488878025167368904555725304997878*y^18 - 608227142873992337098196309368070251231185842702/3244439012583684452277862652498939*y^17 - 1711818141746052642638787731184949396824182249557/6488878025167368904555725304997878*y^16 - 35181600192267195603917049613479629668719523235/138061234578029125628845219255274*y^15 - 405786450553373720976619281893956035104697233705/3244439012583684452277862652498939*y^14 + 413096972164232777939173898827714221331587884159/6488878025167368904555725304997878*y^13 + 1219586043494654787269662052858318571949491723535/6488878025167368904555725304997878*y^12 + 68825752571269184664141612348270441432152180221/381698707362786406150336782646934*y^11 + 584541925943104567572678282997043328688576313869/6488878025167368904555725304997878*y^10 + 76025689345745184469165086478826964470254622159/6488878025167368904555725304997878*y^9 - 47444429906539730789828337643351230319953814967/3244439012583684452277862652498939*y^8 - 64057934239516719696132861739977038366571149323/6488878025167368904555725304997878*y^7 - 7080458723311538606198168661212656066849034090/3244439012583684452277862652498939*y^6 + 1902929039806922804151676139096995820293719839/6488878025167368904555725304997878*y^5 + 853179511953111637367387111446911125618418982/3244439012583684452277862652498939*y^4 + 8507439177397711400154686537209594579908555/190849353681393203075168391323467*y^3 - 217764686333244919751620244932733498878804/75452070060085684936694480290673*y^2 - 5722579656838987282142786816208912283684719/3244439012583684452277862652498939*y - 520239344713754815741181004453972597278855/3244439012583684452277862652498939

# 2 Loop Invariant
-1066367992428861167697961351042095191747506546863880751366985871536775054489916002386838285013338104829100338693845240713662769396475659/18009380663785449079871937852256092752836053676139209883003190165787511339287206815349412945149385168238955266686231450596589779336*y^26 - 15314126945144492998991887210108675043903889127481159886146930729301098533459620282370552879312891825177279252958289987135918175926070291/12006253775856966053247958568170728501890702450759473255335460110525007559524804543566275296766256778825970177790820967064393186224*y^25 - 364961764539153198485075702212259199871007157513570740745269846324205639729763879571864621036967455037403663559993450184177176706281200987/36018761327570898159743875704512185505672107352278419766006380331575022678574413630698825890298770336477910533372462901193179558672*y^24 - 1272272001940669191912532664912021350693564962001259761449353155563962450736234661629992950287749893300427101104567270439084998327545652989/36018761327570898159743875704512185505672107352278419766006380331575022678574413630698825890298770336477910533372462901193179558672*y^23 + 1022108432692761534376269892576010317571657812195147797427721828972572608327034784150585838319825790562577397393261195698661766687849403525/18009380663785449079871937852256092752836053676139209883003190165787511339287206815349412945149385168238955266686231450596589779336*y^22 + 5895022714947539649678742139726513622280134087453293444697176578038231719275622813545291237654602069724437082052354342766765648236116309891/4502345165946362269967984463064023188209013419034802470750797541446877834821801703837353236287346292059738816671557862649147444834*y^21 + 23001370364194540239637071965971984033946193609444563313507715691585959376985511274298436119540454389579394547250534731174860795256720192891/3001563443964241513311989642042682125472675612689868313833865027631251889881201135891568824191564194706492544447705241766098296556*y^20 + 505232642309003187017568681005819711065851214285457729658899685598517381028232778829666926092177934753152577497679473384194936193201660768379/18009380663785449079871937852256092752836053676139209883003190165787511339287206815349412945149385168238955266686231450596589779336*y^19 + 2635383970856802989793021557698659840632615659716692937722790097342065171188194063543337207411307307237962494731869473150837441043964939635979/36018761327570898159743875704512185505672107352278419766006380331575022678574413630698825890298770336477910533372462901193179558672*y^18 + 1692745166629803687850846664703343845642422466716896906771371548218617098039181807497929247546053531494174852293214809890489075943878475451989/12006253775856966053247958568170728501890702450759473255335460110525007559524804543566275296766256778825970177790820967064393186224*y^17 + 7183354249348905945579599306764332420270194874410447888542708558373673519714472523461204053888909274542857098657814145410408598126798674552353/36018761327570898159743875704512185505672107352278419766006380331575022678574413630698825890298770336477910533372462901193179558672*y^16 + 148823863878398354941919482248161614943757169649839948590695383005761938481013088336404528828249321330667979963049793910396514549713370650849/766356623990870173611571823500259266078129943665498292893752773012234525076051353844655870006356815669742777305797083004110203376*y^15 + 1169987134957159863929487078680118901644766841825608016897010608839641441424086947370454989559839426433073041749855917173458594085827692012395/12006253775856966053247958568170728501890702450759473255335460110525007559524804543566275296766256778825970177790820967064393186224*y^14 - 136587409693802358112886590500834860169742189535872126402923298205266626666281478354771011341349976866009380019679293254811992962396396211671/3001563443964241513311989642042682125472675612689868313833865027631251889881201135891568824191564194706492544447705241766098296556*y^13 - 1273794050389439595564900768486690986376378668692145334867644212937859872786685025308331462612212751684502249070461416037799475173056042583227/9004690331892724539935968926128046376418026838069604941501595082893755669643603407674706472574692584119477633343115725298294889668*y^12 - 291811377758810567353340685059885326949702617087926331523475231753835246681959162828717775492232852981715738015468070642804360122418209851765/2118750666327699891749639747324246206216006314839907045059198843033824863445553742982283875899927666851641796080733111834892915216*y^11 - 630145065548833245989015390511522723899701357484340354762651726649767311630877560953706192457636558350040249747832532957686671390450278891735/9004690331892724539935968926128046376418026838069604941501595082893755669643603407674706472574692584119477633343115725298294889668*y^10 - 354426297864192065322323867781134913023040597981882637188539058346531160151199265686760854758364077108494698800783659307178339426585759780979/36018761327570898159743875704512185505672107352278419766006380331575022678574413630698825890298770336477910533372462901193179558672*y^9 + 65932121290930824403333980021575859684545556237066810954137250427079956786665872541636505569763755716655888936233099758897547126874363753025/6003126887928483026623979284085364250945351225379736627667730055262503779762402271783137648383128389412985088895410483532196593112*y^8 + 275747732521406021428266793999542404438953516516384764473669547525033010339173600726465210413534643602330408480378002414297421520032177910695/36018761327570898159743875704512185505672107352278419766006380331575022678574413630698825890298770336477910533372462901193179558672*y^7 + 20985282016321538927317663193829555356812968273318171890918836827316564791574336196347165890738016885741826814701765596502580033524230409329/12006253775856966053247958568170728501890702450759473255335460110525007559524804543566275296766256778825970177790820967064393186224*y^6 - 3814264669580358674901769304770807835212793258493711242938907318411861791157793054899177743067451687977163596436616767023528446934821287109/18009380663785449079871937852256092752836053676139209883003190165787511339287206815349412945149385168238955266686231450596589779336*y^5 - 3698741536682625414459824670917617017426212155903240004631036975512099161850402017805080527878763795677065610525251088923625258662219185755/18009380663785449079871937852256092752836053676139209883003190165787511339287206815349412945149385168238955266686231450596589779336*y^4 - 9504378922766126933911199732797928027445784404002575635527718708290733793524723319270272438448244187426697816247376831989772341463533113/264843833290962486468704968415530775777000789354988380632399855379228107930694217872785484487490958356455224510091638979361614402*y^3 + 443330250940269655763106222487135212598871663065363806023325709715766840140838907003579716842986789992157616810359835263917301958880527/209411403067272663719441137816931311079488996234176859104688257741715248131246590876155964478481222886499479845188737797634764876*y^2 + 50338126951458106212670382609640600786859130407163688217760390290762383144745163255807541992777221956029543139933430706692339793498285959/36018761327570898159743875704512185505672107352278419766006380331575022678574413630698825890298770336477910533372462901193179558672*y + 1551324122573566334257628516666379503237127454641911828296039299458931127307420941704359072399717821274863391243323024469622835905980945/12006253775856966053247958568170728501890702450759473255335460110525007559524804543566275296766256778825970177790820967064393186224

# 3 Loop Invariant
-726887497751579451702924492652125200774464145989072510669441370042269151718998010821983303207943892375431752565546794142785894141036296106753022551961353588620856448028215337600612375/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^26 - 269909431529688372140271628946981331569958067405150805481105019624710095616275626492554640993713686137262966183248798971705961547937206391450548503767628551123163947541917292578417129/398211205894947525659369067375301608878831038100698907782320908692070631653320364192705758656309348177760403449427147925624468102391461608134673788780087690585708205881897624288*y^25 - 124313158691701692201915700596471515221149959876917905336071746983561862553844899278479155094690440592487796975429965813919761698880855688775642464192982024121300550637286074388634345007/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^24 - 433044528226000831031139749842606233730035959609470221544142556719112609330830310088639540623115717010059247310143406183720062120241799912941369462135483837199744353934006525660896055311/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^23 + 349308899490946817979875629821888657770864289493903786787216826389663750091621261488384124889949185024132854100805799279596198769305774886748966786989692567226350153794724484920230994363/11548124970953478244121702953883746657486100104920268325687306352070048317946290561588467001032971097155051700033387289843109574969352386635905539874622543026985537970575031104352*y^22 + 16069291120078688406202696015380557156622462234997591918314768187929325663139008051354277127705033529142120400761059399815541836100633798570362849640103025012304484692354255520410313919161/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^21 + 93996605604985113922919085529374565555756729145033493092666219168344338997180066663956137323868743609450105341752119249673301826239004069566755840533276296357137640608770441276537300625917/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^20 + 171980922737408948191296575916186422848895759565975480968633139592671526968309483884454848212354898010434160876367720105516090931606645477731969198098203376384038730069489153436354966300613/11548124970953478244121702953883746657486100104920268325687306352070048317946290561588467001032971097155051700033387289843109574969352386635905539874622543026985537970575031104352*y^19 + 56042724153342722925690245165447744086497281009701680141675661620346120291014990850812908340860811863942631683924718527334031050530666041811946663714919371681952947844700038299108242708647/1443515621369184780515212869235468332185762513115033540710913294008756039743286320198558375129121387144381462504173411230388696871169048329488192484327817878373192246321878888044*y^18 + 1726963822004978668405018661238476042199703827589488319631544388517770939376869533280953652845623961754552204794975513418277203056680150837920134875246625148025251507096882618055330057862671/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^17 + 305151454189222114559041205260532100293035528185227210884142607347027504638366129912541956934376448509606426609699057742962969091767148685258974103343107746478369400083748580466541839348845/2887031242738369561030425738470936664371525026230067081421826588017512079486572640397116750258242774288762925008346822460777393742338096658976384968655635756746384492643757776088*y^16 + 25261493899491034224986757903631897925320493540472745105932945340314741072775897638799948144094520670725909293582251086731014811059745036069674027277677292149462694887268646924402857013931/245704786616031452002589424550718013989065959679154645227389496852554219530772139608265255341127044620320248936880580634959778190837284822040543401587713681425224212139894278816*y^15 + 1188035515066283788092201661486824561758540978660571317834430425402958961184454652180092949932798657085990417748931783640143448505472949502014588384722937817760843366550435059693948645994275/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^14 - 561499807313330808718477545430189601138395235868065111956141171283444868642733707461875557058244698105777328677156389448757361901798638030700479650678055959260892774219463853064561431941049/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^13 - 1732804004707537495789240044851260216018491214462131729976052625393438365415844460856341166177237108007625090335227976488565330818898250638644990933432765070478312024536218384760760798297577/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^12 - 99037442832685950531942018940645904467470001576716872599336379224330792184277606713673277779519030167522853715620287064227196174116980170412723952695983486675199643779618806822478009283269/1358602937759232734602553288692205489116011777049443332433800747302358625640740066069231411886231893782947258827457328216836420584629692545400651749955593297292416231832356600512*y^11 - 106673556267810106367783764280621527320682780197820023574650295143667635869044340327350580225503324778659298186178824635187001749028688070961917957585851626482178925927627150599581136867281/2887031242738369561030425738470936664371525026230067081421826588017512079486572640397116750258242774288762925008346822460777393742338096658976384968655635756746384492643757776088*y^10 - 118658830834633110321681951922537244664438399669059123108584273968019248579123919712777499819236591370839327799707751932537281594284004817001923334827416823116346817381780830796279443553817/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^9 + 67318850057752125918517726005479793385720425875263087422129926630556050807106346872598702832112239468016198949054215589495644986641394449720204860728918194164476085653263000907047625201741/11548124970953478244121702953883746657486100104920268325687306352070048317946290561588467001032971097155051700033387289843109574969352386635905539874622543026985537970575031104352*y^8 + 93387091094515831033629798895782371904104905542224666537698705361698389560970380275384264097594212118272989799095662529833508303158214835217215024535650051717606549708011426432659322106069/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^7 + 21212569153014393387678821009011188141579960739231712289394120865615108085925049840793680781881409102775780457502319847230996222020402203765027009340190080026196654802188473293120137680755/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y^6 - 653850934821939055643874080286528196080277016831084044480963716259308917175828061796303869294128421053750153381288032811730248283760718326996867211017690762143727187577250512504515057947/5774062485476739122060851476941873328743050052460134162843653176035024158973145280794233500516485548577525850016693644921554787484676193317952769937311271513492768985287515552176*y^5 - 21573796188709629438013820189196043008844874002304100479236728566921192119658836477919795704013607915869942592218622566455081953901505027670793062679949315395031963879322423976537473689/199105602947473762829684533687650804439415519050349453891160454346035315826660182096352879328154674088880201724713573962812234051195730804067336894390043845292854102940948812144*y^4 - 25588526662373133042492902829515126062644569466993422023430031621533775948353696693249461099781873978943472966340316296868492509516524175798484215258786144072698190304448894708905025391/1358602937759232734602553288692205489116011777049443332433800747302358625640740066069231411886231893782947258827457328216836420584629692545400651749955593297292416231832356600512*y^3 + 606923738581053609203590292217920537708975407466796294414620312405681254497255465406700181616004945161555943629112576316761282831729890867609776336592396255078171887172404311140474563/537122091672254802052172230413197518952841865345128759334293318700932479904478630771556604699207958007211706978297083248516724417179180773763048366261513629162118045143024702528*y^2 + 16985050154993726948972994045723963834110889905521078511590922125168869537476051441501553489262498763091406629530710701834791753568660232366584561428131600378383859572710833632576408315/23096249941906956488243405907767493314972200209840536651374612704140096635892581123176934002065942194310103400066774579686219149938704773271811079749245086053971075941150062208704*y + 195662672969270835093036493746275915128053167281405067681326015373999355781936713967530223351617621274207789458056866756640650351596912347775408920602240319338878379603934991465209203/2887031242738369561030425738470936664371525026230067081421826588017512079486572640397116750258242774288762925008346822460777393742338096658976384968655635756746384492643757776088

# 4 Loop Invariant
-89273680922533722485846347262100208544037120827547785983054749377764426736791619614995454500592282546309748182663072877068389571083556195411838516298191270033895074369037536336354515952056811232482377084208168261041853048536020394576002366475962822251287518842914610340038781839219/1282037219674833649033136401981717677363763832675189947533654835274911867613267149581051807156910145915140268564269783638651316426064611233285686037999128135754822975402653666745160607466243842050689409081440646622028640201273931873547197687230551994490781866234308678760616960*y^26 - 1152126697338434006638604111163744272799932471529460262713192474538368179598015488016729997841620335924851170687692629033049263491070469014033693539723740505667122463481981328957934417808669209454639227038947852271862609236190223269121217302094700857746848935765364127524517266024583/769222331804900189419881841189030606418258299605113968520192901164947120567960289748631084294146087549084161138561870183190789855638766739971411622799476881452893785241592200047096364479746305230413645448864387973217184120764359124128318612338331196694469119740585207256370176*y^25 - 760809624833451122796181749588739271757248141597396688503358761710807220154721677378538391632617221453507048274389991442991312721926585185710070690308681775015354281818267654964020187157306398401974324824116219693597257759996036691289326165006815848240160438956839833963153600552091/64101860983741682451656820099085883868188191633759497376682741763745593380663357479052590357845507295757013428213489181932565821303230561664284301899956406787741148770132683337258030373312192102534470454072032331101432010063696593677359884361527599724539093311715433938030848*y^24 - 79188053271483661343895495749459922356354769251151561417428913100970239956528362339951106651861110661270761126973659943814682743413598982724009781022853487978155305369855628150809932757221199599205094425653347100787016112454766125021792492800242308474247282663472957564507673646436709/1923055829512250473549704602972576516045645749012784921300482252912367801419900724371577710735365218872710402846404675457976974639096916849928529056998692203632234463103980500117740911199365763076034113622160969933042960301910897810320796530845827991736172799351463018140925440*y^23 + 32648900445841903424297118267973255387048193758650056213584390716002181107761901188075696807888841360940687649472491126051575110558706288520309235403826553606737973418991692963942356950922825726981210368205534548871928832959762657803033135775910183644533457260284556666991303485027051/480763957378062618387426150743144129011411437253196230325120563228091950354975181092894427683841304718177600711601168864494243659774229212482132264249673050908058615775995125029435227799841440769008528405540242483260740075477724452580199132711456997934043199837865754535231360*y^22 + 1477941428365542661294901090546539872665318126639552822683645096760741069127559233915039135244071127697972000448299132110292632614080285637704949754991526279472757856638001278562164060759937990345606599074382341764679590917752719120829922927410383239382289144031211036480578358879141053/961527914756125236774852301486288258022822874506392460650241126456183900709950362185788855367682609436355201423202337728988487319548458424964264528499346101816117231551990250058870455599682881538017056811080484966521480150955448905160398265422913995868086399675731509070462720*y^21 + 5745847750858125437691501277399570468540955989853911042133793622094443242090738558741569836873550379226248651435204905839858917830604066985702960039802710641716232316807832826165405355606432599989556220140456795546866128354437799157660161761901701215279436534016932984564244634987045429/641018609837416824516568200990858838681881916337594973766827417637455933806633574790525903578455072957570134282134891819325658213032305616642843018999564067877411487701326833372580303733121921025344704540720323311014320100636965936773598843615275997245390933117154339380308480*y^20 + 62930829334870756710361828642466845853291811702003466686381605219694814071370305828927315214322908496087103204556333958895574036842830958180557666455694027007858508254223758932812655792511662172504787399214091823870491035205111761751278868373454257204466780638575298688448349312034568103/1923055829512250473549704602972576516045645749012784921300482252912367801419900724371577710735365218872710402846404675457976974639096916849928529056998692203632234463103980500117740911199365763076034113622160969933042960301910897810320796530845827991736172799351463018140925440*y^19 + 163671127351968340414893559408943396229373914577823083798227743807750585951459348287437427872938926397479935953122052764119225087381041721826157979556501196880146191351891609120710611664589767617064056183370297695110107695486930250872995674629860963766251509339714616995796712342456470583/1923055829512250473549704602972576516045645749012784921300482252912367801419900724371577710735365218872710402846404675457976974639096916849928529056998692203632234463103980500117740911199365763076034113622160969933042960301910897810320796530845827991736172799351463018140925440*y^18 + 69861983702039111539214392258311160500838871850206532602404023982410978878803482464074657243204627757351742769214161868541100968553332223234054001579445725378593150571198113426904612491498556665443564990394874685268493888851630030602238121315016560852712438810576679075915739160806586437/427345739891611216344378800660572559121254610891729982511218278424970622537755716527017269052303381971713422854756594546217105475354870411095228679333042711918274325134217888915053535822081280683563136360480215540676213400424643957849065895743517331496927288744769559586872320*y^17 + 110722722488448831877596298301261054016270552502112478954561990505907709465373504766598635643055323952508519459612626910455167280894447157439296501235553428207050184889784207592516882975683426836062282558509503884853660144745539087489407236174577386545479475079684240716640544327769911001/480763957378062618387426150743144129011411437253196230325120563228091950354975181092894427683841304718177600711601168864494243659774229212482132264249673050908058615775995125029435227799841440769008528405540242483260740075477724452580199132711456997934043199837865754535231360*y^16 + 18235801164242259660619856676395938741511248406560786433801331650751389182544515958138136155036453085472619932198934899881255445914426109371538702602273942167475390328103638865268504201212446229509652214412142853554541842250689503984279352424398432583951905759270485143877497781444440151/81832162957968105257434238424364958129601946766501486012786478847334800060421307420067136627036817824370655440272539381190509559110507099996958683276540093771584445238467255324159187710611309067065281430730254039703955757528123311077480703440247999648347778695806936942167040*y^15 + 422646375963772689539768617697124822086057343659806662012175567476311650428371402633459379973184205322880694857740605029016719392882377685650691921722388058194557253536980260416456243284626161956461990353199596664792441660511738275137994916442997918522532681052193504857602165070668802937/3846111659024500947099409205945153032091291498025569842600964505824735602839801448743155421470730437745420805692809350915953949278193833699857058113997384407264468926207961000235481822398731526152068227244321939866085920603821795620641593061691655983472345598702926036281850880*y^14 - 42270601177816652121913120295164410136775980429208776895199717249635212557446713459168544882127371321902080272831748434757172098435931614744553894390680070080711687999418799807406082260475864753993485664137550497725910917693844445430377460706108356900003820888761449919422211269341128621/769222331804900189419881841189030606418258299605113968520192901164947120567960289748631084294146087549084161138561870183190789855638766739971411622799476881452893785241592200047096364479746305230413645448864387973217184120764359124128318612338331196694469119740585207256370176*y^13 - 78818354737945835180588434473186237187533691790644734113541737238473658903792021761716291390225296059828000919734461231733833487506439177445095110420162627755882181297495925833108995238585063328195909963484829688775625674287012500594268661420162383750613827345791544874807634879374853871/480763957378062618387426150743144129011411437253196230325120563228091950354975181092894427683841304718177600711601168864494243659774229212482132264249673050908058615775995125029435227799841440769008528405540242483260740075477724452580199132711456997934043199837865754535231360*y^12 - 892319395158573391999616209855360147302183692244835808328525960440993233837744287768250671106646395208064594487751117350819559636135247793381787365513788590488006431120763883835714158906148083528112347403268978482544526211476051596617443086826672104619839058560019624756178746588397191/5656046557388971981028542949919342694251899261802308592060241920330493533587943306975228560986368290802089420136484339582285219526755637793907438402937330010683042538541119117993355621174605185517747393006355793920714589123267346500943519208370082328635802351033714759238016*y^11 - 50698760744666256855446263981182087305518132376296886694587832744786479749371819322620804402083698021207023152877623846583721534847696355955145752327914445333337414436619161825222311045110382731303511751962546371773393181798726267429836377383358072019317164508696613830352417662696150659/641018609837416824516568200990858838681881916337594973766827417637455933806633574790525903578455072957570134282134891819325658213032305616642843018999564067877411487701326833372580303733121921025344704540720323311014320100636965936773598843615275997245390933117154339380308480*y^10 - 20105365190650612704976947660858548776257076937978255549648063277689208406657857663291453201784355222875836344178515018855929981670077587451322567753828589157951707400358928575558110298854183063196254994580416895793870339978072270796853896350372502056963701134435420196380931043260929813/1923055829512250473549704602972576516045645749012784921300482252912367801419900724371577710735365218872710402846404675457976974639096916849928529056998692203632234463103980500117740911199365763076034113622160969933042960301910897810320796530845827991736172799351463018140925440*y^9 + 16351410249101060169826505569453358623727522080844512763099198616707485888074455465820139474888155565892797036719141404626835508229488614933243413524002137819903927303250278559645383714837661347017439670679538798189482191365427836915394922731195551030701357525815074164661087544105287723/1282037219674833649033136401981717677363763832675189947533654835274911867613267149581051807156910145915140268564269783638651316426064611233285686037999128135754822975402653666745160607466243842050689409081440646622028640201273931873547197687230551994490781866234308678760616960*y^8 + 3332469827467238547194158483137763824187866033348811424816769116033750711691182030485947049700634425442779504312920120934439978463311836324657141310748720249746786146962828044064822825612948447840285453641651832393183940376744895645169243647441279746533599152191132674444309413994355797/384611165902450094709940920594515303209129149802556984260096450582473560283980144874315542147073043774542080569280935091595394927819383369985705811399738440726446892620796100023548182239873152615206822724432193986608592060382179562064159306169165598347234559870292603628185088*y^7 + 3706740828774383509178783668954162094154390962715515969628305215699855959543624136696009516342369422811644715886081491963945369969133636547435114212538165564882135391661496672433769074575985161039955594123638097721651261114239746452709585222683525236912350611350683218199447577940699897/1923055829512250473549704602972576516045645749012784921300482252912367801419900724371577710735365218872710402846404675457976974639096916849928529056998692203632234463103980500117740911199365763076034113622160969933042960301910897810320796530845827991736172799351463018140925440*y^6 - 977136417259305607925206354515356307428325874395832523662137804486109293300599035606039236208611465380048099331978905788789321730435737952324935724757111981405426626668762225329823118538268360545506450726407732525517741208090734265242906108610981722121575481157553775140184695236702543/3846111659024500947099409205945153032091291498025569842600964505824735602839801448743155421470730437745420805692809350915953949278193833699857058113997384407264468926207961000235481822398731526152068227244321939866085920603821795620641593061691655983472345598702926036281850880*y^5 - 444465499076228061345530986193445489550623270454474193306531533984895249301742080623222547373070607056524919209641905106736388200066019986099001564030384061301637996346754171214456751023679314422909765084050897033862684917208382753820031789725176830008628174973668568468801668447745251/1923055829512250473549704602972576516045645749012784921300482252912367801419900724371577710735365218872710402846404675457976974639096916849928529056998692203632234463103980500117740911199365763076034113622160969933042960301910897810320796530845827991736172799351463018140925440*y^4 - 8914095251073435195449383713142341807468634517822233373377333182189451136225365618159947881681592390377163586599785250889818412891045201999148642071323762579018627775041139550982071254979592189703228737998909227157596344381352696722780237571790618883166076995575217855845911308644871/226241862295558879241141717996773707770075970472092343682409676813219741343517732279009142439454731632083576805459373583291408781070225511756297536117493200427321701541644764719734224846984207420709895720254231756828583564930693860037740768334803293145432094041348590369520640*y^3 + 9350293296542549375097427291157049853320139599330491958433481353494752087231572436772916768383585621689493219912558224533418940141847408308850937289236262988951694653928448396766159329795288694949987123370644588136358612984440978261616420368739844920071572246714084340765730213991/3726852382775679212305629075528249062103964629869738219574578009520092638410660318549569206851482982311454269082179603600730571006001776840946761738369558534170997021519342054491745951936755354798515724073955368087292558724633522888218597927995790681659249611146246159187840*y^2 + 5977837596324953461173356385987905709817971288461965139361681476279212298509073145925984863555014945817807491240461319800965369186654777307848508900199398525671164839134654445272174328606975859215091957198967780421054148343258035327818463065912257438254704611388523415157675285742803/3846111659024500947099409205945153032091291498025569842600964505824735602839801448743155421470730437745420805692809350915953949278193833699857058113997384407264468926207961000235481822398731526152068227244321939866085920603821795620641593061691655983472345598702926036281850880*y + 272521436365246408412534073262630716508431493208258225994139120003295895189699043732644601345833378273353742685873729886653573113591769616254819249683999836263367543436230137370342425234494322430005569269691035739277019118490590335103875549626882476975274390891914798352047405765253/1923055829512250473549704602972576516045645749012784921300482252912367801419900724371577710735365218872710402846404675457976974639096916849928529056998692203632234463103980500117740911199365763076034113622160969933042960301910897810320796530845827991736172799351463018140925440