# Manifold: Census Knot K7_42 # Number of Tetrahedra: 7 # Number Field x^33 + 23*x^32 + 251*x^31 + 1717*x^30 + 8162*x^29 + 28090*x^28 + 69804*x^27 + 116093*x^26 + 82283*x^25 - 179100*x^24 - 722443*x^23 - 1230330*x^22 - 963122*x^21 + 631113*x^20 + 2909314*x^19 + 3895741*x^18 + 1952609*x^17 - 2032825*x^16 - 4794186*x^15 - 3843662*x^14 - 250409*x^13 + 2534433*x^12 + 2481928*x^11 + 697157*x^10 - 612709*x^9 - 672762*x^8 - 198304*x^7 + 73176*x^6 + 72870*x^5 + 15124*x^4 - 4115*x^3 - 2314*x^2 - 255*x + 13 # Approximate Field Generator -0.538978175849714 + 1.30415491177319*I # Shape Parameters -616446783531391496219083615075061501117121289400250129900626/125318034396309804474061115747737000249675208725338237569067*y^32 - 13699048809556555069902630630650953174966172696500747663352251/125318034396309804474061115747737000249675208725338237569067*y^31 - 144064480908398328135453954806774914571930401564028143054255256/125318034396309804474061115747737000249675208725338237569067*y^30 - 315380101081274239256044211647736622397525291276461640136990548/41772678132103268158020371915912333416558402908446079189689*y^29 - 4292815482957241427099198779415570928137745131257936291379469604/125318034396309804474061115747737000249675208725338237569067*y^28 - 13959116384284387691803836771194790369761379182357537067954772532/125318034396309804474061115747737000249675208725338237569067*y^27 - 32093084632193987935793191678250904586599235822179811686362787899/125318034396309804474061115747737000249675208725338237569067*y^26 - 15450713985134769713793974095519618730112171621216338031345762250/41772678132103268158020371915912333416558402908446079189689*y^25 - 4709678191179477084907706854896237650815386410169359527995714155/41772678132103268158020371915912333416558402908446079189689*y^24 + 122065941917719984620557062734791893185539161030617142243911758027/125318034396309804474061115747737000249675208725338237569067*y^23 + 116754427456787816375983400702908185770156402455593172800657755835/41772678132103268158020371915912333416558402908446079189689*y^22 + 161100430873926327828222798132975906557531991196588785014254493634/41772678132103268158020371915912333416558402908446079189689*y^21 + 211617400485704602809996536192557116250974202344595778944041290362/125318034396309804474061115747737000249675208725338237569067*y^20 - 186807271329950906288042878083589941453589399279325920240647961479/41772678132103268158020371915912333416558402908446079189689*y^19 - 452446065710859828980561077005788161583066044920880794533446580164/41772678132103268158020371915912333416558402908446079189689*y^18 - 1332033247029769653327921057943545912986407861375624345974219836608/125318034396309804474061115747737000249675208725338237569067*y^17 - 144647036887747033356205580480870822226824651138853418906838153018/125318034396309804474061115747737000249675208725338237569067*y^16 + 1380484833821800951080365426519686436081305140196491643152298448086/125318034396309804474061115747737000249675208725338237569067*y^15 + 624032831356047720903860459541707330783539338261496358215074421214/41772678132103268158020371915912333416558402908446079189689*y^14 + 294483587315988216807233791823626490695533114361171939489255362605/41772678132103268158020371915912333416558402908446079189689*y^13 - 558552616408474127355348233876646633391660432942238837360545287547/125318034396309804474061115747737000249675208725338237569067*y^12 - 1128984712363144460344363899300010560767964845352888141414713200276/125318034396309804474061115747737000249675208725338237569067*y^11 - 210881495782706497600724823838660481262006897297956481966610275312/41772678132103268158020371915912333416558402908446079189689*y^10 + 80190831513767787623998142451620999100193680814063290326333118667/125318034396309804474061115747737000249675208725338237569067*y^9 + 106126035212531740791649672912921444976636421095851053246151818002/41772678132103268158020371915912333416558402908446079189689*y^8 + 160302982920666282226944861605449285235128982035645997827708009153/125318034396309804474061115747737000249675208725338237569067*y^7 - 8017538485195290264010159152927985927754858781842494703164036991/125318034396309804474061115747737000249675208725338237569067*y^6 - 13189147681929942794983070537873613080171155461688606138868340438/41772678132103268158020371915912333416558402908446079189689*y^5 - 12878113921337743624315723026369895855663698728898557555436070072/125318034396309804474061115747737000249675208725338237569067*y^4 + 1360904088951288077649492068153707330601067827634008118209032688/125318034396309804474061115747737000249675208725338237569067*y^3 + 1481704753727000862643757843826608628903092118420940910443701595/125318034396309804474061115747737000249675208725338237569067*y^2 + 64713819979378137277803852695640250558380645266937152618992005/41772678132103268158020371915912333416558402908446079189689*y - 9227571711629452288564368008211121980032812140727377070013867/125318034396309804474061115747737000249675208725338237569067 -1637811205359310191001039163970881404980587471774441156725148/877226240774168631318427810234159001747726461077367662983469*y^32 - 11995742685648824940424223356002649351455802833090058603411684/292408746924722877106142603411386333915908820359122554327823*y^31 - 373833461799220990355171898015853202922335942432574605377878469/877226240774168631318427810234159001747726461077367662983469*y^30 - 807264204364670977777092381705122923662669506476177929644453577/292408746924722877106142603411386333915908820359122554327823*y^29 - 10815062924129846161101648470123781227652481164165079373026184014/877226240774168631318427810234159001747726461077367662983469*y^28 - 11493243910365461778309391361185767365694431064010975357254290121/292408746924722877106142603411386333915908820359122554327823*y^27 - 25689583871198347301275008062372914197693795485610556846277144325/292408746924722877106142603411386333915908820359122554327823*y^26 - 105204163607784337853364854836676713392591566012524796483989429027/877226240774168631318427810234159001747726461077367662983469*y^25 - 14117332936378046700984688061701238053061631562013728446284231864/877226240774168631318427810234159001747726461077367662983469*y^24 + 324095988572042452160222543979151950573679292053150592035697279698/877226240774168631318427810234159001747726461077367662983469*y^23 + 283206052246818868753104293341351088581492864397841279792927900554/292408746924722877106142603411386333915908820359122554327823*y^22 + 361527720504681775194582639308320162642542611926506116943215815584/292408746924722877106142603411386333915908820359122554327823*y^21 + 322892148164148839973971410618794025962406119404564338743835356871/877226240774168631318427810234159001747726461077367662983469*y^20 - 1531462791468056510406282089804467719236299394829260653386357739715/877226240774168631318427810234159001747726461077367662983469*y^19 - 3216218509136586099057718992874616221901673550618757429982818651734/877226240774168631318427810234159001747726461077367662983469*y^18 - 932083134440229969705775244485439684097811103311522988534604877632/292408746924722877106142603411386333915908820359122554327823*y^17 + 197207732132143023710531340145437783370319158802543086208069946071/877226240774168631318427810234159001747726461077367662983469*y^16 + 3525227150659835824153613944318284174737053256393893514965310900089/877226240774168631318427810234159001747726461077367662983469*y^15 + 4112557974259610825715499372788876674641833107444327797814537211139/877226240774168631318427810234159001747726461077367662983469*y^14 + 1452770873180905498252014333459480584628651321148560826630455458420/877226240774168631318427810234159001747726461077367662983469*y^13 - 568620582569894280481072124829130808345976262897016278142041088097/292408746924722877106142603411386333915908820359122554327823*y^12 - 844965265760684984186323647509113489868449780449525899603861899487/292408746924722877106142603411386333915908820359122554327823*y^11 - 1116471284916060059460168647216191504514877334996400754675271770773/877226240774168631318427810234159001747726461077367662983469*y^10 + 19274401993961933405223791673019979890871455401344171182493198574/41772678132103268158020371915912333416558402908446079189689*y^9 + 713003933589267503695958512301853530471092079281392357796051012220/877226240774168631318427810234159001747726461077367662983469*y^8 + 266216950864532141603073473071115092093449916191876295487763646325/877226240774168631318427810234159001747726461077367662983469*y^7 - 63805935422762057960792586272847617877832669964210495133086439137/877226240774168631318427810234159001747726461077367662983469*y^6 - 82217461735620816743700611702614598400608337956424592477580936330/877226240774168631318427810234159001747726461077367662983469*y^5 - 16732466755834321149206258394411206437724965198419014845657960553/877226240774168631318427810234159001747726461077367662983469*y^4 + 5246449133988914652482485598489403145233343655469334915037633573/877226240774168631318427810234159001747726461077367662983469*y^3 + 111933206738078973922724259386879604289088366507259179098558914/41772678132103268158020371915912333416558402908446079189689*y^2 + 147984428533329808889085225208280492000147414035528572502649948/877226240774168631318427810234159001747726461077367662983469*y - 9797236710141297022593025934584876853411311645147261564583626/877226240774168631318427810234159001747726461077367662983469 -12421805191113114957890371696113273302088223335174397122097/292408746924722877106142603411386333915908820359122554327823*y^32 - 281553896646205655215300979586824081312954955049652293182332/292408746924722877106142603411386333915908820359122554327823*y^31 - 3018831998174242945980203885643006905313689348425925333920159/292408746924722877106142603411386333915908820359122554327823*y^30 - 20202190990385719475152498274188951754037039729655183956859025/292408746924722877106142603411386333915908820359122554327823*y^29 - 93326334049590035023239884088420926928093719404241242954485448/292408746924722877106142603411386333915908820359122554327823*y^28 - 308580172501992772340974993723585345824765313498353812106549437/292408746924722877106142603411386333915908820359122554327823*y^27 - 719380609334572248416036127037836555081857074784799103854216715/292408746924722877106142603411386333915908820359122554327823*y^26 - 1044036112737796849415074572374049779753436276908594440036160022/292408746924722877106142603411386333915908820359122554327823*y^25 - 267679854719995646172912830976487447179140910274253215487678067/292408746924722877106142603411386333915908820359122554327823*y^24 + 3028104486238385659991119837407570070246297741995464122801108017/292408746924722877106142603411386333915908820359122554327823*y^23 + 8581159847454540018855562084302624821190896709593939969071574489/292408746924722877106142603411386333915908820359122554327823*y^22 + 11640234826269428132169377795778958566524107159807117183011222209/292408746924722877106142603411386333915908820359122554327823*y^21 + 4091477581672904967387781694056747258677819969257307691999585491/292408746924722877106142603411386333915908820359122554327823*y^20 - 16660370379703834404423044165792598098259644676981497063948172056/292408746924722877106142603411386333915908820359122554327823*y^19 - 37472341516512767392361501033487915341162598220179267128018383664/292408746924722877106142603411386333915908820359122554327823*y^18 - 34256153888951585636972084823269581248415276586619296777629845130/292408746924722877106142603411386333915908820359122554327823*y^17 + 2792152814019066247701569825736089925741582173127833900525581230/292408746924722877106142603411386333915908820359122554327823*y^16 + 48357605876223184216065968604812550391461672668572626791448319886/292408746924722877106142603411386333915908820359122554327823*y^15 + 59227788020541022013424881065945722874002778083999282657813919609/292408746924722877106142603411386333915908820359122554327823*y^14 + 21207657109889545299786294576943074826256981290281856888746905850/292408746924722877106142603411386333915908820359122554327823*y^13 - 30038402508158420038763274833720393598336446105022355329378211294/292408746924722877106142603411386333915908820359122554327823*y^12 - 46896547730297792420618003781119197046276491432808867091131657028/292408746924722877106142603411386333915908820359122554327823*y^11 - 22267690237776241342764171320452846571504859557916897195104613860/292408746924722877106142603411386333915908820359122554327823*y^10 + 1360048937522532881286014647643583642483375562083853848570297642/41772678132103268158020371915912333416558402908446079189689*y^9 + 18681081108179674945036448414222146622811509552825103624551068022/292408746924722877106142603411386333915908820359122554327823*y^8 + 8547515840231550675725919071241156824321903602095221999719885336/292408746924722877106142603411386333915908820359122554327823*y^7 - 1640495700504135310594223268058108469582419827947750423347938665/292408746924722877106142603411386333915908820359122554327823*y^6 - 3423120916019286893880044328053512617522724457356606499619895887/292408746924722877106142603411386333915908820359122554327823*y^5 - 1188200694447990108895846834166260673150030889092051206050164204/292408746924722877106142603411386333915908820359122554327823*y^4 + 151202315856203786093884813819066717779190186602493531603564899/292408746924722877106142603411386333915908820359122554327823*y^3 + 27926808718546998709722296470609617680134430769703021682421380/41772678132103268158020371915912333416558402908446079189689*y^2 + 32700834264599589137275717877861159075304992248698063270896652/292408746924722877106142603411386333915908820359122554327823*y - 2163945251264414983735440291337576306425950593604387878241142/292408746924722877106142603411386333915908820359122554327823 1/13*y^32 + 23/13*y^31 + 251/13*y^30 + 1717/13*y^29 + 8162/13*y^28 + 28090/13*y^27 + 69804/13*y^26 + 116093/13*y^25 + 82283/13*y^24 - 179100/13*y^23 - 722443/13*y^22 - 1230330/13*y^21 - 963122/13*y^20 + 631113/13*y^19 + 2909314/13*y^18 + 3895741/13*y^17 + 1952609/13*y^16 - 2032825/13*y^15 - 4794186/13*y^14 - 3843662/13*y^13 - 250409/13*y^12 + 2534433/13*y^11 + 2481928/13*y^10 + 697157/13*y^9 - 612709/13*y^8 - 672762/13*y^7 - 198304/13*y^6 + 73176/13*y^5 + 72870/13*y^4 + 15124/13*y^3 - 4115/13*y^2 - 178*y - 255/13 y + 1 -72763810890129151722906245991242296639953619748310069495971129/148251234690834498692814299929572871295365771922075135044206261*y^32 - 1676252245600882810993471615931711589326514856230128528229720190/148251234690834498692814299929572871295365771922075135044206261*y^31 - 18322027321656550118245313085244385306875428795079789223200613204/148251234690834498692814299929572871295365771922075135044206261*y^30 - 41843937116718251911057921001301805981852365405832761032932191449/49417078230278166230938099976524290431788590640691711681402087*y^29 - 597679233366916017577067805441225031726885221885418572834985442986/148251234690834498692814299929572871295365771922075135044206261*y^28 - 2060303140911265097568472961226578513028258053467264149951769383536/148251234690834498692814299929572871295365771922075135044206261*y^27 - 5128890103382253756725494748676007557768862525610847614440956787967/148251234690834498692814299929572871295365771922075135044206261*y^26 - 2849551911141490289725725877721789045001801936054545905530806760970/49417078230278166230938099976524290431788590640691711681402087*y^25 - 2030755833216647710960571904789704910190588189569395879314580155223/49417078230278166230938099976524290431788590640691711681402087*y^24 + 13136212786414648349996404489994350239425616970173093871888019612450/148251234690834498692814299929572871295365771922075135044206261*y^23 + 17744623682835446633917755307074169308056700391365881197007213949918/49417078230278166230938099976524290431788590640691711681402087*y^22 + 30283360230695375997620699063158645975872788912012147239521649112022/49417078230278166230938099976524290431788590640691711681402087*y^21 + 71252003390117222855649744421320440532352997365509604191444589387642/148251234690834498692814299929572871295365771922075135044206261*y^20 - 15565151661137759053664925152908356398791517227303432586642853710624/49417078230278166230938099976524290431788590640691711681402087*y^19 - 71886891319852042209462261490042516210349276203979009707060217242338/49417078230278166230938099976524290431788590640691711681402087*y^18 - 288989099802964955156064745764127180717240399618641405823338449753887/148251234690834498692814299929572871295365771922075135044206261*y^17 - 144426514644241275102380467015449777725578213602972830288561755426718/148251234690834498692814299929572871295365771922075135044206261*y^16 + 152564668850279495723668433141952654063017140673775944204428819811194/148251234690834498692814299929572871295365771922075135044206261*y^15 + 119472746900470124744340364809588368688809655338806683307692614070178/49417078230278166230938099976524290431788590640691711681402087*y^14 + 95551425201344211484854064008580716707187915542554839366200091668817/49417078230278166230938099976524290431788590640691711681402087*y^13 + 16736210837117205037401491108442871669741059379375458378408399374573/148251234690834498692814299929572871295365771922075135044206261*y^12 - 192360094253021129621698021782253413479458745709471927191277861847297/148251234690834498692814299929572871295365771922075135044206261*y^11 - 62513148392967426437974126486084294846874346891308515791449451137798/49417078230278166230938099976524290431788590640691711681402087*y^10 - 7401121098683378540636219608238562258529280231395684110099082250099/21178747812976356956116328561367553042195110274582162149172323*y^9 + 15917569841752823745244429791489727947414707798659497205157778814262/49417078230278166230938099976524290431788590640691711681402087*y^8 + 51998822451193426700351674751334924442262765303778881099467550983699/148251234690834498692814299929572871295365771922075135044206261*y^7 + 15279311585714449268056704915405634322942031667887314464232069616487/148251234690834498692814299929572871295365771922075135044206261*y^6 - 1945506436295613815081462329486581812028102458396995085812290559070/49417078230278166230938099976524290431788590640691711681402087*y^5 - 5844856897940417177682679250364235810009977666930572092207598558305/148251234690834498692814299929572871295365771922075135044206261*y^4 - 1271214519900219554221143804028023261353866432211135167887027232378/148251234690834498692814299929572871295365771922075135044206261*y^3 + 44818048943999206582452013354940694832305262851654919489217459890/21178747812976356956116328561367553042195110274582162149172323*y^2 + 5034703592911530146723795930148834747954404942117349503282775832/3801313710021397402379853844348022340906814664668593206261699*y + 27209135084177576624403764678685907082135429242538761287069692800/148251234690834498692814299929572871295365771922075135044206261 -290977061416012161192557269786495680619776987506686397873863/11403941130064192207139561533044067022720443994005779618785097*y^32 - 2108431384164826432229608455451516945282392065181095099811004/3801313710021397402379853844348022340906814664668593206261699*y^31 - 64639521696962629707408570635764399098424596415284965536486322/11403941130064192207139561533044067022720443994005779618785097*y^30 - 136185451893167592924485916463207567352615911899745071043956899/3801313710021397402379853844348022340906814664668593206261699*y^29 - 1756212767518494250777335942039444648732114002728074834507051698/11403941130064192207139561533044067022720443994005779618785097*y^28 - 1750894305982294900028297801997855245123723935690841007845457796/3801313710021397402379853844348022340906814664668593206261699*y^27 - 3444117936187867144634895923398451006901218833921765454372928492/3801313710021397402379853844348022340906814664668593206261699*y^26 - 9173048361527239684315815925541651266506658515597659830007496305/11403941130064192207139561533044067022720443994005779618785097*y^25 + 16642818074720921537490717818980066359071185234278855485601541037/11403941130064192207139561533044067022720443994005779618785097*y^24 + 80546186866933551407234599350255329410871629499134596667082650133/11403941130064192207139561533044067022720443994005779618785097*y^23 + 49380300122264045486466528714918875319643551293765548036129388603/3801313710021397402379853844348022340906814664668593206261699*y^22 + 36696037276668124089600003753290955552113954237131774496111870634/3801313710021397402379853844348022340906814664668593206261699*y^21 - 139767843037634009364142216597933566243987563319340072570849109296/11403941130064192207139561533044067022720443994005779618785097*y^20 - 514978145549619942598653750762681893233894634203025448958321590463/11403941130064192207139561533044067022720443994005779618785097*y^19 - 649981842945868644854686117397761104027349171558982654385640735886/11403941130064192207139561533044067022720443994005779618785097*y^18 - 61866172575693127521929031598820083675913056945520554463176834752/3801313710021397402379853844348022340906814664668593206261699*y^17 + 715747738430292752213564787236231333083779404022713128275156279493/11403941130064192207139561533044067022720443994005779618785097*y^16 + 1279034052395035525205761630382002630083749225311836010135334732285/11403941130064192207139561533044067022720443994005779618785097*y^15 + 836174474226399182737941248024075288519816415817064885111897778815/11403941130064192207139561533044067022720443994005779618785097*y^14 - 330604288730688946973003347086451134731150981815367422932774583667/11403941130064192207139561533044067022720443994005779618785097*y^13 - 385711428632094737494169765463638678725010864850995047511306947634/3801313710021397402379853844348022340906814664668593206261699*y^12 - 315517568403538227306525608276612064486316907189091248434590957603/3801313710021397402379853844348022340906814664668593206261699*y^11 - 97337367255828347116071093759923462011289381997171039549137304022/11403941130064192207139561533044067022720443994005779618785097*y^10 + 23280185371755840066719183678335228431206553796614291710919051761/543044815717342486054264834906860334415259237809799029465957*y^9 + 446304725918010999590754163959670456340065417412290405449954673804/11403941130064192207139561533044067022720443994005779618785097*y^8 + 116404688794844094483841340962564703914538879040221497651240232029/11403941130064192207139561533044067022720443994005779618785097*y^7 - 82511432622310487922150090226670761903903241617114120214236497121/11403941130064192207139561533044067022720443994005779618785097*y^6 - 82992171898779261116122108566125148083154199013120123243116809277/11403941130064192207139561533044067022720443994005779618785097*y^5 - 25227488968682009322168495432852277468013143037476133491403517340/11403941130064192207139561533044067022720443994005779618785097*y^4 + 2682930947456194137630127549832979129594726271911779444379321118/11403941130064192207139561533044067022720443994005779618785097*y^3 + 205446934088917861691434327745952740436648240964329508907813191/543044815717342486054264834906860334415259237809799029465957*y^2 + 96798709671063301446596248954160237506032596519541764662756444/877226240774168631318427810234159001747726461077367662983469*y + 127507179381986006727963354747392296592030563628900441774087080/11403941130064192207139561533044067022720443994005779618785097 # A Gluing Matrix {{1,-2,2,0,0,1,-2},{-1,2,0,0,0,0,0},{0,0,1,-2,2,3,-4},{0,0,0,0,1,1,-2},{-1,0,2,-1,1,3,-4},{-1,0,2,-2,2,4,-6},{0,0,0,0,0,-1,2}} # B Gluing Matrix {{2,0,0,0,0,2,0},{0,1,0,0,0,0,0},{0,0,1,0,0,4,0},{0,0,0,1,0,2,0},{0,0,0,0,1,4,0},{0,0,0,0,0,6,0},{0,0,0,0,0,0,1}} # nu Gluing Vector {2, 0, 3, 2, 3, 4, 0} # f Combinatorial flattening {10, 7, 9, 1, 0, -8, -5} # f' Combinatorial flattening {-7, -4, 0, 0, 0, 0, 2} # 1 Loop Invariant -2260952947606760173508159895277965733645760653292176666496753437/584817493849445754212285206822772667831817640718245108655646*y^32 - 25206335186823376246629139377013912166841494511584345298639031517/292408746924722877106142603411386333915908820359122554327823*y^31 - 532039357435378373901098939996288128076528603987466545850710725591/584817493849445754212285206822772667831817640718245108655646*y^30 - 1753775766834386699938035798703473428752955693299841003703543512974/292408746924722877106142603411386333915908820359122554327823*y^29 - 7991478486288242133407005000299617049883801602580127904830239956807/292408746924722877106142603411386333915908820359122554327823*y^28 - 26120314136374182785462118704164875511332796325702189135099425536453/292408746924722877106142603411386333915908820359122554327823*y^27 - 60474361444775700019912374353186105775747414549577241811971297919833/292408746924722877106142603411386333915908820359122554327823*y^26 - 176979584643945594739623198260228330090407838644187200317575831474047/584817493849445754212285206822772667831817640718245108655646*y^25 - 30287821867298827002665000401931441574822416151051671578497308266882/292408746924722877106142603411386333915908820359122554327823*y^24 + 224450203880739548531686773968749332093379218532946221414523554904315/292408746924722877106142603411386333915908820359122554327823*y^23 + 1317858431781265791966601977958580954180389097227444256862451560537437/584817493849445754212285206822772667831817640718245108655646*y^22 + 1850593499192762020089478742839335754788098953063082306428832863227123/584817493849445754212285206822772667831817640718245108655646*y^21 + 864986713327047055520065180102125657571669324265731773215772446138253/584817493849445754212285206822772667831817640718245108655646*y^20 - 1024527490608539349874585147593398186199251652855667778500319712850872/292408746924722877106142603411386333915908820359122554327823*y^19 - 2570011062894877898035233254175553762751568680369307567425560754615308/292408746924722877106142603411386333915908820359122554327823*y^18 - 5172102467320330711866648609963729987131585423898528848469313639039983/584817493849445754212285206822772667831817640718245108655646*y^17 - 367725881130177318107773605592055386519136964358550636481198041689981/292408746924722877106142603411386333915908820359122554327823*y^16 + 5147332061869619162420776110916245786455395753320026731614886512348771/584817493849445754212285206822772667831817640718245108655646*y^15 + 7212952029552889971355442091219929889366210624182575377390062827807595/584817493849445754212285206822772667831817640718245108655646*y^14 + 3569682918091908676188149949684705849561686018653863235990621254626547/584817493849445754212285206822772667831817640718245108655646*y^13 - 997753410379699660046534844408831547073782875689897424059674380666123/292408746924722877106142603411386333915908820359122554327823*y^12 - 4340622645895317719654944768189758057029565614865768533538163501418491/584817493849445754212285206822772667831817640718245108655646*y^11 - 2533336291575607971151261289751688593629724703783996114194758419106769/584817493849445754212285206822772667831817640718245108655646*y^10 + 16955881514243045794716446700827327760379497276580789824819144945032/41772678132103268158020371915912333416558402908446079189689*y^9 + 1229629782018559124684276630893132294283390475142912797642475473368163/584817493849445754212285206822772667831817640718245108655646*y^8 + 649097257801269074075539193723811680749223824620058322558167091068803/584817493849445754212285206822772667831817640718245108655646*y^7 - 17100393842768960397714826306435356569853134477805989609619549035167/584817493849445754212285206822772667831817640718245108655646*y^6 - 155866354089141893691252074838109200123429033351110079154364684363621/584817493849445754212285206822772667831817640718245108655646*y^5 - 53893733416889949487948039002792242662300920095402180934745095717343/584817493849445754212285206822772667831817640718245108655646*y^4 + 4671335706693433832583872832162458040560392716807325019243814653091/584817493849445754212285206822772667831817640718245108655646*y^3 + 436319277515447579371469310144977454068808040745694662066128905353/41772678132103268158020371915912333416558402908446079189689*y^2 + 425018810005517298883297015441723942510719818375956408270782989035/292408746924722877106142603411386333915908820359122554327823*y - 40625913526212869140439002747744942676629934593839378304044760263/584817493849445754212285206822772667831817640718245108655646 # 2 Loop Invariant -151577811480242832813554694531248192088446424261683916502927244875138603834492024225107208020168892566845950591801148432239849584445811978351475540802510501216545785423444931925/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^32 - 279021641890084661639771312559033683555220596720800750760810413363922045371936238951078595649397993291334056088367214409087492271420707583549685979027354133569942976151780140409/663325086621104474954261080323916076314765720834225437713321481025089240122004648346124280181468062595676996522168326905746063038040364380534476803832751652770883905614526650332*y^31 - 34983112814431255468225191516352903132845723033861293809534130912527315276476600967452217871314595108271418885822322877265053227175973730186559880845260200556944438933665447679997/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^30 - 4751750622552782269864062355365839866959888007316498232265528051425770924096778000579192852578423826605689084776826708474144275985930965236259457134297032871858924070512934261307/165831271655276118738565270080979019078691430208556359428330370256272310030501162086531070045367015648919249130542081726436515759510091095133619200958187913192720976403631662583*y^29 - 256502400240326780589983867157715230363646730799744168894614935259303466328823828837255896651935369178342812162730055030549160984711321142970641302202697609010456225935872394750363/1989975259863313424862783240971748228944297162502676313139964443075267720366013945038372840544404187787030989566504980717238189114121093141603430411498254958312651716843579950996*y^28 - 549959697949423821874545594216155127004633647737775757675605524711355932719340996471317030308305324516324208810101595340569303300839230475030481657890054621497894331987891875120159/1326650173242208949908522160647832152629531441668450875426642962050178480244009296692248560362936125191353993044336653811492126076080728761068953607665503305541767811229053300664*y^27 - 138193783482693526845743755936124390534594307591936010280010037330461718911422034326620134751189424150534292841780045411495628826590519413504697037708830647041486215845917685892433/147405574804689883323169128960870239181059049074272319491849218005575386693778810743583173373659569465705999227148517090165791786231192084563217067518389256171307534581005922296*y^26 - 10407237056476938126049227881354781149253705705029364008514123834883981448178449303214588979445071483440849851332740289213122974582519511516350305405758137554143660824335128032229113/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^25 - 124700197691785664960685022105991502162303244971458545901546860579600760515198568140834662860973168980008353444142163659806424703847009185403166596307087996885159481383141975785454/497493814965828356215695810242937057236074290625669078284991110768816930091503486259593210136101046946757747391626245179309547278530273285400857602874563739578162929210894987749*y^24 + 7676001866349034690373196087511604276065940653538385075193288836419838096910917315812097395246790653838236171656101206976491976640009704158250743219704371945979457384424887147081153/1989975259863313424862783240971748228944297162502676313139964443075267720366013945038372840544404187787030989566504980717238189114121093141603430411498254958312651716843579950996*y^23 + 9226901777406883479421337415075957983020057785738470178311828642679015926352332133369462260799712524239222920553427607078921613579976319053886680211300498784574598324886787272103355/884433448828139299939014773765221435086354294445633916951095308033452320162672864461499040241957416794235995362891102540994750717387152507379302405110335537027845207486035533776*y^22 + 36339206003705204077989808361146430770171181618570155889958924436181456973319400950589076568569157306235133512834120811577746009856373109516999270949339810824546407001689758522698787/2653300346484417899817044321295664305259062883336901750853285924100356960488018593384497120725872250382707986088673307622984252152161457522137907215331006611083535622458106601328*y^21 + 37195559439113750523687461864454538453176902331906291648146952176166404253332806606562913167302425695345156791242719279417297697969526119684651197160700439599769277097420746691673663/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^20 - 73727175483109754047460123511707165860358489032628492036298653753309002691977810203164454856979805678325498940494341270653159703391468362284997277681941872987722473234411302145125747/3979950519726626849725566481943496457888594325005352626279928886150535440732027890076745681088808375574061979133009961434476378228242186283206860822996509916625303433687159901992*y^19 - 40475666705506194860019085567018376260916904227383644968901140098958237972261409067334235373127578489193376400818560974665056203488267323800785085827634954994507100974751648895952167/994987629931656712431391620485874114472148581251338156569982221537633860183006972519186420272202093893515494783252490358619094557060546570801715205749127479156325858421789975498*y^18 - 32582566587471963645822671175833090108315193067544267470719595435111549738524078111668267679689929762893256990744999448088222305394233254155147941710429856618517214784692585785949303/884433448828139299939014773765221435086354294445633916951095308033452320162672864461499040241957416794235995362891102540994750717387152507379302405110335537027845207486035533776*y^17 + 3333039703980607956710081427365864175777552050977194854875721912752210112563622146096379249068050441004101292464784604977661082809279018690008099246733988430209322143504066127268447/3979950519726626849725566481943496457888594325005352626279928886150535440732027890076745681088808375574061979133009961434476378228242186283206860822996509916625303433687159901992*y^16 + 359754293761119254080002900743695347393236674922078675524432149238909217634351395616938249142324075279495772698385852231977338550366157101362131725716988587079791431004662491395653067/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^15 + 441041042104538974446533716484197392233722144236009175367571650672463152090720912580362256435463921583701064982049778883104830223060856779375951693863243001147179798039171764007109951/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^14 + 171395179502043272513740033455022589931099162778629989554594744594415499910541571919021051484981703563436523553359730882738248909139735305272861949765793869034768551645394456634893887/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^13 - 14730008517516819026467088360930567068765435539778249881557531667678838916766867461904261511862160990018994478241659988254378365104337588542169709020764112368882958688789810390582443/663325086621104474954261080323916076314765720834225437713321481025089240122004648346124280181468062595676996522168326905746063038040364380534476803832751652770883905614526650332*y^12 - 95849050940825806929522248405142828407445950313885757195005737132858246910414240954858138151088872132752981852285737224575426364931778197196202856987569525451821485313110542115160445/2653300346484417899817044321295664305259062883336901750853285924100356960488018593384497120725872250382707986088673307622984252152161457522137907215331006611083535622458106601328*y^11 - 139789347501234081723526087808786031717264767015046472848837696062794325905644500568511382412857561308698377068749813715842408193943075281841042926774851566260628502577377170976425953/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^10 + 980550869637706363368875624448979288487481945780769664016641980367182723382040327220238076460041962507959676920044636459291727382191303426597326081468896786896257269169690248464079/189521453320315564272646022949690307518504491666921553632377566007168354320572756670321222908990875027336284720619521973070303725154389823009850515380786186505966830175579042952*y^9 + 90143802753749552823633683679798649194771148888845739216087016379839427844728716928010207522867044313390375769998302607212844720100316935428184413550122619590670100974642033852527711/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^8 + 40109494059315340209770375534347102291279557338613328322447415991846352543133639584360909457774826746169845776899588166576784447021657207380135913598336180314088882509322919793115123/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^7 - 5967573327351811358544132695260502934996754989408979663564005684887152166752309978910430342598274006703942078311138240275962385051536295343949326780707835911821038839234919605560241/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^6 - 12815620582422098782024133671348440908080091860807793052520756027889230015383199224505566896437809788435144852607526425824046918265561546635461575460091088867385834148072713469344869/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^5 - 4020795958637477659645120124960459939488100915009169545390411156009845796922966914987471232853578744495729191046645150464415228913218713183368139275171258213139206932611489597360365/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^4 + 540444098850134133041011202324292252605974088649545096312282058268213708194540060151754012566122373659472423819856186641465536622102584630524111338569686567037900231744946844541835/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y^3 + 13854397809181607453655222979619834001816546555097903715442884965011454219087626165479888692995924631459785045615118486232283004531149382440341506043873151384908856138414795633677/189521453320315564272646022949690307518504491666921553632377566007168354320572756670321222908990875027336284720619521973070303725154389823009850515380786186505966830175579042952*y^2 + 92480003464396863554959518579823343419972637939400311176013941620138082077359510639742157574699893352598888660277282993385463848888321317431959572649134479447028547805744506082979/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984*y + 103445275639490993321363837788990466431485026798980336259447011391543950063342344879580574970671222352763749916847583075337069821651965267101920317356049646275920657179671653447345/7959901039453253699451132963886992915777188650010705252559857772301070881464055780153491362177616751148123958266019922868952756456484372566413721645993019833250606867374319803984 # 3 Loop Invariant 972867058780474289720240240493787189911199116154872989830797367739238170523810760052988180829248394625774066519150608899053094964482008036557974093517996456726357013677448488950424988507736071707975531415719151165289577720552424068657/9026645967797807622709642948242457908894599648030224815746074940054524090006588696142199548152770458649371256949203228552828665069344030745064988753100932337723094777180510866779797184171092399507502612441077870256398773240552935108944*y^32 + 43773490695257599872203405992883376971037642216215898169784696362455138194623786888438177984150766643383385099623934927325973687784509395736831217954430466189477116719603522413997434964908141137611055427087300486918525287090583986082911/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888*y^31 + 466398197796627434405409667992962650810777828722590304274587767546372975433790270484160599403660924530327020005315741297016822827325239607645023612591228675501258830255847329844021048002803242017768206603170658170339610655357632223648687/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888*y^30 + 1035664791623610586368836756333910061593454566262219450651933626918747816675880271270720033731273152674912854796556044715847888833115804892502242398095201893208936410058170846088729888976848568694827613836079511867944481808685529617910245/6017763978531871748473095298828305272596399765353483210497383293369682726671059130761466365435180305766247504632802152368552443379562687163376659168733954891815396518120340577853198122780728266338335074960718580170932515493701956739296*y^29 + 3581588074269641907403015927820045691086070991811989398163033281610033600529196480990772419673015699910854450749839989730639154091826315545702944089561810179053969331916640126080069269299655655999946712738800731676543838530183962845575985/4513322983898903811354821474121228954447299824015112407873037470027262045003294348071099774076385229324685628474601614276414332534672015372532494376550466168861547388590255433389898592085546199753751306220538935128199386620276467554472*y^28 + 23752014177207596442536614298226965032558318381961831240061412841746459035379242293702229713063895423037712696518893429764735111529803012654597167241737780263734094422901161935150547211462720395222293583222093597114941955394920977322592277/9026645967797807622709642948242457908894599648030224815746074940054524090006588696142199548152770458649371256949203228552828665069344030745064988753100932337723094777180510866779797184171092399507502612441077870256398773240552935108944*y^27 + 112183160506419985559320992959318361998118684493584741659377922680980149416015198449206103822302742405401410024976098511028003498474741232378945884214306157925440584118667586765972481720939002122996377798402533943616367060727404724256784985/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888*y^26 + 3154545322772837879519325416889599913363335999976640766996431486589766874546575926832610874204005278248061819044153087702748340912551351976694662725352161788540732304079288114082035975246288530571908435880149246463286981203516771958045919/334320221029548430470727516601572515144244431408526845027632405187204595926169951708970353635287794764791528035155675131586246854420149286854258842707441938434188695451130032102955451265596014796574170831151032231718473082983442041072*y^25 + 6386690696594958000647117775667415495077618284283869278628597153476848961837697111029117597981489809131750765924625003076388310360365552211542740244590745175236470298248837175516104872166585398255065756869609286637603661255960902701976385/1504440994632967937118273824707076318149099941338370802624345823342420681667764782690366591358795076441561876158200538092138110844890671790844164792183488722953849129530085144463299530695182066584583768740179645042733128873425489184824*y^24 - 191624039592673099060415852750224912828127504284054492663377676526646686957648834842700141702521900107345389886813664513387584562442618116745867112884325005479521705884152926207340441936709080060647310575531674867135651739988914483671795725/9026645967797807622709642948242457908894599648030224815746074940054524090006588696142199548152770458649371256949203228552828665069344030745064988753100932337723094777180510866779797184171092399507502612441077870256398773240552935108944*y^23 - 201652295511453001153001638952278947594396940085241135905893766504344965407585439448967812273732618284908589789208188644347716430141383229603718638876822476518420449510855429172311326780966024715327214819480600113860351714840815525452740475/3008881989265935874236547649414152636298199882676741605248691646684841363335529565380733182717590152883123752316401076184276221689781343581688329584366977445907698259060170288926599061390364133169167537480359290085466257746850978369648*y^22 - 298355262907037060604580482831199846687213697520492627757619369203993103092023280454976270064529395028702165500489381465341765098390097803965511324718284144226110543214099977627126713299197884978054475549139654293542236402589544594835102971/3008881989265935874236547649414152636298199882676741605248691646684841363335529565380733182717590152883123752316401076184276221689781343581688329584366977445907698259060170288926599061390364133169167537480359290085466257746850978369648*y^21 - 248860842568174670815755227707544378492591495328970034091894190295604929743454071636886210867916865492489510632867200553236524474158446868827427798821333424262648892602077991612384495997193883883861861889695439482114922837451591334280135601/4513322983898903811354821474121228954447299824015112407873037470027262045003294348071099774076385229324685628474601614276414332534672015372532494376550466168861547388590255433389898592085546199753751306220538935128199386620276467554472*y^20 + 70389476144460760503300786463805268327455677133345860419397593682429709004072676212089712244324449314712381782379564972080639069820686057096598136782806650491454905898777476290073098103553927603106038993197024324647682635502512210078926903/752220497316483968559136912353538159074549970669185401312172911671210340833882391345183295679397538220780938079100269046069055422445335895422082396091744361476924564765042572231649765347591033292291884370089822521366564436712744592412*y^19 + 1592161528351312666880927321778385943848921691159603551453866134942106180696154093018595784866902919459233538815137061946657111003519685579861415317336905831153879840672936644995188346906379920943502397402566324413662804822740305410492434951/6017763978531871748473095298828305272596399765353483210497383293369682726671059130761466365435180305766247504632802152368552443379562687163376659168733954891815396518120340577853198122780728266338335074960718580170932515493701956739296*y^18 + 5189224678315092465846687344748176897213492686313042669358872844533197726906676035781765579160036779768956090348407877410815944373824465859210737999022532021437474445824430194308601889216920927677311789605558688007826482397553782401036859653/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888*y^17 + 159148345880787211806473171040263775271608799677382065734653529389670743604290222473011014897134687553371286619440949343535810918359761777496174847675586811622676733165549971185409038184632391050512764427737981399347615844185435631500330375/2256661491949451905677410737060614477223649912007556203936518735013631022501647174035549887038192614662342814237300807138207166267336007686266247188275233084430773694295127716694949296042773099876875653110269467564099693310138233777236*y^16 - 4471083737793123401623615760586978670706696346660715864699529871840294461043618016664616841968330640060254155788755779535763046353657934294998891901252118499891984992012398522852589614845086500417607869092056453216480760796123118544146677185/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888*y^15 - 2333602269419386097565813586529099189794553387390834397188140037581314929218938340262815839672747976027191113575612091577586927246950582729397364958577009028940968202923797007627680696748052800519542025559410123290963472284738659224745706285/6017763978531871748473095298828305272596399765353483210497383293369682726671059130761466365435180305766247504632802152368552443379562687163376659168733954891815396518120340577853198122780728266338335074960718580170932515493701956739296*y^14 - 666058003785766154176730867156287451451462798136323131272561068365276391022657174470930138939731637985607069715336504008192614969938076472684338804798374571913109366814981566070591579603975790515782880395587813494717153590515714849192129921/3008881989265935874236547649414152636298199882676741605248691646684841363335529565380733182717590152883123752316401076184276221689781343581688329584366977445907698259060170288926599061390364133169167537480359290085466257746850978369648*y^13 + 1387005332100437912384151877390358616796833911157113021144295156035766733085066426453975039417192742946132917285738876847250511246126835313561073851582573463703517212364821956341458579770538675578132479824835261487539566635885136191891468241/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888*y^12 + 4103924799832453090853395223341279394340374487476935952095960025139784357532989532942264672955591430596645248335159268273628557590239447611140824126450736801959803657930015980324638126686518725231662837188886188762938499682493753384990994057/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888*y^11 + 454996120026052392201581209419682524894534749430511795423102925604686819833490745299409574138505024554766446422557391670355668406423525062616766699266932788027065055652519302127326918894135056503133971787586206598209693705321994063264270653/3008881989265935874236547649414152636298199882676741605248691646684841363335529565380733182717590152883123752316401076184276221689781343581688329584366977445907698259060170288926599061390364133169167537480359290085466257746850978369648*y^10 + 9683904313794550343663869961279841280405332335050034853758822914492593863784081667360132592795427026561221593320933988365020232624981122312753119785107527860413177835927455725198526010451830683061457441406244456954378074095684181097826959/4513322983898903811354821474121228954447299824015112407873037470027262045003294348071099774076385229324685628474601614276414332534672015372532494376550466168861547388590255433389898592085546199753751306220538935128199386620276467554472*y^9 - 379618033692149852857864483289667801547538984381526777759700389754797448972455515506940636509753040677556263528424903868918016432216023244574659826187512070637261337911637356041239547141811928011546282555438784128857058121101563027546631109/6017763978531871748473095298828305272596399765353483210497383293369682726671059130761466365435180305766247504632802152368552443379562687163376659168733954891815396518120340577853198122780728266338335074960718580170932515493701956739296*y^8 - 175734490279053549976844350277436721046979362853606410932213591745509381082754749783676350543122819328315807887973055055690582667105694011639848103937685373294260878274261633585693558020552125554369931279481486748314619790831140802399612899/4513322983898903811354821474121228954447299824015112407873037470027262045003294348071099774076385229324685628474601614276414332534672015372532494376550466168861547388590255433389898592085546199753751306220538935128199386620276467554472*y^7 - 9515580861755816017123099383676916879117680214179491330383049686136158712880324228371802568992324806835962459535438866263431287806096922580388674633881929544313683804396366285345680832691603838936077678866774045884519683005338170617601285/4513322983898903811354821474121228954447299824015112407873037470027262045003294348071099774076385229324685628474601614276414332534672015372532494376550466168861547388590255433389898592085546199753751306220538935128199386620276467554472*y^6 + 16223235943690683306382739589461788819785032483804730473806714362852557076105303205729938211915554923819607794638279872217082772053563730686954799725025488659431649670061971308234363078985613433689632985909447767542345997250964090971223683/2005921326177290582824365099609435090865466588451161070165794431123227575557019710253822121811726768588749168210934050789517481126520895721125553056244651630605132172706780192617732707593576088779445024986906193390310838497900652246432*y^5 + 30383692562601445301474020181673238473970438368813428176262451487398842693303208527891929927354235053123898572386861208665920316220451077335472534264902365617798243010835315500516726029026523036021165296629808607010491300081636023755131361/9026645967797807622709642948242457908894599648030224815746074940054524090006588696142199548152770458649371256949203228552828665069344030745064988753100932337723094777180510866779797184171092399507502612441077870256398773240552935108944*y^4 - 829272036949906686179124950376704439944700727984753828625667911594238618675388580117184537222301658072370400872626594874486691185723698492295233771132520810708259198866015850386080788452360721928146840032181754540341052441061323339350819/9026645967797807622709642948242457908894599648030224815746074940054524090006588696142199548152770458649371256949203228552828665069344030745064988753100932337723094777180510866779797184171092399507502612441077870256398773240552935108944*y^3 - 12383191243850610188776648433032001128382041853352427959778897569951855325556041467337819502973430555848605114062946139437286499625921962618440194900965978738675863889531232122467530332749611707294680409487236145078180370137021140749487793/36106583871191230490838571792969831635578398592120899262984299760218096360026354784568798192611081834597485027796812914211314660277376122980259955012403729350892379108722043467119188736684369598030010449764311481025595092962211740435776*y^2 - 73310354687788372268565328670631683413632012796180557501676721462170598932697271382542010861637345415969827087618349062601297237684375548702693217263702020774364619330063304506428308592595242800945091345867153579821346630588725630234569/1337280884118193721882910066406290060576977725634107380110529620748818383704679806835881414541151179059166112140622700526344987417680597147417035370829767753736754781804520128411821805062384059186296683324604128926873892331933768164288*y + 45824909907783456207002846798713860495183362513596776768029465495788685932759514282980358830987791054483743035140388873520216916371848076957396551052869760163192189996004079412013428256559433945028336705044551899119821662352621055230669/18053291935595615245419285896484915817789199296060449631492149880109048180013177392284399096305540917298742513898406457105657330138688061490129977506201864675446189554361021733559594368342184799015005224882155740512797546481105870217888