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/queen10_10_01.smv > queen10_10_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: 100
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 1470
c 0 cliques
c 2 cliques
c 4 cliques
c 8 cliques
c 16 cliques
c 32 cliques
c The solution is correct.
c Cliques: 61
c Sum: 430
c MaxSize: 0
c Time: 32
c Aborted: false
c ML = 99
c SIZE = 100
c Removed 7 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,4][3,4][4,4][5,4][6,4][7,4][8,4][9,4][10,22]}
c NODE covering index distribution:{[3,4][4,96]}
c EDGE covering index distrubution:{[1,1470]}
c Total edges:1470
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 -- specification  G (((((((((state.token[1] = v2 & state.token[2] = v15) & state.token[3] = v28) & state.token[4] = v49) & state.token[5] = v53) & state.token[6] = v66) & state.token[7] = v74) & state.token[8] = v81) & state.token[9] = v100) ->  G !((((((((((((((((state.token[1] = v2 | state.token[1] = v15) | state.token[1] = v29) | state.token[1] = v36) | state.token[1] = v53) | state.token[1] = v61) | state.token[1] = v77) | state.token[1] = v84) | state.token[1] = v100) & ((((((((state.token[2] = v2 | state.token[2] = v15) | state.token[2] = v29) | state.token[2] = v36) | state.token[2] = v53) | state.token[2] = v61) | state.token[2] = v77) | state.token[2] = v84) | state.token[2] = v100)) & ((((((((state.token[3] = v2 | state.token[3] = v15) | state.token[3] = v29) | state.token[3] = v36) | state.token[3] = v53) | state.token[3] = v61) | state.token[3] = v77) | state.token[3] = v84) | state.token[3] = v100)) & ((((((((state.token[4] = v2 | state.token[4] = v15) | state.token[4] = v29) | state.token[4] = v36) | state.token[4] = v53) | state.token[4] = v61) | state.token[4] = v77) | state.token[4] = v84) | state.token[4] = v100)) & ((((((((state.token[5] = v2 | state.token[5] = v15) | state.token[5] = v29) | state.token[5] = v36) | state.token[5] = v53) | state.token[5] = v61) | state.token[5] = v77) | state.token[5] = v84) | state.token[5] = v100)) & ((((((((state.token[6] = v2 | state.token[6] = v15) | state.token[6] = v29) | state.token[6] = v36) | state.token[6] = v53) | state.token[6] = v61) | state.token[6] = v77) | state.token[6] = v84) | state.token[6] = v100)) & ((((((((state.token[7] = v2 | state.token[7] = v15) | state.token[7] = v29) | state.token[7] = v36) | state.token[7] = v53) | state.token[7] = v61) | state.token[7] = v77) | state.token[7] = v84) | state.token[7] = v100)) & ((((((((state.token[8] = v2 | state.token[8] = v15) | state.token[8] = v29) | state.token[8] = v36) | state.token[8] = v53) | state.token[8] = v61) | state.token[8] = v77) | state.token[8] = v84) | state.token[8] = v100)) & ((((((((state.token[9] = v2 | state.token[9] = v15) | state.token[9] = v29) | state.token[9] = v36) | state.token[9] = v53) | state.token[9] = v61) | state.token[9] = v77) | state.token[9] = v84) | state.token[9] = v100)))    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] = 0ud54_70403238133762
c     state.token[2] = 0ud54_2269400590188544
c     state.token[3] = 0ud54_9051179719852160
c     state.token[4] = 0ud54_567485439016960
c     state.token[5] = 0ud54_1099513733632
c     state.token[6] = 0ud54_1266641723719680
c     state.token[7] = 0ud54_68790780928
c     state.token[8] = 0ud54_4504424261091329
c     state.token[9] = 0ud54_2200113774592
c     state.tid = 1
c     state.vid = 87
c     state.target = 0ud54_0
c     v100 = 0ud54_2200113774592
c     v99 = 0ud54_145136877043712
c     v98 = 0ud54_8797176201216
c     v97 = 0ud54_18255712256
c     v96 = 0ud54_281480345420800
c     v95 = 0ud54_2251800887691264
c     v94 = 0ud54_138579820544
c     v93 = 0ud54_1100618924036
c     v92 = 0ud54_1212153857
c     v91 = 0ud54_13510799955853312
c     v90 = 0ud54_2508529336320
c     v89 = 0ud54_4672942243840
c     v88 = 0ud54_149808459288576
c     v87 = 0ud54_281767042875392
c     v86 = 0ud54_279175233536
c     v85 = 0ud54_2252212130546688
c     v84 = 0ud54_274978572288
c     v83 = 0ud54_1374393745408
c     v82 = 0ud54_9007474266865668
c     v81 = 0ud54_4504424261091329
c     v80 = 0ud54_2267743781120
c     v79 = 0ud54_4501125730304
c     v78 = 0ud54_290339805986816
c     v77 = 0ud54_140823387963392
c     v76 = 0ud54_210461786112
c     v75 = 0ud54_2251868568813568
c     v74 = 0ud54_68790780928
c     v73 = 0ud54_9008367485847552
c     v72 = 0ud54_618609524736
c     v71 = 0ud54_4503668346847748
c     v70 = 0ud54_1145691116146688
c     v69 = 0ud54_1411772930064640
c     v68 = 0ud54_1134730359865344
c     v67 = 0ud54_1126054542442496
c     v66 = 0ud54_1266641723719680
c     v65 = 0ud54_3377699733110784
c     v64 = 0ud54_10133099230789632
c     v63 = 0ud54_1127549174285312
c     v62 = 0ud54_1125900041062912
c     v61 = 0ud54_5629499534262272
c     v60 = 0ud54_283674000105472
c     v59 = 0ud54_21990232825856
c     v58 = 0ud54_8933531984128
c     v57 = 0ud54_51573170176
c     v56 = 0ud54_4315947008
c     v55 = 0ud54_11399736556789760
c     v54 = 0ud54_549831319552
c     v53 = 0ud54_1099513733632
c     v52 = 0ud54_134259712
c     v51 = 0ud54_4503599627905024
c     v50 = 0ud54_565148976939136
c     v49 = 0ud54_567485439016960
c     v48 = 0ud54_589338266042368
c     v47 = 0ud54_562967137485056
c     v46 = 0ud54_9570187862867968
c     v45 = 0ud54_2815299539697664
c     v44 = 0ud54_703687508886016
c     v43 = 0ud54_564049473470464
c     v42 = 0ud54_562950090260480
c     v41 = 0ud54_5066551728276480
c     v40 = 0ud54_2336999145472
c     v39 = 0ud54_4398080131200
c     v38 = 0ud54_8796097413120
c     v37 = 0ud54_9024808620720128
c     v36 = 0ud54_554050846976
c     v35 = 0ud54_2251834173489664
c     v34 = 0ud54_83984384
c     v33 = 0ud54_141837000572928
c     v32 = 0ud54_2290155520
c     v31 = 0ud54_4503599629533216
c     v30 = 0ud54_37383428898832
c     v29 = 0ud54_39582959665152
c     v28 = 0ud54_9051179719852160
c     v27 = 0ud54_35751307902976
c     v26 = 0ud54_52780853101056
c     v25 = 0ud54_2286984185807104
c     v24 = 0ud54_35218799460352
c     v23 = 0ud54_36286047977472
c     v22 = 0ud54_175921994661920
c     v21 = 0ud54_4538784007848000
c     v20 = 0ud54_2207617384456
c     v19 = 0ud54_9011605891186704
c     v18 = 0ud54_9354975641600
c     v17 = 0ud54_25769804416
c     v16 = 0ud54_12885065728
c     v15 = 0ud54_2269400590188544
c     v14 = 0ud54_10804527360
c     v13 = 0ud54_1142461300768
c     v12 = 0ud54_8740929600
c     v11 = 0ud54_4644345705660418
c     v10 = 0ud54_9079767022174208
c     v9 = 0ud54_75316546502664
c     v8 = 0ud54_79164837200400
c     v7 = 0ud54_70386460950528
c     v6 = 0ud54_70373039669376
c     v5 = 0ud54_2322170705477632
c     v4 = 0ud54_87960997330976
c     v3 = 0ud54_71468255805760
c     v2 = 0ud54_70403238133762
c     v1 = 0ud54_4573968388325376
c     v0 = 0ud54_0
c   -> State: 1.2 <-
c     state.tid = 8
c     state.vid = 36
c     state.target = 0ud54_281767042875392
c   -> State: 1.3 <-
c     state.token[8] = 0ud54_281767042875392
c     state.tid = 6
c     state.vid = 61
c     state.target = 0ud54_554050846976
c   -> State: 1.4 <-
c     state.token[6] = 0ud54_554050846976
c     state.tid = 7
c     state.vid = 84
c     state.target = 0ud54_5629499534262272
c   -> State: 1.5 <-
c     state.token[7] = 0ud54_5629499534262272
c     state.tid = 8
c     state.vid = 77
c     state.target = 0ud54_274978572288
c   -> State: 1.6 <-
c     state.token[8] = 0ud54_274978572288
c     state.tid = 3
c     state.vid = 29
c     state.target = 0ud54_140823387963392
c   -> State: 1.7 <-
c     state.token[3] = 0ud54_140823387963392
c     state.tid = 4
c     state.vid = 72
c     state.target = 0ud54_39582959665152
c   -> State: 1.8 <-
c     state.token[4] = 0ud54_39582959665152
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud54_618609524736
s 7 28 32 49 53 66 74 81 100
t 2 15 29 36 53 61 77 84 100
a YES
a 7 28 32 49 53 66 74 81 100
a 15 28 32 49 53 66 74 81 100
a 2 15 28 49 53 66 74 81 100
a 2 15 28 49 53 66 74 87 100
a 2 15 28 36 49 53 74 87 100
a 2 15 28 36 49 53 61 87 100
a 2 15 28 36 49 53 61 84 100
a 2 15 36 49 53 61 77 84 100
a 2 15 29 36 53 61 77 84 100