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/queen008x008_02_8804.smv > queen008x008_02_8804.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: 51
c Sum: 297
c MaxSize: 0
c Time: 25
c Aborted: false
c ML = 63
c SIZE = 64
c Removed 9 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,3][3,4][4,4][5,5][6,4][7,4][8,18]}
c NODE covering index distribution:{[3,4][4,57][5,3]}
c EDGE covering index distrubution:{[1,719][2,9]}
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 -- no counterexample found with bound 10
c -- no counterexample found with bound 11
c -- specification  G (((((((state.token[1] = v4 & state.token[2] = v15) & state.token[3] = v17) & state.token[4] = v32) & state.token[5] = v37) & state.token[6] = v54) & state.token[7] = v59) ->  G !((((((((((((state.token[1] = v51 | state.token[1] = v47) | state.token[1] = v62) | state.token[1] = v24) | state.token[1] = v5) | state.token[1] = v10) | state.token[1] = v25) & ((((((state.token[2] = v51 | state.token[2] = v47) | state.token[2] = v62) | state.token[2] = v24) | state.token[2] = v5) | state.token[2] = v10) | state.token[2] = v25)) & ((((((state.token[3] = v51 | state.token[3] = v47) | state.token[3] = v62) | state.token[3] = v24) | state.token[3] = v5) | state.token[3] = v10) | state.token[3] = v25)) & ((((((state.token[4] = v51 | state.token[4] = v47) | state.token[4] = v62) | state.token[4] = v24) | state.token[4] = v5) | state.token[4] = v10) | state.token[4] = v25)) & ((((((state.token[5] = v51 | state.token[5] = v47) | state.token[5] = v62) | state.token[5] = v24) | state.token[5] = v5) | state.token[5] = v10) | state.token[5] = v25)) & ((((((state.token[6] = v51 | state.token[6] = v47) | state.token[6] = v62) | state.token[6] = v24) | state.token[6] = v5) | state.token[6] = v10) | state.token[6] = v25)) & ((((((state.token[7] = v51 | state.token[7] = v47) | state.token[7] = v62) | state.token[7] = v24) | state.token[7] = v5) | state.token[7] = v10) | state.token[7] = v25)))    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] = 0ud42_1133871370304
c     state.token[2] = 0ud42_2337535950864
c     state.token[3] = 0ud42_4299309056
c     state.token[4] = 0ud42_275146866944
c     state.token[5] = 0ud42_9227468800
c     state.token[6] = 0ud42_552054292512
c     state.token[7] = 0ud42_68719575168
c     state.tid = 1
c     state.vid = 34
c     state.target = 0ud42_0
c     v64 = 0ud42_275414810624
c     v63 = 0ud42_550963806208
c     v62 = 0ud42_2151710724
c     v61 = 0ud42_67149856
c     v60 = 0ud42_34359771904
c     v59 = 0ud42_68719575168
c     v58 = 0ud42_34635777
c     v57 = 0ud42_137439117312
c     v56 = 0ud42_824652595200
c     v55 = 0ud42_551383203844
c     v54 = 0ud42_552054292512
c     v53 = 0ud42_88080640
c     v52 = 0ud42_34376589312
c     v51 = 0ud42_68769808896
c     v50 = 0ud42_137456779392
c     v49 = 0ud42_17196777473
c     v48 = 0ud42_274886557700
c     v47 = 0ud42_550831915040
c     v46 = 0ud42_2684616960
c     v45 = 0ud42_201654272
c     v44 = 0ud42_34397749248
c     v43 = 0ud42_206158700544
c     v42 = 0ud42_17181180416
c     v41 = 0ud42_393352
c     v40 = 0ud42_283467845664
c     v39 = 0ud42_9672065280
c     v38 = 0ud42_10739580928
c     v37 = 0ud42_9227468800
c     v36 = 0ud42_180522844160
c     v35 = 0ud42_94493474816
c     v34 = 0ud42_8590991368
c     v33 = 0ud42_8590068224
c     v32 = 0ud42_275146866944
c     v31 = 0ud42_1074335744
c     v30 = 0ud42_2189950976
c     v29 = 0ud42_137508683776
c     v28 = 0ud42_52077002752
c     v27 = 0ud42_68854218760
c     v26 = 0ud42_5769216
c     v25 = 0ud42_663616
c     v24 = 0ud42_279172939792
c     v23 = 0ud42_5670699008
c     v22 = 0ud42_143881408512
c     v21 = 0ud42_21550333952
c     v20 = 0ud42_38656802824
c     v19 = 0ud42_73551316992
c     v18 = 0ud42_4430233664
c     v17 = 0ud42_4299309056
c     v16 = 0ud42_2473934716930
c     v15 = 0ud42_2337535950864
c     v14 = 0ud42_2218619043840
c     v13 = 0ud42_2199090368520
c     v12 = 0ud42_2233391384576
c     v11 = 0ud42_2267744829504
c     v10 = 0ud42_2199561191424
c     v9 = 0ud42_2199157605376
c     v8 = 0ud42_1511828488192
c     v7 = 0ud42_1117765238786
c     v6 = 0ud42_1101659111448
c     v5 = 0ud42_1099847174144
c     v4 = 0ud42_1133871370304
c     v3 = 0ud42_1168239509504
c     v2 = 0ud42_1099514774528
c     v1 = 0ud42_1100048629760
c     v0 = 0ud42_0
c   -> State: 1.2 <-
c     state.tid = 5
c     state.vid = 21
c     state.target = 0ud42_8590991368
c   -> State: 1.3 <-
c     state.token[5] = 0ud42_8590991368
c     state.tid = 3
c     state.vid = 33
c     state.target = 0ud42_21550333952
c   -> State: 1.4 <-
c     state.token[3] = 0ud42_21550333952
c     state.tid = 5
c     state.vid = 10
c     state.target = 0ud42_8590068224
c   -> State: 1.5 <-
c     state.token[5] = 0ud42_8590068224
c     state.tid = 2
c     state.vid = 47
c     state.target = 0ud42_2199561191424
c   -> State: 1.6 <-
c     state.token[2] = 0ud42_2199561191424
c     state.tid = 6
c     state.vid = 62
c     state.target = 0ud42_550831915040
c   -> State: 1.7 <-
c     state.token[6] = 0ud42_550831915040
c     state.tid = 7
c     state.vid = 51
c     state.target = 0ud42_2151710724
c   -> State: 1.8 <-
c     state.token[7] = 0ud42_2151710724
c     state.tid = 5
c     state.vid = 36
c     state.target = 0ud42_68769808896
c   -> State: 1.9 <-
c     state.token[5] = 0ud42_68769808896
c     state.tid = 1
c     state.vid = 25
c     state.target = 0ud42_180522844160
c   -> State: 1.10 <-
c     state.token[1] = 0ud42_180522844160
c     state.tid = 4
c     state.vid = 5
c     state.target = 0ud42_663616
c   -> State: 1.11 <-
c     state.token[4] = 0ud42_663616
c     state.tid = 3
c     state.vid = 24
c     state.target = 0ud42_1099847174144
c   -> State: 1.12 <-
c     state.token[3] = 0ud42_1099847174144
c     state.tid = 1
c     state.vid = 41
c     state.target = 0ud42_279172939792
c   -> State: 1.13 <-
c     state.token[1] = 0ud42_279172939792
c     state.vid = 1
c     state.target = 0ud42_393352
s 59 15 4 54 32 37 17
t 51 47 62 24 5 10 25
a YES
a 4 15 17 32 37 54 59
a 4 15 17 32 34 54 59
a 4 15 21 32 34 54 59
a 4 15 21 32 33 54 59
a 4 10 21 32 33 54 59
a 4 10 21 32 33 47 59
a 4 10 21 32 33 47 62
a 4 10 21 32 47 51 62
a 10 21 32 36 47 51 62
a 10 21 25 36 47 51 62
a 5 10 25 36 47 51 62
a 5 10 24 25 36 47 51
a 5 10 24 25 47 51 62