c model ISR_TJ
c  /home/toda/src/NuSMV-2.6.0-Linux_untouched/binary/bin/NuSMV -bmc -bmc_length 40 -n 0 /home/toda/2022solver/bin/../tmp/hc-square-02_01.smv > hc-square-02_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: 24
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 33
c 0 cliques
c 2 cliques
c 4 cliques
c 8 cliques
c 16 cliques
c The solution is correct.
c Cliques: 25
c Sum: 54
c MaxSize: 0
c Time: 10
c Aborted: false
c ML = 23
c SIZE = 24
c Removed 0 cliques to minimalize solution.
c Stats already exist, skipping saving step
c Clique size distribution: {[2,21][3,4]}
c NODE covering index distribution:{[2,18][3,6]}
c EDGE covering index distrubution:{[1,33]}
c Total edges:33
c Distributions already exist, skipping saving step
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 -- no counterexample found with bound 13
c -- no counterexample found with bound 14
c -- no counterexample found with bound 15
c -- no counterexample found with bound 16
c -- no counterexample found with bound 17
c -- no counterexample found with bound 18
c -- no counterexample found with bound 19
c -- no counterexample found with bound 20
c -- no counterexample found with bound 21
c -- no counterexample found with bound 22
c -- no counterexample found with bound 23
c -- no counterexample found with bound 24
c -- no counterexample found with bound 25
c -- no counterexample found with bound 26
c -- no counterexample found with bound 27
c -- no counterexample found with bound 28
c -- specification  G ((((((((((state.token[1] = v2 & state.token[2] = v4) & state.token[3] = v7) & state.token[4] = v9) & state.token[5] = v12) & state.token[6] = v14) & state.token[7] = v18) & state.token[8] = v20) & state.token[9] = v21) & state.token[10] = v23) ->  G !((((((((((((((((((state.token[1] = v2 | state.token[1] = v4) | state.token[1] = v8) | state.token[1] = v10) | state.token[1] = v11) | state.token[1] = v13) | state.token[1] = v17) | state.token[1] = v19) | state.token[1] = v22) | state.token[1] = v24) & (((((((((state.token[2] = v2 | state.token[2] = v4) | state.token[2] = v8) | state.token[2] = v10) | state.token[2] = v11) | state.token[2] = v13) | state.token[2] = v17) | state.token[2] = v19) | state.token[2] = v22) | state.token[2] = v24)) & (((((((((state.token[3] = v2 | state.token[3] = v4) | state.token[3] = v8) | state.token[3] = v10) | state.token[3] = v11) | state.token[3] = v13) | state.token[3] = v17) | state.token[3] = v19) | state.token[3] = v22) | state.token[3] = v24)) & (((((((((state.token[4] = v2 | state.token[4] = v4) | state.token[4] = v8) | state.token[4] = v10) | state.token[4] = v11) | state.token[4] = v13) | state.token[4] = v17) | state.token[4] = v19) | state.token[4] = v22) | state.token[4] = v24)) & (((((((((state.token[5] = v2 | state.token[5] = v4) | state.token[5] = v8) | state.token[5] = v10) | state.token[5] = v11) | state.token[5] = v13) | state.token[5] = v17) | state.token[5] = v19) | state.token[5] = v22) | state.token[5] = v24)) & (((((((((state.token[6] = v2 | state.token[6] = v4) | state.token[6] = v8) | state.token[6] = v10) | state.token[6] = v11) | state.token[6] = v13) | state.token[6] = v17) | state.token[6] = v19) | state.token[6] = v22) | state.token[6] = v24)) & (((((((((state.token[7] = v2 | state.token[7] = v4) | state.token[7] = v8) | state.token[7] = v10) | state.token[7] = v11) | state.token[7] = v13) | state.token[7] = v17) | state.token[7] = v19) | state.token[7] = v22) | state.token[7] = v24)) & (((((((((state.token[8] = v2 | state.token[8] = v4) | state.token[8] = v8) | state.token[8] = v10) | state.token[8] = v11) | state.token[8] = v13) | state.token[8] = v17) | state.token[8] = v19) | state.token[8] = v22) | state.token[8] = v24)) & (((((((((state.token[9] = v2 | state.token[9] = v4) | state.token[9] = v8) | state.token[9] = v10) | state.token[9] = v11) | state.token[9] = v13) | state.token[9] = v17) | state.token[9] = v19) | state.token[9] = v22) | state.token[9] = v24)) & (((((((((state.token[10] = v2 | state.token[10] = v4) | state.token[10] = v8) | state.token[10] = v10) | state.token[10] = v11) | state.token[10] = v13) | state.token[10] = v17) | state.token[10] = v19) | state.token[10] = v22) | state.token[10] = v24)))    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] = 0ud25_1048608
c     state.token[2] = 0ud25_516
c     state.token[3] = 0ud25_16785408
c     state.token[4] = 0ud25_4198400
c     state.token[5] = 0ud25_67712
c     state.token[6] = 0ud25_131152
c     state.token[7] = 0ud25_2359296
c     state.token[8] = 0ud25_557056
c     state.token[9] = 0ud25_9
c     state.token[10] = 0ud25_8404994
c     state.tid = 1
c     state.vid = 5
c     state.target = 0ud25_0
c     v24 = 0ud25_49152
c     v23 = 0ud25_8404994
c     v22 = 0ud25_8650753
c     v21 = 0ud25_9
c     v20 = 0ud25_557056
c     v19 = 0ud25_524290
c     v18 = 0ud25_2359296
c     v17 = 0ud25_2097160
c     v16 = 0ud25_524352
c     v15 = 0ud25_2097408
c     v14 = 0ud25_131152
c     v13 = 0ud25_200704
c     v12 = 0ud25_67712
c     v11 = 0ud25_10496
c     v10 = 0ud25_4194320
c     v9 = 0ud25_4198400
c     v8 = 0ud25_16777344
c     v7 = 0ud25_16785408
c     v6 = 0ud25_4194308
c     v5 = 0ud25_16778240
c     v4 = 0ud25_516
c     v3 = 0ud25_1049088
c     v2 = 0ud25_1048608
c     v1 = 0ud25_1056
c     v0 = 0ud25_0
c   -> State: 1.2 <-
c     state.tid = 3
c     state.vid = 11
c     state.target = 0ud25_16778240
c   -> State: 1.3 <-
c     state.token[3] = 0ud25_16778240
c     state.tid = 5
c     state.vid = 8
c     state.target = 0ud25_10496
c   -> State: 1.4 <-
c     state.token[5] = 0ud25_10496
c     state.tid = 3
c     state.vid = 1
c     state.target = 0ud25_16777344
c   -> State: 1.5 <-
c     state.token[3] = 0ud25_16777344
c     state.tid = 1
c     state.vid = 3
c     state.target = 0ud25_1056
c   -> State: 1.6 <-
c     state.token[1] = 0ud25_1056
c     state.tid = 2
c     state.vid = 6
c     state.target = 0ud25_1049088
c   -> State: 1.7 <-
c     state.token[2] = 0ud25_1049088
c     state.tid = 4
c     state.vid = 13
c     state.target = 0ud25_4194308
c   -> State: 1.8 <-
c     state.token[4] = 0ud25_4194308
c     state.tid = 6
c     state.vid = 16
c     state.target = 0ud25_200704
c   -> State: 1.9 <-
c     state.token[6] = 0ud25_200704
c     state.tid = 8
c     state.vid = 24
c     state.target = 0ud25_524352
c   -> State: 1.10 <-
c     state.token[8] = 0ud25_524352
c     state.tid = 10
c     state.vid = 19
c     state.target = 0ud25_49152
c   -> State: 1.11 <-
c     state.token[10] = 0ud25_49152
c     state.tid = 8
c     state.vid = 14
c     state.target = 0ud25_524290
c   -> State: 1.12 <-
c     state.token[8] = 0ud25_524290
c     state.tid = 6
c     state.vid = 9
c     state.target = 0ud25_131152
c   -> State: 1.13 <-
c     state.token[6] = 0ud25_131152
c     state.tid = 4
c     state.vid = 4
c     state.target = 0ud25_4198400
c   -> State: 1.14 <-
c     state.token[4] = 0ud25_4198400
c     state.tid = 2
c     state.vid = 2
c     state.target = 0ud25_516
c   -> State: 1.15 <-
c     state.token[2] = 0ud25_516
c     state.tid = 1
c     state.vid = 5
c     state.target = 0ud25_1048608
c   -> State: 1.16 <-
c     state.token[1] = 0ud25_1048608
c     state.tid = 3
c     state.vid = 12
c     state.target = 0ud25_16778240
c   -> State: 1.17 <-
c     state.token[3] = 0ud25_16778240
c     state.tid = 5
c     state.vid = 15
c     state.target = 0ud25_67712
c   -> State: 1.18 <-
c     state.token[5] = 0ud25_67712
c     state.tid = 7
c     state.vid = 22
c     state.target = 0ud25_2097408
c   -> State: 1.19 <-
c     state.token[7] = 0ud25_2097408
c     state.tid = 9
c     state.vid = 17
c     state.target = 0ud25_8650753
c   -> State: 1.20 <-
c     state.token[9] = 0ud25_8650753
c     state.tid = 7
c     state.vid = 11
c     state.target = 0ud25_2097160
c   -> State: 1.21 <-
c     state.token[7] = 0ud25_2097160
c     state.tid = 5
c     state.vid = 8
c     state.target = 0ud25_10496
c   -> State: 1.22 <-
c     state.token[5] = 0ud25_10496
c     state.tid = 3
c     state.vid = 1
c     state.target = 0ud25_16777344
c   -> State: 1.23 <-
c     state.token[3] = 0ud25_16777344
c     state.tid = 1
c     state.vid = 3
c     state.target = 0ud25_1056
c   -> State: 1.24 <-
c     state.token[1] = 0ud25_1056
c     state.tid = 2
c     state.vid = 6
c     state.target = 0ud25_1049088
c   -> State: 1.25 <-
c     state.token[2] = 0ud25_1049088
c     state.tid = 4
c     state.vid = 13
c     state.target = 0ud25_4194308
c   -> State: 1.26 <-
c     state.token[4] = 0ud25_4194308
c     state.tid = 6
c     state.vid = 10
c     state.target = 0ud25_200704
c   -> State: 1.27 <-
c     state.token[6] = 0ud25_200704
c     state.tid = 4
c     state.vid = 4
c     state.target = 0ud25_4194320
c   -> State: 1.28 <-
c     state.token[4] = 0ud25_4194320
c     state.tid = 2
c     state.vid = 2
c     state.target = 0ud25_516
c   -> State: 1.29 <-
c     state.token[2] = 0ud25_516
c     state.tid = 1
c     state.vid = 19
c     state.target = 0ud25_1048608
c   -> State: 1.30 <-
c     state.token[1] = 0ud25_1048608
c     state.vid = 1
c     state.target = 0ud25_524290
s 1 3 7 9 12 14 18 20 21 23
t 2 4 8 10 11 13 17 19 22 24
a YES
a 1 3 7 9 12 14 18 20 21 23
a 1 4 7 9 12 14 18 20 21 23
a 2 4 7 9 12 14 18 20 21 23
a 2 4 5 9 12 14 18 20 21 23
a 2 4 5 9 11 14 18 20 21 23
a 2 4 8 9 11 14 18 20 21 23
a 1 4 8 9 11 14 18 20 21 23
a 1 3 8 9 11 14 18 20 21 23
a 1 3 6 8 11 14 18 20 21 23
a 1 3 6 8 11 13 18 20 21 23
a 1 3 6 8 11 13 16 18 21 23
a 1 3 6 8 11 13 16 18 21 24
a 1 3 6 8 11 13 18 19 21 24
a 1 3 6 8 11 14 18 19 21 24
a 1 3 8 9 11 14 18 19 21 24
a 1 4 8 9 11 14 18 19 21 24
a 2 4 8 9 11 14 18 19 21 24
a 2 4 5 9 11 14 18 19 21 24
a 2 4 5 9 12 14 18 19 21 24
a 2 4 5 9 12 14 15 19 21 24
a 2 4 5 9 12 14 15 19 22 24
a 2 4 5 9 12 14 17 19 22 24
a 2 4 5 9 11 14 17 19 22 24
a 2 4 8 9 11 14 17 19 22 24
a 1 4 8 9 11 14 17 19 22 24
a 1 3 8 9 11 14 17 19 22 24
a 1 3 6 8 11 14 17 19 22 24
a 1 3 6 8 11 13 17 19 22 24
a 1 3 8 10 11 13 17 19 22 24
a 1 4 8 10 11 13 17 19 22 24
a 2 4 8 10 11 13 17 19 22 24