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/david_01.smv > david_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: 87
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 406
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: 259
c MaxSize: 0
c Time: 19
c Aborted: false
c ML = 86
c SIZE = 87
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,19][3,8][4,12][5,5][6,8][7,3][8,2][9,1][10,3]}
c NODE covering index distribution:{[1,40][2,16][3,10][4,8][5,5][6,2][8,2][9,1][10,1][13,1][40,1]}
c EDGE covering index distrubution:{[1,308][2,61][3,18][4,10][5,5][6,3][8,1]}
c Total edges:406
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 -- specification  G ((((((((((((((((((((((((((((((((((((state.token[1] = v1 & state.token[2] = v3) & state.token[3] = v6) & state.token[4] = v7) & state.token[5] = v8) & state.token[6] = v10) & state.token[7] = v11) & state.token[8] = v16) & state.token[9] = v17) & state.token[10] = v18) & state.token[11] = v21) & state.token[12] = v24) & state.token[13] = v25) & state.token[14] = v26) & state.token[15] = v27) & state.token[16] = v29) & state.token[17] = v30) & state.token[18] = v36) & state.token[19] = v38) & state.token[20] = v41) & state.token[21] = v44) & state.token[22] = v48) & state.token[23] = v54) & state.token[24] = v55) & state.token[25] = v56) & state.token[26] = v57) & state.token[27] = v61) & state.token[28] = v62) & state.token[29] = v64) & state.token[30] = v65) & state.token[31] = v68) & state.token[32] = v75) & state.token[33] = v78) & state.token[34] = v81) & state.token[35] = v82) & state.token[36] = v86) ->  G !((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((state.token[1] = v1 | state.token[1] = v3) | state.token[1] = v6) | state.token[1] = v7) | state.token[1] = v8) | state.token[1] = v10) | state.token[1] = v11) | state.token[1] = v16) | state.token[1] = v17) | state.token[1] = v18) | state.token[1] = v21) | state.token[1] = v24) | state.token[1] = v25) | state.token[1] = v26) | state.token[1] = v27) | state.token[1] = v29) | state.token[1] = v30) | state.token[1] = v36) | state.token[1] = v38) | state.token[1] = v41) | state.token[1] = v44) | state.token[1] = v48) | state.token[1] = v54) | state.token[1] = v55) | state.token[1] = v56) | state.token[1] = v57) | state.token[1] = v61) | state.token[1] = v62) | state.token[1] = v64) | state.token[1] = v65) | state.token[1] = v68) | state.token[1] = v75) | state.token[1] = v78) | state.token[1] = v81) | state.token[1] = v82) | state.token[1] = v86) & (((((((((((((((((((((((((((((((((((state.token[2] = v1 | state.token[2] = v3) | state.token[2] = v6) | state.token[2] = v7) | state.token[2] = v8) | state.token[2] = v10) | state.token[2] = v11) | state.token[2] = v16) | state.token[2] = v17) | state.token[2] = v18) | state.token[2] = v21) | state.token[2] = v24) | state.token[2] = v25) | state.token[2] = v26) | state.token[2] = v27) | state.token[2] = v29) | state.token[2] = v30) | state.token[2] = v36) | state.token[2] = v38) | state.token[2] = v41) | state.token[2] = v44) | state.token[2] = v48) | state.token[2] = v54) | state.token[2] = v55) | state.token[2] = v56) | state.token[2] = v57) | state.token[2] = v61) | state.token[2] = v62) | state.token[2] = v64) | state.token[2] = v65) | state.token[2] = v68) | state.token[2] = v75) | state.token[2] = v78) | state.token[2] = v81) | state.token[2] = v82) | state.token[2] = v86)) & (((((((((((((((((((((((((((((((((((state.token[3] = v1 | state.token[3] = v3) | state.token[3] = v6) | state.token[3] = v7) | state.token[3] = v8) | state.token[3] = v10) | state.token[3] = v11) | state.token[3] = v16) | state.token[3] = v17) | state.token[3] = v18) | state.token[3] = v21) | state.token[3] = v24) | state.token[3] = v25) | state.token[3] = v26) | state.token[3] = v27) | state.token[3] = v29) | state.token[3] = v30) | state.token[3] = v36) | state.token[3] = v38) | state.token[3] = v41) | state.token[3] = v44) | state.token[3] = v48) | state.token[3] = v54) | state.token[3] = v55) | state.token[3] = v56) | state.token[3] = v57) | state.token[3] = v61) | state.token[3] = v62) | state.token[3] = v64) | state.token[3] = v65) | state.token[3] = v68) | state.token[3] = v75) | state.token[3] = v78) | state.token[3] = v81) | state.token[3] = v82) | state.token[3] = v86)) & (((((((((((((((((((((((((((((((((((state.token[4] = v1 | state.token[4] = v3) | state.token[4] = v6) | state.token[4] = v7) | state.token[4] = v8) | state.token[4] = v10) | state.token[4] = v11) | state.token[4] = v16) | state.token[4] = v17) | state.token[4] = v18) | state.token[4] = v21) | state.token[4] = v24) | state.token[4] = v25) | state.token[4] = v26) | state.token[4] = v27) | state.token[4] = v29) | state.token[4] = v30) | state.token[4] = v36) | state.token[4] = v38) | state.token[4] = v41) | state.token[4] = v44) | state.token[4] = v48) | state.token[4] = v54) | state.token[4] = v55) | state.token[4] = v56) | state.token[4] = v57) | state.token[4] = v61) | state.token[4] = v62) | state.token[4] = v64) | state.token[4] = v65) | state.token[4] = v68) | state.token[4] = v75) | state.token[4] = v78) | state.token[4] = v81) | state.token[4] = v82) | state.token[4] = v86)) & (((((((((((((((((((((((((((((((((((state.token[5] = v1 | state.token[5] = v3) | state.token[5] = v6) | state.token[5] = v7) | state.token[5] = v8) | state.token[5] = v10) | state.token[5] = v11) | state.token[5] = v16) | state.token[5] = v17) | state.token[5] = v18) | state.token[5] = v21) | state.token[5] = v24) | state.token[5] = v25) | state.token[5] = v26) | state.token[5] = v27) | state.token[5] = v29) | state.token[5] = v30) | state.token[5] = v36) | state.token[5] = v38) | state.token[5] = v41) | state.token[5] = v44) | state.token[5] = v48) | state.token[5] = v54) | state.token[5] = v55) | state.token[5] = v56) | state.token[5] = v57) | state.token[5] = v61) | state.token[5] = v62) | state.token[5] = v64) | state.token[5] = v65) | state.token[5] = v68) | state.token[5] = v75) | state.token[5] = v78) | state.token[5] = v81) | state.token[5] = v82) | state.token[5] = v86)) & (((((((((((((((((((((((((((((((((((state.token[6] = v1 | state.token[6] = v3) | state.token[6] = v6) | state.token[6] = v7) | state.token[6] = v8) | state.token[6] = v10) | state.token[6] = v11) | state.token[6] = v16) | state.token[6] = v17) | state.token[6] = v18) | state.token[6] = v21) | state.token[6] = v24) | state.token[6] = v25) | state.token[6] = v26) | state.token[6] = v27) | state.token[6] = v29) | state.token[6] = v30) | state.token[6] = v36) | state.token[6] = v38) | state.token[6] = v41) | state.token[6] = v44) | state.token[6] = v48) | state.token[6] = v54) | state.token[6] = v55) | state.token[6] = v56) | state.token[6] = v57) | state.token[6] = v61) | state.token[6] = v62) | state.token[6] = v64) | state.token[6] = v65) | state.token[6] = v68) | state.token[6] = v75) | state.token[6] = v78) | state.token[6] = v81) | state.token[6] = v82) | state.token[6] = v86)) & (((((((((((((((((((((((((((((((((((state.token[7] = v1 | state.token[7] = v3) | state.token[7] = v6) | state.token[7] = v7) | state.token[7] = v8) | state.token[7] = v10) | state.token[7] = v11) | state.token[7] = v16) | state.token[7] = v17) | state.token[7] = v18) | state.token[7] = v21) | state.token[7] = v24) | state.token[7] = v25) | state.token[7] = v26) | state.token[7] = v27) | state.token[7] = v29) | state.token[7] = v30) | state.token[7] = v36) | state.token[7] = v38) | state.token[7] = v41) | state.token[7] = v44) | state.token[7] = v48) | state.token[7] = v54) | state.token[7] = v55) | state.token[7] = v56) | state.token[7] = v57) | state.token[7] = v61) | state.token[7] = v62) | state.token[7] = v64) | state.token[7] = v65) | state.token[7] = v68) | state.token[7] = v75) | state.token[7] = v78) | state.token[7] = v81) | state.token[7] = v82) | state.token[7] = v86)) & (((((((((((((((((((((((((((((((((((state.token[8] = v1 | state.token[8] = v3) | state.token[8] = v6) | state.token[8] = v7) | state.token[8] = v8) | state.token[8] = v10) | state.token[8] = v11) | state.token[8] = v16) | state.token[8] = v17) | state.token[8] = v18) | state.token[8] = v21) | state.token[8] = v24) | state.token[8] = v25) | state.token[8] = v26) | state.token[8] = v27) | state.token[8] = v29) | state.token[8] = v30) | state.token[8] = v36) | state.token[8] = v38) | state.token[8] = v41) | state.token[8] = v44) | state.token[8] = v48) | state.token[8] = v54) | state.token[8] = v55) | state.token[8] = v56) | state.token[8] = v57) | state.token[8] = v61) | state.token[8] = v62) | state.token[8] = v64) | state.token[8] = v65) | state.token[8] = v68) | state.token[8] = v75) | state.token[8] = v78) | state.token[8] = v81) | state.token[8] = v82) | state.token[8] = v86)) & (((((((((((((((((((((((((((((((((((state.token[9] = v1 | state.token[9] = v3) | state.token[9] = v6) | state.token[9] = v7) | state.token[9] = v8) | state.token[9] = v10) | state.token[9] = v11) | state.token[9] = v16) | state.token[9] = v17) | state.token[9] = v18) | state.token[9] = v21) | state.token[9] = v24) | state.token[9] = v25) | state.token[9] = v26) | state.token[9] = v27) | state.token[9] = v29) | state.token[9] = v30) | state.token[9] = v36) | state.token[9] = v38) | state.token[9] = v41) | state.token[9] = v44) | state.token[9] = v48) | state.token[9] = v54) | state.token[9] = v55) | state.token[9] = v56) | state.token[9] = v57) | state.token[9] = v61) | state.token[9] = v62) | state.token[9] = v64) | state.token[9] = v65) | state.token[9] = v68) | state.token[9] = v75) | state.token[9] = v78) | state.token[9] = v81) | state.token[9] = v82) | state.token[9] = v86)) & (((((((((((((((((((((((((((((((((((state.token[10] = v1 | state.token[10] = v3) | state.token[10] = v6) | state.token[10] = v7) | state.token[10] = v8) | state.token[10] = v10) | state.token[10] = v11) | state.token[10] = v16) | state.token[10] = v17) | state.token[10] = v18) | state.token[10] = v21) | state.token[10] = v24) | state.token[10] = v25) | state.token[10] = v26) | state.token[10] = v27) | state.token[10] = v29) | state.token[10] = v30) | state.token[10] = v36) | state.token[10] = v38) | state.token[10] = v41) | state.token[10] = v44) | state.token[10] = v48) | state.token[10] = v54) | state.token[10] = v55) | state.token[10] = v56) | state.token[10] = v57) | state.token[10] = v61) | state.token[10] = v62) | state.token[10] = v64) | state.token[10] = v65) | state.token[10] = v68) | state.token[10] = v75) | state.token[10] = v78) | state.token[10] = v81) | state.token[10] = v82) | state.token[10] = v86)) & (((((((((((((((((((((((((((((((((((state.token[11] = v1 | state.token[11] = v3) | state.token[11] = v6) | state.token[11] = v7) | state.token[11] = v8) | state.token[11] = v10) | state.token[11] = v11) | state.token[11] = v16) | state.token[11] = v17) | state.token[11] = v18) | state.token[11] = v21) | state.token[11] = v24) | state.token[11] = v25) | state.token[11] = v26) | state.token[11] = v27) | state.token[11] = v29) | state.token[11] = v30) | state.token[11] = v36) | state.token[11] = v38) | state.token[11] = v41) | state.token[11] = v44) | state.token[11] = v48) | state.token[11] = v54) | state.token[11] = v55) | state.token[11] = v56) | state.token[11] = v57) | state.token[11] = v61) | state.token[11] = v62) | state.token[11] = v64) | state.token[11] = v65) | state.token[11] = v68) | state.token[11] = v75) | state.token[11] = v78) | state.token[11] = v81) | state.token[11] = v82) | state.token[11] = v86)) & (((((((((((((((((((((((((((((((((((state.token[12] = v1 | state.token[12] = v3) | state.token[12] = v6) | state.token[12] = v7) | state.token[12] = v8) | state.token[12] = v10) | state.token[12] = v11) | state.token[12] = v16) | state.token[12] = v17) | state.token[12] = v18) | state.token[12] = v21) | state.token[12] = v24) | state.token[12] = v25) | state.token[12] = v26) | state.token[12] = v27) | state.token[12] = v29) | state.token[12] = v30) | state.token[12] = v36) | state.token[12] = v38) | state.token[12] = v41) | state.token[12] = v44) | state.token[12] = v48) | state.token[12] = v54) | state.token[12] = v55) | state.token[12] = v56) | state.token[12] = v57) | state.token[12] = v61) | state.token[12] = v62) | state.token[12] = v64) | state.token[12] = v65) | state.token[12] = v68) | state.token[12] = v75) | state.token[12] = v78) | state.token[12] = v81) | state.token[12] = v82) | state.token[12] = v86)) & (((((((((((((((((((((((((((((((((((state.token[13] = v1 | state.token[13] = v3) | state.token[13] = v6) | state.token[13] = v7) | state.token[13] = v8) | state.token[13] = v10) | state.token[13] = v11) | state.token[13] = v16) | state.token[13] = v17) | state.token[13] = v18) | state.token[13] = v21) | state.token[13] = v24) | state.token[13] = v25) | state.token[13] = v26) | state.token[13] = v27) | state.token[13] = v29) | state.token[13] = v30) | state.token[13] = v36) | state.token[13] = v38) | state.token[13] = v41) | state.token[13] = v44) | state.token[13] = v48) | state.token[13] = v54) | state.token[13] = v55) | state.token[13] = v56) | state.token[13] = v57) | state.token[13] = v61) | state.token[13] = v62) | state.token[13] = v64) | state.token[13] = v65) | state.token[13] = v68) | state.token[13] = v75) | state.token[13] = v78) | state.token[13] = v81) | state.token[13] = v82) | state.token[13] = v86)) & (((((((((((((((((((((((((((((((((((state.token[14] = v1 | state.token[14] = v3) | state.token[14] = v6) | state.token[14] = v7) | state.token[14] = v8) | state.token[14] = v10) | state.token[14] = v11) | state.token[14] = v16) | state.token[14] = v17) | state.token[14] = v18) | state.token[14] = v21) | state.token[14] = v24) | state.token[14] = v25) | state.token[14] = v26) | state.token[14] = v27) | state.token[14] = v29) | state.token[14] = v30) | state.token[14] = v36) | state.token[14] = v38) | state.token[14] = v41) | state.token[14] = v44) | state.token[14] = v48) | state.token[14] = v54) | state.token[14] = v55) | state.token[14] = v56) | state.token[14] = v57) | state.token[14] = v61) | state.token[14] = v62) | state.token[14] = v64) | state.token[14] = v65) | state.token[14] = v68) | state.token[14] = v75) | state.token[14] = v78) | state.token[14] = v81) | state.token[14] = v82) | state.token[14] = v86)) & (((((((((((((((((((((((((((((((((((state.token[15] = v1 | state.token[15] = v3) | state.token[15] = v6) | state.token[15] = v7) | state.token[15] = v8) | state.token[15] = v10) | state.token[15] = v11) | state.token[15] = v16) | state.token[15] = v17) | state.token[15] = v18) | state.token[15] = v21) | state.token[15] = v24) | state.token[15] = v25) | state.token[15] = v26) | state.token[15] = v27) | state.token[15] = v29) | state.token[15] = v30) | state.token[15] = v36) | state.token[15] = v38) | state.token[15] = v41) | state.token[15] = v44) | state.token[15] = v48) | state.token[15] = v54) | state.token[15] = v55) | state.token[15] = v56) | state.token[15] = v57) | state.token[15] = v61) | state.token[15] = v62) | state.token[15] = v64) | state.token[15] = v65) | state.token[15] = v68) | state.token[15] = v75) | state.token[15] = v78) | state.token[15] = v81) | state.token[15] = v82) | state.token[15] = v86)) & (((((((((((((((((((((((((((((((((((state.token[16] = v1 | state.token[16] = v3) | state.token[16] = v6) | state.token[16] = v7) | state.token[16] = v8) | state.token[16] = v10) | state.token[16] = v11) | state.token[16] = v16) | state.token[16] = v17) | state.token[16] = v18) | state.token[16] = v21) | state.token[16] = v24) | state.token[16] = v25) | state.token[16] = v26) | state.token[16] = v27) | state.token[16] = v29) | state.token[16] = v30) | state.token[16] = v36) | state.token[16] = v38) | state.token[16] = v41) | state.token[16] = v44) | state.token[16] = v48) | state.token[16] = v54) | state.token[16] = v55) | state.token[16] = v56) | state.token[16] = v57) | state.token[16] = v61) | state.token[16] = v62) | state.token[16] = v64) | state.token[16] = v65) | state.token[16] = v68) | state.token[16] = v75) | state.token[16] = v78) | state.token[16] = v81) | state.token[16] = v82) | state.token[16] = v86)) & (((((((((((((((((((((((((((((((((((state.token[17] = v1 | state.token[17] = v3) | state.token[17] = v6) | state.token[17] = v7) | state.token[17] = v8) | state.token[17] = v10) | state.token[17] = v11) | state.token[17] = v16) | state.token[17] = v17) | state.token[17] = v18) | state.token[17] = v21) | state.token[17] = v24) | state.token[17] = v25) | state.token[17] = v26) | state.token[17] = v27) | state.token[17] = v29) | state.token[17] = v30) | state.token[17] = v36) | state.token[17] = v38) | state.token[17] = v41) | state.token[17] = v44) | state.token[17] = v48) | state.token[17] = v54) | state.token[17] = v55) | state.token[17] = v56) | state.token[17] = v57) | state.token[17] = v61) | state.token[17] = v62) | state.token[17] = v64) | state.token[17] = v65) | state.token[17] = v68) | state.token[17] = v75) | state.token[17] = v78) | state.token[17] = v81) | state.token[17] = v82) | state.token[17] = v86)) & (((((((((((((((((((((((((((((((((((state.token[18] = v1 | state.token[18] = v3) | state.token[18] = v6) | state.token[18] = v7) | state.token[18] = v8) | state.token[18] = v10) | state.token[18] = v11) | state.token[18] = v16) | state.token[18] = v17) | state.token[18] = v18) | state.token[18] = v21) | state.token[18] = v24) | state.token[18] = v25) | state.token[18] = v26) | state.token[18] = v27) | state.token[18] = v29) | state.token[18] = v30) | state.token[18] = v36) | state.token[18] = v38) | state.token[18] = v41) | state.token[18] = v44) | state.token[18] = v48) | state.token[18] = v54) | state.token[18] = v55) | state.token[18] = v56) | state.token[18] = v57) | state.token[18] = v61) | state.token[18] = v62) | state.token[18] = v64) | state.token[18] = v65) | state.token[18] = v68) | state.token[18] = v75) | state.token[18] = v78) | state.token[18] = v81) | state.token[18] = v82) | state.token[18] = v86)) & (((((((((((((((((((((((((((((((((((state.token[19] = v1 | state.token[19] = v3) | state.token[19] = v6) | state.token[19] = v7) | state.token[19] = v8) | state.token[19] = v10) | state.token[19] = v11) | state.token[19] = v16) | state.token[19] = v17) | state.token[19] = v18) | state.token[19] = v21) | state.token[19] = v24) | state.token[19] = v25) | state.token[19] = v26) | state.token[19] = v27) | state.token[19] = v29) | state.token[19] = v30) | state.token[19] = v36) | state.token[19] = v38) | state.token[19] = v41) | state.token[19] = v44) | state.token[19] = v48) | state.token[19] = v54) | state.token[19] = v55) | state.token[19] = v56) | state.token[19] = v57) | state.token[19] = v61) | state.token[19] = v62) | state.token[19] = v64) | state.token[19] = v65) | state.token[19] = v68) | state.token[19] = v75) | state.token[19] = v78) | state.token[19] = v81) | state.token[19] = v82) | state.token[19] = v86)) & (((((((((((((((((((((((((((((((((((state.token[20] = v1 | state.token[20] = v3) | state.token[20] = v6) | state.token[20] = v7) | state.token[20] = v8) | state.token[20] = v10) | state.token[20] = v11) | state.token[20] = v16) | state.token[20] = v17) | state.token[20] = v18) | state.token[20] = v21) | state.token[20] = v24) | state.token[20] = v25) | state.token[20] = v26) | state.token[20] = v27) | state.token[20] = v29) | state.token[20] = v30) | state.token[20] = v36) | state.token[20] = v38) | state.token[20] = v41) | state.token[20] = v44) | state.token[20] = v48) | state.token[20] = v54) | state.token[20] = v55) | state.token[20] = v56) | state.token[20] = v57) | state.token[20] = v61) | state.token[20] = v62) | state.token[20] = v64) | state.token[20] = v65) | state.token[20] = v68) | state.token[20] = v75) | state.token[20] = v78) | state.token[20] = v81) | state.token[20] = v82) | state.token[20] = v86)) & (((((((((((((((((((((((((((((((((((state.token[21] = v1 | state.token[21] = v3) | state.token[21] = v6) | state.token[21] = v7) | state.token[21] = v8) | state.token[21] = v10) | state.token[21] = v11) | state.token[21] = v16) | state.token[21] = v17) | state.token[21] = v18) | state.token[21] = v21) | state.token[21] = v24) | state.token[21] = v25) | state.token[21] = v26) | state.token[21] = v27) | state.token[21] = v29) | state.token[21] = v30) | state.token[21] = v36) | state.token[21] = v38) | state.token[21] = v41) | state.token[21] = v44) | state.token[21] = v48) | state.token[21] = v54) | state.token[21] = v55) | state.token[21] = v56) | state.token[21] = v57) | state.token[21] = v61) | state.token[21] = v62) | state.token[21] = v64) | state.token[21] = v65) | state.token[21] = v68) | state.token[21] = v75) | state.token[21] = v78) | state.token[21] = v81) | state.token[21] = v82) | state.token[21] = v86)) & (((((((((((((((((((((((((((((((((((state.token[22] = v1 | state.token[22] = v3) | state.token[22] = v6) | state.token[22] = v7) | state.token[22] = v8) | state.token[22] = v10) | state.token[22] = v11) | state.token[22] = v16) | state.token[22] = v17) | state.token[22] = v18) | state.token[22] = v21) | state.token[22] = v24) | state.token[22] = v25) | state.token[22] = v26) | state.token[22] = v27) | state.token[22] = v29) | state.token[22] = v30) | state.token[22] = v36) | state.token[22] = v38) | state.token[22] = v41) | state.token[22] = v44) | state.token[22] = v48) | state.token[22] = v54) | state.token[22] = v55) | state.token[22] = v56) | state.token[22] = v57) | state.token[22] = v61) | state.token[22] = v62) | state.token[22] = v64) | state.token[22] = v65) | state.token[22] = v68) | state.token[22] = v75) | state.token[22] = v78) | state.token[22] = v81) | state.token[22] = v82) | state.token[22] = v86)) & (((((((((((((((((((((((((((((((((((state.token[23] = v1 | state.token[23] = v3) | state.token[23] = v6) | state.token[23] = v7) | state.token[23] = v8) | state.token[23] = v10) | state.token[23] = v11) | state.token[23] = v16) | state.token[23] = v17) | state.token[23] = v18) | state.token[23] = v21) | state.token[23] = v24) | state.token[23] = v25) | state.token[23] = v26) | state.token[23] = v27) | state.token[23] = v29) | state.token[23] = v30) | state.token[23] = v36) | state.token[23] = v38) | state.token[23] = v41) | state.token[23] = v44) | state.token[23] = v48) | state.token[23] = v54) | state.token[23] = v55) | state.token[23] = v56) | state.token[23] = v57) | state.token[23] = v61) | state.token[23] = v62) | state.token[23] = v64) | state.token[23] = v65) | state.token[23] = v68) | state.token[23] = v75) | state.token[23] = v78) | state.token[23] = v81) | state.token[23] = v82) | state.token[23] = v86)) & (((((((((((((((((((((((((((((((((((state.token[24] = v1 | state.token[24] = v3) | state.token[24] = v6) | state.token[24] = v7) | state.token[24] = v8) | state.token[24] = v10) | state.token[24] = v11) | state.token[24] = v16) | state.token[24] = v17) | state.token[24] = v18) | state.token[24] = v21) | state.token[24] = v24) | state.token[24] = v25) | state.token[24] = v26) | state.token[24] = v27) | state.token[24] = v29) | state.token[24] = v30) | state.token[24] = v36) | state.token[24] = v38) | state.token[24] = v41) | state.token[24] = v44) | state.token[24] = v48) | state.token[24] = v54) | state.token[24] = v55) | state.token[24] = v56) | state.token[24] = v57) | state.token[24] = v61) | state.token[24] = v62) | state.token[24] = v64) | state.token[24] = v65) | state.token[24] = v68) | state.token[24] = v75) | state.token[24] = v78) | state.token[24] = v81) | state.token[24] = v82) | state.token[24] = v86)) & (((((((((((((((((((((((((((((((((((state.token[25] = v1 | state.token[25] = v3) | state.token[25] = v6) | state.token[25] = v7) | state.token[25] = v8) | state.token[25] = v10) | state.token[25] = v11) | state.token[25] = v16) | state.token[25] = v17) | state.token[25] = v18) | state.token[25] = v21) | state.token[25] = v24) | state.token[25] = v25) | state.token[25] = v26) | state.token[25] = v27) | state.token[25] = v29) | state.token[25] = v30) | state.token[25] = v36) | state.token[25] = v38) | state.token[25] = v41) | state.token[25] = v44) | state.token[25] = v48) | state.token[25] = v54) | state.token[25] = v55) | state.token[25] = v56) | state.token[25] = v57) | state.token[25] = v61) | state.token[25] = v62) | state.token[25] = v64) | state.token[25] = v65) | state.token[25] = v68) | state.token[25] = v75) | state.token[25] = v78) | state.token[25] = v81) | state.token[25] = v82) | state.token[25] = v86)) & (((((((((((((((((((((((((((((((((((state.token[26] = v1 | state.token[26] = v3) | state.token[26] = v6) | state.token[26] = v7) | state.token[26] = v8) | state.token[26] = v10) | state.token[26] = v11) | state.token[26] = v16) | state.token[26] = v17) | state.token[26] = v18) | state.token[26] = v21) | state.token[26] = v24) | state.token[26] = v25) | state.token[26] = v26) | state.token[26] = v27) | state.token[26] = v29) | state.token[26] = v30) | state.token[26] = v36) | state.token[26] = v38) | state.token[26] = v41) | state.token[26] = v44) | state.token[26] = v48) | state.token[26] = v54) | state.token[26] = v55) | state.token[26] = v56) | state.token[26] = v57) | state.token[26] = v61) | state.token[26] = v62) | state.token[26] = v64) | state.token[26] = v65) | state.token[26] = v68) | state.token[26] = v75) | state.token[26] = v78) | state.token[26] = v81) | state.token[26] = v82) | state.token[26] = v86)) & (((((((((((((((((((((((((((((((((((state.token[27] = v1 | state.token[27] = v3) | state.token[27] = v6) | state.token[27] = v7) | state.token[27] = v8) | state.token[27] = v10) | state.token[27] = v11) | state.token[27] = v16) | state.token[27] = v17) | state.token[27] = v18) | state.token[27] = v21) | state.token[27] = v24) | state.token[27] = v25) | state.token[27] = v26) | state.token[27] = v27) | state.token[27] = v29) | state.token[27] = v30) | state.token[27] = v36) | state.token[27] = v38) | state.token[27] = v41) | state.token[27] = v44) | state.token[27] = v48) | state.token[27] = v54) | state.token[27] = v55) | state.token[27] = v56) | state.token[27] = v57) | state.token[27] = v61) | state.token[27] = v62) | state.token[27] = v64) | state.token[27] = v65) | state.token[27] = v68) | state.token[27] = v75) | state.token[27] = v78) | state.token[27] = v81) | state.token[27] = v82) | state.token[27] = v86)) & (((((((((((((((((((((((((((((((((((state.token[28] = v1 | state.token[28] = v3) | state.token[28] = v6) | state.token[28] = v7) | state.token[28] = v8) | state.token[28] = v10) | state.token[28] = v11) | state.token[28] = v16) | state.token[28] = v17) | state.token[28] = v18) | state.token[28] = v21) | state.token[28] = v24) | state.token[28] = v25) | state.token[28] = v26) | state.token[28] = v27) | state.token[28] = v29) | state.token[28] = v30) | state.token[28] = v36) | state.token[28] = v38) | state.token[28] = v41) | state.token[28] = v44) | state.token[28] = v48) | state.token[28] = v54) | state.token[28] = v55) | state.token[28] = v56) | state.token[28] = v57) | state.token[28] = v61) | state.token[28] = v62) | state.token[28] = v64) | state.token[28] = v65) | state.token[28] = v68) | state.token[28] = v75) | state.token[28] = v78) | state.token[28] = v81) | state.token[28] = v82) | state.token[28] = v86)) & (((((((((((((((((((((((((((((((((((state.token[29] = v1 | state.token[29] = v3) | state.token[29] = v6) | state.token[29] = v7) | state.token[29] = v8) | state.token[29] = v10) | state.token[29] = v11) | state.token[29] = v16) | state.token[29] = v17) | state.token[29] = v18) | state.token[29] = v21) | state.token[29] = v24) | state.token[29] = v25) | state.token[29] = v26) | state.token[29] = v27) | state.token[29] = v29) | state.token[29] = v30) | state.token[29] = v36) | state.token[29] = v38) | state.token[29] = v41) | state.token[29] = v44) | state.token[29] = v48) | state.token[29] = v54) | state.token[29] = v55) | state.token[29] = v56) | state.token[29] = v57) | state.token[29] = v61) | state.token[29] = v62) | state.token[29] = v64) | state.token[29] = v65) | state.token[29] = v68) | state.token[29] = v75) | state.token[29] = v78) | state.token[29] = v81) | state.token[29] = v82) | state.token[29] = v86)) & (((((((((((((((((((((((((((((((((((state.token[30] = v1 | state.token[30] = v3) | state.token[30] = v6) | state.token[30] = v7) | state.token[30] = v8) | state.token[30] = v10) | state.token[30] = v11) | state.token[30] = v16) | state.token[30] = v17) | state.token[30] = v18) | state.token[30] = v21) | state.token[30] = v24) | state.token[30] = v25) | state.token[30] = v26) | state.token[30] = v27) | state.token[30] = v29) | state.token[30] = v30) | state.token[30] = v36) | state.token[30] = v38) | state.token[30] = v41) | state.token[30] = v44) | state.token[30] = v48) | state.token[30] = v54) | state.token[30] = v55) | state.token[30] = v56) | state.token[30] = v57) | state.token[30] = v61) | state.token[30] = v62) | state.token[30] = v64) | state.token[30] = v65) | state.token[30] = v68) | state.token[30] = v75) | state.token[30] = v78) | state.token[30] = v81) | state.token[30] = v82) | state.token[30] = v86)) & (((((((((((((((((((((((((((((((((((state.token[31] = v1 | state.token[31] = v3) | state.token[31] = v6) | state.token[31] = v7) | state.token[31] = v8) | state.token[31] = v10) | state.token[31] = v11) | state.token[31] = v16) | state.token[31] = v17) | state.token[31] = v18) | state.token[31] = v21) | state.token[31] = v24) | state.token[31] = v25) | state.token[31] = v26) | state.token[31] = v27) | state.token[31] = v29) | state.token[31] = v30) | state.token[31] = v36) | state.token[31] = v38) | state.token[31] = v41) | state.token[31] = v44) | state.token[31] = v48) | state.token[31] = v54) | state.token[31] = v55) | state.token[31] = v56) | state.token[31] = v57) | state.token[31] = v61) | state.token[31] = v62) | state.token[31] = v64) | state.token[31] = v65) | state.token[31] = v68) | state.token[31] = v75) | state.token[31] = v78) | state.token[31] = v81) | state.token[31] = v82) | state.token[31] = v86)) & (((((((((((((((((((((((((((((((((((state.token[32] = v1 | state.token[32] = v3) | state.token[32] = v6) | state.token[32] = v7) | state.token[32] = v8) | state.token[32] = v10) | state.token[32] = v11) | state.token[32] = v16) | state.token[32] = v17) | state.token[32] = v18) | state.token[32] = v21) | state.token[32] = v24) | state.token[32] = v25) | state.token[32] = v26) | state.token[32] = v27) | state.token[32] = v29) | state.token[32] = v30) | state.token[32] = v36) | state.token[32] = v38) | state.token[32] = v41) | state.token[32] = v44) | state.token[32] = v48) | state.token[32] = v54) | state.token[32] = v55) | state.token[32] = v56) | state.token[32] = v57) | state.token[32] = v61) | state.token[32] = v62) | state.token[32] = v64) | state.token[32] = v65) | state.token[32] = v68) | state.token[32] = v75) | state.token[32] = v78) | state.token[32] = v81) | state.token[32] = v82) | state.token[32] = v86)) & (((((((((((((((((((((((((((((((((((state.token[33] = v1 | state.token[33] = v3) | state.token[33] = v6) | state.token[33] = v7) | state.token[33] = v8) | state.token[33] = v10) | state.token[33] = v11) | state.token[33] = v16) | state.token[33] = v17) | state.token[33] = v18) | state.token[33] = v21) | state.token[33] = v24) | state.token[33] = v25) | state.token[33] = v26) | state.token[33] = v27) | state.token[33] = v29) | state.token[33] = v30) | state.token[33] = v36) | state.token[33] = v38) | state.token[33] = v41) | state.token[33] = v44) | state.token[33] = v48) | state.token[33] = v54) | state.token[33] = v55) | state.token[33] = v56) | state.token[33] = v57) | state.token[33] = v61) | state.token[33] = v62) | state.token[33] = v64) | state.token[33] = v65) | state.token[33] = v68) | state.token[33] = v75) | state.token[33] = v78) | state.token[33] = v81) | state.token[33] = v82) | state.token[33] = v86)) & (((((((((((((((((((((((((((((((((((state.token[34] = v1 | state.token[34] = v3) | state.token[34] = v6) | state.token[34] = v7) | state.token[34] = v8) | state.token[34] = v10) | state.token[34] = v11) | state.token[34] = v16) | state.token[34] = v17) | state.token[34] = v18) | state.token[34] = v21) | state.token[34] = v24) | state.token[34] = v25) | state.token[34] = v26) | state.token[34] = v27) | state.token[34] = v29) | state.token[34] = v30) | state.token[34] = v36) | state.token[34] = v38) | state.token[34] = v41) | state.token[34] = v44) | state.token[34] = v48) | state.token[34] = v54) | state.token[34] = v55) | state.token[34] = v56) | state.token[34] = v57) | state.token[34] = v61) | state.token[34] = v62) | state.token[34] = v64) | state.token[34] = v65) | state.token[34] = v68) | state.token[34] = v75) | state.token[34] = v78) | state.token[34] = v81) | state.token[34] = v82) | state.token[34] = v86)) & (((((((((((((((((((((((((((((((((((state.token[35] = v1 | state.token[35] = v3) | state.token[35] = v6) | state.token[35] = v7) | state.token[35] = v8) | state.token[35] = v10) | state.token[35] = v11) | state.token[35] = v16) | state.token[35] = v17) | state.token[35] = v18) | state.token[35] = v21) | state.token[35] = v24) | state.token[35] = v25) | state.token[35] = v26) | state.token[35] = v27) | state.token[35] = v29) | state.token[35] = v30) | state.token[35] = v36) | state.token[35] = v38) | state.token[35] = v41) | state.token[35] = v44) | state.token[35] = v48) | state.token[35] = v54) | state.token[35] = v55) | state.token[35] = v56) | state.token[35] = v57) | state.token[35] = v61) | state.token[35] = v62) | state.token[35] = v64) | state.token[35] = v65) | state.token[35] = v68) | state.token[35] = v75) | state.token[35] = v78) | state.token[35] = v81) | state.token[35] = v82) | state.token[35] = v86)) & (((((((((((((((((((((((((((((((((((state.token[36] = v1 | state.token[36] = v3) | state.token[36] = v6) | state.token[36] = v7) | state.token[36] = v8) | state.token[36] = v10) | state.token[36] = v11) | state.token[36] = v16) | state.token[36] = v17) | state.token[36] = v18) | state.token[36] = v21) | state.token[36] = v24) | state.token[36] = v25) | state.token[36] = v26) | state.token[36] = v27) | state.token[36] = v29) | state.token[36] = v30) | state.token[36] = v36) | state.token[36] = v38) | state.token[36] = v41) | state.token[36] = v44) | state.token[36] = v48) | state.token[36] = v54) | state.token[36] = v55) | state.token[36] = v56) | state.token[36] = v57) | state.token[36] = v61) | state.token[36] = v62) | state.token[36] = v64) | state.token[36] = v65) | state.token[36] = v68) | state.token[36] = v75) | state.token[36] = v78) | state.token[36] = v81) | state.token[36] = v82) | state.token[36] = v86)))    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] = 0ud61_33554432
c     state.token[2] = 0ud61_18014398509482032
c     state.token[3] = 0ud61_1073741824
c     state.token[4] = 0ud61_34359739392
c     state.token[5] = 0ud61_9007199254740992
c     state.token[6] = 0ud61_68719476736
c     state.token[7] = 0ud61_2199023321088
c     state.token[8] = 0ud61_35201560346624
c     state.token[9] = 0ud61_576460752303423488
c     state.token[10] = 0ud61_70368744177920
c     state.token[11] = 0ud61_36028797018968064
c     state.token[12] = 0ud61_140737488355328
c     state.token[13] = 0ud61_16777216
c     state.token[14] = 0ud61_4
c     state.token[15] = 0ud61_536870912
c     state.token[16] = 0ud61_4503599628419072
c     state.token[17] = 0ud61_67108864
c     state.token[18] = 0ud61_2147483648
c     state.token[19] = 0ud61_64
c     state.token[20] = 0ud61_4194304
c     state.token[21] = 0ud61_2097152
c     state.token[22] = 0ud61_8796093022208
c     state.token[23] = 0ud61_1152921504606846976
c     state.token[24] = 0ud61_144396663052566528
c     state.token[25] = 0ud61_72057594037927936
c     state.token[26] = 0ud61_549755813888
c     state.token[27] = 0ud61_1099511627776
c     state.token[28] = 0ud61_8192
c     state.token[29] = 0ud61_512
c     state.token[30] = 0ud61_274877906944
c     state.token[31] = 0ud61_567347999948800
c     state.token[32] = 0ud61_268435456
c     state.token[33] = 0ud61_131072
c     state.token[34] = 0ud61_17592186044416
c     state.token[35] = 0ud61_8
c     state.token[36] = 0ud61_137438953472
c     state.tid = 4
c     state.vid = 1
c     state.target = 0ud61_0
c     v87 = 0ud61_887508228114481154
c     v86 = 0ud61_137438953472
c     v85 = 0ud61_536903680
c     v84 = 0ud61_576460752303423488
c     v83 = 0ud61_2305561512080712268
c     v82 = 0ud61_8
c     v81 = 0ud61_17592186044416
c     v80 = 0ud61_2392537302040576
c     v79 = 0ud61_1125899940401280
c     v78 = 0ud61_131072
c     v77 = 0ud61_35184372088832
c     v76 = 0ud61_1155175503454273536
c     v75 = 0ud61_268435456
c     v74 = 0ud61_180425460071530496
c     v73 = 0ud61_576460752303423488
c     v72 = 0ud61_310748374422781952
c     v71 = 0ud61_9007203550232832
c     v70 = 0ud61_144115188075855872
c     v69 = 0ud61_567352294899712
c     v68 = 0ud61_567347999948800
c     v67 = 0ud61_1159817658717503488
c     v66 = 0ud61_3817659024021504
c     v65 = 0ud61_274877906944
c     v64 = 0ud61_512
c     v63 = 0ud61_35184372088832
c     v62 = 0ud61_8192
c     v61 = 0ud61_1099511627776
c     v60 = 0ud61_536903680
c     v59 = 0ud61_70368744177921
c     v58 = 0ud61_882705565619322880
c     v57 = 0ud61_549755813888
c     v56 = 0ud61_72057594037927936
c     v55 = 0ud61_144396663052566528
c     v54 = 0ud61_1152921504606846976
c     v53 = 0ud61_17592186044416
c     v52 = 0ud61_562952100904960
c     v51 = 0ud61_4398046543872
c     v50 = 0ud61_576460752303423488
c     v49 = 0ud61_10767517370810368
c     v48 = 0ud61_8796093022208
c     v47 = 0ud61_1073741824
c     v46 = 0ud61_180425460072054784
c     v45 = 0ud61_576460752303423488
c     v44 = 0ud61_2097152
c     v43 = 0ud61_17592857133056
c     v42 = 0ud61_52862457479168
c     v41 = 0ud61_4194304
c     v40 = 0ud61_2748779069440
c     v39 = 0ud61_67110912
c     v38 = 0ud61_64
c     v37 = 0ud61_576460752303423488
c     v36 = 0ud61_2147483648
c     v35 = 0ud61_1229482870070837248
c     v34 = 0ud61_180425503021727744
c     v33 = 0ud61_306244774662243328
c     v32 = 0ud61_180425460071530496
c     v31 = 0ud61_8592293888
c     v30 = 0ud61_67108864
c     v29 = 0ud61_4503599628419072
c     v28 = 0ud61_4398046511104
c     v27 = 0ud61_536870912
c     v26 = 0ud61_4
c     v25 = 0ud61_16777216
c     v24 = 0ud61_140737488355328
c     v23 = 0ud61_4503599762636832
c     v22 = 0ud61_35184372088848
c     v21 = 0ud61_36028797018968064
c     v20 = 0ud61_37154696959885315
c     v19 = 0ud61_577322808745426944
c     v18 = 0ud61_70368744177920
c     v17 = 0ud61_576460752303423488
c     v16 = 0ud61_35201560346624
c     v15 = 0ud61_1099511627776
c     v14 = 0ud61_37156895982616576
c     v13 = 0ud61_536870912
c     v12 = 0ud61_36028799166464000
c     v11 = 0ud61_2199023321088
c     v10 = 0ud61_68719476736
c     v9 = 0ud61_2748779069440
c     v8 = 0ud61_9007199254740992
c     v7 = 0ud61_34359739392
c     v6 = 0ud61_1073741824
c     v5 = 0ud61_8590065664
c     v4 = 0ud61_37506540680249344
c     v3 = 0ud61_18014398509482032
c     v2 = 0ud61_1520264130378926208
c     v1 = 0ud61_33554432
c     v0 = 0ud61_0
s 1 3 7 8 10 11 18 21 24 25 26 29 30 36 38 41 44 47 48 54 56 57 61 62 64 65 69 70 75 77 78 81 82 84 85 86
t 1 3 6 7 8 10 11 16 17 18 21 24 25 26 27 29 30 36 38 41 44 48 54 55 56 57 61 62 64 65 68 75 78 81 82 86
a YES
a 1 3 7 8 10 11 18 21 24 25 26 29 30 36 38 41 44 47 48 54 56 57 61 62 64 65 69 70 75 77 78 81 82 84 85 86
a 1 3 6 7 8 10 11 18 21 24 25 26 29 30 36 38 41 44 48 54 56 57 61 62 64 65 69 70 75 77 78 81 82 84 85 86
a 1 3 6 7 8 10 11 18 21 24 25 26 29 30 36 38 41 44 48 54 56 57 61 62 64 65 68 70 75 77 78 81 82 84 85 86
a 1 3 6 7 8 10 11 18 21 24 25 26 29 30 36 38 41 44 48 54 55 56 57 61 62 64 65 68 75 77 78 81 82 84 85 86
a 1 3 6 7 8 10 11 16 18 21 24 25 26 29 30 36 38 41 44 48 54 55 56 57 61 62 64 65 68 75 78 81 82 84 85 86
a 1 3 6 7 8 10 11 16 17 18 21 24 25 26 29 30 36 38 41 44 48 54 55 56 57 61 62 64 65 68 75 78 81 82 85 86
a 1 3 6 7 8 10 11 16 17 18 21 24 25 26 27 29 30 36 38 41 44 48 54 55 56 57 61 62 64 65 68 75 78 81 82 86