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/DSJC125.9_02.smv > DSJC125.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: 125
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 6961
c 0 cliques
c 2 cliques
c 4 cliques
c 8 cliques
c 16 cliques
c 32 cliques
c 64 cliques
c The solution is correct.
c Cliques: 91
c Sum: 1519
c MaxSize: 0
c Time: 114
c Aborted: false
c ML = 124
c SIZE = 125
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,10][3,5][4,2][5,2][6,3][7,1][8,1][9,1][10,2][12,3][13,1][14,1][16,2][17,1][18,3][19,6][21,4][22,9][23,6][24,13][25,6][26,4][27,3][28,1][29,1]}
c NODE covering index distribution:{[9,4][10,14][11,30][12,25][13,28][14,14][15,7][16,3]}
c EDGE covering index distrubution:{[1,2138][2,2382][3,1522][4,661][5,204][6,45][7,7][8,2]}
c Total edges:6961
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 -- no counterexample found with bound 6
c -- no counterexample found with bound 7
c -- no counterexample found with bound 8
c -- specification  G (((state.token[1] = v30 & state.token[2] = v90) & state.token[3] = v125) ->  G !((((state.token[1] = v20 | state.token[1] = v85) | state.token[1] = v109) & ((state.token[2] = v20 | state.token[2] = v85) | state.token[2] = v109)) & ((state.token[3] = v20 | state.token[3] = v85) | state.token[3] = v109)))    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] = 0ud91_193428223448693981889691664
c     state.token[2] = 0ud91_2469949858431438526874632
c     state.token[3] = 0ud91_98300780870107655439388672
c     state.tid = 1
c     state.vid = 51
c     state.target = 0ud91_0
c     v125 = 0ud91_98300780870107655439388672
c     v124 = 0ud91_1240377444545740678692340736
c     v123 = 0ud91_10333128543136210304892960
c     v122 = 0ud91_96725893125173753306677248
c     v121 = 0ud91_638957658008744808090173440
c     v120 = 0ud91_1859347427225225934940405760
c     v119 = 0ud91_315907466302472008616640512
c     v118 = 0ud91_3674093395963889816961028
c     v117 = 0ud91_628641795441296407235919872
c     v116 = 0ud91_7338596211700516234731520
c     v115 = 0ud91_14814069709602184916893696
c     v114 = 0ud91_78655810649606769390649856
c     v113 = 0ud91_41105880591975280124430336
c     v112 = 0ud91_619358438905394319243345920
c     v111 = 0ud91_331623501075882457684770816
c     v110 = 0ud91_19533045172509871676850176
c     v109 = 0ud91_313206456268048406031630336
c     v108 = 0ud91_625694780305253635337486336
c     v107 = 0ud91_158409450228483952449421312
c     v106 = 0ud91_334168893286376010896375808
c     v105 = 0ud91_116073408141134020288184320
c     v104 = 0ud91_91878510657333677646807040
c     v103 = 0ud91_77693870174530291275669504
c     v102 = 0ud91_20476328743882696683421696
c     v101 = 0ud91_1554283846331936050977439744
c     v100 = 0ud91_1393438528663977354384642048
c     v99 = 0ud91_44806477272536181840543745
c     v98 = 0ud91_4949189990364519921090560
c     v97 = 0ud91_174095943367978338331131904
c     v96 = 0ud91_154785597091986895817146368
c     v95 = 0ud91_453151245651621016084938752
c     v94 = 0ud91_1239224691601716921646448640
c     v93 = 0ud91_389425672437490000571924480
c     v92 = 0ud91_20872882939745487143567360
c     v91 = 0ud91_624145770489634898262884480
c     v90 = 0ud91_2469949858431438526874632
c     v89 = 0ud91_619505013305520437206188032
c     v88 = 0ud91_1320147624847582963723010048
c     v87 = 0ud91_1287505999151714005145354240
c     v86 = 0ud91_624259090874106171680096264
c     v85 = 0ud91_1237979008613554389726003200
c     v84 = 0ud91_1547425199563009526205513728
c     v83 = 0ud91_1587329050571104561399857152
c     v82 = 0ud91_1856958759810323114679599104
c     v81 = 0ud91_1244629566574461726579753088
c     v80 = 0ud91_619123535766295725182304256
c     v79 = 0ud91_319612717778421093964455936
c     v78 = 0ud91_1277261440115988856909594624
c     v77 = 0ud91_735031916706465057689567232
c     v76 = 0ud91_619131022830049620688633856
c     v75 = 0ud91_1890127475545420645564416
c     v74 = 0ud91_754747542409721595480244224
c     v73 = 0ud91_193451156432283752839774208
c     v72 = 0ud91_783912872290716072550656
c     v71 = 0ud91_309563529684672252326510592
c     v70 = 0ud91_1238549556747179798780968960
c     v69 = 0ud91_160976030118221268406829056
c     v68 = 0ud91_29070888798236427713249281
c     v67 = 0ud91_628645041761833814243409920
c     v66 = 0ud91_696367986488389481846013952
c     v65 = 0ud91_1238012065777595253939765248
c     v64 = 0ud91_24783018506220529513406464
c     v63 = 0ud91_1257438728107215327345508352
c     v62 = 0ud91_39365794585709817863602176
c     v61 = 0ud91_87042703400048025804013568
c     v60 = 0ud91_620330656101791773717692416
c     v59 = 0ud91_80091651571558704429957120
c     v58 = 0ud91_386859840945093211708194816
c     v57 = 0ud91_165783439273348002064891904
c     v56 = 0ud91_217609749105726028374867968
c     v55 = 0ud91_14546124703639163598077954
c     v54 = 0ud91_21765430534246673776902144
c     v53 = 0ud91_39478986151187681246183424
c     v52 = 0ud91_11032056956902648813977600
c     v51 = 0ud91_1238565753745104622518796288
c     v50 = 0ud91_793662901945808637946494976
c     v49 = 0ud91_1241283813858922844896888832
c     v48 = 0ud91_212789912130284290459303936
c     v47 = 0ud91_48432886534809210893369600
c     v46 = 0ud91_387012183416993799102070816
c     v45 = 0ud91_79264921451136606732812288
c     v44 = 0ud91_1605605784912049696355123200
c     v43 = 0ud91_658280207661887895914946560
c     v42 = 0ud91_164728539170548900740203008
c     v41 = 0ud91_319803975494193121396260864
c     v40 = 0ud91_87195307837216627336675328
c     v39 = 0ud91_1238095988131907963155644416
c     v38 = 0ud91_38860815245638733026821136
c     v37 = 0ud91_1247635132164856423657766912
c     v36 = 0ud91_157313919355569596048343040
c     v35 = 0ud91_1238016792009327894574661636
c     v34 = 0ud91_473998755790706953676668928
c     v33 = 0ud91_619092801243865726008430592
c     v32 = 0ud91_480264913430647594396155904
c     v31 = 0ud91_77976610626708577389117440
c     v30 = 0ud91_193428223448693981889691664
c     v29 = 0ud91_309494466263741307436666880
c     v28 = 0ud91_309509232774218850932621440
c     v27 = 0ud91_348624868675934423680549888
c     v26 = 0ud91_41141368641154601195667456
c     v25 = 0ud91_464255849006420519448223744
c     v24 = 0ud91_48357109310049239869423616
c     v23 = 0ud91_160789569557724898871214080
c     v22 = 0ud91_7433300138326855872675840
c     v21 = 0ud91_1240812441847228559309930496
c     v20 = 0ud91_638322595696973105198137344
c     v19 = 0ud91_38780377928884357332729856
c     v18 = 0ud91_619596480294825588563116032
c     v17 = 0ud91_154753576417042358463365120
c     v16 = 0ud91_631134873317470860545622080
c     v15 = 0ud91_82208139932825328533111808
c     v14 = 0ud91_77428217172712860592111616
c     v13 = 0ud91_87048589929288451982622720
c     v12 = 0ud91_310090727197569868005113856
c     v11 = 0ud91_466650237176384444346408960
c     v10 = 0ud91_952935796380053361211211776
c     v9 = 0ud91_1859332788885016751504359424
c     v8 = 0ud91_1238247025681305122811945024
c     v7 = 0ud91_81045253687237113642221568
c     v6 = 0ud91_314401584799028315271727104
c     v5 = 0ud91_12089273193150643362070544
c     v4 = 0ud91_193732880619977784634114050
c     v3 = 0ud91_1083198798120963514415710208
c     v2 = 0ud91_657660368248135358653399040
c     v1 = 0ud91_854108603828872079217262592
c     v0 = 0ud91_0
c   -> State: 1.2 <-
c     state.tid = 2
c     state.vid = 55
c     state.target = 0ud91_1238565753745104622518796288
c   -> State: 1.3 <-
c     state.token[2] = 0ud91_1238565753745104622518796288
c     state.tid = 1
c     state.vid = 124
c     state.target = 0ud91_14546124703639163598077954
c   -> State: 1.4 <-
c     state.token[1] = 0ud91_14546124703639163598077954
c     state.tid = 2
c     state.vid = 45
c     state.target = 0ud91_1240377444545740678692340736
c   -> State: 1.5 <-
c     state.token[2] = 0ud91_1240377444545740678692340736
c     state.tid = 3
c     state.vid = 20
c     state.target = 0ud91_79264921451136606732812288
c   -> State: 1.6 <-
c     state.token[3] = 0ud91_79264921451136606732812288
c     state.tid = 1
c     state.vid = 119
c     state.target = 0ud91_638322595696973105198137344
c   -> State: 1.7 <-
c     state.token[1] = 0ud91_638322595696973105198137344
c     state.tid = 3
c     state.vid = 85
c     state.target = 0ud91_315907466302472008616640512
c   -> State: 1.8 <-
c     state.token[3] = 0ud91_315907466302472008616640512
c     state.tid = 2
c     state.vid = 109
c     state.target = 0ud91_1237979008613554389726003200
c   -> State: 1.9 <-
c     state.token[2] = 0ud91_1237979008613554389726003200
c     state.tid = 3
c     state.vid = 1
c     state.target = 0ud91_313206456268048406031630336
c   -> State: 1.10 <-
c     state.token[3] = 0ud91_313206456268048406031630336
c     state.tid = 1
c     state.target = 0ud91_854108603828872079217262592
s 30 90 125
t 20 85 109
a YES
a 30 90 125
a 30 51 125
a 51 55 125
a 55 124 125
a 45 55 124
a 20 45 124
a 20 119 124
a 20 85 119
a 20 85 109