# Manifold: Census Knot K8_24 # Number of Tetrahedra: 8 # Number Field x^21 + 15*x^20 - 53*x^19 - 9*x^18 + 223*x^17 + 366*x^16 - 1897*x^15 + 1265*x^14 + 3340*x^13 + 253*x^12 - 4460*x^11 + 1356*x^10 + 6033*x^9 + 1196*x^8 - 3486*x^7 - 2400*x^6 - 434*x^5 - 155*x^4 + 5*x^3 + 25*x^2 - 10*x + 1 # Approximate Field Generator 0.154303664780844 + 0.140953416395519*I # Shape Parameters -1144790669849301753557071162160061448/32301183692224607312235063832442234975*y^20 - 16767636433838688535079568101123671143/32301183692224607312235063832442234975*y^19 + 66502565895901094338147029262011003451/32301183692224607312235063832442234975*y^18 - 14670145269284005600723752688348138517/32301183692224607312235063832442234975*y^17 - 246933879064475186390685960915963057096/32301183692224607312235063832442234975*y^16 - 325420183127956558279466571760262003189/32301183692224607312235063832442234975*y^15 + 2267410286130839978085037634812214200117/32301183692224607312235063832442234975*y^14 - 2304552910944657923847899809925443387378/32301183692224607312235063832442234975*y^13 - 2880157606633225919736242930800617405948/32301183692224607312235063832442234975*y^12 + 803872512890375166864219091466879016783/32301183692224607312235063832442234975*y^11 + 4392174739615382270578564717061772551963/32301183692224607312235063832442234975*y^10 - 137263821144318330060294436872812231869/1292047347688984292489402553297689399*y^9 - 5431509918310164827090471340979807265009/32301183692224607312235063832442234975*y^8 + 733741096084315204530749742154094129933/32301183692224607312235063832442234975*y^7 + 3060635400562650079373950661332822258361/32301183692224607312235063832442234975*y^6 + 1084360582295280428458727776913935966186/32301183692224607312235063832442234975*y^5 + 162191787199795879647507360617097511393/32301183692224607312235063832442234975*y^4 + 375797300580118316983993236125990489558/32301183692224607312235063832442234975*y^3 + 93772288635930069446253295982585563318/32301183692224607312235063832442234975*y^2 + 222973529471330741546460536892056244968/32301183692224607312235063832442234975*y + 161100330053444054489344344305850745923/32301183692224607312235063832442234975 -35382237950904230255721120267135908642/156337729070367099391217708949020417279*y^20 - 513190290833165672682856319858657959134/156337729070367099391217708949020417279*y^19 + 2129436615281659989201677192376993290155/156337729070367099391217708949020417279*y^18 - 740906027824982342262240571210124915091/156337729070367099391217708949020417279*y^17 - 681881942171447983674352211483543015204/14212520824578827217383428086274583389*y^16 - 9269675425505291166685209877875250301425/156337729070367099391217708949020417279*y^15 + 71700551789083657027476769043312799451793/156337729070367099391217708949020417279*y^14 - 80313493996417222722296201797365976792561/156337729070367099391217708949020417279*y^13 - 77788681436448363682281929087929915900277/156337729070367099391217708949020417279*y^12 + 28045796741890791213907894916422946303517/156337729070367099391217708949020417279*y^11 + 145316977296792145162158962467372416627200/156337729070367099391217708949020417279*y^10 - 120467033213955971338474048516007576500813/156337729070367099391217708949020417279*y^9 - 153427287534839498687637722880725143023349/156337729070367099391217708949020417279*y^8 + 32059441117990598342172254489430089989499/156337729070367099391217708949020417279*y^7 + 9881117927642995852118917258564881622878/14212520824578827217383428086274583389*y^6 + 30981678875246875014368095067355090205793/156337729070367099391217708949020417279*y^5 - 660004271818144980869811765849662470783/156337729070367099391217708949020417279*y^4 + 6147512061113185811796154657079343508890/156337729070367099391217708949020417279*y^3 - 3435907423191851090886477015894238713414/156337729070367099391217708949020417279*y^2 + 84020014467997326820233744592708239123/14212520824578827217383428086274583389*y + 38102125228555113833024811427321482879/156337729070367099391217708949020417279 1468901420409520858600734993204735808613/41398489067302745715652947210211266033359*y^20 + 21894170878400163491968555339803272623084/41398489067302745715652947210211266033359*y^19 - 80041468401105839686423041700709779602252/41398489067302745715652947210211266033359*y^18 - 7276506088829198831376397696291806971224/41398489067302745715652947210211266033359*y^17 + 334817317541495267946186575623605142988567/41398489067302745715652947210211266033359*y^16 + 504568335732437435177815732470560541012195/41398489067302745715652947210211266033359*y^15 - 2859372896654249588170230793710848736472200/41398489067302745715652947210211266033359*y^14 + 2097481504503283748956364154058083158858903/41398489067302745715652947210211266033359*y^13 + 4933575372405483367022058534638324223260194/41398489067302745715652947210211266033359*y^12 - 320794729654089836986224407293594336476714/41398489067302745715652947210211266033359*y^11 - 6829129811252835948880583542756108479174105/41398489067302745715652947210211266033359*y^10 + 2742034319465672595200688007476972604610418/41398489067302745715652947210211266033359*y^9 + 9083385167768070817663739020373467587110196/41398489067302745715652947210211266033359*y^8 + 519959188280750108853355320337243013034180/41398489067302745715652947210211266033359*y^7 - 5759130734908659427266179731105490345264032/41398489067302745715652947210211266033359*y^6 - 2846326248474487347501400382009457169829434/41398489067302745715652947210211266033359*y^5 + 16131638101184072472658411208151801804989/41398489067302745715652947210211266033359*y^4 - 185899375953198641212051480453613948077913/41398489067302745715652947210211266033359*y^3 - 23774960034804176444601989716276794963181/41398489067302745715652947210211266033359*y^2 + 86869590039596798982541318203943083586422/41398489067302745715652947210211266033359*y + 6140647065561614118712738255730668470953/41398489067302745715652947210211266033359 58498510536875307360204118246856295869705294/597758796831140489921210150447723517702133547*y^20 + 882901120034333814738581929980370730848474269/597758796831140489921210150447723517702133547*y^19 - 3020349532623895155509232158403963549828076195/597758796831140489921210150447723517702133547*y^18 - 833301043001957718423807755178876281055639503/597758796831140489921210150447723517702133547*y^17 + 13061647835550640857258919371074708749624648465/597758796831140489921210150447723517702133547*y^16 + 22638368467223735321332639224362623971403936241/597758796831140489921210150447723517702133547*y^15 - 109270377480841539051698617090047811726637834559/597758796831140489921210150447723517702133547*y^14 + 63228306223183822738414536464435945895783415285/597758796831140489921210150447723517702133547*y^13 + 204582657049675832141898142334143571315691477918/597758796831140489921210150447723517702133547*y^12 + 31504102500874073503879459308303093548608252967/597758796831140489921210150447723517702133547*y^11 - 263906859904455021529717276932197086217693831582/597758796831140489921210150447723517702133547*y^10 + 54809718926062178198409139475403827438666264345/597758796831140489921210150447723517702133547*y^9 + 364759360388501404024416020543102064756710144025/597758796831140489921210150447723517702133547*y^8 + 101089350599376590239726645515455129563108017527/597758796831140489921210150447723517702133547*y^7 - 204516727984213388403355235965686089091900514989/597758796831140489921210150447723517702133547*y^6 - 160941698105910383956334568771202815321126753402/597758796831140489921210150447723517702133547*y^5 - 36090253822442265070753931670131609524425641773/597758796831140489921210150447723517702133547*y^4 - 8916451493369341317501239134400894138965681597/597758796831140489921210150447723517702133547*y^3 + 1707775918518621085227765469611023310027773316/597758796831140489921210150447723517702133547*y^2 + 2500953590443677431089938745965553859511870129/597758796831140489921210150447723517702133547*y + 109685873308902679877724139387681704811079139/597758796831140489921210150447723517702133547 1920635788858769919551349538217415417520852/16697173095841913126290786325355405522405965*y^20 + 29068542256598496290126848701632311284135212/16697173095841913126290786325355405522405965*y^19 - 97908981660776854166752348165854233467620574/16697173095841913126290786325355405522405965*y^18 - 30995564899780052858701705483487106831441177/16697173095841913126290786325355405522405965*y^17 + 426321373201019585357734063379027873459470709/16697173095841913126290786325355405522405965*y^16 + 759301424267631904902143366290166044534203531/16697173095841913126290786325355405522405965*y^15 - 3548322072725288937110200760128274282724354583/16697173095841913126290786325355405522405965*y^14 + 1943670274286108747997999742001513855975211837/16697173095841913126290786325355405522405965*y^13 + 6748530692819427397697730241443860020060605302/16697173095841913126290786325355405522405965*y^12 + 1301537862248236636229441266281397164789364638/16697173095841913126290786325355405522405965*y^11 - 8449095261667008564857770958823323749922721337/16697173095841913126290786325355405522405965*y^10 + 303756433337006631752457298595215242915089089/3339434619168382625258157265071081104481193*y^9 + 11887307061459388890110705794062967499170936701/16697173095841913126290786325355405522405965*y^8 + 3752970384835344663483228317213361159693650793/16697173095841913126290786325355405522405965*y^7 - 6294412833467745628486679076043646007784462204/16697173095841913126290786325355405522405965*y^6 - 5381013311182098175221536458983998773657296474/16697173095841913126290786325355405522405965*y^5 - 1531761905630964318060972743130801603702995437/16697173095841913126290786325355405522405965*y^4 - 510650188282201480932853942088407821397957077/16697173095841913126290786325355405522405965*y^3 - 27220367421555490336760065495706873161372217/16697173095841913126290786325355405522405965*y^2 + 72689245554547905026437419056052612983492093/16697173095841913126290786325355405522405965*y - 13065553120669413895703049567990711144595832/16697173095841913126290786325355405522405965 -1081571591080198933248590054153081706539858/3339434619168382625258157265071081104481193*y^20 - 16456633997116249375022489070027722550108646/3339434619168382625258157265071081104481193*y^19 + 53822901599957430655944078736747143951258125/3339434619168382625258157265071081104481193*y^18 + 21988894868477841704398846171071383021938254/3339434619168382625258157265071081104481193*y^17 - 239295786657480197865505436797266226213202142/3339434619168382625258157265071081104481193*y^16 - 446039673088007686933201748126171781759133456/3339434619168382625258157265071081104481193*y^15 + 1965164979972011290580479983361841098667259333/3339434619168382625258157265071081104481193*y^14 - 934489885724129491202511104775358912225456456/3339434619168382625258157265071081104481193*y^13 - 3907486264593139173107411115853988463014345151/3339434619168382625258157265071081104481193*y^12 - 997092908663121108659629557522076195333945672/3339434619168382625258157265071081104481193*y^11 + 4692488006320414270358706240163402334482706521/3339434619168382625258157265071081104481193*y^10 - 514749053080663203872003464926128433715590466/3339434619168382625258157265071081104481193*y^9 - 6795653814996712893842658716543954273160538265/3339434619168382625258157265071081104481193*y^8 - 2571966635267639960432029326038968264341557793/3339434619168382625258157265071081104481193*y^7 + 3384234519935641316373975700942637312262850791/3339434619168382625258157265071081104481193*y^6 + 3239108158465462315496578468575949887697283153/3339434619168382625258157265071081104481193*y^5 + 1069876453085747528195232618217661428630168542/3339434619168382625258157265071081104481193*y^4 + 392494092879132391468366499647909770861502356/3339434619168382625258157265071081104481193*y^3 + 80442738762666567644820445468405005733981785/3339434619168382625258157265071081104481193*y^2 - 31456940639740218142738813238222745526166662/3339434619168382625258157265071081104481193*y + 11425167409716855460790933147330330801107637/3339434619168382625258157265071081104481193 -1081571591080198933248590054153081706539858/3339434619168382625258157265071081104481193*y^20 - 16456633997116249375022489070027722550108646/3339434619168382625258157265071081104481193*y^19 + 53822901599957430655944078736747143951258125/3339434619168382625258157265071081104481193*y^18 + 21988894868477841704398846171071383021938254/3339434619168382625258157265071081104481193*y^17 - 239295786657480197865505436797266226213202142/3339434619168382625258157265071081104481193*y^16 - 446039673088007686933201748126171781759133456/3339434619168382625258157265071081104481193*y^15 + 1965164979972011290580479983361841098667259333/3339434619168382625258157265071081104481193*y^14 - 934489885724129491202511104775358912225456456/3339434619168382625258157265071081104481193*y^13 - 3907486264593139173107411115853988463014345151/3339434619168382625258157265071081104481193*y^12 - 997092908663121108659629557522076195333945672/3339434619168382625258157265071081104481193*y^11 + 4692488006320414270358706240163402334482706521/3339434619168382625258157265071081104481193*y^10 - 514749053080663203872003464926128433715590466/3339434619168382625258157265071081104481193*y^9 - 6795653814996712893842658716543954273160538265/3339434619168382625258157265071081104481193*y^8 - 2571966635267639960432029326038968264341557793/3339434619168382625258157265071081104481193*y^7 + 3384234519935641316373975700942637312262850791/3339434619168382625258157265071081104481193*y^6 + 3239108158465462315496578468575949887697283153/3339434619168382625258157265071081104481193*y^5 + 1069876453085747528195232618217661428630168542/3339434619168382625258157265071081104481193*y^4 + 392494092879132391468366499647909770861502356/3339434619168382625258157265071081104481193*y^3 + 80442738762666567644820445468405005733981785/3339434619168382625258157265071081104481193*y^2 - 31456940639740218142738813238222745526166662/3339434619168382625258157265071081104481193*y + 11425167409716855460790933147330330801107637/3339434619168382625258157265071081104481193 -1081571591080198933248590054153081706539858/3339434619168382625258157265071081104481193*y^20 - 16456633997116249375022489070027722550108646/3339434619168382625258157265071081104481193*y^19 + 53822901599957430655944078736747143951258125/3339434619168382625258157265071081104481193*y^18 + 21988894868477841704398846171071383021938254/3339434619168382625258157265071081104481193*y^17 - 239295786657480197865505436797266226213202142/3339434619168382625258157265071081104481193*y^16 - 446039673088007686933201748126171781759133456/3339434619168382625258157265071081104481193*y^15 + 1965164979972011290580479983361841098667259333/3339434619168382625258157265071081104481193*y^14 - 934489885724129491202511104775358912225456456/3339434619168382625258157265071081104481193*y^13 - 3907486264593139173107411115853988463014345151/3339434619168382625258157265071081104481193*y^12 - 997092908663121108659629557522076195333945672/3339434619168382625258157265071081104481193*y^11 + 4692488006320414270358706240163402334482706521/3339434619168382625258157265071081104481193*y^10 - 514749053080663203872003464926128433715590466/3339434619168382625258157265071081104481193*y^9 - 6795653814996712893842658716543954273160538265/3339434619168382625258157265071081104481193*y^8 - 2571966635267639960432029326038968264341557793/3339434619168382625258157265071081104481193*y^7 + 3384234519935641316373975700942637312262850791/3339434619168382625258157265071081104481193*y^6 + 3239108158465462315496578468575949887697283153/3339434619168382625258157265071081104481193*y^5 + 1069876453085747528195232618217661428630168542/3339434619168382625258157265071081104481193*y^4 + 392494092879132391468366499647909770861502356/3339434619168382625258157265071081104481193*y^3 + 80442738762666567644820445468405005733981785/3339434619168382625258157265071081104481193*y^2 - 31456940639740218142738813238222745526166662/3339434619168382625258157265071081104481193*y + 14764602028885238086049090412401411905588830/3339434619168382625258157265071081104481193 # A Gluing Matrix {{0,2,2,-2,-4,2,-3,0},{0,1,2,-4,-6,4,-4,-2},{0,0,1,-2,-2,1,-2,0},{0,0,0,0,-1,1,-1,0},{-1,2,4,-5,-8,5,-6,-2},{0,0,0,0,-1,1,0,-1},{-1,2,4,-6,-10,6,-7,-2},{0,0,0,0,0,-1,-1,2}} # B Gluing Matrix {{2,0,0,0,0,0,2,1},{0,1,0,0,0,0,4,0},{0,0,1,0,0,0,2,1},{0,0,0,1,0,0,0,0},{0,0,0,0,1,0,4,0},{0,0,0,0,0,1,1,0},{0,0,0,0,0,0,6,1},{0,0,0,0,0,0,0,2}} # nu Gluing Vector {0, 1, 1, 0, 0, 1, 0, 0} # f Combinatorial flattening {4, -3, 3, 2, -2, -2, 0, -1} # f' Combinatorial flattening {0, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant -10524501571815081011513711933888171346018239/6678869238336765250516314530142162208962386*y^20 - 78240025956524253246820318493630110975717899/3339434619168382625258157265071081104481193*y^19 + 290343292613019446005483438226752155740742345/3339434619168382625258157265071081104481193*y^18 + 26141085171640284517716529063493753873251144/3339434619168382625258157265071081104481193*y^17 - 2469710068566703674312331667799254588672238585/6678869238336765250516314530142162208962386*y^16 - 1776784091280825866331987513291552769020982694/3339434619168382625258157265071081104481193*y^15 + 20911965017003935594263157190602710447001073327/6678869238336765250516314530142162208962386*y^14 - 7590351176938523727020544732803306715052999856/3339434619168382625258157265071081104481193*y^13 - 37276170023306981948804321979314866512178844055/6678869238336765250516314530142162208962386*y^12 + 2379909814743793206399463564585706068904478097/3339434619168382625258157265071081104481193*y^11 + 53403198728757178691547562270928778043103608733/6678869238336765250516314530142162208962386*y^10 - 19023327819581160755724537378464022784224758131/6678869238336765250516314530142162208962386*y^9 - 70435772162232847841417206880515365546859092863/6678869238336765250516314530142162208962386*y^8 - 1478929181599078627715951540667713375864133935/6678869238336765250516314530142162208962386*y^7 + 24879384464425267980388123517885023670879660516/3339434619168382625258157265071081104481193*y^6 + 11863855793768253471746805355239274805958956204/3339434619168382625258157265071081104481193*y^5 - 4869912500246140879840679935130908160439749615/6678869238336765250516314530142162208962386*y^4 - 1888086591849389605198726978726523716804472459/3339434619168382625258157265071081104481193*y^3 - 1140191414646036826806291658550729922116738244/3339434619168382625258157265071081104481193*y^2 - 438046299563370305330821202730089027351336419/3339434619168382625258157265071081104481193*y + 50987143409369568227768436298434296122594481/3339434619168382625258157265071081104481193 # 2 Loop Invariant 51330314473661791095774238747469328755577713501115173481638334640792721543717981521796755571451546712218411/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^20 + 643760277097569295858239746523185949718210779808170426080751685937598182538768962345490929433384035324042269/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^19 - 4613766220062032207963086758457399770247955509272704032200544082789069097296471166343920835392135486451740163/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^18 + 9318309151440007650310301454250478516984999143045532346250962862580086347622175970252330698945454461223047821/53803199561382315827896402412108200495834102554839496556397193080202043019161221125130333978039572796971746968*y^17 + 12471038370415824652074087041923580334133790428967265298085978444801471742307535714043645621564091076543197735/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^16 - 26409423786738689503201436856857091372872904756985936933435764358777232378590420266997728345717813533603199391/107606399122764631655792804824216400991668205109678993112794386160404086038322442250260667956079145593943493936*y^15 - 431733484947805150473197498385229380821798434202840999043278958643493528315650459383414217336863511529914294559/107606399122764631655792804824216400991668205109678993112794386160404086038322442250260667956079145593943493936*y^14 + 907478743433146538094099386876563871686071514010025714288159234442898873705420171010815146922758774558133591479/107606399122764631655792804824216400991668205109678993112794386160404086038322442250260667956079145593943493936*y^13 + 10176873368140331371915291105045140177845315985159404346224896125207154224020958441855150197494643112250116859/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^12 - 1173560666209182283927498819261718247169993709872506491365793097364661165505896622310496176033808212957366273421/107606399122764631655792804824216400991668205109678993112794386160404086038322442250260667956079145593943493936*y^11 - 853504880233011766465532604814293134261465600343956594727235143069761565656969605886310685618731365711190717889/107606399122764631655792804824216400991668205109678993112794386160404086038322442250260667956079145593943493936*y^10 + 116319180613156163041763777542921136774609553770486738173419750387022128144096249598629215313047139285478279213/6725399945172789478487050301513525061979262819354937069549649135025255377395152640641291747254946599621468371*y^9 + 70650448419791312429729091136604478824972611209865783072425573164817499282287917099252088631911929898916797279/17934399853794105275965467470702733498611367518279832185465731026734014339720407041710111326013190932323915656*y^8 - 1005607489664075157034358933675727985556282181858323094359195764382053685500890335024129174695778352570507240437/53803199561382315827896402412108200495834102554839496556397193080202043019161221125130333978039572796971746968*y^7 - 180111087971803402137467165731157244348160438801708874866412462910755621431788773004299106673550254118343867969/17934399853794105275965467470702733498611367518279832185465731026734014339720407041710111326013190932323915656*y^6 + 290965425894424335702391629628147772283737478531841973456468237425038120691130730082548474589716629503813968863/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^5 + 282002947336269304027124570290314030605045944998482678111824816236873818967366820541105703039183673215073685897/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^4 + 62331696581707127315794114691346653439130431435901076508199660780088191468898136430100568486254747036691986035/35868799707588210551930934941405466997222735036559664370931462053468028679440814083420222652026381864647831312*y^3 + 26744368147218304902730040986303362930406398109951544370177963530049621240385266189874256605840394754621943415/26901599780691157913948201206054100247917051277419748278198596540101021509580610562565166989019786398485873484*y^2 + 13543255939168646030710558338638683183949945641933226266363947547220416367039505679046956496854785018654619931/53803199561382315827896402412108200495834102554839496556397193080202043019161221125130333978039572796971746968*y - 15176235738515357991776541299578314628089120152840369202881245794244701198194999141494042348002687782030645755/26901599780691157913948201206054100247917051277419748278198596540101021509580610562565166989019786398485873484 # 3 Loop Invariant 454457570673610570815692275641518128179527521418063957602365536065326167436610118101715645452115931555949502065692586811080200444563709225627/58777187033260054269181374706421435454830410496851658579361166391456355537723739405833268480706457378216608930385702265305196256021754936329632*y^20 + 3436292525782162355132770657428892131789082879826433091955128223164350617155040260678930814772210667020750578904709958434532873311849505191713/29388593516630027134590687353210717727415205248425829289680583195728177768861869702916634240353228689108304465192851132652598128010877468164816*y^19 - 46522305489801714412970819768523120055222094287597743799716826598532055357110925847041945428728342710947880853478597021290493279333429298906213/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^18 - 899789162360297331194344087107658616735754559393129592884418378320809174586048307847116587744291532327922960690471960543388673853776935553829/7347148379157506783647671838302679431853801312106457322420145798932044442215467425729158560088307172277076116298212783163149532002719367041204*y^17 + 203001364149008161318935856725305618521840155759497370116611676111279831386215348377576592357317405426313736858414094060527045894023567704589007/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^16 + 357116462468022891149262427321452118161556079210032940826757208826033364537499820097313383053663185432795792972883031515748849286415927986190219/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^15 - 844244250669820090577928655630322309951418658324550815695119000662421467311583367432621717812528437187146585167726059683681745252389674231341321/58777187033260054269181374706421435454830410496851658579361166391456355537723739405833268480706457378216608930385702265305196256021754936329632*y^14 + 466648956129592990503573566692034543568458202812654705121626030353801445206609340544687738801352081529963457356207311796480729753157381398096391/58777187033260054269181374706421435454830410496851658579361166391456355537723739405833268480706457378216608930385702265305196256021754936329632*y^13 + 3222274604837887420924609549952002584233880309984041986297723793693000312120981152604339462555175827680955503370711286921684666683362710370262443/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^12 + 17280703026581704420756533399921357043809182830569594460264136229619936682576706230341357099238372534579764438490264849617293113985428164473887/3673574189578753391823835919151339715926900656053228661210072899466022221107733712864579280044153586138538058149106391581574766001359683520602*y^11 - 4087937326363043113303795974225250681305911999795737957443655097070319919149097344949012141756943367717535362471073703148418729712126172227911001/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^10 + 389111752171164994018272481956198485669682417767974416264613144464364469646799482375636932867877718443018386204506232257925271185190815921533901/58777187033260054269181374706421435454830410496851658579361166391456355537723739405833268480706457378216608930385702265305196256021754936329632*y^9 + 2867939245484692925734095801566619276173157812212292291911575891091542762490374508944974292654452504798678535789049043497420551041830875100157551/58777187033260054269181374706421435454830410496851658579361166391456355537723739405833268480706457378216608930385702265305196256021754936329632*y^8 + 1672416883256128966844822191342691130281921692528898859894294301209515511335871863712389380115675982742602697275826385082304002811191409030757887/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^7 - 1580794205016068987093814287114852910101036832535135383773568163900658688558227291164436725380353108030526482185653800822757223603174851613971527/58777187033260054269181374706421435454830410496851658579361166391456355537723739405833268480706457378216608930385702265305196256021754936329632*y^6 - 2510334591648050199025909382466354952812880011494825392589715301011819141540086977257613897119046421837464873902973123019289944709162750007276695/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^5 - 565646440874087857903521658999356757410178024566873036003115130972921849829066682783695000416274471341662761135570828797985850327694448919623645/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^4 - 187792914256241911104006406640039794966512286912441472821864946402060838719001615931390826532554820742011984024758785727070784750730827999930475/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^3 - 45687736085071426170872710518885485432964937836092330428668385175985292302164213009788668420915496458310266170952337852927149639770217105728699/117554374066520108538362749412842870909660820993703317158722332782912711075447478811666536961412914756433217860771404530610392512043509872659264*y^2 + 75797835677472636962393766368683680340849396214278816708549784449724488086467898837320539165728087583476458464873194803748056886626697296695/422857460670935642224326436736844859387269140265119845894684650298247162141897405797361643746089621426018769283350376009389901122458668606688*y - 1343618204749028732371011090824748786291079823478292209754801245128777015329043179422225338607038844428554623134766845760286945755727981733009/29388593516630027134590687353210717727415205248425829289680583195728177768861869702916634240353228689108304465192851132652598128010877468164816 # 4 Loop Invariant -9585238841926794177006892587451971750160631863090221721196586942172985763378933727150800902526540439233786250791401845780287793802924480758086592131100437843386913920201955344070310708023913270998471461874001/11363842389804467288330153215995918275659647436681358560433603528612849775431327376583652403556964504942333951441960960481157055134111259841159057074318319644134625404303981847763430321257967818099002391076598784*y^20 - 199803740428203185291235282934769342910280653071480263180061527741585056914679535625760968528487051825214990606616457374165332634595639476894204474816673816465306517987832641272250970885919129136102390211680507/14204802987255584110412691519994897844574559295851698200542004410766062219289159220729565504446205631177917439302451200601446318917639074801448821342897899555168281755379977309704287901572459772623752988845748480*y^19 + 1342880835951135899053408982747323318557184496054052053876232651371537712191681012230023118246442003713160650426666910324437841131232512349598576147826969574887174401841548948523203669009587407841431399007996809/56819211949022336441650766079979591378298237183406792802168017643064248877156636882918262017784822524711669757209804802405785275670556299205795285371591598220673127021519909238817151606289839090495011955382993920*y^18 + 400025185467683247149404978726145851197075546126733165008336412936007037769361713471937573099055259944900134113825489812480262247725243739689191450573926925853197118844894632640525081032945772139340436221125101/4734934329085194703470897173331632614858186431950566066847334803588687406429719740243188501482068543725972479767483733533815439639213024933816273780965966518389427251793325769901429300524153257541250996281916160*y^17 - 3467586588814201490130031253020170338730565644718559244312121451317817870805142250230071611898813078029305162112080571932946572694971032513488106010321946810481241092908396216954638776365835327416256590009437321/18939737316340778813883588693326530459432745727802264267389339214354749625718878960972754005928274174903889919069934934135261758556852099735265095123863866073557709007173303079605717202096613030165003985127664640*y^16 - 17677052433170258450347740467694941924714547671398374120186373375824713207835049990121784935705518199105477445380624918336794160792628057175952165566242853047466454437793206727167172810690275464082506172502807539/28409605974511168220825383039989795689149118591703396401084008821532124438578318441459131008892411262355834878604902401202892637835278149602897642685795799110336563510759954619408575803144919545247505977691496960*y^15 + 63055148441458224310741538676475840956254398461141759759363604775362422911780968399336346958585636177119646376050627605026460529500649055558560300773865188104306718285123637684852222312743098145320972105067857343/56819211949022336441650766079979591378298237183406792802168017643064248877156636882918262017784822524711669757209804802405785275670556299205795285371591598220673127021519909238817151606289839090495011955382993920*y^14 + 23529415585255728186330654029087407060446966693968426508391010060521146478143643470719391195355659995011306317515315557484896254109634409417245962600907727633107478567099089842271346706881457436571264986737081091/14204802987255584110412691519994897844574559295851698200542004410766062219289159220729565504446205631177917439302451200601446318917639074801448821342897899555168281755379977309704287901572459772623752988845748480*y^13 - 27643043587804950746422642910194863238087060018165695715432906492053380936514742030744185702020448767097376208716803917448334454947138372815665055333584710325735674648695074002882721984317637496199532698701927601/5681921194902233644165076607997959137829823718340679280216801764306424887715663688291826201778482252471166975720980480240578527567055629920579528537159159822067312702151990923881715160628983909049501195538299392*y^12 - 5536370803363422168967579308240133163372997562947242832726037012159397563106681757081471126721203440902205105498481634690027059891029269835838606089147917858692413062168747756708416439214887143387694100256797423/1183733582271298675867724293332908153714546607987641516711833700897171851607429935060797125370517135931493119941870933383453859909803256233454068445241491629597356812948331442475357325131038314385312749070479040*y^11 + 17474880046691522943586067831066894054080755521058150186364062290549742589519306712785439933944282461460636320382389954984419627699739035905313072783546519044626907410945868908151528255475006311527756240699731399/4734934329085194703470897173331632614858186431950566066847334803588687406429719740243188501482068543725972479767483733533815439639213024933816273780965966518389427251793325769901429300524153257541250996281916160*y^10 + 295772411240851410989391810427697019798648418311149636405040146247615898416928587818923456295238501399436280069927809141117037904140853913493513545650648913579092268490631457208816360992013906065598371227714988471/56819211949022336441650766079979591378298237183406792802168017643064248877156636882918262017784822524711669757209804802405785275670556299205795285371591598220673127021519909238817151606289839090495011955382993920*y^9 - 427859160678159504911336718097875543272226474723116297910546898823846434547974233426770989204738879595758468073257343014143718551019582672483061969604567330057704034467831062701889058941107496138108557262848674771/56819211949022336441650766079979591378298237183406792802168017643064248877156636882918262017784822524711669757209804802405785275670556299205795285371591598220673127021519909238817151606289839090495011955382993920*y^8 - 264228259565375770408253453322952054203645108531776152075585578883820267265422885126646153027645626229427373489930798868872012766113658394509433915934785937237845974640205827066925750780319382959157643315971899661/28409605974511168220825383039989795689149118591703396401084008821532124438578318441459131008892411262355834878604902401202892637835278149602897642685795799110336563510759954619408575803144919545247505977691496960*y^7 + 11274267829741268581563860611592408015551229455279557915616995395519353393480125026929339414647312488387510211497166181790503200617724504735731189923031538136814113220303929879786034455426573836680891684330848873/6313245772113592937961196231108843486477581909267421422463113071451583208572959653657584668642758058301296639689978311378420586185617366578421698374621288691185903002391101026535239067365537676721667995042554880*y^6 + 201906695321718016131593964834860366079744661093395995148396678675593517794518501729944183295276455808730990789573554154495316251276692471137420225406784157285436838628608221868646654630497897826443780653020365633/28409605974511168220825383039989795689149118591703396401084008821532124438578318441459131008892411262355834878604902401202892637835278149602897642685795799110336563510759954619408575803144919545247505977691496960*y^5 + 194361578408660898795517884031035711199978829149529203108199819198304492090526134446684879596280187066744748097726536689715285481936697063473751727639513319306389302512155470371030231185587964286570832653891881703/56819211949022336441650766079979591378298237183406792802168017643064248877156636882918262017784822524711669757209804802405785275670556299205795285371591598220673127021519909238817151606289839090495011955382993920*y^4 + 4930973225644063776319301368960878713128709110664760997454159199475120304857081407605995837432868956490519900578230736615917028301296994159252368978015580968770201440931158458454431842899003583410500322527789723/14204802987255584110412691519994897844574559295851698200542004410766062219289159220729565504446205631177917439302451200601446318917639074801448821342897899555168281755379977309704287901572459772623752988845748480*y^3 + 293404882436774189543324771282146457029123361574636745061209532720426036678762237188669043386376153147962529051379622363957440317815604835764127919504300917329304333439130118530573745654842602839797499235260709/5681921194902233644165076607997959137829823718340679280216801764306424887715663688291826201778482252471166975720980480240578527567055629920579528537159159822067312702151990923881715160628983909049501195538299392*y^2 - 39864521271429818979854256112419545278926797564971571262408769462208359374803383864962250362807770611505536368951232245990340729026497548739599342964225600087396516389124928533812104615471406142094370059069425/1420480298725558411041269151999489784457455929585169820054200441076606221928915922072956550444620563117791743930245120060144631891763907480144882134289789955516828175537997730970428790157245977262375298884574848*y + 85407943292291643073689766728539268739505971016401757185269333639289253501746391039477174553867779731303125024247963363646819949332176693088112334775323157303845203983421747424365234585365833038406563735235655/5681921194902233644165076607997959137829823718340679280216801764306424887715663688291826201778482252471166975720980480240578527567055629920579528537159159822067312702151990923881715160628983909049501195538299392