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/qg.order30_01.smv > qg.order30_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: 900
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 26100
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: 1800
c MaxSize: 0
c Time: 215
c Aborted: false
c ML = 899
c SIZE = 900
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[30,60]}
c NODE covering index distribution:{[2,900]}
c EDGE covering index distrubution:{[1,26100]}
c Total edges:26100
c Distributions saved!
c *** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015)
c *** Enabled addons are: compass
c *** For more information on NuSMV see <http://nusmv.fbk.eu>
c *** or email to <nusmv-users@list.fbk.eu>.
c *** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
c 
c *** Copyright (c) 2010-2014, Fondazione Bruno Kessler
c 
c *** This version of NuSMV is linked to the CUDD library version 2.4.1
c *** Copyright (c) 1995-2004, Regents of the University of Colorado
c 
c *** This version of NuSMV is linked to the MiniSat SAT solver. 
c *** See http://minisat.se/MiniSat.html
c *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
c *** Copyright (c) 2007-2010, Niklas Sorensson
c 
c -- no counterexample found with bound 0
c -- no counterexample found with bound 1
c -- no counterexample found with bound 2
c -- no counterexample found with bound 3
c -- no counterexample found with bound 4
c -- no counterexample found with bound 5
c -- no counterexample found with bound 6
c -- no counterexample found with bound 7
c -- no counterexample found with bound 8
c -- no counterexample found with bound 9
c -- specification  G (((((((((((((((((((((((((((((state.token[1] = v4 & state.token[2] = v49) & state.token[3] = v85) & state.token[4] = v103) & state.token[5] = v150) & state.token[6] = v168) & state.token[7] = v215) & state.token[8] = v250) & state.token[9] = v276) & state.token[10] = v329) & state.token[11] = v358) & state.token[12] = v382) & state.token[13] = v393) & state.token[14] = v447) & state.token[15] = v458) & state.token[16] = v501) & state.token[17] = v534) & state.token[18] = v557) & state.token[19] = v584) & state.token[20] = v620) & state.token[21] = v631) & state.token[22] = v675) & state.token[23] = v697) & state.token[24] = v746) & state.token[25] = v752) & state.token[26] = v791) & state.token[27] = v826) & state.token[28] = v863) & state.token[29] = v879) ->  G !((((((((((((((((((((((((((((((((((((((((((((((((((((((((state.token[1] = v4 | state.token[1] = v49) | state.token[1] = v85) | state.token[1] = v103) | state.token[1] = v142) | state.token[1] = v174) | state.token[1] = v215) | state.token[1] = v250) | state.token[1] = v276) | state.token[1] = v323) | state.token[1] = v344) | state.token[1] = v378) | state.token[1] = v393) | state.token[1] = v447) | state.token[1] = v458) | state.token[1] = v501) | state.token[1] = v538) | state.token[1] = v557) | state.token[1] = v600) | state.token[1] = v620) | state.token[1] = v631) | state.token[1] = v675) | state.token[1] = v697) | state.token[1] = v746) | state.token[1] = v752) | state.token[1] = v791) | state.token[1] = v826) | state.token[1] = v869) | state.token[1] = v879) & ((((((((((((((((((((((((((((state.token[2] = v4 | state.token[2] = v49) | state.token[2] = v85) | state.token[2] = v103) | state.token[2] = v142) | state.token[2] = v174) | state.token[2] = v215) | state.token[2] = v250) | state.token[2] = v276) | state.token[2] = v323) | state.token[2] = v344) | state.token[2] = v378) | state.token[2] = v393) | state.token[2] = v447) | state.token[2] = v458) | state.token[2] = v501) | state.token[2] = v538) | state.token[2] = v557) | state.token[2] = v600) | state.token[2] = v620) | state.token[2] = v631) | state.token[2] = v675) | state.token[2] = v697) | state.token[2] = v746) | state.token[2] = v752) | state.token[2] = v791) | state.token[2] = v826) | state.token[2] = v869) | state.token[2] = v879)) & ((((((((((((((((((((((((((((state.token[3] = v4 | state.token[3] = v49) | state.token[3] = v85) | state.token[3] = v103) | state.token[3] = v142) | state.token[3] = v174) | state.token[3] = v215) | state.token[3] = v250) | state.token[3] = v276) | state.token[3] = v323) | state.token[3] = v344) | state.token[3] = v378) | state.token[3] = v393) | state.token[3] = v447) | state.token[3] = v458) | state.token[3] = v501) | state.token[3] = v538) | state.token[3] = v557) | state.token[3] = v600) | state.token[3] = v620) | state.token[3] = v631) | state.token[3] = v675) | state.token[3] = v697) | state.token[3] = v746) | state.token[3] = v752) | state.token[3] = v791) | state.token[3] = v826) | state.token[3] = v869) | state.token[3] = v879)) & ((((((((((((((((((((((((((((state.token[4] = v4 | state.token[4] = v49) | state.token[4] = v85) | state.token[4] = v103) | state.token[4] = v142) | state.token[4] = v174) | state.token[4] = v215) | state.token[4] = v250) | state.token[4] = v276) | state.token[4] = v323) | state.token[4] = v344) | state.token[4] = v378) | state.token[4] = v393) | state.token[4] = v447) | state.token[4] = v458) | state.token[4] = v501) | state.token[4] = v538) | state.token[4] = v557) | state.token[4] = v600) | state.token[4] = v620) | state.token[4] = v631) | state.token[4] = v675) | state.token[4] = v697) | state.token[4] = v746) | state.token[4] = v752) | state.token[4] = v791) | state.token[4] = v826) | state.token[4] = v869) | state.token[4] = v879)) & ((((((((((((((((((((((((((((state.token[5] = v4 | state.token[5] = v49) | state.token[5] = v85) | state.token[5] = v103) | state.token[5] = v142) | state.token[5] = v174) | state.token[5] = v215) | state.token[5] = v250) | state.token[5] = v276) | state.token[5] = v323) | state.token[5] = v344) | state.token[5] = v378) | state.token[5] = v393) | state.token[5] = v447) | state.token[5] = v458) | state.token[5] = v501) | state.token[5] = v538) | state.token[5] = v557) | state.token[5] = v600) | state.token[5] = v620) | state.token[5] = v631) | state.token[5] = v675) | state.token[5] = v697) | state.token[5] = v746) | state.token[5] = v752) | state.token[5] = v791) | state.token[5] = v826) | state.token[5] = v869) | state.token[5] = v879)) & ((((((((((((((((((((((((((((state.token[6] = v4 | state.token[6] = v49) | state.token[6] = v85) | state.token[6] = v103) | state.token[6] = v142) | state.token[6] = v174) | state.token[6] = v215) | state.token[6] = v250) | state.token[6] = v276) | state.token[6] = v323) | state.token[6] = v344) | state.token[6] = v378) | state.token[6] = v393) | state.token[6] = v447) | state.token[6] = v458) | state.token[6] = v501) | state.token[6] = v538) | state.token[6] = v557) | state.token[6] = v600) | state.token[6] = v620) | state.token[6] = v631) | state.token[6] = v675) | state.token[6] = v697) | state.token[6] = v746) | state.token[6] = v752) | state.token[6] = v791) | state.token[6] = v826) | state.token[6] = v869) | state.token[6] = v879)) & ((((((((((((((((((((((((((((state.token[7] = v4 | state.token[7] = v49) | state.token[7] = v85) | state.token[7] = v103) | state.token[7] = v142) | state.token[7] = v174) | state.token[7] = v215) | state.token[7] = v250) | state.token[7] = v276) | state.token[7] = v323) | state.token[7] = v344) | state.token[7] = v378) | state.token[7] = v393) | state.token[7] = v447) | state.token[7] = v458) | state.token[7] = v501) | state.token[7] = v538) | state.token[7] = v557) | state.token[7] = v600) | state.token[7] = v620) | state.token[7] = v631) | state.token[7] = v675) | state.token[7] = v697) | state.token[7] = v746) | state.token[7] = v752) | state.token[7] = v791) | state.token[7] = v826) | state.token[7] = v869) | state.token[7] = v879)) & ((((((((((((((((((((((((((((state.token[8] = v4 | state.token[8] = v49) | state.token[8] = v85) | state.token[8] = v103) | state.token[8] = v142) | state.token[8] = v174) | state.token[8] = v215) | state.token[8] = v250) | state.token[8] = v276) | state.token[8] = v323) | state.token[8] = v344) | state.token[8] = v378) | state.token[8] = v393) | state.token[8] = v447) | state.token[8] = v458) | state.token[8] = v501) | state.token[8] = v538) | state.token[8] = v557) | state.token[8] = v600) | state.token[8] = v620) | state.token[8] = v631) | state.token[8] = v675) | state.token[8] = v697) | state.token[8] = v746) | state.token[8] = v752) | state.token[8] = v791) | state.token[8] = v826) | state.token[8] = v869) | state.token[8] = v879)) & ((((((((((((((((((((((((((((state.token[9] = v4 | state.token[9] = v49) | state.token[9] = v85) | state.token[9] = v103) | state.token[9] = v142) | state.token[9] = v174) | state.token[9] = v215) | state.token[9] = v250) | state.token[9] = v276) | state.token[9] = v323) | state.token[9] = v344) | state.token[9] = v378) | state.token[9] = v393) | state.token[9] = v447) | state.token[9] = v458) | state.token[9] = v501) | state.token[9] = v538) | state.token[9] = v557) | state.token[9] = v600) | state.token[9] = v620) | state.token[9] = v631) | state.token[9] = v675) | state.token[9] = v697) | state.token[9] = v746) | state.token[9] = v752) | state.token[9] = v791) | state.token[9] = v826) | state.token[9] = v869) | state.token[9] = v879)) & ((((((((((((((((((((((((((((state.token[10] = v4 | state.token[10] = v49) | state.token[10] = v85) | state.token[10] = v103) | state.token[10] = v142) | state.token[10] = v174) | state.token[10] = v215) | state.token[10] = v250) | state.token[10] = v276) | state.token[10] = v323) | state.token[10] = v344) | state.token[10] = v378) | state.token[10] = v393) | state.token[10] = v447) | state.token[10] = v458) | state.token[10] = v501) | state.token[10] = v538) | state.token[10] = v557) | state.token[10] = v600) | state.token[10] = v620) | state.token[10] = v631) | state.token[10] = v675) | state.token[10] = v697) | state.token[10] = v746) | state.token[10] = v752) | state.token[10] = v791) | state.token[10] = v826) | state.token[10] = v869) | state.token[10] = v879)) & ((((((((((((((((((((((((((((state.token[11] = v4 | state.token[11] = v49) | state.token[11] = v85) | state.token[11] = v103) | state.token[11] = v142) | state.token[11] = v174) | state.token[11] = v215) | state.token[11] = v250) | state.token[11] = v276) | state.token[11] = v323) | state.token[11] = v344) | state.token[11] = v378) | state.token[11] = v393) | state.token[11] = v447) | state.token[11] = v458) | state.token[11] = v501) | state.token[11] = v538) | state.token[11] = v557) | state.token[11] = v600) | state.token[11] = v620) | state.token[11] = v631) | state.token[11] = v675) | state.token[11] = v697) | state.token[11] = v746) | state.token[11] = v752) | state.token[11] = v791) | state.token[11] = v826) | state.token[11] = v869) | state.token[11] = v879)) & ((((((((((((((((((((((((((((state.token[12] = v4 | state.token[12] = v49) | state.token[12] = v85) | state.token[12] = v103) | state.token[12] = v142) | state.token[12] = v174) | state.token[12] = v215) | state.token[12] = v250) | state.token[12] = v276) | state.token[12] = v323) | state.token[12] = v344) | state.token[12] = v378) | state.token[12] = v393) | state.token[12] = v447) | state.token[12] = v458) | state.token[12] = v501) | state.token[12] = v538) | state.token[12] = v557) | state.token[12] = v600) | state.token[12] = v620) | state.token[12] = v631) | state.token[12] = v675) | state.token[12] = v697) | state.token[12] = v746) | state.token[12] = v752) | state.token[12] = v791) | state.token[12] = v826) | state.token[12] = v869) | state.token[12] = v879)) & ((((((((((((((((((((((((((((state.token[13] = v4 | state.token[13] = v49) | state.token[13] = v85) | state.token[13] = v103) | state.token[13] = v142) | state.token[13] = v174) | state.token[13] = v215) | state.token[13] = v250) | state.token[13] = v276) | state.token[13] = v323) | state.token[13] = v344) | state.token[13] = v378) | state.token[13] = v393) | state.token[13] = v447) | state.token[13] = v458) | state.token[13] = v501) | state.token[13] = v538) | state.token[13] = v557) | state.token[13] = v600) | state.token[13] = v620) | state.token[13] = v631) | state.token[13] = v675) | state.token[13] = v697) | state.token[13] = v746) | state.token[13] = v752) | state.token[13] = v791) | state.token[13] = v826) | state.token[13] = v869) | state.token[13] = v879)) & ((((((((((((((((((((((((((((state.token[14] = v4 | state.token[14] = v49) | state.token[14] = v85) | state.token[14] = v103) | state.token[14] = v142) | state.token[14] = v174) | state.token[14] = v215) | state.token[14] = v250) | state.token[14] = v276) | state.token[14] = v323) | state.token[14] = v344) | state.token[14] = v378) | state.token[14] = v393) | state.token[14] = v447) | state.token[14] = v458) | state.token[14] = v501) | state.token[14] = v538) | state.token[14] = v557) | state.token[14] = v600) | state.token[14] = v620) | state.token[14] = v631) | state.token[14] = v675) | state.token[14] = v697) | state.token[14] = v746) | state.token[14] = v752) | state.token[14] = v791) | state.token[14] = v826) | state.token[14] = v869) | state.token[14] = v879)) & ((((((((((((((((((((((((((((state.token[15] = v4 | state.token[15] = v49) | state.token[15] = v85) | state.token[15] = v103) | state.token[15] = v142) | state.token[15] = v174) | state.token[15] = v215) | state.token[15] = v250) | state.token[15] = v276) | state.token[15] = v323) | state.token[15] = v344) | state.token[15] = v378) | state.token[15] = v393) | state.token[15] = v447) | state.token[15] = v458) | state.token[15] = v501) | state.token[15] = v538) | state.token[15] = v557) | state.token[15] = v600) | state.token[15] = v620) | state.token[15] = v631) | state.token[15] = v675) | state.token[15] = v697) | state.token[15] = v746) | state.token[15] = v752) | state.token[15] = v791) | state.token[15] = v826) | state.token[15] = v869) | state.token[15] = v879)) & ((((((((((((((((((((((((((((state.token[16] = v4 | state.token[16] = v49) | state.token[16] = v85) | state.token[16] = v103) | state.token[16] = v142) | state.token[16] = v174) | state.token[16] = v215) | state.token[16] = v250) | state.token[16] = v276) | state.token[16] = v323) | state.token[16] = v344) | state.token[16] = v378) | state.token[16] = v393) | state.token[16] = v447) | state.token[16] = v458) | state.token[16] = v501) | state.token[16] = v538) | state.token[16] = v557) | state.token[16] = v600) | state.token[16] = v620) | state.token[16] = v631) | state.token[16] = v675) | state.token[16] = v697) | state.token[16] = v746) | state.token[16] = v752) | state.token[16] = v791) | state.token[16] = v826) | state.token[16] = v869) | state.token[16] = v879)) & ((((((((((((((((((((((((((((state.token[17] = v4 | state.token[17] = v49) | state.token[17] = v85) | state.token[17] = v103) | state.token[17] = v142) | state.token[17] = v174) | state.token[17] = v215) | state.token[17] = v250) | state.token[17] = v276) | state.token[17] = v323) | state.token[17] = v344) | state.token[17] = v378) | state.token[17] = v393) | state.token[17] = v447) | state.token[17] = v458) | state.token[17] = v501) | state.token[17] = v538) | state.token[17] = v557) | state.token[17] = v600) | state.token[17] = v620) | state.token[17] = v631) | state.token[17] = v675) | state.token[17] = v697) | state.token[17] = v746) | state.token[17] = v752) | state.token[17] = v791) | state.token[17] = v826) | state.token[17] = v869) | state.token[17] = v879)) & ((((((((((((((((((((((((((((state.token[18] = v4 | state.token[18] = v49) | state.token[18] = v85) | state.token[18] = v103) | state.token[18] = v142) | state.token[18] = v174) | state.token[18] = v215) | state.token[18] = v250) | state.token[18] = v276) | state.token[18] = v323) | state.token[18] = v344) | state.token[18] = v378) | state.token[18] = v393) | state.token[18] = v447) | state.token[18] = v458) | state.token[18] = v501) | state.token[18] = v538) | state.token[18] = v557) | state.token[18] = v600) | state.token[18] = v620) | state.token[18] = v631) | state.token[18] = v675) | state.token[18] = v697) | state.token[18] = v746) | state.token[18] = v752) | state.token[18] = v791) | state.token[18] = v826) | state.token[18] = v869) | state.token[18] = v879)) & ((((((((((((((((((((((((((((state.token[19] = v4 | state.token[19] = v49) | state.token[19] = v85) | state.token[19] = v103) | state.token[19] = v142) | state.token[19] = v174) | state.token[19] = v215) | state.token[19] = v250) | state.token[19] = v276) | state.token[19] = v323) | state.token[19] = v344) | state.token[19] = v378) | state.token[19] = v393) | state.token[19] = v447) | state.token[19] = v458) | state.token[19] = v501) | state.token[19] = v538) | state.token[19] = v557) | state.token[19] = v600) | state.token[19] = v620) | state.token[19] = v631) | state.token[19] = v675) | state.token[19] = v697) | state.token[19] = v746) | state.token[19] = v752) | state.token[19] = v791) | state.token[19] = v826) | state.token[19] = v869) | state.token[19] = v879)) & ((((((((((((((((((((((((((((state.token[20] = v4 | state.token[20] = v49) | state.token[20] = v85) | state.token[20] = v103) | state.token[20] = v142) | state.token[20] = v174) | state.token[20] = v215) | state.token[20] = v250) | state.token[20] = v276) | state.token[20] = v323) | state.token[20] = v344) | state.token[20] = v378) | state.token[20] = v393) | state.token[20] = v447) | state.token[20] = v458) | state.token[20] = v501) | state.token[20] = v538) | state.token[20] = v557) | state.token[20] = v600) | state.token[20] = v620) | state.token[20] = v631) | state.token[20] = v675) | state.token[20] = v697) | state.token[20] = v746) | state.token[20] = v752) | state.token[20] = v791) | state.token[20] = v826) | state.token[20] = v869) | state.token[20] = v879)) & ((((((((((((((((((((((((((((state.token[21] = v4 | state.token[21] = v49) | state.token[21] = v85) | state.token[21] = v103) | state.token[21] = v142) | state.token[21] = v174) | state.token[21] = v215) | state.token[21] = v250) | state.token[21] = v276) | state.token[21] = v323) | state.token[21] = v344) | state.token[21] = v378) | state.token[21] = v393) | state.token[21] = v447) | state.token[21] = v458) | state.token[21] = v501) | state.token[21] = v538) | state.token[21] = v557) | state.token[21] = v600) | state.token[21] = v620) | state.token[21] = v631) | state.token[21] = v675) | state.token[21] = v697) | state.token[21] = v746) | state.token[21] = v752) | state.token[21] = v791) | state.token[21] = v826) | state.token[21] = v869) | state.token[21] = v879)) & ((((((((((((((((((((((((((((state.token[22] = v4 | state.token[22] = v49) | state.token[22] = v85) | state.token[22] = v103) | state.token[22] = v142) | state.token[22] = v174) | state.token[22] = v215) | state.token[22] = v250) | state.token[22] = v276) | state.token[22] = v323) | state.token[22] = v344) | state.token[22] = v378) | state.token[22] = v393) | state.token[22] = v447) | state.token[22] = v458) | state.token[22] = v501) | state.token[22] = v538) | state.token[22] = v557) | state.token[22] = v600) | state.token[22] = v620) | state.token[22] = v631) | state.token[22] = v675) | state.token[22] = v697) | state.token[22] = v746) | state.token[22] = v752) | state.token[22] = v791) | state.token[22] = v826) | state.token[22] = v869) | state.token[22] = v879)) & ((((((((((((((((((((((((((((state.token[23] = v4 | state.token[23] = v49) | state.token[23] = v85) | state.token[23] = v103) | state.token[23] = v142) | state.token[23] = v174) | state.token[23] = v215) | state.token[23] = v250) | state.token[23] = v276) | state.token[23] = v323) | state.token[23] = v344) | state.token[23] = v378) | state.token[23] = v393) | state.token[23] = v447) | state.token[23] = v458) | state.token[23] = v501) | state.token[23] = v538) | state.token[23] = v557) | state.token[23] = v600) | state.token[23] = v620) | state.token[23] = v631) | state.token[23] = v675) | state.token[23] = v697) | state.token[23] = v746) | state.token[23] = v752) | state.token[23] = v791) | state.token[23] = v826) | state.token[23] = v869) | state.token[23] = v879)) & ((((((((((((((((((((((((((((state.token[24] = v4 | state.token[24] = v49) | state.token[24] = v85) | state.token[24] = v103) | state.token[24] = v142) | state.token[24] = v174) | state.token[24] = v215) | state.token[24] = v250) | state.token[24] = v276) | state.token[24] = v323) | state.token[24] = v344) | state.token[24] = v378) | state.token[24] = v393) | state.token[24] = v447) | state.token[24] = v458) | state.token[24] = v501) | state.token[24] = v538) | state.token[24] = v557) | state.token[24] = v600) | state.token[24] = v620) | state.token[24] = v631) | state.token[24] = v675) | state.token[24] = v697) | state.token[24] = v746) | state.token[24] = v752) | state.token[24] = v791) | state.token[24] = v826) | state.token[24] = v869) | state.token[24] = v879)) & ((((((((((((((((((((((((((((state.token[25] = v4 | state.token[25] = v49) | state.token[25] = v85) | state.token[25] = v103) | state.token[25] = v142) | state.token[25] = v174) | state.token[25] = v215) | state.token[25] = v250) | state.token[25] = v276) | state.token[25] = v323) | state.token[25] = v344) | state.token[25] = v378) | state.token[25] = v393) | state.token[25] = v447) | state.token[25] = v458) | state.token[25] = v501) | state.token[25] = v538) | state.token[25] = v557) | state.token[25] = v600) | state.token[25] = v620) | state.token[25] = v631) | state.token[25] = v675) | state.token[25] = v697) | state.token[25] = v746) | state.token[25] = v752) | state.token[25] = v791) | state.token[25] = v826) | state.token[25] = v869) | state.token[25] = v879)) & ((((((((((((((((((((((((((((state.token[26] = v4 | state.token[26] = v49) | state.token[26] = v85) | state.token[26] = v103) | state.token[26] = v142) | state.token[26] = v174) | state.token[26] = v215) | state.token[26] = v250) | state.token[26] = v276) | state.token[26] = v323) | state.token[26] = v344) | state.token[26] = v378) | state.token[26] = v393) | state.token[26] = v447) | state.token[26] = v458) | state.token[26] = v501) | state.token[26] = v538) | state.token[26] = v557) | state.token[26] = v600) | state.token[26] = v620) | state.token[26] = v631) | state.token[26] = v675) | state.token[26] = v697) | state.token[26] = v746) | state.token[26] = v752) | state.token[26] = v791) | state.token[26] = v826) | state.token[26] = v869) | state.token[26] = v879)) & ((((((((((((((((((((((((((((state.token[27] = v4 | state.token[27] = v49) | state.token[27] = v85) | state.token[27] = v103) | state.token[27] = v142) | state.token[27] = v174) | state.token[27] = v215) | state.token[27] = v250) | state.token[27] = v276) | state.token[27] = v323) | state.token[27] = v344) | state.token[27] = v378) | state.token[27] = v393) | state.token[27] = v447) | state.token[27] = v458) | state.token[27] = v501) | state.token[27] = v538) | state.token[27] = v557) | state.token[27] = v600) | state.token[27] = v620) | state.token[27] = v631) | state.token[27] = v675) | state.token[27] = v697) | state.token[27] = v746) | state.token[27] = v752) | state.token[27] = v791) | state.token[27] = v826) | state.token[27] = v869) | state.token[27] = v879)) & ((((((((((((((((((((((((((((state.token[28] = v4 | state.token[28] = v49) | state.token[28] = v85) | state.token[28] = v103) | state.token[28] = v142) | state.token[28] = v174) | state.token[28] = v215) | state.token[28] = v250) | state.token[28] = v276) | state.token[28] = v323) | state.token[28] = v344) | state.token[28] = v378) | state.token[28] = v393) | state.token[28] = v447) | state.token[28] = v458) | state.token[28] = v501) | state.token[28] = v538) | state.token[28] = v557) | state.token[28] = v600) | state.token[28] = v620) | state.token[28] = v631) | state.token[28] = v675) | state.token[28] = v697) | state.token[28] = v746) | state.token[28] = v752) | state.token[28] = v791) | state.token[28] = v826) | state.token[28] = v869) | state.token[28] = v879)) & ((((((((((((((((((((((((((((state.token[29] = v4 | state.token[29] = v49) | state.token[29] = v85) | state.token[29] = v103) | state.token[29] = v142) | state.token[29] = v174) | state.token[29] = v215) | state.token[29] = v250) | state.token[29] = v276) | state.token[29] = v323) | state.token[29] = v344) | state.token[29] = v378) | state.token[29] = v393) | state.token[29] = v447) | state.token[29] = v458) | state.token[29] = v501) | state.token[29] = v538) | state.token[29] = v557) | state.token[29] = v600) | state.token[29] = v620) | state.token[29] = v631) | state.token[29] = v675) | state.token[29] = v697) | state.token[29] = v746) | state.token[29] = v752) | state.token[29] = v791) | state.token[29] = v826) | state.token[29] = v869) | state.token[29] = v879)))    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_137455730688
c     state.token[2] = 0ud60_1082130432
c     state.token[3] = 0ud60_524292
c     state.token[4] = 0ud60_8589934593
c     state.token[5] = 0ud60_144115188077953024
c     state.token[6] = 0ud60_68719476768
c     state.token[7] = 0ud60_36028797023158272
c     state.token[8] = 0ud60_1116691496960
c     state.token[9] = 0ud60_72057594037928192
c     state.token[10] = 0ud60_35188667056128
c     state.token[11] = 0ud60_4398046513152
c     state.token[12] = 0ud60_17592320262144
c     state.token[13] = 0ud60_2199023256576
c     state.token[14] = 0ud60_1134695999864832
c     state.token[15] = 0ud60_4503599627632640
c     state.token[16] = 0ud60_268443648
c     state.token[17] = 0ud60_34359738370
c     state.token[18] = 0ud60_274877939712
c     state.token[19] = 0ud60_131136
c     state.token[20] = 0ud60_9007199254741008
c     state.token[21] = 0ud60_351843720888320
c     state.token[22] = 0ud60_549755814400
c     state.token[23] = 0ud60_140739635838976
c     state.token[24] = 0ud60_562949953421320
c     state.token[25] = 0ud60_2251799813750784
c     state.token[26] = 0ud60_18014398509482112
c     state.token[27] = 0ud60_67112960
c     state.token[28] = 0ud60_536887296
c     state.token[29] = 0ud60_576460752304472064
c     state.tid = 1
c     state.vid = 192
c     state.target = 0ud60_0
c     v900 = 0ud60_144115188076904448
c     v899 = 0ud60_35184373137408
c     v898 = 0ud60_1050624
c     v897 = 0ud60_1125899907891200
c     v896 = 0ud60_562949954469888
c     v895 = 0ud60_1048580
c     v894 = 0ud60_34360786944
c     v893 = 0ud60_1064960
c     v892 = 0ud60_135266304
c     v891 = 0ud60_269484032
c     v890 = 0ud60_9007199255789568
c     v889 = 0ud60_1074790400
c     v888 = 0ud60_1048608
c     v887 = 0ud60_274878955520
c     v886 = 0ud60_68157440
c     v885 = 0ud60_549756862464
c     v884 = 0ud60_1048640
c     v883 = 0ud60_8590983168
c     v882 = 0ud60_288230376152760320
c     v881 = 0ud60_1048704
c     v880 = 0ud60_17180917760
c     v879 = 0ud60_576460752304472064
c     v878 = 0ud60_4503599628419072
c     v877 = 0ud60_140737489403904
c     v876 = 0ud60_72057594038976512
c     v875 = 0ud60_5242880
c     v874 = 0ud60_137440002048
c     v873 = 0ud60_2199024304128
c     v872 = 0ud60_2251799814733824
c     v871 = 0ud60_70368745226240
c     v870 = 0ud60_144115188612726784
c     v869 = 0ud60_35184908959744
c     v868 = 0ud60_536872960
c     v867 = 0ud60_1125900443713536
c     v866 = 0ud60_562950490292224
c     v865 = 0ud60_536870916
c     v864 = 0ud60_34896609280
c     v863 = 0ud60_536887296
c     v862 = 0ud60_671088640
c     v861 = 0ud60_805306368
c     v860 = 0ud60_9007199791611904
c     v859 = 0ud60_1610612736
c     v858 = 0ud60_536870944
c     v857 = 0ud60_275414777856
c     v856 = 0ud60_603979776
c     v855 = 0ud60_550292684800
c     v854 = 0ud60_536870976
c     v853 = 0ud60_9126805504
c     v852 = 0ud60_288230376688582656
c     v851 = 0ud60_536871040
c     v850 = 0ud60_17716740096
c     v849 = 0ud60_576460752840294400
c     v848 = 0ud60_4503600164241408
c     v847 = 0ud60_140738025226240
c     v846 = 0ud60_72057594574798848
c     v845 = 0ud60_541065216
c     v844 = 0ud60_137975824384
c     v843 = 0ud60_2199560126464
c     v842 = 0ud60_2251800350556160
c     v841 = 0ud60_70369281048576
c     v840 = 0ud60_144115188075859968
c     v839 = 0ud60_35184372092928
c     v838 = 0ud60_6144
c     v837 = 0ud60_1125899906846720
c     v836 = 0ud60_562949953425408
c     v835 = 0ud60_4100
c     v834 = 0ud60_34359742464
c     v833 = 0ud60_20480
c     v832 = 0ud60_134221824
c     v831 = 0ud60_268439552
c     v830 = 0ud60_9007199254745088
c     v829 = 0ud60_1073745920
c     v828 = 0ud60_4128
c     v827 = 0ud60_274877911040
c     v826 = 0ud60_67112960
c     v825 = 0ud60_549755817984
c     v824 = 0ud60_4160
c     v823 = 0ud60_8589938688
c     v822 = 0ud60_288230376151715840
c     v821 = 0ud60_4224
c     v820 = 0ud60_17179873280
c     v819 = 0ud60_576460752303427584
c     v818 = 0ud60_4503599627374592
c     v817 = 0ud60_140737488359424
c     v816 = 0ud60_72057594037932032
c     v815 = 0ud60_4198400
c     v814 = 0ud60_137438957568
c     v813 = 0ud60_2199023259648
c     v812 = 0ud60_2251799813689344
c     v811 = 0ud60_70368744181760
c     v810 = 0ud60_162129586585337856
c     v809 = 0ud60_18049582881570816
c     v808 = 0ud60_18014398509484032
c     v807 = 0ud60_19140298416324608
c     v806 = 0ud60_18577348462903296
c     v805 = 0ud60_18014398509481988
c     v804 = 0ud60_18014432869220352
c     v803 = 0ud60_18014398509498368
c     v802 = 0ud60_18014398643699712
c     v801 = 0ud60_18014398777917440
c     v800 = 0ud60_27021597764222976
c     v799 = 0ud60_18014399583223808
c     v798 = 0ud60_18014398509482016
c     v797 = 0ud60_18014673387388928
c     v796 = 0ud60_18014398576590848
c     v795 = 0ud60_18014948265295872
c     v794 = 0ud60_18014398509482048
c     v793 = 0ud60_18014407099416576
c     v792 = 0ud60_306244774661193728
c     v791 = 0ud60_18014398509482112
c     v790 = 0ud60_18014415689351168
c     v789 = 0ud60_594475150812905472
c     v788 = 0ud60_22517998136852480
c     v787 = 0ud60_18155135997837312
c     v786 = 0ud60_90071992547409920
c     v785 = 0ud60_18014398513676288
c     v784 = 0ud60_18014535948435456
c     v783 = 0ud60_18016597532737536
c     v782 = 0ud60_20266198323167232
c     v781 = 0ud60_18084767253659648
c     v780 = 0ud60_144115188075921408
c     v779 = 0ud60_35184372154368
c     v778 = 0ud60_67584
c     v777 = 0ud60_1125899906908160
c     v776 = 0ud60_562949953486848
c     v775 = 0ud60_65540
c     v774 = 0ud60_34359803904
c     v773 = 0ud60_81920
c     v772 = 0ud60_134283264
c     v771 = 0ud60_268500992
c     v770 = 0ud60_9007199254806528
c     v769 = 0ud60_1073807360
c     v768 = 0ud60_65568
c     v767 = 0ud60_274877972480
c     v766 = 0ud60_67174400
c     v765 = 0ud60_549755879424
c     v764 = 0ud60_65600
c     v763 = 0ud60_8590000128
c     v762 = 0ud60_288230376151777280
c     v761 = 0ud60_65664
c     v760 = 0ud60_17179934720
c     v759 = 0ud60_576460752303489024
c     v758 = 0ud60_4503599627436032
c     v757 = 0ud60_140737488420864
c     v756 = 0ud60_72057594037993472
c     v755 = 0ud60_4259840
c     v754 = 0ud60_137439019008
c     v753 = 0ud60_2199023321088
c     v752 = 0ud60_2251799813750784
c     v751 = 0ud60_70368744243200
c     v750 = 0ud60_144115188075855880
c     v749 = 0ud60_35184372088840
c     v748 = 0ud60_2056
c     v747 = 0ud60_1125899906842632
c     v746 = 0ud60_562949953421320
c     v745 = 0ud60_12
c     v744 = 0ud60_34359738376
c     v743 = 0ud60_16392
c     v742 = 0ud60_134217736
c     v741 = 0ud60_268435464
c     v740 = 0ud60_9007199254741000
c     v739 = 0ud60_1073741832
c     v738 = 0ud60_40
c     v737 = 0ud60_274877906952
c     v736 = 0ud60_67108872
c     v735 = 0ud60_549755813896
c     v734 = 0ud60_72
c     v733 = 0ud60_8589934600
c     v732 = 0ud60_288230376151711752
c     v731 = 0ud60_136
c     v730 = 0ud60_17179869192
c     v729 = 0ud60_576460752303423496
c     v728 = 0ud60_4503599627370504
c     v727 = 0ud60_140737488355336
c     v726 = 0ud60_72057594037927944
c     v725 = 0ud60_4194312
c     v724 = 0ud60_137438953480
c     v723 = 0ud60_2199023255560
c     v722 = 0ud60_2251799813685256
c     v721 = 0ud60_70368744177672
c     v720 = 0ud60_144115190223339520
c     v719 = 0ud60_35186519572480
c     v718 = 0ud60_2147485696
c     v717 = 0ud60_1125902054326272
c     v716 = 0ud60_562952100904960
c     v715 = 0ud60_2147483652
c     v714 = 0ud60_36507222016
c     v713 = 0ud60_2147500032
c     v712 = 0ud60_2281701376
c     v711 = 0ud60_2415919104
c     v710 = 0ud60_9007201402224640
c     v709 = 0ud60_3221225472
c     v708 = 0ud60_2147483680
c     v707 = 0ud60_277025390592
c     v706 = 0ud60_2214592512
c     v705 = 0ud60_551903297536
c     v704 = 0ud60_2147483712
c     v703 = 0ud60_10737418240
c     v702 = 0ud60_288230378299195392
c     v701 = 0ud60_2147483776
c     v700 = 0ud60_19327352832
c     v699 = 0ud60_576460754450907136
c     v698 = 0ud60_4503601774854144
c     v697 = 0ud60_140739635838976
c     v696 = 0ud60_72057596185411584
c     v695 = 0ud60_2151677952
c     v694 = 0ud60_139586437120
c     v693 = 0ud60_2201170739200
c     v692 = 0ud60_2251801961168896
c     v691 = 0ud60_70370891661312
c     v690 = 0ud60_144115188075856384
c     v689 = 0ud60_35184372089344
c     v688 = 0ud60_2560
c     v687 = 0ud60_1125899906843136
c     v686 = 0ud60_562949953421824
c     v685 = 0ud60_516
c     v684 = 0ud60_34359738880
c     v683 = 0ud60_16896
c     v682 = 0ud60_134218240
c     v681 = 0ud60_268435968
c     v680 = 0ud60_9007199254741504
c     v679 = 0ud60_1073742336
c     v678 = 0ud60_544
c     v677 = 0ud60_274877907456
c     v676 = 0ud60_67109376
c     v675 = 0ud60_549755814400
c     v674 = 0ud60_576
c     v673 = 0ud60_8589935104
c     v672 = 0ud60_288230376151712256
c     v671 = 0ud60_640
c     v670 = 0ud60_17179869696
c     v669 = 0ud60_576460752303424000
c     v668 = 0ud60_4503599627371008
c     v667 = 0ud60_140737488355840
c     v666 = 0ud60_72057594037928448
c     v665 = 0ud60_4194816
c     v664 = 0ud60_137438953984
c     v663 = 0ud60_2199023256064
c     v662 = 0ud60_2251799813685760
c     v661 = 0ud60_70368744178176
c     v660 = 0ud60_144396663052566528
c     v659 = 0ud60_316659348799488
c     v658 = 0ud60_281474976712704
c     v657 = 0ud60_1407374883553280
c     v656 = 0ud60_844424930131968
c     v655 = 0ud60_281474976710660
c     v654 = 0ud60_281509336449024
c     v653 = 0ud60_281474976727040
c     v652 = 0ud60_281475110928384
c     v651 = 0ud60_281475245146112
c     v650 = 0ud60_9288674231451648
c     v649 = 0ud60_281476050452480
c     v648 = 0ud60_281474976710688
c     v647 = 0ud60_281749854617600
c     v646 = 0ud60_281475043819520
c     v645 = 0ud60_282024732524544
c     v644 = 0ud60_281474976710720
c     v643 = 0ud60_281483566645248
c     v642 = 0ud60_288511851128422400
c     v641 = 0ud60_281474976710784
c     v640 = 0ud60_281492156579840
c     v639 = 0ud60_576742227280134144
c     v638 = 0ud60_4785074604081152
c     v637 = 0ud60_422212465065984
c     v636 = 0ud60_72339069014638592
c     v635 = 0ud60_281474980904960
c     v634 = 0ud60_281612415664128
c     v633 = 0ud60_283673999966208
c     v632 = 0ud60_2533274790395904
c     v631 = 0ud60_351843720888320
c     v630 = 0ud60_144115188075855888
c     v629 = 0ud60_35184372088848
c     v628 = 0ud60_2064
c     v627 = 0ud60_1125899906842640
c     v626 = 0ud60_562949953421328
c     v625 = 0ud60_20
c     v624 = 0ud60_34359738384
c     v623 = 0ud60_16400
c     v622 = 0ud60_134217744
c     v621 = 0ud60_268435472
c     v620 = 0ud60_9007199254741008
c     v619 = 0ud60_1073741840
c     v618 = 0ud60_48
c     v617 = 0ud60_274877906960
c     v616 = 0ud60_67108880
c     v615 = 0ud60_549755813904
c     v614 = 0ud60_80
c     v613 = 0ud60_8589934608
c     v612 = 0ud60_288230376151711760
c     v611 = 0ud60_144
c     v610 = 0ud60_17179869200
c     v609 = 0ud60_576460752303423504
c     v608 = 0ud60_4503599627370512
c     v607 = 0ud60_140737488355344
c     v606 = 0ud60_72057594037927952
c     v605 = 0ud60_4194320
c     v604 = 0ud60_137438953488
c     v603 = 0ud60_2199023255568
c     v602 = 0ud60_2251799813685264
c     v601 = 0ud60_70368744177680
c     v600 = 0ud60_144115188075986944
c     v599 = 0ud60_35184372219904
c     v598 = 0ud60_133120
c     v597 = 0ud60_1125899906973696
c     v596 = 0ud60_562949953552384
c     v595 = 0ud60_131076
c     v594 = 0ud60_34359869440
c     v593 = 0ud60_147456
c     v592 = 0ud60_134348800
c     v591 = 0ud60_268566528
c     v590 = 0ud60_9007199254872064
c     v589 = 0ud60_1073872896
c     v588 = 0ud60_131104
c     v587 = 0ud60_274878038016
c     v586 = 0ud60_67239936
c     v585 = 0ud60_549755944960
c     v584 = 0ud60_131136
c     v583 = 0ud60_8590065664
c     v582 = 0ud60_288230376151842816
c     v581 = 0ud60_131200
c     v580 = 0ud60_17180000256
c     v579 = 0ud60_576460752303554560
c     v578 = 0ud60_4503599627501568
c     v577 = 0ud60_140737488486400
c     v576 = 0ud60_72057594038059008
c     v575 = 0ud60_4325376
c     v574 = 0ud60_137439084544
c     v573 = 0ud60_2199023386624
c     v572 = 0ud60_2251799813816320
c     v571 = 0ud60_70368744308736
c     v570 = 0ud60_144115188075888640
c     v569 = 0ud60_35184372121600
c     v568 = 0ud60_34816
c     v567 = 0ud60_1125899906875392
c     v566 = 0ud60_562949953454080
c     v565 = 0ud60_32772
c     v564 = 0ud60_34359771136
c     v563 = 0ud60_49152
c     v562 = 0ud60_134250496
c     v561 = 0ud60_268468224
c     v560 = 0ud60_9007199254773760
c     v559 = 0ud60_1073774592
c     v558 = 0ud60_32800
c     v557 = 0ud60_274877939712
c     v556 = 0ud60_67141632
c     v555 = 0ud60_549755846656
c     v554 = 0ud60_32832
c     v553 = 0ud60_8589967360
c     v552 = 0ud60_288230376151744512
c     v551 = 0ud60_32896
c     v550 = 0ud60_17179901952
c     v549 = 0ud60_576460752303456256
c     v548 = 0ud60_4503599627403264
c     v547 = 0ud60_140737488388096
c     v546 = 0ud60_72057594037960704
c     v545 = 0ud60_4227072
c     v544 = 0ud60_137438986240
c     v543 = 0ud60_2199023288320
c     v542 = 0ud60_2251799813718016
c     v541 = 0ud60_70368744210432
c     v540 = 0ud60_144115188075855874
c     v539 = 0ud60_35184372088834
c     v538 = 0ud60_2050
c     v537 = 0ud60_1125899906842626
c     v536 = 0ud60_562949953421314
c     v535 = 0ud60_6
c     v534 = 0ud60_34359738370
c     v533 = 0ud60_16386
c     v532 = 0ud60_134217730
c     v531 = 0ud60_268435458
c     v530 = 0ud60_9007199254740994
c     v529 = 0ud60_1073741826
c     v528 = 0ud60_34
c     v527 = 0ud60_274877906946
c     v526 = 0ud60_67108866
c     v525 = 0ud60_549755813890
c     v524 = 0ud60_66
c     v523 = 0ud60_8589934594
c     v522 = 0ud60_288230376151711746
c     v521 = 0ud60_130
c     v520 = 0ud60_17179869186
c     v519 = 0ud60_576460752303423490
c     v518 = 0ud60_4503599627370498
c     v517 = 0ud60_140737488355330
c     v516 = 0ud60_72057594037927938
c     v515 = 0ud60_4194306
c     v514 = 0ud60_137438953474
c     v513 = 0ud60_2199023255554
c     v512 = 0ud60_2251799813685250
c     v511 = 0ud60_70368744177666
c     v510 = 0ud60_144115188075864064
c     v509 = 0ud60_35184372097024
c     v508 = 0ud60_10240
c     v507 = 0ud60_1125899906850816
c     v506 = 0ud60_562949953429504
c     v505 = 0ud60_8196
c     v504 = 0ud60_34359746560
c     v503 = 0ud60_24576
c     v502 = 0ud60_134225920
c     v501 = 0ud60_268443648
c     v500 = 0ud60_9007199254749184
c     v499 = 0ud60_1073750016
c     v498 = 0ud60_8224
c     v497 = 0ud60_274877915136
c     v496 = 0ud60_67117056
c     v495 = 0ud60_549755822080
c     v494 = 0ud60_8256
c     v493 = 0ud60_8589942784
c     v492 = 0ud60_288230376151719936
c     v491 = 0ud60_8320
c     v490 = 0ud60_17179877376
c     v489 = 0ud60_576460752303431680
c     v488 = 0ud60_4503599627378688
c     v487 = 0ud60_140737488363520
c     v486 = 0ud60_72057594037936128
c     v485 = 0ud60_4202496
c     v484 = 0ud60_137438961664
c     v483 = 0ud60_2199023263744
c     v482 = 0ud60_2251799813693440
c     v481 = 0ud60_70368744185856
c     v480 = 0ud60_144115188076118016
c     v479 = 0ud60_35184372350976
c     v478 = 0ud60_264192
c     v477 = 0ud60_1125899907104768
c     v476 = 0ud60_562949953683456
c     v475 = 0ud60_262148
c     v474 = 0ud60_34360000512
c     v473 = 0ud60_278528
c     v472 = 0ud60_134479872
c     v471 = 0ud60_268697600
c     v470 = 0ud60_9007199255003136
c     v469 = 0ud60_1074003968
c     v468 = 0ud60_262176
c     v467 = 0ud60_274878169088
c     v466 = 0ud60_67371008
c     v465 = 0ud60_549756076032
c     v464 = 0ud60_262208
c     v463 = 0ud60_8590196736
c     v462 = 0ud60_288230376151973888
c     v461 = 0ud60_262272
c     v460 = 0ud60_17180131328
c     v459 = 0ud60_576460752303685632
c     v458 = 0ud60_4503599627632640
c     v457 = 0ud60_140737488617472
c     v456 = 0ud60_72057594038190080
c     v455 = 0ud60_4456448
c     v454 = 0ud60_137439215616
c     v453 = 0ud60_2199023517696
c     v452 = 0ud60_2251799813947392
c     v451 = 0ud60_70368744439808
c     v450 = 0ud60_144123984168878080
c     v449 = 0ud60_43980465111040
c     v448 = 0ud60_8796093024256
c     v447 = 0ud60_1134695999864832
c     v446 = 0ud60_571746046443520
c     v445 = 0ud60_8796093022212
c     v444 = 0ud60_8830452760576
c     v443 = 0ud60_8796093038592
c     v442 = 0ud60_8796227239936
c     v441 = 0ud60_8796361457664
c     v440 = 0ud60_9015995347763200
c     v439 = 0ud60_8797166764032
c     v438 = 0ud60_8796093022240
c     v437 = 0ud60_9070970929152
c     v436 = 0ud60_8796160131072
c     v435 = 0ud60_9345848836096
c     v434 = 0ud60_8796093022272
c     v433 = 0ud60_8804682956800
c     v432 = 0ud60_288239172244733952
c     v431 = 0ud60_8796093022336
c     v430 = 0ud60_8813272891392
c     v429 = 0ud60_576469548396445696
c     v428 = 0ud60_4512395720392704
c     v427 = 0ud60_149533581377536
c     v426 = 0ud60_72066390130950144
c     v425 = 0ud60_8796097216512
c     v424 = 0ud60_8933531975680
c     v423 = 0ud60_10995116277760
c     v422 = 0ud60_2260595906707456
c     v421 = 0ud60_79164837199872
c     v420 = 0ud60_144115188075856896
c     v419 = 0ud60_35184372089856
c     v418 = 0ud60_3072
c     v417 = 0ud60_1125899906843648
c     v416 = 0ud60_562949953422336
c     v415 = 0ud60_1028
c     v414 = 0ud60_34359739392
c     v413 = 0ud60_17408
c     v412 = 0ud60_134218752
c     v411 = 0ud60_268436480
c     v410 = 0ud60_9007199254742016
c     v409 = 0ud60_1073742848
c     v408 = 0ud60_1056
c     v407 = 0ud60_274877907968
c     v406 = 0ud60_67109888
c     v405 = 0ud60_549755814912
c     v404 = 0ud60_1088
c     v403 = 0ud60_8589935616
c     v402 = 0ud60_288230376151712768
c     v401 = 0ud60_1152
c     v400 = 0ud60_17179870208
c     v399 = 0ud60_576460752303424512
c     v398 = 0ud60_4503599627371520
c     v397 = 0ud60_140737488356352
c     v396 = 0ud60_72057594037928960
c     v395 = 0ud60_4195328
c     v394 = 0ud60_137438954496
c     v393 = 0ud60_2199023256576
c     v392 = 0ud60_2251799813686272
c     v391 = 0ud60_70368744178688
c     v390 = 0ud60_144132780261900288
c     v389 = 0ud60_52776558133248
c     v388 = 0ud60_17592186046464
c     v387 = 0ud60_1143492092887040
c     v386 = 0ud60_580542139465728
c     v385 = 0ud60_17592186044420
c     v384 = 0ud60_17626545782784
c     v383 = 0ud60_17592186060800
c     v382 = 0ud60_17592320262144
c     v381 = 0ud60_17592454479872
c     v380 = 0ud60_9024791440785408
c     v379 = 0ud60_17593259786240
c     v378 = 0ud60_17592186044448
c     v377 = 0ud60_17867063951360
c     v376 = 0ud60_17592253153280
c     v375 = 0ud60_18141941858304
c     v374 = 0ud60_17592186044480
c     v373 = 0ud60_17600775979008
c     v372 = 0ud60_288247968337756160
c     v371 = 0ud60_17592186044544
c     v370 = 0ud60_17609365913600
c     v369 = 0ud60_576478344489467904
c     v368 = 0ud60_4521191813414912
c     v367 = 0ud60_158329674399744
c     v366 = 0ud60_72075186223972352
c     v365 = 0ud60_17592190238720
c     v364 = 0ud60_17729624997888
c     v363 = 0ud60_19791209299968
c     v362 = 0ud60_2269391999729664
c     v361 = 0ud60_87960930222080
c     v360 = 0ud60_144119586122366976
c     v359 = 0ud60_39582418599936
c     v358 = 0ud60_4398046513152
c     v357 = 0ud60_1130297953353728
c     v356 = 0ud60_567347999932416
c     v355 = 0ud60_4398046511108
c     v354 = 0ud60_4432406249472
c     v353 = 0ud60_4398046527488
c     v352 = 0ud60_4398180728832
c     v351 = 0ud60_4398314946560
c     v350 = 0ud60_9011597301252096
c     v349 = 0ud60_4399120252928
c     v348 = 0ud60_4398046511136
c     v347 = 0ud60_4672924418048
c     v346 = 0ud60_4398113619968
c     v345 = 0ud60_4947802324992
c     v344 = 0ud60_4398046511168
c     v343 = 0ud60_4406636445696
c     v342 = 0ud60_288234774198222848
c     v341 = 0ud60_4398046511232
c     v340 = 0ud60_4415226380288
c     v339 = 0ud60_576465150349934592
c     v338 = 0ud60_4507997673881600
c     v337 = 0ud60_145135534866432
c     v336 = 0ud60_72061992084439040
c     v335 = 0ud60_4398050705408
c     v334 = 0ud60_4535485464576
c     v333 = 0ud60_6597069766656
c     v332 = 0ud60_2256197860196352
c     v331 = 0ud60_74766790688768
c     v330 = 0ud60_144115192370823168
c     v329 = 0ud60_35188667056128
c     v328 = 0ud60_4294969344
c     v327 = 0ud60_1125904201809920
c     v326 = 0ud60_562954248388608
c     v325 = 0ud60_4294967300
c     v324 = 0ud60_38654705664
c     v323 = 0ud60_4294983680
c     v322 = 0ud60_4429185024
c     v321 = 0ud60_4563402752
c     v320 = 0ud60_9007203549708288
c     v319 = 0ud60_5368709120
c     v318 = 0ud60_4294967328
c     v317 = 0ud60_279172874240
c     v316 = 0ud60_4362076160
c     v315 = 0ud60_554050781184
c     v314 = 0ud60_4294967360
c     v313 = 0ud60_12884901888
c     v312 = 0ud60_288230380446679040
c     v311 = 0ud60_4294967424
c     v310 = 0ud60_21474836480
c     v309 = 0ud60_576460756598390784
c     v308 = 0ud60_4503603922337792
c     v307 = 0ud60_140741783322624
c     v306 = 0ud60_72057598332895232
c     v305 = 0ud60_4299161600
c     v304 = 0ud60_141733920768
c     v303 = 0ud60_2203318222848
c     v302 = 0ud60_2251804108652544
c     v301 = 0ud60_70373039144960
c     v300 = 0ud60_144115188075856128
c     v299 = 0ud60_35184372089088
c     v298 = 0ud60_2304
c     v297 = 0ud60_1125899906842880
c     v296 = 0ud60_562949953421568
c     v295 = 0ud60_260
c     v294 = 0ud60_34359738624
c     v293 = 0ud60_16640
c     v292 = 0ud60_134217984
c     v291 = 0ud60_268435712
c     v290 = 0ud60_9007199254741248
c     v289 = 0ud60_1073742080
c     v288 = 0ud60_288
c     v287 = 0ud60_274877907200
c     v286 = 0ud60_67109120
c     v285 = 0ud60_549755814144
c     v284 = 0ud60_320
c     v283 = 0ud60_8589934848
c     v282 = 0ud60_288230376151712000
c     v281 = 0ud60_384
c     v280 = 0ud60_17179869440
c     v279 = 0ud60_576460752303423744
c     v278 = 0ud60_4503599627370752
c     v277 = 0ud60_140737488355584
c     v276 = 0ud60_72057594037928192
c     v275 = 0ud60_4194560
c     v274 = 0ud60_137438953728
c     v273 = 0ud60_2199023255808
c     v272 = 0ud60_2251799813685504
c     v271 = 0ud60_70368744177920
c     v270 = 0ud60_144116287587483648
c     v269 = 0ud60_36283883716608
c     v268 = 0ud60_1099511629824
c     v267 = 0ud60_1126999418470400
c     v266 = 0ud60_564049465049088
c     v265 = 0ud60_1099511627780
c     v264 = 0ud60_1133871366144
c     v263 = 0ud60_1099511644160
c     v262 = 0ud60_1099645845504
c     v261 = 0ud60_1099780063232
c     v260 = 0ud60_9008298766368768
c     v259 = 0ud60_1100585369600
c     v258 = 0ud60_1099511627808
c     v257 = 0ud60_1374389534720
c     v256 = 0ud60_1099578736640
c     v255 = 0ud60_1649267441664
c     v254 = 0ud60_1099511627840
c     v253 = 0ud60_1108101562368
c     v252 = 0ud60_288231475663339520
c     v251 = 0ud60_1099511627904
c     v250 = 0ud60_1116691496960
c     v249 = 0ud60_576461851815051264
c     v248 = 0ud60_4504699138998272
c     v247 = 0ud60_141836999983104
c     v246 = 0ud60_72058693549555712
c     v245 = 0ud60_1099515822080
c     v244 = 0ud60_1236950581248
c     v243 = 0ud60_3298534883328
c     v242 = 0ud60_2252899325313024
c     v241 = 0ud60_71468255805440
c     v240 = 0ud60_180143985094819840
c     v239 = 0ud60_36063981391052800
c     v238 = 0ud60_36028797018966016
c     v237 = 0ud60_37154696925806592
c     v236 = 0ud60_36591746972385280
c     v235 = 0ud60_36028797018963972
c     v234 = 0ud60_36028831378702336
c     v233 = 0ud60_36028797018980352
c     v232 = 0ud60_36028797153181696
c     v231 = 0ud60_36028797287399424
c     v230 = 0ud60_45035996273704960
c     v229 = 0ud60_36028798092705792
c     v228 = 0ud60_36028797018964000
c     v227 = 0ud60_36029071896870912
c     v226 = 0ud60_36028797086072832
c     v225 = 0ud60_36029346774777856
c     v224 = 0ud60_36028797018964032
c     v223 = 0ud60_36028805608898560
c     v222 = 0ud60_324259173170675712
c     v221 = 0ud60_36028797018964096
c     v220 = 0ud60_36028814198833152
c     v219 = 0ud60_612489549322387456
c     v218 = 0ud60_40532396646334464
c     v217 = 0ud60_36169534507319296
c     v216 = 0ud60_108086391056891904
c     v215 = 0ud60_36028797023158272
c     v214 = 0ud60_36028934457917440
c     v213 = 0ud60_36030996042219520
c     v212 = 0ud60_38280596832649216
c     v211 = 0ud60_36099165763141632
c     v210 = 0ud60_144115188109410304
c     v209 = 0ud60_35184405643264
c     v208 = 0ud60_33556480
c     v207 = 0ud60_1125899940397056
c     v206 = 0ud60_562949986975744
c     v205 = 0ud60_33554436
c     v204 = 0ud60_34393292800
c     v203 = 0ud60_33570816
c     v202 = 0ud60_167772160
c     v201 = 0ud60_301989888
c     v200 = 0ud60_9007199288295424
c     v199 = 0ud60_1107296256
c     v198 = 0ud60_33554464
c     v197 = 0ud60_274911461376
c     v196 = 0ud60_100663296
c     v195 = 0ud60_549789368320
c     v194 = 0ud60_33554496
c     v193 = 0ud60_8623489024
c     v192 = 0ud60_288230376185266176
c     v191 = 0ud60_33554560
c     v190 = 0ud60_17213423616
c     v189 = 0ud60_576460752336977920
c     v188 = 0ud60_4503599660924928
c     v187 = 0ud60_140737521909760
c     v186 = 0ud60_72057594071482368
c     v185 = 0ud60_37748736
c     v184 = 0ud60_137472507904
c     v183 = 0ud60_2199056809984
c     v182 = 0ud60_2251799847239680
c     v181 = 0ud60_70368777732096
c     v180 = 0ud60_144115256795332608
c     v179 = 0ud60_35253091565568
c     v178 = 0ud60_68719478784
c     v177 = 0ud60_1125968626319360
c     v176 = 0ud60_563018672898048
c     v175 = 0ud60_68719476740
c     v174 = 0ud60_103079215104
c     v173 = 0ud60_68719493120
c     v172 = 0ud60_68853694464
c     v171 = 0ud60_68987912192
c     v170 = 0ud60_9007267974217728
c     v169 = 0ud60_69793218560
c     v168 = 0ud60_68719476768
c     v167 = 0ud60_343597383680
c     v166 = 0ud60_68786585600
c     v165 = 0ud60_618475290624
c     v164 = 0ud60_68719476800
c     v163 = 0ud60_77309411328
c     v162 = 0ud60_288230444871188480
c     v161 = 0ud60_68719476864
c     v160 = 0ud60_85899345920
c     v159 = 0ud60_576460821022900224
c     v158 = 0ud60_4503668346847232
c     v157 = 0ud60_140806207832064
c     v156 = 0ud60_72057662757404672
c     v155 = 0ud60_68723671040
c     v154 = 0ud60_206158430208
c     v153 = 0ud60_2267742732288
c     v152 = 0ud60_2251868533161984
c     v151 = 0ud60_70437463654400
c     v150 = 0ud60_144115188077953024
c     v149 = 0ud60_35184374185984
c     v148 = 0ud60_2099200
c     v147 = 0ud60_1125899908939776
c     v146 = 0ud60_562949955518464
c     v145 = 0ud60_2097156
c     v144 = 0ud60_34361835520
c     v143 = 0ud60_2113536
c     v142 = 0ud60_136314880
c     v141 = 0ud60_270532608
c     v140 = 0ud60_9007199256838144
c     v139 = 0ud60_1075838976
c     v138 = 0ud60_2097184
c     v137 = 0ud60_274880004096
c     v136 = 0ud60_69206016
c     v135 = 0ud60_549757911040
c     v134 = 0ud60_2097216
c     v133 = 0ud60_8592031744
c     v132 = 0ud60_288230376153808896
c     v131 = 0ud60_2097280
c     v130 = 0ud60_17181966336
c     v129 = 0ud60_576460752305520640
c     v128 = 0ud60_4503599629467648
c     v127 = 0ud60_140737490452480
c     v126 = 0ud60_72057594040025088
c     v125 = 0ud60_6291456
c     v124 = 0ud60_137441050624
c     v123 = 0ud60_2199025352704
c     v122 = 0ud60_2251799815782400
c     v121 = 0ud60_70368746274816
c     v120 = 0ud60_144115188075855873
c     v119 = 0ud60_35184372088833
c     v118 = 0ud60_2049
c     v117 = 0ud60_1125899906842625
c     v116 = 0ud60_562949953421313
c     v115 = 0ud60_5
c     v114 = 0ud60_34359738369
c     v113 = 0ud60_16385
c     v112 = 0ud60_134217729
c     v111 = 0ud60_268435457
c     v110 = 0ud60_9007199254740993
c     v109 = 0ud60_1073741825
c     v108 = 0ud60_33
c     v107 = 0ud60_274877906945
c     v106 = 0ud60_67108865
c     v105 = 0ud60_549755813889
c     v104 = 0ud60_65
c     v103 = 0ud60_8589934593
c     v102 = 0ud60_288230376151711745
c     v101 = 0ud60_129
c     v100 = 0ud60_17179869185
c     v99 = 0ud60_576460752303423489
c     v98 = 0ud60_4503599627370497
c     v97 = 0ud60_140737488355329
c     v96 = 0ud60_72057594037927937
c     v95 = 0ud60_4194305
c     v94 = 0ud60_137438953473
c     v93 = 0ud60_2199023255553
c     v92 = 0ud60_2251799813685249
c     v91 = 0ud60_70368744177665
c     v90 = 0ud60_144115188076380160
c     v89 = 0ud60_35184372613120
c     v88 = 0ud60_526336
c     v87 = 0ud60_1125899907366912
c     v86 = 0ud60_562949953945600
c     v85 = 0ud60_524292
c     v84 = 0ud60_34360262656
c     v83 = 0ud60_540672
c     v82 = 0ud60_134742016
c     v81 = 0ud60_268959744
c     v80 = 0ud60_9007199255265280
c     v79 = 0ud60_1074266112
c     v78 = 0ud60_524320
c     v77 = 0ud60_274878431232
c     v76 = 0ud60_67633152
c     v75 = 0ud60_549756338176
c     v74 = 0ud60_524352
c     v73 = 0ud60_8590458880
c     v72 = 0ud60_288230376152236032
c     v71 = 0ud60_524416
c     v70 = 0ud60_17180393472
c     v69 = 0ud60_576460752303947776
c     v68 = 0ud60_4503599627894784
c     v67 = 0ud60_140737488879616
c     v66 = 0ud60_72057594038452224
c     v65 = 0ud60_4718592
c     v64 = 0ud60_137439477760
c     v63 = 0ud60_2199023779840
c     v62 = 0ud60_2251799814209536
c     v61 = 0ud60_70368744701952
c     v60 = 0ud60_144115188084244480
c     v59 = 0ud60_35184380477440
c     v58 = 0ud60_8390656
c     v57 = 0ud60_1125899915231232
c     v56 = 0ud60_562949961809920
c     v55 = 0ud60_8388612
c     v54 = 0ud60_34368126976
c     v53 = 0ud60_8404992
c     v52 = 0ud60_142606336
c     v51 = 0ud60_276824064
c     v50 = 0ud60_9007199263129600
c     v49 = 0ud60_1082130432
c     v48 = 0ud60_8388640
c     v47 = 0ud60_274886295552
c     v46 = 0ud60_75497472
c     v45 = 0ud60_549764202496
c     v44 = 0ud60_8388672
c     v43 = 0ud60_8598323200
c     v42 = 0ud60_288230376160100352
c     v41 = 0ud60_8388736
c     v40 = 0ud60_17188257792
c     v39 = 0ud60_576460752311812096
c     v38 = 0ud60_4503599635759104
c     v37 = 0ud60_140737496743936
c     v36 = 0ud60_72057594046316544
c     v35 = 0ud60_12582912
c     v34 = 0ud60_137447342080
c     v33 = 0ud60_2199031644160
c     v32 = 0ud60_2251799822073856
c     v31 = 0ud60_70368752566272
c     v30 = 0ud60_144115188092633088
c     v29 = 0ud60_35184388866048
c     v28 = 0ud60_16779264
c     v27 = 0ud60_1125899923619840
c     v26 = 0ud60_562949970198528
c     v25 = 0ud60_16777220
c     v24 = 0ud60_34376515584
c     v23 = 0ud60_16793600
c     v22 = 0ud60_150994944
c     v21 = 0ud60_285212672
c     v20 = 0ud60_9007199271518208
c     v19 = 0ud60_1090519040
c     v18 = 0ud60_16777248
c     v17 = 0ud60_274894684160
c     v16 = 0ud60_83886080
c     v15 = 0ud60_549772591104
c     v14 = 0ud60_16777280
c     v13 = 0ud60_8606711808
c     v12 = 0ud60_288230376168488960
c     v11 = 0ud60_16777344
c     v10 = 0ud60_17196646400
c     v9 = 0ud60_576460752320200704
c     v8 = 0ud60_4503599644147712
c     v7 = 0ud60_140737505132544
c     v6 = 0ud60_72057594054705152
c     v5 = 0ud60_20971520
c     v4 = 0ud60_137455730688
c     v3 = 0ud60_2199040032768
c     v2 = 0ud60_2251799830462464
c     v1 = 0ud60_70368760954880
c     v0 = 0ud60_0
c   -> State: 1.2 <-
c     state.tid = 11
c     state.vid = 538
c     state.target = 0ud60_288230376185266176
c   -> State: 1.3 <-
c     state.token[11] = 0ud60_288230376185266176
c     state.tid = 17
c     state.vid = 174
c     state.target = 0ud60_2050
c   -> State: 1.4 <-
c     state.token[17] = 0ud60_2050
c     state.tid = 6
c     state.vid = 378
c     state.target = 0ud60_103079215104
c   -> State: 1.5 <-
c     state.token[6] = 0ud60_103079215104
c     state.tid = 12
c     state.vid = 344
c     state.target = 0ud60_17592186044448
c   -> State: 1.6 <-
c     state.token[12] = 0ud60_17592186044448
c     state.tid = 19
c     state.vid = 600
c     state.target = 0ud60_4398046511168
c   -> State: 1.7 <-
c     state.token[19] = 0ud60_4398046511168
c     state.tid = 5
c     state.vid = 142
c     state.target = 0ud60_144115188075986944
c   -> State: 1.8 <-
c     state.token[5] = 0ud60_144115188075986944
c     state.tid = 10
c     state.vid = 323
c     state.target = 0ud60_136314880
c   -> State: 1.9 <-
c     state.token[10] = 0ud60_136314880
c     state.tid = 28
c     state.vid = 869
c     state.target = 0ud60_4294983680
c   -> State: 1.10 <-
c     state.token[28] = 0ud60_4294983680
c     state.tid = 11
c     state.vid = 641
c     state.target = 0ud60_35184908959744
c   -> State: 1.11 <-
c     state.token[11] = 0ud60_35184908959744
c     state.tid = 1
c     state.vid = 1
c     state.target = 0ud60_281474976710784
s 21 55 87 99 150 168 226 251 282 329 358 382 391 435 470 499 534 543 584 605 637 686 700 722 756 793 814 863 878
t 4 49 85 103 142 174 215 250 276 323 344 378 393 447 458 501 538 557 600 620 631 675 697 746 752 791 826 869 879
a YES
a 21 55 87 99 150 168 226 251 282 329 358 382 391 435 470 499 534 543 584 605 637 686 700 722 756 793 814 863 878
a 21 55 87 99 150 168 226 251 282 329 358 382 391 435 470 499 534 557 584 605 637 686 700 722 756 793 814 863 878
a 21 55 87 99 150 168 226 251 282 329 358 382 393 435 470 499 534 557 584 605 637 686 700 722 756 793 814 863 878
a 21 55 87 99 150 168 226 251 282 329 358 382 393 435 470 499 534 557 584 605 631 686 700 722 756 793 814 863 878
a 21 55 87 99 150 168 226 251 282 329 358 382 393 435 470 499 534 557 584 605 631 686 697 722 756 793 814 863 878
a 21 55 87 99 150 168 226 250 282 329 358 382 393 435 470 499 534 557 584 605 631 686 697 722 756 793 814 863 878
a 21 55 87 99 150 168 226 250 282 329 358 382 393 435 470 499 534 557 584 605 631 686 697 722 756 791 814 863 878
a 21 55 87 103 150 168 226 250 282 329 358 382 393 435 470 499 534 557 584 605 631 686 697 722 756 791 814 863 878
a 21 55 87 103 150 168 226 250 282 329 358 382 393 435 470 499 534 557 584 605 631 686 697 722 756 791 814 863 879
a 21 55 87 103 150 168 226 250 282 329 358 382 393 435 458 499 534 557 584 605 631 686 697 722 756 791 814 863 879
a 21 55 87 103 150 168 226 250 282 329 358 382 393 435 458 499 534 557 584 620 631 686 697 722 756 791 814 863 879
a 21 55 87 103 150 168 215 250 282 329 358 382 393 435 458 499 534 557 584 620 631 686 697 722 756 791 814 863 879
a 21 55 87 103 150 168 215 250 282 329 358 382 393 435 458 499 534 557 584 620 631 686 697 722 756 791 826 863 879
a 4 55 87 103 150 168 215 250 282 329 358 382 393 435 458 499 534 557 584 620 631 686 697 722 756 791 826 863 879
a 4 55 87 103 150 168 215 250 282 329 358 382 393 435 458 501 534 557 584 620 631 686 697 722 756 791 826 863 879
a 4 49 87 103 150 168 215 250 282 329 358 382 393 435 458 501 534 557 584 620 631 686 697 722 756 791 826 863 879
a 4 49 85 103 150 168 215 250 282 329 358 382 393 435 458 501 534 557 584 620 631 686 697 722 756 791 826 863 879
a 4 49 85 103 150 168 215 250 282 329 358 382 393 447 458 501 534 557 584 620 631 686 697 722 756 791 826 863 879
a 4 49 85 103 150 168 215 250 282 329 358 382 393 447 458 501 534 557 584 620 631 675 697 722 756 791 826 863 879
a 4 49 85 103 150 168 215 250 282 329 358 382 393 447 458 501 534 557 584 620 631 675 697 746 756 791 826 863 879
a 4 49 85 103 150 168 215 250 282 329 358 382 393 447 458 501 534 557 584 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 150 168 215 250 276 329 358 382 393 447 458 501 534 557 584 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 150 168 192 215 250 276 329 382 393 447 458 501 534 557 584 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 150 168 192 215 250 276 329 382 393 447 458 501 538 557 584 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 150 174 192 215 250 276 329 382 393 447 458 501 538 557 584 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 150 174 192 215 250 276 329 378 393 447 458 501 538 557 584 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 150 174 192 215 250 276 329 344 378 393 447 458 501 538 557 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 174 192 215 250 276 329 344 378 393 447 458 501 538 557 600 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 142 174 192 215 250 276 344 378 393 447 458 501 538 557 600 620 631 675 697 746 752 791 826 863 879
a 4 49 85 103 142 174 192 215 250 276 323 344 378 393 447 458 501 538 557 600 620 631 675 697 746 752 791 826 879
a 4 49 85 103 142 174 215 250 276 323 344 378 393 447 458 501 538 557 600 620 631 675 697 746 752 791 826 869 879