# Manifold: Census Knot K7_13 # Number of Tetrahedra: 7 # Number Field x^24 + 10*x^23 - 61*x^22 + 135*x^21 - 2411*x^20 + 10036*x^19 + 1107*x^18 - 65760*x^17 + 59192*x^16 + 98482*x^15 - 179731*x^14 + 16806*x^13 + 291580*x^12 - 107633*x^11 - 290506*x^10 + 37103*x^9 + 143159*x^8 + 9355*x^7 - 32389*x^6 - 4999*x^5 + 3252*x^4 + 385*x^3 - 188*x^2 + 7*x + 1 # Approximate Field Generator 2.65536054091161 - 1.33947550015724*I # Shape Parameters -358359377717521177378598249580544591225033127449371051897508934305/336064808395431621669241884848173449093802827500740854335803778197*y^23 - 3650462476710171124602551323348036426028807338359511716725903241562/336064808395431621669241884848173449093802827500740854335803778197*y^22 + 21181409404274414400875301644661807995996981920388242364658280935708/336064808395431621669241884848173449093802827500740854335803778197*y^21 - 44399887144810004843197963291773969346263900714522558293570060171412/336064808395431621669241884848173449093802827500740854335803778197*y^20 + 855555830413366512794521362359051531594610757752926920859267173763990/336064808395431621669241884848173449093802827500740854335803778197*y^19 - 3436468975914240103180520282674536416880871150881400960916280481534900/336064808395431621669241884848173449093802827500740854335803778197*y^18 - 1044413048113093196664011695063174548223254890442274205098375953171774/336064808395431621669241884848173449093802827500740854335803778197*y^17 + 23398204001584844720516981387867844724671246542225748453251895114034361/336064808395431621669241884848173449093802827500740854335803778197*y^16 - 16847556386052071096128642184875557548920002465894731353200789626894582/336064808395431621669241884848173449093802827500740854335803778197*y^15 - 38602795294877286166171791615725473308518283013050850283186648388781157/336064808395431621669241884848173449093802827500740854335803778197*y^14 + 57379323346345496105728263647315250739390679470533354214765539615923556/336064808395431621669241884848173449093802827500740854335803778197*y^13 + 4884213781300117271052084327156997931563904685591845096115897377402859/336064808395431621669241884848173449093802827500740854335803778197*y^12 - 104034720100364561281798773343573059644930865148504137495453235919014931/336064808395431621669241884848173449093802827500740854335803778197*y^11 + 19302336495418522818033142707269070975887022782791811088558379199149095/336064808395431621669241884848173449093802827500740854335803778197*y^10 + 108357123056640077027320237897595037097784203516340627144276519525856722/336064808395431621669241884848173449093802827500740854335803778197*y^9 + 6600961273159323383226608112106810610331909198094138739750751821602934/336064808395431621669241884848173449093802827500740854335803778197*y^8 - 50647248179259631981913403434888476514108459915666918531492074358385804/336064808395431621669241884848173449093802827500740854335803778197*y^7 - 12704617709757189468990263496806101089453458503201115857596824183422329/336064808395431621669241884848173449093802827500740854335803778197*y^6 + 9460839046785424915546042299836929436770888259118653243231747170003245/336064808395431621669241884848173449093802827500740854335803778197*y^5 + 3556340166713138555527366483547422572249168417883749212915340380037991/336064808395431621669241884848173449093802827500740854335803778197*y^4 - 536243508078968865648334554083790389232008338177966694535753206369762/336064808395431621669241884848173449093802827500740854335803778197*y^3 - 237990670300998973088186854116683961561031379819903431524070778222811/336064808395431621669241884848173449093802827500740854335803778197*y^2 + 25260260901186512180197649049508984115710675521886006284729778631679/336064808395431621669241884848173449093802827500740854335803778197*y + 2186460644985756298131763997214714835256085619610214404343407237510/336064808395431621669241884848173449093802827500740854335803778197 -152327229363528756287383072449902260531929832278459324637640506306/336064808395431621669241884848173449093802827500740854335803778197*y^23 - 1560997444248034573886398903563624888616350276603303685371737260660/336064808395431621669241884848173449093802827500740854335803778197*y^22 + 8906308631751314964941806037661506849013192866649915416661175012928/336064808395431621669241884848173449093802827500740854335803778197*y^21 - 18348744099534928407974287482937185667399063346008704302586624366159/336064808395431621669241884848173449093802827500740854335803778197*y^20 + 362662407324388245711874921349798984382778150254247379691991509595375/336064808395431621669241884848173449093802827500740854335803778197*y^19 - 1438827085198927485975660576927842265797051725157063943641073416448234/336064808395431621669241884848173449093802827500740854335803778197*y^18 - 527214035507749665562413546152341118492800201123782356204848048154111/336064808395431621669241884848173449093802827500740854335803778197*y^17 + 9895272198178388342669360038679638957593825040889624693398802504797505/336064808395431621669241884848173449093802827500740854335803778197*y^16 - 6562670218208373967682147396180516279508686597783959382595563239565510/336064808395431621669241884848173449093802827500740854335803778197*y^15 - 16685577045781935873557611062172760848673401960007903363363017248993769/336064808395431621669241884848173449093802827500740854335803778197*y^14 + 23282604241025652501878410746815250502069667863917415471383525211344470/336064808395431621669241884848173449093802827500740854335803778197*y^13 + 3298141053653365614829358081058164384816968612456913257561252158569225/336064808395431621669241884848173449093802827500740854335803778197*y^12 - 43722903031985268129371484086118687274015033907950078836431470175903860/336064808395431621669241884848173449093802827500740854335803778197*y^11 + 5553469071357699283177163116392178803207832856975440548234462431951304/336064808395431621669241884848173449093802827500740854335803778197*y^10 + 45860914886382550065430927824579709933192290563311874695459126968939973/336064808395431621669241884848173449093802827500740854335803778197*y^9 + 5701360486770658392518464631039282361925014598552190441857028229500328/336064808395431621669241884848173449093802827500740854335803778197*y^8 - 20632818458477237956403397234483288944264351212625943058119563225661697/336064808395431621669241884848173449093802827500740854335803778197*y^7 - 6610244287375816146705599691359822317754720840890268092285239871268616/336064808395431621669241884848173449093802827500740854335803778197*y^6 + 3383331644808457317752041308010851734396952894961199224074799395517345/336064808395431621669241884848173449093802827500740854335803778197*y^5 + 1649890131323140813107366482914714053067632046240061390224321740275459/336064808395431621669241884848173449093802827500740854335803778197*y^4 - 93164387069249878613385756844031389338419782239520150845842699092060/336064808395431621669241884848173449093802827500740854335803778197*y^3 - 92469415393661229130455629105416957250179090772414994944427175865259/336064808395431621669241884848173449093802827500740854335803778197*y^2 + 5106031443452775346023221279666165841418063625321583593482871314395/336064808395431621669241884848173449093802827500740854335803778197*y + 1034761399530040240461337377626769824095744389179259459843446482174/336064808395431621669241884848173449093802827500740854335803778197 220597003462899758873386914018353209944728893493520723314922371788/3024583275558884595023176963633561041844225447506667689022234003773*y^23 + 791634089116796465311729378439047360284027100109679726660497887907/1008194425186294865007725654544520347281408482502222563007411334591*y^22 - 11848676934650037924177853365867837269215748957451536174224000262836/3024583275558884595023176963633561041844225447506667689022234003773*y^21 + 18695695040139468993646251445666787766373294888374921915159258567775/3024583275558884595023176963633561041844225447506667689022234003773*y^20 - 55971821599072913295885807844367909263246130429714916081541672120619/336064808395431621669241884848173449093802827500740854335803778197*y^19 + 1793158365311328591101860202048857604799484911882064269999449675021509/3024583275558884595023176963633561041844225447506667689022234003773*y^18 + 2142896833213741775283574214708268943279240056850933113333783940267271/3024583275558884595023176963633561041844225447506667689022234003773*y^17 - 15228943465446597713156033789056805781660713237795002250507301626529527/3024583275558884595023176963633561041844225447506667689022234003773*y^16 + 2285203452371956400748706189072887545263234387545631941009683191166266/3024583275558884595023176963633561041844225447506667689022234003773*y^15 + 12275506610022906781956574904389281725876254149929106163277692195533374/1008194425186294865007725654544520347281408482502222563007411334591*y^14 - 30088045723145130696037547914534681544129401051522630689425310733797406/3024583275558884595023176963633561041844225447506667689022234003773*y^13 - 30863483789952352632872375243395735999693527034884110143187511774840161/3024583275558884595023176963633561041844225447506667689022234003773*y^12 + 9224490815240968891060200236024963585468301705938665511390576698100683/336064808395431621669241884848173449093802827500740854335803778197*y^11 + 16245960865572585489028048156353732296596347946845381684077918846125213/3024583275558884595023176963633561041844225447506667689022234003773*y^10 - 100174687639809012468314262589794909302407481294703877312022257632657191/3024583275558884595023176963633561041844225447506667689022234003773*y^9 - 24648992774225472018246821117782749376444969987158041582972392243270829/3024583275558884595023176963633561041844225447506667689022234003773*y^8 + 51621989483708612873692716259488388018712701950072449041564233479753107/3024583275558884595023176963633561041844225447506667689022234003773*y^7 + 6045525463152610420220904029280639641596846584009234194099532441020921/1008194425186294865007725654544520347281408482502222563007411334591*y^6 - 11166858098307066167806873487308086269650070396434781866358521176965854/3024583275558884595023176963633561041844225447506667689022234003773*y^5 - 1617999872110725735910636992164542924252731046011338643752580040411307/1008194425186294865007725654544520347281408482502222563007411334591*y^4 + 98841057424302534586313667531677623172025535361108335434025605706445/336064808395431621669241884848173449093802827500740854335803778197*y^3 + 431817197432662448211399429976465948374893547746564265991896547670548/3024583275558884595023176963633561041844225447506667689022234003773*y^2 - 5594994839300283030417250498630878505077873618219365414390185373564/336064808395431621669241884848173449093802827500740854335803778197*y - 2952678913187310440164762877384785562014121731151626686137218812845/3024583275558884595023176963633561041844225447506667689022234003773 8899345883778335589961736705579475815999374148662361341229007604005/1344259233581726486676967539392693796375211310002963417343215112788*y^23 + 22669717792953660997365763890481571563109706072198301403146984608135/336064808395431621669241884848173449093802827500740854335803778197*y^22 - 262868995514444900929153682091870217393761407138339746609810977457539/672129616790863243338483769696346898187605655001481708671607556394*y^21 + 550660419341695378984825341655699282098066841304704281100962071940129/672129616790863243338483769696346898187605655001481708671607556394*y^20 - 10622368828256786260275076047083085569534886960659503306058880889276793/672129616790863243338483769696346898187605655001481708671607556394*y^19 + 85284147632579151330673217959057898933028012023601797781130323902654227/1344259233581726486676967539392693796375211310002963417343215112788*y^18 + 13062569881570038950427084932031691648281247941169370198386120220399973/672129616790863243338483769696346898187605655001481708671607556394*y^17 - 290379903462137755172097920226576653282113901194639956774988270404468713/672129616790863243338483769696346898187605655001481708671607556394*y^16 + 104153128200637709398379777731710241188644494961667224112697830383974600/336064808395431621669241884848173449093802827500740854335803778197*y^15 + 239671117476256559703339638795793833549906986298824120088120339788048777/336064808395431621669241884848173449093802827500740854335803778197*y^14 - 1420244101048673243945288461874886358871739655074088382927444849519896453/1344259233581726486676967539392693796375211310002963417343215112788*y^13 - 62549071158996495228685608057490840987040929197349516367607719863379811/672129616790863243338483769696346898187605655001481708671607556394*y^12 + 2579422208270534870226890907707157630514943107251712925772986417330744019/1344259233581726486676967539392693796375211310002963417343215112788*y^11 - 234207715590191601031946551648346797951775183003992338191958458203000655/672129616790863243338483769696346898187605655001481708671607556394*y^10 - 672316893180818906796004564990991831266027504884096479549001908802371331/336064808395431621669241884848173449093802827500740854335803778197*y^9 - 176423099580883209705280388212975544956288646167605958045894320374454521/1344259233581726486676967539392693796375211310002963417343215112788*y^8 + 1256397181112326213676496659861419219285790440736902222609475057202670585/1344259233581726486676967539392693796375211310002963417343215112788*y^7 + 160995441296450855258687353860964690957046033947777034745120028845482001/672129616790863243338483769696346898187605655001481708671607556394*y^6 - 234524029691406252470291481349449410089048833525129136536643361908569549/1344259233581726486676967539392693796375211310002963417343215112788*y^5 - 90495215045341520680681738070372470003399577570158110035509137625094939/1344259233581726486676967539392693796375211310002963417343215112788*y^4 + 13179357025765914857804412530440389745904053943960266838885417531051229/1344259233581726486676967539392693796375211310002963417343215112788*y^3 + 6348658279761934418238257117970575686210861189441109481643335878300765/1344259233581726486676967539392693796375211310002963417343215112788*y^2 - 566477615457979876318635501176192275273445948268799535657424660622297/1344259233581726486676967539392693796375211310002963417343215112788*y - 71637956977838744923463694883050409720571715239175287122241588893703/1344259233581726486676967539392693796375211310002963417343215112788 -284519988818228677178939544346344220313676276955461701751945630508/1008194425186294865007725654544520347281408482502222563007411334591*y^23 - 960084261266571702062976426784008493668021386819976471970388682630/336064808395431621669241884848173449093802827500740854335803778197*y^22 + 17000496396863445148879511512757131319959123422206258309142744459712/1008194425186294865007725654544520347281408482502222563007411334591*y^21 - 36318627742980612938198492834251183849704510852768346433208389084575/1008194425186294865007725654544520347281408482502222563007411334591*y^20 + 227178761808346646524482114094596508183579936493744111342144097492446/336064808395431621669241884848173449093802827500740854335803778197*y^19 - 2771565674354627968430806563369796744257485047756694847942750441885955/1008194425186294865007725654544520347281408482502222563007411334591*y^18 - 655496082559532412330671246438955254116313771695702628709852786672332/1008194425186294865007725654544520347281408482502222563007411334591*y^17 + 18623671455727292104692958799228873001367356777533841263337230305681523/1008194425186294865007725654544520347281408482502222563007411334591*y^16 - 14542425573258920722702824925758024202749823676697133042643028481241938/1008194425186294865007725654544520347281408482502222563007411334591*y^15 - 9923193814698956411994076280880288700091336860467606465102828977599414/336064808395431621669241884848173449093802827500740854335803778197*y^14 + 47385974461009643860484622669776414946221730823844166738781684937818267/1008194425186294865007725654544520347281408482502222563007411334591*y^13 + 977391767871068527386313168541443960006597026829488595172982049398692/1008194425186294865007725654544520347281408482502222563007411334591*y^12 - 27522931571272320923128790456579257565025887705198975520405979485206194/336064808395431621669241884848173449093802827500740854335803778197*y^11 + 20364351280735777840454473001432579597523359877166930084293286765020149/1008194425186294865007725654544520347281408482502222563007411334591*y^10 + 84804965893948187246301281667816565170238019435731589664136816277203019/1008194425186294865007725654544520347281408482502222563007411334591*y^9 + 349256236246647939735247034779133667000719126636535735573797521574198/1008194425186294865007725654544520347281408482502222563007411334591*y^8 - 40384176151183800659837974173553800724800805376140085649132639249022042/1008194425186294865007725654544520347281408482502222563007411334591*y^7 - 2712240105186603772923370566273603276322233234685861399970607239806684/336064808395431621669241884848173449093802827500740854335803778197*y^6 + 7998499364753274702215791563192280699013885903800024289487415728928954/1008194425186294865007725654544520347281408482502222563007411334591*y^5 + 859655939252127488886264890011337889941808749733990660152386674766572/336064808395431621669241884848173449093802827500740854335803778197*y^4 - 179966341244053489545035848173062945510439520576877033984865076994336/336064808395431621669241884848173449093802827500740854335803778197*y^3 - 194422968989272018755906946244485690419022004312798969510202433779457/1008194425186294865007725654544520347281408482502222563007411334591*y^2 + 7388974047739011713230708127225345638778181423035626549361114275063/336064808395431621669241884848173449093802827500740854335803778197*y + 2875983758664737244886527588210388284946142530426096023079006846679/1008194425186294865007725654544520347281408482502222563007411334591 132046428787455839705693561350475855366113331274586305560026421340/336064808395431621669241884848173449093802827500740854335803778197*y^23 + 1353866178385212577701309537875483369597004876362282376825745567440/336064808395431621669241884848173449093802827500740854335803778197*y^22 - 7713096317133148060618005736642023110940931037520051609870376052751/336064808395431621669241884848173449093802827500740854335803778197*y^21 + 15869052034230476030650994371068213040518868607792734360524656817618/336064808395431621669241884848173449093802827500740854335803778197*y^20 - 314294001372819226280619914670683492137156941984472538476917210178742/336064808395431621669241884848173449093802827500740854335803778197*y^19 + 1245538639872324965433014769522174026287234440934765745663807844822084/336064808395431621669241884848173449093802827500740854335803778197*y^18 + 463213294227312761422312512996925054682774571183614981414138883215059/336064808395431621669241884848173449093802827500740854335803778197*y^17 - 8576519736469987850494684472268685194923837979742727922281258789976086/336064808395431621669241884848173449093802827500740854335803778197*y^16 + 5659346549008303501773308054844617742312585177870076592342278715559438/336064808395431621669241884848173449093802827500740854335803778197*y^15 + 14476934145667437013399693457766547133561060167217298330864544183660126/336064808395431621669241884848173449093802827500740854335803778197*y^14 - 20186018648878392063359965701800168818161414929189565614922905376696993/336064808395431621669241884848173449093802827500740854335803778197*y^13 - 2845135434368072558265303327686605581742440763421292011944782962330956/336064808395431621669241884848173449093802827500740854335803778197*y^12 + 37949456313678294302015799043479520207353306621116243923992130396603236/336064808395431621669241884848173449093802827500740854335803778197*y^11 - 4859339933720200194650009221154763564426554030228746333881504776407569/336064808395431621669241884848173449093802827500740854335803778197*y^10 - 39610695974489627640822758950403129397195914747357992998607457564446403/336064808395431621669241884848173449093802827500740854335803778197*y^9 - 4835369747329803827650309215502356053815843259206535994556571722733742/336064808395431621669241884848173449093802827500740854335803778197*y^8 + 17617433080162116548350992429175388589556900391969900279835076785810201/336064808395431621669241884848173449093802827500740854335803778197*y^7 + 5562020975850138831742626540862099152964785823494057386566486967313928/336064808395431621669241884848173449093802827500740854335803778197*y^6 - 2850289047431579022650538508119912694102245925533224726370816573658757/336064808395431621669241884848173449093802827500740854335803778197*y^5 - 1371397541682876982110555116293108077066008717491437023091100528235577/336064808395431621669241884848173449093802827500740854335803778197*y^4 + 77125242754326435195718938060979525237619362264795745557711252551610/336064808395431621669241884848173449093802827500740854335803778197*y^3 + 75169167001637748741251968609449125412011911509867637061144506471217/336064808395431621669241884848173449093802827500740854335803778197*y^2 - 4184997299295379623225615052960818233066222623175754722566653857421/336064808395431621669241884848173449093802827500740854335803778197*y + 144099157996812791275220414336155814520089917788139153666973258398/336064808395431621669241884848173449093802827500740854335803778197 -94669178387880929776881640459357034203319800734022289188135028801/1008194425186294865007725654544520347281408482502222563007411334591*y^23 - 319828889484299971374692274252799543132355295619742827492508212394/336064808395431621669241884848173449093802827500740854335803778197*y^22 + 5640823159027065230504941033474692137920152162063467440807059850961/1008194425186294865007725654544520347281408482502222563007411334591*y^21 - 12059749239361410091799822876753328702266653242197545938744049449404/1008194425186294865007725654544520347281408482502222563007411334591*y^20 + 75631613863022319019925087514781988861717786476117861435601322256273/336064808395431621669241884848173449093802827500740854335803778197*y^19 - 920103359489058181284757370646206320678807559634765292450377588730760/1008194425186294865007725654544520347281408482502222563007411334591*y^18 - 218553933946273527386243864010431336111049160990300783303366235709562/1008194425186294865007725654544520347281408482502222563007411334591*y^17 + 6149222210184443816210870922933855129399600957256237934209032680188312/1008194425186294865007725654544520347281408482502222563007411334591*y^16 - 4763329163626434375704231335791441115505747800658408372238118898236112/1008194425186294865007725654544520347281408482502222563007411334591*y^15 - 3226900129411025693901307792776657440196354359053402031785739467718526/336064808395431621669241884848173449093802827500740854335803778197*y^14 + 15352542561765321052594895562745538606378077042081334133414072461292596/1008194425186294865007725654544520347281408482502222563007411334591*y^13 + 154413760286641501983551478306518843294643969460580660460065579524807/1008194425186294865007725654544520347281408482502222563007411334591*y^12 - 8884297385941796471361570240346884485240018668636319325893886188800229/336064808395431621669241884848173449093802827500740854335803778197*y^11 + 6187001925883432271687679776709940366296849652726693375283645930766811/1008194425186294865007725654544520347281408482502222563007411334591*y^10 + 27164979891390821193525127478992686053794827148735802921430447262214239/1008194425186294865007725654544520347281408482502222563007411334591*y^9 + 1096088499540374564601845027719499912920646978456231676273130584750790/1008194425186294865007725654544520347281408482502222563007411334591*y^8 - 12467290095034863711696149009104495617803867017249463293494543511653026/1008194425186294865007725654544520347281408482502222563007411334591*y^7 - 1029451741106357918296450893561023065145745878448126441945882879505196/336064808395431621669241884848173449093802827500740854335803778197*y^6 + 2225029319389766699407344024680986037225529645925831542525374757964010/1008194425186294865007725654544520347281408482502222563007411334591*y^5 + 289049181763721241212838508578576353542618050234197038970202549683037/336064808395431621669241884848173449093802827500740854335803778197*y^4 - 33986257518265001329170836141522116089736623706413532212781989789135/336064808395431621669241884848173449093802827500740854335803778197*y^3 - 53990189442247646786895437358943790504255141104222084902222989290355/1008194425186294865007725654544520347281408482502222563007411334591*y^2 + 1462116557168034617435586629230260958907008195984613392179115264390/336064808395431621669241884848173449093802827500740854335803778197*y + 61718504356633601823437423798280501117637661261467049850546654694/1008194425186294865007725654544520347281408482502222563007411334591 # A Gluing Matrix {{3,0,4,2,-2,-2,-2},{0,0,-1,0,0,0,0},{2,-1,5,2,-2,-2,-2},{1,0,2,1,0,0,0},{-1,0,-2,0,2,2,2},{-1,0,-2,0,2,4,4},{-1,0,-2,0,2,4,6}} # B Gluing Matrix {{2,0,0,0,0,0,0},{0,1,0,0,0,0,0},{0,0,1,0,0,0,0},{0,0,0,1,0,0,0},{0,0,0,0,1,0,0},{0,0,0,0,0,1,0},{0,0,0,0,0,0,1}} # nu Gluing Vector {2, 0, 1, 1, 0, 0, 0} # f Combinatorial flattening {-2, 1, 0, 3, 0, 0, 0} # f' Combinatorial flattening {1, 0, 0, 0, -2, -2, -2} # 1 Loop Invariant -85177562023644990044567883785496727246554779638418522889219808861335/336064808395431621669241884848173449093802827500740854335803778197*y^23 - 1733781255876942972416951810547164999159005492181458994734475788891589/672129616790863243338483769696346898187605655001481708671607556394*y^22 + 10084355652960001790138528807257349583463231524769295265360974828941395/672129616790863243338483769696346898187605655001481708671607556394*y^21 - 21204517933457197632042794099547328506249402463036994232623031310891869/672129616790863243338483769696346898187605655001481708671607556394*y^20 + 406945094379538830692640344195029357544774748243883104779065512749582431/672129616790863243338483769696346898187605655001481708671607556394*y^19 - 1637443107618100603673270496992997859332997103915119447481777816306997141/672129616790863243338483769696346898187605655001481708671607556394*y^18 - 239983765422428663869547758661559713296562119436773560965201534504553487/336064808395431621669241884848173449093802827500740854335803778197*y^17 + 5560062734347093712408270618567463777832701598633062538308980365213575608/336064808395431621669241884848173449093802827500740854335803778197*y^16 - 4053249740038462296908328845414791726404936494574790239532174828674889453/336064808395431621669241884848173449093802827500740854335803778197*y^15 - 9119313737487454235200189122259187599158819590988831244940968381919355970/336064808395431621669241884848173449093802827500740854335803778197*y^14 + 13690479496653993342408158627453136300278509979850869514388576967408322591/336064808395431621669241884848173449093802827500740854335803778197*y^13 + 2050425692955086528435593039089120574103084366451007778260376436190316245/672129616790863243338483769696346898187605655001481708671607556394*y^12 - 49343944671345257921101596819684456697596992149971719445163586653107815517/672129616790863243338483769696346898187605655001481708671607556394*y^11 + 4765632988844002730376080713031878623753372756602163733663243223557589510/336064808395431621669241884848173449093802827500740854335803778197*y^10 + 25647976057475700743187552021584167569898285018811724099964019987262052588/336064808395431621669241884848173449093802827500740854335803778197*y^9 + 1413991428282926152479824243853677621776132628151316677776128097267072769/336064808395431621669241884848173449093802827500740854335803778197*y^8 - 24017451806573575752928335623692935706893826922847203469171467654652151041/672129616790863243338483769696346898187605655001481708671607556394*y^7 - 2959495626687840697599343349578460352233410588078877006271786145054849317/336064808395431621669241884848173449093802827500740854335803778197*y^6 + 2258012314340757380059151378811593479600567218502637561506937414864380767/336064808395431621669241884848173449093802827500740854335803778197*y^5 + 1682893871988157703038550172415212221722964621192709222333625518133357493/672129616790863243338483769696346898187605655001481708671607556394*y^4 - 130472405609071341947701070124774393069888312437716978943408968533617305/336064808395431621669241884848173449093802827500740854335803778197*y^3 - 116539926788432899193787679378010394306476893362148091794989730384327125/672129616790863243338483769696346898187605655001481708671607556394*y^2 + 5832489734208153668239130908133516704149655234072759355986374128012482/336064808395431621669241884848173449093802827500740854335803778197*y + 1159593119568302156698778608601845518655512052876710353749960281165581/672129616790863243338483769696346898187605655001481708671607556394 # 2 Loop Invariant -749706403354853586923488316700880898364600128040527509302947455260804590705642100349825128649809181150040061611770205462026146669460430299301225/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^23 - 7689105708203262054501198202590447787700310584088143690244879204963692336611645595045620068975528093946147117077539327258670057093619663148991023/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^22 + 43769298367388279907571553323069970193958110161511519616015223351844552029175471459976161307466859923509795477036108575529146386271791735799011293/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^21 - 5620871636309644275787932272742316904080425769508796405013808938418699696285410733106363636789073429092603050711729775808257035264324324676304526/772916606626392527450859415050737822762654071989341297850308117519243702569670402522286165393792810703790917048392393325871685312122011269937839*y^20 + 892028613509114499016641796665178328175432674023028726065000760868615477507584398248032992713934179653987184476864765592651459363485342614965674203/6183332853011140219606875320405902582101232575914730382802464940153949620557363220178289323150342485630327336387139146606973482496976090159502712*y^19 - 441618281555508404773160595086749394958124377984058121865052203827803186473407489089117741958210002342551288334331730642225670998751370188654352405/772916606626392527450859415050737822762654071989341297850308117519243702569670402522286165393792810703790917048392393325871685312122011269937839*y^18 - 2657019804789402610746919302421706216463287206301197984136984188699312237645466808126454391714430187468212635815427660826911755528844580632125892555/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^17 + 48697546735563612689399198491972172814371119343877639472628869816774338856042289304868215658418796621694376048208378698207606704155297449901850089545/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^16 - 5323039031368328050530134782221349756771760613778010211667868404167269524839390267627010829587887536585474485738785690061696512333978135044475172473/2061110951003713406535625106801967527367077525304910127600821646717983206852454406726096441050114161876775778795713048868991160832325363386500904*y^15 - 82428478277361036915411441755948739267690051403242476376703762437242809872199832337549083396383237365896228636576934546852220270812515297754449422657/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^14 + 114243738150709091708730937252086029522655180122087959299050304316026045307871792147720925087740231605319754342118606816139172255583308142279429988215/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^13 + 705484701959885096463649204507262630911657906052154356371486151969810995131738380726496527742747005073241762284440676327974520335451413796266234815/515277737750928351633906276700491881841769381326227531900205411679495801713113601681524110262528540469193944698928262217247790208081340846625226*y^12 - 26938730458760893908155730056528548299619367395859224658450552667141961440282946845117947676949358388425599073943811077219314360250750030466246061149/1545833213252785054901718830101475645525308143978682595700616235038487405139340805044572330787585621407581834096784786651743370624244022539875678*y^11 + 13169479329289121040913646943474833234785776929078151281746690265713322467756278012037310082576607857344897410436981761196624309014252652178226457027/6183332853011140219606875320405902582101232575914730382802464940153949620557363220178289323150342485630327336387139146606973482496976090159502712*y^10 + 75271582929456394455627671034542167754827360531761315589885166621175133874951649188719020294433727902786950087182503357657103299460724403297962010465/4122221902007426813071250213603935054734155050609820255201643293435966413704908813452192882100228323753551557591426097737982321664650726773001808*y^9 + 28756291450966208080323400530300516603483109138282910884162551627258458617433317710750912319058893991703003640069336390812880899582280239912333145979/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^8 - 100940360915679973067187479072128451803939719907538295443586998769073454067099465587710294431526859414125745574759964903218413964981255824417050321319/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^7 - 5395549337681409125911981175018023185169478689968855285216109461748468088387617886276499564505142635428886528617343619370897969732042680211477728593/2061110951003713406535625106801967527367077525304910127600821646717983206852454406726096441050114161876775778795713048868991160832325363386500904*y^6 + 8196662169433642662571991440061149206972817303893926030002274451727629072259137720757871821619803178120935963194997733092740721817510472204774484019/6183332853011140219606875320405902582101232575914730382802464940153949620557363220178289323150342485630327336387139146606973482496976090159502712*y^5 + 7941500607001890130471499973694415742158010693941140745345662417688505628173637438080681759783702119298380071203005864380379045905329146490203554321/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^4 - 149649010872121517982421778764365699051026226870089103640664107455211843640229553608646753842791495071521429770882363814582501196065842668751121917/4122221902007426813071250213603935054734155050609820255201643293435966413704908813452192882100228323753551557591426097737982321664650726773001808*y^3 - 431498434722672501991325811638676145678108729739708259861068848638202647407282875315155189833597749366510898110884392155991386516683511345624891085/12366665706022280439213750640811805164202465151829460765604929880307899241114726440356578646300684971260654672774278293213946964993952180319005424*y^2 + 12664790612250416155108849641538466526609198462640788861392056790225656751870205099102672914322034665056367658280146377739746203432495027701224937/6183332853011140219606875320405902582101232575914730382802464940153949620557363220178289323150342485630327336387139146606973482496976090159502712*y + 2699009920595887051771116166833862454829630475118511698577748761918604314927459642885350848946305901129528405481802149107127469955703669653751509/6183332853011140219606875320405902582101232575914730382802464940153949620557363220178289323150342485630327336387139146606973482496976090159502712 # 3 Loop Invariant -5906619875623381465464322955236778275616446123459413718156839242676837078941972363939756802123167397881405023988025340747495545700183841459982875919458326637300065953123136513092600/225582578856750231911254982925250459473840883137826382668593768240214460957938086326500756318055083157316669538083817772616971190514376415523033923112756499013254780779233241797816301*y^23 - 3865187438404245193151235718781168886478884591231090682779044171307759103269981543100643947746016337182440748626748128746783204080889669331521318676815644543956576624171796817762007553/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^22 + 22197477027261743540426611920879109305547223819969374071586448181503924144464723378203260603841937490066663069332045243198441339790687324723438400762887772110228154930608677107467514509/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^21 - 45980931628139386050139430496415803043065245601793833845753780170407775299071419021895597677069572674608571964351677519083683881751049924385685293637029668487102941901299291861739665525/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^20 + 112582111239548361783481369017184758626309925171329014220492694736883050337259192722143068080008536089891292277523789381839080895445071391007290976752557789052308556698028606337433387235/1804660630854001855290039863402003675790727065102611061348750145921715687663504690612006050544440665258533356304670542180935769524115011324184271384902051992106038246233865934382530408*y^19 - 1795192510123117566485186404361508335863653942935433257611067489436301789419327933099944498892497434954008265035357820953882159295706472125217239052103357043710908383736770207039644637849/7218642523416007421160159453608014703162908260410444245395000583686862750654018762448024202177762661034133425218682168723743078096460045296737085539608207968424152984935463737530121632*y^18 - 620893040517761850825066895014828270515524048193083287162724447165184658460557399322281931990074571719046066326837696738446901242559480038602356562836360561053969111641362305707891108237/7218642523416007421160159453608014703162908260410444245395000583686862750654018762448024202177762661034133425218682168723743078096460045296737085539608207968424152984935463737530121632*y^17 + 12326190801236535287248686138924931904137026388593262560199399618788685777787933470333078065389879197548537226939122835509517785142231390553552183152507583431387121091596687097674184189237/7218642523416007421160159453608014703162908260410444245395000583686862750654018762448024202177762661034133425218682168723743078096460045296737085539608207968424152984935463737530121632*y^16 - 16858552257532575276324677785700474672654131658098304804236931230695273734829849144759992768684867767659209407460690694836025613094701988591255560786184801805581844232480021908910397837653/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^15 - 10356610031217650568620497944487245338057521709388736307507976621624216406895730476594852801630352719993965138567499691796256391205971994234976927556692336135542040944490278239213841748163/3609321261708003710580079726804007351581454130205222122697500291843431375327009381224012101088881330517066712609341084361871539048230022648368542769804103984212076492467731868765060816*y^14 + 14791632319391626251933740730432487903595103960833540417028290754300641293890953752179416824956627534576543910976143304235645791558124110666088636734014037252143193466753311591000163905769/3609321261708003710580079726804007351581454130205222122697500291843431375327009381224012101088881330517066712609341084361871539048230022648368542769804103984212076492467731868765060816*y^13 + 1824437338961236938031000280904664622224903037653003229286237361348897870307223399388980128658328747344609556993043459985838141719208484486454631548120547394374857972743231586655639065005/3609321261708003710580079726804007351581454130205222122697500291843431375327009381224012101088881330517066712609341084361871539048230022648368542769804103984212076492467731868765060816*y^12 - 109774186037436049671319860343750481985677547246514404271396853355745081588482001582895276290245137197313595009043597915044978984994246628328943772052935891120282978038159145391067240306453/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^11 + 16668214509443046936722100466499557620520232384516899860032891746932168339150453298975135569549457850530870667745597932659930657950459305603883282069436009749369888563927420354808568046983/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^10 + 28739800376005374591178165416070639493910306941355606214475735211602412037950535155976596287190613546101360962312132776041974548239428966200611504157337498035735813523361731004174371690225/3609321261708003710580079726804007351581454130205222122697500291843431375327009381224012101088881330517066712609341084361871539048230022648368542769804103984212076492467731868765060816*y^9 + 10726841623010301316063890389912079621748433233023845319979557030048231122542023065682062022059248208806725179482854168004499420181054689715590805857041423958263482147409283582358187108825/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^8 - 52839246454391424465462442513264812866519803375203440959971371580106704194032070323408635907443285645318651222402914644907157523934886860079251869566441518912128926640661308819272298362887/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^7 - 15009821818185796008812052675667394440239198674085752198142483775745881515620747225211908430989836546476904019192964952947525945665833478951449825419411771686281565380380468994135634373657/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^6 + 2329506690127239835091661433290795776721578129618494733170622849202107671493482627835345185846310914039659155460233112812089499857837146966093566328607465946263075564140753446947180579157/3609321261708003710580079726804007351581454130205222122697500291843431375327009381224012101088881330517066712609341084361871539048230022648368542769804103984212076492467731868765060816*y^5 + 3974339590116032256191015750150708072745427241107787184147932441620450960285543597518485832877408077482610854728703924383991626444463255944104887294551553694428314360306838746253814615439/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^4 - 201460160386713604004013875057006912779724855920316206540294352491656370779949510840943732932169178379209666502120127337563310332854444604259482113170358975950202281913778741029912504991/7218642523416007421160159453608014703162908260410444245395000583686862750654018762448024202177762661034133425218682168723743078096460045296737085539608207968424152984935463737530121632*y^3 - 249065266046235530414803011436327539664460795143786620297940585316645834001826126108571607977638254219410471188828322279718652825533018884982645320611480144232618401066134683798777832185/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264*y^2 + 9254086953524619491046929702025594822665166373265219108913941575306133386319634454733269349823984643002378896000131477830054212511140125586318101008498363417028770906006718136702211041/7218642523416007421160159453608014703162908260410444245395000583686862750654018762448024202177762661034133425218682168723743078096460045296737085539608207968424152984935463737530121632*y + 2070086719507401099633340740556963420386009180056648154299542436875183589032346637728054961355598502772891395718888055576427268153413655569354822101041115014605535041077634934788897771/14437285046832014842320318907216029406325816520820888490790001167373725501308037524896048404355525322068266850437364337447486156192920090593474171079216415936848305969870927475060243264