/*************************************************** * File automatically generated for file 'NAV04.hym' * Reachability analysis * 10 states and 11 transitions * Program terminated after 1.092 seconds ***************************************************/ /* DESCRIPTION OF THE STATES STATE 0: nav: Q_hub ==> 2*x0 = 1 & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 & 2*x = 1 & 2*y = 1 & 2*vx = 1 & 4*vy = 1 STATE 1: nav: Q_0_0 ==> 500000000000000*vy >= 11091270347399 + 50000000000000*x + 177817459305202*y & 26*y + 20*vy >= 5 + 26*x & 2*y >= 1 & 277817459305202*y + 111091270347399 >= 500000000000000*vy & 20695436482630050000000000000*x + 73600198691069234668292130402*y + 53204364826300607665853934799 >= 206954364826300500000000000000*vy & 827817459305202*x + 11091270347399 >= 600000000000000*y + 500000000000000*vy & 1 >= x & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 & 26*x + 20*vx = 5 + 26*y + 20*vy & 2*x0 = 1 STATE 2: nav: Q_1_0 ==> 26*y + 20*vy >= 21 + 20*vx & 500000000000000*vx + 6000000000000000*vy >= 269186514516187 + 2961626970967626*y & 1480813485483813*y + 889087296526010*vy + 1106865081389596 >= 4139087296526010*vx & 2*vx >= 1 & 1225843257258090700687797695226*y + 743395333948483024656101152387 >= 206954364826300500000000000000*vx + 2483452377915606000000000000000*vy & 1 >= y & 2*vx0 = 1 & 4*vy0 = 1 & 26*x + 20*vx = 5 + 26*y + 20*vy & 2*y0 = 1 & 2*x0 = 1 STATE 3: nav: Q_0_1 ==> 2*x0 = 1 & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 & x = 1 & y = 1 & 500000000000000*vx = 363908729652601 & 500000000000000*vy = 238908729652601 STATE 4: nav: Q_1_1 ==> 777817459305202*x + 190993590561183 >= 322182540694798*y + 675244199465540*vx + 324755800534460*vy & 598754705848283325396309841859552745728091413*y + 6663104915899485697381739875712250710095626897 >= 63492350632970812202719685638135694465188369*x + 4961422562384891124255192756770314250485731940*vx + 4549682289142343037183200328907685749514268060*vy & 836887656702130831283563717656697254271908587*y + 6783205648752167354759841167250453627571846797 >= 1430223431800351844703294230457091474368548478*x + 1721782299567654491450891405478185749514268060*vx + 6359153276808335450377754561167314250485731940*vy & 498691785981363421822589005753447254271908587*y + 4487762480383145043189719583996877398931389732 >= 1430223431800351844703294230457091474368548478*x + 315778894130740526280463631929359520873810995*vx + 3789346729568886315365563583152314250485731940*vy & 52817918327725712069986023681758237184274239*y + 402647356430220973697207420450933746092390368 >= 321357219232406837987113302468796437378567015*vx + 280728051288002444087124053482828562621432985*vy & 7150000000000000*y + 500000000000000*vx + 6000000000000000*vy >= 10380813485483813 & 287284226380274302002438195603 >= 89147888547945782191985549659*x + 217976898568765475236934192570*vy & 10*vx >= 4 + y & 26*x + 20*vx + 21 >= 52*y + 20*vy & 5734883735037314559*x + 4804699026951780430*vx + 115005225673794510750*vy + 2202395407003665086 >= 11581176205111943677*y & y >= 1 & 410784845695559806250000000000000000000000000*x + 313692956032875571167073032600500000000000000*vx + 228458977538146525245123164395159754271908587 >= 854393722772156813560855633812850000000000000*y + 27544641718352895995123608794000000000000000*vy & 2778911213290964064704865064447 >= 25116571572614075687797695226*x + 1812678566873410076658539347990*vx + 1831999006544651673341460652010*vy & 2968603672596167787358528021231 >= 520558037422470225343898847613*x + 647182540694796923341460652010*vx + 2560610114112860826658539347990*vy & 5734883735037314559*x + 4804699026951780430*vx + 369907145225827320*vy + 2202395407003665086 >= 11581176205111943677*y & 2 >= x & 4550232136935431700000000000000000000000000000*x + 3812196176791219237671949423806500000000000000*vx + 244032752140313852063393085678000000000000000*vy + 1747426406666046284393613781185451805534811631 >= 9188844588981608701291123239567050000000000000*y & 1 >= vx & 4928686008222670875343898847613 >= 2959447417016097150000000000000*y + 206954364826300500000000000000*vx + 2483452377915606000000000000000*vy & 4*vy0 = 1 & 2*vx0 = 1 & 2*y0 = 1 & 2*x0 = 1 STATE 5: nav: Q_1_1 ==> 24000000000000*x + 841908729652601 >= 622000000000000*y + 20000000000000*vx & 600000000000000*x + 500000000000000*vx + 286091270347399 >= 1250000000000000*y & 838908729652601 >= 600000000000000*y & 500000000000000*vx >= 313908729652601 + 50000000000000*y & 600000000000000*x + 50000000000000*y >= 286091270347399 + 500000000000000*vx & 2 >= x & y >= 1 & 1 >= vx & 2*x0 = 1 & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 & 7150000000000000*y + 500000000000000*vx + 6000000000000000*vy = 10380813485483813 STATE 6: nav: Q_2_1 ==> vx >= 0 & 246206090012092199932692296092842117496475744416200000000000000*x + 116781193509550203512366613046090581115923701608000000000000000*vx + 23785414629958331321476395624665798426326975134000000000000000*vy >= 474498707240530313639103692069991720151469026825353902468417657 + 57854064648642857146394959665030300000000000000000000000000000*y & 2798119867610392032003730767530245100000000000000*x + 742319292880502762374386766960157000000000000000*vy >= 4438860154980492358145722715637904409400146479547 + 657508543787169880650000000000000000000000000000*y + 108376063748331028561738819422585790599853520453*vx & 2418141141545645251925096352049547800000000000000*x + 2029209349548793218398682253468152000000000000000*vx + 169100779129066101533223521122346000000000000000*vy >= 5149689372499743335521349065607798310510095930883 + 557403436774590383250000000000000000000000000000*y & 229689849164479367343190577459049800000000000000*x + 70351998193753069791099214788254150000000000000*y + 59036641840911666957565774647486000000000000000*vy >= 433743214963652799626510535095933860046372357353 + 122858157838532254787724257361681000000000000000*vx & 349421394953345738903176422871159657100000000000000*x + 91555726429090310321238298802178997000000000000000*vy >= 557578954661258650420269948592186433537417724025187 + 80544796613928310379625000000000000000000000000000*y + 12760904475167644416832897150132880662582275974813*vx & 5546198948791278662708540041023174951580936143817461100000000000000*x + 10392756050874269545335104667954593979075641603894008240011199955250*vy + 8934453314010792111537485931417127401420602670347576900238651213273 >= 1046564087646879746786639389463448530833401542551540852441747193019*y + 18357139968219541291562200695272391200293039545138757852025759897075*vx & 2418141141545645251925096352049547800000000000000*x + 2021625629320567498898682253468152000000000000000*vx + 169100779129066101533223521122346000000000000000*vy >= 5145897512385630475771349065607798310510095930883 + 557403436774590383250000000000000000000000000000*y & 8047783195524406703527789842566457498918172675589400000000000000*x + 8056807564665351963706357796353699899421765906729250000000000000*vx >= 19332224912539085799058716652806087540751717072815560043353775459 + 769723246814495540216686239971621700000000000000000000000000000*y + 29312763596856240479423692106390293781945966742000000000000000*vy & 242*x + 244*vx >= 583 + 22*y + 2*vy & 40757710023525581749257685789309377800000000000000*x + 41036391645063017016742714025343683220092744714706*vx >= 98144239090767543965359588379967408210046372357353 + 3735934767948398745501317746531848000000000000000*y + 306884021733458592051644929582682000000000000000*vy & 10691071463633214628607068284585811548555214283947512239917978127400000000000000*x + 10687231708848863387939614390218901228208565504151991040490611016000000000000000*vx >= 25687250169580890082702345021158578230598037795224165660885372728659794927048389 + 1014119014541602288604915674187373362563059559291725000000000000000000000000000*y + 32464174568140597625664624578691988785904955822479913292449082000000000000000*vy & 843261590696260195960489817734672845866660642532458*vy + 2971281302708421364958315186373948908158330321266229 >= 456338904087431859380168136753728275875000000000000*x + 60638406626401310796141288520206544050000000000000*y + 1841309401438805117582121140577286297125000000000000*vx & 10465778623141822517354433061428633427352288688855630982824247900769 >= 3440480808535674044992219333664044948343963989762023600000000000000*x + 431001774553613311266438446439511990105495498720252950000000000000*y + 2897163423819064776946068402292427275768955690679559500000000000000*vx + 236224949876786638280935187552877248945655782209767000000000000000*vy & 1930932899495990810877600000000000000*x + 2124156421688287786344000000000000000*vx + 6180548065299545327352000000000000000*vy + 8836241751679659959395021158581796797 >= 7204242036190625614188000000000000000*y & 3517717577762013716376000000000000000*x + 21963253898306455081294763815393679506*vy + 37218547014562686030584981907696839753 >= 14478184977946814348452800000000000000*y + 13976669835043314110272000000000000000*vx & 493709811168022690244292816226166272461467306633351928000000000000000*x + 414293323136992634491107813512257623564609622149202080000000000000000*vx + 1739704722901232696503076710544466651654798672693305616000000000000000*vy + 2692821294809210256688720227967105318876363880360665754721216679591091 >= 2032005643859967072479142012046642237183512809406743198400000000000000*y & 980795685255158096867198800556153894*vy + 12160412680399603503646024400278076947 >= 3404896043606817552775125000000000000*x + 452443280560837948389150000000000000*y + 4342131730024970767514750000000000000*vx & 12576202841764628784000000000000000*vx + 42697089137659445739909341990953091 >= 12784812841509539688000000000000000*x + 14489454553710811646400000000000000*y + 11026528557945290640000000000000000*vy & 10847580842254865175343898847613 >= 2959447417016097150000000000000*x + 2959447417016097150000000000000*y + 206954364826300500000000000000*vx + 2483452377915606000000000000000*vy & 284182326260579086378396058441013017298596842737211138961817848237500000000000*x + 64013836584661992595781247493617461040108786492327972281089960500000000000000*vx + 4097762022825434704397436676149353729625180018935667373079526000000000000000*vy >= 386208470334157827363163954946100463425035267490049707839312209894496639118773 + 154297724629699372903296707387434557378796714204309996380413564850000000000000*y & 1432678061313042698404083867037529609003343593415155*x + 322719192912742012912650342649330102847841802089240*vx + 24845705150374550564916579826247291399731158737760*vy >= 1947032343277618609003234914403337115437957609968438 + 777877618749643220603263253393425614906583028148036*y & 577515770980134946166117605611730*x + 606075473326164415166117605611730*vx >= 1394373276445124745775401747706217 + 54367195134260236763172772085043*y + 18657614087934234753438988476130*vy & 4261604280503179896000000000000000*x + 3576171424198472640000000000000000*vx + 298014285349872720000000000000000*vy + 11017695246009762386165474321351521 >= 14489454553710811646400000000000000*y & 17610355292093847460788637450688382012156958767256900000000000000*x + 4526348211958017112733315558182263502598388724983000000000000000*vy >= 29736950967957711409753034185471752994419075178064742346651733393 + 455809167811788247760832796734190961369348641097348000000000000*y + 4756551697181844369668682615392703171910313276135641653348266607*vx & 210133846523854901459883476315211*y + 8882479786109440615723579327778999 >= 2997673612819221738187500000000000*x + 3097266406994852040808462804094210*vx & 49647689867862045788400000000000000*x + 41662397091912206256000000000000000*vx + 133983497514735901503000000000000000*vy + 175231726512835979627198328213500963 >= 156613957308491861178000000000000000*y & 63069040917843390209613786829049667301953450592505653773034172796736369975788144000000000000000*vx + 187639157400948028489993302995553162555385233063433812429165318234075762748343431494683384006231 >= 64115209843020887203612119785929638086583010199490344712397298885781759999083208000000000000000*x + 49585375453140865783906494780372608600852419975362365907012925269790554106240502400000000000000*y + 62109746516918241665993197753796690896628898539315078227080108433161294171650040000000000000000*vy & 7150000000000000*y + 6000000000000000*vy + 7580813485483813 >= 17461626970967626*vx & 111945684527605408520633930856780*vx + 246774702409801545648489737513433 >= 115706741058901797768914436618715*x + 3123348224534821352063393085678*y + 136421428662531666037828873237430*vy & 3778948849626079940584693109844662698330310216745261338308609375741*vx + 10772263861825562396751911834470285958478485764875470683850612376780 >= 3360566073644551203398711210237955816632529792731040000000000000000*x + 3554860909954277449463558788001834992829887381244628000000000000000*y + 3292682186439312156069963937248987848142667453289508000000000000000*vy & 934953075983879022960975552205533298791164263913586087600000000000000*x + 713578420454127134625208984596380169600977004682729584000000000000000*vx + 2523144248320190943518518539435188342809043269619432667000000000000000*vy + 3335419538216123280752174357826991291341113051639034700547239650982607 >= 2949315497202365158267455068116167273010754223075046242000000000000000*y & 160849890295734174802268830961394600000000000000*x + 44593004614326804487917900107464000000000000000*vx + 11089145050857794332326491675622000000000000000*vy >= 230839814071824344818873438881855688379954617781 + 81904178464837770600000000000000000000000000000*y & 12963621412719463320000000000000000*vx + 42503379852182028471909341990953091 >= 12784812841509539688000000000000000*x + 14489454553710811646400000000000000*y + 11413947128900125176000000000000000*vy & 3570459483729266746200000000000000*x + 3604724782293788671049312202304774*vx >= 8599323204264116396924656101152387 + 327815713884859992000000000000000*y + 32284880912902878000000000000000*vy & 38019783522453268363943734692692051 >= 12499781062158176831240625000000000*x + 1559628788767483198050000000000000*y + 10531868822067027513656250000000000*vx + 855614017430934485906250000000000*vy & 129109326002118147509452519244974530085113162060200000000000000*x + 20911470129479712750979295970257479120418772861000000000000000*vx + 15671623919750357468126707410305284143604951537500000000000000*vy >= 227061556989283188758714448185976183396777863637714142145370997 + 30338401836048781422070849551216300000000000000000000000000000*y & 561554566930016969826653995955184804148132385775750*vy + 29787227716624499139599993357450834492119363194011139 >= 9468477419519230732294671904964364942562500000000000*x + 56549277220224231867672365472319070428108652181017*y + 10760052923458269762895976095661289992103204487284225*vx & 31485458777027688222867095981177552805*x + 8121557365114196286654234220885456810*vx + 2159540358797164449740272673630202180*vy >= 36399803971681203108284897003640474748 + 21745139264216517296923082937563818716*y & 17494323469347620780566390492793494528291808528018250*vy + 1113441545661492037103080810997661128266702928466287404 >= 356288984301190859219539432231399740163500000000000000*x + 1761701187930509257676891525445992977584522130370847*y + 398052920439345753188751670302888456055848356826829630*vx & 204884421463718579669697379452061411*vx + 633773366715920790352640129864296365 >= 191772192622643095320000000000000000*x + 217341818305662174696000000000000000*y + 178763869067121151092000000000000000*vy & 456189046461283798306766207567083714515*x + 398841595189039008276662027796801175530*vy >= 77971090080200066572156925986790811414 + 441357120398857627854630907563967830468*y + 38342189202669115816482612919634493370*vx & 1531604648149480496054246323592634792522118681601535384885882686000000000000000*vy + 115811793360132621233876913142820666153765273140786702055034996313489647621673047 >= 37252815815365160036033962905881275809650365266837541826531734219125000000000000*x + 154191051671698328051452389396609211395956758754457312177656465850000000000000*y + 41060153382161285534441370502549818875084088663424893595344422317750000000000000*vx & 33941073313934333925643570723815340843889447602870*x + 33930783266219084024881564315369251843889447602870*vx >= 81683552969570714019063134576663709375102812460123 + 3098624314775062483629250499003701284852668333817*y + 130721953264866722071077059295793899536276426470*vy & 729577117427919643356204098482663518370007228961050400000000000000*x + 514442688092487905247550507648329706438467099200808000000000000000*vx + 93536708406709451351588517754058179100669621634888000000000000000*vy + 1518392464546311961008097937019656034251740213781848797159718982941 >= 2188731352283758930068612295447990555110021686883151200000000000000*y & 934953075983879022960975552205533298791164263913586087600000000000000*x + 713578420454127134625208984596380169600977004682729584000000000000000*vx + 96249850230326907972072420699631795300081417056894132000000000000000*vy + 2121972339171191262978951298459213017586632125357765433047239650982607 >= 2949315497202365158267455068116167273010754223075046242000000000000000*y & 451627030736817979671620671789896076150287365842227668700792956005335151678793053125000000000*vx + 1344187911266258564297784765381730269074179638150226133522095141193424708691959140862918416731 >= 481665655708879555488849948466534356720641715638615726061763110652591968298672844531250000000*x + 306993087109268338473416602205970911651087315103820748224235275813361066932199155312500000000*y + 472225180384406525640976913683416607598735790170396248068338370707635345605430139062500000000*vy & 42971237598217257691253208719832778*vy + 545184766893350347433351604359916389 >= 153321572057061453098625000000000000*x + 19671446980905997756050000000000000*y + 194657906798457466630750000000000000*vx & 85800000000000000*x + 7150000000000000*y + 500000000000000*vx + 6000000000000000*vy >= 181980813485483813 & 456189046461283798306766207567083714515*x + 215013580723457788749238617602920959950*vy >= 169885097312990676335868631083730919204 + 441357120398857627854630907563967830468*y + 38342189202669115816482612919634493370*vx & 330008194551679018355494800000000000000*x + 1552522493723805835877172224729718197878*vy + 2424820558156681219524218512364859098939 >= 1041012974229545401250166000000000000000*y + 919312219095067893727368000000000000000*vx & 20941138847370152788444037887950189994706788096500000000000000*vx + 415251321897139222233354797711868634868295162074722339728562073 >= 135001686093906763673042916384203478941285974081125000000000000*x + 80240117324909002267697071621720881868249511250150000000000000*y + 71163844522231174029210538756862460104337804044250000000000000*vy & 109475835478579257028904978799755139626*x + 59076586615313411491799059707899810770*vy >= 94105657852355091575863374483762179827 + 61705120541572240053467544757192628340*y + 26400313736641589402232858528414425145*vx & 52815119087097122*y + 123954364826300500*vy + 213686765289448953 >= 285095039100491150*vx & 471459734384296636368975747062475432000000000000000*x + 26668261265051837324955989038729528116019130347021342*vy + 49700032872508890796173175030031022805209565173510671 >= 1940429012044841945476521232646609409600000000000000*y + 43847596180859647626093520375291381248000000000000000*vx & 19869003373170217532719688120805987616657550905296494250000000000000*vy + 1484721696708079085552296105915701776177010682122848429159703912023809 >= 477875368211153541461786714389965216025614325581788831625000000000000*x + 63500176370623971014973187876457569911984775293960724950000000000000*y + 401014564261888630968170389832245092234264840704269110000000000000000*vx & 12616106070418958406206945105460052161730324930875000000000000*vy + 1058143255018862454429622286342679437052948187186573686243072321 >= 341084903356855953961863627660933657552036145009875000000000000*x + 12134537439583202492657260255626779530261241246550000000000000*y + 352866156249151937265582266237023271950728864888250000000000000*vx & 31485458777027688222867095981177552805*x + 8121557365114196286654234220885456810*vx + 694547966916684076558629212804806560*vy >= 36399803971681203108284897003640474748 + 21745139264216517296923082937563818716*y & 10811447299552063233548241327015151700*vy + 645838784526130543867365249240367230028 >= 206146539469069065867750750000000000000*x + 1587565873979926310787258928126302279*y + 231012868258038811304911705052134848910*vx & 8996720147728935336000000000000000*x + 10139108241570114096000000000000000*vx + 31702097421552015792000000000000000*vy + 47775658898553592744394419673409617 >= 37028606081705407540800000000000000*y & 38741857095483453600000000000000*x + 29801428534987272000000000000000*vx + 99338095116624240000000000000000*vy + 126573136284437472379470685018969 >= 116225571286450360800000000000000*y & 229689849164479367343190577459049800000000000000*x + 192746726571591077490789295769832000000000000000*vx + 59036641840911666957565774647486000000000000000*vy >= 469624361423026503374668096873436210046372357353 + 51569297551934892600000000000000000000000000000*y & 456802425875497589765150658828469094283177078313750000000000000*vy + 37714417100538152374831877034618077237762398789340551313756927679 >= 12147359954428320998374475566779031029947963854990125000000000000*x + 138950040667577432239612830632220242344738758753450000000000000*y + 13198005533941965454834322082084509946799271135111750000000000000*vx & 23654292955345483497761880567015310500000000000000*vy + 1801916613594074884462684828472671141354518798984041 >= 580209040533102162943981258680925461750000000000000*x + 641029620846228155258864740835215748070759277522670*vx & 4269979063227725827055629793924510067019222745320200000000000000*vx + 18017302930583182471874667750549736202950128179912325725212533803 >= 5550919068020294791586231748774419795202897286801650000000000000*x + 5550919068020294791586231748774419795202897286801650000000000000*y + 4658113903233813811121313355614897730240193527386000000000000000*vy & 39261491139448548409075707543867024274490556630000880800000000000000*x + 30053126173224044967573842064179431595761966638462216000000000000000*vx + 4003636941836740626739941512907648990751560865886376000000000000000*vy + 89473190841445555971141862199476719440713776466589688381298361686457 >= 124134568188836213617807647025915258423471669890002642400000000000000*y & 37105231055824046049409375799873*y + 11191009165850148018257302340854238 >= 3907033596401950779477226843762212*x + 3279356902467184966709961873314615*vx + 281946865586711805747274042153260*vy & 366530332968094516917688252236795*y + 109991271490247363366234938106633613 >= 38404431278124311568805252534923719*x + 32218450823665284254501946360440090*vx + 2785108071887008770485484241092900*vy & 15201327529410306624457813471560515853920068564373904000000000000000*vx + 51111609999315292733471977884845329518156762043149893467068372351721 >= 15453482251462136355195265353790192657184145531081528000000000000000*x + 17183741623591578312911113465791214026942031601892398400000000000000*y + 13663690797712582344000651111153019913448782607002856000000000000000*vy & 4261604280503179896000000000000000*x + 3576171424198472640000000000000000*vx + 12372559746775549092000000000000000*vy + 17054967976722600572165474321351521 >= 14489454553710811646400000000000000*y & 362066661263612724750000000000000*vy + 27015159105283342424759464449416683 >= 8708174024569865863875000000000000*x + 1157143940053293985650000000000000*y + 7226639465369587159500000000000000*vx & 20495752025893774816798436774183033800000000000000*x + 17503359095869823338753932957356392000000000000000*vx + 5082788891500131897062827746446366000000000000000*vy >= 42444450774492918849598115846748333013756160945593 + 4349010760213175942600000000000000000000000000000*y & 19364151332943889494835507041731800000000000000*x + 16143571465012694408253572342712000000000000000*vx + 81344250713437950687797695226000000000000000*vy >= 41061474868141724293151645170312382731488396123 + 4550232136935431700000000000000000000000000000*y & 1952363717898074622417119908401923300000000000000*x + 501811455647749169139309084503631000000000000000*vy >= 3139875210198084272063408816000996970788330075001 + 438339029191446587100000000000000000000000000000*y + 65516547936757854570831000802849629211669924999*vx & 72009494127254206275343898847613 >= 23675579336128777200000000000000*x + 2959447417016097150000000000000*y + 19936603811600281500000000000000*vx + 2483452377915606000000000000000*vy & 46527833841346635654144835347265735013257220483967478476464325841834*vx + 143527341189798086573670595648288597687368866938137790117115946778687 >= 43547970397188422989432431055442052448159708576782216000000000000000*x + 49057080557369028802597111274425322901052445861175866400000000000000*y + 40781528428548792994265780075113328976205357555924248000000000000000*vy & 2482384493393102289420000000000000000*x + 1900586104818813271800000000000000000*vx + 249580974457644916456427267363020218*vy + 5628056249890622422513130044356558259 >= 7830697865424593058900000000000000000*y & 49647689867862045788400000000000000*x + 39531594951660616308000000000000000*vx + 3471866424326017188000000000000000*vy + 111041312037756832443698328213500963 >= 156613957308491861178000000000000000*y & 38741857095483453600000000000000*x + 29801428534987272000000000000000*vx + 2483452377915606000000000000000*vy + 78145814915083155379470685018969 >= 116225571286450360800000000000000*y & 868278006904299738474440588313318166*x + 28643823306457642801659440590359180*vx + 118254285424829307688083083199318955*vy >= 1655047678849147183144624333239196628 + 69042652419923862500571818302400802*y & 146612133187237806767075300894718*y + 3053969736141995769583268887006706 >= 1287774778139523210459045704215921*x + 92836935729566959016182808036430*vx + 1114043228754803508194193696437160*vy & 44229126502804712605046358965868912303600000000000000*x + 1914578513622346127503165317012164474250206530178267546*vy + 3541086244110842919557486437896650788918303265089133773 >= 139521064289963363797034651673449143962000000000000000*y + 3142407339576963671049186378527291543546400000000000000*vx & 3455844627570866805468916690200843*y + 1160324138792791470000000000000000*vy + 94284594121739694062404943136885702 >= 31370142620370629790000000000000000*x + 35528258309527259032812314788665730*vx & 729577117427919643356204098482663518370007228961050400000000000000*x + 514442688092487905247550507648329706438467099200808000000000000000*vx + 1870710557507486265015907944827342354794890330669360000000000000000*vy + 2406979389096700367840257650556298122098850568299084797159718982941 >= 2188731352283758930068612295447990555110021686883151200000000000000*y & 1358306642283590991321702509457781753*vy + 97503645416707618300555774527357840553 >= 31349426488451517109950000000000000000*x + 4165718184191858348340000000000000000*y + 26404314027236514552600000000000000000*vx & 53164546559475666716810169232469754900*x + 242862695713188426651726277660944730*vx + 5813158945350445098058406941523618250*vy >= 105638007514227493478034104560974465556 + 585392686810463068413082482877684447*y & 21581173970026287584883476315211*y + 72520258674549466875000000000000*vy + 6054189697802011407598579327778999 >= 1960633913773164361875000000000000*x + 2154503044225708971433462804094210*vx & 38741857095483453600000000000000*x + 29801428534987272000000000000000*vx + 78145814915083155379470685018969 >= 116225571286450360800000000000000*y + 29801428534987272000000000000000*vy & 39080394357587314073617958573718048026202329492592000000000000000*vx + 129863179138755360553412236445810464027715184239995704066440321783 >= 39728647344561511226497877317831854510049287564744000000000000000*x + 43005653731170302813080922984500455589136193001885800000000000000*y + 35859499187932506445481680429883696922415902838146000000000000000*vy & 36663036599972636310400377953927745869202636631846*vy + 131309884414207412149330066035670705259601318315923 >= 20548820659841876420687265291374340375000000000000*x + 2636452462017448295484403848704632350000000000000*y + 80764929240336365907728700240224689125000000000000*vx & 70534041918809154040123076069987451246826179543*y + 4991877897376467167535986557072996125000000000000*vy + 417894585324802854035901598985658243977470383729239 >= 134958772595301705099007998035872429125000000000000*x + 147791538810989300265496803104478538215551945466830*vx & 12624216254404330500000000000000*vx + 253283286932525514380846280409421 >= 81384803967942671625000000000000*x + 50310606089273651550000000000000*y + 40873487053194348750000000000000*vy & 1087641123027139594913166855653758650000000000000*y + 912705837505291967759300857891266000000000000000*vy + 12216741047677461634959100782231165936253173820457 >= 3657492520283445059538460536816292875000000000000*x + 6404802031694252613092051870868850250000000000000*vx & 11*x + 10*vx >= 26 + y & 223323032076772090911620090713804152000000000000000*x + 10430169133032364501707288983450448867039466299816446*vy + 19328703861078159820954391600743949603119733149908223 >= 759298309061025109099508308426934116800000000000000*y + 17118916239105640881356313174555096288000000000000000*vx & x >= 2 & 36082900578171247319841525123435135011603758412776424142250946461304412072454307400000000000000*vx + 104348229835620604516802520417242157569043704694012731914549203668390358155132413145316615993769 >= 34951859808981757637551132536635928764280987140410736220067675434218240000916792000000000000000*x + 29283002540399713728741975851860492487794259699032606577335009015109647489697408940000000000000*y + 34245827534391460755188138615067740900896010790238153444899582784640721787729073400000000000000*vy & 2024262033239010450600000000000000000*x + 1504475450541274114800000000000000000*vx + 7242705243318373917643405018915563506*vy + 11247668527549729510332149445432727331 >= 8331436368383716696680000000000000000*y & 2418141141545645251925096352049547800000000000000*x + 2029209349548793218398682253468152000000000000000*vx + 633603643107891420908223521122346000000000000000*vy >= 4917437940510330675833849065607798310510095930883 + 557403436774590383250000000000000000000000000000*y & 28600000000000000*x + 24000000000000000*vx + 2000000000000000*vy >= 70193604495161271 & 425580093518950905281250000000000*vy + 38660380577928211059537484692692051 >= 12499781062158176831240625000000000*x + 1559628788767483198050000000000000*y + 10531868822067027513656250000000000*vx & 3122630265077629298584410664575283645*x + 1684110651892037499117575013511116790*vy >= 2681702028219434988362417331583605910 + 1763003444044921144384786993062646524*y + 750824234274056949386011866500284972*vx & 5586943595726285423511213777194060122184606552938233917728234628*y + 1758391399333400392721239119730287792093225114466735830154124285585 >= 613082585596389918857657264529899287206118637862842107320063485448*x + 517532820510576702232051737456182766238153452568874144788086817925*vx + 42452807601572184052271205325700256492309869013393618081822621360*vy & 3382853383913434631200000000000000*x + 337301276162652511000000000000000*vx + 433511153402661345500000000000000*vy >= 6620591731865478354278513553131513 + 236337575642905393800000000000000*y & 39261491139448548409075707543867024274490556630000880800000000000000*x + 30053126173224044967573842064179431595761966638462216000000000000000*vx + 106191032311637302612210967454733602831295661269407858000000000000000*vy + 140566888526345836963877375170389696360985826668350429381298361686457 >= 124134568188836213617807647025915258423471669890002642400000000000000*y & 1666287273676743339336000000000000000*x + 8537039082788620429784199080703110578*vy + 13640574111934126470176899540351555289 >= 5665376730500927353742400000000000000*y + 5147143795610815021056000000000000000*vx & 1077112255733486897071375127212562022176838917958433100000000000000*x + 103005990395786641487963044713213453750000000000000000000000000000*vx + 139883740000487344905528323421235799177643282795350763318521605907*vy >= 1861112566242919459021943197050792748853677835916866200000000000000 + 248284131485442534053912124381532469625000000000000000000000000000*y & 95775383383737605876887549093661116733386422847125000000000000*vy + 8035104432676263967982811238428873685297401668567650128099934511 >= 2589351833526803739385008565686769097701554216736125000000000000*x + 28888597623236275253193862131057990077746578751050000000000000*y + 2809635215309400232901849928602189666188342989284512500000000000*vx & 1224161400163321506680846280409421 >= 402484848714189212400000000000000*x + 50310606089273651550000000000000*y + 338922264797204785500000000000000*vx + 27697392492586550250000000000000*vy & 4977568069083571082814016051603974136863193500462000000000000000*vx + 21665465905299163661104235900332431778992607086809870927851503601 >= 6998972759007997496533998922809968586952975238731500000000000000*x + 5931601948991255540353369128161402513095305588050550000000000000*y + 5947905169098791042978224955829943294915620455626500000000000000*vy & 1193580443520821836130846280409421 >= 392126782754632872375000000000000*x + 50310606089273651550000000000000*y + 329057440073817795000000000000000*vx + 27421453339484816250000000000000*vy & 377105345107657227750000000000000*vy + 31572427359244569727369123104974681 >= 10195296351620454681750000000000000*x + 11160253482033634076284239628659470*vx & 121*x + 120*vx >= 291 + 11*y & 14504051734909893375000000000000*vy + 1214543196058019190943346280409421 >= 392126782754632872375000000000000*x + 50310606089273651550000000000000*y + 329057440073817795000000000000000*vx & 1662919712252289777600000000000000*vx + 4942985845337469069533112669644311 >= 1448945455371081164640000000000000*x + 1789873797811335556320000000000000*y + 1352984855488422148800000000000000*vy & 5112477902651403236696673140723509400000000000000*x + 4368149769606015357123082355851896000000000000000*vx + 1293018208758151918510256862987658000000000000000*vy >= 10532632311240222473704333324682785176436796296659 + 1114806873549180766500000000000000000000000000000*y & 10410501028951126658704692043832810005293211903500000000000000*vx + 205973565359485503396743141502039192901625773546027660271437927 >= 67113598846475910795665904036676271058714025918875000000000000*x + 39497877238257097303916790173073030631750488749850000000000000*y + 35515702490968229833022068283472119484350972966250000000000000*vy & 27 >= 11*x + 10*vy & 49647689867862045788400000000000000*x + 41662397091912206256000000000000000*vx + 3471866424326017188000000000000000*vy + 109975910967631037469698328213500963 >= 156613957308491861178000000000000000*y & 1952363717898074622417119908401923300000000000000*x + 3380857848464447129031109133991703097372233083330*vy + 2618217575435311647720191282975147223956136091659 >= 438339029191446587100000000000000000000000000000*y + 5823609333570153774354431099778993823956136091659*vx & 1432678061313042698404083867037529609003343593415155*x + 322719192912742012912650342649330102847841802089240*vx + 98676248229448123391499137451355167655815435770780*vy >= 1947032343277618609003234914403337115437957609968438 + 777877618749643220603263253393425614906583028148036*y & 28 >= 9*x + 10*vx & 76556700725851145171985874996082075000000000000*x + 18999822407450249805380471781658000000000000000*vx + 5275694721682928713825555746795500000000000000*vy >= 107076822146485648197633567087185719583395565107 + 40113583408269524314095401408631300000000000000*y & 468911681642403315857570275604469783759521461371*y + 9427822696768758531787845710838369725900503452750*vy + 698294485800834559827187752199184003512063232470439 >= 224769989077097025051642271608183605625000000000000*x + 249223419328282913039760779258421262045822753931810*vx & 1532550372612759272456467346548253768287303328835791244725287623*y + 311443575049309331694075593734694670199672834098644985610735335750*vy + 23730700804643385934701351165027792861440997237636043613746672075079 >= 7641533565932725609548117198957744763198504960847707875000000000000*x + 8443603134979844139775249295269691318242066507725565047215919731630*vx & 411 >= 143*x + 120*vx + 10*vy & 118575081927381206125839544503972466229360655243892125000000000000*vy + 10643178639043906439557820427457058284939796907582460545324247900769 >= 3440480808535674044992219333664044948343963989762023600000000000000*x + 431001774553613311266438446439511990105495498720252950000000000000*y + 2897163423819064776946068402292427275768955690679559500000000000000*vx & 267459484709942709841925378452507372426961417686129125000000000000*vy + 22397120309629418696512581721992009469381389989219544205264865356319 >= 7230946853567143155381518822680927618159122180653410125000000000000*x + 917593840661903600711348914776011419718574747177534234375000000000*y + 6089316563381796204998741877186233232481281427755251718750000000000*vx & 1255812127923246831244323730519414723*vy + 100667604771864946767203395748419473523 >= 32468097612083601832650000000000000000*x + 4165718184191858348340000000000000000*y + 27343059026088613620600000000000000000*vx & 686783284350500835312929163609692826246826179543*y + 252688281994943056063647061169222284825152025928735 >= 87409163635266902445270037262441786669790527849838*x + 76063745913176317508853544764653525348652531966650*vx + 5218574008302204529139690803041120294216120828660*vy & 15960719440421518480670079111549313902582*x + 13989050238236250869350050359535260829390*vy >= 2695986593568258380855600156031384057159 + 15447499213960016974912081764738874066380*y + 1348529050674990675873267178074558496220*vx & 229689849164479367343190577459049800000000000000*x + 192746726571591077490789295769832000000000000000*vx + 16062227214299256457565774647486000000000000000*vy >= 491111568736332708624668096873436210046372357353 + 51569297551934892600000000000000000000000000000*y & 324488728945707926903303345458486043606803687619800000000000000*x + 157771998680199259183750085029599043586128968632000000000000000*vx + 31325903868268940584620472302104086965510747386000000000000000*vy >= 632225573528780059898059570697659210740684366119876991905843803 + 72853266594587301591756615874482600000000000000000000000000000*y & 2450422461289328440200000000000000000*x + 1862092592961121378800000000000000000*vx + 7223975142941356047488647461038829446*vy + 10013462863137410843183795195815954021 >= 8331436368383716696680000000000000000*y & 19364151332943889494835507041731800000000000000*x + 16143571465012694408253572342712000000000000000*vx + 1345297622084391200687797695226000000000000000*vy >= 41061474868141724293151645170312382731488396123 + 4550232136935431700000000000000000000000000000*y & 6018277411084660422111900413167392262041919347371300000000000000*x + 560576818480471518301839699119529000000000000000000000000000000*vx + 784328213085683415280186451289666277153172635269255418815623561*vy >= 10441387773330929904790837248787403324083838694742600000000000000 + 1351206157743904947232174826566163100000000000000000000000000000*y & 1531443392755478487818237493382512930936244782662200000000000000*x + 242623874292542888286803952215671270324606501471000000000000000*vx + 187660332087717403285862084970519125579654466912500000000000000*vy >= 2712922223605031276609313080329204492364556500014855563599080967 + 343835220808552856116802961580451400000000000000000000000000000*y & 2526588340809273040775096352049547800000000000000*x + 2106991095479313418398682253468152000000000000000*vx + 177580800254756432196221933414474000000000000000*vy >= 5395167657246833272289849859461734310510095930883 + 567262273071283818600000000000000000000000000000*y & 3416169884240640370530142740189655129674840563817800000000000000*x + 1632820323831436242702899030721581979447418654952000000000000000*vx + 331192425894361262490299046155424456620618221246000000000000000*vy >= 6612000440535747428417560940939840718147528027318646910964281833 + 787458102162083333381486950996245750000000000000000000000000000*y & 26599552557002097771176059872545025800000000000000*x + 22178378886889394534885504788149672000000000000000*vx + 1864141924458317867098951587660382000000000000000*vy >= 56573104441404215881868093294028493415611055239713 + 6131437804520494215750000000000000000000000000000*y & 16122812076551100742107923846236987090298692609284200000000000000*x + 2589189466974141627173137446843930473570671516181000000000000000*vx + 1968942458942413102663688962204163881376199136037500000000000000*vy >= 28444289196474407931562705160219774016010121500163411199589890637 + 3716454224915975724203679070023996750000000000000000000000000000*y & 2154224511466973794142750254425124044353677835916866200000000000000*x + 5306437709627643006155314584742391232903089697220469326637043211814*vy + 5858762304552486005000108257460123819390511340859636063318521605907 >= 496568262970885068107824248763064939250000000000000000000000000000*y + 9187306910571792340082956137594423136896322164083133800000000000000*vx & 1048264184860037216709529268613478971300000000000000*x + 1790708465703327626775327224169345437625822759748130*vy + 1359345708848337440362414809749057592639392347420699 >= 241634389841784931138875000000000000000000000000000*y + 3070365286257616324873723346976015535239392347420699*vx & 12036554822169320844223800826334784524083838694742600000000000000*x + 28633680876061689615449398410923970406032565225777910837631247122*vy + 30823322823983213618458476200549062030764766528661155418815623561 >= 2702412315487809894464349653132326200000000000000000000000000000*y + 49686065161715120702582764572411050475916161305257400000000000000*vx & 19364151332943889494835507041731800000000000000*x + 16143571465012694408253572342712000000000000000*vx + 5137157736197250950687797695226000000000000000*vy >= 39165544811085294418151645170312382731488396123 + 4550232136935431700000000000000000000000000000*y & 5902312579877317553343190577459049800000000000000*x + 5865369457284429263490789295769832000000000000000*vx + 16062227214299256457565774647486000000000000000*vy >= 14156975419999079247624668096873436210046372357353 + 567262273071283818600000000000000000000000000000*y & 8625371101895249996920485952521070127701148082301100000000000000*x + 840865227720707277452759548679293500000000000000000000000000000*vx + 1113302523308660840642247414574009953327630436325212919987781867*vy >= 14857991630532913584691526538721068455402296164602200000000000000 + 2026809236615857420848262239849244650000000000000000000000000000*y & 319679472370682381694835507041731800000000000000*x + 319492380594041474408253572342712000000000000000*vx + 81344250713437950687797695226000000000000000*vy >= 766065128686520508493151645170312382731488396123 + 31851624958548021900000000000000000000000000000*y & 104157559543548561*vy + 193570059543548561 >= 178825000000000000*vx & vy + 1 >= 0 & y >= 1 & 2*x0 = 1 & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 STATE 7: nav: Q_2_1 ==> 936650000000000000*y + 786000000000000000*vy + 1205505057056429875 >= 85800000000000000*x + 2328291623654809378*vx & 1299885830293521606000000000000000*vy + 109730905981152364232214666318774831 >= 35773307225922916735800000000000000*x + 4514733788941285775450000000000000*y + 30019558511263986072000000000000000*vx & 134693313485483813 >= 44687500000000000*x + 7150000000000000*y + 34625000000000000*vx + 4375000000000000*vy & 943358710166127699 >= 314600000000000000*x + 164450000000000000*y + 12150000000000000*vx + 124350000000000000*vy & 8709000000000000000*vx + 31865445803537009069 >= 10424700000000000000*x + 10853700000000000000*y + 8748000000000000000*vy & 506521138576353602364114314966784000000000000000*vy + 48310986703068994995137791257966180625980540535969 >= 15776376606105787477415215055926390200000000000000*x + 1931214176494056315950474978819241300000000000000*y + 13283934079167888240160797598885065000000000000000*vx & 4337626895572623756000000000000000*vy + 9998053445019399995960509481383109 >= 204983690041931658000000000000000*x + 5178419332231031918900000000000000*y + 172014285349872720000000000000000*vx & 46683187266332956625000000000000*y + 93891130753472193000000000000000*vy + 183243678534291123045977829704393 >= 10249184502096582900000000000000*x + 226198785235082626800000000000000*vx & 10817950000000000000*y + 9078000000000000000*vy + 12269307868493298778 >= 429000000000000000*x + 26360978672030307847*vx & 30500000000000000*vx + 585973829253224821 >= 196625000000000000*x + 121550000000000000*y + 98750000000000000*vy & 393000000000000000*vy + 962404622614512593 >= 42900000000000000*x + 471900000000000000*y + 3000000000000000*vx & 135587063485483813 >= 44687500000000000*x + 7150000000000000*y + 34625000000000000*vx + 2587500000000000*vy & 7150000000000000*x + 6000000000000000*vx + 500000000000000*vy >= 18905813485483813 & 847595474158798643850000000000000*y + 711268929364026834000000000000000*vy + 5302903815143815210824757599226993 >= 1494626785490712467880000000000000*x + 3484969515673341936700000000000000*vx & 8250000000000000*vx + 92404940456451439 >= 31281250000000000*x + 20556250000000000*y + 18000000000000000*vy & 3345815034429553797282168008961427 >= 1110337797811335556320000000000000*x + 139388909228513527440000000000000*y + 931751998163358508800000000000000*vx + 77645999846946542400000000000000*vy & 266000000000000000*vx + 6052000000000000000*vy + 13707312354985429903 >= 286000000000000000*x + 7235800000000000000*y & 517342440456451439 >= 171600000000000000*x + 21450000000000000*y + 144500000000000000*vx + 18000000000000000*vy & 8709000000000000000*vx + 32079945803537009069 >= 10424700000000000000*x + 10853700000000000000*y + 8319000000000000000*vy & 6052000000000000000*vy + 13850312354985429903 >= 286000000000000000*x + 7235800000000000000*y + 20000000000000000*vx & 7150000000000000*y + 6000000000000000*vy + 7314622997146237 >= 17195436482630050*vx & 31630592712701214375000000000000*x + 7488631919112680050000000000000*y + 523680553784103500000000000000*vx + 6284166645409242000000000000000*vy >= 74133645735017734452407291933291 & 213524677127012143750000000000*x + 7465897801643781250000000000*vx + 89590773619725375000000000000*vy >= 337811879090407861084146065201 + 67922929350576315625000000000*y & 4856712607671860076000000000000000*vy + 377338668269620196815567203770639981 >= 122905704445641068780400000000000000*x + 16029724561279055655600000000000000*y + 102016694320728235644000000000000000*vx & 838908729652601 >= 600000000000000*y & 2137458180672525267700000000000000*y + 4337626895572623756000000000000000*vy + 7686931564370389597760509481383109 >= 204983690041931658000000000000000*x + 10181525549858966296800000000000000*vx & 500000000000000*vy + 1088908729652601 >= 600000000000000*y & vx >= 0 & 17399903382057415453862903437892813 >= 5777171048102802605400000000000000*x + 707193730644664220100000000000000*y + 4864460407047682005000000000000000*vx + 396830713502226348000000000000000*vy & 172391618056770537500000000000*y + 358363094478901500000000000000*vy + 590139631146075714502438195603 >= 824235117301473450000000000000*vx & 38511424510148063800000000000000*vy + 3403893746608101100382168008961427 >= 1110337797811335556320000000000000*x + 139388909228513527440000000000000*y + 931751998163358508800000000000000*vx & 24680813485483813 >= 7150000000000000*x + 7150000000000000*y + 500000000000000*vx + 6000000000000000*vy & 798000000000000000*vx + 2652661566598379503 >= 858000000000000000*x + 943800000000000000*y + 720000000000000000*vy & 11970000000000000000*vx + 39049546672420843633 >= 12870000000000000000*x + 13758262656848370518*y + 11483278966806438860*vy & 634755268920148883038377140239143305452886659835394000000000000000*vy + 53545696066015197176781866745265057437256214561969352084284768969669 >= 17468684340705806420018496876180763275467369648403364200000000000000*x + 2085342468364993734037546287002178748421799717471264300000000000000*y + 14822226740527740676265750099936844792900872764747395000000000000000*vx & 4162745705466919824000000000000*y + 1205375464649802000000000000000*vy + 71232772331435880958690235890829 >= 24390587910177029640000000000000*x + 27162951478871574240000000000000*vx & 7073055553570794230144500988435406000000000000000*vy + 585574167883127977440289844213409745171126826856131 >= 194652932932404892542693873312955075800000000000000*x + 4986493218444470357391033075446163240000000000000*y + 179497091657171178034965264840716235600000000000000*vx & 46842688056923160575405540496012825000000000000000*y + 63674415946282786420877146609455312000000000000000*vy + 1423101319251889423099798629770912323438200144502727 >= 446970585579449925554626623169724798400000000000000*x + 593421742255900334322644060371472016000000000000000*vx & 16375000000000000*vx + 65104940456451439 >= 21450000000000000*x + 21450000000000000*y + 18000000000000000*vy & 93891130753472193000000000000000*vy + 233485458548400044745977829704393 >= 10249184502096582900000000000000*x + 112357628231570460475000000000000*y + 8600714267493636000000000000000*vx & 49837211854788464043500000000000000*vx + 197069101589798544189584376177199351 >= 64996806295145173213050000000000000*x + 64897121959357265842550000000000000*y + 54542774513408536962000000000000000*vy & 25428529645078527417000000000000000*vx + 103934057972759273397989146433700097 >= 34307673842123105381100000000000000*x + 33709567827395661158100000000000000*y + 28329574821222054414000000000000000*vy & 18149500000000000000*vx + 71119137418901422827 >= 23444850000000000000*x + 23516350000000000000*y + 19729000000000000000*vy & 26127000000000000000*vx + 94855960584056178295 >= 31274100000000000000*x + 32162362656848370518*y + 26927278966806438860*vy & 66500000000000000*vx + 697658710166127699 >= 235950000000000000*x + 157950000000000000*y + 138000000000000000*vy & 66500000000000000*vx + 707408710166127699 >= 235950000000000000*x + 164450000000000000*y + 131500000000000000*vy & 1396500000000000000*vx + 14819832913488681679 >= 4954950000000000000*x + 3453450000000000000*y + 2833000000000000000*vy & 246330813485483813 >= 85800000000000000*x + 72000000000000000*vx + 6000000000000000*vy & y >= 1 & 2*x0 = 1 & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 STATE 8: nav: Q_safe ==> 20495752025893774816798436774183033800000000000000*x + 17503359095869823338753932957356392000000000000000*vx + 5082788891500131897062827746446366000000000000000*vy >= 46793461534706094792198115846748333013756160945593 & 5902312579877317553343190577459049800000000000000*x + 5865369457284429263490789295769832000000000000000*vx + 16062227214299256457565774647486000000000000000*vy >= 14724237693070363066224668096873436210046372357353 & 5112477902651403236696673140723509400000000000000*x + 4368149769606015357123082355851896000000000000000*vx + 1293018208758151918510256862987658000000000000000*vy >= 11647439184789403240204333324682785176436796296659 & 319679472370682381694835507041731800000000000000*x + 319492380594041474408253572342712000000000000000*vx + 81344250713437950687797695226000000000000000*vy >= 797916753645068530393151645170312382731488396123 & 308555211944857581142214279307412189489904069117*x + 308461666056537127498923311957902289489904069117*vx >= 770747066221325240933567137051521915090504370854 + 1188381393316970200646155084507217268511603877*vy & 229689849164479367343190577459049800000000000000*x + 192746726571591077490789295769832000000000000000*vx + 59036641840911666957565774647486000000000000000*vy >= 521193658974961395974668096873436210046372357353 & 229689849164479367343190577459049800000000000000*x + 59036641840911666957565774647486000000000000000*vy >= 363391216769899729835411320307679710046372357353 + 122858157838532254787724257361681000000000000000*vx & 57751577098013494616611760561173*x + 60607547332616441516611760561173*vx >= 144874047157938498253857451979126 + 1865761408793423475343898847613*vy & 85800000000000000*x + 500000000000000*vx + 6000000000000000*vy >= 174830813485483813 & 28600000000000000*x + 24000000000000000*vx + 2000000000000000*vy >= 70193604495161271 & 242*x + 244*vx >= 605 + 2*vy & 121*x + 120*vx >= 302 & vx >= 0 & vy + 1 >= 0 & 0 >= vy & 6000000000000000*vy + 14730813485483813 >= 17461626970967626*vx & 27 >= 11*x + 10*vy & 411 >= 143*x + 120*vx + 10*vy & 22389136905521081704126786171356*vx + 48730270837053344859285268885551 >= 23141348211780359553782887323743*x + 27284285732506333207565774647486*vy & 12624216254404330500000000000000*vx + 202972680843251862830846280409421 >= 81384803967942671625000000000000*x + 40873487053194348750000000000000*vy & 909261363263329551718346280409421 >= 299767361281922173818750000000000*x + 309726640699485204080846280409421*vx & 14504051734909893375000000000000*vy + 1164232589968745539393346280409421 >= 392126782754632872375000000000000*x + 329057440073817795000000000000000*vx & 3200581869329233576350344187901424 >= 1287774778139523210459045704215921*x + 92836935729566959016182808036430*vx + 1114043228754803508194193696437160*vy & 11228114396905972064306711716654111 >= 3907033596401950779477226843762212*x + 3279356902467184966709961873314615*vx + 281946865586711805747274042153260*vy & 232064827758558294000000000000000*vy + 19548087749862112173574771965417309 >= 6274028524074125958000000000000000*x + 7105651661905451806562462957733146*vx & 362066661263612724750000000000000*vy + 25858015165230048439109464449416683 >= 8708174024569865863875000000000000*x + 7226639465369587159500000000000000*vx & 12576202841764628784000000000000000*vx + 28207634583948634093509341990953091 >= 12784812841509539688000000000000000*x + 11026528557945290640000000000000000*vy & 110357801823215457883152626358870408 >= 38404431278124311568805252534923719*x + 32218450823665284254501946360440090*vx + 2785108071887008770485484241092900*vy & 10410501028951126658704692043832810005293211903500000000000000*vx + 166475688121228406092826351328966162269875284796177660271437927 >= 67113598846475910795665904036676271058714025918875000000000000*x + 35515702490968229833022068283472119484350972966250000000000000*vy & 723720418946518432280094309456022987539523201690715625000000000*vx + 1662077381514142287897340405075840655440505356108330078263368887 >= 771856524116951225967510081038128040634062981251685156250000000*x + 756728411112432375456957766931922505872386495576020312500000000*vy & 57821897596863176026391028920269178926580178592909800000000000000*vx + 120290049197854749121472550774474182760809973060514044730843539613 >= 56009434560742520056645186837299263610542163212184000000000000000*x + 54878036440655202601166065620816464135711124221491800000000000000*vy & 101066476559538818314033248285954239711774375581488000000000000000*vx + 221227548637675357477391070242435727920202037840930055269156460387 >= 102742934701521689707867923020555376389457836787816000000000000000*x + 99529232554019642677555114723603723726423882357080000000000000000*vy & 1763978342929126678144750333507481852215409721019674064071852520213 >= 613082585596389918857657264529899287206118637862842107320063485448*x + 517532820510576702232051737456182766238153452568874144788086817925*vx + 42452807601572184052271205325700256492309869013393618081822621360*vy & 2*x0 = 1 & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 & y = 1 STATE 9: nav: Q_safe ==> 31630592712701214375000000000000*x + 523680553784103500000000000000*vx + 6284166645409242000000000000000*vy >= 66645013815905054402407291933291 & 7150000000000000*x + 6000000000000000*vx + 500000000000000*vy >= 18905813485483813 & vx >= 0 & 500000000000000*vy + 488908729652601 >= 0 & 0 >= vy & 6000000000000000*vy + 14464622997146237 >= 17195436482630050*vx & 17530813485483813 >= 7150000000000000*x + 500000000000000*vx + 6000000000000000*vy & 8250000000000000*vx + 71848690456451439 >= 31281250000000000*x + 18000000000000000*vy & 393000000000000000*vy + 490504622614512593 >= 42900000000000000*x + 3000000000000000*vx & 246330813485483813 >= 85800000000000000*x + 72000000000000000*vx + 6000000000000000*vy & 786000000000000000*vy + 2142155057056429875 >= 85800000000000000*x + 2328291623654809378*vx & 30500000000000000*vx + 464423829253224821 >= 196625000000000000*x + 98750000000000000*vy & 66500000000000000*vx + 542958710166127699 >= 235950000000000000*x + 131500000000000000*vy & 66500000000000000*vx + 539708710166127699 >= 235950000000000000*x + 138000000000000000*vy & 266000000000000000*vx + 6052000000000000000*vy + 6471512354985429903 >= 286000000000000000*x & 778908710166127699 >= 314600000000000000*x + 12150000000000000*vx + 124350000000000000*vy & 9078000000000000000*vy + 23087257868493298778 >= 429000000000000000*x + 26360978672030307847*vx & 798000000000000000*vx + 1708861566598379503 >= 858000000000000000*x + 720000000000000000*vy & 2394000000000000000*vx + 5058256803114494623 >= 2574000000000000000*x + 2296655793361287772*vy & 8709000000000000000*vx + 21226245803537009069 >= 10424700000000000000*x + 8319000000000000000*vy & 26127000000000000000*vx + 62693597927207807777 >= 31274100000000000000*x + 26927278966806438860*vy & 1205375464649802000000000000000*vy + 75395518036902800782690235890829 >= 24390587910177029640000000000000*x + 27162951478871574240000000000000*vx & 1299885830293521606000000000000000*vy + 105216172192211078456764666318774831 >= 35773307225922916735800000000000000*x + 30019558511263986072000000000000000*vx & 49837211854788464043500000000000000*vx + 132171979630441278347034376177199351 >= 64996806295145173213050000000000000*x + 54542774513408536962000000000000000*vy & 4856712607671860076000000000000000*vy + 361308943708341141159967203770639981 >= 122905704445641068780400000000000000*x + 102016694320728235644000000000000000*vx & 7073055553570794230144500988435406000000000000000*vy + 580587674664683507082898811137963581931126826856131 >= 194652932932404892542693873312955075800000000000000*x + 179497091657171178034965264840716235600000000000000*vx & 2*x0 = 1 & 2*y0 = 1 & 2*vx0 = 1 & 4*vy0 = 1 & y = 1 */ digraph G { s0 -> s1; s1 -> s3 [label="north"]; s1 -> s2 [label="east"]; s2 -> s4 [label="north"]; s3 -> s5 [label="east"]; s4 -> s6 [label="east"]; s5 -> s7 [label="east"]; s6 -> s8 [label="south"]; s7 -> s9 [label="south"]; s8 -> s8; s9 -> s9; s0[fillcolor=red, style=filled, shape=Mrecord, label="s0|{Q_hub}"]; s1[fillcolor=green, style=filled, shape=Mrecord, label="s1|{Q_0_0}"]; s2[fillcolor=blue, style=filled, shape=Mrecord, label="s2|{Q_1_0}"]; s3[fillcolor=yellow, style=filled, shape=Mrecord, label="s3|{Q_0_1}"]; s4[fillcolor=cyan, style=filled, shape=Mrecord, label="s4|{Q_1_1}"]; s5[fillcolor=cyan, style=filled, shape=Mrecord, label="s5|{Q_1_1}"]; s6[fillcolor=magenta, style=filled, shape=Mrecord, label="s6|{Q_2_1}"]; s7[fillcolor=magenta, style=filled, shape=Mrecord, label="s7|{Q_2_1}"]; s8[fillcolor=paleturquoise2, style=filled, shape=Mrecord, label="s8|{Q_safe}"]; s9[fillcolor=paleturquoise2, style=filled, shape=Mrecord, label="s9|{Q_safe}"]; }