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/queen8_8_02.smv > queen8_8_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: 64
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 728
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: 59
c Sum: 331
c MaxSize: 0
c Time: 25
c Aborted: false
c ML = 63
c SIZE = 64
c Removed 11 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,5][3,2][4,6][5,10][6,3][7,4][8,18]}
c NODE covering index distribution:{[3,2][4,41][5,17][6,3][7,1]}
c EDGE covering index distrubution:{[1,677][2,50][3,1]}
c Total edges:728
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 -- no counterexample found with bound 9
c -- specification  G (((((((state.token[1] = v3 & state.token[2] = v13) & state.token[3] = v18) & state.token[4] = v32) & state.token[5] = v38) & state.token[6] = v55) & state.token[7] = v57) ->  G !((((((((((((state.token[1] = v7 | state.token[1] = v12) | state.token[1] = v18) | state.token[1] = v29) | state.token[1] = v40) | state.token[1] = v46) | state.token[1] = v51) & ((((((state.token[2] = v7 | state.token[2] = v12) | state.token[2] = v18) | state.token[2] = v29) | state.token[2] = v40) | state.token[2] = v46) | state.token[2] = v51)) & ((((((state.token[3] = v7 | state.token[3] = v12) | state.token[3] = v18) | state.token[3] = v29) | state.token[3] = v40) | state.token[3] = v46) | state.token[3] = v51)) & ((((((state.token[4] = v7 | state.token[4] = v12) | state.token[4] = v18) | state.token[4] = v29) | state.token[4] = v40) | state.token[4] = v46) | state.token[4] = v51)) & ((((((state.token[5] = v7 | state.token[5] = v12) | state.token[5] = v18) | state.token[5] = v29) | state.token[5] = v40) | state.token[5] = v46) | state.token[5] = v51)) & ((((((state.token[6] = v7 | state.token[6] = v12) | state.token[6] = v18) | state.token[6] = v29) | state.token[6] = v40) | state.token[6] = v46) | state.token[6] = v51)) & ((((((state.token[7] = v7 | state.token[7] = v12) | state.token[7] = v18) | state.token[7] = v29) | state.token[7] = v40) | state.token[7] = v46) | state.token[7] = v51)))    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_5100275714
c     state.token[2] = 0ud48_8796101427264
c     state.token[3] = 0ud48_6047313953024
c     state.token[4] = 0ud48_140781511770112
c     state.token[5] = 0ud48_72705206452224
c     state.token[6] = 0ud48_292057809920
c     state.token[7] = 0ud48_67375104
c     state.tid = 1
c     state.vid = 44
c     state.target = 0ud48_0
c     v64 = 0ud48_140754735334400
c     v63 = 0ud48_4672991527040
c     v62 = 0ud48_87978196074496
c     v61 = 0ud48_8796160270336
c     v60 = 0ud48_8674869256
c     v59 = 0ud48_335609872
c     v58 = 0ud48_18691768975392
c     v57 = 0ud48_67375104
c     v56 = 0ud48_140874927341696
c     v55 = 0ud48_292057809920
c     v54 = 0ud48_74766790729728
c     v53 = 0ud48_8804701863936
c     v52 = 0ud48_1277952
c     v51 = 0ud48_35184644751368
c     v50 = 0ud48_1099511922704
c     v49 = 0ud48_134254624
c     v48 = 0ud48_140754668750848
c     v47 = 0ud48_412317392896
c     v46 = 0ud48_70394531283968
c     v45 = 0ud48_13194140123136
c     v44 = 0ud48_52845300154368
c     v43 = 0ud48_35184641441792
c     v42 = 0ud48_36284018458632
c     v41 = 0ud48_68720005200
c     v40 = 0ud48_142936511635456
c     v39 = 0ud48_2482491099136
c     v38 = 0ud48_72705206452224
c     v37 = 0ud48_10995120473088
c     v36 = 0ud48_6597071077376
c     v35 = 0ud48_37383800094720
c     v34 = 0ud48_3298535014464
c     v33 = 0ud48_2199056814088
c     v32 = 0ud48_140781511770112
c     v31 = 0ud48_309237727232
c     v30 = 0ud48_87995294156800
c     v29 = 0ud48_8967891976192
c     v28 = 0ud48_34495005696
c     v27 = 0ud48_4432674684992
c     v26 = 0ud48_18726093062144
c     v25 = 0ud48_34359873792
c     v24 = 0ud48_141287244235264
c     v23 = 0ud48_825711656960
c     v22 = 0ud48_70918500270080
c     v21 = 0ud48_9345983055872
c     v20 = 0ud48_755915292736
c     v19 = 0ud48_550594675712
c     v18 = 0ud48_6047313953024
c     v17 = 0ud48_620624875522
c     v16 = 0ud48_140737500938244
c     v15 = 0ud48_274886558208
c     v14 = 0ud48_70369960525824
c     v13 = 0ud48_8796101427264
c     v12 = 0ud48_579864576
c     v11 = 0ud48_138252648704
c     v10 = 0ud48_1102204371968
c     v9 = 0ud48_4400202387457
c     v8 = 0ud48_140741783584768
c     v7 = 0ud48_279307091972
c     v6 = 0ud48_70373039145536
c     v5 = 0ud48_8801495285760
c     v4 = 0ud48_4296032512
c     v3 = 0ud48_5100275714
c     v2 = 0ud48_1241245548545
c     v1 = 0ud48_6442456064
c     v0 = 0ud48_0
c   -> State: 1.2 <-
c     state.vid = 7
c     state.target = 0ud48_52845300154368
c   -> State: 1.3 <-
c     state.token[1] = 0ud48_52845300154368
c     state.tid = 6
c     state.vid = 51
c     state.target = 0ud48_279307091972
c   -> State: 1.4 <-
c     state.token[6] = 0ud48_279307091972
c     state.tid = 1
c     state.vid = 12
c     state.target = 0ud48_35184644751368
c   -> State: 1.5 <-
c     state.token[1] = 0ud48_35184644751368
c     state.tid = 2
c     state.vid = 41
c     state.target = 0ud48_579864576
c   -> State: 1.6 <-
c     state.token[2] = 0ud48_579864576
c     state.tid = 7
c     state.vid = 62
c     state.target = 0ud48_68720005200
c   -> State: 1.7 <-
c     state.token[7] = 0ud48_68720005200
c     state.tid = 5
c     state.vid = 40
c     state.target = 0ud48_87978196074496
c   -> State: 1.8 <-
c     state.token[5] = 0ud48_87978196074496
c     state.tid = 4
c     state.vid = 29
c     state.target = 0ud48_142936511635456
c   -> State: 1.9 <-
c     state.token[4] = 0ud48_142936511635456
c     state.tid = 7
c     state.vid = 46
c     state.target = 0ud48_8967891976192
c   -> State: 1.10 <-
c     state.token[7] = 0ud48_8967891976192
c     state.tid = 5
c     state.vid = 2
c     state.target = 0ud48_70394531283968
c   -> State: 1.11 <-
c     state.token[5] = 0ud48_70394531283968
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud48_1241245548545
s 3 13 18 32 38 55 57
t 7 12 18 29 40 46 51
a YES
a 3 13 18 32 38 55 57
a 13 18 32 38 44 55 57
a 7 13 18 32 38 44 57
a 7 13 18 32 38 51 57
a 7 12 18 32 38 51 57
a 7 12 18 32 38 41 51
a 7 12 18 32 41 51 62
a 7 12 18 40 41 51 62
a 7 12 18 29 40 51 62
a 7 12 18 29 40 46 51