# Manifold: Census Knot K8_18

# Number of Tetrahedra: 8

# Number Field
x^30 - 4*x^29 - 232*x^28 - 1035*x^27 + 2219*x^26 + 16529*x^25 - 7642*x^24 - 157745*x^23 + 340716*x^22 - 600809*x^21 + 1732487*x^20 - 1947636*x^19 - 3384837*x^18 + 10617554*x^17 - 7237589*x^16 - 5439954*x^15 + 9377681*x^14 - 918094*x^13 - 4426827*x^12 + 1530778*x^11 + 1121208*x^10 - 555367*x^9 - 173147*x^8 + 106367*x^7 + 16867*x^6 - 11623*x^5 - 814*x^4 + 669*x^3 - 6*x^2 - 26*x - 2 

# Approximate Field Generator
0.458581908281963 - 0.281416774232928*I

# Shape Parameters
37513115819168841629956713533203743038770629704003575830883001818069328648098630475990817758917866/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^29 - 162610448867586608870542674818944468519031830930815302792371544983882742164964370387162687512562440/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 - 8650616294505348329156734660518302811607169208612511822363290908872900751310743914640585155585708370/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 - 35922457462751122898902491653055958471719227857434940103601847288543477574159472061331087893594995904/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^26 + 95734024749818555769019313709094446171874660147301496501067598775965147200081511926281556175533308587/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^25 + 590162337050437167434978407622186222255723127898524715955746245684561013964625333035764290981318166552/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 - 488243439527184661933853212444284789576078257341503419318821047703886199898275551942034209433579222041/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^23 - 5787398147619408145098321990976066034319424540138143867078316036643323030161198731619948536758871098660/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 + 14727858559296222092959945276863391105744826559867154731641777914548250702534614187579048994124425538467/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 - 27158045738653546513307891874128516286863015068096245692019559425538486942950808434186635441345186281426/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^20 + 73448876867953084746359873076214064540802256215756306664516662204731105955534120246092558516320554981090/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^19 - 96470994022093774939564431657399463192124355787871523630386515989314137990836839403334284779453634724287/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^18 - 98112030542010408202121308926453191466451792955074511133872954372266322912736618995593084418315449356482/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^17 + 434756232344141745789413846683630109377517456316550831749951104656210746719139810265893415156740495310929/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^16 - 410419610920452385531580989032999856211414363180073388834777812318778485075753991031189278552877159272479/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^15 - 86220144756047060685648738166242205044870756081989751480283909462223224311241223203760096941011635318689/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 + 393760225557075007548708556085546581896835914284735348872448032304333198353600086239080125812296385098967/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^13 - 157641338089168560209720845859667337712206195644596518269414722654513403510998255558896754421815505969570/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 - 128399665168048114706372290535254144982653703533607298537628005467272544869401376501174520822342322845037/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 + 102536429320415457983816146745546998271703519994920847817131487104572633316408684182530546738395690192460/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 + 13604045733529401009186536467640956761600233077468144023937431245743171003471533140843182887542892189786/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 - 27726469497562829500059457216724712562436518144132064443358684887169181058896551201349748695917613720904/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^8 + 1752495767034560167964836460975102608514213499387106307133544189383266141296553310838430141156378630022/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^7 + 4114384859649085372304292588343465706970614107829381879131702673806823065863362986538751024770380844468/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^6 - 684659202427336858657415678942235898956224251782993739577745805441954842856845202552245566107143408613/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^5 - 334626733608210567521855340931972870095777647403232958274021193559077489236654499443757664657802750772/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 + 89580194869619311163096992712472302932056948082795617500586336166477612297164043904304993356770557466/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^3 + 9595293239693543085880398857580051417633819488374846521655000401711095256007652363658213878991859789/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 - 5567367212054691672333039747899558701565426339453807675595768552790773495247396827685618470776565280/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y + 396608112010535844298305440383386919303457633363623442121324253991916708824989579524677309690320800/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891

829952291066786645006605688061521975586493119593363649414244550699272725300061626147561219676396711/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^29 - 1665309702207074655413184042295657990067369047073488213605074693961323013244399481637151236894587523/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^28 - 48127228537447236347301797124851927392728226656265562957358383243289870611120866928823546720459926380/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 - 856474422256334699341385814086992102909649346709078625079253761311217805212740666957952268925377287291/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^26 + 1853580191894788743572352521581975972687656224438553965851017684593857158302275526900501476445874738663/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^25 + 13696390412263168058792042130869237948710517276265404029196501313447546875569449356312813755620542848885/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^24 - 3267029126733135060752077735982131836455698478431708621123681131970720681596828931111908160171679033741/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^23 - 130880707570720235562665547130440246599468871399227445073741258600662569984459660338524411794744924144097/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^22 + 71149405452566312326452617851334124446303422756440429150166482130664859226132343484894908336965054261806/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 - 501841842976936316687918468232931874512830183389504822738658584316480334725965192020729076709927696159007/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^20 + 1442438257922488515161317809398141831973775124581340621219251877370510973316196401682224607794802431648157/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^19 - 815786269866422292674560447728966578356979340324621429490250919033416931763099055879458464226685321166215/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^18 - 2796758369878399435959501002957136521759250391257770722954967203239614290987631015901064309359258543641801/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^17 + 4431904284743098443130119382953840758131218362456868524548512400138211407566383544950620737383277940942975/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^16 - 6119781383505848002454790349490913712487295316675538381813821581350888617503479948495029947210067784566995/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^15 - 2244947814134283113663279458420516070123004764992549841618538268989327212175298516742880117147719451633537/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^14 + 7917653331827845947005684865148351950082937395136264648684779424624171147431721997486454156150129529172859/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^13 - 438377929373733811747230465579533157226448881293713695137076033979070376579546531159047440548154161259179/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^12 - 3723778015466916044437477191655414742041703161041801065317262146923629448608478137188863312151481683847869/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^11 + 681588711794817522776404502120291532729574665002051383063618628902249004040806990579185074551838214040965/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^10 + 231649024926254675260363808584233479121224262899438483486112518601661686688815296114876403524201483113031/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 - 496231363412251710031825949145375217999158312615191847439489518985256980394217963527856211100712337691143/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^8 - 136015749678381195205637079942073103715414407303888588444082350998304667996368333792337746303778805963551/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^7 + 95448320820287169600773979402279543002614282082111495676921272783950730239291788855827205558964740645115/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^6 + 11798165644422890557983785942946294002608277141673815643875488361950537647114106444774160661317794253301/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^5 - 10372603478317514513834857215973201588463850733406961749322087078701753503517126668071638920551724782381/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^4 - 194681204194958418078319724414561221115624877642996838105315216305956831000687787111295620176911374785/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^3 + 569931976198590931413087337037080742306973191314600966970104461871911090018200213800213354875386387969/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^2 - 11921781563540831702162425052496642607993439037411150739654843562653485664090429880679349588696556477/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y - 7394358166885120567277382656595117972763526437716478199782070342187434084969863050179610180850459647/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782

8293558866219007465606740231949481840442129882279316141065101039991113443801581516648511581743066689/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^29 - 8519603122743774195000605626746975469241219758854146764581329689567077426693690842617415900483207772/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 - 1920392403559371744121041317656172817611830563806975556792361123429648954850974988663509056260974573863/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^27 - 8374458357857317887115878815864932805960047513351662223928295591666677829368361039745538113366161338949/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^26 + 19316861701036936139713455296468460302310585195245589621836764614225141972089703925332772445041277383249/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^25 + 33744939981359070543032516288419982136931282905910300307425197361216471863231216064509925798223214844004/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 - 78101859260310933981052413657597884495000249739621893923092968717428027289423698963393319071586559720437/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^23 - 324944375010344433413576275982669891930185862492877549856129283950424436729620739156592632475902183573536/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 + 741877316661445121516738832080534500592222528771595274449088575149641334905998265671940476231447426247407/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 - 2653052945267943257880635991471228535046682663410059612072113412456668224086438931957006573542613583209601/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^20 + 14945835309265534553133597652709445840287705463477864391457210446520236555333695422962689388308308425775091/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^19 - 17779781612561814782115725655834649335752307972220153400467196264456473629607368208789816004706286963142391/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^18 - 13069832125716966412201836570920587826785216898226901562895233361022270671273809801546299208866245670576335/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^17 + 45458468080177159432961282084068786654666690962076784569344400226674212317402159665920020780885557849493625/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^16 - 34969606162419905370782441288585769796459978243577076863647342925452550585666397451297520400026383989693775/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^15 - 9379881731620669588276240286013897354562813474264548048340388153452371650109219725283436069428699321358949/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 + 40957792263547177608695200985280169173324671398802318515695015769005942001570966849666866061270367826065531/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^13 - 4142648544175101046480033417665839574264636469990066449896847623612898068531422183899407184189001642844591/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 - 8732947921500761841245917170484784709319632693002298409600408422114835725112117283056996893364400103574963/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 + 4134494693158896892422194687572908702487203879342326041672415689973337052001942152576330640191487688627884/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 + 7492860974565820865515668612306617434475495850700098792897782306602139597696617130780659898294598475730087/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^9 - 5436832752496244330876184287195484480803064387215657735295906024495014088883387736201426405914586469950297/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^8 - 838946736764757242986385598908486491543772850550624477875359697451888746611837062794535530958096968183517/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^7 + 488365291345430548947715715061346108964914438616573444768348474168398512726455525187264920039625081350339/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^6 + 16141562409529304978408465295727289974031780824575450917045158854104360532930277050733109724977849975489/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y^5 - 25097707355565370299265065308880718090151263549097379861125544778241489094401634936840185315123104869751/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 + 4330013196936015511999133997351300352334840351122855028188506596715250369916577117414068418635749546151/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564*y^3 + 1281828408399646664921161697164225039588586707751464852456156304155210095522411314069005610943523919579/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 - 309115814167996468483541464478886331761000945630037202439383338222485001004552846642302239838624594939/925883325148278747759493378822499218749394095004249402989010510491014944481244465195620511417551782*y - 151993915192788900278310939346058715867674041578690971579405077152823826107614664378313294934786143573/1851766650296557495518986757644998437498788190008498805978021020982029888962488930391241022835103564

60740390929716344808890140012981437297218053831884737816204069790842230862375436291305771002103576/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^29 - 251964380487993119505658383207202632881207951708818850130658944683652951590566979838224016677222017/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 - 14058080203423478511571076079762159859506116106180735356706089213200808880096200022601690641616928535/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 - 60768562749998181041718087590417746629854692025576608917838430898323559545763507919033821152213516573/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^26 + 144640005841627903890781169681382650781383616621142847115128945794647054409478594632025865473733095750/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^25 + 986447930649765438090786668646360886193243886217960581007651666732612115784018636558609692790196433753/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 - 617925086834015258073831978796650786299472711305797323435804800851224814764336748985060962694806929258/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^23 - 9551435271134960248796988466924080481166377127406517994807120164344473952423494150514552163705219460697/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 + 22129809420202122738351018367026320307860786847460173791671172664386569785437961634469983010289694143690/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 - 39194259192303349585722442373399215317653557036321189155663791066520001078550336690120589127484113314934/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^20 + 109880475670594140595350341702758115562739524006235133109405794842025519447026719286659757654669448985123/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^19 - 132558769181532330875156669810928497261334173136319406988084550996412869557448427731385663715907621706789/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^18 - 191966691132867640879170303101387210317862636863436630370508262888153689709150310370864015272091740485519/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^17 + 679531280430872281816431520512131405847396933849897379745740792021013908506364391392824563585289345783910/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^16 - 526925732578284440465997334247100343914577628584776680933792888930438225946483056594864292577458387293147/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^15 - 289433830750123916548682502806279212715646652106921172454445338694820936448206195235030683008906577776229/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 + 633975323666988177111698127964303767192633071640012353287555218177673344571459846197291487898503322565399/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^13 - 126665661935419943161039043460817041278292298637804598978567483902510617001785418086148792891748249824325/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 - 282584792398183833313344389691385848317196114965998702812205626955291524822981140713259282864160224010794/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 + 135798711483043244349889793515761711368295517290267555930014146281142295605111407164175631868470711889686/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 + 63590572345263416447295283556474516314548586203415904542212096235383815820517405106909961202047342528496/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 - 47756644870852206594931861455379328090374287137670013688533954913356138161143021731883001654490853101978/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^8 - 7130120597624973062567629419027922484323860104572053080487238085295641938990154413680139029574835304752/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^7 + 9141380561732890093250852151432890539743791957601249194294639177238124361813996613566514603981866773551/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^6 + 167034789546350060895788991359233261696813674311067792377193026162138755546543414229591411721846453360/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^5 - 1002963473892387585125924919592778669694869026928985614260063818779640215482199510633049471823571199716/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 + 56827349025462029172248331472412594172034168274098119964867769325521365185295034074036431264201533813/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^3 + 54985762395095456034963769023860636230829948132006160696971082730219604693162703698889664344632676980/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 - 7478449626228786002726780601426643640141719255329080519457707929469554076166774763957578590675085694/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y - 871739430360971802459349323171138521595639690774090519301262569729714387547831063628505188270936183/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891

280940999832879311576410766917273871930530032824169291885738154479298229043415003311065306064117765/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^29 - 1158937310407060618047685962684184088445194865545441472018123302046982547185982501363520344137614125/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 - 65043110796511494212650311530023260405567251760953219562388477468590858786237709147584518264008682754/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 - 282591601757600224567827472193138856309486189056493175930668372013302255502327037353583512454110643913/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^26 + 661083315592717127366231722263188619211453031353622629514133938598347089566083759482960361798476354065/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^25 + 4571282236022012298109386548082556013911933680036591927507555090598697557398848818164698409804130489704/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 - 2740057533664901314608142727200680619898922964270028313595929292040505729982613705000090918211119672396/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^23 - 44135749252136043823792839102372065178665071206943658100682103986086569997103250890851082002545152414843/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 + 101309094428263622659859306211300279785733767482893869462320828440872717132166531367664843600159509632660/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 - 179955046087795397919554836089857635867787794442733488999497222126021193322902551526986081605986975907593/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^20 + 505971082418379886498852877603786107403388483508842535018810779275059173931462860253047011911920164203555/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^19 - 604349101062162188075102371055093140168840152629560288567799804992008992956411663907638325283244651574897/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^18 - 892857247777295058950772555766484621015571361512564182323082005010380043081312181388282366426693554154430/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^17 + 3114501599749617505938771082953801777336332728295563617180575091504541590456712938440189638879842348500403/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^16 - 2393054131986739763815568989051721065747752372102586853655475745567309371508018112680647031601819197175886/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^15 - 1327888168423682182736001816347074758613309334762508433917997318605743192929824280376486854014884367449859/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 + 2875798782112789800677713176837375738616713818607372200599374948436570309411786900134325700994609883965541/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^13 - 583808774591476728724989551472982852137996823710543233051494576841907936688809333838272271493273360916428/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 - 1246788973761150673976521004970465264189755044678462426071017563367823206080959321356977924876560415676536/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 + 601762537316570896261074264654419958193968072091975861375462369818961870127893021317154287925636592613137/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 + 267836065807078939158148776713426040062778442188529209455111962110306543370663187996137177176691404089549/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 - 201991956732973143703894219534991630316961247177689083539512525024691495125959747599545516694289595514644/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^8 - 28672651540323006753285109346099621107311537463267326507687184675899346778618626534754131256657157628364/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^7 + 36877363434459162404980597074360486646571353230285453850162230670560799029470997634609439673726875842891/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^6 + 699226409775670344384320736548912948302859938382143107526529136470863458970607756838982208208357594919/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^5 - 3860507646248752819775904392914895343744084405759757416408161215390125610727327182428216134276810037149/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 + 220834346766140795245061352296377527550850693957539558562261960304884736434607591013442587217971917573/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^3 + 197509268473412697418655349070535752899371955282678064667930210556197073293303692527948626883384831960/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 - 26767181983365138464221828063755854993891209060437895180821893552284500700381081400605587524997657812/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y - 5032578966442124580898010656187842327127090853687367126088106962227782138005999977049025034379984256/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891

280940999832879311576410766917273871930530032824169291885738154479298229043415003311065306064117765/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^29 - 1158937310407060618047685962684184088445194865545441472018123302046982547185982501363520344137614125/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 - 65043110796511494212650311530023260405567251760953219562388477468590858786237709147584518264008682754/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 - 282591601757600224567827472193138856309486189056493175930668372013302255502327037353583512454110643913/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^26 + 661083315592717127366231722263188619211453031353622629514133938598347089566083759482960361798476354065/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^25 + 4571282236022012298109386548082556013911933680036591927507555090598697557398848818164698409804130489704/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 - 2740057533664901314608142727200680619898922964270028313595929292040505729982613705000090918211119672396/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^23 - 44135749252136043823792839102372065178665071206943658100682103986086569997103250890851082002545152414843/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 + 101309094428263622659859306211300279785733767482893869462320828440872717132166531367664843600159509632660/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 - 179955046087795397919554836089857635867787794442733488999497222126021193322902551526986081605986975907593/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^20 + 505971082418379886498852877603786107403388483508842535018810779275059173931462860253047011911920164203555/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^19 - 604349101062162188075102371055093140168840152629560288567799804992008992956411663907638325283244651574897/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^18 - 892857247777295058950772555766484621015571361512564182323082005010380043081312181388282366426693554154430/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^17 + 3114501599749617505938771082953801777336332728295563617180575091504541590456712938440189638879842348500403/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^16 - 2393054131986739763815568989051721065747752372102586853655475745567309371508018112680647031601819197175886/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^15 - 1327888168423682182736001816347074758613309334762508433917997318605743192929824280376486854014884367449859/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 + 2875798782112789800677713176837375738616713818607372200599374948436570309411786900134325700994609883965541/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^13 - 583808774591476728724989551472982852137996823710543233051494576841907936688809333838272271493273360916428/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 - 1246788973761150673976521004970465264189755044678462426071017563367823206080959321356977924876560415676536/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 + 601762537316570896261074264654419958193968072091975861375462369818961870127893021317154287925636592613137/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 + 267836065807078939158148776713426040062778442188529209455111962110306543370663187996137177176691404089549/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 - 201991956732973143703894219534991630316961247177689083539512525024691495125959747599545516694289595514644/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^8 - 28672651540323006753285109346099621107311537463267326507687184675899346778618626534754131256657157628364/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^7 + 36877363434459162404980597074360486646571353230285453850162230670560799029470997634609439673726875842891/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^6 + 699226409775670344384320736548912948302859938382143107526529136470863458970607756838982208208357594919/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^5 - 3860507646248752819775904392914895343744084405759757416408161215390125610727327182428216134276810037149/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 + 220834346766140795245061352296377527550850693957539558562261960304884736434607591013442587217971917573/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^3 + 197509268473412697418655349070535752899371955282678064667930210556197073293303692527948626883384831960/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 - 26767181983365138464221828063755854993891209060437895180821893552284500700381081400605587524997657812/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y - 5032578966442124580898010656187842327127090853687367126088106962227782138005999977049025034379984256/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891

-133904700962530272849381410641324286659883120596873450062897491622325688039764931737802526484012881/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^29 + 558951367951219903431089228112859432980294445303269888265879565577754858379942946645043007024593048/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 + 30981061356931985087765817807287049032060941909635128330096772884219975417292275341274177572820654449/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 + 133147150756204841591888323212609069179091260699413361680338487124653068235535000114606588843792171454/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^26 - 323264223332574392007945415323434872703461094869369227115993242807105841327879776705652355987628798100/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^25 - 2171029615384712608066296913920099495501406401092320722916034113717933512080150550602851666316904012780/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 + 1423958643035628915730977826724629266330383502582857768361942419843462579601603455048373881259856829690/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^23 + 21087458139717184063530278238007695478378283723154989511549315384007570144396024987014701913589413548291/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 - 49314949846812153588605295654023617406215679248303374928653555670400024842769666980696806624527116397410/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 + 87097230223449172089808115570874760639679814496227708601095092725546159374961423193184486980045240319595/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^20 - 243568629010289929657102191077182947357379385086462919664422951958700289758354465804524675328397134107149/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^19 + 296581920254546872646190622025680508858922214110636386604388510657228197838343691813029800991495290907428/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^18 + 421682746620614613495444883272955318939696055661292535436685235361496454112002424537313308370672863819030/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^17 - 1513951169418192137926367744670147799383721842427611124377515926867238531846637962862932195612798735907717/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^16 + 1187778925046311350021138560978361010423951861126183187597476612953778241851849937991391092363015778315642/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^15 + 635340159364624431119008588937070669519727954042425352960328775684092497827400037631913751381362232027252/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 - 1425666022731558670392886617640692387549524063819105959985373437429852733656710498359919695070207859491723/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^13 + 303634785970024342944970179592044448554101973027371800344887122798083742841623570331468994616790073906709/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 + 621588963426411960395596868096922683565392262927185271914657640622284056865809687056004975484846102254779/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 - 306878936792857007743917561805006671916508329853454344369061688904622285810749366376885253458115942522306/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 - 135141137401455369585279493638176711193423687138868363106812633252580516063860877544960073740250755532006/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 + 103334441578586658984946978988518429031321233016390730321326526894714933224205855738468721176317338712768/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^8 + 14904217466456733989510297735062399573841632477008665735539797169670492398004852074842769412847239929684/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^7 - 18887666960890622754000013452759534488424546704598076551809507031529951393653987648093204668512143951826/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^6 - 477273137690886101957474681294035577500879381821802443936092154458751948628235913136038894852072468173/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^5 + 1969045157586189291833147392811370167665147798062607550902220838717887402522548080738039093981020384605/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 - 91136813149609133496321012524655712781788957236081161925240176790018754129395431648069561684007897154/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^3 - 97534150215346537799167022398191927601461368568959239123194967751459663999287233156076078497386272684/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 + 12946139830143214488052758678688725269927553802576398601457670652816906404582884692733578847758183480/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y + 2879588802770944550092916436555132582923087885452779261819130482615557093164928217236943061961246003/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891

190563753606520823591683882732633963114440742976316837178437469795530109210669733355210125261830667/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^29 - 781586917862076771637257302576504139004645639624512765994299281098708920312442078369396821208631473/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 - 44136200567133469532447576899727722656694744136480588154859330312672581018132741660857357320574495697/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 - 192737367805329048893884775813113947564068847355314202315407057133124232286138563529739739105408903341/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^26 + 443502836046533033965403972001116262951102403245899785842591135756662418485661252675410533103677258918/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^25 + 3109729781399424201942651503536156205090357510405031993179125425710442720940748761003475201986709825169/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 - 1781827928948271229530610380288800981079448198327979285821442183866562593735369723353015182134968623241/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^23 - 29956576844758302842256646661585028152436456585111679610511916879540246331586986930277686562404649046087/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 + 67998734282382064485054661595398036749823261679329157174935951374277845861361317107726494273727427006154/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 - 120665773399618797009237801087372208458816992633778251458020059123181968852150197922130968726716700592327/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^20 + 340816060335649972442178477547614331761403497812712195075781788105718172165919795248091421468736465157773/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^19 - 402772931450621601967423320948438390275405924487007640615664225914475591216536193875331571436536414258523/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^18 - 612600350125786100847998212735352940534193659415467898338877737993189190829698125173647349991635144431618/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^17 + 2095058021145427341324988266174952373024428750005691350997427389052366731362644055202852323508546264738602/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^16 - 1577492261217833577256712684236939004579319746478900028951463256825022801743681292573452479351493161923640/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^15 - 923989738500705384018711041988495905327800116359619730871548951676697475358725979088778031240336805334854/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 + 1917022797198534093259922337495737697468537168913720753358606471198110689887489155520992621638371087801536/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^13 - 354075008566027335288619721385756032192873752958546677646650720683080587090705091931679091443550408128589/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 - 843428271094714919285524393043406733960695378184009576689853912824602964243636400248372333547286138495122/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 + 385446296830323034179415959557173385740755050818173388238793568663314219706730122811879560137189514435335/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 + 186743247992045954286311428771372654079304922462742228685992273775913048631797434049436370129565118667369/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 - 130621715255933947480282991533290138713379476911571361342357170879860633211755717231813265383506101629449/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^8 - 21526576333314289743365960544386266957722570662103647359890304157044799975061553776824437631855641099554/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^7 + 23857831046346200760509063854665767262821196523254239608458221957273426712604280174929431611713443446296/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^6 + 861066071806210171844474587983317646007994795480464602534972388449433768849111062706427456340664455884/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^5 - 2472933845405641784676115361645705220537299140918367208567212077896934084828811143837715077668324150009/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 + 110326363426568425946681380910827097996748472873301794242310170139643868050587736854744598271108389081/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^3 + 123686005381872422315628473454353427164452756699657616718137891619908302253584139377278750553621698277/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 - 16475498270654918067170095758079527244718195990151155170464172090035091160598298017001586256005435678/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y - 3053604170743806277580766513717904288924446133041730795817125035634911893063751310675329837705584330/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891


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

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

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

# f Combinatorial flattening
{-4, 1, -3, 1, 6, 0, 4, 0}

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

# 1 Loop Invariant
-21541084060624810843250768974562720830848773730490149613503910490685075432309021383107818957648653860/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^29 + 88712890960177631982517224031648972080999158457606066309221044525129838500541862567632776594695997005/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^28 + 4987125898941346175618043604369854335108479595913748147407566666405218388306265479188432863223226271478/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^27 + 21704594727463612928633402472961141304451868854866120722043268160498474685770445176953063478573513990423/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^26 - 50388307085569592436873998739452509940305348804588162573790103451220865467575837197352988828087046475703/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^25 - 350176806073881988433388936802239114035505260812934560792879521425484286607175687382426659068982517708073/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^24 + 206272281428329522055181836246149657864885333172701066159246048949456476625692726305519662345217958624682/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^23 + 3374965381329707047576184856025191914405073072037155596513780782291155145179574024832806489083939485394976/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^22 - 7739873435790383240596399824618064584314416116693425230908672128377024865759475965729882669184567556250306/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^21 + 13844463856760810374414965082503399135673267615724812129590900954642839927488353817709751498501618316303538/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^20 - 38921535194156643420370480488504321825696937279682116280409744640202857134368694226408191954105690122755961/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^19 + 46488018413988651526665669189793677205425102222010954522346538627476219245333817791913845892066327369756593/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^18 + 67598612743573122639871143412055649349235182897062292562245901648925792631920851917492139414576776890779549/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^17 - 236963881318805083998236687081393188807305387890285202466286185907584362792753442242540333300769061384768885/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^16 + 183758273044797588864425711830510997371852765023731698016154427060045344805249880711745074309661997215548810/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^15 + 96464483285303275432338235151087074878646975573814073635914914457489353120290478143490443655867781803618894/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^14 - 214553204311676435337859320443739670874416416873851881833010404241406712754283162222830672339220268247134061/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^13 + 45213209621192069701481215968134838506079490473772517007088115673989219908931499678374897219494080394023830/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^12 + 90879843401688434225329257764874607020223725439474617285743985828104868181665128019412359283680464903131051/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^11 - 44282361974096033883448777787585718532410580582169105485007736477663471822409865549265535131753980426506524/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^10 - 19076035678227961091798774524589172512888465007236803144371791451488479056192890043925980794007437744139115/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^9 + 14497448433706142072934631621004432274007088799696652530899518184518572240669062470247117547109408438514555/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^8 + 1982888257436785516435670078874990487186231390657693586090728966821988925540144915861473851851206460580423/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^7 - 2586416389575606622940652552160266006873673865207207267886427115956624431336067483069542417012367536123625/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^6 - 40267025259820254886656102609322632717795036046220414365226947613807331708920268955364569233500921505050/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^5 + 261878165498435666829590864896159425316295114363722261900183319831570955876426638300902977026211795694030/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^4 - 16361678820896315556876016759471214175908602174635288001720426570373336051142249314191247465093774010897/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^3 - 12766579333749296587431933723726477134992631335901843052531884484149516472809253815521067913109540247797/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y^2 + 1878605365886241596771242613703252999896833598888208266326980215932706246811694705183171176941151605677/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891*y + 323093513806523708579015934106926231217004089768323635511016562814951291258846845659243606836369952792/462941662574139373879746689411249609374697047502124701494505255245507472240622232597810255708775891

# 2 Loop Invariant
11694469892090843019502859434135339816499374097595645596768609551715586995476701671018185679835319499694009824714657591208481376421865203002852851632189294302287633576576902986693386559783427202301389/74153767252085716984373591340379981859566041313450990414236075914476679647092237779855244532027291217230477465788628699668159048319484873494472427489996287795274257610006090147100462349361119783843784*y^29 - 96322707050977721404541728848526173187557550354934532833343715753943833745988327480379085509522239263055188391366857928435194885477663631900145126936164490426206447122148448746390624826600552295977931/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^28 - 1805007483282325416870848333008128331698444222611494610772088960201269832066321783073729113316102371672212034606371872008845673436306404733659123124527157816671680298551727632639382869008402710828320573/49435844834723811322915727560253321239710694208967326942824050609651119764728158519903496354684860811486984977192419133112106032212989915662981618326664191863516171740004060098066974899574079855895856*y^27 - 1472888626242138569161634309782983373360954876353293065834237866299235545542592664030252121845757302814278998778460768885938265253625734056009731036507756905367113661775705186900776152767234701612199238/9269220906510714623046698917547497732445755164181373801779509489309584955886529722481905566503411402153809683223578587458519881039935609186809053436249535974409282201250761268387557793670139972980473*y^26 + 27365268789382363657844584940425103039125259703956426328091230970662430716912351105031400390422215212378917920407613928613657376617505427689606566785894068236878887478931426959980961598740249428164877145/74153767252085716984373591340379981859566041313450990414236075914476679647092237779855244532027291217230477465788628699668159048319484873494472427489996287795274257610006090147100462349361119783843784*y^25 + 63385398945374144395306819300379581406769778394398775778926775488761372696215147131440557144599120092117795026587461022736244201815922392118311777370824910860260584329609197090805326046333716357893461591/24717922417361905661457863780126660619855347104483663471412025304825559882364079259951748177342430405743492488596209566556053016106494957831490809163332095931758085870002030049033487449787039927947928*y^24 - 74707282217173635126125324261606411310391811394374345547112521385437672263123214363493717368772189831060978287597596443612534842609398046142892548025349754938962927329669010481630883274317326146162479871/49435844834723811322915727560253321239710694208967326942824050609651119764728158519903496354684860811486984977192419133112106032212989915662981618326664191863516171740004060098066974899574079855895856*y^23 - 1221990971957055216432504965004466258957856945748146494557589130861387554210128106630483716071608911325230990668406598885840321410653054018459199977926033700444389740091367518126439491636154313144731563295/49435844834723811322915727560253321239710694208967326942824050609651119764728158519903496354684860811486984977192419133112106032212989915662981618326664191863516171740004060098066974899574079855895856*y^22 + 4201956464007460049907314561001681461452747667777084904608257183141084382638036492808290446254543654184282996777853542573861269470614836127007692320542995260889254756947482578516325358323980479509626990605/74153767252085716984373591340379981859566041313450990414236075914476679647092237779855244532027291217230477465788628699668159048319484873494472427489996287795274257610006090147100462349361119783843784*y^21 - 15018195246000299443010408935125066941859692020779064577379850522403871769450838881774516328790365038230625681915254445891947275155630382936412553863533559518804371310533196109555703528815056489273168538365/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^20 + 2639758170994116347280613535088355599333261690615643048420718091515498672593144600859212463619891451352067624236132523002015919952693660505916751404901511088323664011978914087896322289890142181740037245345/9269220906510714623046698917547497732445755164181373801779509489309584955886529722481905566503411402153809683223578587458519881039935609186809053436249535974409282201250761268387557793670139972980473*y^19 - 8405783408587057872862123100245598801071114530516448169633202501266125043237127757496138571829728219938717898162915194032616836391264107278488871068096592079721617838450228567621200917249386722116062988959/24717922417361905661457863780126660619855347104483663471412025304825559882364079259951748177342430405743492488596209566556053016106494957831490809163332095931758085870002030049033487449787039927947928*y^18 - 36764745772499038454491002339134292942778926355741214448598300866863217686197227463971859465795224510763479057262432292995832707214074313011544897117379338092798153965472285466706759960320393164068851093447/74153767252085716984373591340379981859566041313450990414236075914476679647092237779855244532027291217230477465788628699668159048319484873494472427489996287795274257610006090147100462349361119783843784*y^17 + 257406748728292958143029528117943514350998839771333019388361901811038144324206910744693406725664885953819514142622045522691043816506743819175517365474871780316926587704139511488514555739249289169595733433237/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^16 - 12448452401621291239827608276457810534359837836279096616245365203424531197364484804796740753450348897815433398409490377788958605399395051929425855505898182629357300581495576427481517972074590349320009817025/9269220906510714623046698917547497732445755164181373801779509489309584955886529722481905566503411402153809683223578587458519881039935609186809053436249535974409282201250761268387557793670139972980473*y^15 - 35174328260859941922030983243903670176922986785178467059340475845792937952276350743824230401367320316592402251992981653852729850752944117210499948773436898246822710657099263503597428259689603125902437243369/49435844834723811322915727560253321239710694208967326942824050609651119764728158519903496354684860811486984977192419133112106032212989915662981618326664191863516171740004060098066974899574079855895856*y^14 + 233220039642727158300042148378737069745871377875974165066395697221334152954694726193877682989772769472528263248717351564797794964517239259756092108812033806822552583055954928586284333049855905235347918241751/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^13 - 8070749877608127703874135881860683244096506358258332207055575308827053198159558180526110040422272098768812642945149382846319206479324612628986776491020362594013582007427889581608606084698172970718805810287/24717922417361905661457863780126660619855347104483663471412025304825559882364079259951748177342430405743492488596209566556053016106494957831490809163332095931758085870002030049033487449787039927947928*y^12 - 24803163612657360126401101309892739221337013654955822398549308730352204575798029391714778793822487115759277914078862296642085973031676004999742609651642095999767646784757274762451792744827953714873925606453/37076883626042858492186795670189990929783020656725495207118037957238339823546118889927622266013645608615238732894314349834079524159742436747236213744998143897637128805003045073550231174680559891921892*y^11 + 47775538594616244011406348494455817436295446306353119941436829723902015182700562396707782830937568350966184977322931356120264660075534658911790800537678359936537446640948808690237669503155015021413152943225/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^10 + 3523041132996296728282360458909122609409258610385141001390588354723582690194819319379485657180380570807552290804451930285510127914854187848970924393753632456489093310793972215976742841869799418601432750261/24717922417361905661457863780126660619855347104483663471412025304825559882364079259951748177342430405743492488596209566556053016106494957831490809163332095931758085870002030049033487449787039927947928*y^9 - 15705446972321768359180002143318401920244090567257879145498205146595574448823500868846272610615097929709665212526910188839492855054633424185847938283556126946546982385467252378759242281406353155856340906505/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^8 - 2324621048970716894935906641996099150102983765836851623391576179240508062197957359860174533093732296440384717450042802831890757041220529018049294611171828672777454331689999879340930678728122116847622884523/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^7 + 944612115313170225717260142883556876875451273402380023617669747997014425112979019847720552361502144844671095703516759669762904035216522164974493586600551950083463315178350916409164816129619841008367111573/49435844834723811322915727560253321239710694208967326942824050609651119764728158519903496354684860811486984977192419133112106032212989915662981618326664191863516171740004060098066974899574079855895856*y^6 + 77823358386341706107623176362369094699822355223539771994240783236673223021524445267739716167471533269803194570697432451111682880185714886624873467555751356721017457693189783986865636158346826157674813199/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^5 - 294091200855899615168957123079811516604465384612868753178110144416153732186720592914261740618489497197482408396528708027393468382076588319933229840435631722703696500333338249652525580498922747801165620125/148307534504171433968747182680759963719132082626901980828472151828953359294184475559710489064054582434460954931577257399336318096638969746988944854979992575590548515220012180294200924698722239567687568*y^4 + 909909840089507496632329941078620571781163415473286298460985028303502504157204036852092542761511410893934690884487746990295314790624967328483208397628777281545430465555174926306144658399417823048452033/9269220906510714623046698917547497732445755164181373801779509489309584955886529722481905566503411402153809683223578587458519881039935609186809053436249535974409282201250761268387557793670139972980473*y^3 + 3753958137914416441254717893889481246673084432922271308649094763501822848949298968234274653509371611299135394713109530924020429641523306403289031745740112406698710573368750489110471090886277039813440541/37076883626042858492186795670189990929783020656725495207118037957238339823546118889927622266013645608615238732894314349834079524159742436747236213744998143897637128805003045073550231174680559891921892*y^2 - 119188552880323725377436614842462672124128204284505215226939669551684546929925794790420777672369363533767875771945645812437072676021699800314085505568515919136441518138255961361599142986850536867602758/9269220906510714623046698917547497732445755164181373801779509489309584955886529722481905566503411402153809683223578587458519881039935609186809053436249535974409282201250761268387557793670139972980473*y - 16455950506502822718611133417877200093808851487609861212200265844762250568078623479247828588395539467952872647070549441315591654413703299793530571147808093874676311509991482128900199382192362070084107/12358961208680952830728931890063330309927673552241831735706012652412779941182039629975874088671215202871746244298104783278026508053247478915745404581666047965879042935001015024516743724893519963973964

# 3 Loop Invariant
275046711467779932064597904139618423467506421086168603433981469777510024298612933917790742141615338651957622869152620906125959748953235769653710883363852525232156169610614054222942203414101200563172062242683770338093565925882686123296788707474155195/4038683460317336713787144010960983602694069890034544683164471532815163939001972377881839325784265565589940629760563549471695753559769118732178525223416983262807712807335791863354252170727040059891221909126458662567114878538299491080374320643903703344*y^29 - 4479894392588677746077657600915493786135531009026271592066180161224967438562685915305236873147247392039497581515996090393296345928091587347825709691067679159471706947729132984933637276958833040040146028368020389755744347948443468657389671756463107149/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^28 - 127461894086845583648852828482024233066527887592298554176745093246619524154541796490184969506086594280494656760342540518319919584397612288542282466556437110788355199785266923939609900999393006415517710135990840444158426882245390484606322589764996039007/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^27 - 560171074994884132302099024397883371804124463838037132088171161095388440406005824202189612325315999418636848547441558910989885743571769091730339056425105903392883602787609624602323011939459081483768912524477748769343449492401687350818240950187236688297/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^26 + 2522541292063530533525212169794101437228396732870376572295814098046620506197346636126970010369855914261176882718687277290769908816533048126405553576120441263299212657564757305142242874192145794883532653981791442971067095179019682423111481418443717953193/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^25 + 9003017676601055180308646463005429747239157388679135678224544285805038429868844103718509065679851182575315619510708564746828187893423479074027498164778319030329991842045733970739057858680575608985260622556809488025408660664012479281143151119094189089547/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^24 - 9711021883238333048322651990954503074900115410009143150084750915056865223552895524404050287243476782601186829065302452528651142000823132687789456581668429850589479017737995120041051916263277626475846540165267706040294855607848122789511604569681822622765/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^23 - 86447839257494232351440960302854935752276547342745996683701756294622126761368383112779476753830872941138921959479997382793775471647188855991622553256653904828413703157258505750136817701764052087570222013347975098957874294995357842481921250725341619962163/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^22 + 12104323771600483821349515827690358337523473197959081385079148920504017534116634173129114338610296625786048099061213370283583527409341264063219924434490659761334805432245025231331908688246029303632011749071461434666209437489448838986317297702559116738753/504835432539667089223393001370122950336758736254318085395558941601895492375246547235229915723033195698742578720070443683961969194971139841522315652927122907850964100916973982919281521340880007486402738640807332820889359817287436385046790080487962918*y^21 - 344198967306803974693755324938326419896957615839122482234695640230623253675157475089628294486296877350462864399985099121886325381301301787052538458634251372938779279128496853854594982666787990004849963768384112468461354804348133141692693424628910923298775/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^20 + 1954421757466864053273704841631683943864642581471387134399224372415639982504592285413606641362875825593688368932249129120453278960680662097750691904459126725780807499282647050424660910970939351390644785866547860920553708911443180361974371039628515275347181/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^19 - 142611668191484976608355887293578138951554335733003223315270305477470314470126733576377703341860486669844400278282274251472649145383814106637688815949579205207337445926266613119086324742190361214991192211604504684430572926804035889386424058044460428526379/1009670865079334178446786002740245900673517472508636170791117883203790984750493094470459831446066391397485157440140887367923938389942279683044631305854245815701928201833947965838563042681760014972805477281614665641778719634574872770093580160975925836*y^18 - 1782009669281770999694838043346610578783829626636722708187135926827964936461834197348281666541788339156858166849503616504266385618274863539204063240180536485665150429470945803260812593051971930191197863307099997352185996279921892456152623311438219286690361/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^17 + 11942700546596558702596165448938652534372161491908336000438278787237133182244933748928432352078880721667415695710082254293251835402306206625059855308460920303035361218618284350874432732629801344146419146182471700571031445809900349970838976828709689827010183/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^16 - 8808535134197139929079597831372803116249118501106701391583049433353027305087539987019655268872037786513798785721196325885003978934562553792166206809620930577905560560833968189513382295384755360244595980958734487512713511840929970225899829476441623142051155/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^15 - 5393035944539432804249000458617497829538173484000795663111140526173104125237345710441172436713525511273010300942130846970382539760898788651165088551574091482842212105984023412819566438687856454949932982264079374783456874834850809610665894041239494393191357/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^14 + 10731106777985382311859630765935052934700143643418890382996299306022907483494673274673437953269688881029004052874378853677136430598091668231701171985619960036617850065197403548550142524397477669890993886154196580581840812913253876453917896056109893293386023/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^13 - 1741210394029360608724865462350786086630557115946528643299556872919283177416401198892196835136706921569261110835337272005216409628053356913123711225129749432177328136646730468440449353787280692752393449428927283198116233887711917340581843015365490184387025/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^12 - 4814185331173172868581438295499412264544168439109731387224292302209005692533527903194660408972180458226778892049199345764278334857735800181287711660139324280066294043338965458469566874022382083267556968761715341372034807890889832924399282698995747097174069/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^11 + 2045666482747509887590894757573898026655807510386371895603950431621985393949134465199527898537221128681856805071776454296157288545564062811048295155450339657842549268825257369730014348371069106089588326082993149420724797493422740685876627319980810673885719/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^10 + 280806783225432833974643478702536842315044493173076301029298704157747621343192461326634081761243549620588778967735242436659986929810703327009911072569276184136479744201724403274396962657498728368524972062427712378671797836374808558292357026499131990966821/4038683460317336713787144010960983602694069890034544683164471532815163939001972377881839325784265565589940629760563549471695753559769118732178525223416983262807712807335791863354252170727040059891221909126458662567114878538299491080374320643903703344*y^9 - 179175440821818442321510023646226217924145836230552001158055931432879631965041286799477048445375996819084181403872041066055904597070406867101928787329008042189740230414056159318121830523551140762383392585934349551326163691973790867161064281237724547195403/4038683460317336713787144010960983602694069890034544683164471532815163939001972377881839325784265565589940629760563549471695753559769118732178525223416983262807712807335791863354252170727040059891221909126458662567114878538299491080374320643903703344*y^8 - 144065399675603982312871408334423832459304709796071303007862748441672424413251037581525753599549252004116363320955621657823435608835319065095282229588748374820455715799316585914718955010229770381219977566599018261925145861083847216346455509035028400708569/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^7 + 136489423174665113524409475416133119766711297360765108901098907691062442832768160295723928077503573808612960554559019881301479425590664022947962788125203365978585065170683023305180656544071716563334809193531460130459811091679793793557284341919221767445249/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^6 + 3802541269159184671626519922570632493483328042948443966700740574343679724275638571291092617830113295615487784300905880867620164939722609245460944901713902940255554654268363793095858554946043540082018418189339159296476625250701054157181062685855399486745/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^5 - 14671858061073219505235399816445112524858756382483987305764284634761043054421032371824381474844833769134822043091951637264199938827912977692293698285949450672240320284773351388628381132194522715743728041411725777176267796910391743947468119200199339296881/16154733841269346855148576043843934410776279560138178732657886131260655756007889511527357303137062262359762519042254197886783014239076474928714100893667933051230851229343167453417008682908160239564887636505834650268459514153197964321497282575614813376*y^4 + 269653049626672399934029310281963576315810652214982683099605538453562273889328954495394266129797168448339701899466364744929279120258593543876104761074389954762440907386866436033893298445221366930700894457331078767001404731759666217266591001084721939819/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y^3 + 95406062164101381494789231302693728562196587789714221275886461550000523071888203340100021820671525344651821942287544847212204411234032795530943993279509991649280715426470572234262935439701600828149910941656291411996924069630684686438974066065928354147/2019341730158668356893572005480491801347034945017272341582235766407581969500986188940919662892132782794970314880281774735847876779884559366089262611708491631403856403667895931677126085363520029945610954563229331283557439269149745540187160321951851672*y^2 - 45813738006456563291657196865021991405136338045991644754309901215191669555580534589348493853244485840114935164710874137109668665345561880844391181837181390488181657871474904929947625180425934498548296536215976088511040731887262091099986247820362140697/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688*y - 10488349249075121160297019531275510251923234843074558426250423009471663832781113472856123202626467253647211366526011218931254397412896288400298933973781740182337635325905571903816370084745222248454483376373746904905226754616375683167294294615236064151/8077366920634673427574288021921967205388139780069089366328943065630327878003944755763678651568531131179881259521127098943391507119538237464357050446833966525615425614671583726708504341454080119782443818252917325134229757076598982160748641287807406688

# 4 Loop Invariant
-16203451553593265106337175694100729353099311953920684886587473125138906719117301648332789110716227508973213829820740574209097214005238263679979612782820474740315709870863944700489981763603795531925558526687371581386941105121948719978093823352729216804558029437297397278697894741326166196622133878935969824487200478114184855471373044354456714778168891041/8625524338019101934291785267693834052978081046110139584466956705459467775429173450303594654112274528413336965831335872202973388748992779895061985124426856587304915874880342926595357468548561527118807793276856985277155976030441280477709722301587603192970988464769875083765401954096336016274900938593415581569813621041946878469581518898427591919226158080*y^29 + 601621611960156733781260074036014817610345935133425477063599077028710880737374515021871396249445120869529649504452588563378576803686843001432614077937644403722913460503790045652859467074013954056472331886998205545887313495353708313280690509747576563182208206846938817588954757445165054323825945712557279080770867063185749004741674519636797889169543771617/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^28 + 8439236723605853898113560185330997052750166176552317401272634463742597296600376981510464616526129599213591631252898291529060230007566921944813291806005184554847383780633789792572087225469997486442388300769356639675184766082765869987680394630788541074092970294598450623038182642948283129490924530755585103958329128619778641949701256380924242277424655680401/19407429760542979352156516852311126619200682353747814065050652587283802494715640263183087971752617688930008173120505712456690124685233754763889466529960427321436060718480771584839554304234263436017317534872928216873600946068492881074846875178572107184184724045732218938472154396716756036618527111835185058532080647344380476556558417521462081818258855680*y^27 + 146701329712188352066974231236573613585224111714511722436602608454653882037828500065448989286806140400780713228944241098314842104627685706980722370225416783008872327809032914357096247030624493883178039659758492331796841608649258455971975911786318260924779021747709237170705698533339771463024439182118887057696503381024373722828203711176592541107434513369909/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^26 - 1780830009845541349105973719646320825473143053053761810898757336051564058499850300273915521677491069990847063055154381050770472269718163791974829805809920995789279575265096617272848416090770065816672548219062458243824800193601074050387137629818443246179788577110346950056603750540487760850830731591855438682530065856751360622922830106810905821644895518569/404321453344645403169927434423148471233347549036412793021888595568412551973242505482980999411512868519375170273343869009514377597609036557581030552707508902529917931635016074684157381338213821583694115309852671184866686376426935022392643232886918899670515084286087894551503216598265750762885981496566355386085013486341259928261633698363793371213726160*y^25 - 295898435513980257267083318138498002021554671584325687206111498025985069277133649621943856784188787937151567305929247080150018101002369809595432297861685193939060490326334855415696514767855377640888412478283065519699680156206028002579163188165487688324429678193963488504594803039856872088756765435482387424601005923112285256921326913424314304853995818992063/9703714880271489676078258426155563309600341176873907032525326293641901247357820131591543985876308844465004086560252856228345062342616877381944733264980213660718030359240385792419777152117131718008658767436464108436800473034246440537423437589286053592092362022866109469236077198358378018309263555917592529266040323672190238278279208760731040909129427840*y^24 + 1410474753023263613643222134298721284518223654700036862373657572995420266815534729808985643301439789735607814906809969578081413009485597374974461906938831461677120596425819092905096662244489497590366407404649385347812792604016214063840271575465014271545838222033866834275670059923392030527970832674916064752420314594066361114137726845261044427729076821562549/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^23 + 22821321951012575964552863876209643216800696824583716355824774487703047689330815815474331275125989791154693924706504393240320781950386271841798629004055332108283969018020341534510010709916177093683341116030282870153880171270419041063739599146341356936342015377338490193527835422927877646974140398551533817294628391904127347874420935129917727862251190298536879/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^22 - 52545128856206501926599706393651795999512344016774790143844632476538110317832286674108156921513789758347659243523444977572122286254488124649156408599479986042400387573662635068390559640639600676220184041174128941568242002580046003809202194248068761557691475698749002872151855228314068142072690205312458461241448846888660492726856225258287939283179485593428723/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^21 + 31422265511031575713561719749612381306064472503581161397629501556218169789758600647559052259938781302602517500328008684682869065340432567727391630178777715478827707212785395882010714897237193854350017372752808945567726410076779752840774544239119321873401131527316386821256293718015673129222946327084020505205345275204671070699964773004553551777791620678737127/25876573014057305802875355803081502158934243138330418753400870116378403326287520350910783962336823585240010897494007616608920166246978339685185955373280569761914747624641028779786072405645684581356423379830570955831467928091323841433129166904762809578912965394309625251296205862289008048824702815780246744709440863125840635408744556695282775757678474240*y^20 - 17641919980538343074342016281581402797014124475800742576881358697168417058485482146691931928648422153350710215486789061337746383351526944002447372015276278108068356222468985545851880523376299429316304825913767766834642400089168658740855072650797870943669175777142616994670904928815408522005679277428335709967111998628661836329375009835311444714217355880137133/5175314602811461160575071160616300431786848627666083750680174023275680665257504070182156792467364717048002179498801523321784033249395667937037191074656113952382949524928205755957214481129136916271284675966114191166293585618264768286625833380952561915782593078861925050259241172457801609764940563156049348941888172625168127081748911339056555151535694848*y^19 + 26459179651517079208744824420137265964660762534595278805903739126643465169654702291998283394775969196876063423693059097988968889035194331037863663217579984618205753832991678293218166619664406743298560134161547213975078655140158732854162514632826028850645279896568142463653322178140142729891743776884196967323646280815353564088355625624378823824990942808719687/6469143253514326450718838950770375539733560784582604688350217529094600831571880087727695990584205896310002724373501904152230041561744584921296488843320142440478686906160257194946518101411421145339105844957642738957866982022830960358282291726190702394728241348577406312824051465572252012206175703945061686177360215781460158852186139173820693939419618560*y^18 + 30201743733183745460078641852940058744656911650897702007064017663393350154945467357449494372550543045239694629132008522098297466740226855076832569190614104281833653558173551140348382096190416858551653066218382108138342775412009384384059508743662465744483210644489550872584620524288051082115440229214951060129158542124987982727075350269416487332316731374007035/5175314602811461160575071160616300431786848627666083750680174023275680665257504070182156792467364717048002179498801523321784033249395667937037191074656113952382949524928205755957214481129136916271284675966114191166293585618264768286625833380952561915782593078861925050259241172457801609764940563156049348941888172625168127081748911339056555151535694848*y^17 - 89122433406672883530703368064769188564576926026745444039181487731584708247530117677669780313342352785491514684370464378926256243331057037908432075457763174211323730355919822074437821040588542152549007187927903251781868402272754327582996361438071672728518255234983030338451091902413493746074373501921460556984609451039154670549427147871088691356851260780223167/4312762169009550967145892633846917026489040523055069792233478352729733887714586725151797327056137264206668482915667936101486694374496389947530992562213428293652457937440171463297678734274280763559403896638428492638577988015220640238854861150793801596485494232384937541882700977048168008137450469296707790784906810520973439234790759449213795959613079040*y^16 + 209610897380418785534117880759271720294439715499412568608058676219935588572742202475674054921789696555933461314432988944636953834659937141613189302960852032552061972168528687909831103619823864954680792039137453956013457147505748639708778650672563625009253127003286574232017710448731758295661791482883482957176990933115551484710578889055114813581861418960099603/12938286507028652901437677901540751079467121569165209376700435058189201663143760175455391981168411792620005448747003808304460083123489169842592977686640284880957373812320514389893036202822842290678211689915285477915733964045661920716564583452381404789456482697154812625648102931144504024412351407890123372354720431562920317704372278347641387878839237120*y^15 + 631096754018692204218723455650532291800659551559825603801693500236153942702670050680863739058971247322056544192612093410220395000582438275659462804885386581392056899968024830665217111940873622390126885597990797770735495146037350031309970112545387878225806540699277453984210176497537605292348549383412024827961425776541480372577920500377711987917831868728193699/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^14 - 16025697521550310664183362549823514704726894257205798154359804926327975038962733494060479881508161825243338348913697670398050248376440178568909000682030433576443187583070856430487449554308816777782046923284186405165999971873269419581560511829144150045234212227689059659866916977137615344409935723259555870822923545684762938832700275060112200149347393641303197/862552433801910193429178526769383405297808104611013958446695670545946777542917345030359465411227452841333696583133587220297338874899277989506198512442685658730491587488034292659535746854856152711880779327685698527715597603044128047770972230158760319297098846476987508376540195409633601627490093859341558156981362104194687846958151889842759191922615808*y^13 + 7009259803493280801339861564167471796602437300970841518093928406782198600089007488988828542118938521082673940752538313817275327218002401696421977392678624287282473258332292106285480542372581384722850548391576381803566210148661651766232458640527048852444637333831918658557168160041579657975645110761468191238693961337833348048420415795707914942569065997381367/1725104867603820386858357053538766810595616209222027916893391341091893555085834690060718930822454905682667393166267174440594677749798555979012397024885371317460983174976068585319071493709712305423761558655371397055431195206088256095541944460317520638594197692953975016753080390819267203254980187718683116313962724208389375693916303779685518383845231616*y^12 + 6269836035358196835705597131348982024570862549351776536976119418051175186197038470920254914248888186716541617399768984452989989856875070278670869255347224572735720283722003935160188013527428381638584034864162075113776466444960459732972748045817284823043261023619049710421064763568976480536206004614464678626466324994015457363029067726304364865152971988373237/808642906689290806339854868846296942466695098072825586043777191136825103946485010965961998823025737038750340546687738019028755195218073115162061105415017805059835863270032149368314762676427643167388230619705342369733372752853870044785286465773837799341030168572175789103006433196531501525771962993132710772170026972682519856523267396727586742427452320*y^11 - 296724263404046330628830445241107650982721485296304952737342892424420675195226597830416083103164372187076636905669019138843118340658206985153520301285103740484943665941689439357495818871343890855214275462162722824948383449193151366735698485346742003275593366319759994643772799469758706739568075489556372179554880233335839943582981388060135521950830142382225463/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^10 - 31297618037056295216229350079301524067535694635258032691480617880888464828339609715162558945840832829288107271311648832702916873436274968164189088155427865553174124509835810773611379727208963985509768573663759087221089086427698123411690725820251357336743699052777511857963666924839132577270985219369123830873383030276412689286531432320015104992622365019530347/19407429760542979352156516852311126619200682353747814065050652587283802494715640263183087971752617688930008173120505712456690124685233754763889466529960427321436060718480771584839554304234263436017317534872928216873600946068492881074846875178572107184184724045732218938472154396716756036618527111835185058532080647344380476556558417521462081818258855680*y^9 + 11938031172640034092891373899004323235397667627470346287377320537882500728638882281894016546075333795957373752003563047260421482723225411125789057549060265799501102838490181023619692192954664785522260136289488649992124348588442954435759771898701329165542667538578506100129493863918846072519851200500096737069084765401866317965431383452006144024504299498609327/9703714880271489676078258426155563309600341176873907032525326293641901247357820131591543985876308844465004086560252856228345062342616877381944733264980213660718030359240385792419777152117131718008658767436464108436800473034246440537423437589286053592092362022866109469236077198358378018309263555917592529266040323672190238278279208760731040909129427840*y^8 + 13301494226799593259696329444238359607263844402384758269011927620648449157133990779080295326330556720736222947957520066898667575089812295501130566108252335507614380283276933881047173470512194663465830204498609381420880801004870747699300238522871788348898516448602460881709365659859921151393350060021323939930396342162793802945980792530647512592795675599866083/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^7 - 4226742831322926094723904883559937902388639168475665998374329079652843829629914838634886054186011827145734553754939792147209923698059035907314591405008959975433104065107532041410181485660346041256542707754702672941262513696971115642329613651286445779530934123057895095960053142151991685896536544087198143722201190175764014902167884315734786336736506583105523/19407429760542979352156516852311126619200682353747814065050652587283802494715640263183087971752617688930008173120505712456690124685233754763889466529960427321436060718480771584839554304234263436017317534872928216873600946068492881074846875178572107184184724045732218938472154396716756036618527111835185058532080647344380476556558417521462081818258855680*y^6 - 134033581024521521047023476173160897478575654108988428329330132971421465946396657765599763228973393337029025014139123771983534629975568207868154674599944794167744311923882805137862004631526390236616826526002924314112347581755227170032549491066996712120779367726646962912934989618450120080799598220546026624923119955197529167151472595613218195685360437902427/25876573014057305802875355803081502158934243138330418753400870116378403326287520350910783962336823585240010897494007616608920166246978339685185955373280569761914747624641028779786072405645684581356423379830570955831467928091323841433129166904762809578912965394309625251296205862289008048824702815780246744709440863125840635408744556695282775757678474240*y^5 + 171812833763152955708291768585754935615284257046752981193584805586965192833036693609357726279254235318444475849299462809631456724944056479427355014077280909005635554452740679863920614154704374384002204632342078357947880921873235834286571975057448103463131603838664145728178647878466672865068651960506862398004144209307344469808840296917378349187249072981685/7762971904217191740862606740924450647680272941499125626020261034913520997886256105273235188701047075572003269248202284982676049874093501905555786611984170928574424287392308633935821721693705374406927013949171286749440378427397152429938750071428842873673889618292887575388861758686702414647410844734074023412832258937752190622623367008584832727303542272*y^4 - 86171346321366524031887950904146914996926651434962307013348876572036470949320604418374141245434507182487370997875808267803883772163903708375234658435315012326394201119603180084274880164708670992436076781774486041929226359796220045317448765935567430562604589936395176124016481015713259601881893078490615542958683857760339508215709688216770630735436030052867/77629719042171917408626067409244506476802729414991256260202610349135209978862561052732351887010470755720032692482022849826760498740935019055557866119841709285744242873923086339358217216937053744069270139491712867494403784273971524299387500714288428736738896182928875753888617586867024146474108447340740234128322589377521906226233670085848327273035422720*y^3 - 43006353590013909328637304873632000656889536978455738278790717231181625748424709806152238520985786448132536162000102477791151639004375249853752505084840920153478390421992727408581992762055053750725795933853057284358762764917364404852263848828337673412149722120083160497862507052690557849007535913133104824745000707739467653350659587966113097861419651726799/38814859521085958704313033704622253238401364707495628130101305174567604989431280526366175943505235377860016346241011424913380249370467509527778933059920854642872121436961543169679108608468526872034635069745856433747201892136985762149693750357144214368369448091464437876944308793433512073237054223670370117064161294688760953113116835042924163636517711360*y^2 + 5502335146597091866049936954035582177511588085235095940402439578367584410853866652912916711805349197474423226972948624121543558943807491492330066607117511728112920630154261470500865554479945970905369573331238944456858036601976120746716925602801070404377901273369508316107971159059512721278855706415572687650774963217903668461427892735856909271017953590431/38814859521085958704313033704622253238401364707495628130101305174567604989431280526366175943505235377860016346241011424913380249370467509527778933059920854642872121436961543169679108608468526872034635069745856433747201892136985762149693750357144214368369448091464437876944308793433512073237054223670370117064161294688760953113116835042924163636517711360*y + 136061738548686138496547202432523155567677978282916382977627658926532404023999556698274350181255375405008969722081941125444124535027506552784322091869338986716572250149181243867414216252570667855538864917927954452383544320052230036379726692769412444108569924386101462579736570325513975427923504914999848956138697677073760648081145194944874898308816589677/4312762169009550967145892633846917026489040523055069792233478352729733887714586725151797327056137264206668482915667936101486694374496389947530992562213428293652457937440171463297678734274280763559403896638428492638577988015220640238854861150793801596485494232384937541882700977048168008137450469296707790784906810520973439234790759449213795959613079040