# Manifold: Census Knot K8_149 # Number of Tetrahedra: 8 # Number Field x^20 + 4*x^19 + 58*x^18 - 412*x^17 + 1515*x^16 - 4504*x^15 + 22510*x^14 - 68000*x^13 + 104407*x^12 - 77393*x^11 + 3856*x^10 + 47974*x^9 - 43190*x^8 + 13972*x^7 + 898*x^6 - 2015*x^5 + 627*x^4 + 31*x^3 - 21*x^2 + 6*x + 1 # Approximate Field Generator 0.793063039080743 - 0.155327022073753*I # Shape Parameters 46970753180361686232316774607610956210881193587/4344329116666315782151354313150691617167667575*y^19 + 7184445720431539936490304335059278871388991532/173773164666652631286054172526027664686706703*y^18 + 2692048365939019751799636670612259692173995163746/4344329116666315782151354313150691617167667575*y^17 - 19828890485641930688767223027868030668162803118378/4344329116666315782151354313150691617167667575*y^16 + 74615021791630399994237197256123051653668858693692/4344329116666315782151354313150691617167667575*y^15 - 224459768523351572896480268646220422365648356738466/4344329116666315782151354313150691617167667575*y^14 + 1096038457112600961869837303371698814047685866311609/4344329116666315782151354313150691617167667575*y^13 - 3384738540179622760693035885149098451517580579376961/4344329116666315782151354313150691617167667575*y^12 + 5487621719059019425849536638738609753419711079238203/4344329116666315782151354313150691617167667575*y^11 - 4566912515894482945832678472599249480544640121712103/4344329116666315782151354313150691617167667575*y^10 + 943368903930892263142284476704994024249931539135034/4344329116666315782151354313150691617167667575*y^9 + 2101623996767455757016967841564398395394571842975677/4344329116666315782151354313150691617167667575*y^8 - 2379454411556295113689377999504499180471804225026638/4344329116666315782151354313150691617167667575*y^7 + 1049321544856098030844940396917013553799269691611516/4344329116666315782151354313150691617167667575*y^6 - 133799476288876223793157667516545085388961335350488/4344329116666315782151354313150691617167667575*y^5 - 67258280618251820358857698458700972367871655908128/4344329116666315782151354313150691617167667575*y^4 + 38879488932069909553136832787514316598128790897761/4344329116666315782151354313150691617167667575*y^3 - 424254745815156817876631093840316254581030815544/334179162820485829396258024088514739782128275*y^2 + 65978734894581335279522437960768955539005465711/4344329116666315782151354313150691617167667575*y + 231574893171023996407569900878294481973761039853/4344329116666315782151354313150691617167667575 3084559680265598556416618764049551945086383/173773164666652631286054172526027664686706703*y^19 + 9570843673715887256588934998360221308134229/173773164666652631286054172526027664686706703*y^18 + 168017163596118310301092472244066220787850318/173773164666652631286054172526027664686706703*y^17 - 1430596300059913766927298101241344189591374838/173773164666652631286054172526027664686706703*y^16 + 5823728130070006272339014332079480135871317223/173773164666652631286054172526027664686706703*y^15 - 18160313739088884221954475217035498112693999452/173773164666652631286054172526027664686706703*y^14 + 82151814064010819053135845405047248267268175955/173773164666652631286054172526027664686706703*y^13 - 272759113456458753470360436927850635799142889787/173773164666652631286054172526027664686706703*y^12 + 513994292024940821548687776311248731960361326715/173773164666652631286054172526027664686706703*y^11 - 538859893462790901343823703016066234335478108593/173773164666652631286054172526027664686706703*y^10 + 239607809734645370669856763678409102011285460319/173773164666652631286054172526027664686706703*y^9 + 135715434227598428589562712070650305971550272040/173773164666652631286054172526027664686706703*y^8 - 278713797298229241679090556898724344684804246397/173773164666652631286054172526027664686706703*y^7 + 176918363806602590095675528027464439882849132845/173773164666652631286054172526027664686706703*y^6 - 40940971783119804894393947136292617226963706409/173773164666652631286054172526027664686706703*y^5 - 11588451005499194013064209021201640212845975573/173773164666652631286054172526027664686706703*y^4 + 10055810796740421509862412352628492578067933009/173773164666652631286054172526027664686706703*y^3 - 167261362838976659966930678605010324804410207/13367166512819433175850320963540589591285131*y^2 - 53948900720034498471286898950999387841384503/173773164666652631286054172526027664686706703*y + 287219900311274543015698636629262702385559568/173773164666652631286054172526027664686706703 -222760130179234510405947259738928843847442584432/395333949616634736175773242496712937162257749325*y^19 - 36119911028171249570204796437902361147796189909/15813357984665389447030929699868517486490309973*y^18 - 12972213229875354752341668389497445474804083686706/395333949616634736175773242496712937162257749325*y^17 + 91065034929888286711944731447177181543712375792058/395333949616634736175773242496712937162257749325*y^16 - 332811186958777865712938033090078919333030356384462/395333949616634736175773242496712937162257749325*y^15 + 986878631014683277581753988470327414644055303086826/395333949616634736175773242496712937162257749325*y^14 - 4966459195666184743998503830502630493636577189195024/395333949616634736175773242496712937162257749325*y^13 + 14896098905330345692054524063137328918735378437691521/395333949616634736175773242496712937162257749325*y^12 - 22536196177978063245125862787833756751916531100620483/395333949616634736175773242496712937162257749325*y^11 + 2322193204971240479248262887815645898748265546256819/56476278516662105167967606070958991023179678475*y^10 - 305597781547817895659354184604414757870744595809399/395333949616634736175773242496712937162257749325*y^9 - 10493953345888401499775105796015376716750303568542722/395333949616634736175773242496712937162257749325*y^8 + 9074066938801206268988343800541268030910110545034243/395333949616634736175773242496712937162257749325*y^7 - 2778358368377182061645858799492118865801644089066326/395333949616634736175773242496712937162257749325*y^6 - 229875935993564031903916681073917918680890425800982/395333949616634736175773242496712937162257749325*y^5 + 402881433125722211929755964328368725903843600042358/395333949616634736175773242496712937162257749325*y^4 - 121850285432763882073851377985387813405699605249921/395333949616634736175773242496712937162257749325*y^3 - 542656039221875515678586194132479839008321384966/30410303816664210475059480192054841320173673025*y^2 + 2307914365006874236974760365333903937143890546104/395333949616634736175773242496712937162257749325*y - 1081617341069457874527843541965937907282617117633/395333949616634736175773242496712937162257749325 -3004194012198212314590018663937018755585417701/251636909603825829535382292138651599055942591075*y^19 - 178723483055839848753465342858825427393879231/3355158794717677727138430561848687987412567881*y^18 - 180149081905278114587889260480407909179957661358/251636909603825829535382292138651599055942591075*y^17 + 1155339621824416375706418629228052845269493541319/251636909603825829535382292138651599055942591075*y^16 - 4002481833579899453296697300670718547243249399716/251636909603825829535382292138651599055942591075*y^15 + 3848733380201669497003265252394034741183294115631/83878969867941943178460764046217199685314197025*y^14 - 61722621000653118585534064389719629356579577858532/251636909603825829535382292138651599055942591075*y^13 + 57990884205892636918651536208019242664596988466226/83878969867941943178460764046217199685314197025*y^12 - 225309259695409828296285989797381097574818906198969/251636909603825829535382292138651599055942591075*y^11 + 33785907278185034495119053814978579008090078558023/83878969867941943178460764046217199685314197025*y^10 + 88791745408146034183352592673240043306489894649343/251636909603825829535382292138651599055942591075*y^9 - 54931930143757200379067216494149189031872010952707/83878969867941943178460764046217199685314197025*y^8 + 361514272604831285247338007798334051903003312349/1002537488461457488188774072265544219346384825*y^7 + 275409800851563394936184708807919079851920749594/83878969867941943178460764046217199685314197025*y^6 - 24741344691522998281743399982231968780412111698176/251636909603825829535382292138651599055942591075*y^5 + 4858027208413915747620642739090727833527877517123/83878969867941943178460764046217199685314197025*y^4 - 1350728906278630111341082842412619326877810037426/83878969867941943178460764046217199685314197025*y^3 + 4797559057773867009216167086018006561468456756/251636909603825829535382292138651599055942591075*y^2 - 59908566613430092015806279003861934571246560228/251636909603825829535382292138651599055942591075*y + 269957070014291699814158535876002316714204282631/251636909603825829535382292138651599055942591075 -91870080596875638635371639732275516125278528/51129411911534331897627477685542755186665626075*y^19 - 20673980091756564671233101745207688650525657/681725492153791091968366369140570069155541681*y^18 - 10251999143632634776199303027391910202771432749/51129411911534331897627477685542755186665626075*y^17 - 31603732893549507287179782459827156967040703668/51129411911534331897627477685542755186665626075*y^16 + 336791008393373849439044521776507290694601977952/51129411911534331897627477685542755186665626075*y^15 - 434748048999404423710256660307513031480864827307/17043137303844777299209159228514251728888542025*y^14 + 2995648811456700086279794393057241707990763071304/51129411911534331897627477685542755186665626075*y^13 - 6534769778512193289494634065767352045865266755772/17043137303844777299209159228514251728888542025*y^12 + 66784946104230702278205864573037066352775000372968/51129411911534331897627477685542755186665626075*y^11 - 34918897957995252832917914310392550543623175116756/17043137303844777299209159228514251728888542025*y^10 + 74671027609171772064614982774234945196370025498029/51129411911534331897627477685542755186665626075*y^9 + 700402742025123605526765879434197310823457758529/17043137303844777299209159228514251728888542025*y^8 - 3084120537497550341110215021958779759360906673559/3007612465384372464566322216796632658039154475*y^7 + 4699519300137416685918429456555543968979381808669/5681045767948259099736386409504750576296180675*y^6 - 10482326131341880474562907125692279155587761584778/51129411911534331897627477685542755186665626075*y^5 - 969935830936708739324565834069002656800231807631/17043137303844777299209159228514251728888542025*y^4 + 782718711652852305994299184550090402794070985872/17043137303844777299209159228514251728888542025*y^3 - 496160372470748492808430802885068008064881119032/51129411911534331897627477685542755186665626075*y^2 - 200956598888798831064728179013446947847525269434/51129411911534331897627477685542755186665626075*y + 94484550509136285681820371416492644668315549893/51129411911534331897627477685542755186665626075 -11957254987343197631330871991843653305134409997/395333949616634736175773242496712937162257749325*y^19 - 2085027179190125951869092985582901266096551586/15813357984665389447030929699868517486490309973*y^18 - 712138703956331575305539565261502121433968993926/395333949616634736175773242496712937162257749325*y^17 + 4670410262762417552072065414398279095845159030018/395333949616634736175773242496712937162257749325*y^16 - 16432995312588957286632469393808098044826097194902/395333949616634736175773242496712937162257749325*y^15 + 47871334668384085239368986220657781369355386369296/395333949616634736175773242496712937162257749325*y^14 - 251589946857601015549889599109832462890717303684479/395333949616634736175773242496712937162257749325*y^13 + 721520733645274282827872759728587047663406812171341/395333949616634736175773242496712937162257749325*y^12 - 984722320162813109109636058265398720647265113148043/395333949616634736175773242496712937162257749325*y^11 + 79052182917615768066568349849842123429284858537199/56476278516662105167967606070958991023179678475*y^10 + 192741139330194902439808042699995637986906976998046/395333949616634736175773242496712937162257749325*y^9 - 546943083639932235444518347583068734860934676583837/395333949616634736175773242496712937162257749325*y^8 + 334046170487082517746036313580194940434823700617578/395333949616634736175773242496712937162257749325*y^7 - 29837339092611441559376041828359816905886984981046/395333949616634736175773242496712937162257749325*y^6 - 45980229185435326538227764045572894448753207588122/395333949616634736175773242496712937162257749325*y^5 + 17820316189616155950677553870920571686646895188943/395333949616634736175773242496712937162257749325*y^4 - 148964474328111881237255471815443747837457887166/395333949616634736175773242496712937162257749325*y^3 - 182311412981311575503856314552584752588646440536/30410303816664210475059480192054841320173673025*y^2 - 140390509610685548267933226029077781360219360366/395333949616634736175773242496712937162257749325*y + 222760130179234510405947259738928843847442584432/395333949616634736175773242496712937162257749325 -28825678822935738117515000500422242457369898/334179162820485829396258024088514739782128275*y^19 - 4888465388018283264416273684731125126429810/13367166512819433175850320963540589591285131*y^18 - 1701226818218882901623093413825130387465544934/334179162820485829396258024088514739782128275*y^17 + 11467628771456075441117921119711390460743329412/334179162820485829396258024088514739782128275*y^16 - 40927771928452823322638747218905498904637565893/334179162820485829396258024088514739782128275*y^15 + 120003030300941871496492856810986461977780033239/334179162820485829396258024088514739782128275*y^14 - 619935775234333159472382754212554740591013920511/334179162820485829396258024088514739782128275*y^13 + 1810939964629455929756572282651838868222582815619/334179162820485829396258024088514739782128275*y^12 - 2574190572346855723180582834966086311384220088762/334179162820485829396258024088514739782128275*y^11 + 1604247361377171000071124120952931329216767769837/334179162820485829396258024088514739782128275*y^10 + 304624548315262198439489098451898369770856289314/334179162820485829396258024088514739782128275*y^9 - 1354016142189302378241092507524249540943295856758/334179162820485829396258024088514739782128275*y^8 + 945256425582451257357501234741910771980881469602/334179162820485829396258024088514739782128275*y^7 - 167199807453294454798398030773197173586329454414/334179162820485829396258024088514739782128275*y^6 - 91000380496796192470222398413633369423789421573/334179162820485829396258024088514739782128275*y^5 + 51216353900139225093705378837648018562481009112/334179162820485829396258024088514739782128275*y^4 - 6637797187503940168473171222217485660449297319/334179162820485829396258024088514739782128275*y^3 - 5193306191714183200996845544744152501955614587/334179162820485829396258024088514739782128275*y^2 + 509714942603743217481079805848540254275204781/334179162820485829396258024088514739782128275*y - 177446743614733616294015631575890614234128087/334179162820485829396258024088514739782128275 83543295619728022933405552357841364407792992039/7822800022464752780337004085888041543559840789475*y^19 + 4515876608692397299944218232766919381931833398/104304000299530037071160054478507220580797877193*y^18 + 4840034280661347011858318728221120424279519120687/7822800022464752780337004085888041543559840789475*y^17 - 34273605035125591689259887140193654312918866172116/7822800022464752780337004085888041543559840789475*y^16 + 123236619642959117743999430731915850803427116258199/7822800022464752780337004085888041543559840789475*y^15 - 120357834244702320610179561067478668743746061513884/2607600007488250926779001361962680514519946929825*y^14 + 1832314799866036264664122124161793079387146839475698/7822800022464752780337004085888041543559840789475*y^13 - 1833124925603834115978152979755456130388073003924014/2607600007488250926779001361962680514519946929825*y^12 + 7960520719808829366834623690890719742811677535571316/7822800022464752780337004085888041543559840789475*y^11 - 1605237212656104803150636087476129831137341214310972/2607600007488250926779001361962680514519946929825*y^10 - 1372349958228095827131458913937612252858213809871877/7822800022464752780337004085888041543559840789475*y^9 + 1510129375239397315196353268955955873326167544112823/2607600007488250926779001361962680514519946929825*y^8 - 171688785314025009386732145889427876708332523393608/460164707203808987078647299169884796679990634675*y^7 + 24416387808724337198694698693422357970544063979703/869200002496083642259667120654226838173315643275*y^6 + 456102060225786188865598841028605283504591982245664/7822800022464752780337004085888041543559840789475*y^5 - 51708747539487281358070313105799165683584216623347/2607600007488250926779001361962680514519946929825*y^4 - 1389661765858430250270964965732989315644400871011/2607600007488250926779001361962680514519946929825*y^3 + 24911147440714285871036996895535524959267239869691/7822800022464752780337004085888041543559840789475*y^2 + 2596974855737473426289587286721417903036571685342/7822800022464752780337004085888041543559840789475*y + 1213817584459737925838854234882866097449512458216/7822800022464752780337004085888041543559840789475 # A Gluing Matrix {{1,1,2,0,2,0,0,0},{2,1,4,0,4,0,0,0},{0,1,0,1,-1,0,0,0},{0,0,1,1,1,0,0,0},{0,1,-1,1,0,1,-1,-1},{0,0,0,0,1,1,0,0},{0,0,0,0,-1,0,0,0},{0,0,0,0,-2,0,0,1}} # B Gluing Matrix {{1,2,0,0,0,0,0,0},{0,4,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,2}} # nu Gluing Vector {3, 4, 0, 1, 0, 1, 0, 0} # f Combinatorial flattening {-5, 2, 3, -2, 0, 1, -2, 0} # f' Combinatorial flattening {0, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant 41961473137044781108297237256681951385642826326/4344329116666315782151354313150691617167667575*y^19 + 13373908538237258529256800312242945799421513065/347546329333305262572108345052055329373413406*y^18 + 2432105212553625415948236280980248623177135755408/4344329116666315782151354313150691617167667575*y^17 - 17322838655552026713847765902986048322011358185919/4344329116666315782151354313150691617167667575*y^16 + 63909013223963278179641855819826685121283947548616/4344329116666315782151354313150691617167667575*y^15 - 190425843614499321558317175593750308514968192851368/4344329116666315782151354313150691617167667575*y^14 + 949089648836173460363702493489650512047763755179357/4344329116666315782151354313150691617167667575*y^13 - 5745995410861820039814465845264113289677284153058531/8688658233332631564302708626301383234335335150*y^12 + 8899055653239524911404968857996478073141618337170963/8688658233332631564302708626301383234335335150*y^11 - 6770023524591345988282396545176712454471713384530263/8688658233332631564302708626301383234335335150*y^10 + 631508887457100022452879698320555523909198122248989/8688658233332631564302708626301383234335335150*y^9 + 1933662870476227550786968096042604154678026746300496/4344329116666315782151354313150691617167667575*y^8 - 3674280789187143324960479296118327377287193891411173/8688658233332631564302708626301383234335335150*y^7 + 659290390284232520145332925898780795398640467185368/4344329116666315782151354313150691617167667575*y^6 - 13842394639635054720862649697853578952560805452399/4344329116666315782151354313150691617167667575*y^5 - 69106559740061316929503577058663121501517705776794/4344329116666315782151354313150691617167667575*y^4 + 27087130820468573706680757533901643102330492641678/4344329116666315782151354313150691617167667575*y^3 - 149211762186686475601813044543705565654460967749/668358325640971658792516048177029479564256550*y^2 - 258287779433274256075159092230719482262779435847/4344329116666315782151354313150691617167667575*y + 489447716175550957090991910400984854373978499763/8688658233332631564302708626301383234335335150 # 2 Loop Invariant -206367114013651146601684393411252597002005450248064700246413150385858390048326415270340965385644799565137/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^19 - 58388022664816671777351636905372374863942256334267845352302848610077365259841862016751620410460731563251/878536402544214356986863997777744142261546460318292488935950372734170835741865233997739484027227404241788*y^18 - 12184799771587438513169287502775154940880765047499166064533662613114310858808959647489885378705019774282131/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^17 + 20509409238644939823253861915967459182681085662014580469665578074345408454887730103213519496407852143116012/3294511509540803838700739991666540533480799226193596833509813897753140634031994627491523065102102765906705*y^16 - 292759077400184567932934191920255579571883886148779726387830610203786852936425175885517017329647939326485597/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^15 + 429235235584443996198124892685894041669057928052159920596084671033252755356574768629217722826437482544763943/6589023019081607677401479983333081066961598452387193667019627795506281268063989254983046130204205531813410*y^14 - 369713905435071500890232200264582656746922137833708345792821199313215731321828399481513674922526904288197507/1098170503180267946233579997222180177826933075397865611169937965917713544677331542497174355034034255302235*y^13 + 4317182743995030576125604603166890052418904286541783871773211839309205747281737607597804182737291029454138727/4392682012721071784934319988888720711307732301591462444679751863670854178709326169988697420136137021208940*y^12 - 18406348407290931554285314097261370999643836592335808144516665473398414850659534888539764578002446933765229593/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^11 + 3831119735185951583775393190454704556656171080993772707180418072505106820149486478828943623517639568417633681/4392682012721071784934319988888720711307732301591462444679751863670854178709326169988697420136137021208940*y^10 + 1064013836548988542311032102797469552852630395084025581236089995526570567196253567370535488591893686493661293/6589023019081607677401479983333081066961598452387193667019627795506281268063989254983046130204205531813410*y^9 - 9645395443696607240094940161829996344906926430757733869811091973700542743782962307820452245207927640714588327/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^8 + 6762457989490731683515721021498981361012691686752287711327558896463700274317056982692933545516375333539163283/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^7 - 1225902510872532144098696183453003711715533954493481300139111633920814023121577616754958602196235575533188801/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^6 - 316249674243853042316419790299807540169076360704559016633620126087623225460378814997376684262858815975992501/6589023019081607677401479983333081066961598452387193667019627795506281268063989254983046130204205531813410*y^5 + 366465307826156215540031782072360000461564083513057747103669709483636962877147820748072627272649152598560783/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y^4 - 16880266151603931789068907473536604557283036447109987012387810478457191870084136182248258498815784418065597/4392682012721071784934319988888720711307732301591462444679751863670854178709326169988697420136137021208940*y^3 - 455569194769351088280779071577708238215811945688469546251889754638993630643677369248883880518405761939891/168949308181579684035935384188027719665682011599671632487682763987340545334974083461103746928312962354190*y^2 + 3003623896960668206315890968404231309059077695307018708110426369649190523359831431203321005618041814574629/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820*y - 12695297951334413449794867976376890259464330833388575119017302656762476200809848365403142338276833980927393/13178046038163215354802959966666162133923196904774387334039255591012562536127978509966092260408411063626820 # 3 Loop Invariant 2734326484866570477868580793842706961861756281985865731491477443303069030841522749538278214304520316416540036572910886133627809005601/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^19 + 482776179316597358047205365105706623910153444511968745853543853039918909041438686894428760616527217213284681497522669425056585787719/246921155093377936943364194012882761020855014126312109641319462054329610384305352913602330891518114625708392461097257820848251530064871*y^18 + 162914895032065345550211322075543909624787678175229516088667873692186193983949661468410775960876894139774318505422587237335855850503883/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^17 - 1061750929379971239862653256280754543989325043767665941070149020838339901236346823658771541291387997611938170593478401267229858459180294/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^16 + 3663991705927190762765082202592630266769826468039178699100431106402232988069904056913864061015850075986899197648181571251527500346486991/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^15 - 10519226513472685651176027376789054802082804242469473813478928642195571607093855419113713482631621189932027003611527063581020364880437743/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^14 + 56161101455378726088823336888462212135582791515173879216736521434156357132587136191377460024060542976987403266241544074306204173917425507/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^13 - 159603532023458837855738829692502576724061031004243616625552243561373455164390396868749565900432108314384224960558963777655993250717834053/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^12 + 204121427343482910420756548115640914663240685640370143412812337330875235393928958761533962879421133938223530441861086126285867734578493269/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^11 - 80667825274313447357173699680866166034197545124804618841084818942834934043809166981905457099602705589016061505258636947499356024196338769/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^10 - 95140588415975080789645120261192693099304532946517765335661467375441018937736491270197883787284785143192478797405429973114370405121001143/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^9 + 146289996011217183144199390053321673531277887739730340407927578216422179004572621152179202259123039237421535278154446445015893265944921096/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^8 - 59786924754176154060783524961155417598263547205128002279293725710911051758238997059816562489107315151893362875187310065803621857106615724/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^7 - 22907786774721891176416362445631131297599825028589863421645927878137969284542435765153091039825532363975443966934934679769828046610087607/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^6 + 26590704504608312813811380959395757097855924656692022798522563499400782936289175027124734102837152720672057600835817609174037742127865476/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^5 - 5502743640930304640780475855093992141931129220022972761035979731076534053966691015984646895667035791100050621865716743059124962606255319/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y^4 - 5007193963497803880510098865773574559780934391838525933925993812652255144109499842863408999347134632240884468483494268994781126372785419/12346057754668896847168209700644138051042750706315605482065973102716480519215267645680116544575905731285419623054862891042412576503243550*y^3 + 174536320386377249494420991988653449855245692340128991460400667120955496351857075726732125625157950171507805572412365703668855496729738/474848375179572955660315757717082232732413488704446364694845119335249250739048755603081405560611758895593062425187034270862022173201675*y^2 - 476649652166187140719427495284016979168639645249127940683390039339320625395880859763332804483927763403333370788853152949325399750727197/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775*y + 65410705627830606612821371594057232908191860212335553623337417340887532728831229515335219608496410084092369053526963914343477242140119/6173028877334448423584104850322069025521375353157802741032986551358240259607633822840058272287952865642709811527431445521206288251621775 # 4 Loop Invariant 960507656186633293743834817050512721558292314059975356047372135668211763677996327319521838873562214370139145869034504771111334737402944660171937142335677882645161738264890437576617792197451380223/936260312649243684710602294515839597516251190591558418865991915107678992180450778846867308512936665325053632340351952334232342635880375661237528425229308962441217780072577614169939778074865008037000*y^19 + 52848135230428525883787678787124890121669830161576392941799214608448620898227805272064759214556259158365997785026833224413822643542517373668580746955398704709486585623664243974386398499434391833/12483470835323249129474697260211194633550015874554112251546558868102386562406010384624897446839155537667381764538026031123097901811738342149833712336390786165882903734301034855599197040998200107160*y^18 + 337011604460929173181189385492686296724221227043073495500291257939117361593906159756724233553574523434238530626148077401654573970390717277467011500729827238559453628182941673167359854789205973561379/5617561875895462108263613767095037585097507143549350513195951490646073953082704673081203851077619991950321794042111714005394055815282253967425170551375853774647306680435465685019638668449190048222000*y^17 - 97199758317687592141109818040256798725658561050169679432191420831460537891017025685054846528771741017860937229484315150091636189664100329889053951303951578659342658173442281525806222247609765357653/234065078162310921177650573628959899379062797647889604716497978776919748045112694711716827128234166331263408085087988083558085658970093915309382106307327240610304445018144403542484944518716252009250*y^16 + 2806878940922383095660602108878429227068384442667056193385877420844096859205434364420038301574578859201648642778624191866109802432054756511310154038812412996595775262989569669681542757231377179966811/1872520625298487369421204589031679195032502381183116837731983830215357984360901557693734617025873330650107264680703904668464685271760751322475056850458617924882435560145155228339879556149730016074000*y^15 - 12394629600585137660166902305394816168193289802374860036961525136465978703766078922757593300759156023546368741609855662424409563682596239781368364112314698100263932086789314353104090064890527209972717/2808780937947731054131806883547518792548753571774675256597975745323036976541352336540601925538809995975160897021055857002697027907641126983712585275687926887323653340217732842509819334224595024111000*y^14 + 126221064577013885443859764276857886447516968202682149375334210298342897860058647240406254825104323972975334572353805593541040053186647952036026970436169347154843263133719139431425629865422079990928441/5617561875895462108263613767095037585097507143549350513195951490646073953082704673081203851077619991950321794042111714005394055815282253967425170551375853774647306680435465685019638668449190048222000*y^13 - 374821746420859656925827255872942970585166445872329055275523867020694342260292010455725326877024407334161977914766812936918007329630164534956651747821000124476066401976705321832413058640539688066918339/5617561875895462108263613767095037585097507143549350513195951490646073953082704673081203851077619991950321794042111714005394055815282253967425170551375853774647306680435465685019638668449190048222000*y^12 + 548682041221121778793456644513407121710532879365903179049725010458170782818401635054068994647372042470549656649289795878304076166427145719769513718295165009595667632344267514419417875330149692059095147/5617561875895462108263613767095037585097507143549350513195951490646073953082704673081203851077619991950321794042111714005394055815282253967425170551375853774647306680435465685019638668449190048222000*y^11 - 40026469276004584165846292312884928432381236051001262200811508516831953458476850591508217245437954490711213349959173658360425853029591998240375646191434185931467874037127518455187697405400094767178933/624173541766162456473734863010559731677500793727705612577327943405119328120300519231244872341957776883369088226901301556154895090586917107491685616819539308294145186715051742779959852049910005358000*y^10 - 47481410428337882550601816411649870344801991596414388364984042646780684293317122972788746874853852362218938339388199953562442765386697181589679798423747786256205228468442389419505123680219223954545509/5617561875895462108263613767095037585097507143549350513195951490646073953082704673081203851077619991950321794042111714005394055815282253967425170551375853774647306680435465685019638668449190048222000*y^9 + 143973847194514493939004431445224625393031742036336558418888574088201983923824205088222725342653097830311451411924031555425412517670227163464013415893730704774725147291102901237107541501160247563404699/2808780937947731054131806883547518792548753571774675256597975745323036976541352336540601925538809995975160897021055857002697027907641126983712585275687926887323653340217732842509819334224595024111000*y^8 - 106849487320482732219154815788081844808618107058532132956377693188282190943199021241076465998500033666881513631932229440639767421678417077404232235687871848116821887265163471360069442386069684950384131/2808780937947731054131806883547518792548753571774675256597975745323036976541352336540601925538809995975160897021055857002697027907641126983712585275687926887323653340217732842509819334224595024111000*y^7 + 4777363923185273491950170029042388978739713675333997674598603827549176602428921581212181519169356052769889974270622201764045674394896183722841077684682951261925444130936943933506669109244750365907001/624173541766162456473734863010559731677500793727705612577327943405119328120300519231244872341957776883369088226901301556154895090586917107491685616819539308294145186715051742779959852049910005358000*y^6 + 3463127461418357087538094263177150966729308173864611285651063648780314226444754718607489257599781139435441876773192304321020682882314927049608256663628005556373343404469609365656327799341231855175273/936260312649243684710602294515839597516251190591558418865991915107678992180450778846867308512936665325053632340351952334232342635880375661237528425229308962441217780072577614169939778074865008037000*y^5 - 13355096006783676562578363485309212719711870501025037991989181466991667257812461716598755016017370070976268658927497789354412457087173849314036444112517769373970720669755082222870291382911244091304597/5617561875895462108263613767095037585097507143549350513195951490646073953082704673081203851077619991950321794042111714005394055815282253967425170551375853774647306680435465685019638668449190048222000*y^4 + 452630831298731628736105927792084304002707159640830937478592736937149702845700054443565243737632845879954368301033483703985738776300337375089272506717767296395186917048412295035505675531724294650819/936260312649243684710602294515839597516251190591558418865991915107678992180450778846867308512936665325053632340351952334232342635880375661237528425229308962441217780072577614169939778074865008037000*y^3 + 58991909529185520807736368783386522851895562293669772687093117403542406012588641461585222254018494986314875416753398683164048815663152416451050045741776800559852614459663489792260930357973575142119/432120144299650931404893366699618275776731318734565424091996268511236457929438821006246450082893845534640138003239362615799542755021711843648090042413527213434408206187343514232279897573014619094000*y^2 - 229437345451124442974376890922979534315630813128440704967883173282240111973747139130137861764323491051221118528508205197761669175180533304369942051131875280364379699054977756093140013496536150085311/5617561875895462108263613767095037585097507143549350513195951490646073953082704673081203851077619991950321794042111714005394055815282253967425170551375853774647306680435465685019638668449190048222000*y + 1960955063941943641560212416142335146468079959633848941682090762605027062241539410400739188989736696370255544481290606409578096655821818702354719080588635194501424326336564724039016159357555948731/468130156324621842355301147257919798758125595295779209432995957553839496090225389423433654256468332662526816170175976167116171317940187830618764212614654481220608890036288807084969889037432504018500