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/huck_01.smv > huck_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: 74
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 301
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: 35
c Sum: 154
c MaxSize: 0
c Time: 16
c Aborted: false
c ML = 73
c SIZE = 74
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,9][3,9][4,4][5,3][6,3][7,2][8,2][9,1][10,1][11,1]}
c NODE covering index distribution:{[1,47][2,13][3,5][4,1][5,1][6,4][7,1][10,1][16,1]}
c EDGE covering index distrubution:{[1,253][2,34][3,11][4,1][5,1][6,1]}
c Total edges:301
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] = v7 & state.token[2] = v10) & state.token[3] = v14) & state.token[4] = v15) & state.token[5] = v16) & state.token[6] = v21) & state.token[7] = v26) & state.token[8] = v27) & state.token[9] = v28) & state.token[10] = v30) & state.token[11] = v32) & state.token[12] = v33) & state.token[13] = v36) & state.token[14] = v37) & state.token[15] = v42) & state.token[16] = v45) & state.token[17] = v46) & state.token[18] = v47) & state.token[19] = v48) & state.token[20] = v50) & state.token[21] = v53) & state.token[22] = v54) & state.token[23] = v61) & state.token[24] = v63) & state.token[25] = v66) & state.token[26] = v69) & state.token[27] = v74) ->  G !((((((((((((((((((((((((((((((((((((((((((((((((((((state.token[1] = v7 | state.token[1] = v10) | state.token[1] = v14) | state.token[1] = v15) | state.token[1] = v16) | state.token[1] = v21) | state.token[1] = v26) | state.token[1] = v27) | state.token[1] = v28) | state.token[1] = v30) | state.token[1] = v32) | state.token[1] = v33) | state.token[1] = v36) | state.token[1] = v37) | state.token[1] = v42) | state.token[1] = v45) | state.token[1] = v46) | state.token[1] = v47) | state.token[1] = v48) | state.token[1] = v50) | state.token[1] = v53) | state.token[1] = v54) | state.token[1] = v61) | state.token[1] = v63) | state.token[1] = v66) | state.token[1] = v69) | state.token[1] = v74) & ((((((((((((((((((((((((((state.token[2] = v7 | state.token[2] = v10) | state.token[2] = v14) | state.token[2] = v15) | state.token[2] = v16) | state.token[2] = v21) | state.token[2] = v26) | state.token[2] = v27) | state.token[2] = v28) | state.token[2] = v30) | state.token[2] = v32) | state.token[2] = v33) | state.token[2] = v36) | state.token[2] = v37) | state.token[2] = v42) | state.token[2] = v45) | state.token[2] = v46) | state.token[2] = v47) | state.token[2] = v48) | state.token[2] = v50) | state.token[2] = v53) | state.token[2] = v54) | state.token[2] = v61) | state.token[2] = v63) | state.token[2] = v66) | state.token[2] = v69) | state.token[2] = v74)) & ((((((((((((((((((((((((((state.token[3] = v7 | state.token[3] = v10) | state.token[3] = v14) | state.token[3] = v15) | state.token[3] = v16) | state.token[3] = v21) | state.token[3] = v26) | state.token[3] = v27) | state.token[3] = v28) | state.token[3] = v30) | state.token[3] = v32) | state.token[3] = v33) | state.token[3] = v36) | state.token[3] = v37) | state.token[3] = v42) | state.token[3] = v45) | state.token[3] = v46) | state.token[3] = v47) | state.token[3] = v48) | state.token[3] = v50) | state.token[3] = v53) | state.token[3] = v54) | state.token[3] = v61) | state.token[3] = v63) | state.token[3] = v66) | state.token[3] = v69) | state.token[3] = v74)) & ((((((((((((((((((((((((((state.token[4] = v7 | state.token[4] = v10) | state.token[4] = v14) | state.token[4] = v15) | state.token[4] = v16) | state.token[4] = v21) | state.token[4] = v26) | state.token[4] = v27) | state.token[4] = v28) | state.token[4] = v30) | state.token[4] = v32) | state.token[4] = v33) | state.token[4] = v36) | state.token[4] = v37) | state.token[4] = v42) | state.token[4] = v45) | state.token[4] = v46) | state.token[4] = v47) | state.token[4] = v48) | state.token[4] = v50) | state.token[4] = v53) | state.token[4] = v54) | state.token[4] = v61) | state.token[4] = v63) | state.token[4] = v66) | state.token[4] = v69) | state.token[4] = v74)) & ((((((((((((((((((((((((((state.token[5] = v7 | state.token[5] = v10) | state.token[5] = v14) | state.token[5] = v15) | state.token[5] = v16) | state.token[5] = v21) | state.token[5] = v26) | state.token[5] = v27) | state.token[5] = v28) | state.token[5] = v30) | state.token[5] = v32) | state.token[5] = v33) | state.token[5] = v36) | state.token[5] = v37) | state.token[5] = v42) | state.token[5] = v45) | state.token[5] = v46) | state.token[5] = v47) | state.token[5] = v48) | state.token[5] = v50) | state.token[5] = v53) | state.token[5] = v54) | state.token[5] = v61) | state.token[5] = v63) | state.token[5] = v66) | state.token[5] = v69) | state.token[5] = v74)) & ((((((((((((((((((((((((((state.token[6] = v7 | state.token[6] = v10) | state.token[6] = v14) | state.token[6] = v15) | state.token[6] = v16) | state.token[6] = v21) | state.token[6] = v26) | state.token[6] = v27) | state.token[6] = v28) | state.token[6] = v30) | state.token[6] = v32) | state.token[6] = v33) | state.token[6] = v36) | state.token[6] = v37) | state.token[6] = v42) | state.token[6] = v45) | state.token[6] = v46) | state.token[6] = v47) | state.token[6] = v48) | state.token[6] = v50) | state.token[6] = v53) | state.token[6] = v54) | state.token[6] = v61) | state.token[6] = v63) | state.token[6] = v66) | state.token[6] = v69) | state.token[6] = v74)) & ((((((((((((((((((((((((((state.token[7] = v7 | state.token[7] = v10) | state.token[7] = v14) | state.token[7] = v15) | state.token[7] = v16) | state.token[7] = v21) | state.token[7] = v26) | state.token[7] = v27) | state.token[7] = v28) | state.token[7] = v30) | state.token[7] = v32) | state.token[7] = v33) | state.token[7] = v36) | state.token[7] = v37) | state.token[7] = v42) | state.token[7] = v45) | state.token[7] = v46) | state.token[7] = v47) | state.token[7] = v48) | state.token[7] = v50) | state.token[7] = v53) | state.token[7] = v54) | state.token[7] = v61) | state.token[7] = v63) | state.token[7] = v66) | state.token[7] = v69) | state.token[7] = v74)) & ((((((((((((((((((((((((((state.token[8] = v7 | state.token[8] = v10) | state.token[8] = v14) | state.token[8] = v15) | state.token[8] = v16) | state.token[8] = v21) | state.token[8] = v26) | state.token[8] = v27) | state.token[8] = v28) | state.token[8] = v30) | state.token[8] = v32) | state.token[8] = v33) | state.token[8] = v36) | state.token[8] = v37) | state.token[8] = v42) | state.token[8] = v45) | state.token[8] = v46) | state.token[8] = v47) | state.token[8] = v48) | state.token[8] = v50) | state.token[8] = v53) | state.token[8] = v54) | state.token[8] = v61) | state.token[8] = v63) | state.token[8] = v66) | state.token[8] = v69) | state.token[8] = v74)) & ((((((((((((((((((((((((((state.token[9] = v7 | state.token[9] = v10) | state.token[9] = v14) | state.token[9] = v15) | state.token[9] = v16) | state.token[9] = v21) | state.token[9] = v26) | state.token[9] = v27) | state.token[9] = v28) | state.token[9] = v30) | state.token[9] = v32) | state.token[9] = v33) | state.token[9] = v36) | state.token[9] = v37) | state.token[9] = v42) | state.token[9] = v45) | state.token[9] = v46) | state.token[9] = v47) | state.token[9] = v48) | state.token[9] = v50) | state.token[9] = v53) | state.token[9] = v54) | state.token[9] = v61) | state.token[9] = v63) | state.token[9] = v66) | state.token[9] = v69) | state.token[9] = v74)) & ((((((((((((((((((((((((((state.token[10] = v7 | state.token[10] = v10) | state.token[10] = v14) | state.token[10] = v15) | state.token[10] = v16) | state.token[10] = v21) | state.token[10] = v26) | state.token[10] = v27) | state.token[10] = v28) | state.token[10] = v30) | state.token[10] = v32) | state.token[10] = v33) | state.token[10] = v36) | state.token[10] = v37) | state.token[10] = v42) | state.token[10] = v45) | state.token[10] = v46) | state.token[10] = v47) | state.token[10] = v48) | state.token[10] = v50) | state.token[10] = v53) | state.token[10] = v54) | state.token[10] = v61) | state.token[10] = v63) | state.token[10] = v66) | state.token[10] = v69) | state.token[10] = v74)) & ((((((((((((((((((((((((((state.token[11] = v7 | state.token[11] = v10) | state.token[11] = v14) | state.token[11] = v15) | state.token[11] = v16) | state.token[11] = v21) | state.token[11] = v26) | state.token[11] = v27) | state.token[11] = v28) | state.token[11] = v30) | state.token[11] = v32) | state.token[11] = v33) | state.token[11] = v36) | state.token[11] = v37) | state.token[11] = v42) | state.token[11] = v45) | state.token[11] = v46) | state.token[11] = v47) | state.token[11] = v48) | state.token[11] = v50) | state.token[11] = v53) | state.token[11] = v54) | state.token[11] = v61) | state.token[11] = v63) | state.token[11] = v66) | state.token[11] = v69) | state.token[11] = v74)) & ((((((((((((((((((((((((((state.token[12] = v7 | state.token[12] = v10) | state.token[12] = v14) | state.token[12] = v15) | state.token[12] = v16) | state.token[12] = v21) | state.token[12] = v26) | state.token[12] = v27) | state.token[12] = v28) | state.token[12] = v30) | state.token[12] = v32) | state.token[12] = v33) | state.token[12] = v36) | state.token[12] = v37) | state.token[12] = v42) | state.token[12] = v45) | state.token[12] = v46) | state.token[12] = v47) | state.token[12] = v48) | state.token[12] = v50) | state.token[12] = v53) | state.token[12] = v54) | state.token[12] = v61) | state.token[12] = v63) | state.token[12] = v66) | state.token[12] = v69) | state.token[12] = v74)) & ((((((((((((((((((((((((((state.token[13] = v7 | state.token[13] = v10) | state.token[13] = v14) | state.token[13] = v15) | state.token[13] = v16) | state.token[13] = v21) | state.token[13] = v26) | state.token[13] = v27) | state.token[13] = v28) | state.token[13] = v30) | state.token[13] = v32) | state.token[13] = v33) | state.token[13] = v36) | state.token[13] = v37) | state.token[13] = v42) | state.token[13] = v45) | state.token[13] = v46) | state.token[13] = v47) | state.token[13] = v48) | state.token[13] = v50) | state.token[13] = v53) | state.token[13] = v54) | state.token[13] = v61) | state.token[13] = v63) | state.token[13] = v66) | state.token[13] = v69) | state.token[13] = v74)) & ((((((((((((((((((((((((((state.token[14] = v7 | state.token[14] = v10) | state.token[14] = v14) | state.token[14] = v15) | state.token[14] = v16) | state.token[14] = v21) | state.token[14] = v26) | state.token[14] = v27) | state.token[14] = v28) | state.token[14] = v30) | state.token[14] = v32) | state.token[14] = v33) | state.token[14] = v36) | state.token[14] = v37) | state.token[14] = v42) | state.token[14] = v45) | state.token[14] = v46) | state.token[14] = v47) | state.token[14] = v48) | state.token[14] = v50) | state.token[14] = v53) | state.token[14] = v54) | state.token[14] = v61) | state.token[14] = v63) | state.token[14] = v66) | state.token[14] = v69) | state.token[14] = v74)) & ((((((((((((((((((((((((((state.token[15] = v7 | state.token[15] = v10) | state.token[15] = v14) | state.token[15] = v15) | state.token[15] = v16) | state.token[15] = v21) | state.token[15] = v26) | state.token[15] = v27) | state.token[15] = v28) | state.token[15] = v30) | state.token[15] = v32) | state.token[15] = v33) | state.token[15] = v36) | state.token[15] = v37) | state.token[15] = v42) | state.token[15] = v45) | state.token[15] = v46) | state.token[15] = v47) | state.token[15] = v48) | state.token[15] = v50) | state.token[15] = v53) | state.token[15] = v54) | state.token[15] = v61) | state.token[15] = v63) | state.token[15] = v66) | state.token[15] = v69) | state.token[15] = v74)) & ((((((((((((((((((((((((((state.token[16] = v7 | state.token[16] = v10) | state.token[16] = v14) | state.token[16] = v15) | state.token[16] = v16) | state.token[16] = v21) | state.token[16] = v26) | state.token[16] = v27) | state.token[16] = v28) | state.token[16] = v30) | state.token[16] = v32) | state.token[16] = v33) | state.token[16] = v36) | state.token[16] = v37) | state.token[16] = v42) | state.token[16] = v45) | state.token[16] = v46) | state.token[16] = v47) | state.token[16] = v48) | state.token[16] = v50) | state.token[16] = v53) | state.token[16] = v54) | state.token[16] = v61) | state.token[16] = v63) | state.token[16] = v66) | state.token[16] = v69) | state.token[16] = v74)) & ((((((((((((((((((((((((((state.token[17] = v7 | state.token[17] = v10) | state.token[17] = v14) | state.token[17] = v15) | state.token[17] = v16) | state.token[17] = v21) | state.token[17] = v26) | state.token[17] = v27) | state.token[17] = v28) | state.token[17] = v30) | state.token[17] = v32) | state.token[17] = v33) | state.token[17] = v36) | state.token[17] = v37) | state.token[17] = v42) | state.token[17] = v45) | state.token[17] = v46) | state.token[17] = v47) | state.token[17] = v48) | state.token[17] = v50) | state.token[17] = v53) | state.token[17] = v54) | state.token[17] = v61) | state.token[17] = v63) | state.token[17] = v66) | state.token[17] = v69) | state.token[17] = v74)) & ((((((((((((((((((((((((((state.token[18] = v7 | state.token[18] = v10) | state.token[18] = v14) | state.token[18] = v15) | state.token[18] = v16) | state.token[18] = v21) | state.token[18] = v26) | state.token[18] = v27) | state.token[18] = v28) | state.token[18] = v30) | state.token[18] = v32) | state.token[18] = v33) | state.token[18] = v36) | state.token[18] = v37) | state.token[18] = v42) | state.token[18] = v45) | state.token[18] = v46) | state.token[18] = v47) | state.token[18] = v48) | state.token[18] = v50) | state.token[18] = v53) | state.token[18] = v54) | state.token[18] = v61) | state.token[18] = v63) | state.token[18] = v66) | state.token[18] = v69) | state.token[18] = v74)) & ((((((((((((((((((((((((((state.token[19] = v7 | state.token[19] = v10) | state.token[19] = v14) | state.token[19] = v15) | state.token[19] = v16) | state.token[19] = v21) | state.token[19] = v26) | state.token[19] = v27) | state.token[19] = v28) | state.token[19] = v30) | state.token[19] = v32) | state.token[19] = v33) | state.token[19] = v36) | state.token[19] = v37) | state.token[19] = v42) | state.token[19] = v45) | state.token[19] = v46) | state.token[19] = v47) | state.token[19] = v48) | state.token[19] = v50) | state.token[19] = v53) | state.token[19] = v54) | state.token[19] = v61) | state.token[19] = v63) | state.token[19] = v66) | state.token[19] = v69) | state.token[19] = v74)) & ((((((((((((((((((((((((((state.token[20] = v7 | state.token[20] = v10) | state.token[20] = v14) | state.token[20] = v15) | state.token[20] = v16) | state.token[20] = v21) | state.token[20] = v26) | state.token[20] = v27) | state.token[20] = v28) | state.token[20] = v30) | state.token[20] = v32) | state.token[20] = v33) | state.token[20] = v36) | state.token[20] = v37) | state.token[20] = v42) | state.token[20] = v45) | state.token[20] = v46) | state.token[20] = v47) | state.token[20] = v48) | state.token[20] = v50) | state.token[20] = v53) | state.token[20] = v54) | state.token[20] = v61) | state.token[20] = v63) | state.token[20] = v66) | state.token[20] = v69) | state.token[20] = v74)) & ((((((((((((((((((((((((((state.token[21] = v7 | state.token[21] = v10) | state.token[21] = v14) | state.token[21] = v15) | state.token[21] = v16) | state.token[21] = v21) | state.token[21] = v26) | state.token[21] = v27) | state.token[21] = v28) | state.token[21] = v30) | state.token[21] = v32) | state.token[21] = v33) | state.token[21] = v36) | state.token[21] = v37) | state.token[21] = v42) | state.token[21] = v45) | state.token[21] = v46) | state.token[21] = v47) | state.token[21] = v48) | state.token[21] = v50) | state.token[21] = v53) | state.token[21] = v54) | state.token[21] = v61) | state.token[21] = v63) | state.token[21] = v66) | state.token[21] = v69) | state.token[21] = v74)) & ((((((((((((((((((((((((((state.token[22] = v7 | state.token[22] = v10) | state.token[22] = v14) | state.token[22] = v15) | state.token[22] = v16) | state.token[22] = v21) | state.token[22] = v26) | state.token[22] = v27) | state.token[22] = v28) | state.token[22] = v30) | state.token[22] = v32) | state.token[22] = v33) | state.token[22] = v36) | state.token[22] = v37) | state.token[22] = v42) | state.token[22] = v45) | state.token[22] = v46) | state.token[22] = v47) | state.token[22] = v48) | state.token[22] = v50) | state.token[22] = v53) | state.token[22] = v54) | state.token[22] = v61) | state.token[22] = v63) | state.token[22] = v66) | state.token[22] = v69) | state.token[22] = v74)) & ((((((((((((((((((((((((((state.token[23] = v7 | state.token[23] = v10) | state.token[23] = v14) | state.token[23] = v15) | state.token[23] = v16) | state.token[23] = v21) | state.token[23] = v26) | state.token[23] = v27) | state.token[23] = v28) | state.token[23] = v30) | state.token[23] = v32) | state.token[23] = v33) | state.token[23] = v36) | state.token[23] = v37) | state.token[23] = v42) | state.token[23] = v45) | state.token[23] = v46) | state.token[23] = v47) | state.token[23] = v48) | state.token[23] = v50) | state.token[23] = v53) | state.token[23] = v54) | state.token[23] = v61) | state.token[23] = v63) | state.token[23] = v66) | state.token[23] = v69) | state.token[23] = v74)) & ((((((((((((((((((((((((((state.token[24] = v7 | state.token[24] = v10) | state.token[24] = v14) | state.token[24] = v15) | state.token[24] = v16) | state.token[24] = v21) | state.token[24] = v26) | state.token[24] = v27) | state.token[24] = v28) | state.token[24] = v30) | state.token[24] = v32) | state.token[24] = v33) | state.token[24] = v36) | state.token[24] = v37) | state.token[24] = v42) | state.token[24] = v45) | state.token[24] = v46) | state.token[24] = v47) | state.token[24] = v48) | state.token[24] = v50) | state.token[24] = v53) | state.token[24] = v54) | state.token[24] = v61) | state.token[24] = v63) | state.token[24] = v66) | state.token[24] = v69) | state.token[24] = v74)) & ((((((((((((((((((((((((((state.token[25] = v7 | state.token[25] = v10) | state.token[25] = v14) | state.token[25] = v15) | state.token[25] = v16) | state.token[25] = v21) | state.token[25] = v26) | state.token[25] = v27) | state.token[25] = v28) | state.token[25] = v30) | state.token[25] = v32) | state.token[25] = v33) | state.token[25] = v36) | state.token[25] = v37) | state.token[25] = v42) | state.token[25] = v45) | state.token[25] = v46) | state.token[25] = v47) | state.token[25] = v48) | state.token[25] = v50) | state.token[25] = v53) | state.token[25] = v54) | state.token[25] = v61) | state.token[25] = v63) | state.token[25] = v66) | state.token[25] = v69) | state.token[25] = v74)) & ((((((((((((((((((((((((((state.token[26] = v7 | state.token[26] = v10) | state.token[26] = v14) | state.token[26] = v15) | state.token[26] = v16) | state.token[26] = v21) | state.token[26] = v26) | state.token[26] = v27) | state.token[26] = v28) | state.token[26] = v30) | state.token[26] = v32) | state.token[26] = v33) | state.token[26] = v36) | state.token[26] = v37) | state.token[26] = v42) | state.token[26] = v45) | state.token[26] = v46) | state.token[26] = v47) | state.token[26] = v48) | state.token[26] = v50) | state.token[26] = v53) | state.token[26] = v54) | state.token[26] = v61) | state.token[26] = v63) | state.token[26] = v66) | state.token[26] = v69) | state.token[26] = v74)) & ((((((((((((((((((((((((((state.token[27] = v7 | state.token[27] = v10) | state.token[27] = v14) | state.token[27] = v15) | state.token[27] = v16) | state.token[27] = v21) | state.token[27] = v26) | state.token[27] = v27) | state.token[27] = v28) | state.token[27] = v30) | state.token[27] = v32) | state.token[27] = v33) | state.token[27] = v36) | state.token[27] = v37) | state.token[27] = v42) | state.token[27] = v45) | state.token[27] = v46) | state.token[27] = v47) | state.token[27] = v48) | state.token[27] = v50) | state.token[27] = v53) | state.token[27] = v54) | state.token[27] = v61) | state.token[27] = v63) | state.token[27] = v66) | state.token[27] = v69) | state.token[27] = v74)))    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] = 0ud35_256
c     state.token[2] = 0ud35_134217728
c     state.token[3] = 0ud35_4194304
c     state.token[4] = 0ud35_4096
c     state.token[5] = 0ud35_512
c     state.token[6] = 0ud35_1073741824
c     state.token[7] = 0ud35_4294967296
c     state.token[8] = 0ud35_536936448
c     state.token[9] = 0ud35_1
c     state.token[10] = 0ud35_67108864
c     state.token[11] = 0ud35_32768
c     state.token[12] = 0ud35_4
c     state.token[13] = 0ud35_128
c     state.token[14] = 0ud35_16
c     state.token[15] = 0ud35_524320
c     state.token[16] = 0ud35_2097152
c     state.token[17] = 0ud35_8388608
c     state.token[18] = 0ud35_33556480
c     state.token[19] = 0ud35_16777216
c     state.token[20] = 0ud35_17179869184
c     state.token[21] = 0ud35_2147483648
c     state.token[22] = 0ud35_131072
c     state.token[23] = 0ud35_8
c     state.token[24] = 0ud35_1024
c     state.token[25] = 0ud35_1048576
c     state.token[26] = 0ud35_268435456
c     state.token[27] = 0ud35_64
c     state.tid = 1
c     state.vid = 2
c     state.target = 0ud35_0
c     v74 = 0ud35_64
c     v73 = 0ud35_570425344
c     v72 = 0ud35_134217744
c     v71 = 0ud35_2129920
c     v70 = 0ud35_256
c     v69 = 0ud35_268435456
c     v68 = 0ud35_536870912
c     v67 = 0ud35_33556480
c     v66 = 0ud35_1048576
c     v65 = 0ud35_512
c     v64 = 0ud35_1073741824
c     v63 = 0ud35_1024
c     v62 = 0ud35_8456192
c     v61 = 0ud35_8
c     v60 = 0ud35_536871040
c     v59 = 0ud35_17179869184
c     v58 = 0ud35_16777216
c     v57 = 0ud35_579076288
c     v56 = 0ud35_536870912
c     v55 = 0ud35_30007761536
c     v54 = 0ud35_131072
c     v53 = 0ud35_2147483648
c     v52 = 0ud35_10741612544
c     v51 = 0ud35_64
c     v50 = 0ud35_17179869184
c     v49 = 0ud35_17582530580
c     v48 = 0ud35_16777216
c     v47 = 0ud35_33556480
c     v46 = 0ud35_8388608
c     v45 = 0ud35_2097152
c     v44 = 0ud35_8594137088
c     v43 = 0ud35_33554496
c     v42 = 0ud35_524320
c     v41 = 0ud35_579076288
c     v40 = 0ud35_17179869184
c     v39 = 0ud35_1073741824
c     v38 = 0ud35_4194304
c     v37 = 0ud35_16
c     v36 = 0ud35_128
c     v35 = 0ud35_16777216
c     v34 = 0ud35_1073741824
c     v33 = 0ud35_4
c     v32 = 0ud35_32768
c     v31 = 0ud35_8594145280
c     v30 = 0ud35_67108864
c     v29 = 0ud35_17179869184
c     v28 = 0ud35_1
c     v27 = 0ud35_536936448
c     v26 = 0ud35_4294967296
c     v25 = 0ud35_17179869184
c     v24 = 0ud35_540672
c     v23 = 0ud35_1140850688
c     v22 = 0ud35_4564726826
c     v21 = 0ud35_1073741824
c     v20 = 0ud35_1073741824
c     v19 = 0ud35_536870912
c     v18 = 0ud35_8594145282
c     v17 = 0ud35_1140850689
c     v16 = 0ud35_512
c     v15 = 0ud35_4096
c     v14 = 0ud35_4194304
c     v13 = 0ud35_17179869184
c     v12 = 0ud35_33556480
c     v11 = 0ud35_17179869184
c     v10 = 0ud35_134217728
c     v9 = 0ud35_11145314304
c     v8 = 0ud35_4194304
c     v7 = 0ud35_256
c     v6 = 0ud35_1073741824
c     v5 = 0ud35_17179869184
c     v4 = 0ud35_849380352
c     v3 = 0ud35_2147483648
c     v2 = 0ud35_8388672
c     v1 = 0ud35_17582531584
c     v0 = 0ud35_0
s 10 15 26 28 30 32 33 36 37 42 44 45 46 48 53 54 59 61 63 64 65 66 67 68 69 70 74
t 7 10 14 15 16 21 26 27 28 30 32 33 36 37 42 45 46 47 48 50 53 54 61 63 66 69 74
a YES
a 10 15 26 28 30 32 33 36 37 42 44 45 46 48 53 54 59 61 63 64 65 66 67 68 69 70 74
a 10 14 15 26 28 30 32 33 36 37 42 45 46 48 53 54 59 61 63 64 65 66 67 68 69 70 74
a 10 14 15 26 28 30 32 33 36 37 42 45 46 48 50 53 54 61 63 64 65 66 67 68 69 70 74
a 10 14 15 21 26 28 30 32 33 36 37 42 45 46 48 50 53 54 61 63 65 66 67 68 69 70 74
a 10 14 15 16 21 26 28 30 32 33 36 37 42 45 46 48 50 53 54 61 63 66 67 68 69 70 74
a 10 14 15 16 21 26 28 30 32 33 36 37 42 45 46 47 48 50 53 54 61 63 66 68 69 70 74
a 10 14 15 16 21 26 27 28 30 32 33 36 37 42 45 46 47 48 50 53 54 61 63 66 69 70 74
a 7 10 14 15 16 21 26 27 28 30 32 33 36 37 42 45 46 47 48 50 53 54 61 63 66 69 74