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/queen10_10_02.smv > queen10_10_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: 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: 60
c Sum: 429
c MaxSize: 0
c Time: 32
c Aborted: false
c ML = 99
c SIZE = 100
c Removed 6 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,3][3,3][4,4][5,6][6,4][7,4][8,4][9,4][10,22]}
c NODE covering index distribution:{[3,3][4,93][5,4]}
c EDGE covering index distrubution:{[1,1454][2,16]}
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 -- no counterexample found with bound 10
c -- no counterexample found with bound 11
c -- no counterexample found with bound 12
c -- specification  G (((((((((state.token[1] = v3 & state.token[2] = v20) & state.token[3] = v35) & state.token[4] = v49) & state.token[5] = v52) & state.token[6] = v64) & state.token[7] = v77) & state.token[8] = v81) & state.token[9] = v98) ->  G !((((((((((((((((state.token[1] = v3 | state.token[1] = v18) | state.token[1] = v37) | state.token[1] = v49) | state.token[1] = v52) | state.token[1] = v66) | state.token[1] = v71) | state.token[1] = v90) | state.token[1] = v95) & ((((((((state.token[2] = v3 | state.token[2] = v18) | state.token[2] = v37) | state.token[2] = v49) | state.token[2] = v52) | state.token[2] = v66) | state.token[2] = v71) | state.token[2] = v90) | state.token[2] = v95)) & ((((((((state.token[3] = v3 | state.token[3] = v18) | state.token[3] = v37) | state.token[3] = v49) | state.token[3] = v52) | state.token[3] = v66) | state.token[3] = v71) | state.token[3] = v90) | state.token[3] = v95)) & ((((((((state.token[4] = v3 | state.token[4] = v18) | state.token[4] = v37) | state.token[4] = v49) | state.token[4] = v52) | state.token[4] = v66) | state.token[4] = v71) | state.token[4] = v90) | state.token[4] = v95)) & ((((((((state.token[5] = v3 | state.token[5] = v18) | state.token[5] = v37) | state.token[5] = v49) | state.token[5] = v52) | state.token[5] = v66) | state.token[5] = v71) | state.token[5] = v90) | state.token[5] = v95)) & ((((((((state.token[6] = v3 | state.token[6] = v18) | state.token[6] = v37) | state.token[6] = v49) | state.token[6] = v52) | state.token[6] = v66) | state.token[6] = v71) | state.token[6] = v90) | state.token[6] = v95)) & ((((((((state.token[7] = v3 | state.token[7] = v18) | state.token[7] = v37) | state.token[7] = v49) | state.token[7] = v52) | state.token[7] = v66) | state.token[7] = v71) | state.token[7] = v90) | state.token[7] = v95)) & ((((((((state.token[8] = v3 | state.token[8] = v18) | state.token[8] = v37) | state.token[8] = v49) | state.token[8] = v52) | state.token[8] = v66) | state.token[8] = v71) | state.token[8] = v90) | state.token[8] = v95)) & ((((((((state.token[9] = v3 | state.token[9] = v18) | state.token[9] = v37) | state.token[9] = v49) | state.token[9] = v52) | state.token[9] = v66) | state.token[9] = v71) | state.token[9] = v90) | state.token[9] = v95)))    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_2814749775495172
c     state.token[2] = 0ud54_53884659695616
c     state.token[3] = 0ud54_4432408608768
c     state.token[4] = 0ud54_1266637429800960
c     state.token[5] = 0ud54_21474842624
c     state.token[6] = 0ud54_283811443113984
c     state.token[7] = 0ud54_70439879573504
c     state.token[8] = 0ud54_4503600701636610
c     state.token[9] = 0ud54_550359801856
c     state.tid = 1
c     state.vid = 23
c     state.target = 0ud54_0
c     v100 = 0ud54_17592387371008
c     v99 = 0ud54_2215641344
c     v98 = 0ud54_550359801856
c     v97 = 0ud54_137774497800
c     v96 = 0ud54_274961795072
c     v95 = 0ud54_103146324480
c     v94 = 0ud54_2199123935232
c     v93 = 0ud54_562950020661280
c     v92 = 0ud54_25836912642
c     v91 = 0ud54_71827456
c     v90 = 0ud54_4521191815512320
c     v89 = 0ud54_4503599762644992
c     v88 = 0ud54_4504151530668040
c     v87 = 0ud54_4503600449454080
c     v86 = 0ud54_4504080663707648
c     v85 = 0ud54_4503634020665344
c     v84 = 0ud54_4505798650757632
c     v83 = 0ud54_5066558170742784
c     v82 = 0ud54_4503616811434016
c     v81 = 0ud54_4503600701636610
c     v80 = 0ud54_87960938618880
c     v79 = 0ud54_70368747323400
c     v78 = 0ud54_70918650986496
c     v77 = 0ud54_70439879573504
c     v76 = 0ud54_70644192509952
c     v75 = 0ud54_70540543000576
c     v74 = 0ud54_72576357369856
c     v73 = 0ud54_633318701793792
c     v72 = 0ud54_70386997805056
c     v71 = 0ud54_70368744964128
c     v70 = 0ud54_299067162820616
c     v69 = 0ud54_281475002925056
c     v68 = 0ud54_282093454098432
c     v67 = 0ud54_281475412918272
c     v66 = 0ud54_281752002232320
c     v65 = 0ud54_281518463254528
c     v64 = 0ud54_283811443113984
c     v63 = 0ud54_844426003875840
c     v62 = 0ud54_281492156842496
c     v61 = 0ud54_281474977255424
c     v60 = 0ud54_158333986144256
c     v59 = 0ud54_73015558144
c     v58 = 0ud54_554092724224
c     v57 = 0ud54_4565630976
c     v56 = 0ud54_287897026560
c     v55 = 0ud54_40806383616
c     v54 = 0ud54_2204928835584
c     v53 = 0ud54_563091687604224
c     v52 = 0ud54_21474842624
c     v51 = 0ud54_4295524864
c     v50 = 0ud54_1143560812363840
c     v49 = 0ud54_1266637429800960
c     v48 = 0ud54_1126449662853120
c     v47 = 0ud54_1125908773601280
c     v46 = 0ud54_1126174791041024
c     v45 = 0ud54_1125935474540544
c     v44 = 0ud54_1128101077843968
c     v43 = 0ud54_1688850397138944
c     v42 = 0ud54_1126054525698048
c     v41 = 0ud54_1125899907369984
c     v40 = 0ud54_21990266109968
c     v39 = 0ud54_4398047690816
c     v38 = 0ud54_145693880614912
c     v37 = 0ud54_4398319206400
c     v36 = 0ud54_4674006548480
c     v35 = 0ud54_4432408608768
c     v34 = 0ud54_6597203988480
c     v33 = 0ud54_567350147448832
c     v32 = 0ud54_4415763252224
c     v31 = 0ud54_4535485988992
c     v30 = 0ud54_9033587533938688
c     v29 = 0ud54_9042392217813008
c     v28 = 0ud54_9016545107771456
c     v27 = 0ud54_9147938085273600
c     v26 = 0ud54_9007474132975616
c     v25 = 0ud54_9007233622872064
c     v24 = 0ud54_9009398280126464
c     v23 = 0ud54_9570149342381056
c     v22 = 0ud54_9007218582093952
c     v21 = 0ud54_9007199792136196
c     v20 = 0ud54_53884659695616
c     v19 = 0ud54_45079981981696
c     v18 = 0ud54_36834713272336
c     v17 = 0ud54_1099780325440
c     v16 = 0ud54_142111877894144
c     v15 = 0ud54_1133871464448
c     v14 = 0ud54_3298543272960
c     v13 = 0ud54_564049467146368
c     v12 = 0ud54_1116825714692
c     v11 = 0ud54_1101659635713
c     v10 = 0ud54_2278188096946176
c     v9 = 0ud54_2286985260564480
c     v8 = 0ud54_2261145662783488
c     v7 = 0ud54_2251800082124816
c     v6 = 0ud54_2252074691625024
c     v5 = 0ud54_2392571661779968
c     v4 = 0ud54_2253998837006464
c     v3 = 0ud54_2814749775495172
c     v2 = 0ud54_2251816995651585
c     v1 = 0ud54_2251799948427264
c     v0 = 0ud54_0
c   -> State: 1.2 <-
c     state.vid = 4
c     state.target = 0ud54_9570149342381056
c   -> State: 1.3 <-
c     state.token[1] = 0ud54_9570149342381056
c     state.tid = 6
c     state.vid = 66
c     state.target = 0ud54_2253998837006464
c   -> State: 1.4 <-
c     state.token[6] = 0ud54_2253998837006464
c     state.tid = 7
c     state.vid = 97
c     state.target = 0ud54_281752002232320
c   -> State: 1.5 <-
c     state.token[7] = 0ud54_281752002232320
c     state.tid = 9
c     state.vid = 80
c     state.target = 0ud54_137774497800
c   -> State: 1.6 <-
c     state.token[9] = 0ud54_137774497800
c     state.tid = 2
c     state.vid = 18
c     state.target = 0ud54_87960938618880
c   -> State: 1.7 <-
c     state.token[2] = 0ud54_87960938618880
c     state.tid = 8
c     state.vid = 87
c     state.target = 0ud54_36834713272336
c   -> State: 1.8 <-
c     state.token[8] = 0ud54_36834713272336
c     state.tid = 9
c     state.vid = 95
c     state.target = 0ud54_4503600449454080
c   -> State: 1.9 <-
c     state.token[9] = 0ud54_4503600449454080
c     state.tid = 3
c     state.vid = 71
c     state.target = 0ud54_103146324480
c   -> State: 1.10 <-
c     state.token[3] = 0ud54_103146324480
c     state.tid = 2
c     state.vid = 90
c     state.target = 0ud54_70368744964128
c   -> State: 1.11 <-
c     state.token[2] = 0ud54_70368744964128
c     state.tid = 9
c     state.vid = 37
c     state.target = 0ud54_4521191815512320
c   -> State: 1.12 <-
c     state.token[9] = 0ud54_4521191815512320
c     state.tid = 6
c     state.vid = 3
c     state.target = 0ud54_4398319206400
c   -> State: 1.13 <-
c     state.token[6] = 0ud54_4398319206400
c     state.tid = 1
c     state.vid = 73
c     state.target = 0ud54_2814749775495172
c   -> State: 1.14 <-
c     state.token[1] = 0ud54_2814749775495172
c     state.vid = 1
c     state.target = 0ud54_633318701793792
s 6 20 23 35 52 64 77 81 98
t 3 18 37 49 52 66 71 90 95
a YES
a 6 20 23 35 52 64 77 81 98
a 6 20 35 49 52 64 77 81 98
a 3 20 35 49 52 64 77 81 98
a 20 23 35 49 52 64 77 81 98
a 4 20 23 35 49 52 77 81 98
a 4 20 23 35 49 52 66 81 98
a 4 20 23 35 49 52 66 81 97
a 4 23 35 49 52 66 80 81 97
a 4 18 23 35 49 52 66 80 97
a 4 18 23 35 49 52 66 80 87
a 4 18 23 49 52 66 80 87 95
a 4 18 23 49 52 66 71 87 95
a 4 18 23 49 52 66 71 90 95
a 18 23 37 49 52 66 71 90 95
a 3 18 37 49 52 66 71 90 95