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/queen010x010_02_5832.smv > queen010x010_02_5832.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: 434
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,2][4,5][5,5][6,4][7,4][8,4][9,4][10,22]}
c NODE covering index distribution:{[3,2][4,97][5,1]}
c EDGE covering index distrubution:{[1,1460][2,10]}
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 -- 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] = v7 & state.token[2] = v13) & state.token[3] = v26) & state.token[4] = v39) & state.token[5] = v41) & state.token[6] = v60) & state.token[7] = v65) & state.token[8] = v82) & state.token[9] = v94) ->  G !((((((((((((((((state.token[1] = v13 | state.token[1] = v54) | state.token[1] = v41) | state.token[1] = v82) | state.token[1] = v75) | state.token[1] = v26) | state.token[1] = v7) | state.token[1] = v69) | state.token[1] = v100) & ((((((((state.token[2] = v13 | state.token[2] = v54) | state.token[2] = v41) | state.token[2] = v82) | state.token[2] = v75) | state.token[2] = v26) | state.token[2] = v7) | state.token[2] = v69) | state.token[2] = v100)) & ((((((((state.token[3] = v13 | state.token[3] = v54) | state.token[3] = v41) | state.token[3] = v82) | state.token[3] = v75) | state.token[3] = v26) | state.token[3] = v7) | state.token[3] = v69) | state.token[3] = v100)) & ((((((((state.token[4] = v13 | state.token[4] = v54) | state.token[4] = v41) | state.token[4] = v82) | state.token[4] = v75) | state.token[4] = v26) | state.token[4] = v7) | state.token[4] = v69) | state.token[4] = v100)) & ((((((((state.token[5] = v13 | state.token[5] = v54) | state.token[5] = v41) | state.token[5] = v82) | state.token[5] = v75) | state.token[5] = v26) | state.token[5] = v7) | state.token[5] = v69) | state.token[5] = v100)) & ((((((((state.token[6] = v13 | state.token[6] = v54) | state.token[6] = v41) | state.token[6] = v82) | state.token[6] = v75) | state.token[6] = v26) | state.token[6] = v7) | state.token[6] = v69) | state.token[6] = v100)) & ((((((((state.token[7] = v13 | state.token[7] = v54) | state.token[7] = v41) | state.token[7] = v82) | state.token[7] = v75) | state.token[7] = v26) | state.token[7] = v7) | state.token[7] = v69) | state.token[7] = v100)) & ((((((((state.token[8] = v13 | state.token[8] = v54) | state.token[8] = v41) | state.token[8] = v82) | state.token[8] = v75) | state.token[8] = v26) | state.token[8] = v7) | state.token[8] = v69) | state.token[8] = v100)) & ((((((((state.token[9] = v13 | state.token[9] = v54) | state.token[9] = v41) | state.token[9] = v82) | state.token[9] = v75) | state.token[9] = v26) | state.token[9] = v7) | state.token[9] = v69) | 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_70368778125312
c     state.token[2] = 0ud54_4508272551788545
c     state.token[3] = 0ud54_8728363008
c     state.token[4] = 0ud54_704375685120
c     state.token[5] = 0ud54_9007200330582016
c     state.token[6] = 0ud54_562954248389888
c     state.token[7] = 0ud54_175922397323264
c     state.token[8] = 0ud54_292470092988418
c     state.token[9] = 0ud54_1099528409216
c     state.tid = 1
c     state.vid = 80
c     state.target = 0ud54_0
c     v100 = 0ud54_2814749783883776
c     v99 = 0ud54_17609382756352
c     v98 = 0ud54_34376523808
c     v97 = 0ud54_70368761479680
c     v96 = 0ud54_1094713600
c     v95 = 0ud54_140806224609344
c     v94 = 0ud54_1099528409216
c     v93 = 0ud54_4503737083101186
c     v92 = 0ud54_8796646703104
c     v91 = 0ud54_281474995585024
c     v90 = 0ud54_565423854649344
c     v89 = 0ud54_2254016016810016
c     v88 = 0ud54_19825569038848
c     v87 = 0ud54_72567767441664
c     v86 = 0ud54_2267747450880
c     v85 = 0ud54_142937585356800
c     v84 = 0ud54_3435973836864
c     v83 = 0ud54_4505799187497088
c     v82 = 0ud54_292470092988418
c     v81 = 0ud54_2201172869120
c     v80 = 0ud54_562950230245408
c     v79 = 0ud54_292326212096
c     v78 = 0ud54_2251834441859328
c     v77 = 0ud54_88029918134272
c     v76 = 0ud54_272642048
c     v75 = 0ud54_140875196268544
c     v74 = 0ud54_1101390675968
c     v73 = 0ud54_4785074872516672
c     v72 = 0ud54_8798508941440
c     v71 = 0ud54_404750338
c     v70 = 0ud54_598134325527040
c     v69 = 0ud54_35201560346880
c     v68 = 0ud54_35562329210880
c     v67 = 0ud54_2357352929955840
c     v66 = 0ud54_52914001281024
c     v65 = 0ud54_175922397323264
c     v64 = 0ud54_317758860951552
c     v63 = 0ud54_4538787220684800
c     v62 = 0ud54_43980599328832
c     v61 = 0ud54_35184374448256
c     v60 = 0ud54_562954248389888
c     v59 = 0ud54_90194329600
c     v58 = 0ud54_38663098368
c     v57 = 0ud54_70785356005376
c     v56 = 0ud54_2251804649717760
c     v55 = 0ud54_439808946077696
c     v54 = 0ud54_1105954086912
c     v53 = 0ud54_4503604057079808
c     v52 = 0ud54_8801461993472
c     v51 = 0ud54_4297064528
c     v50 = 0ud54_9570217928687616
c     v49 = 0ud54_9007216434615296
c     v48 = 0ud54_9007371053449216
c     v47 = 0ud54_9077568544178176
c     v46 = 0ud54_9288949113552896
c     v45 = 0ud54_11399738704265216
c     v44 = 0ud54_9025891086630912
c     v43 = 0ud54_13510798882381824
c     v42 = 0ud54_9015995348287504
c     v41 = 0ud54_9007200330582016
c     v40 = 0ud54_563499709370368
c     v39 = 0ud54_704375685120
c     v38 = 0ud54_584652424192
c     v37 = 0ud54_352393476718592
c     v36 = 0ud54_551915880448
c     v35 = 0ud54_141562256293888
c     v34 = 0ud54_2253449081389056
c     v33 = 0ud54_4521741569228816
c     v32 = 0ud54_9345848846336
c     v31 = 0ud54_549758435329
c     v30 = 0ud54_563096049418240
c     v29 = 0ud54_26306805760
c     v28 = 0ud54_281517927432192
c     v27 = 0ud54_70379481596928
c     v26 = 0ud54_8728363008
c     v25 = 0ud54_140746086940672
c     v24 = 0ud54_1382979469328
c     v23 = 0ud54_7881307937835008
c     v22 = 0ud54_26396869001217
c     v21 = 0ud54_1125908498882560
c     v20 = 0ud54_567348536803336
c     v19 = 0ud54_285890270199808
c     v18 = 0ud54_4434553864192
c     v17 = 0ud54_74766925955072
c     v16 = 0ud54_4398050968576
c     v15 = 0ud54_145135534882832
c     v14 = 0ud54_5497566529536
c     v13 = 0ud54_4508272551788545
c     v12 = 0ud54_3390893860061184
c     v11 = 0ud54_21990234652676
c     v10 = 0ud54_844425030795264
c     v9 = 0ud54_19360907272
c     v8 = 0ud54_34594619392
c     v7 = 0ud54_70368778125312
c     v6 = 0ud54_38797328
c     v5 = 0ud54_140737521912832
c     v4 = 0ud54_1099545198593
c     v3 = 0ud54_5629499576156160
c     v2 = 0ud54_9071004483588
c     v1 = 0ud54_3377699756179456
c     v0 = 0ud54_0
c   -> State: 1.2 <-
c     state.tid = 6
c     state.vid = 51
c     state.target = 0ud54_562950230245408
c   -> State: 1.3 <-
c     state.token[6] = 0ud54_562950230245408
c     state.tid = 5
c     state.vid = 45
c     state.target = 0ud54_4297064528
c   -> State: 1.4 <-
c     state.token[5] = 0ud54_4297064528
c     state.tid = 7
c     state.vid = 38
c     state.target = 0ud54_11399738704265216
c   -> State: 1.5 <-
c     state.token[7] = 0ud54_11399738704265216
c     state.tid = 4
c     state.vid = 69
c     state.target = 0ud54_584652424192
c   -> State: 1.6 <-
c     state.token[4] = 0ud54_584652424192
c     state.tid = 6
c     state.vid = 75
c     state.target = 0ud54_35201560346880
c   -> State: 1.7 <-
c     state.token[6] = 0ud54_35201560346880
c     state.tid = 7
c     state.vid = 41
c     state.target = 0ud54_140875196268544
c   -> State: 1.8 <-
c     state.token[7] = 0ud54_140875196268544
c     state.tid = 5
c     state.vid = 54
c     state.target = 0ud54_9007200330582016
c   -> State: 1.9 <-
c     state.token[5] = 0ud54_9007200330582016
c     state.tid = 9
c     state.vid = 100
c     state.target = 0ud54_1105954086912
c   -> State: 1.10 <-
c     state.token[9] = 0ud54_1105954086912
c     state.tid = 4
c     state.vid = 45
c     state.target = 0ud54_2814749783883776
c   -> State: 1.11 <-
c     state.token[4] = 0ud54_2814749783883776
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud54_11399738704265216
s 26 39 77 41 94 60 65 82 18
t 13 54 41 82 75 26 7 69 100
a YES
a 18 26 39 41 60 65 77 82 94
a 13 26 39 41 60 65 77 82 94
a 7 13 26 39 41 60 65 82 94
a 7 13 26 39 41 65 80 82 94
a 7 13 26 39 51 65 80 82 94
a 7 13 26 39 45 51 80 82 94
a 7 13 26 38 45 51 80 82 94
a 7 13 26 38 45 51 69 82 94
a 7 13 26 38 51 69 75 82 94
a 7 13 26 38 41 69 75 82 94
a 7 13 26 38 41 54 69 75 82
a 7 13 26 41 54 69 75 82 100