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/queen9_9_02.smv > queen9_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: 81
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 1056
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: 54
c Sum: 349
c MaxSize: 0
c Time: 28
c Aborted: false
c ML = 80
c SIZE = 81
c Removed 6 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,4][3,2][4,5][5,5][6,4][7,4][8,4][9,20]}
c NODE covering index distribution:{[3,2][4,78][5,1]}
c EDGE covering index distrubution:{[1,1046][2,10]}
c Total edges:1056
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 -- specification  G ((((((((state.token[1] = v8 & state.token[2] = v15) & state.token[3] = v21) & state.token[4] = v36) & state.token[5] = v43) & state.token[6] = v46) & state.token[7] = v65) & state.token[8] = v77) ->  G !((((((((((((((state.token[1] = v8 | state.token[1] = v15) | state.token[1] = v21) | state.token[1] = v36) | state.token[1] = v43) | state.token[1] = v46) | state.token[1] = v65) | state.token[1] = v77) & (((((((state.token[2] = v8 | state.token[2] = v15) | state.token[2] = v21) | state.token[2] = v36) | state.token[2] = v43) | state.token[2] = v46) | state.token[2] = v65) | state.token[2] = v77)) & (((((((state.token[3] = v8 | state.token[3] = v15) | state.token[3] = v21) | state.token[3] = v36) | state.token[3] = v43) | state.token[3] = v46) | state.token[3] = v65) | state.token[3] = v77)) & (((((((state.token[4] = v8 | state.token[4] = v15) | state.token[4] = v21) | state.token[4] = v36) | state.token[4] = v43) | state.token[4] = v46) | state.token[4] = v65) | state.token[4] = v77)) & (((((((state.token[5] = v8 | state.token[5] = v15) | state.token[5] = v21) | state.token[5] = v36) | state.token[5] = v43) | state.token[5] = v46) | state.token[5] = v65) | state.token[5] = v77)) & (((((((state.token[6] = v8 | state.token[6] = v15) | state.token[6] = v21) | state.token[6] = v36) | state.token[6] = v43) | state.token[6] = v46) | state.token[6] = v65) | state.token[6] = v77)) & (((((((state.token[7] = v8 | state.token[7] = v15) | state.token[7] = v21) | state.token[7] = v36) | state.token[7] = v43) | state.token[7] = v46) | state.token[7] = v65) | state.token[7] = v77)) & (((((((state.token[8] = v8 | state.token[8] = v15) | state.token[8] = v21) | state.token[8] = v36) | state.token[8] = v43) | state.token[8] = v46) | state.token[8] = v65) | state.token[8] = v77)))    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] = 0ud48_9895738867728
c     state.token[2] = 0ud48_137506209792
c     state.token[3] = 0ud48_22024592293952
c     state.token[4] = 0ud48_8589948928
c     state.token[5] = 0ud48_211106773598208
c     state.token[6] = 0ud48_549756403968
c     state.token[7] = 0ud48_1075053568
c     state.token[8] = 0ud48_17450402304
c     state.tid = 8
c     state.vid = 1
c     state.target = 0ud48_0
c     v81 = 0ud48_39599598477312
c     v80 = 0ud48_86033563656
c     v79 = 0ud48_105570296135808
c     v78 = 0ud48_154627244032
c     v77 = 0ud48_17450402304
c     v76 = 0ud48_30064771328
c     v75 = 0ud48_51544850432
c     v74 = 0ud48_292057777153
c     v73 = 0ud48_18254725120
c     v72 = 0ud48_2199023525896
c     v71 = 0ud48_39582553079808
c     v70 = 0ud48_70437472305152
c     v69 = 0ud48_137707651200
c     v68 = 0ud48_8590230016
c     v67 = 0ud48_4301520896
c     v66 = 0ud48_309237907712
c     v65 = 0ud48_1075053568
c     v64 = 0ud48_1099511955457
c     v63 = 0ud48_35187056451584
c     v62 = 0ud48_2201313345536
c     v61 = 0ud48_109953578696704
c     v60 = 0ud48_216895848448
c     v59 = 0ud48_2151678592
c     v58 = 0ud48_281320390656
c     v57 = 0ud48_37583060992
c     v56 = 0ud48_1101659112704
c     v55 = 0ud48_2148728832
c     v54 = 0ud48_25698304
c     v53 = 0ud48_940048384
c     v52 = 0ud48_72576357892096
c     v51 = 0ud48_4535490183168
c     v50 = 0ud48_343597908480
c     v49 = 0ud48_5369233536
c     v48 = 0ud48_1133871923200
c     v47 = 0ud48_2753536
c     v46 = 0ud48_549756403968
c     v45 = 0ud48_140737756815360
c     v44 = 0ud48_140746229284864
c     v43 = 0ud48_211106773598208
c     v42 = 0ud48_143348828471296
c     v41 = 0ud48_145136608608768
c     v40 = 0ud48_141910014427136
c     v39 = 0ud48_140771848224896
c     v38 = 0ud48_141287244203008
c     v37 = 0ud48_140737490518080
c     v36 = 0ud48_8589948928
c     v35 = 0ud48_138430464
c     v34 = 0ud48_70643638863872
c     v33 = 0ud48_139049568256
c     v32 = 0ud48_3298534885888
c     v31 = 0ud48_4402341611520
c     v30 = 0ud48_652835031040
c     v29 = 0ud48_3264
c     v28 = 0ud48_33654784
c     v27 = 0ud48_17592190246916
c     v26 = 0ud48_17867198173184
c     v25 = 0ud48_87962003980288
c     v24 = 0ud48_18829153402880
c     v23 = 0ud48_17592723046912
c     v22 = 0ud48_20345260081152
c     v21 = 0ud48_22024592293952
c     v20 = 0ud48_17660939076608
c     v19 = 0ud48_17592186110112
c     v18 = 0ud48_274945024016
c     v17 = 0ud48_1275068420
c     v16 = 0ud48_71468322918400
c     v15 = 0ud48_137506209792
c     v14 = 0ud48_549839700480
c     v13 = 0ud48_4898947136
c     v12 = 0ud48_2233483657216
c     v11 = 0ud48_4398113621024
c     v10 = 0ud48_68786651138
c     v9 = 0ud48_8797166772224
c     v8 = 0ud48_9895738867728
c     v7 = 0ud48_79164837330948
c     v6 = 0ud48_9483287793664
c     v5 = 0ud48_8796093039168
c     v4 = 0ud48_8800438321152
c     v3 = 0ud48_8830989631520
c     v2 = 0ud48_10995116278786
c     v1 = 0ud48_13194139598848
c     v0 = 0ud48_0
s 3 15 27 34 40 46 62 77
t 8 15 21 36 43 46 65 77
a YES
a 3 15 27 34 40 46 62 77
a 15 27 34 40 46 62 65 77
a 15 21 34 40 46 62 65 77
a 15 21 36 40 46 62 65 77
a 15 21 36 43 46 62 65 77
a 8 15 21 36 43 46 65 77