c model ISR_TJ
c  /home/toda/src/NuSMV-2.6.0-Linux_untouched/binary/bin/NuSMV -bmc -bmc_length 20 -n 0 /home/toda/2022solver/bin/../tmp/DSJC250.9_02.smv > DSJC250.9_02.log
c ECC Heuristic Algorithm by Alessio Conte, Roberto Grossi and Andrea Marino. University of Pisa.
c This code is compiled using Java 1.8
c Parsing: 250
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 27897
c 0 cliques
c 2 cliques
c 4 cliques
c 8 cliques
c 16 cliques
c 32 cliques
c 64 cliques
c 128 cliques
c The solution is correct.
c Cliques: 229
c Sum: 5123
c MaxSize: 0
c Time: 427
c Aborted: false
c ML = 249
c SIZE = 250
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,14][3,11][4,6][5,7][6,2][7,3][8,1][11,2][12,2][13,1][14,2][15,5][16,2][17,2][18,2][19,3][20,4][21,2][22,3][23,6][24,3][25,5][26,13][27,22][28,22][29,21][30,22][31,25][32,8][33,4][34,3][36,1]}
c NODE covering index distribution:{[15,1][16,4][17,14][18,28][19,40][20,38][21,50][22,34][23,18][24,12][25,6][26,4][28,1]}
c EDGE covering index distrubution:{[1,7502][2,8987][3,6536][4,3276][5,1156][6,336][7,89][8,14][9,1]}
c Total edges:27897
c Distributions saved!
c *** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015)
c *** Enabled addons are: compass
c *** For more information on NuSMV see <http://nusmv.fbk.eu>
c *** or email to <nusmv-users@list.fbk.eu>.
c *** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
c 
c *** Copyright (c) 2010-2014, Fondazione Bruno Kessler
c 
c *** This version of NuSMV is linked to the CUDD library version 2.4.1
c *** Copyright (c) 1995-2004, Regents of the University of Colorado
c 
c *** This version of NuSMV is linked to the MiniSat SAT solver. 
c *** See http://minisat.se/MiniSat.html
c *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
c *** Copyright (c) 2007-2010, Niklas Sorensson
c 
c -- no counterexample found with bound 0
c -- no counterexample found with bound 1
c -- no counterexample found with bound 2
c -- no counterexample found with bound 3
c -- no counterexample found with bound 4
c -- no counterexample found with bound 5
c -- specification  G ((((state.token[1] = v3 & state.token[2] = v69) & state.token[3] = v154) & state.token[4] = v223) ->  G !((((((state.token[1] = v3 | state.token[1] = v39) | state.token[1] = v186) | state.token[1] = v238) & (((state.token[2] = v3 | state.token[2] = v39) | state.token[2] = v186) | state.token[2] = v238)) & (((state.token[3] = v3 | state.token[3] = v39) | state.token[3] = v186) | state.token[3] = v238)) & (((state.token[4] = v3 | state.token[4] = v39) | state.token[4] = v186) | state.token[4] = v238)))    is false
c -- as demonstrated by the following execution sequence
c Trace Description: BMC Counterexample 
c Trace Type: Counterexample 
c   -> State: 1.1 <-
c     state.token[1] = 0ud229_205695133799314420120060905042671130622624406171847384478777344
c     state.token[2] = 0ud229_115699723277674148500564470076432600993699593911256069223481344
c     state.token[3] = 0ud229_6753151531824046293356158404452297062861313188195708645003883446272
c     state.token[4] = 0ud229_52707869354868719306268314132000914833752356098554133244509421568
c     state.tid = 1
c     state.vid = 88
c     state.target = 0ud229_0
c     v250 = 0ud229_216209432263904490003069170770534859820992494896987802477443825009156
c     v249 = 0ud229_458322590063902630872883002598149797792024267769869412159709239050240
c     v248 = 0ud229_216006205991931458968034005855295912815964947533118739557369595822080
c     v247 = 0ud229_136484736631069552515147847620570011230838158050620793412765242949632
c     v246 = 0ud229_54025225110142711176597578204393415262890889505952237344012481069312
c     v245 = 0ud229_6754797017647814292428493186177125749638008376726786919775600640000
c     v244 = 0ud229_1686645388373109226751339929160212546463434611979040752631742988288
c     v243 = 0ud229_20233127252316336430281010852155830367417596329402438210606434615296
c     v242 = 0ud229_431359355803901025194591577356123974635695471108778023588052993048576
c     v241 = 0ud229_111209780129108468535627489740406744091133933805957606645426598969344
c     v240 = 0ud229_41283241914930507607959377087970395142610414067103122544443716042752
c     v239 = 0ud229_434414810073912509080163431787907800054037207077099089776456237056
c     v238 = 0ud229_53946221432523033922598560180696032948636670616132382959682042462208
c     v237 = 0ud229_215692739482771882498918486875371681740225893285703260816806640615424
c     v236 = 0ud229_13480954369252154245703374345611089676755290633825134717913366790144
c     v235 = 0ud229_842550163377869799204525872665672191623528553351318625641438380032
c     v234 = 0ud229_107841432977416605237025256761137051649152664930738573449014271803392
c     v233 = 0ud229_13901646757002214644945319035424736531258497054068965597916673605632
c     v232 = 0ud229_107848168507658419535090260337797683562913897096654372283368672854016
c     v231 = 0ud229_14460694100740210311765203371928163346060213988875431194194471813120
c     v230 = 0ud229_8424983534462265974888930303925531761524455112471619707273438363648
c     v229 = 0ud229_26973939896293096608681762052842756734557214222448754139147605639168
c     v228 = 0ud229_289608809934933378263728854441972095470244842267455670659942711296
c     v227 = 0ud229_7419233147485129372508570435741318459432584783871772868103634948
c     v226 = 0ud229_212286169930227094831208155691361378461716137709183775211641634816
c     v225 = 0ud229_213941504376769299217132524469003062139140350550656078942568448000
c     v224 = 0ud229_6749911116345929172994565313002771326056865968316343344222512873472
c     v223 = 0ud229_52707869354868719306268314132000914833752356098554133244509421568
c     v222 = 0ud229_431359230235582395528508520504764249025742160112598632549444367679488
c     v221 = 0ud229_13690604369969958892476792657973324403022164543153996909308322775040
c     v220 = 0ud229_53478911059560020586337486216705675633828432650597042588479389696
c     v219 = 0ud229_54762404642419215689129835196691521569379875925659759610809410387968
c     v218 = 0ud229_211061670540705793822033547434103207703985959893203066014257905664
c     v217 = 0ud229_948247712754297672883928130276305464158177027969766190809838845952
c     v216 = 0ud229_108109650238407777042401370325751602281667059629301457126423284154368
c     v215 = 0ud229_5055401378584755041544323301106555564764119352380963526659054501888
c     v214 = 0ud229_16007468835788892586246516255655190245780287612536921580734926290944
c     v213 = 0ud229_431885708448177385039202594072934178648152682077892781820946187026432
c     v212 = 0ud229_111315156571579061011284582546357721926259450358062531041743329034240
c     v211 = 0ud229_16849966667410700342394226830806034913038436128162655857027552657408
c     v210 = 0ud229_432201645224331203598887126198424971279109519777258443277968254959616
c     v209 = 0ud229_7582491832761361648676899020058124645313703796076992310043171880960
c     v208 = 0ud229_215681236518083991707345378970828438456342178631482400208287680167938
c     v207 = 0ud229_53926732567759111915816097337953856376084264074477471805346888548384
c     v206 = 0ud229_3491040762416291146030686341525971716563280414466062310116186652672
c     v205 = 0ud229_27180151815209393642154432871898108928063344647045083782822494208
c     v204 = 0ud229_107945921712623337876781990308955510314072749032999212990701640876032
c     v203 = 0ud229_1686847872025990643200221186372504485073741982420024811927170449408
c     v202 = 0ud229_26966532301382843621287723501603401669257348195630952261708293341696
c     v201 = 0ud229_223262109784467155008603002411763125852202351240232868766063643328512
c     v200 = 0ud229_1685305255295725673152863975690673471489528991349660559935952388096
c     v199 = 0ud229_431806730367256040184098295004217250770011716865371217255158624813056
c     v198 = 0ud229_1270335952282807025694717396094797802279994328137369804705917566976
c     v197 = 0ud229_60663174224084363759047854780197082888606631938293155132746317694976
c     v196 = 0ud229_26381102706289396054889992932502788313765955898900450745115475968
c     v195 = 0ud229_5054992410507772577578758059384029972153607345628009166336149159936
c     v194 = 0ud229_6740000376174009462454315385226127754613423918243329339925056192512
c     v193 = 0ud229_78985022229635238298901192221967770390276241926938679312098787328
c     v192 = 0ud229_108050822678308125714246601621194914982040450292780571903058818105344
c     v191 = 0ud229_57513688946662245583773615110298483974679489123961915621972874625024
c     v190 = 0ud229_27499878706846047409746171666868765063403961900593065361036955090944
c     v189 = 0ud229_1059704986308639917304742210394316634468471828089329260752409722880
c     v188 = 0ud229_107839903975079888954093856699951771587074648226459026719141846319104
c     v187 = 0ud229_434755468483485567523088635116819660739937419957087284401011058278400
c     v186 = 0ud229_1234542804788159516759914670012701119841628593228647515159527424
c     v185 = 0ud229_1902205680251915971585030054446296535454651409524645050336724125696
c     v184 = 0ud229_215682864349495103502728098711774083560748326523309482002594154938368
c     v183 = 0ud229_54762805554629959274431633526821034826746144485957678100618003087360
c     v182 = 0ud229_844350335783681678167667412688760192595557161276788689483138596864
c     v181 = 0ud229_3475306428580648198693826959561831597921769227786229763532316999680
c     v180 = 0ud229_219049576313821063124976542050689094633802964164106557087652669030400
c     v179 = 0ud229_107840018682837106081983531389034179759916159852795848156567385931776
c     v178 = 0ud229_222420485628553278686551699115420470345520323413063497127947577327616
c     v177 = 0ud229_114579786197386224520821542731966507624277356182603581415372984680448
c     v176 = 0ud229_27066930577725792722919466670322199236580436943012309005821297295360
c     v175 = 0ud229_431385680435397616222080344539600340368504522496598590813238550593536
c     v174 = 0ud229_13484909948073469593267554487066952031914371908763564940860118335488
c     v173 = 0ud229_539253647248337993267954508984317788400754519662847161251260461481984
c     v172 = 0ud229_107867969148611266615281798755550195463172551758092549228071984562176
c     v171 = 0ud229_215705914265627761145823728128651831565088970499675308462642747670528
c     v170 = 0ud229_26960100933206771110526009996581105754095645515980222569247317966848
c     v169 = 0ud229_54130518124979677096036822303909148983514996888195695633687946199040
c     v168 = 0ud229_131653646939098742516580229120998352738021156375059655219344445440
c     v167 = 0ud229_431793561486050462556230838598082368938821763133798912950678780379136
c     v166 = 0ud229_874174297154801535072093952460675328233639175648854085432508416
c     v165 = 0ud229_647038746174575390408583853072704347165328309642982498533130968760320
c     v164 = 0ud229_107840616051072992789567451148224304595572982134813838482010890305536
c     v163 = 0ud229_34226597637100579915100760121813582848504837193724606178239258296320
c     v162 = 0ud229_10320630294529240090753645266008012070896111576359834534415215624704
c     v161 = 0ud229_108261039463441686830087451164625381348043826406841294350994806669312
c     v160 = 0ud229_431372310911786658288475327579215150041983420205472220277554794201088
c     v159 = 0ud229_121326354904166330008783067340544892510016586525808018787258886782976
c     v158 = 0ud229_13483277399061585758521850294205769765253632835355359906198003400704
c     v157 = 0ud229_13481618940258240008989043766072872679250185252692312897390018297856
c     v156 = 0ud229_26960158808231074982603992890121070268256718379403275812862686134272
c     v155 = 0ud229_14007357544222822622867180335758503804436066535358349781080154832896
c     v154 = 0ud229_6753151531824046293356158404452297062861313188195708645003883446272
c     v153 = 0ud229_3370459351703862597871447539504201933569551771875937801620611399680
c     v152 = 0ud229_1895634105636654712356823796512983128468865866269463929117099425792
c     v151 = 0ud229_108024083279456449651709569496510550592196201614232176885407644909568
c     v150 = 0ud229_1737729970690247881457850692615733808221286316967836201449695477760
c     v149 = 0ud229_3584011820294158990287089541402777996247409634772503668052285456384
c     v148 = 0ud229_431359165961590270688484338705167229833456611595315354286061944569856
c     v147 = 0ud229_53949518844871025422861267324657509670519548273005871211571012698112
c     v146 = 0ud229_60659982958111609618719908603613554588764158479417381369130147381248
c     v145 = 0ud229_433044143441740006905654412811819987370191065906630676729644491735040
c     v144 = 0ud229_219049592384761616107197367565367938621036890868192109119210507997184
c     v143 = 0ud229_3476128415003849808512838036112098893724170633435463659059685621768
c     v142 = 0ud229_4114062694186314214484056725867225233261519456702557225201172480
c     v141 = 0ud229_26961606634150503052770021381240669056789874036331886561533859201024
c     v140 = 0ud229_216101034620590048677174222846880871695919975419298770766846574460928
c     v139 = 0ud229_215681270270070750049432966746380376697407074274940259254738784092160
c     v138 = 0ud229_6993595824734501569391036516366585398994363234074889946723778560
c     v137 = 0ud229_438954808976482604695850657791822766768656120053627567263354565165184
c     v136 = 0ud229_107843078493740451323427249132521087815339666637387959868682538065920
c     v135 = 0ud229_431372311564573816529521807936077280504095218343294063842787405594624
c     v134 = 0ud229_13486581565091818313895575034149412564198561437777289453710233042944
c     v133 = 0ud229_121319811474412493165730220356169325297925680576451974304736915488768
c     v132 = 0ud229_7161648016208987299011811414735067764096794973998369574518144368640
c     v131 = 0ud229_3370829192260914438891163108377480054235670319001161575630717059072
c     v130 = 0ud229_6741632585635228232595847345255395872866821541315544887053638451200
c     v129 = 0ud229_107892449355961531652444418151149942942370938665619895030297363742736
c     v128 = 0ud229_438101190229839005061180203887440849866157160142002250039259803156480
c     v127 = 0ud229_269599884478597755974211958833880555389573056272113097077010435407872
c     v126 = 0ud229_15168288346361142237353108175238857251551294719970616558904095539200
c     v125 = 0ud229_67399970140013924465028773448588607695974849105772083822211786342400
c     v124 = 0ud229_222420386773812906674288136066226018156477786687926494955606665854976
c     v123 = 0ud229_28750265342474196044192299718775900295380528678753609308081676615680
c     v122 = 0ud229_215791467773527712519178468787671325628090037985504162093783880564736
c     v121 = 0ud229_121770651552254772224137505641931210330983319069999755088253419520
c     v120 = 0ud229_27190317355392805741175101104755070581605016022353190231918218575872
c     v119 = 0ud229_20219961615156596247651776555778014770974411900096954803269903843328
c     v118 = 0ud229_1738065092597717651606324387353918751116242226253846504021109506048
c     v117 = 0ud229_53920414082673507233085425693727046944712878694662930140765783851008
c     v116 = 0ud229_55953632919641979979853757656773426062687064984925921870964850688
c     v115 = 0ud229_1349315846164934194560522488223294925628940812704734021369817202688
c     v114 = 0ud229_3376576960154955168329447829262392020481904288334545191688365670400
c     v113 = 0ud229_57401780977692575944840583631209551159452042561467298038634017457152
c     v112 = 0ud229_54314710097920074778710456621502089735151110999738200028652503048
c     v111 = 0ud229_54354306588438618897874920365627261695408123198795624488490216980480
c     v110 = 0ud229_54025215270736655442539522579060643350141509184163395766727982710784
c     v109 = 0ud229_13533093922167107504784989103203552976737818935286385648354226864192
c     v108 = 0ud229_26974763038097642456795390941782985078075940013447589497274158284800
c     v107 = 0ud229_8438714620672694848992815134692282173082850842560658756034281603072
c     v106 = 0ud229_868929352701781406318548947440054823468422052756893308139840995328
c     v105 = 0ud229_219049592394557345568958684379669175869221202207405117241451429756928
c     v104 = 0ud229_107849661303480671440050265446830198181864440972015639842069814444032
c     v103 = 0ud229_107853169251970002041449357594405719157701654162910324084644008427520
c     v102 = 0ud229_424745914101403371055154534087846581519684051974075688791446650880
c     v101 = 0ud229_6792642877158398245136875413474930956182322890286745422663677673472
c     v100 = 0ud229_458582387139670463038212896191128327812378436146698244714331727986688
c     v99 = 0ud229_107853053555385324668894805816114340656568928323291732778227905593344
c     v98 = 0ud229_13273308641370225115472222665358511255601987042454173040838180864
c     v97 = 0ud229_109946032905283619443851602209054476871564938581354701895416007360512
c     v96 = 0ud229_54314531007832919838603972711385573133592677039929617735319814144
c     v95 = 0ud229_448399993451571530563603014519106396398400627699088696410892140544
c     v94 = 0ud229_26966940080350563121147336886945088980821985581988115411003452162048
c     v93 = 0ud229_60659880208264139798848610217170054710477656824151303585955175202816
c     v92 = 0ud229_108052879734752467253654037806632431227832735692588647890790396329984
c     v91 = 0ud229_215686438211054259791316926801470951934410886079768375637529843466240
c     v90 = 0ud229_30330569920653203239556733339356188189824939242195278815711213912064
c     v89 = 0ud229_242850375987715263074861905154299192619322064003451587454295263412224
c     v88 = 0ud229_444846119831675624208954182248068396567414532838844193487797234958336
c     v87 = 0ud229_431570645432448007176441782920663393174422495551385850112758966648832
c     v86 = 0ud229_256119802673504993095098763985214668580316059213056052603306333175808
c     v85 = 0ud229_216548425684476354439192091393327348035803869124916617251633967923200
c     v84 = 0ud229_431362492319540983578618288923144100474963827882205617390640097787904
c     v83 = 0ud229_6845504700273613800514835922786181690297336025645988965532762636288
c     v82 = 0ud229_228343787786880772211185548794730629505375996759982989455136798015488
c     v81 = 0ud229_215891843629326040068916372435795905811979633223093536723582580686848
c     v80 = 0ud229_431465391794006574416226167914040705532059970191292267433317564940288
c     v79 = 0ud229_2106670165571055518402966990312896558996399661970499488291343040512
c     v78 = 0ud229_458319093793518343505592596790657590058692333618362022871344313532416
c     v77 = 0ud229_229192868138067738666623095382626622684578566767370279163035713011712
c     v76 = 0ud229_121425123715964998004568708223887980747418761719005535373283993583616
c     v75 = 0ud229_13519465461782334809216871674582693449988353442993354932913493245952
c     v74 = 0ud229_216100823310928470379396518542941102267856742884010871718337310621696
c     v73 = 0ud229_14059190937997973198710404133514826549238970708361191187661472137217
c     v72 = 0ud229_427986254424802709527660806132718113107884049657625074940053028864
c     v71 = 0ud229_13485321224171251560201260492200002867796597333420588962655663816704
c     v70 = 0ud229_215679579967394215855551638451649446559095007134803586429818788381696
c     v69 = 0ud229_115699723277674148500564470076432600993699593911256069223481344
c     v68 = 0ud229_53273712260454231191054582967110859310262482384556576373532073984
c     v67 = 0ud229_431466131085547473148448803412598777139986414082713214686752642433024
c     v66 = 0ud229_431411909279890047082081499408100158567884166330876652440883967295488
c     v65 = 0ud229_21066162325903460672624078477858798410313651293525448232284656238592
c     v64 = 0ud229_26960052750967631770296050905058024668660625941668401912631577804800
c     v63 = 0ud229_27039342274620159299863986539377561955843959081928051459965669343232
c     v62 = 0ud229_27907757342391126304756519378633045954952214517353086854012996681728
c     v61 = 0ud229_53953009113517392911586030900034862720684032276681217722800150675456
c     v60 = 0ud229_223789825023833674256581780989674113996375817391621789803366842370
c     v59 = 0ud229_1741020954671961547037455267248188730962078677741469029796348428288
c     v58 = 0ud229_1685819421721861487907810427271319491073715430197627800415107022848
c     v57 = 0ud229_868879538800946339007130746971100277970679170388563996914634194944
c     v56 = 0ud229_3396328260921416581214509226540480513885576171916602458562224979968
c     v55 = 0ud229_13690601256331335717201089533755492264770089582457129313808525819904
c     v54 = 0ud229_3396325777527696237224389910722385557881984013219528261937806704644
c     v53 = 0ud229_431991022045095094307101105053903267240924268305246995129538592112640
c     v52 = 0ud229_53972756775290638595432926092192584273837706724314196058266077757440
c     v51 = 0ud229_825168962828727675311757765807453307731830935958571149137281024
c     v50 = 0ud229_2001036385789523971164623210489139310954162624392448506843679948864
c     v49 = 0ud229_431359353970204194158944013423995212086436234304647865041193158049792
c     v48 = 0ud229_13506301607378107853099814891402452429873235468509259105850707935266
c     v47 = 0ud229_4265250858263303858750245623202508351443259078033529294694855475200
c     v46 = 0ud229_431596101041959375126858686333076485915483140243874422911761687511040
c     v45 = 0ud229_26963263792159340028318336703127474745531878723656345606001034526720
c     v44 = 0ud229_1263760431060752366225056054899939631473376459356362470046310596608
c     v43 = 0ud229_7446958914887588221171762611642487545591673227771698145707163648
c     v42 = 0ud229_67413040346012498500266070494856303821982465621348633270262328983552
c     v41 = 0ud229_107899024848375734385693215353222834650256248078221229441448757166080
c     v40 = 0ud229_54304864469983715077070491438518941899682165001983122725524209664
c     v39 = 0ud229_6740012478254517424234456671883939635397135642647917809141689614400
c     v38 = 0ud229_1685102925499818070790663605245675094664478380153561068743279247360
c     v37 = 0ud229_27170623099374141075139778355547768202855165259260065810442329522432
c     v36 = 0ud229_447605010274107080559983329550644028166853363922755422167813324800
c     v35 = 0ud229_431412654497481915529482247584116209273826727364480481165240160485376
c     v34 = 0ud229_106985165370241827017534893507534621516698053203235288467457974272
c     v33 = 0ud229_54342839429119521310654441699354373002092948490353651745034959060992
c     v32 = 0ud229_222472318997798894464827858921720962634085407701977077012341597405184
c     v31 = 0ud229_3371696687727066106592123911998823282880199255852193273081623478400
c     v30 = 0ud229_862347232074666000432757471581311134234541911076874431816955592704
c     v29 = 0ud229_105325575585104704721628544405361788088965687115343940589042270208
c     v28 = 0ud229_3374209948237642159920506180610400967539367710609060294302799757313
c     v27 = 0ud229_2527909590061560550302364532058681426313362968900095200870247956480
c     v26 = 0ud229_60785145240767589422917123915387128751119202725783418829752716230656
c     v25 = 0ud229_1701863091548020382355295989707163158662208760543853317293904756736
c     v24 = 0ud229_55608798124539131226837828581039753737517603479340384127251107545088
c     v23 = 0ud229_26965294607671446411850834396188187830890169336653141938028266127360
c     v22 = 0ud229_54343199383290475228734305376092978644126383879036816004598951051264
c     v21 = 0ud229_7583519868285696042235540944379006512285034389668828942458932953088
c     v20 = 0ud229_27223227396542724096485114934322617958444124189815712786342349897728
c     v19 = 0ud229_1698167162710009141451307062684454664694814897275908830942271127552
c     v18 = 0ud229_27065670593104336197420770670553487802992548386506122889577057222656
c     v17 = 0ud229_6766316397251976636130752426877441005350866946314579801854374314000
c     v16 = 0ud229_80883131012141967212101934209628250697541105194963500611789517750272
c     v15 = 0ud229_53972555908406486083121953852659743112847388923397533752001826914304
c     v14 = 0ud229_60975816901989188439366609147650806646243779438079535488973244727296
c     v13 = 0ud229_849080353931662016050031143616919721474000852685471624888548589568
c     v12 = 0ud229_54762394931745710835541096562245347492855179753979234243047896121344
c     v11 = 0ud229_215679727678582780358379891266676588321818031268009366573281148141568
c     v10 = 0ud229_856022325694376019094197708530326099148137006302314664393521004544
c     v9 = 0ud229_26960075225529657105534406340400288508868874343003289720104742289408
c     v8 = 0ud229_80879865819174613582490466290457717206339424267818711313966107230208
c     v7 = 0ud229_107852976868021161942625673150975385418236390461081703958155666391040
c     v6 = 0ud229_4002075985399972630264855651428356906020196390170436861678514601984
c     v5 = 0ud229_432201645032867196960734757349862717547476741214836183449040253353984
c     v4 = 0ud229_70770091400374855460496398572570970764362894697602600209353046753280
c     v3 = 0ud229_205695133799314420120060905042671130622624406171847384478777344
c     v2 = 0ud229_108682387847556669155485422206686895094869300239461895189036334579712
c     v1 = 0ud229_808864221805515521577909029144306397301585189992366311431973061525504
c     v0 = 0ud229_0
c   -> State: 1.2 <-
c     state.tid = 4
c     state.vid = 238
c     state.target = 0ud229_444846119831675624208954182248068396567414532838844193487797234958336
c   -> State: 1.3 <-
c     state.token[4] = 0ud229_444846119831675624208954182248068396567414532838844193487797234958336
c     state.tid = 3
c     state.vid = 131
c     state.target = 0ud229_53946221432523033922598560180696032948636670616132382959682042462208
c   -> State: 1.4 <-
c     state.token[3] = 0ud229_53946221432523033922598560180696032948636670616132382959682042462208
c     state.tid = 2
c     state.vid = 39
c     state.target = 0ud229_3370829192260914438891163108377480054235670319001161575630717059072
c   -> State: 1.5 <-
c     state.token[2] = 0ud229_3370829192260914438891163108377480054235670319001161575630717059072
c     state.tid = 4
c     state.vid = 186
c     state.target = 0ud229_6740012478254517424234456671883939635397135642647917809141689614400
c   -> State: 1.6 <-
c     state.token[4] = 0ud229_6740012478254517424234456671883939635397135642647917809141689614400
c     state.tid = 2
c     state.vid = 32
c     state.target = 0ud229_1234542804788159516759914670012701119841628593228647515159527424
c   -> State: 1.7 <-
c     state.token[2] = 0ud229_1234542804788159516759914670012701119841628593228647515159527424
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud229_222472318997798894464827858921720962634085407701977077012341597405184
s 3 69 154 223
t 3 39 186 238
a YES
a 3 69 154 223
a 3 69 88 154
a 3 69 88 238
a 3 88 131 238
a 3 39 131 238
a 3 39 186 238