# Manifold: Census Knot K7_111

# Number of Tetrahedra: 7

# Number Field
x^24 - 23/7*x^23 - 295/7*x^22 + 53/7*x^21 + 112*x^20 - 1940/7*x^19 + 408/7*x^18 + 5672/7*x^17 - 5035/7*x^16 + 231*x^15 + 1153/7*x^14 - 17270/7*x^13 + 19888/7*x^12 + 6236/7*x^11 - 18104/7*x^10 + 7792/7*x^9 - 420*x^8 + 4593/7*x^7 - 3803/7*x^6 + 1359/7*x^5 + 17/7*x^4 - 27*x^3 + 93/7*x^2 - 34/7*x + 4/7 

# Approximate Field Generator
0.881527909381378 - 0.275559541306701*I

# Shape Parameters
-259050201811704256777670020223345988082671992421479/142856500379598853971342508975445495823048335544967*y^23 + 702366261848346644578643287288449459346982221960921/142856500379598853971342508975445495823048335544967*y^22 + 11300639315592488231553637625977319064763407380435671/142856500379598853971342508975445495823048335544967*y^21 + 4583686106160511516618158306298065296833828081887424/142856500379598853971342508975445495823048335544967*y^20 - 25510605926335617998816155905037549888497738913594685/142856500379598853971342508975445495823048335544967*y^19 + 57491120633905218209491510698543583795304164319584033/142856500379598853971342508975445495823048335544967*y^18 + 15908404704842946567598854890377257712302648580616168/142856500379598853971342508975445495823048335544967*y^17 - 196379203814544394033624724622496594499534837560142773/142856500379598853971342508975445495823048335544967*y^16 + 74884038646067830823109470071790104346253706645847100/142856500379598853971342508975445495823048335544967*y^15 - 32158224736755453114343417851644574301610589195832369/142856500379598853971342508975445495823048335544967*y^14 - 55507428560570639845709035947226218777832923580478525/142856500379598853971342508975445495823048335544967*y^13 + 605686601637877063845185778592675569760506801053926968/142856500379598853971342508975445495823048335544967*y^12 - 392478934702396773857544892130057455873741756715272924/142856500379598853971342508975445495823048335544967*y^11 - 409580862275659960965917966423387878365227136544855655/142856500379598853971342508975445495823048335544967*y^10 + 404670463000103971189456606988567813644595675761272924/142856500379598853971342508975445495823048335544967*y^9 - 90351628433022501102587732994029598493941664222208162/142856500379598853971342508975445495823048335544967*y^8 + 89104161779361029447918682820507972041126084358700004/142856500379598853971342508975445495823048335544967*y^7 - 123192281747760976220355669132181432029398112781667395/142856500379598853971342508975445495823048335544967*y^6 + 75732640068234169067213232086872956425543121671700179/142856500379598853971342508975445495823048335544967*y^5 - 16299724980237875586900684211424839245241778401577847/142856500379598853971342508975445495823048335544967*y^4 - 4749876834052849047804148275188950961043249836124799/142856500379598853971342508975445495823048335544967*y^3 + 3149101710623797915452766954046263494509499367254417/142856500379598853971342508975445495823048335544967*y^2 - 1864097010394093264042320686394408745363062125687714/142856500379598853971342508975445495823048335544967*y + 423047984241101426094264704352738560767910079768507/142856500379598853971342508975445495823048335544967

-571314217865788491643999718761487060792976514453137669/119428034317344641920042337503472434508068408515592412*y^23 + 454451230515491850200577611313187775591749237758261696/29857008579336160480010584375868108627017102128898103*y^22 + 6071035901376459381522876628855738579151494884300404310/29857008579336160480010584375868108627017102128898103*y^21 - 463629255899910209434114211552929930119215892712616544/29857008579336160480010584375868108627017102128898103*y^20 - 3420203924771754797244209811943489790703736616639932403/6285686016702349574739070394919601816214126763978548*y^19 + 6880754341984337363516987369265057007459106190985163897/5428547014424756450911015341066928841275836750708746*y^18 - 3849467697660356621333750967239052970166080267374112428/29857008579336160480010584375868108627017102128898103*y^17 - 117109424584954833764345706664547705131563409372603720844/29857008579336160480010584375868108627017102128898103*y^16 + 32853457659137285599011236932937952727345271595260987371/10857094028849512901822030682133857682551673501417492*y^15 - 3594042385909705265663787172359563677711673662189550261/5428547014424756450911015341066928841275836750708746*y^14 - 26973114347069450227605113228038533353265822882242788997/29857008579336160480010584375868108627017102128898103*y^13 + 1397558701893120609912394266432496882867275773146771321189/119428034317344641920042337503472434508068408515592412*y^12 - 368999382496714975450482055015458671710608665798593177401/29857008579336160480010584375868108627017102128898103*y^11 - 16095803491556826771957175717346518013592168537018684036/2714273507212378225455507670533464420637918375354373*y^10 + 18868232716748214274107982172613301535529701116167619128/1571421504175587393684767598729900454053531690994637*y^9 - 112190429237473302719609809569312474040025152555891836343/29857008579336160480010584375868108627017102128898103*y^8 + 40678415714716112391434633724074667118272644166106432177/29857008579336160480010584375868108627017102128898103*y^7 - 357287922750819070833678553296171978047400570399375142515/119428034317344641920042337503472434508068408515592412*y^6 + 12172642374687528160792076515203545729740149561475816131/5428547014424756450911015341066928841275836750708746*y^5 - 37030170703747574736546624519697972386044979440955821991/59714017158672320960021168751736217254034204257796206*y^4 - 7038973596505626464386333433686103575402466314518177719/59714017158672320960021168751736217254034204257796206*y^3 + 7179338220773808275348093080488303404905023197505777815/59714017158672320960021168751736217254034204257796206*y^2 - 2727508867669205566014686513711075265340852669202020983/59714017158672320960021168751736217254034204257796206*y + 2143189497302089544760124197432590553806792501654415217/119428034317344641920042337503472434508068408515592412

5224126848694229925302242299092916967617303684326128/2714273507212378225455507670533464420637918375354373*y^23 - 13498085976739201728172847747453833514827936205917753/2714273507212378225455507670533464420637918375354373*y^22 - 229741080033485634484382699340419836794242755548308155/2714273507212378225455507670533464420637918375354373*y^21 - 121493736592258073411583795546209933333596582548493161/2714273507212378225455507670533464420637918375354373*y^20 + 26560387259658870733645550552606463112306614996006005/142856500379598853971342508975445495823048335544967*y^19 - 1088088231112124471790411301487965504221214096653220577/2714273507212378225455507670533464420637918375354373*y^18 - 466182875516390424135314555375995927004662252273334063/2714273507212378225455507670533464420637918375354373*y^17 + 3920291477336711990952352019666771002503120455970224468/2714273507212378225455507670533464420637918375354373*y^16 - 989279501630786972784068325563137498227511169067395814/2714273507212378225455507670533464420637918375354373*y^15 + 452604550700574269719743641620550638258321567115715651/2714273507212378225455507670533464420637918375354373*y^14 + 1142739731275185909132146545861370461025165495737014765/2714273507212378225455507670533464420637918375354373*y^13 - 12125850919810318283898254999730580374805502225236516526/2714273507212378225455507670533464420637918375354373*y^12 + 6352320099260436016786889798544301564219585158747488928/2714273507212378225455507670533464420637918375354373*y^11 + 9340534932592453469758021750866461513660771342463702546/2714273507212378225455507670533464420637918375354373*y^10 - 365164928015759701443726449285761181805139515008446180/142856500379598853971342508975445495823048335544967*y^9 + 796361336813380133651100087411817893211425667821285448/2714273507212378225455507670533464420637918375354373*y^8 - 1798566326850840626503310806712563955749602463800039250/2714273507212378225455507670533464420637918375354373*y^7 + 2195088252919812530979705498471745161498943499235424583/2714273507212378225455507670533464420637918375354373*y^6 - 1100519943821137689267894988179734959167840796887687383/2714273507212378225455507670533464420637918375354373*y^5 + 161459758521398944230353053227242871736442523293500683/2714273507212378225455507670533464420637918375354373*y^4 + 139810005569518120709265550004911245220265811587762924/2714273507212378225455507670533464420637918375354373*y^3 - 77713221206454287983232434905474617752423358977203539/2714273507212378225455507670533464420637918375354373*y^2 + 39011977641967200544279899134355978208646532617789918/2714273507212378225455507670533464420637918375354373*y - 5514021646351520775099595681449413630615748149695424/2714273507212378225455507670533464420637918375354373

-26927264223811873143766817728802957474925549319505213/5428547014424756450911015341066928841275836750708746*y^23 + 71848162090301447513459023954656163859697253103906595/5428547014424756450911015341066928841275836750708746*y^22 + 1178583139634311903457446554620052056439791319493016383/5428547014424756450911015341066928841275836750708746*y^21 + 525248309215423677961495201068012701858445582205519735/5428547014424756450911015341066928841275836750708746*y^20 - 70156381829602100643865433472887480377864948078353843/142856500379598853971342508975445495823048335544967*y^19 + 2917338009707849980731741005316664277730550396765677513/2714273507212378225455507670533464420637918375354373*y^18 + 988891388548238025039135945205076922283901545310396263/2714273507212378225455507670533464420637918375354373*y^17 - 10246227874776553275952789445085728401334573323252355689/2714273507212378225455507670533464420637918375354373*y^16 + 6793459209080556232785215285077704218996850179893471085/5428547014424756450911015341066928841275836750708746*y^15 - 2454415001601522714585553055216248106506737320553957673/5428547014424756450911015341066928841275836750708746*y^14 - 5942424158087210290746296974550975496660299287365640211/5428547014424756450911015341066928841275836750708746*y^13 + 31388360443152803516465316480080200484477079603595355591/2714273507212378225455507670533464420637918375354373*y^12 - 18926838870996390428433299797010084468966503933258506330/2714273507212378225455507670533464420637918375354373*y^11 - 23028910599557936540628645135616316514140248073733288337/2714273507212378225455507670533464420637918375354373*y^10 + 1073540055144002276094827092830270744345570425032406534/142856500379598853971342508975445495823048335544967*y^9 - 3036698823780350308345203460806958292710591259783276377/2714273507212378225455507670533464420637918375354373*y^8 + 4043469551147249579162408558780565025117645062546669926/2714273507212378225455507670533464420637918375354373*y^7 - 12457649908212155160264229229627386509963872599276779513/5428547014424756450911015341066928841275836750708746*y^6 + 7090448765794573666073292219235049536510819381639447827/5428547014424756450911015341066928841275836750708746*y^5 - 1093531284463414282651362068903169059546789416864804309/5428547014424756450911015341066928841275836750708746*y^4 - 659546418224564711630199455746772065125708577270564261/5428547014424756450911015341066928841275836750708746*y^3 + 331305133999576207717616736500564263715842963097284377/5428547014424756450911015341066928841275836750708746*y^2 - 168929382116039488043529968620133672135042063373485633/5428547014424756450911015341066928841275836750708746*y + 12383070124147769329742725198890877054741656637300697/2714273507212378225455507670533464420637918375354373

-18244487541162451051919658509277747722154794084895366/2714273507212378225455507670533464420637918375354373*y^23 + 46723635322250936107717137988192753425245436273407293/2714273507212378225455507670533464420637918375354373*y^22 + 803873146260862356505897925701206392247059689256576045/2714273507212378225455507670533464420637918375354373*y^21 + 441017485001521176912444400767289722862588723096012157/2714273507212378225455507670533464420637918375354373*y^20 - 93278570961247776426025861494360523867790495213943597/142856500379598853971342508975445495823048335544967*y^19 + 3767689891557750752013958114088787265569759930307927857/2714273507212378225455507670533464420637918375354373*y^18 + 1784944964658001305696297257219572430154507151201123307/2714273507212378225455507670533464420637918375354373*y^17 - 13776908358655279262680692905171612361450934482959964268/2714273507212378225455507670533464420637918375354373*y^16 + 3148255466511919656279275662847909769311511362098364863/2714273507212378225455507670533464420637918375354373*y^15 - 1059910820116786045486318521111605199766346398069440679/2714273507212378225455507670533464420637918375354373*y^14 - 4366913330732367997229274925614460487737011338646506530/2714273507212378225455507670533464420637918375354373*y^13 + 42093213183068716649258061994381567724420650390396186435/2714273507212378225455507670533464420637918375354373*y^12 - 21172138504682503352747691061344198783535646168992021536/2714273507212378225455507670533464420637918375354373*y^11 - 34261598951638518762748131231634724798930907178031334653/2714273507212378225455507670533464420637918375354373*y^10 + 1312549941777992462907330675903242674159352836392324665/142856500379598853971342508975445495823048335544967*y^9 - 1022172556678482495056027604506580245451658840472332102/2714273507212378225455507670533464420637918375354373*y^8 + 4690504462504194241456015862762860432106783021798895074/2714273507212378225455507670533464420637918375354373*y^7 - 7815149845523645634711277639051925809713276745248853897/2714273507212378225455507670533464420637918375354373*y^6 + 3686923547076577609656492221990118364541778571508109654/2714273507212378225455507670533464420637918375354373*y^5 - 9296211633938180727614137323922722974944570219253435/2714273507212378225455507670533464420637918375354373*y^4 - 614548829614631177124779291316906530865194766619087570/2714273507212378225455507670533464420637918375354373*y^3 + 255054973319536970547006928852084768222779956378568883/2714273507212378225455507670533464420637918375354373*y^2 - 125256777539541707953750647742309944716721213060841110/2714273507212378225455507670533464420637918375354373*y + 19797294123750954406195972992519793528064949484036993/2714273507212378225455507670533464420637918375354373

-24527223434693522264121343042955813997795372296521849/5428547014424756450911015341066928841275836750708746*y^23 + 59099176194530595524187859937956279665167296080292071/5428547014424756450911015341066928841275836750708746*y^22 + 1087022396747099572838597111202335223370988241963579181/5428547014424756450911015341066928841275836750708746*y^21 + 762903006320515375076819939133296573311782469202883043/5428547014424756450911015341066928841275836750708746*y^20 - 56559116170578844896549043298363544280271822393750579/142856500379598853971342508975445495823048335544967*y^19 + 2431938673112777485247657522544103699653142148802546595/2714273507212378225455507670533464420637918375354373*y^18 + 1484575220063379290370549326505958944976371009194774343/2714273507212378225455507670533464420637918375354373*y^17 - 8795332513755334015287406456974347308210673695933612787/2714273507212378225455507670533464420637918375354373*y^16 + 2033553625713552431089722122238507346335739188672572059/5428547014424756450911015341066928841275836750708746*y^15 - 2746949116714773338840144730497448334371856495126502871/5428547014424756450911015341066928841275836750708746*y^14 - 6580557028228665753316461033971056442731475042237216917/5428547014424756450911015341066928841275836750708746*y^13 + 27471886482577443202573975669221151480306138998553480058/2714273507212378225455507670533464420637918375354373*y^12 - 10538874976956721473941281228545162330942943314569872777/2714273507212378225455507670533464420637918375354373*y^11 - 21939437523417521901989720376620474100419871795667448060/2714273507212378225455507670533464420637918375354373*y^10 + 693090520431201333537727182835984663730380588402286351/142856500379598853971342508975445495823048335544967*y^9 - 714465103185804419822859157589443724721903110349325925/2714273507212378225455507670533464420637918375354373*y^8 + 3640111547669702634080385440937995389215177881318338985/2714273507212378225455507670533464420637918375354373*y^7 - 9540497094273839840047729448439984576344570265501884587/5428547014424756450911015341066928841275836750708746*y^6 + 4539909742082784851945502327210791039326418701549623651/5428547014424756450911015341066928841275836750708746*y^5 - 210491910916951271360748737376767302150530851812487365/5428547014424756450911015341066928841275836750708746*y^4 - 533753278452979018504153688089949834580724912307759797/5428547014424756450911015341066928841275836750708746*y^3 + 208515665861124739462971984710199316503943975116750963/5428547014424756450911015341066928841275836750708746*y^2 - 107704750198052106579676734346330583636141724720805871/5428547014424756450911015341066928841275836750708746*y + 7424000425239694487396637850462082648745589417112959/2714273507212378225455507670533464420637918375354373

170190906738801289667001869135949084371991668085630151/10857094028849512901822030682133857682551673501417492*y^23 - 279718213360721766367379131927291473892984271835998149/5428547014424756450911015341066928841275836750708746*y^22 - 3595745928268736426222738515446708296501139572896655485/5428547014424756450911015341066928841275836750708746*y^21 + 673507647373123978152121212184317422548312523983659903/5428547014424756450911015341066928841275836750708746*y^20 + 1049676701323998004747418110093754478723097992838813067/571426001518395415885370035901781983292193342179868*y^19 - 23295725625093582966309616109813003025407900919222913057/5428547014424756450911015341066928841275836750708746*y^18 + 2041508359227109934175664037425014862501978420901764224/2714273507212378225455507670533464420637918375354373*y^17 + 35445470917931877645409796582026748470849613177707939583/2714273507212378225455507670533464420637918375354373*y^16 - 120219763780805380151131749605547777292540413772297728355/10857094028849512901822030682133857682551673501417492*y^15 + 6232016742937520922973826592234540338673651923418844810/2714273507212378225455507670533464420637918375354373*y^14 + 14768883942997184644065374014534071142342154778361463695/5428547014424756450911015341066928841275836750708746*y^13 - 421499437983049281493705014873906870844764018309123774605/10857094028849512901822030682133857682551673501417492*y^12 + 119835217985379800598093036421186003845804318011082514511/2714273507212378225455507670533464420637918375354373*y^11 + 49051383552471603305885248480255987888087219070477516069/2714273507212378225455507670533464420637918375354373*y^10 - 6020944953766651394926836457147598155442766512902430153/142856500379598853971342508975445495823048335544967*y^9 + 38060848711104984057605261957235252288566163308246812326/2714273507212378225455507670533464420637918375354373*y^8 - 12689654793821020003845636985816057604497783227534880942/2714273507212378225455507670533464420637918375354373*y^7 + 112078544800521138638466740962762729251370458086601017301/10857094028849512901822030682133857682551673501417492*y^6 - 21601417644668546586429669107022431196571445902589518016/2714273507212378225455507670533464420637918375354373*y^5 + 6344245974202476528745995624678210278179399213241921043/2714273507212378225455507670533464420637918375354373*y^4 + 964096021709080489686859280429502434709553130425955970/2714273507212378225455507670533464420637918375354373*y^3 - 1174978263309333704128588059174520755877700604772086887/2714273507212378225455507670533464420637918375354373*y^2 + 449687376372750799569279853769025281601974619617788137/2714273507212378225455507670533464420637918375354373*y - 676478507838547683207520452393016983208541858309215249/10857094028849512901822030682133857682551673501417492


# A Gluing Matrix
{{0,2,0,2,0,0,0},{2,-1,-1,0,1,0,0},{0,-1,0,0,0,0,0},{2,0,0,-3,-1,2,0},{0,2,0,-2,0,2,1},{0,0,0,2,1,0,0},{0,0,0,0,1,0,0}}

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

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

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

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

# 1 Loop Invariant
6662709738725054201717200892300718099005369098808875355/5428547014424756450911015341066928841275836750708746*y^23 - 8481701770571930225326897489428946832853959379162200062/2714273507212378225455507670533464420637918375354373*y^22 - 146668704423888703243376305495554629294431918828753271402/2714273507212378225455507670533464420637918375354373*y^21 - 83260206363611849059474046906621131536953787357481437128/2714273507212378225455507670533464420637918375354373*y^20 + 32801054815783384153651312619238298644079157403103065307/285713000759197707942685017950890991646096671089934*y^19 - 692767289078614429323841924962824592653249879766445745995/2714273507212378225455507670533464420637918375354373*y^18 - 318419246077215842930941037559074232315731149915193952623/2714273507212378225455507670533464420637918375354373*y^17 + 2464474428242939758727511203132128679499535208541345046169/2714273507212378225455507670533464420637918375354373*y^16 - 1146699438324179015065240588168566337012477861589758121791/5428547014424756450911015341066928841275836750708746*y^15 + 344034607397412197918346238198986813231988979795551259759/2714273507212378225455507670533464420637918375354373*y^14 + 804955413779591446732925627281181839354756417284938450856/2714273507212378225455507670533464420637918375354373*y^13 - 15249429994899791260032282664497333902838845466487076707247/5428547014424756450911015341066928841275836750708746*y^12 + 3823878540757504425707834232597591350785880544120233070659/2714273507212378225455507670533464420637918375354373*y^11 + 5800804414460284285626984747695409256207977077325282514021/2714273507212378225455507670533464420637918375354373*y^10 - 227968193006569671667600543544121806179291975804910062963/142856500379598853971342508975445495823048335544967*y^9 + 505090772875414616401015729334589656385000844618553531508/2714273507212378225455507670533464420637918375354373*y^8 - 1019395135314609320802406621971360516472380243788847852535/2714273507212378225455507670533464420637918375354373*y^7 + 2854870903762525222207097011617678807609582299359203172895/5428547014424756450911015341066928841275836750708746*y^6 - 752991096605103726908582809135891279370157581919920939713/2714273507212378225455507670533464420637918375354373*y^5 + 88142266638383009821237362563022619291598667883014373729/2714273507212378225455507670533464420637918375354373*y^4 + 74982222443090006852673170854571737695929798037259302344/2714273507212378225455507670533464420637918375354373*y^3 - 35267127935372251337245400463760399421758002210545380986/2714273507212378225455507670533464420637918375354373*y^2 + 18305706907129083743556625528654462684412174799588235212/2714273507212378225455507670533464420637918375354373*y - 5126432876888048191099350106690448695436052878000870367/5428547014424756450911015341066928841275836750708746

# 2 Loop Invariant
5316067973551069929262526708952366590015379512172682657963333059893962407679071086532700645053992702486852700581343845525263439/29566989591074783142908898971723244441239353488545663533066765984769889275762746152517118437071143408328421053797482984757164368*y^23 - 46348517420813567389152367390583938782287586787750830625724931927663965603223973913446041015522423256390466533138855427628328523/88700968773224349428726696915169733323718060465636990599200297954309667827288238457551355311213430224985263161392448954271493104*y^22 - 76568996887561868314081251219078239234879539842589900073113570730909464253017303775396972379850784527933834216006183992351697657/9855663197024927714302966323907748147079784496181887844355588661589963091920915384172372812357047802776140351265827661585721456*y^21 - 142688062381615843997701888770018548590522341000121211445446796512368663827953782967933613637600067827244295215323050148455490217/88700968773224349428726696915169733323718060465636990599200297954309667827288238457551355311213430224985263161392448954271493104*y^20 + 44938457701945857573692542380355003979485365497842192812206070681213944957547275890863462026455206081208590445800901965214224607/2334236020348009195492807813557098245361001591200973436821060472481833363876006275198719876610879742762770083194538130375565608*y^19 - 3765757660179938489346879503787267762358100556332314805940279684030347902712350364588845755309507427085638163178079558156878811001/88700968773224349428726696915169733323718060465636990599200297954309667827288238457551355311213430224985263161392448954271493104*y^18 - 421075504652595702081338503672487936867117398533657240308373848775767211196103377819173300924254887203785593783244227647409147639/88700968773224349428726696915169733323718060465636990599200297954309667827288238457551355311213430224985263161392448954271493104*y^17 + 788071851348851075056435545118670993863883931049152270268793841387163164576225296837558803133400935076920736456750058663083286421/5543810548326521839295418557198108332732378779102311912450018622144354239205514903596959706950839389061578947587028059641968319*y^16 - 6677732538599077056114927583545035130676712570646941566089727061379168097174119193996670504868048239759577345825587499639659598031/88700968773224349428726696915169733323718060465636990599200297954309667827288238457551355311213430224985263161392448954271493104*y^15 + 562042967596059764704786704455282484502398931748466453332989783601987500313001296470745575006231597960883247828901786085656478933/29566989591074783142908898971723244441239353488545663533066765984769889275762746152517118437071143408328421053797482984757164368*y^14 + 954834874145023192888622228329884981427389476805296344317318884919322807181902192118874543271701728225976024939398446238781130661/29566989591074783142908898971723244441239353488545663533066765984769889275762746152517118437071143408328421053797482984757164368*y^13 - 12786432064806777487652087908667250383360919163704907943487512524711011316153505680537489603120472550893002596671525157808021383407/29566989591074783142908898971723244441239353488545663533066765984769889275762746152517118437071143408328421053797482984757164368*y^12 + 7732129883534647199258125284102450146822862762256729995977645471415103060891981129470645308217724385116610982941911878527146366393/22175242193306087357181674228792433330929515116409247649800074488577416956822059614387838827803357556246315790348112238567873276*y^11 + 509932699794310153270328669711476337318778399516808308329992477484221056245382171653216456842471008104463500203893742761107737957/1847936849442173946431806185732702777577459593034103970816672874048118079735171634532319902316946463020526315862342686547322773*y^10 - 799234583622887014320086879172621842284553195334430292090218289417554433381434028019490183891611800356695683602577479257387750271/2334236020348009195492807813557098245361001591200973436821060472481833363876006275198719876610879742762770083194538130375565608*y^9 + 1861999252380205139003692834797354385649778470341221134611204235357298099934523071545220645729518183012238721414597606383725187675/22175242193306087357181674228792433330929515116409247649800074488577416956822059614387838827803357556246315790348112238567873276*y^8 - 365485247414540731093974482658276973417269454898098975678733846631643248593502907399192696792565975328624311585502903613613986768/5543810548326521839295418557198108332732378779102311912450018622144354239205514903596959706950839389061578947587028059641968319*y^7 + 1053742582827275784655542540102403757248864349272196061080526069434738530067440967046106450205292817322295961079899543779791476493/11087621096653043678590837114396216665464757558204623824900037244288708478411029807193919413901678778123157895174056119283936638*y^6 - 5220644476435251966886108700051789653476948152168171815975347037167726333973301250678725662986878610488733815054060328114655438931/88700968773224349428726696915169733323718060465636990599200297954309667827288238457551355311213430224985263161392448954271493104*y^5 + 1357864001967877207761769390293358605816247783551952444514216959774458581758048009773503012875404910757098943103077172072559387141/88700968773224349428726696915169733323718060465636990599200297954309667827288238457551355311213430224985263161392448954271493104*y^4 + 182689883527422276305855258506756185544847507606999876429281208007250632174875302835428468419776698314938421647445358731269778427/44350484386612174714363348457584866661859030232818495299600148977154833913644119228775677655606715112492631580696224477135746552*y^3 - 10230969241287701311213736518373667416294590749395681753734484325682174140786226908353965921883162570415860996713715189750352329/2687908144643162103900808997429385858294486680776878503006069634979080843251158741137919857915558491666220095799771180432469488*y^2 + 78460914124638218611200150509541639337145439609559026544811441642075659520668163428912292547234770590347483252758133859393128109/44350484386612174714363348457584866661859030232818495299600148977154833913644119228775677655606715112492631580696224477135746552*y - 8480641206722792744148006676678906663420158486412715224479283250764346295905521123484132640015854305670361905216338229321198119/14783494795537391571454449485861622220619676744272831766533382992384944637881373076258559218535571704164210526898741492378582184

# 3 Loop Invariant
72806662874657736236659512424889342780366585482976784312252225048040425631730991975700575138993176700412573013756155814930688104634894568826527072885290361129772765/1542957142122710439897243808947981155389026745626338445153957371914262103960391451446732427928041117258142453641272837488278322655701146117119323122689667160202536864*y^23 - 227024368572737116138949279484583710373234669722468979769316460590289480977640069299563704652663197333911081076267488376915700330420366022914104160080118277485307149/1542957142122710439897243808947981155389026745626338445153957371914262103960391451446732427928041117258142453641272837488278322655701146117119323122689667160202536864*y^22 - 6209611889775158399496631887837867874011788816580379837883709925726216027634118889878069276202655856107389538499662792408508319203843437890473736111830589380688423313/3085914284245420879794487617895962310778053491252676890307914743828524207920782902893464855856082234516284907282545674976556645311402292234238646245379334320405073728*y^21 + 4963112897378275648088192402689488287811879291033752893983056579697509377167210569939561132621731098714245051026395349477776125538523943753830209143427222372638353/280537662204129170890407965263269300979823044659334262755264976711684018901889354808496805077825657683298627934776879543323331391945662930385331476852666756400461248*y^20 + 425936155743638183556384374948599186314545459289350705414905452220142022415964098646306127117169174022063364778745789723944233864735727045781559833122837764267643673/81208270638037391573539147839367429231001407664544128692313545890224321261073234286670127785686374592533813349540675657277806455563218216690490690667877218958028256*y^19 - 12574807361835627137619762253250331833815967865374938226571295338626847275959828551213320858451277654096172832647111434132142691236773505831368015663251104510187711863/1028638094748473626598162539298654103592684497084225630102638247942841402640260967631154951952027411505428302427515224992185548437134097411412882081793111440135024576*y^18 + 2407963543372171289457654612029099944300767120602855813429142773476855138543137141612982954546489650068853659033239664411887831104445545420015564488830452767565728549/3085914284245420879794487617895962310778053491252676890307914743828524207920782902893464855856082234516284907282545674976556645311402292234238646245379334320405073728*y^17 + 19615701959242490185141124600468363188561343540537529085524345634827438459313822412952298307129123433605997139498042508229515816323796267296097181331597717560961800317/514319047374236813299081269649327051796342248542112815051319123971420701320130483815577475976013705752714151213757612496092774218567048705706441040896555720067512288*y^16 - 42662968750659247464764224005933420639190447306033078541339045046871529367797285929535298939206536830216732993111192277452951355138366939534057030973532353625542994035/1542957142122710439897243808947981155389026745626338445153957371914262103960391451446732427928041117258142453641272837488278322655701146117119323122689667160202536864*y^15 + 5363051000113880327527485718679320197325146184981722002196222072043359442639579154374933958591278904759393026161554571397632586224211444987019742386962214599973353441/771478571061355219948621904473990577694513372813169222576978685957131051980195725723366213964020558629071226820636418744139161327850573058559661561344833580101268432*y^14 + 26837023177620670626551516683545228704816328105777152188204229713870577762040620448353829828300105028970511240792559835848823830050653201462941266735875345021117780357/3085914284245420879794487617895962310778053491252676890307914743828524207920782902893464855856082234516284907282545674976556645311402292234238646245379334320405073728*y^13 - 88529491631884639437629694376896554253926958974316413628634092198592550838283105550412452702842293216563957121828348856339305352010451214568164333941778732213336740881/771478571061355219948621904473990577694513372813169222576978685957131051980195725723366213964020558629071226820636418744139161327850573058559661561344833580101268432*y^12 + 118573710856865190188793992304427196009348379363734719234928445560451883572030301141793937674469900178065424040443347194537004390487025006687560961565756264982314816911/1028638094748473626598162539298654103592684497084225630102638247942841402640260967631154951952027411505428302427515224992185548437134097411412882081793111440135024576*y^11 + 45729040275050531984382086859121818600035980552288053368336430934443689907316767887347331449748658252039852352833924917598704422104579533119812543174806708766319721411/771478571061355219948621904473990577694513372813169222576978685957131051980195725723366213964020558629071226820636418744139161327850573058559661561344833580101268432*y^10 - 18003864650019292524041655663819902291168659260868353915221292641364323559294673999920610786917537083125701484278603771241823490306829655700222283571191525760816268169/162416541276074783147078295678734858462002815329088257384627091780448642522146468573340255571372749185067626699081351314555612911126436433380981381335754437916056512*y^9 + 9904166049503047770207837846590604092988624884685071011643197065158465696542542123629481664442393125443829115499803790746424515321116412193858864739025782563725768815/280537662204129170890407965263269300979823044659334262755264976711684018901889354808496805077825657683298627934776879543323331391945662930385331476852666756400461248*y^8 - 48108834535756443010054366846613426822962814431777354626761335876037899554202322029494498566189767711050178020594653065284842872674611157236735885606554554805751764933/3085914284245420879794487617895962310778053491252676890307914743828524207920782902893464855856082234516284907282545674976556645311402292234238646245379334320405073728*y^7 + 88656497763982112731384938202149220003137797124644626364839871708761669590161911150221540503513105893814211994552116380965198418070696692120061898745868499162961361695/3085914284245420879794487617895962310778053491252676890307914743828524207920782902893464855856082234516284907282545674976556645311402292234238646245379334320405073728*y^6 - 64310888361651519581095157435896637742124349503485943665342629973467785100467299302491264860157751998468800799268775063008958949682270809984078427537966126739356063707/3085914284245420879794487617895962310778053491252676890307914743828524207920782902893464855856082234516284907282545674976556645311402292234238646245379334320405073728*y^5 + 18495212455507231361887606763333305238099823859381421886759116206798027028067022065526568228419859748372404316152802257303043315926601490490897014740181586691193293383/3085914284245420879794487617895962310778053491252676890307914743828524207920782902893464855856082234516284907282545674976556645311402292234238646245379334320405073728*y^4 + 48222858314952510305174604199967280822157232013641768694525043276491595950063765104046224174647688874955016078122093922660608513842548772084637508101701766940395199/57146560819359645922120141072147450199593583171345868339035458219046744591125609312841941775112633972523794579306401388454752690951894300634049004544061746674168032*y^3 - 112976329921998525331924169536922250433428702090323065381923760186120744188670360936949039758493137372657862337278515032418666939671266422892633845450416497330567047/114293121638719291844240282144294900399187166342691736678070916438093489182251218625683883550225267945047589158612802776909505381903788601268098009088123493348336064*y^2 + 623581837587021997345987152310159435783240966109649689768788046584455826847378055741137923876058311661050283102614822531084436427925189892190618450935307261975931549/1542957142122710439897243808947981155389026745626338445153957371914262103960391451446732427928041117258142453641272837488278322655701146117119323122689667160202536864*y - 112366323581426029603771458035857740793622986944385040400059173808611430682025500832543184793109504179589460009987519191629407717573141426325059528018312397746530475/771478571061355219948621904473990577694513372813169222576978685957131051980195725723366213964020558629071226820636418744139161327850573058559661561344833580101268432