# Manifold: Census Knot K7_69 # Number of Tetrahedra: 7 # Number Field x^29 - 26*x^28 + 169*x^27 - 465*x^26 + 1800*x^25 - 9379*x^24 + 4209*x^23 + 21620*x^22 - 128906*x^21 + 446785*x^20 + 754086*x^19 - 2075055*x^18 - 1678901*x^17 + 3691892*x^16 + 961040*x^15 - 4889823*x^14 - 2000258*x^13 + 1064369*x^12 + 545676*x^11 + 495863*x^10 + 188300*x^9 - 186432*x^8 - 85678*x^7 + 6386*x^6 + 5411*x^5 + 2564*x^4 + 3202*x^3 - 1224*x^2 - 180*x + 61 # Approximate Field Generator -0.435421967464165 + 0.303042574730782*I # Shape Parameters 77713858069460696988448625173519764462299180468548071378619924851647853731945093684434232785270991408/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^28 - 664808489683911685786569857223328479910514763907032193989225381452323337714630405155338016957335210349/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^27 + 12463296964653322562822911995043910692600088569620659608192713704990382446036811542793376163778763174004/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^26 - 31954788493442151630971845534550713390053234718587325397623893217718510640937581549226521692622923272229/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^25 + 129189344116418089807168987665802494832531999468321766215917643231444984496590137034831181777435689226747/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^24 - 685525761391336798838526533171640055164551610570038166795379991421939547451798196465104601231155094441004/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^23 + 97000966624276521648681278149200337644492866282988386822753642760640627998261480205650950409077160630190/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^22 + 570068832651828957876232106047716761885950987375727372188531424672690380651036517844949879684794174340576/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^21 - 9445657804863625181867929450454837703493640995435564809121456625567063451588700258713519516685332073108096/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^20 + 10518532400202598238272159995064142919923424845700535071124472736210430241047983040132842792318463116277816/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^19 + 23057971371660040348733966161119619267187590714499413384392307194661526413072160555905569064446321719149192/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^18 - 45962720897156088644798786022458749308098796167916997472500315483731483272125338730002661070146340158696352/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^17 - 176353117318575829321198290991874353153888072400974834833713726074670582760696158663883688843424890117784602/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^16 + 227146668017146013142493701858174076567817914505840010578997337378837535348861650366206857571786411873991199/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^15 + 149624076548461542803382185739789196362308910961031922324823744892190684934207977595249624123131702104470910/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^14 - 329003334523176412950577196423340494341752688601557585853405059541584341980363592430023891512585132195150789/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^13 - 264546642163814623567360834960974284004963026174945825270147921321308701213564674815965216955446395322250280/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^12 - 283707930046241545600237739903957509140595404403929205511020864657524590847482381416790617681674858055623/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^11 + 12508809296319610603559778311168993543971921535704734463694037349525197639144183392811719595642430660304620/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^10 + 50356560000571359235049812965126241722659813857294285183650693396256901269929612385389080211319823670198772/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^9 + 10516237262833423236151328818384878467372906876816167740484451449921678500000283385264768511973950333323350/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^8 - 1197802725424403545340486931375256483428711511707444636782694790913438334943405771491944450777890989678215/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^7 - 7583941517966318197035867841215018361792934004231180317166036234060459050455916344824466938341982232224293/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^6 - 663593435891236885091262401629956065599110506158697771361473779866655570361324037836474155842559207491029/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^5 - 279507347376109938876434398308419089242330167506134716357146574865569377319989560354903388744374788738060/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^4 + 9548527185584079460982181415700722165489565593468858591081028835163763786434386116900312284462117773691/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^3 + 270133919345276633454644716962365096994466383059365326478651805573998834106888867569194768465149328785231/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^2 - 5617633986714837177377558864132298168163586135117816753771866311593438374104737021352893848217740359908/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y - 12107734637647075264974930441325252070684401348991255097831678133137548263837153568136255653548981504666/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631 -43430933054416209261305005684422735630359647382623899686159332924907907815439878306521915072164013477/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^28 + 1114099593267981109353631526902604752851119163619498701011382112195624508446507543663954315740028609592/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^27 - 772485974723977372982096869425859708606985508816185206363071858101505889196676778593738926743837032093/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^26 + 17777616633488305686222638634374763969558153694809964422052550338224555364729550007756987041096938500134/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^25 - 71990100382275541126280861310605646972420369532813265667050186817166154006790522496691771824340709350338/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^24 + 382274448476906414008039857749689725077872601977935650720165400653287654676336375840136724721131228942420/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^23 - 49780296529350983907870820541691075702279846321926465254803667142430548638044378170142516685047301906628/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^22 - 956542333490705691799124216151465423243829920139109068671061039474074303774283499663156007297658790194433/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^21 + 5267719272384175597525167340679003525022880552786810167465101329071662332940625079469866766245296163608559/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^20 - 5857890676292133272248882716791398365656317535527053738713161861660068742002876408621492625795583925237874/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^19 - 12954467957688910604874708781981400103960684473139708636094276075965079778251713992299753758341708670372149/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^18 + 25541293678539952200751668679452802168115992618548320293123035079084358880774395509377334055405040521057996/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^17 + 99462068088030957164179605489201236555391104403218667058109685759888710230683295461161157951315110653336358/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^16 - 125850574071690363789175068411493245380693344310736007924758083487375426840326672463816573552732275301011414/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^15 - 85153110451693890163935840176237347401386839907483870443320338038433573831893241590389183230649155163212629/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^14 + 60974273102400180675568283026303231748268616639844606152806668595411623023711270296378509631808449583391414/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^13 + 50036292451024714924123216418099061519015717141792843013121498468938876739835605749606624351441420321819819/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^12 + 6070086236169411821952910112495463811312093728351986397474785742960530517814372424033717726618811857229491/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^11 - 21190634318560860268707399950349678397447931862123953720473753329481430269820656351242189443011225540787957/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^10 - 3170154647089203017903828845983103873960478625392793874160569572745971558481469333940206351775128855778132/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^9 - 17589277166193554174710877542831568054938221685891738665082691652473251652040290967758156902860374881599964/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^8 + 2102508304778584324670781427654066242350359237732624819392217531599820570257755545938848302893988157949214/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^7 + 479651002739630921653844085355623117549701631265377991883024550585073192589245424195257792610892462004288/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^6 + 1149449030692239021469159494223832727193951733631421766955749951192351167875618792127368533893601079914951/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^5 + 131962104121132760507442214862057130115739401433258696816842143714051545450553811249799122357174293974744/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^4 - 19817873919814000756543493170606381990932034205502797936397644600881892873177173692330384668528189594309/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^3 - 155779024614570577214250010913643740317096593318312195991830534980148639354199551960790887932282023707748/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^2 + 1412906143244122306444262019038923138745593361957860828075392407177204102568465916654147903374694983461/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y + 6986771297991915331989531348452874267672878228026505828567848210333242448142638548816139663647139563295/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877 -554242180848510017951693977319814626522005986259918218832287621801310537703789468307257119117812221/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^28 + 42352118602174559268257742751945980589357281648465254572966512361018057613171386733617317420648961898/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^27 - 258486575456562653384576802308405471007824531553302425683952850067947359038816855353858241857161493809/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^26 + 633031974895839874427698611874558222528896080361562600055525783072144290057282067927610023727408432278/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^25 - 2632905137021820955090141979861153553772609861649206599513056929243324385863392180547874094072091734788/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^24 + 14119277000612290784622597674584117947536712561726653575288230698420676223164985865395468743003754998181/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^23 + 770714646524658090135695897434518359183363459908964158088443948995912813477120113216700716364561648437/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^22 - 37038585273719517832463806406906569974202230302651613192503838397396353431597281311577232026869007062679/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^21 + 65553453496138712060637117550596183251370180920240666794901688142147781835201035680752081426537641283079/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^20 - 212471080726097460403754164627773372068595967458236288589280333543979590771724164649997748415183177581981/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^19 - 536391535494057536957942761119188582033906080669271191992980407229451426990490634886605441414994036421877/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^18 + 891695772554010747982532420167140126119703227689346324407841203027271568307381139909369534836478707327808/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^17 + 1412536752193891831434024229222384912910734580474745950176501229574951617045843792423479506455270000812262/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^16 - 4226455448589164137538163753983127418053658328137297587633350594663866918020196079400047869441060050343477/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^15 - 3783198159509034901901397629264849434791767133841271887835394984539411597357962758571873853681093252847395/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^14 + 6656126175463875660125269172250155884405519729974198692095741526541805824074981103220208796246910370373091/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^13 + 6586675486600569780183470475574610665259910351013583684042285469673256291870573917966222923615485398958416/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^12 + 1219664698141487012632682662147789457039528417306522491830489723821591242489403424510038746789306681857007/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^11 - 52182201520230977945566994040491541418245761806500366936080120660807752883265854500616500274227501484842/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^10 - 729332301337422886709767005052334083891453537344271979633680891004274839023057314437151928203892947796915/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^9 - 184461768073904951284369739474453189789061818141233395285537220590333524207142809966667140490435269365775/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^8 + 77598374669118722596393458674860100676833380088644195717875553265157203584383769640907427499203075442587/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^7 + 126848337835563018593753460361517475622562955165036873291392267076814571727593120555712980956768472148370/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^6 + 20634119401078732422400492218310727105811219325009999298986702637064027839973430110922976730481765350457/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^5 - 3061559469409554300166431367310893888389557355603497782585572549428953125161225932733159295981096166016/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^4 - 1541641106958670463733989659326029390890154315409605707699018499454927037930777026954392708797492647739/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^3 - 2113416904864374034430285563339437677948428656722098993316286435576456205763353652624123962005193944313/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^2 + 843279561842854248974052168269857266834332979890228453996884502091224847086985432602779297189579538525/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y + 142548940446396568460146336463444232208669636095554859132206677144165335940724750083930139745808862996/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653 -2139997419532300072217143242099291910134046221902689593036432223361396246547116528946985378819225711/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^28 + 6177698611504221696613901857419190187473416340866853205464690335762704938758047346472340670368396895/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^27 - 360290911308890651307860258665127447298735086167202691819244329837513817631414091037158431476827159646/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^26 + 980757615987706678618186810538774861854419000219771785861490002122481252330156180332321972013357625253/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^25 - 3796610576978879397047333763762319319980718931225707994652383559122402665526177612683479940255110507411/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^24 + 19952147876506807534894944673805738541588474791259201796161635110589592712885108334162639573118384372857/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^23 - 8311904880264290389086132796178032770038064455723068010465313596636878300891534597190606917951421894564/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^22 - 16109326339536313142008161107574512833087263178831600099491091229031163476789855597699417941448853869197/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^21 + 270808915549070103981560521653686431792180493852890165025301305481127233234242666417151478722508685468645/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^20 - 314702564351220131033963548676461714631095454912500205864401913853083643056802008737011998043931721316626/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^19 - 553088575832825495327955788210224014732789164461081411250201288773727854260110163625074904228408019831888/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^18 + 1491474823183856030271620506206461942369077091136276642797345868928804735907399556237735415505587663370068/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^17 + 4160087740948507882152379788904789455139486286481606530102676778912789734465457077446344512742750605998516/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^16 - 7884638969635163079591908056173340718545389951850875128748727436227739276243099327201972688813044891434501/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^15 - 3697584646064939319074458091147257307881458701332614966528330718774062252697348107590023817396389307270644/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^14 + 10073063134825421381069335760824265223099285612889480333911745052262726933202532398201438635365084679134239/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^13 + 6142303495345274179988002819885630506377454730536222882079646607577926388203354324890552940980239718145478/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^12 - 279654081258525032432660511458435618053103026852373252967706619936303771784769599744498319341919453796694/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^11 - 1324899927586575018407257947236162024401474580222606874720154285517399039304625209817717137972456524787661/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^10 - 3143068950092746786805045802808898928523559631426873960655775363094163692009420668803491274122967325165552/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^9 - 135139348425913926448412987534245451290778402179250698233577438626183466374510976514731790425195981875717/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^8 + 33422893947137734584775393388304945944765454491325984229777577289981207487220188712726596714230584391053/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^7 + 458360405388690882977915317114397349665467761327271405929250846882883660409583215830124070497639200658793/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^6 + 58205051059206343528703874034358408511630388576238283339169452823954242620056467245382208190320974012295/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^5 + 32110711823806858431883274328136350552465604315218863825256216108949264422862901052088502209691612953420/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^4 - 720256074425098534899965293006846654627400214104050161504135965216800056393792868295353478977595321276/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^3 - 11728681435764602038185236632845580397819964142393190444983134081044043638286349623605219201194508326645/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^2 - 1078852436130044792227009488304690184562265453320441002920049759212211652195798174806933371233515534834/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y + 749108397383507038762152505231896234523364173309260773205191189781575790185134694445493681790076942302/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877 -268651491971308504083872968537484018037289268203965958082853435225151920136325479761518298963821488658/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^28 + 758208135205421689634511177701333981720293788666991287531635146799688876155590735986594757911265393148/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^27 - 41299658291972526071020002219204946887736994700376045884766211731904987483213026046977170474867360449528/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^26 + 99875116607589477227538043236699225501418317314332869353313714711776339515710293390194306887602311183115/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^25 - 421951198885392328090773902972766238235079496585616250868778633126410733813972738381349060178317838041509/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^24 + 2262464700171436952170834875422868680162066275579482311692787716842837434519433510338356343957128153782586/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^23 + 243561941322165646926075114452902027205933465627423191781797469634746209278678320441158004956971273408398/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^22 - 639761223122130334328483173297597721233030651144742487782584589746205095901136478220448668854986276185968/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^21 + 31170755058373919014391907024836390935719460023385660418889674583509183657489922670746051731523041177030203/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^20 - 33700869473142051890016366932134154104267313260729359604777420785948949298611840495715727585986310806075611/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^19 - 88173142020687799328172897835889125871828489294688261830740871153499095288688469592509770189853438096703608/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^18 + 134389419254329571170904000931416067269684685300839180743980006404457255237079726200042477844866745767284087/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^17 + 703752389367795380741727334127214503319825811573516637280756508903859008365497598186788407890364835884411180/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^16 - 586906643203020780305517168553931580443820335351380787019361842577181690332306364991815783927304999558575933/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^15 - 638780323498425235264833643873487231864934974685723711336209303821583228032796412042127452174743843887053440/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^14 + 955213392773587540328039030232780067502712151042939444666960887256432995364819209700755403434533228858234804/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^13 + 1134888874583922363542927019397263543777459665987678489007754704387223293305798755696497968366984589022550438/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^12 + 118292797883862398217706936132796841496773114722729265530533401982423989521880845442259539113454496945234226/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^11 + 761184837688208466913119626121789222164278014874602554236504091848215967546422402858627092651013586212797/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^10 - 136942698391882495245135792071981688039174392775870615926225091491322150016194911085733919575833617133960466/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^9 - 45198668144007572288678337504634809130478205437245997102255650335485366082529690139525244511451969735343743/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^8 - 974924630818709148182924430268035192193619306579125498379014239652251400863578203441995397779510738275366/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^7 + 12444030935476096121873573645769437447486903395546547464661887457848497670779147089393573907867835328630762/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^6 + 2294820423004177115403094153461855374627062709910980312944276094325593015712595734658328312393693223448042/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^5 + 2431917195869182496716806654997840295816438337277306473026959126307590318837822294972344044078261039072861/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^4 + 21637018109573202446839123466161682891583737141741059969959816521693065548884882406334566373321763277227/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^3 - 606235622847818367155675477293945082194059910349417334286099781688591444560781514114223712385293749757107/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^2 - 60226499077283719194483992215779283595745492515720728176967327833230821308770466047515545478815782165692/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y + 30437096578544331368970688375939222351619970468363712354666428747983593151294333322170433767080798172776/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631 63539895658681059473081058207691514388696737929046047899156234086459989201951371096983789118883845931/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^28 - 60373292519425071175464432187051090073433810488629482314731201905848197651356108279643668096869097042/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^27 + 10174234412812282923975101819402152747369410779378764752529351209804451462411329065113384037928614488351/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^26 - 26012313999590873127601934931606303821271510465404857530076392788171619744281168427491634010238791704931/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^25 + 105266414186224595862994552136963597134947266652537919841702617264111325488278719952108594925459547172853/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^24 - 559235988103254927813279208616810647840545515408026467617026858610136145673355800412365479710014945593241/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^23 + 72915632241461924834514606312900075047443413273014028057345314411870387076711152531321319021252787568276/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^22 + 156157214486539399577765515841122472205470945121393570684074274365240145578182119026754980007949130513488/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^21 - 7708428739282831128260642872195829572706873274283683907030931971648504387382057821759344826555600503620693/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^20 + 8570398472637938765879827760811951877535918406179762437825783471082658045444006172448255523601013111719082/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^19 + 18962997650991256192254574479356631829653311581213296086373934090255442620531512109082548569517202777414252/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^18 - 37500741244612266623966173389371632959313024184034175399862755045293296066333679090491050212876118546953310/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^17 - 146030361203763548806031403225624494537582134812889109249435250622886534185221617263571504679490579920487676/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^16 + 185513427049070535525456764338498017178056148611579289219115321418258711459447448188476342580573505135415362/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^15 + 126075133409968747856022816334483347584968609176909651854978941835180006025492137757410268344523445009732960/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^14 - 269459153277498573002476520445939887346276546055220452464148137090504763987018787678777154593482925701719931/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^13 - 220361437002341175880981805561307553444952093620403401799282808051833867969531354969271376001222132789875999/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^12 - 1883013189683348457735415231848965121474812690350335796785799508362153422345003764518125940925490985972825/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^11 + 3740477869850708705591046495993569689938746462189462743349199037496253121847340854933618006518574273942285/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^10 + 42986244663818242475540769636626597979488146744382624987051618830400060224601454829656493512836113589396417/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^9 + 8928893496534311799430746295319580143970003862426971684661658289950490662231337382459777128684944217433900/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^8 - 317046770604684411343007361306026282204244026936936391334392971660504732230137966170387570243117681423947/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^7 - 6486187292922539081560708497899400741955381120310817656144597513395227290479503388053891251160872276618419/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^6 - 600868889268110524917941907632213790026069977770012450918626534967432095511894670271018198147724006791372/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^5 - 272286691388187437756667157532627087731435844297013118307962907256827718068539768273373478314852044376761/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^4 + 2306958288947855308839422525857913706998716525968300236516397013238857248730249204953472692682269378440/67475782926763046979479241264469869557756014054117191800501652723685784148007473458009701215227574653*y^3 + 225539279640828404753496068002069352143870638674853513598559979736021848142723132084862528497668713326996/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^2 + 1884661885348601322368770440595282198523332360319236390959976682468670796989329803695641704428928412039/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y - 9953723080315170543101802681047645084614909240770356511632651004562391580279805407175684250109363698561/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631 -1725069843392545683405250253051633692263792416333793332235137566654713890260479060481994522275548771731/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^28 + 14716747407060134477937485109489817153928674499355063970694991816785946668663182450116470114996731224488/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^27 - 39084934432970219483356623729279205405707857943452117384455789906068696236402559712479753942444360521639/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^26 + 691231223266159414808825904279368917095497758643895560627298550804117404464186808414627566217844168828682/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^25 - 2826164561372611598865630726147597174877108412663321531393285426055963424466268384804145779701989979234492/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^24 + 15035725796083860058292982171993250372120654368102924668160899550114873832599282894164466637258323020843077/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^23 - 1168932570476130617999737787175030866627340712526575468482742033489513100264331885594695846229161516903863/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^22 - 12550329523168283509488547813380475148515872019401559084644445524546041963820644530932788968216106973022472/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^21 + 29575751172138125313085440486537780654907032268708180770147169832492307878040548065580045823108206162180740/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^20 - 228931698390706648918785522689703853671589978155370735095472691205395394882477108196902065265919113156954295/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^19 - 526184675182889450785594584216102525117538130501709159985943879315324849970287846480374468932955401467368486/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^18 + 977359407212837950430349433022608592502331297056127811173997952049523749278031046875720307114848996441096172/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^17 + 4077527862638006385042268923068607862702468227229270202884168292595554237235495077992607703329859824528383201/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^16 - 4687911326805594153576437919220046739148726566764754798509101205611544671994130057551123914504610894665260692/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^15 - 3537584646223259987511450070984591889360759857101003016097285123982422782359841152803162728006673941023457520/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^14 + 994735496565346852665253970859819490118734845364204926837965649553844635518292490445048783630443298565942169/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^13 + 6263005347158389924283448923619559904714083098414852789503990974042744926714800645724654119495142724125760100/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^12 + 252556377447440102073156593647485854059325196212713354595934048579679794931376295429715957394887004745066478/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^11 - 197131546013066878067736674311912029915357767792694215789944401775002755352195044241305563975258674672095633/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^10 - 1083174452613963846302816361258865218940189282813645256651927363801682433624215720925205281689885721239157792/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^9 - 85144117319991373517305260776004677773979898181392807996060714483733594719235506587403294043211936806929121/1416991441462023986569064066553867260712876295136461027810534707197401467108156942618203725519779067713*y^8 + 511064290084691206060634493217037086079834170978484851383222301790892756778398525610707599514096316343776/4250974324386071959707192199661601782138628885409383083431604121592204401324470827854611176559337203139*y^7 + 143366421976739369064590108187697804243153664543657570742117606377412983624581492029023210131965910498822448/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^6 + 1731406890513531886167159273490978131815259313787184457503198840397775698861442849050718519249810885847411/472330480487341328856354688851289086904292098378820342603511569065800489036052314206067908506593022571*y^5 + 10197526855521490078711934853745478735339451642788453486975073868344381861200175936693720968558732500445813/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^4 + 8980318358438492860638751016873287914522378496149374464637633089052144063971999500200439610415484349042/1416991441462023986569064066553867260712876295136461027810534707197401467108156942618203725519779067713*y^3 - 5384977138065469648054648140000844844890929536885312419621745854885872447135077803436626423230416812390460/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y^2 - 80934745789440963381488134656530092922984363310333963093302761482848778466916067019562561485556217417694/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417*y + 260493438856430049521424269804423244458580944829654286412649486660217542617627461867046566961740743319189/12752922973158215879121576598984805346415886656228149250294812364776613203973412483563833529678011609417 # A Gluing Matrix {{2,0,2,0,0,-1,-2},{0,1,-2,0,0,1,2},{1,-2,3,0,0,-1,-2},{0,0,0,1,-1,-1,-2},{0,0,0,-1,2,1,2},{-1,2,-2,-2,2,3,4},{-1,2,-2,-2,2,2,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,2,0},{0,0,0,0,0,0,1}} # nu Gluing Vector {0, 1, -1, -1, 2, 4, 4} # f Combinatorial flattening {-2, -5, -3, 0, 1, 4, -2} # f' Combinatorial flattening {5, 0, 0, 0, 0, 0, 8} # 1 Loop Invariant -27304548568386361904826620124069767586773349355857213684118987180281706249534094268610091724903442887949/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^28 + 233755241974983740797819276591768391761338794452498066536835815756657893104836423491072076016416068458457/1214564092681734845630626342760457652039608252974109452409029749026344114664134522244174621874096343754*y^27 - 4392525297748267621018488222318942602068012925428470073207892121976294547037084677768540776020555298558129/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^26 + 11311907123010157871276169387766950242303255164859485831530095755018295833880212709033850106353064836946327/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^25 - 22804715171821253815471767581861109152062161955801186274329395821928548030623562757991705766234519106016610/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^24 + 120877691989219672333041598204201079578693214112071668855923945817133810009052894439108828509726638152541659/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^23 - 38781726823360041063080230946764500106791361572570978680409470496510905683201408587050881700426398443184913/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^22 - 200042197588258758218574789100766533119838532666269090770390168717797964338649817589625391847091369636645563/1214564092681734845630626342760457652039608252974109452409029749026344114664134522244174621874096343754*y^21 + 1664530208294173719917438364640819574179298106713948126364521482571149551708999893316217680441608971347344521/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^20 - 1858559530978189065355453317046978020901686545710625076929815683153586576369983210636687296905790286331402897/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^19 - 4014609356763932778042202098483741698866716238215262324195823852211369404315862639894721187497183426111692400/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^18 + 16302375390344639078193471472757924298881572580982662597049522276090670822663827867988247134755958472574110461/1214564092681734845630626342760457652039608252974109452409029749026344114664134522244174621874096343754*y^17 + 30547617203192902936516122517104111434451814049997454767960301082120735585329779459573167262895151519331842635/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^16 - 80871443380056476644642259136588043425547516551024114190629108485402652185255657110163023139513778745016814181/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^15 - 51277353609184449145426652660794004163373593324682376870146953321591577454538984041586455028856818737560042633/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^14 + 116209760451549237694604567771325222841804845879139164519285661551789748428580264142207723734032938919438987877/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^13 + 45507775630261258869094562618690156779059935223630798317391986264842572262126271000745232576929192229410685250/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631*y^12 + 68185157979162695231899816492833452442098796309363403587427589358899920577336199771146222196403036779791482/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^11 - 2300230196302506086749660495850083839654724483905657440520692292974578438631184461164159493750532861188393029/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^10 - 18193230280676524153169538698077151536402451231643323797060518321173781406481696592175015442638469829450722417/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^9 - 3697115939098808455618347480683454195993190749240769206359978824853874787977504336490617075034813625856787073/1214564092681734845630626342760457652039608252974109452409029749026344114664134522244174621874096343754*y^8 + 232140854124978483752568319847845177004784229542975097240209366243376290071814215885614782797230699239131186/607282046340867422815313171380228826019804126487054726204514874513172057332067261122087310937048171877*y^7 + 2703769960700371332220536912652922049046912828723597365449214738375912370464714673825866771188509500854604583/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^6 + 243519981347501721103962455465098313511406270674469535431319233194873879002049739324360805034955521884817727/1214564092681734845630626342760457652039608252974109452409029749026344114664134522244174621874096343754*y^5 + 111223931675016243613562472889199297066505993999002370822832966167804493542036577182587225996549165778876799/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^4 - 1791273641689642308595532088286062074448149060846441102604133531460713497242203840875805251777229558594090/202427348780289140938437723793409608673268042162351575401504958171057352444022420374029103645682723959*y^3 - 98438128315584110734524412451056591949529758774444110028227788100144353231232006051539030802586520994868245/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y^2 + 1665910672359507859369136363568691213384873606175387760284603835774645870197420523427378322199047144969491/3643692278045204536891879028281372956118824758922328357227089247079032343992403566732523865622289031262*y + 2229650009408913195117630629656438637599418525518356742802834037415154960305032616876595798342352276352057/1821846139022602268445939514140686478059412379461164178613544623539516171996201783366261932811144515631 # 2 Loop Invariant 51702393007857853908823110244591878971699178256927647044571626325263209713720393549378835157870297266364893480460431064928903283745988470927428550969729891639499576996839865646506157849331700010834961/7877946185160824180932829395857101764740507295234485747922229714363104446866239242790952310659418767412154170878001864415596349318256667703823677307654272389592861666417866467173001292952316893450084620*y^28 - 293987934854659380963175675523786166949272269763770285237711279312776589304001583371162098198265081755253922674411660725692477700937913116157778739849148348379984834584054012620399679913324603664672649/1750654707813516484651739865746022614386779398940996832871606603191800988192497609509100513479870837202700926861778192092354744292945926156405261623923171642131747036981748103816222509544959309655574360*y^27 + 32770095739446198218659120220668499621518278330374377321092527421685340976948874931369926882029603238306663983118551127252824069564763060138848196174290210376416305362176807377958092429711536447543002551/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y^26 - 8268020305703754709686988945472047935205252939547143661930855634727497776090832153557119551824007136207481019709012681472654040904028149897422221424509805296547788379821868193371132197811704166475967369/3151178474064329672373131758342840705896202918093794299168891885745241778746495697116380924263767506964861668351200745766238539727302667081529470923061708955837144666567146586869200517180926757380033848*y^25 + 338281861644156528607792311519724513874766352471616055473881904280886684958124023099393761455682448508912008070434689543209788013633358525708548971120441458194661691804311945011847246923951552383484193739/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y^24 - 1800283049075617752528976033024183601321122393102995957379830256416465069022841477614347726362670395710958337561599110468048254972373948653200816439074467547602313462340398788618310670787809086454198632719/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y^23 + 25809659156218046665627574829010683623393838978498379677261116381097660606298602527821817768185413433592311812522098608134476073161531627809080368076970251320213589363937617587804888473321306012896941453/6302356948128659344746263516685681411792405836187588598337783771490483557492991394232761848527535013929723336702401491532477079454605334163058941846123417911674289333134293173738401034361853514760067696*y^22 + 376570875168035080633714094813565768504802324794162903105984454347237166630928305423962762533234535725822150951090957071338438523015093930504512790354420554542059472519883901423629652193060640707416399387/2625982061720274726977609798619033921580169098411495249307409904787701482288746414263650770219806255804051390292667288138532116439418889234607892435884757463197620555472622155724333764317438964483361540*y^21 - 24813475772794420566980121979431098999699343400454516022877255386944747687893470046985766668888363769071733379163423166922471262765549572972016046075150996327587899535065294719906985547527561444864328782537/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y^20 + 1369945455581346657330426784504479643817465340711154219533170943888140813109075362500643639075282393156664158305208451076985986449404224571445458938212570805852051259011732998547157275650634385630125960001/525196412344054945395521959723806784316033819682299049861481980957540296457749282852730154043961251160810278058533457627706423287883777846921578487176951492639524111094524431144866752863487792896672308*y^19 + 31626394612826574401342149107938289854644867263737797158981120138220344139819764902417774377212655967317504920457391629563337532218657393776523414242313763702534569798346045525273561128125072358585051532621/5251964123440549453955219597238067843160338196822990498614819809575402964577492828527301540439612511608102780585334576277064232878837778469215784871769514926395241110945244311448667528634877928966723080*y^18 - 116914295095514277520684420592798674514318829455327950907625785354791679507980694375459976616447984040387668150974929259341677516229160418550100639889920099725212688689400723415311838748647998534761044035009/10503928246881098907910439194476135686320676393645980997229639619150805929154985657054603080879225023216205561170669152554128465757675556938431569743539029852790482221890488622897335057269755857933446160*y^17 - 122503022964735122426544004871337947598171530885568313318032421758804598264100131669221901173142595919166885105804483416365922770637940180417988413159604300608112005084166842755310286078078291775898636361689/7877946185160824180932829395857101764740507295234485747922229714363104446866239242790952310659418767412154170878001864415596349318256667703823677307654272389592861666417866467173001292952316893450084620*y^16 + 280691152012537318732701018528468691386936960644072586446028394509208191700648142580821308437926500023790476688947226964527529186671884750036920395036187932947513995315313716120966698589667066116976846771751/15755892370321648361865658791714203529481014590468971495844459428726208893732478485581904621318837534824308341756003728831192698636513335407647354615308544779185723332835732934346002585904633786900169240*y^15 + 424054353609920356966769728569517603825981625765701735955561073161445915844527234812666239280869947435738474547740407055717127507072228197972553938179006600026601571371182533374156175699178500853597345758707/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y^14 - 104676319528043438270741905718274367867025317064572309639952684845487264056559437709697420118246820033359976143729456347626260569873113456751314430738229846221731807691396600935010357851687991428126742545071/3938973092580412090466414697928550882370253647617242873961114857181552223433119621395476155329709383706077085439000932207798174659128333851911838653827136194796430833208933233586500646476158446725042310*y^13 - 187712363850067439307511613677995310006989965121811043220382825130085470076100638162971175600920418172731509465451313591941869725545078517847905019702103085922264562093284483687179718407527406540884059794667/7877946185160824180932829395857101764740507295234485747922229714363104446866239242790952310659418767412154170878001864415596349318256667703823677307654272389592861666417866467173001292952316893450084620*y^12 - 338256344326024042923980206667375014135205451498630970162185190931673750695210118099666557689178591103763051956263262789639624868954837946717929734470787786880835190103309869181334789918664379825559366813/116710313854234432310115991049734840959118626596066455524773773546120065879499840633940034231991389146846728457451879472823649619529728410427017441594878109475449802465449873587748167302997287310371624*y^11 + 21093654675483739130290053428077961945094541075123934701563851065047388028580929391592530346891474016068165304926160318195712936336871526882670841784476040026575227327560183733123412158118596563575914700179/10503928246881098907910439194476135686320676393645980997229639619150805929154985657054603080879225023216205561170669152554128465757675556938431569743539029852790482221890488622897335057269755857933446160*y^10 + 122982097040543546524821141380854765543808876577821080191339661504166160134982987433168585744695328648219659187976543894831496422323115712958209350258455103680480143647984891010813908184748786824192054669973/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y^9 + 4963499963758212292733824288414445081547295923577967978913390482209469880578209665317012893888266250797017463744365772673161983268443225332474339010365686463557462292081440691741193744128704694116922872179/1750654707813516484651739865746022614386779398940996832871606603191800988192497609509100513479870837202700926861778192092354744292945926156405261623923171642131747036981748103816222509544959309655574360*y^8 - 8184458837625255048773013943575078104532557036236654249315850451182861551038767952367337318538528948663656265774199659202264383871862408315972736368048674596045639460816226946196428906815332740244800353/233420627708468864620231982099469681918237253192132911049547547092240131758999681267880068463982778293693456914903758945647299239059456820854034883189756218950899604930899747175496334605994574620743248*y^7 - 2110823213573331801382580308864317239020144795400663344362193988583793776193770734819654033969752034592200115864218622713147120368135815572345625458426924495664708134269177414252869987165248693393029021483/3938973092580412090466414697928550882370253647617242873961114857181552223433119621395476155329709383706077085439000932207798174659128333851911838653827136194796430833208933233586500646476158446725042310*y^6 - 106228647126358203915267286369203809631645490354866286932012044826136588501246189018414918129352350982657126979127710468434271759207046173468433498993349658761261217965217429132542708531163841865391567206/656495515430068681744402449654758480395042274602873812326852476196925370572186603565912692554951563951012847573166822034633029109854722308651973108971189365799405138868155538931083441079359741120840385*y^5 - 1040999513639587190972932025583766168694721522079575451901541920261640235708160947046311648823656899428982276009212714432350720853792752017452249931329462345195319039931383397503831630390506156282948528621/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y^4 + 550666947575263647696021627512219853775370036958263940775849138469450892907884936320876119374353301258606454532673393487217793555706720887469885585687220976911898956286845235531570101926861267981121709/583551569271172161550579955248674204795593132980332277623868867730600329397499203169700171159956945734233642287259397364118248097648642052135087207974390547377249012327249367938740836514986436551858120*y^3 + 324560978626815405562347402419740644843820506317810975823850059079829511416173883498056873319837027648132711923992426920809794797746303355100704869987061249522293342468060219247083297349906981220656709421/15755892370321648361865658791714203529481014590468971495844459428726208893732478485581904621318837534824308341756003728831192698636513335407647354615308544779185723332835732934346002585904633786900169240*y^2 + 3842208380332154309752745667943728649595696591461964462463112933843179276313511106248929514091285403647952027411760831984182649678444068347535601524887797752766126501876234291858521020938724455657320699/31511784740643296723731317583428407058962029180937942991688918857452417787464956971163809242637675069648616683512007457662385397273026670815294709230617089558371446665671465868692005171809267573800338480*y + 10417329722085656927632775200357637478177211244526385468415100493302720258259186263901523185443843347635615414230150445734683589811467405706146830666189857670603422387184210602567908544320291854574547261/6302356948128659344746263516685681411792405836187588598337783771490483557492991394232761848527535013929723336702401491532477079454605334163058941846123417911674289333134293173738401034361853514760067696 # 3 Loop Invariant -14650603335073365607998404703244911323910815774793149354668489158103473915094561198621490743397373486426732181152325134789600377927070699656538192588709964903779729620143847627657541462241481469266593722093071582911768220372833293122648066660134356621/4633494585811723836872529403199141093221914427427520013351892829766144492125054234009003728887826725766271668400062350040896624549500036862498113400413453923846401697300127699151925859892217901146823275905092246347786289574826874682469263584295271824800*y^28 + 249984811582243269414381899757458857075300764011033725392212687810096383870325849797911708461786985279455975169726055022582437970411784214744304221534661810423172145788892154942710016604061258759989663021962230923573388845181463448436673080675187434897/3088996390541149224581686268799427395481276284951680008901261886510762994750036156006002485925217817177514445600041566693931083033000024574998742266942302615897601131533418466101283906594811934097882183936728164231857526383217916454979509056196847883200*y^27 - 2324167650426223933625259892571335668866735904497992148290937010275844246469279346271935215496609828279140090480789920011634111179178996318441395999720137949199112702421426008823162040802509795105876113347574926338963543833177534515027478182279661525569/4633494585811723836872529403199141093221914427427520013351892829766144492125054234009003728887826725766271668400062350040896624549500036862498113400413453923846401697300127699151925859892217901146823275905092246347786289574826874682469263584295271824800*y^26 + 587580177139232990996697863483747758090173132834595858743438168161608310276232079504079594156793819089969159411719603720775940940070519939003874734968718603869926996227393972193500538785166307524772985484865935582243419518071861779258536848988638085759/463349458581172383687252940319914109322191442742752001335189282976614449212505423400900372888782672576627166840006235004089662454950003686249811340041345392384640169730012769915192585989221790114682327590509224634778628957482687468246926358429527182480*y^25 - 48045358223601354965461507481813760642177967268694929770748860353975469910394096141794483271149112509441641391823963208628486440783780136377163591156647344453677468950837356017023923475354718989396985042371840560309356343296019380591893996246775215138187/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^24 + 255512985482456313837636306807745405641458132253085474502679727143279609942518342879350645345826358601467124915636063120469573309400400892391650553439876640965944844676994753720148641113789597092508240433764534874709071130343503144810091144299943099153587/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^23 - 4093157334728216656715650959258752763508209276420787934450042145055992602096086711568609008573850717327519966178994019857349913096794118684974635791580912280051154620600110491542187642789122439207152317131216251298287154122244256734512318123526201311897/1853397834324689534749011761279656437288765770971008005340757131906457796850021693603601491555130690306508667360024940016358649819800014744999245360165381569538560678920051079660770343956887160458729310362036898539114515829930749872987705433718108729920*y^22 - 212693290107362868626955617445842406423821169259551211816985033100667360878041346574338415356482240231308599212124060156558381838502296519426206722234829410005286461736824561951667555109094055721859377127151555802420495417892714547606341517069790427477279/3088996390541149224581686268799427395481276284951680008901261886510762994750036156006002485925217817177514445600041566693931083033000024574998742266942302615897601131533418466101283906594811934097882183936728164231857526383217916454979509056196847883200*y^21 + 3517891228992771889089379238641606466353628643881805061597306863716479789455768963666169312969717435412679112760520725336242687376768498972557589314953945570526680107937334954261695935284017155231280478033660451403125014128147738964595008051603702639326361/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^20 - 778229924341383540708583629081569260051466414433678425367655463504775045323602983565331112457775430777907681100937699760108232219311286823465773588110649950165447103379304596003562320935227655471435851330800924980097892324369694132917642924097175323156297/617799278108229844916337253759885479096255256990336001780252377302152598950007231201200497185043563435502889120008313338786216606600004914999748453388460523179520226306683693220256781318962386819576436787345632846371505276643583290995901811239369576640*y^19 - 8925870542464190864316207497435195210719312260772203689115837113686037779154810270901797411337867523912170228670647444257252058145472363039608897260611380595716865291447320928358038493484146933196189633106630535532880231154039631500348390142466767044402211/3088996390541149224581686268799427395481276284951680008901261886510762994750036156006002485925217817177514445600041566693931083033000024574998742266942302615897601131533418466101283906594811934097882183936728164231857526383217916454979509056196847883200*y^18 + 16592769813723306131622873051664666715485585607505712109806499297903217081708768062295439957364902203965709541779245116945081650414525205160097530731495493502850573804222447039669737112292076506941085914312735886535608073897245827406796833772832825408094507/3088996390541149224581686268799427395481276284951680008901261886510762994750036156006002485925217817177514445600041566693931083033000024574998742266942302615897601131533418466101283906594811934097882183936728164231857526383217916454979509056196847883200*y^17 + 69006491280906623368255233911879963688140269955563783931525840772323649408831919749936613182817648716236181832507670926066829269984823605731512941464727592341393311719313151291612653890857569394030416181678593690634756226597613465051277227859105291987075993/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^16 - 79537955280679571447097920797875030099980514444376692855020681871410900098753506825141432237167109459078596574564866012573036387919964802840986797635277404875905324433784246757009687679556677956758158538305326124254880077897368131267680717481805193095928131/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^15 - 7437865824606069210189307752318945180949106171648401447741144490451981436097001541102031306605402163427671474117285937612381690726290022780393573708650924550649769501876520869388819306756591756931446656077689285544366622734713513248251373987941255215221677/1158373646452930959218132350799785273305478606856880003337973207441536123031263558502250932221956681441567917100015587510224156137375009215624528350103363480961600424325031924787981464973054475286705818976273061586946572393706718670617315896073817956200*y^14 + 59105847230664350248353602762485125439317626079952461235102146874596512643858662133652686523715253773864930638889477707032186398806860790338506457098966991138891481800869872986293097113620594947640639356053440056544014210787706457930675938548951547110636237/4633494585811723836872529403199141093221914427427520013351892829766144492125054234009003728887826725766271668400062350040896624549500036862498113400413453923846401697300127699151925859892217901146823275905092246347786289574826874682469263584295271824800*y^13 + 105839342923344436630522169274503052666990006166246840077170886082825705195774452243754927124581357454660328840321987607996226537780954417064841352323919577356090386223858249170328016947925634005412828162040513353882670830624689914619388765247772551153792429/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^12 + 4548025366865888426916621657073625009788280669493194676053391856399363695018486181727676073414046126511336865324782367371731077354577798860672627887956713661302115819515773365845855388478397566612857773313573516736427550488367001552568853824300104975929/3217704573480363775605923196666070203626329463491333342605481131782044786197954329172919256172101892893244214166709965306178211492708358932290356528064898558226667845347310902188837402702929098018627274934091837741518256649185329640603655266871716545*y^11 - 769658318856834495077997795874947498168385945235142274628096309592611415398275640796904526179227275435945095569069820418294012539930310079303419758739647117812443915720809620451471999071348627535075201949213966013236023442099995916912505347450212384930213/772249097635287306145421567199856848870319071237920002225315471627690748687509039001500621481304454294378611400010391673482770758250006143749685566735575653974400282883354616525320976648702983524470545984182041057964381595804479113744877264049211970800*y^10 - 8865798030134632230583108874925917202584493821287924727529307939235006763572169260675869450160173199137064288350644844131925221565838668290189363355122500311745882468120935446175930908418583346622150446329413461756942028432266586272894492991153589740450007/4633494585811723836872529403199141093221914427427520013351892829766144492125054234009003728887826725766271668400062350040896624549500036862498113400413453923846401697300127699151925859892217901146823275905092246347786289574826874682469263584295271824800*y^9 - 4219097536474424352731922268707485626716700707471925199634892023922694384767966981033823177163711332015907259835217876928713660037593186180757342211277697625826040175211036076515097731363246741934345574244529333226513555057123833124116381873404543558259567/3088996390541149224581686268799427395481276284951680008901261886510762994750036156006002485925217817177514445600041566693931083033000024574998742266942302615897601131533418466101283906594811934097882183936728164231857526383217916454979509056196847883200*y^8 + 4121193963143699877892633187358289950928100767770202724034957849063931424206294175465606184489549589089956439223367096066478984294098235144996938795969565010184477941285505835838027903470203565993861418226343967564757200705826569455481625747889139332623/308899639054114922458168626879942739548127628495168000890126188651076299475003615600600248592521781717751444560004156669393108303300002457499874226694230261589760113153341846610128390659481193409788218393672816423185752638321791645497950905619684788320*y^7 + 2385658354448004044123901234728911447449569740076171859302154323049734364643967411019539516342767406325471883312265839876298860568494229521820230969904254004778825570459574967322756895494325744766433185548868892875862261587766061598172298137684365617638887/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^6 + 244484942042796370816106072573461947142412210964515753097128561360667833572270207046532118698053292768572149466980052039004622684388993649281299560919586910713738781912882918175083341592946684987335110344394631537215457314515342620346677810315639470944043/3088996390541149224581686268799427395481276284951680008901261886510762994750036156006002485925217817177514445600041566693931083033000024574998742266942302615897601131533418466101283906594811934097882183936728164231857526383217916454979509056196847883200*y^5 + 75836437862369122541591263189342883601838630655914832168882761165514655519648963446524822398141632280272318662334271452848955037519536209858899546832248331758708895609317167221951454627483697073701050803666825289684697821509340788802653878232340222140009/4633494585811723836872529403199141093221914427427520013351892829766144492125054234009003728887826725766271668400062350040896624549500036862498113400413453923846401697300127699151925859892217901146823275905092246347786289574826874682469263584295271824800*y^4 - 444519113093902202753794580486654923056049730142895349751153540111045392286522606034768430573564271889407749889415767947471178246273841357749929925550284336737123237878987645133102162462226882998285713668339749010283752300548521606497410390445156278227/1029665463513716408193895422933142465160425428317226669633753962170254331583345385335334161975072605725838148533347188897977027677666674858332914088980767538632533710511139488700427968864937311365960727978909388077285842127739305484993169685398949294400*y^3 - 90919122900397476538423978755790087879375496671837008167700766274791603640738466900119418809290811020243181324580740501475493663852001693047391140561850135313730375913850991256743632510196153116541135616237030875250202951908735786031076716334228415173541/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y^2 - 203960129210342959223328713059280689949716564672999239595128097426742063869426549278565979878053845524166031696804234566872770715026863508280436933689170785289454773597447698128450150593682165656845324054426227434380430525273905089956090131781529443577/9266989171623447673745058806398282186443828854855040026703785659532288984250108468018007457775653451532543336800124700081793249099000073724996226800826907847692803394600255398303851719784435802293646551810184492695572579149653749364938527168590543649600*y + 30412216684662538406249241396499965485164017539704923481723183339353285668290628794279518493658817007741150489959183806902943820481534720825534842699106671570132323979317664582486522663039213451159385233859505384133040147608404163530926985443451579919/57918682322646547960906617539989263665273930342844000166898660372076806151563177925112546611097834072078395855000779375511207806868750460781226417505168174048080021216251596239399073248652723764335290948813653079347328619685335933530865794803690897810