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_01.smv > DSJC250.9_01.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: 236
c Sum: 5124
c MaxSize: 0
c Time: 445
c Aborted: false
c ML = 249
c SIZE = 250
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,22][3,14][4,3][5,2][6,1][7,2][8,2][9,4][11,5][12,1][13,3][14,1][16,1][17,2][18,6][19,5][20,1][21,6][22,2][23,3][24,4][25,9][26,18][27,16][28,20][29,26][30,24][31,14][32,12][33,3][34,1][35,2][36,1]}
c NODE covering index distribution:{[15,1][16,3][17,11][18,24][19,44][20,50][21,46][22,33][23,17][24,8][25,7][26,6]}
c EDGE covering index distrubution:{[1,7581][2,9051][3,6624][4,3135][5,1118][6,305][7,65][8,18]}
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] = v69 & state.token[2] = v88) & state.token[3] = v154) & state.token[4] = v223) ->  G !((((((state.token[1] = v39 | state.token[1] = v131) | state.token[1] = v136) | state.token[1] = v238) & (((state.token[2] = v39 | state.token[2] = v131) | state.token[2] = v136) | state.token[2] = v238)) & (((state.token[3] = v39 | state.token[3] = v131) | state.token[3] = v136) | state.token[3] = v238)) & (((state.token[4] = v39 | state.token[4] = v131) | state.token[4] = v136) | 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] = 0ud236_485489667807509321081239214004406911287964788757025945639340835078144
c     state.token[2] = 0ud236_62115770034371191606379685519650130659467454704288774571680705019904000
c     state.token[3] = 0ud236_863587224206058947475978903736785053596153902399166147585180398780416
c     state.token[4] = 0ud236_13911335772266319604990011911506600607309116391006022450382421635366912
c     state.tid = 1
c     state.vid = 3
c     state.target = 0ud236_0
c     v250 = 0ud236_34724417889610345182917797852454705658365348843591421704990032245293056
c     v249 = 0ud236_55234192791205570026612668232507576982260678089268790198238390136111104
c     v248 = 0ud236_1725699894746334641315747672666378020441978864845838937473490851201024
c     v247 = 0ud236_7764465887123307396039413478536678757095030870707453907648012164792320
c     v246 = 0ud236_55216078691383258509021092011400728025388208700397869155238443887886400
c     v245 = 0ud236_1732229235952194477522070033968726951139094616763980411175177952428032
c     v244 = 0ud236_10162639359891857797964292431041099112162903497833758343200170311680
c     v243 = 0ud236_13803650688133139073759885048395110759953262274867556692094145957724160
c     v242 = 0ud236_55217340819086984051650697611514768443762429459316084708430860880183808
c     v241 = 0ud236_862728166407574626936369534441970664356725955090742556700273174118400
c     v240 = 0ud236_56946149006049016098455444980204842834709645250337891387934929491853312
c     v239 = 0ud236_863251436825490685275918046172055615105240487056348022943297518436352
c     v238 = 0ud236_15164976534759661541414691864241373075671379772072899978929234771968
c     v237 = 0ud236_57408362996631395821471456954155268578732174723376344043334852935680
c     v236 = 0ud236_6901799832118783589193351999096771062814737891579811596897905077649408
c     v235 = 0ud236_27433852180538686588466122059433084019744097523378873585584893329408
c     v234 = 0ud236_13911332583497117793318527758129651719354893186891211222160655593250816
c     v233 = 0ud236_13803946853090035365230434015599034003043704971197742595073414391136256
c     v232 = 0ud236_108683532864716644460354143467295002608128753197392214247386069860352
c     v231 = 0ud236_121537005170652841078169031668748381001361072401583889496829692215296
c     v230 = 0ud236_215893540351674295177979397112361013481229884183877418070440180449282
c     v229 = 0ud236_54026852737857521896045865854664291344378008751379360894417417273344
c     v228 = 0ud236_997518027488631556703824787641370606656972139091383172031836145582080
c     v227 = 0ud236_28644948155066651399584474417891766155357249191063900477100170149888
c     v226 = 0ud236_3457613166991991019666220950899862538674878087376318811408181594423296
c     v225 = 0ud236_3452564959379923629241494728935148412124724203842279813292157673930752
c     v224 = 0ud236_864618028372802010027820004703077910397362360824994523752504596889600
c     v223 = 0ud236_13911335772266319604990011911506600607309116391006022450382421635366912
c     v222 = 0ud236_6905117267327210687717676395896578373166463859301244031773701507645440
c     v221 = 0ud236_3466044725517356382628546248924484337915340390268604284357242735558656
c     v220 = 0ud236_28031439995949409029942736037494357310625331723971796313407750144
c     v219 = 0ud236_26960255300081299652702421503498551257232797229346020133015157473280
c     v218 = 0ud236_107945924929662520025976580166241277247362627528615083875448106516484
c     v217 = 0ud236_7766202293203001248104825876266487624099512933076622301730724011573248
c     v216 = 0ud236_6929364497691150474218924026244246159350123048600477499192384549814272
c     v215 = 0ud236_862734954886030455666320968385754831755102418511860506874088261681152
c     v214 = 0ud236_1078819141676769919712113201741904986411419846129079022975702660022272
c     v213 = 0ud236_27633946387981164346266236398488682694742766340672568503164501275705344
c     v212 = 0ud236_7226114839373436088716095117738439511039856914424515708335864326127616
c     v211 = 0ud236_14019172887221526950783939806498307645469065095385101424478954740252672
c     v210 = 0ud236_55219868674084308723316008453012926428524902706653817105164900509941760
c     v209 = 0ud236_4320331608078678331585632323904221396506759974612098872352769472217088
c     v208 = 0ud236_27607406646379353906529436130610456247815242241767970236743829107507200
c     v207 = 0ud236_431520406523203597034093363959749194405980455016002113533640100020224
c     v206 = 0ud236_1833276376584092014563680440234385724832146250130243007099037707927552
c     v205 = 0ud236_458371800912551182128496364548514309386136247962047011614612032323584
c     v204 = 0ud236_168499718192338709682665376421140526311114941343485111135949809516560
c     v203 = 0ud236_6950612463178132800505597648348290103723160123272660558207355191296
c     v202 = 0ud236_6902170912677361465628717147390396929855884802038072378912531585957888
c     v201 = 0ud236_27608723142969876197115280236745691272352034959451330427141876713783296
c     v200 = 0ud236_13611613698995124969330742489957865168865269553249816444567675731968
c     v199 = 0ud236_10381264474768262610737992937886279608978842583909218764076841248497664
c     v198 = 0ud236_7118268424951653607926403793182441315749314481194692337026708625424384
c     v197 = 0ud236_1725489249472096190618310497935666473287460971610891940201470906859520
c     v196 = 0ud236_27608671233095765157937568686762678870630827339725497306791323757445121
c     v195 = 0ud236_3369998157356525793806256250095500766996120342595941612261602230272
c     v194 = 0ud236_229580797846520307431445885709927809051372661327436923357229318406144
c     v193 = 0ud236_3450886344863829112619191237387040541850897071844664791754411757010944
c     v192 = 0ud236_108892917645092895256468467319344960868699434018309891617428999307264
c     v191 = 0ud236_3505217607307217662953723035401559976689038884969624330999727805956096
c     v190 = 0ud236_10356094852326961205499092534351120999206546072163612348599360525697024
c     v189 = 0ud236_242797597726199808534127471526382840698848287510949484600182777577472
c     v188 = 0ud236_27617123340739914356725074950388820047160875108600387615699836738732032
c     v187 = 0ud236_957078106688849781336292860700270740848240625005467134490530338045952
c     v186 = 0ud236_161789299285802882007502759776678785210505133812950135365162376364032
c     v185 = 0ud236_2588207536998609045081490472606496935325900971298206530146846967332864
c     v184 = 0ud236_14238225124610992830245079513799167776700215551578580226989591703453696
c     v183 = 0ud236_431819901006850365940165618504669553978737050831228559548740492328976
c     v182 = 0ud236_2158480733353205030244357822643609609180929593431460870419612220522496
c     v181 = 0ud236_1725437437571335430027753391179533772709614425324437042907983973974016
c     v180 = 0ud236_13804124773422610464319537977950928836069210379725173033926159193079808
c     v179 = 0ud236_296572580993867822831366128601013590253009139672972771390352254828544
c     v178 = 0ud236_13803545402881462419697589192910454044172827897074710569579655500660736
c     v177 = 0ud236_27729157518525126422238238229244453789978388050226841708442679196516352
c     v176 = 0ud236_1725858298670324813218250866025478673586893704011404547621845383249920
c     v175 = 0ud236_55213974888087865292567162679099970808100864159255067283894501178867712
c     v174 = 0ud236_6901858241919623406664847488152269559247680414181386033185987527442432
c     v173 = 0ud236_57075681887509358995528679407542907916464254956936363579428249364594688
c     v172 = 0ud236_431392201390029779783198892792514789338266233996521538307420049113088
c     v171 = 0ud236_31273538133896508075593409210610475350853558373854912111523509452144640
c     v170 = 0ud236_8532146817782225695819275648534462877538696447478747288692177502208
c     v169 = 0ud236_4313591674258811702286084946000598488100370303523936955049734010044672
c     v168 = 0ud236_27660905614821271963744672359598648761997444823798146835777985674477568
c     v167 = 0ud236_55217557974309736783473255992693596997820336084942507567510907911144448
c     v166 = 0ud236_55214010270501472452883744892382637884580323698415609138110790304268288
c     v165 = 0ud236_55429650424819868734252282441013235365242427918169581653796329988554752
c     v164 = 0ud236_864614737351161137422952380183971793841335904893348634956989250666496
c     v163 = 0ud236_3465195670773220516065362200047489256208909187425843077308504269127680
c     v162 = 0ud236_108688893145479376397540537975996211915255322244534603007190519250944
c     v161 = 0ud236_27660905300183142800120472098022299050844564471356817795465514995154944
c     v160 = 0ud236_27607828711464909168711533630013400967945020530258446877642148420780032
c     v159 = 0ud236_3562091283764197803061762405761536627306359358092636398781155623567360
c     v158 = 0ud236_55227451004770134295860450362786665831050454222755208597996598238117888
c     v157 = 0ud236_5265845982579984725700006667914529411270805463236304956891529740288
c     v156 = 0ud236_6901774371790063329702415067897347696739732941280007860734484327432192
c     v155 = 0ud236_1725469509644330097309021045611053953592445863590776917404698697269248
c     v154 = 0ud236_863587224206058947475978903736785053596153902399166147585180398780416
c     v153 = 0ud236_539410586467134928976545732741021397607633753404060795107785469591552
c     v152 = 0ud236_229173534262986690729436037180646951578170733440948280578251723636736
c     v151 = 0ud236_3454246046415043575545619295585797339507652039357714140753098530881536
c     v150 = 0ud236_111262848352547428618774916940924881587622444575675057653394410831872
c     v149 = 0ud236_58664844154252145067967900915043895625914604864825466085140036946231328
c     v148 = 0ud236_13803501027161825104284715676219159622110518796782347436201055482806272
c     v147 = 0ud236_891363545214773391008899261445239463047187299550383892493980814802944
c     v146 = 0ud236_3451771824584987778975759071409899120408014923756200789811644776579072
c     v145 = 0ud236_3451087191831793578464390305827275427760800118578585561023663294119936
c     v144 = 0ud236_27714930538354682892861415100258422221899385153813611501544104186085376
c     v143 = 0ud236_55828678620795460504268400750567867296499445361556932901361625858048
c     v142 = 0ud236_55214813274265213640020898820636145287855319665737143164190284572524544
c     v141 = 0ud236_13816972673342504137119883969163361275972295642498740348955780410507264
c     v140 = 0ud236_14019626464745170506024024116543131471501618376343128432055831062642688
c     v139 = 0ud236_107859539152661097540255746766161085760493067193556175475835358150658
c     v138 = 0ud236_54130582195175492645232010401860667847809358580491958403627669782528
c     v137 = 0ud236_4532706866703595632150284616217438276832319689997798405193076398096384
c     v136 = 0ud236_57290095619863807471930510946701249282386869609605275997935513894912
c     v135 = 0ud236_109525095133066923457548563733877871489399604546786020080670931419144
c     v134 = 0ud236_141559466107837846886007248829329961130416612160967752698289308303360
c     v133 = 0ud236_55227450799142974443449037094876269673808137570550489566265618047434752
c     v132 = 0ud236_3450890046345572583711469693116286384548171449573520238347085554909184
c     v131 = 0ud236_27607406637132414511274364523090631491311987710283504505816600767627264
c     v130 = 0ud236_1752401495991206769481581598099782467459482992302626145237963875811328
c     v129 = 0ud236_857308075428147930043096229646944469202008829195229629714500943872
c     v128 = 0ud236_6928917331024968726806408414238581369985254580342745909969280357629952
c     v127 = 0ud236_34512312352172420064199890875299107177357225072035753120671821031538688
c     v126 = 0ud236_13805190868960245047484282898411157671516538393134535966480100709367808
c     v125 = 0ud236_55241013009109579933147108095143628397982558103803711885545770892394496
c     v124 = 0ud236_15636769068756757918481668825150467559773561959446069432630175609126912
c     v123 = 0ud236_108366348534969266141705626087553946893470014871829473158407219314688
c     v122 = 0ud236_1321037425257139995313574710233374666644609223833166441341321278914560
c     v121 = 0ud236_3386449182840739609835095871390882094258838136194990804178193940480
c     v120 = 0ud236_6846121811175031705680273762571490669789128130068845589625206734848
c     v119 = 0ud236_1732183361077396980836986848817579519046650350584340243059608706351104
c     v118 = 0ud236_432201658666928254532809364912424948028228688428293764723028328972288
c     v117 = 0ud236_431781218920557245583642451778831518237025025141450822486406887178240
c     v116 = 0ud236_7548785169649377105741688906566345924771451274098762542333795762176000
c     v115 = 0ud236_33703240487764735750888711959640273366130193199757585507311811559552
c     v114 = 0ud236_6766726116040324917342381008691631598657869730011442929534249205824
c     v113 = 0ud236_1752923120735408785127347666739276312880889128748861316372519628832768
c     v112 = 0ud236_3019514026724010308328175986279734807443697900681856755386936566218752
c     v111 = 0ud236_6901851874411931808009517543632256339838789081825779665761801309519872
c     v110 = 0ud236_431360856506755996158983371222462644211421449250731679847529817573380
c     v109 = 0ud236_1078411037477430266854813852544740498895507398360181625007489461256192
c     v108 = 0ud236_8681109409267579110193498742278413084827198835026446553199370230038528
c     v107 = 0ud236_55268102116263186739857472217632755198412653506139247345926435386687488
c     v106 = 0ud236_7764517296360764732969198781078681139240542463487789701408773577375744
c     v105 = 0ud236_6905129658853312886480788198880074353874247547368085828374525858807808
c     v104 = 0ud236_16856574421327811242134456653145716125032226965203888823053710262272
c     v103 = 0ud236_55429914039873738404598084066156920790319223609315145942787418199425024
c     v102 = 0ud236_3882232371494964579224088264488197371573527290891112992145449909485568
c     v101 = 0ud236_1738929930157528160230765923228998594606010785649055590281211430305792
c     v100 = 0ud236_59231030852729864727777847896582060617431698268819727169660998790414336
c     v99 = 0ud236_168552322828080364091760368488877387870330423702942266714213442387968
c     v98 = 0ud236_6957456555514170306959653377333302161239854195169620379002462581817344
c     v97 = 0ud236_55267897250882250551013199971886839725440658250109156419215517064101888
c     v96 = 0ud236_33706515352964865432197281594342350382844041405841489561206149611520
c     v95 = 0ud236_13805204069743182026276512466963741254469747420270075349526183596261376
c     v94 = 0ud236_6756853289379717807893311274964313370792477676322278707825393795072
c     v93 = 0ud236_13912596227749801958924373853176880004341719062645433095193294920482816
c     v92 = 0ud236_1756609025037811742117584760244556921901542502977245040516797437083648
c     v91 = 0ud236_27829457629029466096606389088742875571182469374297241137075059771441152
c     v90 = 0ud236_6916187294818079294763436636776815319388691476813787582575840061292544
c     v89 = 0ud236_27662594005391923640090848478018553416143783609160818297978683379417088
c     v88 = 0ud236_62115770034371191606379685519650130659467454704288774571680705019904000
c     v87 = 0ud236_56186214699572351243609662534382834438021997050808046651714768528736256
c     v86 = 0ud236_13831190700464257831965442808872743405904009732836674417059903500713984
c     v85 = 0ud236_41413953386475355068696311394323942193668864080709516373087276488458240
c     v84 = 0ud236_55483622897145038567514739925791958171168365207523904134016273079074816
c     v83 = 0ud236_1941221986559242994830962101407458642574599303698824905934944807682048
c     v82 = 0ud236_20713351378668647070661073979874900279988597388856301199844749839695872
c     v81 = 0ud236_55215023897643028463621701107567740276512531022843242049730698803150848
c     v80 = 0ud236_55215032124766336588174510095908075892946109757106009793166782830215168
c     v79 = 0ud236_3451110130082612419577662830852240462569243783823490009585744221306880
c     v78 = 0ud236_55227872000038642264172030914683631918335095591136380140844892528050176
c     v77 = 0ud236_17254373278175491020632749592296762200039056161314972151998998353281024
c     v76 = 0ud236_27876612007873618841377569038617879606433681555927363596235731137200384
c     v75 = 0ud236_215745419233649164603004951417505063118177266763359004795848695480320
c     v74 = 0ud236_15528929293988449113379683943968592317731775163516516750424499667599360
c     v73 = 0ud236_55213971828576304074035233842908382596510880092821563466919419800715264
c     v72 = 0ud236_229186700811859827359367271890539977779605028273833968263840787333120
c     v71 = 0ud236_432208227038566702619654405375388856908093426037549484725919000035328
c     v70 = 0ud236_947823682982431619699188484308705849072399521550010807292467871744
c     v69 = 0ud236_485489667807509321081239214004406911287964788757025945639340835078144
c     v68 = 0ud236_54341631010141370535831848565816643042398218750004596424202134749184
c     v67 = 0ud236_31169068393588488893389939299397689116568794451520889555423604359823360
c     v66 = 0ud236_55220763829317549754271497030810153185744346604684060305041533215705088
c     v65 = 0ud236_432218106581529983382012095690427750824583460367306588888446854496257
c     v64 = 0ud236_217418871662143075304757069146962759504819319406488907633448441610240
c     v63 = 0ud236_13803756385692721625648026236431905081398143566993367099711539552190464
c     v62 = 0ud236_55214132290881215003587227661247725731408199915539155352468497446731776
c     v61 = 0ud236_30383009129480648849507008101497649689471655556729467809464762501120
c     v60 = 0ud236_57291532473651393882279185082586493842211728466063024126914346352640
c     v59 = 0ud236_1078820761358533722497791311004029528720063485364936668356114460442624
c     v58 = 0ud236_648723716678557472386002463012742945115873899776551089907974587547648
c     v57 = 0ud236_27607039701768977291186914273664663234618486842713779910664957095575552
c     v56 = 0ud236_111639256716602555371349975254480191629620442059105843743125265203200
c     v55 = 0ud236_2106258715258941049490849793314939385657246073875243694408620572672
c     v54 = 0ud236_54867922504493017107039834481734049233136355545980091376719852732416
c     v53 = 0ud236_3451017977847523871360957612022110229318388679699638849027051190484992
c     v52 = 0ud236_447996663220323944245972681653892154765164635409419563584492404864
c     v51 = 0ud236_26355391158325588450015971630714245886418039089451155626129358848
c     v50 = 0ud236_862731509210011767605508732997271039595891838696620355895078055576576
c     v49 = 0ud236_30382609001907766127947017032302939210628991402594080431939050799104
c     v48 = 0ud236_27606995260195903859418312088157130239174648710219995775569189878628352
c     v47 = 0ud236_863587119806092143251508240137729372434518444391768013356565023162368
c     v46 = 0ud236_3669922743380485677464735157688457697660515227515232860267990585704448
c     v45 = 0ud236_7339847228483516933743549722298809942241968413249930072696788789231618
c     v44 = 0ud236_444844063006013964536548604089279237999110393149568637602332321775616
c     v43 = 0ud236_1779415719812753362027586982499264013306585348360584137285234694553600
c     v42 = 0ud236_7009586352407662467766245516478338172444156553749654920704171465277440
c     v41 = 0ud236_539199347933029747582520964289808497158663097426950050731775804571648
c     v40 = 0ud236_1685832280806071255580799038922429749727730818802082995093521825792
c     v39 = 0ud236_3450925880966272402865244668740470579700174782722555597488541692592128
c     v38 = 0ud236_431991535060502772544269506366540208332252132894448729945382448005120
c     v37 = 0ud236_17321767379149640288112524675597230191447243877368144561829848713003008
c     v36 = 0ud236_27606994055438017267546440828096997930438424606164758898771019125751840
c     v35 = 0ud236_55269575667542524309750286754982283245054929770936127796297082773438464
c     v34 = 0ud236_33646026606649129600689222691951289101253440732211142553080841416736768
c     v33 = 0ud236_27633974953740064040173858886576761001644625924877429001720522279485440
c     v32 = 0ud236_1728071039520714395373936569291068962495737319843872537734580321517568
c     v31 = 0ud236_216100941819030091565512060036768134747514481711864802362647598071808
c     v30 = 0ud236_485437011773090651623071204691441088234430732531223461268972940296192
c     v29 = 0ud236_970558903177719442026421867692395019011372261630165306469204856143872
c     v28 = 0ud236_14666213044024852332062012340645302445658892793155445613308400461938688
c     v27 = 0ud236_13803716585070078782382958421810073243965418104917855362176553307865088
c     v26 = 0ud236_15542514591866105176839253024656614218053721360349522682793238133211648
c     v25 = 0ud236_329101115470079411504497800377968027659116918079063325788562522112
c     v24 = 0ud236_55645331876039943539206627704936102301927197124305714607530720247152640
c     v23 = 0ud236_6915239551664555869315936103260854309619702870516764539034010556301312
c     v22 = 0ud236_1732598651915163999711852902075935705462191940462751644031971292610560
c     v21 = 0ud236_439994757805304251793339147810541926630554193698164694880894043815936
c     v20 = 0ud236_3465195902172341792410532710792086542136631814468882204951830130065408
c     v19 = 0ud236_6903643716414298763659440268703652293752262306589040709326281795174400
c     v18 = 0ud236_242851791699194439995418593029454311463455534638258847592840236630016
c     v17 = 0ud236_55214076099609779849998359563631498960001024885199334709971760483139584
c     v16 = 0ud236_13804335423370054475203857335793181457924438504120197974875168403619840
c     v15 = 0ud236_7333131924589867251718871128142886638157229652010184584229343838863360
c     v14 = 0ud236_3491313967601689487361495002494142535718633653978524797843939818209280
c     v13 = 0ud236_1732179866037269508103863747446782513280176767509127822447339582259200
c     v12 = 0ud236_2163535726643919144607534014166428073030241370428726441592304493920256
c     v11 = 0ud236_15528929434971672883617621178901202715020678166358236766058263313645568
c     v10 = 0ud236_14667053896727367365237758865465386144753018187079278561585138895945728
c     v9 = 0ud236_13483266351364145912226173405436272711955051644089610109392141680648
c     v8 = 0ud236_6915661144904670834622031386617263372792374645799562284991391461539840
c     v7 = 0ud236_67399983170884808265108309505792634704594727620411598456897150128128
c     v6 = 0ud236_1725884167253895944337093325400516242553902071799032959209270730031104
c     v5 = 0ud236_866088293113117345148501282168014533673804369397602471189506951221248
c     v4 = 0ud236_27620886815352145219727921506826100011119572372818187527838756480483328
c     v3 = 0ud236_26960358094391036899505971152081136473295863111991540637899595710464
c     v2 = 0ud236_7013798625151515102073668869869762474727483921211059485462903271194624
c     v1 = 0ud236_97921896294852319930493240759873698466192655579378953349132043516116992
c     v0 = 0ud236_0
c   -> State: 1.2 <-
c     state.tid = 3
c     state.vid = 238
c     state.target = 0ud236_26960358094391036899505971152081136473295863111991540637899595710464
c   -> State: 1.3 <-
c     state.token[3] = 0ud236_26960358094391036899505971152081136473295863111991540637899595710464
c     state.tid = 4
c     state.vid = 131
c     state.target = 0ud236_15164976534759661541414691864241373075671379772072899978929234771968
c   -> State: 1.4 <-
c     state.token[4] = 0ud236_15164976534759661541414691864241373075671379772072899978929234771968
c     state.tid = 1
c     state.vid = 39
c     state.target = 0ud236_27607406637132414511274364523090631491311987710283504505816600767627264
c   -> State: 1.5 <-
c     state.token[1] = 0ud236_27607406637132414511274364523090631491311987710283504505816600767627264
c     state.tid = 2
c     state.vid = 136
c     state.target = 0ud236_3450925880966272402865244668740470579700174782722555597488541692592128
c   -> State: 1.6 <-
c     state.token[2] = 0ud236_3450925880966272402865244668740470579700174782722555597488541692592128
c     state.tid = 3
c     state.vid = 243
c     state.target = 0ud236_57290095619863807471930510946701249282386869609605275997935513894912
c   -> State: 1.7 <-
c     state.token[3] = 0ud236_57290095619863807471930510946701249282386869609605275997935513894912
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud236_13803650688133139073759885048395110759953262274867556692094145957724160
s 69 88 154 223
t 39 131 136 238
a YES
a 69 88 154 223
a 3 69 88 223
a 3 69 88 238
a 3 88 131 238
a 3 39 131 238
a 39 131 136 238