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_02.smv > david_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: 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: 60
c Sum: 259
c MaxSize: 0
c Time: 20
c Aborted: false
c ML = 86
c SIZE = 87
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,17][3,10][4,9][5,7][6,8][7,4][8,1][9,1][10,2][11,1]}
c NODE covering index distribution:{[1,40][2,16][3,11][4,6][5,7][6,1][8,2][9,1][10,1][13,1][41,1]}
c EDGE covering index distrubution:{[1,303][2,62][3,24][4,9][5,4][6,1][7,2][9,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] = v3 & state.token[2] = v6) & state.token[3] = v7) & state.token[4] = v8) & state.token[5] = v10) & state.token[6] = v11) & state.token[7] = v24) & state.token[8] = v25) & state.token[9] = v26) & state.token[10] = v28) & state.token[11] = v29) & state.token[12] = v30) & state.token[13] = v36) & state.token[14] = v38) & state.token[15] = v41) & state.token[16] = v44) & state.token[17] = v48) & state.token[18] = v50) & state.token[19] = v53) & state.token[20] = v54) & state.token[21] = v55) & state.token[22] = v56) & state.token[23] = v57) & state.token[24] = v59) & state.token[25] = v60) & state.token[26] = v61) & state.token[27] = v62) & state.token[28] = v64) & state.token[29] = v65) & state.token[30] = v75) & state.token[31] = v77) & state.token[32] = v78) & state.token[33] = v79) & state.token[34] = v82) & state.token[35] = v86) ->  G !((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((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] = v24) | state.token[1] = v25) | state.token[1] = v26) | state.token[1] = v28) | 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] = v50) | state.token[1] = v53) | state.token[1] = v54) | state.token[1] = v55) | state.token[1] = v56) | state.token[1] = v57) | state.token[1] = v59) | state.token[1] = v60) | state.token[1] = v61) | state.token[1] = v62) | state.token[1] = v64) | state.token[1] = v65) | state.token[1] = v75) | state.token[1] = v77) | state.token[1] = v78) | state.token[1] = v79) | state.token[1] = v82) | state.token[1] = v86) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[2] = v25) | state.token[2] = v26) | state.token[2] = v28) | 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] = v50) | state.token[2] = v53) | state.token[2] = v54) | state.token[2] = v55) | state.token[2] = v56) | state.token[2] = v57) | state.token[2] = v59) | state.token[2] = v60) | state.token[2] = v61) | state.token[2] = v62) | state.token[2] = v64) | state.token[2] = v65) | state.token[2] = v75) | state.token[2] = v77) | state.token[2] = v78) | state.token[2] = v79) | state.token[2] = v82) | state.token[2] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[3] = v25) | state.token[3] = v26) | state.token[3] = v28) | 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] = v50) | state.token[3] = v53) | state.token[3] = v54) | state.token[3] = v55) | state.token[3] = v56) | state.token[3] = v57) | state.token[3] = v59) | state.token[3] = v60) | state.token[3] = v61) | state.token[3] = v62) | state.token[3] = v64) | state.token[3] = v65) | state.token[3] = v75) | state.token[3] = v77) | state.token[3] = v78) | state.token[3] = v79) | state.token[3] = v82) | state.token[3] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[4] = v25) | state.token[4] = v26) | state.token[4] = v28) | 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] = v50) | state.token[4] = v53) | state.token[4] = v54) | state.token[4] = v55) | state.token[4] = v56) | state.token[4] = v57) | state.token[4] = v59) | state.token[4] = v60) | state.token[4] = v61) | state.token[4] = v62) | state.token[4] = v64) | state.token[4] = v65) | state.token[4] = v75) | state.token[4] = v77) | state.token[4] = v78) | state.token[4] = v79) | state.token[4] = v82) | state.token[4] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[5] = v25) | state.token[5] = v26) | state.token[5] = v28) | 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] = v50) | state.token[5] = v53) | state.token[5] = v54) | state.token[5] = v55) | state.token[5] = v56) | state.token[5] = v57) | state.token[5] = v59) | state.token[5] = v60) | state.token[5] = v61) | state.token[5] = v62) | state.token[5] = v64) | state.token[5] = v65) | state.token[5] = v75) | state.token[5] = v77) | state.token[5] = v78) | state.token[5] = v79) | state.token[5] = v82) | state.token[5] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[6] = v25) | state.token[6] = v26) | state.token[6] = v28) | 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] = v50) | state.token[6] = v53) | state.token[6] = v54) | state.token[6] = v55) | state.token[6] = v56) | state.token[6] = v57) | state.token[6] = v59) | state.token[6] = v60) | state.token[6] = v61) | state.token[6] = v62) | state.token[6] = v64) | state.token[6] = v65) | state.token[6] = v75) | state.token[6] = v77) | state.token[6] = v78) | state.token[6] = v79) | state.token[6] = v82) | state.token[6] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[7] = v25) | state.token[7] = v26) | state.token[7] = v28) | 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] = v50) | state.token[7] = v53) | state.token[7] = v54) | state.token[7] = v55) | state.token[7] = v56) | state.token[7] = v57) | state.token[7] = v59) | state.token[7] = v60) | state.token[7] = v61) | state.token[7] = v62) | state.token[7] = v64) | state.token[7] = v65) | state.token[7] = v75) | state.token[7] = v77) | state.token[7] = v78) | state.token[7] = v79) | state.token[7] = v82) | state.token[7] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[8] = v25) | state.token[8] = v26) | state.token[8] = v28) | 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] = v50) | state.token[8] = v53) | state.token[8] = v54) | state.token[8] = v55) | state.token[8] = v56) | state.token[8] = v57) | state.token[8] = v59) | state.token[8] = v60) | state.token[8] = v61) | state.token[8] = v62) | state.token[8] = v64) | state.token[8] = v65) | state.token[8] = v75) | state.token[8] = v77) | state.token[8] = v78) | state.token[8] = v79) | state.token[8] = v82) | state.token[8] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[9] = v25) | state.token[9] = v26) | state.token[9] = v28) | 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] = v50) | state.token[9] = v53) | state.token[9] = v54) | state.token[9] = v55) | state.token[9] = v56) | state.token[9] = v57) | state.token[9] = v59) | state.token[9] = v60) | state.token[9] = v61) | state.token[9] = v62) | state.token[9] = v64) | state.token[9] = v65) | state.token[9] = v75) | state.token[9] = v77) | state.token[9] = v78) | state.token[9] = v79) | state.token[9] = v82) | state.token[9] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[10] = v25) | state.token[10] = v26) | state.token[10] = v28) | 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] = v50) | state.token[10] = v53) | state.token[10] = v54) | state.token[10] = v55) | state.token[10] = v56) | state.token[10] = v57) | state.token[10] = v59) | state.token[10] = v60) | state.token[10] = v61) | state.token[10] = v62) | state.token[10] = v64) | state.token[10] = v65) | state.token[10] = v75) | state.token[10] = v77) | state.token[10] = v78) | state.token[10] = v79) | state.token[10] = v82) | state.token[10] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[11] = v25) | state.token[11] = v26) | state.token[11] = v28) | 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] = v50) | state.token[11] = v53) | state.token[11] = v54) | state.token[11] = v55) | state.token[11] = v56) | state.token[11] = v57) | state.token[11] = v59) | state.token[11] = v60) | state.token[11] = v61) | state.token[11] = v62) | state.token[11] = v64) | state.token[11] = v65) | state.token[11] = v75) | state.token[11] = v77) | state.token[11] = v78) | state.token[11] = v79) | state.token[11] = v82) | state.token[11] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[12] = v25) | state.token[12] = v26) | state.token[12] = v28) | 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] = v50) | state.token[12] = v53) | state.token[12] = v54) | state.token[12] = v55) | state.token[12] = v56) | state.token[12] = v57) | state.token[12] = v59) | state.token[12] = v60) | state.token[12] = v61) | state.token[12] = v62) | state.token[12] = v64) | state.token[12] = v65) | state.token[12] = v75) | state.token[12] = v77) | state.token[12] = v78) | state.token[12] = v79) | state.token[12] = v82) | state.token[12] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[13] = v25) | state.token[13] = v26) | state.token[13] = v28) | 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] = v50) | state.token[13] = v53) | state.token[13] = v54) | state.token[13] = v55) | state.token[13] = v56) | state.token[13] = v57) | state.token[13] = v59) | state.token[13] = v60) | state.token[13] = v61) | state.token[13] = v62) | state.token[13] = v64) | state.token[13] = v65) | state.token[13] = v75) | state.token[13] = v77) | state.token[13] = v78) | state.token[13] = v79) | state.token[13] = v82) | state.token[13] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[14] = v25) | state.token[14] = v26) | state.token[14] = v28) | 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] = v50) | state.token[14] = v53) | state.token[14] = v54) | state.token[14] = v55) | state.token[14] = v56) | state.token[14] = v57) | state.token[14] = v59) | state.token[14] = v60) | state.token[14] = v61) | state.token[14] = v62) | state.token[14] = v64) | state.token[14] = v65) | state.token[14] = v75) | state.token[14] = v77) | state.token[14] = v78) | state.token[14] = v79) | state.token[14] = v82) | state.token[14] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[15] = v25) | state.token[15] = v26) | state.token[15] = v28) | 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] = v50) | state.token[15] = v53) | state.token[15] = v54) | state.token[15] = v55) | state.token[15] = v56) | state.token[15] = v57) | state.token[15] = v59) | state.token[15] = v60) | state.token[15] = v61) | state.token[15] = v62) | state.token[15] = v64) | state.token[15] = v65) | state.token[15] = v75) | state.token[15] = v77) | state.token[15] = v78) | state.token[15] = v79) | state.token[15] = v82) | state.token[15] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[16] = v25) | state.token[16] = v26) | state.token[16] = v28) | 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] = v50) | state.token[16] = v53) | state.token[16] = v54) | state.token[16] = v55) | state.token[16] = v56) | state.token[16] = v57) | state.token[16] = v59) | state.token[16] = v60) | state.token[16] = v61) | state.token[16] = v62) | state.token[16] = v64) | state.token[16] = v65) | state.token[16] = v75) | state.token[16] = v77) | state.token[16] = v78) | state.token[16] = v79) | state.token[16] = v82) | state.token[16] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[17] = v25) | state.token[17] = v26) | state.token[17] = v28) | 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] = v50) | state.token[17] = v53) | state.token[17] = v54) | state.token[17] = v55) | state.token[17] = v56) | state.token[17] = v57) | state.token[17] = v59) | state.token[17] = v60) | state.token[17] = v61) | state.token[17] = v62) | state.token[17] = v64) | state.token[17] = v65) | state.token[17] = v75) | state.token[17] = v77) | state.token[17] = v78) | state.token[17] = v79) | state.token[17] = v82) | state.token[17] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[18] = v25) | state.token[18] = v26) | state.token[18] = v28) | 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] = v50) | state.token[18] = v53) | state.token[18] = v54) | state.token[18] = v55) | state.token[18] = v56) | state.token[18] = v57) | state.token[18] = v59) | state.token[18] = v60) | state.token[18] = v61) | state.token[18] = v62) | state.token[18] = v64) | state.token[18] = v65) | state.token[18] = v75) | state.token[18] = v77) | state.token[18] = v78) | state.token[18] = v79) | state.token[18] = v82) | state.token[18] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[19] = v25) | state.token[19] = v26) | state.token[19] = v28) | 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] = v50) | state.token[19] = v53) | state.token[19] = v54) | state.token[19] = v55) | state.token[19] = v56) | state.token[19] = v57) | state.token[19] = v59) | state.token[19] = v60) | state.token[19] = v61) | state.token[19] = v62) | state.token[19] = v64) | state.token[19] = v65) | state.token[19] = v75) | state.token[19] = v77) | state.token[19] = v78) | state.token[19] = v79) | state.token[19] = v82) | state.token[19] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[20] = v25) | state.token[20] = v26) | state.token[20] = v28) | 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] = v50) | state.token[20] = v53) | state.token[20] = v54) | state.token[20] = v55) | state.token[20] = v56) | state.token[20] = v57) | state.token[20] = v59) | state.token[20] = v60) | state.token[20] = v61) | state.token[20] = v62) | state.token[20] = v64) | state.token[20] = v65) | state.token[20] = v75) | state.token[20] = v77) | state.token[20] = v78) | state.token[20] = v79) | state.token[20] = v82) | state.token[20] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[21] = v25) | state.token[21] = v26) | state.token[21] = v28) | 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] = v50) | state.token[21] = v53) | state.token[21] = v54) | state.token[21] = v55) | state.token[21] = v56) | state.token[21] = v57) | state.token[21] = v59) | state.token[21] = v60) | state.token[21] = v61) | state.token[21] = v62) | state.token[21] = v64) | state.token[21] = v65) | state.token[21] = v75) | state.token[21] = v77) | state.token[21] = v78) | state.token[21] = v79) | state.token[21] = v82) | state.token[21] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[22] = v25) | state.token[22] = v26) | state.token[22] = v28) | 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] = v50) | state.token[22] = v53) | state.token[22] = v54) | state.token[22] = v55) | state.token[22] = v56) | state.token[22] = v57) | state.token[22] = v59) | state.token[22] = v60) | state.token[22] = v61) | state.token[22] = v62) | state.token[22] = v64) | state.token[22] = v65) | state.token[22] = v75) | state.token[22] = v77) | state.token[22] = v78) | state.token[22] = v79) | state.token[22] = v82) | state.token[22] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[23] = v25) | state.token[23] = v26) | state.token[23] = v28) | 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] = v50) | state.token[23] = v53) | state.token[23] = v54) | state.token[23] = v55) | state.token[23] = v56) | state.token[23] = v57) | state.token[23] = v59) | state.token[23] = v60) | state.token[23] = v61) | state.token[23] = v62) | state.token[23] = v64) | state.token[23] = v65) | state.token[23] = v75) | state.token[23] = v77) | state.token[23] = v78) | state.token[23] = v79) | state.token[23] = v82) | state.token[23] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[24] = v25) | state.token[24] = v26) | state.token[24] = v28) | 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] = v50) | state.token[24] = v53) | state.token[24] = v54) | state.token[24] = v55) | state.token[24] = v56) | state.token[24] = v57) | state.token[24] = v59) | state.token[24] = v60) | state.token[24] = v61) | state.token[24] = v62) | state.token[24] = v64) | state.token[24] = v65) | state.token[24] = v75) | state.token[24] = v77) | state.token[24] = v78) | state.token[24] = v79) | state.token[24] = v82) | state.token[24] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[25] = v25) | state.token[25] = v26) | state.token[25] = v28) | 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] = v50) | state.token[25] = v53) | state.token[25] = v54) | state.token[25] = v55) | state.token[25] = v56) | state.token[25] = v57) | state.token[25] = v59) | state.token[25] = v60) | state.token[25] = v61) | state.token[25] = v62) | state.token[25] = v64) | state.token[25] = v65) | state.token[25] = v75) | state.token[25] = v77) | state.token[25] = v78) | state.token[25] = v79) | state.token[25] = v82) | state.token[25] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[26] = v25) | state.token[26] = v26) | state.token[26] = v28) | 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] = v50) | state.token[26] = v53) | state.token[26] = v54) | state.token[26] = v55) | state.token[26] = v56) | state.token[26] = v57) | state.token[26] = v59) | state.token[26] = v60) | state.token[26] = v61) | state.token[26] = v62) | state.token[26] = v64) | state.token[26] = v65) | state.token[26] = v75) | state.token[26] = v77) | state.token[26] = v78) | state.token[26] = v79) | state.token[26] = v82) | state.token[26] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[27] = v25) | state.token[27] = v26) | state.token[27] = v28) | 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] = v50) | state.token[27] = v53) | state.token[27] = v54) | state.token[27] = v55) | state.token[27] = v56) | state.token[27] = v57) | state.token[27] = v59) | state.token[27] = v60) | state.token[27] = v61) | state.token[27] = v62) | state.token[27] = v64) | state.token[27] = v65) | state.token[27] = v75) | state.token[27] = v77) | state.token[27] = v78) | state.token[27] = v79) | state.token[27] = v82) | state.token[27] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[28] = v25) | state.token[28] = v26) | state.token[28] = v28) | 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] = v50) | state.token[28] = v53) | state.token[28] = v54) | state.token[28] = v55) | state.token[28] = v56) | state.token[28] = v57) | state.token[28] = v59) | state.token[28] = v60) | state.token[28] = v61) | state.token[28] = v62) | state.token[28] = v64) | state.token[28] = v65) | state.token[28] = v75) | state.token[28] = v77) | state.token[28] = v78) | state.token[28] = v79) | state.token[28] = v82) | state.token[28] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[29] = v25) | state.token[29] = v26) | state.token[29] = v28) | 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] = v50) | state.token[29] = v53) | state.token[29] = v54) | state.token[29] = v55) | state.token[29] = v56) | state.token[29] = v57) | state.token[29] = v59) | state.token[29] = v60) | state.token[29] = v61) | state.token[29] = v62) | state.token[29] = v64) | state.token[29] = v65) | state.token[29] = v75) | state.token[29] = v77) | state.token[29] = v78) | state.token[29] = v79) | state.token[29] = v82) | state.token[29] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[30] = v25) | state.token[30] = v26) | state.token[30] = v28) | 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] = v50) | state.token[30] = v53) | state.token[30] = v54) | state.token[30] = v55) | state.token[30] = v56) | state.token[30] = v57) | state.token[30] = v59) | state.token[30] = v60) | state.token[30] = v61) | state.token[30] = v62) | state.token[30] = v64) | state.token[30] = v65) | state.token[30] = v75) | state.token[30] = v77) | state.token[30] = v78) | state.token[30] = v79) | state.token[30] = v82) | state.token[30] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[31] = v25) | state.token[31] = v26) | state.token[31] = v28) | 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] = v50) | state.token[31] = v53) | state.token[31] = v54) | state.token[31] = v55) | state.token[31] = v56) | state.token[31] = v57) | state.token[31] = v59) | state.token[31] = v60) | state.token[31] = v61) | state.token[31] = v62) | state.token[31] = v64) | state.token[31] = v65) | state.token[31] = v75) | state.token[31] = v77) | state.token[31] = v78) | state.token[31] = v79) | state.token[31] = v82) | state.token[31] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[32] = v25) | state.token[32] = v26) | state.token[32] = v28) | 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] = v50) | state.token[32] = v53) | state.token[32] = v54) | state.token[32] = v55) | state.token[32] = v56) | state.token[32] = v57) | state.token[32] = v59) | state.token[32] = v60) | state.token[32] = v61) | state.token[32] = v62) | state.token[32] = v64) | state.token[32] = v65) | state.token[32] = v75) | state.token[32] = v77) | state.token[32] = v78) | state.token[32] = v79) | state.token[32] = v82) | state.token[32] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[33] = v25) | state.token[33] = v26) | state.token[33] = v28) | 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] = v50) | state.token[33] = v53) | state.token[33] = v54) | state.token[33] = v55) | state.token[33] = v56) | state.token[33] = v57) | state.token[33] = v59) | state.token[33] = v60) | state.token[33] = v61) | state.token[33] = v62) | state.token[33] = v64) | state.token[33] = v65) | state.token[33] = v75) | state.token[33] = v77) | state.token[33] = v78) | state.token[33] = v79) | state.token[33] = v82) | state.token[33] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[34] = v25) | state.token[34] = v26) | state.token[34] = v28) | 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] = v50) | state.token[34] = v53) | state.token[34] = v54) | state.token[34] = v55) | state.token[34] = v56) | state.token[34] = v57) | state.token[34] = v59) | state.token[34] = v60) | state.token[34] = v61) | state.token[34] = v62) | state.token[34] = v64) | state.token[34] = v65) | state.token[34] = v75) | state.token[34] = v77) | state.token[34] = v78) | state.token[34] = v79) | state.token[34] = v82) | state.token[34] = v86)) & ((((((((((((((((((((((((((((((((((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] = v24) | state.token[35] = v25) | state.token[35] = v26) | state.token[35] = v28) | 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] = v50) | state.token[35] = v53) | state.token[35] = v54) | state.token[35] = v55) | state.token[35] = v56) | state.token[35] = v57) | state.token[35] = v59) | state.token[35] = v60) | state.token[35] = v61) | state.token[35] = v62) | state.token[35] = v64) | state.token[35] = v65) | state.token[35] = v75) | state.token[35] = v77) | state.token[35] = v78) | state.token[35] = v79) | state.token[35] = v82) | state.token[35] = 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] = 0ud60_34393292928
c     state.token[2] = 0ud60_4096
c     state.token[3] = 0ud60_562952100904960
c     state.token[4] = 0ud60_262144
c     state.token[5] = 0ud60_8
c     state.token[6] = 0ud60_35184372090880
c     state.token[7] = 0ud60_17592186044416
c     state.token[8] = 0ud60_8796093022208
c     state.token[9] = 0ud60_32768
c     state.token[10] = 0ud60_4294967296
c     state.token[11] = 0ud60_343597383680
c     state.token[12] = 0ud60_2199023255552
c     state.token[13] = 0ud60_4398046511104
c     state.token[14] = 0ud60_4
c     state.token[15] = 0ud60_256
c     state.token[16] = 0ud60_8388608
c     state.token[17] = 0ud60_32
c     state.token[18] = 0ud60_576460752303423488
c     state.token[19] = 0ud60_70368744177664
c     state.token[20] = 0ud60_288230376151711744
c     state.token[21] = 0ud60_72058693549555712
c     state.token[22] = 0ud60_1048576
c     state.token[23] = 0ud60_512
c     state.token[24] = 0ud60_140875195744256
c     state.token[25] = 0ud60_550292684800
c     state.token[26] = 0ud60_524288
c     state.token[27] = 0ud60_64
c     state.token[28] = 0ud60_1073741824
c     state.token[29] = 0ud60_65536
c     state.token[30] = 0ud60_1024
c     state.token[31] = 0ud60_4503599627370496
c     state.token[32] = 0ud60_131072
c     state.token[33] = 0ud60_2533274792493058
c     state.token[34] = 0ud60_8589934592
c     state.token[35] = 0ud60_1125899906842624
c     state.tid = 5
c     state.vid = 1
c     state.target = 0ud60_0
c     v87 = 0ud60_685180771312336896
c     v86 = 0ud60_1125899906842624
c     v85 = 0ud60_550292684800
c     v84 = 0ud60_576460752303423488
c     v83 = 0ud60_1152920728436184940
c     v82 = 0ud60_8589934592
c     v81 = 0ud60_70368744177664
c     v80 = 0ud60_18031990695526400
c     v79 = 0ud60_2533274792493058
c     v78 = 0ud60_131072
c     v77 = 0ud60_4503599627370496
c     v76 = 0ud60_306279959041679360
c     v75 = 0ud60_1024
c     v74 = 0ud60_81065892804296704
c     v73 = 0ud60_576460752303423488
c     v72 = 0ud60_36029174976086016
c     v71 = 0ud60_140754941116416
c     v70 = 0ud60_1099511627776
c     v69 = 0ud60_144115192375017472
c     v68 = 0ud60_144115192370823169
c     v67 = 0ud60_306262710511732752
c     v66 = 0ud60_93819128241995778
c     v65 = 0ud60_65536
c     v64 = 0ud60_1073741824
c     v63 = 0ud60_4503599627370496
c     v62 = 0ud60_64
c     v61 = 0ud60_524288
c     v60 = 0ud60_550292684800
c     v59 = 0ud60_140875195744256
c     v58 = 0ud60_577023738768261120
c     v57 = 0ud60_512
c     v56 = 0ud60_1048576
c     v55 = 0ud60_72058693549555712
c     v54 = 0ud60_288230376151711744
c     v53 = 0ud60_70368744177664
c     v52 = 0ud60_144119586122366976
c     v51 = 0ud60_4831838208
c     v50 = 0ud60_576460752303423488
c     v49 = 0ud60_146507725378682880
c     v48 = 0ud60_32
c     v47 = 0ud60_4096
c     v46 = 0ud60_81065909984165888
c     v45 = 0ud60_576460752303423488
c     v44 = 0ud60_8388608
c     v43 = 0ud60_36099715518955520
c     v42 = 0ud60_4573968438657032
c     v41 = 0ud60_256
c     v40 = 0ud60_35184372089344
c     v39 = 0ud60_2199023271936
c     v38 = 0ud60_4
c     v37 = 0ud60_576460752303423488
c     v36 = 0ud60_4398046511104
c     v35 = 0ud60_289356553084993536
c     v34 = 0ud60_81065912265867264
c     v33 = 0ud60_563053032636416
c     v32 = 0ud60_81065892804296704
c     v31 = 0ud60_142606352
c     v30 = 0ud60_2199023255552
c     v29 = 0ud60_343597383680
c     v28 = 0ud60_4294967296
c     v27 = 0ud60_549755813888
c     v26 = 0ud60_32768
c     v25 = 0ud60_8796093022208
c     v24 = 0ud60_17592186044416
c     v23 = 0ud60_36029140649902080
c     v22 = 0ud60_4503599627370624
c     v21 = 0ud60_9007199254740994
c     v20 = 0ud60_11540474330349568
c     v19 = 0ud60_828733269800386560
c     v18 = 0ud60_140874927308800
c     v17 = 0ud60_576460752303423488
c     v16 = 0ud60_4503599694487552
c     v15 = 0ud60_524288
c     v14 = 0ud60_11575658417225728
c     v13 = 0ud60_549755813888
c     v12 = 0ud60_9011597301252097
c     v11 = 0ud60_35184372090880
c     v10 = 0ud60_8
c     v9 = 0ud60_35184372089344
c     v8 = 0ud60_262144
c     v7 = 0ud60_562952100904960
c     v6 = 0ud60_4096
c     v5 = 0ud60_134348800
c     v4 = 0ud60_83598205522018304
c     v3 = 0ud60_34393292928
c     v2 = 0ud60_416090659270707200
c     v1 = 0ud60_281474976710656
c     v0 = 0ud60_0
s 1 3 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 3 6 7 8 10 11 24 25 26 28 29 30 36 38 41 44 48 50 53 54 55 56 57 59 60 61 62 64 65 75 77 78 79 82 86
a YES
a 1 3 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 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 3 7 8 10 11 21 24 25 26 29 30 36 38 41 44 47 48 54 56 57 59 61 62 64 65 69 70 75 77 78 81 82 84 85 86
a 3 7 8 10 11 24 25 26 29 30 36 38 41 44 47 48 54 56 57 59 61 62 64 65 69 70 75 77 78 79 81 82 84 85 86
a 3 6 7 8 10 11 24 25 26 29 30 36 38 41 44 48 54 56 57 59 61 62 64 65 69 70 75 77 78 79 81 82 84 85 86
a 3 6 7 8 10 11 24 25 26 28 29 30 36 38 41 44 48 54 56 57 59 61 62 64 65 70 75 77 78 79 81 82 84 85 86
a 3 6 7 8 10 11 24 25 26 28 29 30 36 38 41 44 48 54 55 56 57 59 61 62 64 65 75 77 78 79 81 82 84 85 86
a 3 6 7 8 10 11 24 25 26 28 29 30 36 38 41 44 48 53 54 55 56 57 59 61 62 64 65 75 77 78 79 82 84 85 86
a 3 6 7 8 10 11 24 25 26 28 29 30 36 38 41 44 48 50 53 54 55 56 57 59 61 62 64 65 75 77 78 79 82 85 86
a 3 6 7 8 10 11 24 25 26 28 29 30 36 38 41 44 48 50 53 54 55 56 57 59 60 61 62 64 65 75 77 78 79 82 86