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/queen6_6_01.smv > queen6_6_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: 36
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 290
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: 41
c Sum: 192
c MaxSize: 0
c Time: 17
c Aborted: false
c ML = 35
c SIZE = 36
c Removed 1 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,4][3,2][4,10][5,10][6,14]}
c NODE covering index distribution:{[3,2][4,8][5,14][6,5][7,6][8,1]}
c EDGE covering index distrubution:{[1,206][2,78][3,6]}
c Total edges:290
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] = v5 & state.token[2] = v9) & state.token[3] = v24) & state.token[4] = v28) & state.token[5] = v32) ->  G !((((((((state.token[1] = v3 | state.token[1] = v16) | state.token[1] = v19) | state.token[1] = v29) | state.token[1] = v32) & ((((state.token[2] = v3 | state.token[2] = v16) | state.token[2] = v19) | state.token[2] = v29) | state.token[2] = v32)) & ((((state.token[3] = v3 | state.token[3] = v16) | state.token[3] = v19) | state.token[3] = v29) | state.token[3] = v32)) & ((((state.token[4] = v3 | state.token[4] = v16) | state.token[4] = v19) | state.token[4] = v29) | state.token[4] = v32)) & ((((state.token[5] = v3 | state.token[5] = v16) | state.token[5] = v19) | state.token[5] = v29) | state.token[5] = v32)))    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] = 0ud40_68787634208
c     state.token[2] = 0ud40_10737549840
c     state.token[3] = 0ud40_35032924224
c     state.token[4] = 0ud40_50347268
c     state.token[5] = 0ud40_137715793928
c     state.tid = 1
c     state.vid = 13
c     state.target = 0ud40_0
c     v36 = 0ud40_805306496
c     v35 = 0ud40_154888307712
c     v34 = 0ud40_402921472
c     v33 = 0ud40_8891990016
c     v32 = 0ud40_137715793928
c     v31 = 0ud40_21743796224
c     v30 = 0ud40_536872704
c     v29 = 0ud40_1076893056
c     v28 = 0ud40_50347268
c     v27 = 0ud40_9663959304
c     v26 = 0ud40_8995072
c     v25 = 0ud40_4362092800
c     v24 = 0ud40_35032924224
c     v23 = 0ud40_34396448256
c     v22 = 0ud40_35567708296
c     v21 = 0ud40_60130074626
c     v20 = 0ud40_309447622656
c     v19 = 0ud40_313532809216
c     v18 = 0ud40_550343049216
c     v17 = 0ud40_688271687744
c     v16 = 0ud40_17345024
c     v15 = 0ud40_9735012480
c     v14 = 0ud40_414489542658
c     v13 = 0ud40_279177363456
c     v12 = 0ud40_550292684856
c     v11 = 0ud40_566937255953
c     v10 = 0ud40_201328720
c     v9 = 0ud40_10737549840
c     v8 = 0ud40_2160066704
c     v7 = 0ud40_23622320148
c     v6 = 0ud40_69256871936
c     v5 = 0ud40_68787634208
c     v4 = 0ud40_68736387073
c     v3 = 0ud40_77313605696
c     v2 = 0ud40_70875349504
c     v1 = 0ud40_73018638464
c     v0 = 0ud40_0
c   -> State: 1.2 <-
c     state.tid = 3
c     state.vid = 6
c     state.target = 0ud40_279177363456
c   -> State: 1.3 <-
c     state.token[3] = 0ud40_279177363456
c     state.tid = 1
c     state.vid = 29
c     state.target = 0ud40_69256871936
c   -> State: 1.4 <-
c     state.token[1] = 0ud40_69256871936
c     state.tid = 4
c     state.vid = 10
c     state.target = 0ud40_1076893056
c   -> State: 1.5 <-
c     state.token[4] = 0ud40_1076893056
c     state.tid = 2
c     state.vid = 19
c     state.target = 0ud40_201328720
c   -> State: 1.6 <-
c     state.token[2] = 0ud40_201328720
c     state.tid = 3
c     state.vid = 18
c     state.target = 0ud40_313532809216
c   -> State: 1.7 <-
c     state.token[3] = 0ud40_313532809216
c     state.tid = 1
c     state.vid = 3
c     state.target = 0ud40_550343049216
c   -> State: 1.8 <-
c     state.token[1] = 0ud40_550343049216
c     state.tid = 2
c     state.vid = 16
c     state.target = 0ud40_77313605696
c   -> State: 1.9 <-
c     state.token[2] = 0ud40_77313605696
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud40_17345024
c   -> State: 1.10 <-
c     state.token[1] = 0ud40_17345024
c     state.target = 0ud40_73018638464
s 5 9 24 28 32
t 3 16 19 29 32
a YES
a 5 9 24 28 32
a 5 9 13 28 32
a 6 9 13 28 32
a 6 9 13 29 32
a 6 10 13 29 32
a 6 10 19 29 32
a 10 18 19 29 32
a 3 18 19 29 32
a 3 16 19 29 32