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/queen12_12_02.smv > queen12_12_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: 144 c Reading graph from file.. c Removing duplicates................. c Done. c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc c Edges: 2596 c 0 cliques c 2 cliques c 4 cliques c 8 cliques c 16 cliques c 32 cliques c 64 cliques c The solution is correct. c Cliques: 69 c Sum: 587 c MaxSize: 0 c Time: 40 c Aborted: false c ML = 143 c SIZE = 144 c Removed 3 cliques to minimalize solution. c Result saved! c Clique size distribution: {[2,4][3,4][4,4][5,4][6,4][7,4][8,4][9,4][10,4][11,4][12,26]} c NODE covering index distribution:{[3,4][4,140]} c EDGE covering index distrubution:{[1,2596]} c Total edges:2596 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 c *** or email to . c *** Please report bugs to > c c *** Copyright (c) 2010-2014, Fondazione Bruno Kessler c c *** This version of NuSMV is linked to the CUDD library version 2.4.1 c *** Copyright (c) 1995-2004, Regents of the University of Colorado c c *** This version of NuSMV is linked to the MiniSat SAT solver. c *** See http://minisat.se/MiniSat.html c *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson c *** Copyright (c) 2007-2010, Niklas Sorensson c c -- no counterexample found with bound 0 c -- no counterexample found with bound 1 c -- no counterexample found with bound 2 c -- no counterexample found with bound 3 c -- no counterexample found with bound 4 c -- no counterexample found with bound 5 c -- no counterexample found with bound 6 c -- no counterexample found with bound 7 c -- no counterexample found with bound 8 c -- no counterexample found with bound 9 c -- no counterexample found with bound 10 c -- specification G (((((((((((state.token[1] = v10 & state.token[2] = v14) & state.token[3] = v30) & state.token[4] = v39) & state.token[5] = v60) & state.token[6] = v80) & state.token[7] = v89) & state.token[8] = v97) & state.token[9] = v112) & state.token[10] = v129) & state.token[11] = v139) -> G !((((((((((((((((((((state.token[1] = v10 | state.token[1] = v16) | state.token[1] = v30) | state.token[1] = v37) | state.token[1] = v60) | state.token[1] = v80) | state.token[1] = v86) | state.token[1] = v101) | state.token[1] = v111) | state.token[1] = v129) | state.token[1] = v143) & ((((((((((state.token[2] = v10 | state.token[2] = v16) | state.token[2] = v30) | state.token[2] = v37) | state.token[2] = v60) | state.token[2] = v80) | state.token[2] = v86) | state.token[2] = v101) | state.token[2] = v111) | state.token[2] = v129) | state.token[2] = v143)) & ((((((((((state.token[3] = v10 | state.token[3] = v16) | state.token[3] = v30) | state.token[3] = v37) | state.token[3] = v60) | state.token[3] = v80) | state.token[3] = v86) | state.token[3] = v101) | state.token[3] = v111) | state.token[3] = v129) | state.token[3] = v143)) & ((((((((((state.token[4] = v10 | state.token[4] = v16) | state.token[4] = v30) | state.token[4] = v37) | state.token[4] = v60) | state.token[4] = v80) | state.token[4] = v86) | state.token[4] = v101) | state.token[4] = v111) | state.token[4] = v129) | state.token[4] = v143)) & ((((((((((state.token[5] = v10 | state.token[5] = v16) | state.token[5] = v30) | state.token[5] = v37) | state.token[5] = v60) | state.token[5] = v80) | state.token[5] = v86) | state.token[5] = v101) | state.token[5] = v111) | state.token[5] = v129) | state.token[5] = v143)) & ((((((((((state.token[6] = v10 | state.token[6] = v16) | state.token[6] = v30) | state.token[6] = v37) | state.token[6] = v60) | state.token[6] = v80) | state.token[6] = v86) | state.token[6] = v101) | state.token[6] = v111) | state.token[6] = v129) | state.token[6] = v143)) & ((((((((((state.token[7] = v10 | state.token[7] = v16) | state.token[7] = v30) | state.token[7] = v37) | state.token[7] = v60) | state.token[7] = v80) | state.token[7] = v86) | state.token[7] = v101) | state.token[7] = v111) | state.token[7] = v129) | state.token[7] = v143)) & ((((((((((state.token[8] = v10 | state.token[8] = v16) | state.token[8] = v30) | state.token[8] = v37) | state.token[8] = v60) | state.token[8] = v80) | state.token[8] = v86) | state.token[8] = v101) | state.token[8] = v111) | state.token[8] = v129) | state.token[8] = v143)) & ((((((((((state.token[9] = v10 | state.token[9] = v16) | state.token[9] = v30) | state.token[9] = v37) | state.token[9] = v60) | state.token[9] = v80) | state.token[9] = v86) | state.token[9] = v101) | state.token[9] = v111) | state.token[9] = v129) | state.token[9] = v143)) & ((((((((((state.token[10] = v10 | state.token[10] = v16) | state.token[10] = v30) | state.token[10] = v37) | state.token[10] = v60) | state.token[10] = v80) | state.token[10] = v86) | state.token[10] = v101) | state.token[10] = v111) | state.token[10] = v129) | state.token[10] = v143)) & ((((((((((state.token[11] = v10 | state.token[11] = v16) | state.token[11] = v30) | state.token[11] = v37) | state.token[11] = v60) | state.token[11] = v80) | state.token[11] = v86) | state.token[11] = v101) | state.token[11] = v111) | state.token[11] = v129) | state.token[11] = v143))) 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] = 0ud66_36028801448149000 c state.token[2] = 0ud66_18448995942242713856 c state.token[3] = 0ud66_1226104998552666112 c state.token[4] = 0ud66_36893558524753739776 c state.token[5] = 0ud66_14293651165184 c state.token[6] = 0ud66_2783143002112 c state.token[7] = 0ud66_148618925142212608 c state.token[8] = 0ud66_4899916394595876992 c state.token[9] = 0ud66_9570149208440832 c state.token[10] = 0ud66_2882304036397121536 c state.token[11] = 0ud66_140738570486784 c state.tid = 1 c state.vid = 11 c state.target = 0ud66_0 c v144 = 0ud66_2252900399054848 c v143 = 0ud66_281484640387104 c v142 = 0ud66_576460757672132672 c v141 = 0ud66_275951747072 c v140 = 0ud66_9223372037934809088 c v139 = 0ud66_140738570486784 c v138 = 0ud66_1125901517471744 c v137 = 0ud66_144159169614708736 c v136 = 0ud66_580543213207680 c v135 = 0ud66_36893488698248659456 c v134 = 0ud66_18455751274038034433 c v133 = 0ud66_4616189619128500224 c v132 = 0ud66_2305846307748577312 c v131 = 0ud66_2308376284004089920 c v130 = 0ud66_2305843022098661376 c v129 = 0ud66_2882304036397121536 c v128 = 0ud66_2305843009217922048 c v127 = 0ud66_11529355784093696000 c v126 = 0ud66_2306977705221947392 c v125 = 0ud66_2449975789475610624 c v124 = 0ud66_2306441693295017984 c v123 = 0ud66_39208338355887538304 c v122 = 0ud66_20757090682550616576 c v121 = 0ud66_6917529029788565505 c v120 = 0ud66_1116691759168 c v119 = 0ud66_283674000293888 c v118 = 0ud66_2251804111011840 c v117 = 0ud66_283468104704 c v116 = 0ud66_576460752844750848 c v115 = 0ud66_149533581672448 c v114 = 0ud66_9224515528947924992 c v113 = 0ud66_144115737840320512 c v112 = 0ud66_9570149208440832 c v111 = 0ud66_36898026931418824704 c v110 = 0ud66_18446744075857297536 c v109 = 0ud66_4611686018561868288 c v108 = 0ud66_360289069701332992 c v107 = 0ud66_288511868310388736 c v106 = 0ud66_288232579469935616 c v105 = 0ud66_290482451380174848 c v104 = 0ud66_288239180838862848 c v103 = 0ud66_864849458129534976 c v102 = 0ud66_289356825814401024 c v101 = 0ud66_9664724800337084416 c v100 = 0ud66_293296925740892160 c v99 = 0ud66_37181718525718315008 c v98 = 0ud66_18735009634367569920 c v97 = 0ud66_4899916394595876992 c v96 = 0ud66_1237221113856 c v95 = 0ud66_72339206453593088 c v94 = 0ud66_159450660864 c v93 = 0ud66_11407433138176 c v92 = 0ud66_2269529442877440 c v91 = 0ud66_141433273057280 c v90 = 0ud66_586593988903960576 c v89 = 0ud66_148618925142212608 c v88 = 0ud66_9223935126394634240 c v87 = 0ud66_36893488285000663040 c v86 = 0ud66_18446744211165298688 c v85 = 0ud66_4611721340239478784 c v84 = 0ud66_1133938476032 c v83 = 0ud66_281510141755392 c v82 = 0ud66_72066428785655808 c v81 = 0ud66_17918603558912 c v80 = 0ud66_2783143002112 c v79 = 0ud66_11399770916519936 c v78 = 0ud66_5629542483886080 c v77 = 0ud66_720575976886501376 c v76 = 0ud66_562984447410176 c v75 = 0ud66_46116860218650394624 c v74 = 0ud66_18446744108078727168 c v73 = 0ud66_4629700451296624640 c v72 = 0ud66_1100082184192 c v71 = 0ud66_290271170396160 c v70 = 0ud66_17596783001600 c v69 = 0ud66_72058418705203200 c v68 = 0ud66_9007216472358912 c v67 = 0ud66_4646536172535808 c v66 = 0ud66_3377701901565952 c v65 = 0ud66_144115196833562624 c v64 = 0ud66_577023702307176448 c v63 = 0ud66_36893488147453739008 c v62 = 0ud66_27688130509107363840 c v61 = 0ud66_4611686018469855232 c v60 = 0ud66_14293651165184 c v59 = 0ud66_303465209397248 c v58 = 0ud66_4952164401152 c v57 = 0ud66_9011872447594496 c v56 = 0ud66_76565591716003840 c v55 = 0ud66_145154862219264 c v54 = 0ud66_1132497110827008 c v53 = 0ud66_146371385952829440 c v52 = 0ud66_567356590915584 c v51 = 0ud66_37487967696278519808 c v50 = 0ud66_18446748471756619776 c v49 = 0ud66_13835062453328683008 c v48 = 0ud66_89060441849860 c v47 = 0ud66_352393476706304 c v46 = 0ud66_9077572294017024 c v45 = 0ud66_4574243316563968 c v44 = 0ud66_70371164291072 c v43 = 0ud66_72268700404678656 c v42 = 0ud66_1196285847666688 c v41 = 0ud66_144187755844337664 c v40 = 0ud66_20899517020766208 c v39 = 0ud66_36893558524753739776 c v38 = 0ud66_19023275194757160960 c v37 = 0ud66_4611756387171600384 c v36 = 0ud66_1152923153874288648 c v35 = 0ud66_1162210178838298628 c v34 = 0ud66_1157425108529188864 c v33 = 0ud66_1152921781632368640 c v32 = 0ud66_1152921504812367872 c v31 = 0ud66_1153062242380414976 c v30 = 0ud66_1226104998552666112 c v29 = 0ud66_1315051108372054016 c v28 = 0ud66_1153486653584048128 c v27 = 0ud66_38048661451839643648 c v26 = 0ud66_19599665586906335232 c v25 = 0ud66_6341068275337658624 c v24 = 0ud66_9008367485845520 c v23 = 0ud66_4785143323557896 c v22 = 0ud66_75161927684 c v21 = 0ud66_343731605504 c v20 = 0ud66_68740579328 c v19 = 0ud66_140806275989504 c v18 = 0ud66_19140367404236800 c v17 = 0ud66_216172850833784832 c v16 = 0ud66_563035852775424 c v15 = 0ud66_36893490415161837568 c v14 = 0ud66_18448995942242713856 c v13 = 0ud66_4611686095736799234 c v12 = 0ud66_40533496157962240 c v11 = 0ud66_36310274143158288 c v10 = 0ud66_36028801448149000 c v9 = 0ud66_36029071913648132 c v8 = 0ud66_36028797024210944 c v7 = 0ud66_54183933016932352 c v6 = 0ud66_37154696993439744 c v5 = 0ud66_180143985363263488 c v4 = 0ud66_108649341010315264 c v3 = 0ud66_36929516961617936640 c v2 = 0ud66_18482775069751771138 c v1 = 0ud66_4649966615260037120 c v0 = 0ud66_0 c -> State: 1.2 <- c state.vid = 70 c state.target = 0ud66_36310274143158288 c -> State: 1.3 <- c state.token[1] = 0ud66_36310274143158288 c state.tid = 9 c state.vid = 109 c state.target = 0ud66_17596783001600 c -> State: 1.4 <- c state.token[9] = 0ud66_17596783001600 c state.tid = 8 c state.vid = 101 c state.target = 0ud66_4611686018561868288 c -> State: 1.5 <- c state.token[8] = 0ud66_4611686018561868288 c state.tid = 7 c state.vid = 16 c state.target = 0ud66_9664724800337084416 c -> State: 1.6 <- c state.token[7] = 0ud66_9664724800337084416 c state.tid = 2 c state.vid = 86 c state.target = 0ud66_563035852775424 c -> State: 1.7 <- c state.token[2] = 0ud66_563035852775424 c state.tid = 4 c state.vid = 111 c state.target = 0ud66_18446744211165298688 c -> State: 1.8 <- c state.token[4] = 0ud66_18446744211165298688 c state.tid = 8 c state.vid = 37 c state.target = 0ud66_36898026931418824704 c -> State: 1.9 <- c state.token[8] = 0ud66_36898026931418824704 c state.tid = 1 c state.vid = 10 c state.target = 0ud66_4611756387171600384 c -> State: 1.10 <- c state.token[1] = 0ud66_4611756387171600384 c state.tid = 9 c state.vid = 143 c state.target = 0ud66_36028801448149000 c -> State: 1.11 <- c state.token[9] = 0ud66_36028801448149000 c state.tid = 11 c state.vid = 1 c state.target = 0ud66_281484640387104 c -> State: 1.12 <- c state.token[11] = 0ud66_281484640387104 c state.tid = 1 c state.target = 0ud66_4649966615260037120 s 11 14 30 39 60 80 89 97 112 129 139 t 10 16 30 37 60 80 86 101 111 129 143 a YES a 11 14 30 39 60 80 89 97 112 129 139 a 11 14 30 39 60 70 80 89 97 129 139 a 11 14 30 39 60 70 80 89 109 129 139 a 11 14 30 39 60 70 80 101 109 129 139 a 11 16 30 39 60 70 80 101 109 129 139 a 11 16 30 60 70 80 86 101 109 129 139 a 11 16 30 60 70 80 86 101 111 129 139 a 16 30 37 60 70 80 86 101 111 129 139 a 10 16 30 37 60 80 86 101 111 129 139 a 10 16 30 37 60 80 86 101 111 129 143