# Manifold: Rolfsen Knot 9_27 # Number of Tetrahedra: 12 # Number Field x^24 + 6*x^23 + 9*x^22 - 18*x^21 - 61*x^20 - 6*x^19 + 141*x^18 + 122*x^17 - 123*x^16 - 310*x^15 - 104*x^14 + 344*x^13 + 393*x^12 - 30*x^11 - 410*x^10 - 320*x^9 + 119*x^8 + 307*x^7 + 120*x^6 - 91*x^5 - 112*x^4 - 14*x^3 + 27*x^2 + 10*x + 1 # Approximate Field Generator -0.989874694342250 + 0.132066199545939*I # Shape Parameters 36032796554833315/39580055895628477*y^23 + 239038072746103041/39580055895628477*y^22 + 463163345278718943/39580055895628477*y^21 - 404654837310621618/39580055895628477*y^20 - 2416129620158783285/39580055895628477*y^19 - 1297187635711571283/39580055895628477*y^18 + 4625885722115874692/39580055895628477*y^17 + 6112815012031068227/39580055895628477*y^16 - 2354790975155016241/39580055895628477*y^15 - 11467489245806415503/39580055895628477*y^14 - 7473512269067639795/39580055895628477*y^13 + 9409919207320650949/39580055895628477*y^12 + 16086202430022989927/39580055895628477*y^11 + 3147386618450310472/39580055895628477*y^10 - 12055003038549011311/39580055895628477*y^9 - 13242328923061925526/39580055895628477*y^8 + 854810625064723718/39580055895628477*y^7 + 9933460272753624167/39580055895628477*y^6 + 4912502928244440611/39580055895628477*y^5 - 2108758322466545469/39580055895628477*y^4 - 3599821106100454524/39580055895628477*y^3 - 535848654188287318/39580055895628477*y^2 + 935015437672706613/39580055895628477*y + 189367219535083065/39580055895628477 36032796554833315/39580055895628477*y^23 + 239038072746103041/39580055895628477*y^22 + 463163345278718943/39580055895628477*y^21 - 404654837310621618/39580055895628477*y^20 - 2416129620158783285/39580055895628477*y^19 - 1297187635711571283/39580055895628477*y^18 + 4625885722115874692/39580055895628477*y^17 + 6112815012031068227/39580055895628477*y^16 - 2354790975155016241/39580055895628477*y^15 - 11467489245806415503/39580055895628477*y^14 - 7473512269067639795/39580055895628477*y^13 + 9409919207320650949/39580055895628477*y^12 + 16086202430022989927/39580055895628477*y^11 + 3147386618450310472/39580055895628477*y^10 - 12055003038549011311/39580055895628477*y^9 - 13242328923061925526/39580055895628477*y^8 + 854810625064723718/39580055895628477*y^7 + 9933460272753624167/39580055895628477*y^6 + 4912502928244440611/39580055895628477*y^5 - 2108758322466545469/39580055895628477*y^4 - 3599821106100454524/39580055895628477*y^3 - 535848654188287318/39580055895628477*y^2 + 935015437672706613/39580055895628477*y + 189367219535083065/39580055895628477 16364117530629375/39580055895628477*y^23 + 109032528124701700/39580055895628477*y^22 + 206029526000529132/39580055895628477*y^21 - 227842837589087972/39580055895628477*y^20 - 1212179831751233284/39580055895628477*y^19 - 605944323607779122/39580055895628477*y^18 + 2468271911636964495/39580055895628477*y^17 + 3196495658640660040/39580055895628477*y^16 - 1442360777410606000/39580055895628477*y^15 - 6214094082415402371/39580055895628477*y^14 - 3810100146059562346/39580055895628477*y^13 + 5409368070347053557/39580055895628477*y^12 + 8985076161948199713/39580055895628477*y^11 + 1544278343052444133/39580055895628477*y^10 - 7032644212051097712/39580055895628477*y^9 - 7622535225417758739/39580055895628477*y^8 + 377641316913744944/39580055895628477*y^7 + 5758762399808461113/39580055895628477*y^6 + 3044748977097251901/39580055895628477*y^5 - 1032044041275352946/39580055895628477*y^4 - 2056024366676380102/39580055895628477*y^3 - 420229659636845951/39580055895628477*y^2 + 469645563544615779/39580055895628477*y + 119602274631618313/39580055895628477 -9924939785144133/39580055895628477*y^23 - 105507375050842246/39580055895628477*y^22 - 433869905863242484/39580055895628477*y^21 - 718384335009367033/39580055895628477*y^20 + 291691829195046698/39580055895628477*y^19 + 2767371088064694781/39580055895628477*y^18 + 2665142214070943311/39580055895628477*y^17 - 3171586161832515607/39580055895628477*y^16 - 8063633580290855475/39580055895628477*y^15 - 2632111271741158004/39580055895628477*y^14 + 9867571711720247331/39580055895628477*y^13 + 13926904694698305374/39580055895628477*y^12 + 616484151816010156/39580055895628477*y^11 - 15171970084652655781/39580055895628477*y^10 - 14250131391193871723/39580055895628477*y^9 + 980852378601262148/39580055895628477*y^8 + 13042113467231035847/39580055895628477*y^7 + 9140346328127063298/39580055895628477*y^6 - 1984106718843856829/39580055895628477*y^5 - 5993440126640181337/39580055895628477*y^4 - 2773088548237492972/39580055895628477*y^3 + 965681714854979414/39580055895628477*y^2 + 1233556994844375141/39580055895628477*y + 199292159320227198/39580055895628477 209035898559287005/39580055895628477*y^23 + 1230176065277066416/39580055895628477*y^22 + 1722400722347834355/39580055895628477*y^21 - 4048585296631747759/39580055895628477*y^20 - 12350695342736995348/39580055895628477*y^19 + 588682990844492734/39580055895628477*y^18 + 30155579400637193645/39580055895628477*y^17 + 21393234414554667425/39580055895628477*y^16 - 30317413212590695463/39580055895628477*y^15 - 61602442244111747041/39580055895628477*y^14 - 11890113708850300706/39580055895628477*y^13 + 76616386926109811547/39580055895628477*y^12 + 72112524338041783810/39580055895628477*y^11 - 20164110740677615538/39580055895628477*y^10 - 85810305454332280721/39580055895628477*y^9 - 54162300910321736276/39580055895628477*y^8 + 36254197355887789035/39580055895628477*y^7 + 61455623645150940291/39580055895628477*y^6 + 14658360022603532343/39580055895628477*y^5 - 23221634187128192049/39580055895628477*y^4 - 20644167004886832233/39580055895628477*y^3 + 833061038057850247/39580055895628477*y^2 + 6114133455763620907/39580055895628477*y + 1068001758477217266/39580055895628477 -41900536811253001/39580055895628477*y^23 - 236184514735467595/39580055895628477*y^22 - 316919971080087473/39580055895628477*y^21 + 713385438753356883/39580055895628477*y^20 + 2038341099436455753/39580055895628477*y^19 - 138034199493105929/39580055895628477*y^18 - 4411111145313503693/39580055895628477*y^17 - 3027289294039761535/39580055895628477*y^16 + 3534750357485917669/39580055895628477*y^15 + 8637084056575247651/39580055895628477*y^14 + 2438152361880965296/39580055895628477*y^13 - 9149181400067163110/39580055895628477*y^12 - 9092040586293514324/39580055895628477*y^11 - 95932134444319492/39580055895628477*y^10 + 9169847450515195258/39580055895628477*y^9 + 7079791843971750989/39580055895628477*y^8 - 2441334408246938698/39580055895628477*y^7 - 4950644562250551405/39580055895628477*y^6 - 2182327520107540915/39580055895628477*y^5 + 1370193611651676908/39580055895628477*y^4 + 1363298777573822789/39580055895628477*y^3 - 170904731131909445/39580055895628477*y^2 - 91031555911652943/39580055895628477*y - 12638493398611979/39580055895628477 129864985141479140/39580055895628477*y^23 + 789452621358735667/39580055895628477*y^22 + 1256987957372967424/39580055895628477*y^21 - 2047969718733520213/39580055895628477*y^20 - 7610863342994088987/39580055895628477*y^19 - 1322157338903334706/39580055895628477*y^18 + 16494239382083700628/39580055895628477*y^17 + 14867902522678194453/39580055895628477*y^16 - 13228696243144209458/39580055895628477*y^15 - 35579266198673030319/39580055895628477*y^14 - 13450880294995789849/39580055895628477*y^13 + 37447217072945936492/39580055895628477*y^12 + 43530873614210976494/39580055895628477*y^11 - 1959401799912341158/39580055895628477*y^10 - 42630901307022039455/39580055895628477*y^9 - 33606485610279411792/39580055895628477*y^8 + 13087531291623368316/39580055895628477*y^7 + 31100875823477126310/39580055895628477*y^6 + 10344417045461545963/39580055895628477*y^5 - 10066807158398792224/39580055895628477*y^4 - 10683129525669937520/39580055895628477*y^3 - 137828600184747370/39580055895628477*y^2 + 2986933476801465690/39580055895628477*y + 636092253525716688/39580055895628477 -52210111376620818/39580055895628477*y^23 - 323570242825092725/39580055895628477*y^22 - 557276730479212492/39580055895628477*y^21 + 699425245380049705/39580055895628477*y^20 + 3170856600600562720/39580055895628477*y^19 + 1445776169423831875/39580055895628477*y^18 - 5777815335186597534/39580055895628477*y^17 - 7736337777820833637/39580055895628477*y^16 + 1712795215543288512/39580055895628477*y^15 + 14363179384809824423/39580055895628477*y^14 + 11155946911403141844/39580055895628477*y^13 - 9242483764035384844/39580055895628477*y^12 - 20611876134980203208/39580055895628477*y^11 - 9953532207388064344/39580055895628477*y^10 + 11548545591470790528/39580055895628477*y^9 + 19085933781474257030/39580055895628477*y^8 + 5793138683684628699/39580055895628477*y^7 - 7794031100691023729/39580055895628477*y^6 - 9108599903634970484/39580055895628477*y^5 - 2175152248254935131/39580055895628477*y^4 + 2302186614274919577/39580055895628477*y^3 + 1669829395973788240/39580055895628477*y^2 + 431061119936935599/39580055895628477*y + 39571617978008839/39580055895628477 -39713533692511213/39580055895628477*y^23 - 247636056569460302/39580055895628477*y^22 - 419970142299468082/39580055895628477*y^21 + 583159643287021280/39580055895628477*y^20 + 2492777286729915514/39580055895628477*y^19 + 925125277499880801/39580055895628477*y^18 - 4840043963278397417/39580055895628477*y^17 - 5652149142253785769/39580055895628477*y^16 + 2381719116550843873/39580055895628477*y^15 + 11143868132297144960/39580055895628477*y^14 + 7343467501210626065/39580055895628477*y^13 - 8794150830599758957/39580055895628477*y^12 - 15270907284341332526/39580055895628477*y^11 - 5004666319395392388/39580055895628477*y^10 + 9922932777783884408/39580055895628477*y^9 + 13379872454196479734/39580055895628477*y^8 + 1862180558974365052/39580055895628477*y^7 - 6721377406212860729/39580055895628477*y^6 - 5360404730639237426/39580055895628477*y^5 - 373304989341468224/39580055895628477*y^4 + 1939008535702837554/39580055895628477*y^3 + 662210763413575705/39580055895628477*y^2 - 1862369408190636/39580055895628477*y + 25997489792514992/39580055895628477 23009125966522160/39580055895628477*y^23 + 173456214628589523/39580055895628477*y^22 + 454406339642704884/39580055895628477*y^21 + 163609833844312304/39580055895628477*y^20 - 1382999015858128851/39580055895628477*y^19 - 2149255015245277360/39580055895628477*y^18 + 813000222813115700/39580055895628477*y^17 + 4646283587364572399/39580055895628477*y^16 + 3258974254197787218/39580055895628477*y^15 - 3936930915852365505/39580055895628477*y^14 - 8979436360963449787/39580055895628477*y^13 - 3316208185007760026/39580055895628477*y^12 + 7042531339284982858/39580055895628477*y^11 + 9975261630762560662/39580055895628477*y^10 + 2960705580736286947/39580055895628477*y^9 - 6203239632858712770/39580055895628477*y^8 - 6879331893336424156/39580055895628477*y^7 - 1172540267896059622/39580055895628477*y^6 + 2725903393176268371/39580055895628477*y^5 + 2426446747096756042/39580055895628477*y^4 + 268332320496774824/39580055895628477*y^3 - 486049617860095490/39580055895628477*y^2 - 227891617923215046/39580055895628477*y - 28180251266585940/39580055895628477 35639181447514501/39580055895628477*y^23 + 219966066184282909/39580055895628477*y^22 + 378402175791861744/39580055895628477*y^21 - 456655299744480447/39580055895628477*y^20 - 2060312095034097520/39580055895628477*y^19 - 864007327870744322/39580055895628477*y^18 + 3741051533514462890/39580055895628477*y^17 + 4704090521433481498/39580055895628477*y^16 - 1264004929935123161/39580055895628477*y^15 - 8840476941606983925/39580055895628477*y^14 - 6559424100166024020/39580055895628477*y^13 + 5886695523131996341/39580055895628477*y^12 + 12059865451387566128/39580055895628477*y^11 + 5521653492141859378/39580055895628477*y^10 - 6767157439535593639/39580055895628477*y^9 - 10802872956532947218/39580055895628477*y^8 - 2896196770800819036/39580055895628477*y^7 + 4246687479057255487/39580055895628477*y^6 + 4710093235598112995/39580055895628477*y^5 + 1078974020640756720/39580055895628477*y^4 - 1123513008178689782/39580055895628477*y^3 - 691416945695630081/39580055895628477*y^2 - 263152178903865875/39580055895628477*y - 28171813348966302/39580055895628477 35639181447514501/39580055895628477*y^23 + 219966066184282909/39580055895628477*y^22 + 378402175791861744/39580055895628477*y^21 - 456655299744480447/39580055895628477*y^20 - 2060312095034097520/39580055895628477*y^19 - 864007327870744322/39580055895628477*y^18 + 3741051533514462890/39580055895628477*y^17 + 4704090521433481498/39580055895628477*y^16 - 1264004929935123161/39580055895628477*y^15 - 8840476941606983925/39580055895628477*y^14 - 6559424100166024020/39580055895628477*y^13 + 5886695523131996341/39580055895628477*y^12 + 12059865451387566128/39580055895628477*y^11 + 5521653492141859378/39580055895628477*y^10 - 6767157439535593639/39580055895628477*y^9 - 10802872956532947218/39580055895628477*y^8 - 2896196770800819036/39580055895628477*y^7 + 4246687479057255487/39580055895628477*y^6 + 4710093235598112995/39580055895628477*y^5 + 1078974020640756720/39580055895628477*y^4 - 1123513008178689782/39580055895628477*y^3 - 691416945695630081/39580055895628477*y^2 - 263152178903865875/39580055895628477*y - 28171813348966302/39580055895628477 # A Gluing Matrix {{0,-1,1,0,0,0,0,0,0,0,0,0},{-1,0,1,0,0,0,0,0,0,0,0,0},{1,1,0,1,0,0,0,0,0,0,0,0},{0,0,1,1,0,-1,1,-1,-1,1,1,1},{0,0,0,0,0,-1,1,-1,-1,1,1,1},{0,0,0,-1,-1,-1,1,-1,-1,1,1,1},{0,0,0,1,1,1,0,0,0,0,0,0},{0,0,0,-1,-1,-1,0,-1,-1,1,1,1},{0,0,0,-1,-1,-1,0,-1,1,0,0,0},{0,0,0,1,1,1,0,1,0,0,0,0},{0,0,0,1,1,1,0,1,0,0,0,-1},{0,0,0,1,1,1,0,1,0,0,-1,0}} # B Gluing Matrix {{1,0,0,0,0,0,0,0,0,0,0,0},{0,1,0,0,0,0,0,0,0,0,0,0},{0,0,1,0,0,0,0,0,0,0,0,0},{0,0,0,1,0,0,0,0,0,0,0,0},{0,0,0,0,1,0,0,0,0,0,0,0},{0,0,0,0,0,1,0,0,0,0,0,0},{0,0,0,0,0,0,1,0,0,0,0,0},{0,0,0,0,0,0,0,1,0,0,0,0},{0,0,0,0,0,0,0,0,1,0,0,0},{0,0,0,0,0,0,0,0,0,1,0,0},{0,0,0,0,0,0,0,0,0,0,1,0},{0,0,0,0,0,0,0,0,0,0,0,1}} # nu Gluing Vector {0, 0, 2, 1, 0, -1, 2, -1, -1, 2, 2, 2} # f Combinatorial flattening {1, 1, 1, 0, 1, 1, 0, 0, 1, 2, 0, 0} # f' Combinatorial flattening {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0} # 1 Loop Invariant -502745119305804773/79160111791256954*y^23 - 3153375632333090231/79160111791256954*y^22 - 2764409662329881677/39580055895628477*y^21 + 6374636202174146039/79160111791256954*y^20 + 29187063105270876643/79160111791256954*y^19 + 9754933967107006809/79160111791256954*y^18 - 57759213893296062553/79160111791256954*y^17 - 61236115747355314255/79160111791256954*y^16 + 35819966378284671889/79160111791256954*y^15 + 63726732232943836439/39580055895628477*y^14 + 34030172622708580077/39580055895628477*y^13 - 57566931724318382114/39580055895628477*y^12 - 79586128104518710479/39580055895628477*y^11 - 9924732143935259302/39580055895628477*y^10 + 64123403689156101487/39580055895628477*y^9 + 63675076035661893631/39580055895628477*y^8 - 21734576337590901383/79160111791256954*y^7 - 90477747587429746517/79160111791256954*y^6 - 20228605834734285916/39580055895628477*y^5 + 19973379905639435799/79160111791256954*y^4 + 28876309051038917493/79160111791256954*y^3 + 180696010358261038/39580055895628477*y^2 - 5012966190123507845/79160111791256954*y - 264229023142709981/79160111791256954 # 2 Loop Invariant 18598443943443198322361192197350277236650182755753315119491911120397209366994571/65029491326030329849724005813484982916508355610232258908860633358052436726149262*y^23 + 38685898756645541130273824766716453763283556706613100255909631142159903638353309/21676497108676776616574668604494994305502785203410752969620211119350812242049754*y^22 + 389921680882702427883085017734846653940760658563268318121537504702149785909056029/130058982652060659699448011626969965833016711220464517817721266716104873452298524*y^21 - 278506067140083815562578143479442275077685795088323330296719822726855544655777047/65029491326030329849724005813484982916508355610232258908860633358052436726149262*y^20 - 755470528094413050626666740610819245160291507911616193332366753333957790374731039/43352994217353553233149337208989988611005570406821505939240422238701624484099508*y^19 - 244206960949746775476588297772116717207608535805259033434534789911358608697767839/65029491326030329849724005813484982916508355610232258908860633358052436726149262*y^18 + 4989363074382192284691520883501266304751201570750102366380202101267504127070301405/130058982652060659699448011626969965833016711220464517817721266716104873452298524*y^17 + 4616222596260204743968594783022071764776856603741718271172102975572713158528942353/130058982652060659699448011626969965833016711220464517817721266716104873452298524*y^16 - 346776580063273210490684700849937295849917331408213716091464205059641055107826533/10838248554338388308287334302247497152751392601705376484810105559675406121024877*y^15 - 10844031748699794333979440380287875800699072394207744222610493541318585167630284829/130058982652060659699448011626969965833016711220464517817721266716104873452298524*y^14 - 4013160291185849136231756171928751344055391191414670247736881364361794421192432203/130058982652060659699448011626969965833016711220464517817721266716104873452298524*y^13 + 11753574492828488241703187179536059728725513044779683056101764608940544874689075709/130058982652060659699448011626969965833016711220464517817721266716104873452298524*y^12 + 1120956740557696539476637934619558998061343797574936924982521551877120550017073614/10838248554338388308287334302247497152751392601705376484810105559675406121024877*y^11 - 1489146908359791107803716833511644826115361509709609674102197729625545017540606309/130058982652060659699448011626969965833016711220464517817721266716104873452298524*y^10 - 621489247534433488641549799470960865107777293433880134564681198457597186309659331/5911771938730029986338545983044089356046214146384750809896421214368403338740842*y^9 - 2569871069407830969900329432428890939962884838134515598302876433401144647508538256/32514745663015164924862002906742491458254177805116129454430316679026218363074631*y^8 + 2403163064602698999076562363836941286386692003701627065999782364489179509332029909/65029491326030329849724005813484982916508355610232258908860633358052436726149262*y^7 + 2605080852492544113296347192660546285421048816118595111639102309089333796148091616/32514745663015164924862002906742491458254177805116129454430316679026218363074631*y^6 + 247648956564244430446183126307484202613328644926830230316117729103188515358615634/10838248554338388308287334302247497152751392601705376484810105559675406121024877*y^5 - 163784879374013098268461442743982865727191605172622126638550354387211794020092209/5911771938730029986338545983044089356046214146384750809896421214368403338740842*y^4 - 904426225533145653342222047855681150527655068795755459909645652049229815017810937/32514745663015164924862002906742491458254177805116129454430316679026218363074631*y^3 + 27660726661643784610097099531713150518975318893809631073118074034056160582423/358289208407880605232639150487520567033103887659681867266449770567782020529748*y^2 + 360094077623526966564613075866545524461056560875554575312965030635219680844932139/43352994217353553233149337208989988611005570406821505939240422238701624484099508*y + 189747091935850182374934813041493615240011657830187382797624346337095096793057549/130058982652060659699448011626969965833016711220464517817721266716104873452298524 # 3 Loop Invariant -543909611663243620109584310009450509822068419042973632168681728459869992714035081125978255308340427356647883/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^23 - 3466342547096959529690311716917307178629323065975482151368930853409730632967993034709212897220833370793300629/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^22 - 3096816796356026247008812329436289250963396962297083265840637679348738102950892680271395658594324493708038867/32609021616001983326773355278034784384081974118871511532132789110809269757271066536765905515889506256386346014*y^21 - 67646883302148485728867642382229517933278637859418525297719873982188931633336572943856904644853018502479559347/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^20 + 18284166651061312329677546493562819783050996292781334179723733549575244154916656478991296727170839028450226883/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^19 + 292067028280349079090135149472247528968007885292196303230159152209174936812266908216722159590305355042716334289/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^18 + 2499335257758641103687897381671613992573736968575940847555690210276932715454802364655954476730713274481451757/2964456510545634847888486843457707671280179465351955593830253555528115432479187866978718683262682386944213274*y^17 - 210294765787497004044614667265004165879557793378402614899758473127206613263635791796192964937817196487373484201/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^16 - 983689955426927623930170244375315916054405585413887341867679617523571064011653704224011653195715247308460875099/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^15 - 6293022437945021064566669697083980000075632216179522755385844367955132270014146187506070954449928056863054774/16304510808000991663386677639017392192040987059435755766066394555404634878635533268382952757944753128193173007*y^14 + 675149538624836639996885818016911332466019172633768869123113394613726315515890081883673483771518526812918259371/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^13 + 1577676183473908618695408008914740595343018431470396814391153628174991098767771793330185105607913571034866873777/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^12 - 207962333698831739271825316354672701160897799312823557401691713933055045175786277804060332355082997917211124415/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^11 - 2263349430988045310432393425041897721224163004623826506340117412308677199486910842749216421533088738410538180281/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^10 - 705447593443818822610646072618904896149395058975068571652886878880716803936719063795228296038728315415829163419/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^9 + 432114840495555879129674015543892200813430828113327732936285465881005177705902882503839690128998130112162590087/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^8 + 2102519332770329394238934397836586827412439477325745067642859681928400367300131903730119243669958288222422345283/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^7 + 451609473048195373523652760665269251040632912596553775596084313633005956846378454851198677262233023477893822569/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^6 - 438935223532990976626065328173422424964110318621630579230425500189582023746590953318652409801417327744809980574/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^5 - 1053638735420546635639157462192663835907998350567453191110746050938801331868737942869836688781215222066327250795/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^4 - 259693274890581814990203579483766013527661081675279890611229738439544037453113460875003745888610240526420218935/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154*y^3 + 164465501642303238987193695794637683934579634588500125514276947014504026161423614881160624175957694079023320516/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y^2 + 118698557834937461505560813679509930352086449582689540936251999322324020795122490814043035966875320958345730724/179349618888010908297253454029191314112450857653793313426730340109450983664990865952212480337392284410124903077*y + 7725521383887501505286190277920667021434115934730040227013901998380379052579684932112766975173439529895669913/358699237776021816594506908058382628224901715307586626853460680218901967329981731904424960674784568820249806154 # 4 Loop Invariant -2677388956040456632506163509170853145131587929038686182978779827132441905280539033328741401811212959134588220282124899920214211250308377669734567850520637967358936001288031019/35360276953301330653440371046811212646419026554474462236354736250326412446378075693658400521016643456931205412041281581613333318529951128075511191797863812377140717030014023440*y^23 - 990464368722670570342771896215315124565325295122317768224974600149984254955845204818422431563780423139491492193623586340249231724235036158320503851459867095278839887905392123/2210017309581333165840023190425700790401189159654653889772171015645400777898629730853650032563540216058200338252580098850833332408121945504719449487366488273571294814375876465*y^22 - 2922683574460106288523616907788192014237298467125139562245751468775024028476201529928218199226189551406072978362669912705593038291714036747801201674185802089781788925962527297/4420034619162666331680046380851401580802378319309307779544342031290801555797259461707300065127080432116400676505160197701666664816243891009438898974732976547142589628751752930*y^21 + 46283414746483309229299897214507703415774553928948530101496391097691835544100388641145630704867435579395672058167293960069061086833842331566706915364095364945899833783690208671/35360276953301330653440371046811212646419026554474462236354736250326412446378075693658400521016643456931205412041281581613333318529951128075511191797863812377140717030014023440*y^20 + 7583016332427029809095089434105716361386259743046492597300840523234932794200584643236728709279385700240928479686962238580962121466937036203984363925849569738126602750682238623/1768013847665066532672018552340560632320951327723723111817736812516320622318903784682920026050832172846560270602064079080666665926497556403775559589893190618857035851500701172*y^19 + 2442421963383333705916687643655543008640824104201391622072353413728811293562983263596943838588159616778578602424539600459297249296020170115675950467212618272393973719269510681/11786758984433776884480123682270404215473008851491487412118245416775470815459358564552800173672214485643735137347093860537777772843317042691837063932621270792380239010004674480*y^18 - 171982271310190166336490794724042975683258909168446202976105173959119084172121067989059638991179673817042598783576308750825359080224788541601452745715992077570033301264101835949/17680138476650665326720185523405606323209513277237231118177368125163206223189037846829200260508321728465602706020640790806666659264975564037755595898931906188570358515007011720*y^17 - 90680526212384800593292312101492994716474889046757791809778853307872760090680256284257900768562497069071567361196096315090608282311712527891628255545631586593067269804809635637/11786758984433776884480123682270404215473008851491487412118245416775470815459358564552800173672214485643735137347093860537777772843317042691837063932621270792380239010004674480*y^16 + 150372309377405007877445971913911049527115869396928956222315352858492872611851606640027059070963589710491425926254156496123930948681264122426259727213590791326433123069496193351/17680138476650665326720185523405606323209513277237231118177368125163206223189037846829200260508321728465602706020640790806666659264975564037755595898931906188570358515007011720*y^15 + 39766998505473073583116866384524750407547496216947802070194160008749168751555827600055032647568510366129672626743950390659331337926020393392095422394735804767976833015189253399/1964459830738962814080020613711734035912168141915247902019707569462578469243226427425466695612035747607289189557848976756296295473886173781972843988770211798730039835000779080*y^14 + 21603746058738062748310283272293620452811660357824403860181246849159351492964653321006033242650598421552613256298850107418040412240218552488278244605016751055278167224813315149/3536027695330133065344037104681121264641902655447446223635473625032641244637807569365840052101664345693120541204128158161333331852995112807551119179786381237714071703001402344*y^13 - 134465706139857613978837920286002245179715951556046475279361754107339957053713741095651476287116524948941476119540406426636977825501742571998512773479393373830935700167216298899/5893379492216888442240061841135202107736504425745743706059122708387735407729679282276400086836107242821867568673546930268888886421658521345918531966310635396190119505002337240*y^12 - 850954895122611883640068087404071260499341618711783717049689190420160666619798069270532392737871774413125302480740137510026681621219853941992901950856049690422874229859157461309/35360276953301330653440371046811212646419026554474462236354736250326412446378075693658400521016643456931205412041281581613333318529951128075511191797863812377140717030014023440*y^11 + 11467887411422097929547800551112102451931099506197104724714183987510794325502113945562808645440849843384430006216782158788211467025203494352419199377416310979862493768404279711/3928919661477925628160041227423468071824336283830495804039415138925156938486452854850933391224071495214578379115697953512592590947772347563945687977540423597460079670001558160*y^10 + 9066302622518153790161979800966177200322123612892495991304848576712660058439246796703756516333526386731654068452825273947718342864667255205794724820765576535877088918450579411/357174514679811420741821929765769824711303298530045073094492285356832448953313895895539399202188317746779852646881632137508417358888395233085971634321856690678189060909232560*y^9 + 82262356888592766530723161503169779001171433010543227390818321435751371862420550601951359933006049563312837821860718819394547896954051724862624579553492149337313387336691807009/4420034619162666331680046380851401580802378319309307779544342031290801555797259461707300065127080432116400676505160197701666664816243891009438898974732976547142589628751752930*y^8 - 306281564332520722702960052120409495509767450316923417103389666054603688185375129555763642019648667833767229936326015649556010267465201814434079458866427986179045643155514572593/35360276953301330653440371046811212646419026554474462236354736250326412446378075693658400521016643456931205412041281581613333318529951128075511191797863812377140717030014023440*y^7 - 317105497937713734205465724146475016340833164059645426310361506493723563414270409084104021999799305110885017395910607270519348053275957124763507409692250340853099099689244616189/17680138476650665326720185523405606323209513277237231118177368125163206223189037846829200260508321728465602706020640790806666659264975564037755595898931906188570358515007011720*y^6 - 21831853252816505608126634610946268273983456466936820544217714570499088607183919615545949624252712882717256817478835926020492720116235696098724432348124959315880835122386206139/3928919661477925628160041227423468071824336283830495804039415138925156938486452854850933391224071495214578379115697953512592590947772347563945687977540423597460079670001558160*y^5 + 2135264708436020607287484349583948487821075632317952750700328165958635131837017580486712295514587518098879970808563975356721565999599061677025383925327861565175895160228389413/357174514679811420741821929765769824711303298530045073094492285356832448953313895895539399202188317746779852646881632137508417358888395233085971634321856690678189060909232560*y^4 + 213434501976817685081921678137984531098039372965323945801866297170421358487321382328833523578281367113457011086377100914833165473014360265299918920868911660102562035530288498163/35360276953301330653440371046811212646419026554474462236354736250326412446378075693658400521016643456931205412041281581613333318529951128075511191797863812377140717030014023440*y^3 - 126845816183192889440608472750291005714197610522495950846360677630832075283934394538887124282848504503883933480832676133387788263000895735108964131862103896192863120706189667/3214570632118302786676397367891928422401729686770405657850430568211492040579825063059854592819694859721018673821934689237575756229995557097773744708896710216103701548183093040*y^2 - 3225796678934443823184264295585532508777157659648983450071807265019458387308030384821088370203756542617660759784288944200615663387313242834568859074822853046928374321794599757/1964459830738962814080020613711734035912168141915247902019707569462578469243226427425466695612035747607289189557848976756296295473886173781972843988770211798730039835000779080*y - 3507713044022654743850254993537985384095659934590527355870160968898179438015246303432547143494934466693104652974314663891383460240485684379715197600201709380756883080588586137/11786758984433776884480123682270404215473008851491487412118245416775470815459358564552800173672214485643735137347093860537777772843317042691837063932621270792380239010004674480