# Manifold: Census Knot K8_155

# Number of Tetrahedra: 8

# Number Field
x^20 + 6*x^19 + 61*x^18 - 1066*x^17 - 2359*x^16 + 12994*x^15 + 43961*x^14 + 3405*x^13 - 161328*x^12 - 257710*x^11 - 42175*x^10 + 359933*x^9 + 528137*x^8 + 297090*x^7 - 35571*x^6 - 179966*x^5 - 166659*x^4 - 105798*x^3 - 44126*x^2 - 9841*x - 845 

# Approximate Field Generator
-0.487810895280551 + 0.984628811912258*I

# Shape Parameters
36535949775517861645832512027257163/768136442179735237323145610729396288*y^19 + 201435361099057332859297576459549901/768136442179735237323145610729396288*y^18 + 532970181154505623881267171224048219/192034110544933809330786402682349072*y^17 - 1537672841821629510544911670873090101/29543709314605201435505600412669088*y^16 - 66667167238443652391019961288299055487/768136442179735237323145610729396288*y^15 + 505786231606967601377252221972492385239/768136442179735237323145610729396288*y^14 + 679704307865202849847059371112446110149/384068221089867618661572805364698144*y^13 - 519687711261433394915752574983222108647/768136442179735237323145610729396288*y^12 - 5616269510422877233875408190426660020023/768136442179735237323145610729396288*y^11 - 6727671063230568108844233422675593651441/768136442179735237323145610729396288*y^10 + 800406143366730264703894372247291625069/384068221089867618661572805364698144*y^9 + 12299408644830048395496318179542425871929/768136442179735237323145610729396288*y^8 + 3359197287898761211642110906946613199607/192034110544933809330786402682349072*y^7 + 2282123264017123480274156906703999300313/384068221089867618661572805364698144*y^6 - 3365575541165112897321228748995162562239/768136442179735237323145610729396288*y^5 - 4950581086301250310913650437614219046953/768136442179735237323145610729396288*y^4 - 1875387237750171459953686884918592996613/384068221089867618661572805364698144*y^3 - 524723540818125184747773376404636407235/192034110544933809330786402682349072*y^2 - 315077220988814653977836873550511367211/384068221089867618661572805364698144*y - 5009726252781859205385277824005778101/59087418629210402871011200825338176

-118153519438721115952772261066461066/780138574088793600406319760897043105*y^19 - 653756137313234501763517152296715371/780138574088793600406319760897043105*y^18 - 6904456994649557044174564360371424121/780138574088793600406319760897043105*y^17 + 9935780168293752543692584337648276142/60010659545291815415870750838234085*y^16 + 218293822808931428425272084609913517934/780138574088793600406319760897043105*y^15 - 1634518743853173280225496102932122766694/780138574088793600406319760897043105*y^14 - 4429854012463171007505876444312063672536/780138574088793600406319760897043105*y^13 + 326498641820156019656179328785490398374/156027714817758720081263952179408621*y^12 + 18251317173001959360029643762738720398293/780138574088793600406319760897043105*y^11 + 4403062217192857129576495243171260826443/156027714817758720081263952179408621*y^10 - 1008094304357894072737508301419349670233/156027714817758720081263952179408621*y^9 - 40037142158862717257459509999155950574223/780138574088793600406319760897043105*y^8 - 43958910670982866064023661812244941623822/780138574088793600406319760897043105*y^7 - 3013397329716147014073280949246488279039/156027714817758720081263952179408621*y^6 + 10936637542810013035591471911056083143631/780138574088793600406319760897043105*y^5 + 16195420849766600683267617561538452559016/780138574088793600406319760897043105*y^4 + 12288607627567025351424009384695655144754/780138574088793600406319760897043105*y^3 + 6896887342896953204072423986323579263818/780138574088793600406319760897043105*y^2 + 2084577703896613921731050089082759271931/780138574088793600406319760897043105*y + 1323810453852738644192783741468724669/4616204580407062724297750064479545

6267348288157624264813562128184384924800871/477714979652382074462680653731958170463524120*y^19 + 7091424464419241077663976750221309481518893/95542995930476414892536130746391634092704824*y^18 + 92344805022446993918741767395503516462269479/119428744913095518615670163432989542615881030*y^17 - 3405338918787069479144979351884304076683891421/238857489826191037231340326865979085231762060*y^16 - 12492494173204068944341535851711856361247892387/477714979652382074462680653731958170463524120*y^15 + 86635091345840995972479556155743957567902084091/477714979652382074462680653731958170463524120*y^14 + 24590446871942066668614722014675106257798828253/47771497965238207446268065373195817046352412*y^13 - 14780974374270711410046317899082639840808836359/95542995930476414892536130746391634092704824*y^12 - 998475117137608732603639817648008860418014657443/477714979652382074462680653731958170463524120*y^11 - 1242207414751774327915244940752599624834827316117/477714979652382074462680653731958170463524120*y^10 + 118117923991258687188606977509716552339952230221/238857489826191037231340326865979085231762060*y^9 + 2204980009937826638607205869750155895884144480421/477714979652382074462680653731958170463524120*y^8 + 617694136906396051462410490125640085981884964359/119428744913095518615670163432989542615881030*y^7 + 437342973616407367262727765922209181474857796457/238857489826191037231340326865979085231762060*y^6 - 119387852160957702492177093096632165254352465831/95542995930476414892536130746391634092704824*y^5 - 902591541399533109410858565842153366171065981661/477714979652382074462680653731958170463524120*y^4 - 343702200573468809289215971819412563204741343509/238857489826191037231340326865979085231762060*y^3 - 19463709906723666701922640611128792547644468395/23885748982619103723134032686597908523176206*y^2 - 4575013848159088086880537351697728243448045951/18373653063553156710103102066613775787058620*y - 194452113880012320869595785589066539784592477/7349461225421262684041240826645510314823448

187648818654242602465863560114921439102434714898257/3357668939129671605714620630862402392794437020404360*y^19 + 204059808194806539240662228898879681077592967762795/671533787825934321142924126172480478558887404080872*y^18 + 2722679498473709985769444218315468751854782136242743/839417234782417901428655157715600598198609255101090*y^17 - 103041893112737842605234542959205187925251859453366007/1678834469564835802857310315431201196397218510202180*y^16 - 325724810626498206575354353082023516549419973212102589/3357668939129671605714620630862402392794437020404360*y^15 + 2600401013534174775704498270339815145367245784988352517/3357668939129671605714620630862402392794437020404360*y^14 + 677871300725937833213987365822910781343537304679419839/335766893912967160571462063086240239279443702040436*y^13 - 582884461018811449150172605127024675922947230697318025/671533787825934321142924126172480478558887404080872*y^12 - 28274332234033069164072699960649426887226570139701583381/3357668939129671605714620630862402392794437020404360*y^11 - 543276638117457787108384905716365377165342029130845279/55043753100486419765813452964957416275318639678760*y^10 + 337911059474364347391513219410990803220385881753495199/129141113043448907912100793494707784338247577707860*y^9 + 61598311926985701545035608323687103244341857464601874747/3357668939129671605714620630862402392794437020404360*y^8 + 16601729806539155976863083790179789526703629907052702223/839417234782417901428655157715600598198609255101090*y^7 + 11051279838061765825032537018832512261725852054354437039/1678834469564835802857310315431201196397218510202180*y^6 - 3376465002172982247781323640676722761227030946539855041/671533787825934321142924126172480478558887404080872*y^5 - 24609493786076866177510170935207803372127012155227282667/3357668939129671605714620630862402392794437020404360*y^4 - 9323976587152729835527650363039088254809184923734536383/1678834469564835802857310315431201196397218510202180*y^3 - 518795914831483524524176445089122354705257280911491089/167883446956483580285731031543120119639721851020218*y^2 - 120293077703092534003635592984623171064984939486607497/129141113043448907912100793494707784338247577707860*y - 5201747783079076152332544089313543378087617826211291/51656445217379563164840317397883113735299031083144

-3201475323825661097491247059684325584019234032026/419708617391208950714327578857800299099304627550545*y^19 - 4879463337090222458175761578894526760240460483119/83941723478241790142865515771560059819860925510109*y^18 - 216663778688430927073921365166640386466925837915266/419708617391208950714327578857800299099304627550545*y^17 + 3141923073219748407943354810829223785477112786779597/419708617391208950714327578857800299099304627550545*y^16 + 13616517972649411401656709854181240277219409796016582/419708617391208950714327578857800299099304627550545*y^15 - 40472852211646721655760375006295693175798941236287061/419708617391208950714327578857800299099304627550545*y^14 - 43313955907485566913779405650466537941354133442821790/83941723478241790142865515771560059819860925510109*y^13 - 19868702171998501149533933775251134232069178228692937/83941723478241790142865515771560059819860925510109*y^12 + 743957295960049186327148141560170473683221189649378753/419708617391208950714327578857800299099304627550545*y^11 + 22122220356580692169628092909133656653304958195535962/6880469137560802470726681620619677034414829959845*y^10 + 279882504489151373609681590599784380405464591214256768/419708617391208950714327578857800299099304627550545*y^9 - 1814550625533567241698115102082051017278133666359431411/419708617391208950714327578857800299099304627550545*y^8 - 2638339973103854734845965830499416340693566679610269506/419708617391208950714327578857800299099304627550545*y^7 - 1308346437046280562425965425332998028589853802930821674/419708617391208950714327578857800299099304627550545*y^6 + 81837040898532563014950915027197980864268091746636249/83941723478241790142865515771560059819860925510109*y^5 + 913591681410105832491129824096813499681742925603595506/419708617391208950714327578857800299099304627550545*y^4 + 727201589804031524143159449092636114323523123672247098/419708617391208950714327578857800299099304627550545*y^3 + 91118065880968247880301405412065944910349921876506355/83941723478241790142865515771560059819860925510109*y^2 + 12008199040759761169470023647493284417324313656121182/32285278260862226978025198373676946084561894426965*y + 297648922955029570773903357784845757442203746533335/6457055652172445395605039674735389216912378885393

-20902968591094456729702659300865847942336828892813/83941723478241790142865515771560059819860925510109*y^19 - 111961559146514074996838520140935931096224973033327/83941723478241790142865515771560059819860925510109*y^18 - 1205495208507222253234344205016597167273409956491593/83941723478241790142865515771560059819860925510109*y^17 + 23047769494864510952342994259048906858823141221575648/83941723478241790142865515771560059819860925510109*y^16 + 34340473653322419918599512239420534418701346234651358/83941723478241790142865515771560059819860925510109*y^15 - 22372449572818506690475086845121617570747582876036922/6457055652172445395605039674735389216912378885393*y^14 - 730489889008716952372992963368422495667379905449674266/83941723478241790142865515771560059819860925510109*y^13 + 363235484176267113302628908437779613417561855037078761/83941723478241790142865515771560059819860925510109*y^12 + 3087465532039898164278250651461507662365305559026359906/83941723478241790142865515771560059819860925510109*y^11 + 57275874212191253697397152657074446125847932025336460/1376093827512160494145336324123935406882965991969*y^10 - 84237822524397719144950857322366322895914288778943599/6457055652172445395605039674735389216912378885393*y^9 - 6676720400391080651588628197999203655741260592967663710/83941723478241790142865515771560059819860925510109*y^8 - 7013984569203752718089301969134279333471178954286393797/83941723478241790142865515771560059819860925510109*y^7 - 2215041141323176342889005203418155047336519369683520118/83941723478241790142865515771560059819860925510109*y^6 + 1857025679609382924214586175275859576400234725440356487/83941723478241790142865515771560059819860925510109*y^5 + 2615229525320446989682076904052920609521581507408665708/83941723478241790142865515771560059819860925510109*y^4 + 1970763930703044145949874881938671973706871590091117784/83941723478241790142865515771560059819860925510109*y^3 + 1082714699615571399905886983923089648585983484123378753/83941723478241790142865515771560059819860925510109*y^2 + 24616887926865773342033410891529826375845315427139024/6457055652172445395605039674735389216912378885393*y + 2602618193028056156632871791679999220801022056206748/6457055652172445395605039674735389216912378885393

-2525549276668184231205261697370383628356333245862471/2098543086956044753571637894289001495496523137752725*y^19 - 14056882946502751226198449365639122743873714436775861/2098543086956044753571637894289001495496523137752725*y^18 - 147970458548844468629039062277334717141841508805447061/2098543086956044753571637894289001495496523137752725*y^17 + 2756410770710457054374021827875861562541449625697487226/2098543086956044753571637894289001495496523137752725*y^16 + 4760364289393738129265614126505512079725038745118331304/2098543086956044753571637894289001495496523137752725*y^15 - 34866900260157434904656157440732957898929640453182572094/2098543086956044753571637894289001495496523137752725*y^14 - 95881911426778257331970282634649795090832826147540557631/2098543086956044753571637894289001495496523137752725*y^13 + 6563513000135304201341658420560309207403965754873861063/419708617391208950714327578857800299099304627550545*y^12 + 392897953491499755065143466706537168723703802857140657413/2098543086956044753571637894289001495496523137752725*y^11 + 121270629068677649643104326886121673404569263326339881/529266856735446343902052432355359771878063843065*y^10 - 20129058375703215412402903663829332589773512899496969363/419708617391208950714327578857800299099304627550545*y^9 - 66500235610895795957218609124751198986710053329551138631/161426391304311134890125991868384730422809472134825*y^8 - 960110362638034162383413906274445412626665942810685837047/2098543086956044753571637894289001495496523137752725*y^7 - 67306982971228409633452873377972350262549126392520972616/419708617391208950714327578857800299099304627550545*y^6 + 234107013538742166559344497420164364507832999727648843296/2098543086956044753571637894289001495496523137752725*y^5 + 353159567352034699800970172423157595627337950892959621916/2098543086956044753571637894289001495496523137752725*y^4 + 268585491120812705453282777559782219738083597591804580699/2098543086956044753571637894289001495496523137752725*y^3 + 151414373303601535539127289991082643183840128215064659043/2098543086956044753571637894289001495496523137752725*y^2 + 3558445698392690090717901272208155058938782930743666472/161426391304311134890125991868384730422809472134825*y + 382355375166103189572324434771226812120413114649819742/161426391304311134890125991868384730422809472134825

52389823488278746390575030103967870646576359822119/419708617391208950714327578857800299099304627550545*y^19 + 54797001656520536634118169560490869396023079815612/83941723478241790142865515771560059819860925510109*y^18 + 2992928774189442229234557492737984949157645564567609/419708617391208950714327578857800299099304627550545*y^17 - 58117615636579465608741253775412440013956927703332623/419708617391208950714327578857800299099304627550545*y^16 - 78386363195547101114645642928411695232190165366136203/419708617391208950714327578857800299099304627550545*y^15 + 731644667040697596304531010912879671132954064987209134/419708617391208950714327578857800299099304627550545*y^14 + 347209712985752314111482470346117605529256980742245386/83941723478241790142865515771560059819860925510109*y^13 - 208256011483809448926994262583840394144216219400916531/83941723478241790142865515771560059819860925510109*y^12 - 7486885841654640617928053847741029243830239598487357442/419708617391208950714327578857800299099304627550545*y^11 - 131916432566255199405209910458109743078745674202988928/6880469137560802470726681620619677034414829959845*y^10 + 3106870102533863787477391449720211443239480267675199178/419708617391208950714327578857800299099304627550545*y^9 + 16016650842183867002640975496045818715837116827571544734/419708617391208950714327578857800299099304627550545*y^8 + 16226221129649545199409247741592410742194361057032577064/419708617391208950714327578857800299099304627550545*y^7 + 4745354181039280567362042574222324372650484453910756471/419708617391208950714327578857800299099304627550545*y^6 - 905005413805630022453829643344494938189415783969475347/83941723478241790142865515771560059819860925510109*y^5 - 6110773296457561226999938519255956936988552961874561229/419708617391208950714327578857800299099304627550545*y^4 - 4575541386024140383739779491718208981976487167752853467/419708617391208950714327578857800299099304627550545*y^3 - 493693073139279800388390183524269372313708812454416653/83941723478241790142865515771560059819860925510109*y^2 - 54902838919896533726642011440895490983181385784205518/32285278260862226978025198373676946084561894426965*y - 1133332879984621614426709779387264653512310354977037/6457055652172445395605039674735389216912378885393


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

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

# nu Gluing Vector
{10, 10, 5, 5, 2, -1, 3, 5}

# f Combinatorial flattening
{-2, 19, -1, -32, -31, -31, -1, -1}

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

# 1 Loop Invariant
246627323179674005760948740261682668589863825619491/839417234782417901428655157715600598198609255101090*y^19 + 284359864264664449443423268475665326795838608663713/167883446956483580285731031543120119639721851020218*y^18 + 7340682789925094219481079366923281094840677550070683/419708617391208950714327578857800299099304627550545*y^17 - 133243062348074759903845832051536972254384509312898421/419708617391208950714327578857800299099304627550545*y^16 - 520709523292521907459600450969344718619764680022848517/839417234782417901428655157715600598198609255101090*y^15 + 3359999602304602205139267595310341583388173414039590631/839417234782417901428655157715600598198609255101090*y^14 + 1007327230396733699078391427825367360140099516709811470/83941723478241790142865515771560059819860925510109*y^13 - 389991741282786002343595092540958054664803255820478427/167883446956483580285731031543120119639721851020218*y^12 - 39990229007869807821166911601251157292315523135550498483/839417234782417901428655157715600598198609255101090*y^11 - 870017765565849025285869883335634381897387633177478127/13760938275121604941453363241239354068829659919690*y^10 + 2732155710536642451976796256335926745364462612131049746/419708617391208950714327578857800299099304627550545*y^9 + 89375389161805559444795757326922566084433754309122760981/839417234782417901428655157715600598198609255101090*y^8 + 52983277430824345027560286886754411567638632550893550953/419708617391208950714327578857800299099304627550545*y^7 + 20930191318983031882678958516411021398318951664568617312/419708617391208950714327578857800299099304627550545*y^6 - 348148494044479753137080623382384835660797342200345001/12914111304344890791210079349470778433824757770786*y^5 - 38486001576277611692985812829817345323772486953094377531/839417234782417901428655157715600598198609255101090*y^4 - 1150279366109369181794477368179247053429811206106586518/32285278260862226978025198373676946084561894426965*y^3 - 1733745625055396318216591928878144766595648882418305167/83941723478241790142865515771560059819860925510109*y^2 - 2807574513238349568623558764350044234878272248630513713/419708617391208950714327578857800299099304627550545*y - 10437407874520465935160071658039771774485955161464099/12914111304344890791210079349470778433824757770786

# 2 Loop Invariant
26218971900056225394662858041236572795264379127002662956679540276527075022456977337456834991449110337788153/15628736128345290909532296946256260512094835567735145857928476652828513361040626885563483514572294711675863340*y^19 + 81959824287487232064263714741174530201143775342015195224452338963390599247092302714029650632697983891721829/4167662967558744242541945852335002803225289484729372228780927107420936896277500502816928937219278589780230224*y^18 + 745168601936061293754464448513950895582691268118063341930081552931414252771291048692598759997721000878741911/5209578709448430303177432315418753504031611855911715285976158884276171120346875628521161171524098237225287780*y^17 - 80090335107699068770194194174364533357115120803796301256629959603511932407995159708514262541953595889907174679/62514944513381163638129187785025042048379342270940583431713906611314053444162507542253934058289178846703453360*y^16 - 944792398914703281637008570453701699538700074406530144954265669423042184265268444200673047683720901423010954189/62514944513381163638129187785025042048379342270940583431713906611314053444162507542253934058289178846703453360*y^15 + 71995393133493804455460022558755796862602428196580913140317899671369131560608517927775893495675816247773477817/3907184032086322727383074236564065128023708891933786464482119163207128340260156721390870878643073677918965835*y^14 + 884592354400835503368078985777696215542802846970193751498185873297025240730622359623462432062936198953940119465/4167662967558744242541945852335002803225289484729372228780927107420936896277500502816928937219278589780230224*y^13 + 2339354895781419485800329804259553377159963991870098810275848959798346475742993812730497393205351333598411768789/12502988902676232727625837557005008409675868454188116686342781322262810688832501508450786811657835769340690672*y^12 - 3409722793156828394017432912490490039760675206698056466188119246974433794886382517680835149018336448823751252223/5209578709448430303177432315418753504031611855911715285976158884276171120346875628521161171524098237225287780*y^11 - 9477255615899181003645779767598349813954151708056476316789847701175860526733335191923731595413197991694172459/6569456127929924720274189552860975414920065392070258872605496701483191828936791460934629472287639643411460*y^10 - 1989187932101568162366071642657329984232955960959512815307301361121687333015881316650115014871920081069391317556/3907184032086322727383074236564065128023708891933786464482119163207128340260156721390870878643073677918965835*y^9 + 53362796148791298301098147522238761192867896807824087046893874953830164251147312854182337298732401161161559472671/31257472256690581819064593892512521024189671135470291715856953305657026722081253771126967029144589423351726680*y^8 + 57894077859522398065064189472864061518498571638287378484728468183981108172118338855186486903952767514841040016699/20838314837793721212709729261675014016126447423646861143904635537104684481387502514084644686096392948901151120*y^7 + 93500706508000991517056104709637039705698188848070732222215593631550589039538035827490580908036475932268505482193/62514944513381163638129187785025042048379342270940583431713906611314053444162507542253934058289178846703453360*y^6 - 4597115575820787039401724669897000732660356458337137760837919035901696278567880767254301041854313838783301235703/12502988902676232727625837557005008409675868454188116686342781322262810688832501508450786811657835769340690672*y^5 - 29283877102895573127030607431101860862760682528981761239920375546994918991911478359286880511913762138727159831271/31257472256690581819064593892512521024189671135470291715856953305657026722081253771126967029144589423351726680*y^4 - 23445656323172141055974584547121248970138963559594346590612353558964198790138783952662856891317622643847418211843/31257472256690581819064593892512521024189671135470291715856953305657026722081253771126967029144589423351726680*y^3 - 1523570732034813901549178864056722670906093997302052181968833922205185081271804383053879220602777603003571628761/3125747225669058181906459389251252102418967113547029171585695330565702672208125377112696702914458942335172668*y^2 - 2643141264606531186087723095358384660306344637950559618735702403883547614528338481596924234251487766790564281813/15628736128345290909532296946256260512094835567735145857928476652828513361040626885563483514572294711675863340*y - 9013703226056876318980492631939869024229347359064719271040285679357616013558843344827723414308483388766694759/480884188564470489524070675269423400372148786699542949474722358548569641878173134940414877371455221897718872

# 3 Loop Invariant
-125484213667456584477110090619671679581189116653802416063424714246161064748775041990477266531361596660066074035245337664006612503672266137/4643227360852787292530501409327432332695384041881681884256689393216176064692492722275552803459471037265779073423301868359605215702830361280*y^19 - 142108854901405609227746184122413039775701591293930017674859435280090569091783404454513685615384267786301150199144148794088625174364408695/928645472170557458506100281865486466539076808376336376851337878643235212938498544455110560691894207453155814684660373671921043140566072256*y^18 - 1851387898352371987294953741573352010740053699047653765763360037921630675609279071546996319723356493637673120291722957760473171059986994833/1160806840213196823132625352331858083173846010470420471064172348304044016173123180568888200864867759316444768355825467089901303925707590320*y^17 + 136306436637375382090830191933526017559635130906961068106244514579835334828894360866949317774904526222127581427023952817546277952554272393749/4643227360852787292530501409327432332695384041881681884256689393216176064692492722275552803459471037265779073423301868359605215702830361280*y^16 + 250491090620816723219616952945597235963996536444155948736692215059395052893568124314668243773922899606183811594864501570593011309510846381979/4643227360852787292530501409327432332695384041881681884256689393216176064692492722275552803459471037265779073423301868359605215702830361280*y^15 - 862807891236634377589729430539467960196860208383930604197945783333100861306584911700290009086928571078954965965529158082077757340669349007701/2321613680426393646265250704663716166347692020940840942128344696608088032346246361137776401729735518632889536711650934179802607851415180640*y^14 - 493899958632494812960847763023995486630476500377135600986535880707770157746857253799126454681654679455928424616821548078654001928603504500283/464322736085278729253050140932743233269538404188168188425668939321617606469249272227555280345947103726577907342330186835960521570283036128*y^13 + 68583062406745901372062345141897548757210787595092009924870563768933936590356128694795155673378995764521185763597967476132300004218433366411/232161368042639364626525070466371616634769202094084094212834469660808803234624636113777640172973551863288953671165093417980260785141518064*y^12 + 2497058160187713291751583808647984173051647987265085766283130220097560135551290264628732247438855443971329792145121548683713200924597403310237/580403420106598411566312676165929041586923005235210235532086174152022008086561590284444100432433879658222384177912733544950651962853795160*y^11 + 15922939167816538877623831378228047486039911585937683880365352270541656828364642146427708741193786780873048324257046682210253275280096435279/2927633897132904976374843259348948507374138740152384542406487637589013912164245096012328375447333567002382770128185289003534183923600480*y^10 - 4260290349684140022727178531638572269998065215571770046022036418422967455721377012803835042636376649178471467420617942797148504431105213383599/4643227360852787292530501409327432332695384041881681884256689393216176064692492722275552803459471037265779073423301868359605215702830361280*y^9 - 22145416147690908258774113337118692002439525373383881727948014053467150400457494305386830435450330049298896684366097016125112738122061376471881/2321613680426393646265250704663716166347692020940840942128344696608088032346246361137776401729735518632889536711650934179802607851415180640*y^8 - 25158516916174771931965689879748095030362687675542792008039098618588274874259234627452651625683610887361503700989701398719146359900386124297581/2321613680426393646265250704663716166347692020940840942128344696608088032346246361137776401729735518632889536711650934179802607851415180640*y^7 - 1409259686809730323571006228223345356448375197840732985758133585915651072714749490469779353328620341353230285263044477708227242344634203321511/357171335450214407117730877640571717899644926298590914173591491785859697284037901713504061804574695174290697955638605258431170438679258560*y^6 + 2372527989913158540831516855038562282217682445790651587754560016316297157930890385869689183319290567079392549469882030442290162537457419909405/928645472170557458506100281865486466539076808376336376851337878643235212938498544455110560691894207453155814684660373671921043140566072256*y^5 + 176997282251157757678820660667201747373974001878664938960619248194478812970701235266705545009281299577972007857404410094502398450086658744873/44646416931276800889716359705071464737455615787323864271698936473232462160504737714188007725571836896786337244454825657303896304834907320*y^4 + 270111170249770545675248890079500822629142548321076939864651514685678528289290056783265311939125075278771887968363765567126113958609410793283/89292833862553601779432719410142929474911231574647728543397872946464924321009475428376015451143673793572674488909651314607792609669814640*y^3 + 30780726033207861203811489947353841784953906611543673271530091961973682082732987342021631596278074031782498184313023515403563701819016708385/17858566772510720355886543882028585894982246314929545708679574589292984864201895085675203090228734758714534897781930262921558521933962928*y^2 + 618458242937133621912176725315008965544040235386128701280055259965104651457849032330811980061738509373454394187030786834379578768339125609043/1160806840213196823132625352331858083173846010470420471064172348304044016173123180568888200864867759316444768355825467089901303925707590320*y + 4120004398485074055687822867789813856609229751404334268063478720428202353910025335725636321559683862840706166957761258306373011278523271927/71434267090042881423546175528114343579928985259718182834718298357171939456807580342700812360914939034858139591127721051686234087735851712

# 4 Loop Invariant
-37051249380086426108322676628170134503034823087918738301070149662057063311317491890153874612819461303030410381099081568402613695747912377365592005533502903601889036359327443429355777252146787672855/207480443907229500273871374327742707368127963648300028900656488058015745726663999794457832524720985039443833669946190135033496262844143248224773676878135125723040275692244016532789949980118716431872*y^19 - 1029633531054151302935742780839221945674624718999240486411848117763520179939668482169972229077607154393329402609500690743419848379225635728850836502336534928767432759215509844617229022776950560013967/1037402219536147501369356871638713536840639818241500144503282440290078728633319998972289162623604925197219168349730950675167481314220716241123868384390675628615201378461220082663949749900593582159360*y^18 - 21693721579716650473531470368396233010851702099512476917800906297553784003496022935474632169037766093081644917219762815947483762761775759443163431394860705445487807450046231210600090999611151148913357/2074804439072295002738713743277427073681279636483000289006564880580157457266639997944578325247209850394438336699461901350334962628441432482247736768781351257230402756922440165327899499801187164318720*y^17 + 404543577218608238541916552262689810045125023223774844784982234961509960988540893261574226168258589850685540394523715321079940772395455985808943280457300360267370751094602541876988850384080299787637207/2074804439072295002738713743277427073681279636483000289006564880580157457266639997944578325247209850394438336699461901350334962628441432482247736768781351257230402756922440165327899499801187164318720*y^16 + 43439247323127366916503643731393232547954528955212110744961534094930574975096158516953523018837951038154050454921819029426788132222153361442589724367021078488509413149967188171570486817671336487270973/129675277442018437671169608954839192105079977280187518062910305036259841079164999871536145327950615649652396043716368834395935164277589530140483548048834453576900172307652510332993718737574197769920*y^15 - 2559221989569625151840049689026368801317794734649899613933458044766877801555308494813347398915104153441643896483472697628420339453707687529659180263893150890265759053065956808245661081688382127414448511/1037402219536147501369356871638713536840639818241500144503282440290078728633319998972289162623604925197219168349730950675167481314220716241123868384390675628615201378461220082663949749900593582159360*y^14 - 1685370664729124001539793254123767659208610669525466165966411150335242415748858895359164793282828323863817568018981057339038791318525887181455131961664559063308353626969568792978308851795098415921435/249375533542343149367633863374690754048230725538822150120981355838961232844548076676031048707597337787793069314839170835376798392841518327193237592401604718417115715976254827563449459110719611096*y^13 + 61186851389654510486457090620492412094239224453916644388541606395197402948872655637395632316453691930042184284099165194550102213471275555486021476231075264478268524694744995247602420243045729783887219/25935055488403687534233921790967838421015995456037503612582061007251968215832999974307229065590123129930479208743273766879187032855517906028096709609766890715380034461530502066598743747514839553984*y^12 + 6392737671075424392802058031420832678405324545954555745139214521389826587456929158280089683303687970137442480707744676362582972801515606861557369360143738046062209806727840697386269527663330992668554351/230533826563588333637634860364158563742364404053666698778507208953350828585182221993842036138578872266048704077717989038926106958715714720249748529864594584136711417435826685036433277755687462702080*y^11 + 143756539230281250687942901754898809827749077049540913857832668704671270312967514832098313084458694668309687171109569270960952210397841688275646487612988463531229129089117350368592180518442334353088381/4251648440721915989218675703437350560822294337055328461079026394631470199316885241689709682883626742611553968646438322439210988992707853447228968788486375527111481059267295420753892417625383533440*y^10 - 15019106995251470679595705424050812355574689798702621372725095389309459414185808205251776379168978954777188291054925464676338528209260162001576016524857174331841382577731720486532437305214878551262429769/2074804439072295002738713743277427073681279636483000289006564880580157457266639997944578325247209850394438336699461901350334962628441432482247736768781351257230402756922440165327899499801187164318720*y^9 - 126488150708952826903492470748412907184615613929330489041479715825101325719227718995756983696436490455137581120434343627996812344618144899894474398747059818886789877391156877481508985390583489165714834879/2074804439072295002738713743277427073681279636483000289006564880580157457266639997944578325247209850394438336699461901350334962628441432482247736768781351257230402756922440165327899499801187164318720*y^8 - 140096206704922587164134995135901922193115348321298909389810436338102990006437736142511224564059465219345214758134475233923860292663285022044652050311830405490076701730094147184550177714165926581981291917/2074804439072295002738713743277427073681279636483000289006564880580157457266639997944578325247209850394438336699461901350334962628441432482247736768781351257230402756922440165327899499801187164318720*y^7 - 24429349307060280626106733971552441146228490267247271405947408978941518387357144507148465013731702212620132025725184546282114224501790882885930543324787581233236854939364161975381166491300438363223970619/1037402219536147501369356871638713536840639818241500144503282440290078728633319998972289162623604925197219168349730950675167481314220716241123868384390675628615201378461220082663949749900593582159360*y^6 + 34311701774049758348599380901266901991931754720567995092826513576251123338652080628189017720269636110067492991640858282124876284876712148395460024706557953748124809665048231674564905508416872640606622029/2074804439072295002738713743277427073681279636483000289006564880580157457266639997944578325247209850394438336699461901350334962628441432482247736768781351257230402756922440165327899499801187164318720*y^5 + 6445485152210678017258053613074197973223172615860218044062953580828043680196079899747835647692243661217476661311020690514280972724404724225596042197991925370932430669011936471590648791973803501216360009/259350554884036875342339217909678384210159954560375036125820610072519682158329999743072290655901231299304792087432737668791870328555179060280967096097668907153800344615305020665987437475148395539840*y^4 + 1633139171079139187881036478641568930592969945080965080433171412950146447872210836465379532519314891798869934306743533072337354781025376886786907560910749742783373688840385051306822895692582055296820637/86450184961345625114113072636559461403386651520125012041940203357506560719443333247690763551967077099768264029144245889597290109518393020093655698699222969051266781538435006888662479158382798513280*y^3 + 22062222874159674981226547390973981398369610606019700538646346944870873873541856494143040620042586355294857922418198714141407834991609378170975421817572799516635247196200101155750072010303242693033544921/2074804439072295002738713743277427073681279636483000289006564880580157457266639997944578325247209850394438336699461901350334962628441432482247736768781351257230402756922440165327899499801187164318720*y^2 + 34502145565962708006958201830005700654799838928410627534856342264180100771320060662844313037486249593167797593643924152611932361100635864158924119618083751839754124669208082236222251273348684365828987/10640022764473307706352378170653472172724510956323078405161871182462345934700717938177324744857486412279170957433137955642743398094571448626911470609135134652463603881653539309373843588724036740096*y + 11105768756326322570134256471862871937843392377523919917648818574297151951892261325109048898874892867351444689926823336757752221492603003100927313769916806693246247907914261607054926280490616786075645/31920068293419923119057134511960416518173532868969235215485613547387037804102153814531974234572459236837512872299413866928230194283714345880734411827405403957390811644960617928121530766172110220288