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/queen11_11_02.smv > queen11_11_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: 121 c Reading graph from file.. c Removing duplicates................. c Done. c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc c Edges: 1980 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: 66 c Sum: 509 c MaxSize: 0 c Time: 37 c Aborted: false c ML = 120 c SIZE = 121 c Removed 6 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,24]} c NODE covering index distribution:{[3,4][4,117]} c EDGE covering index distrubution:{[1,1980]} c Total edges:1980 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 -- specification G ((((((((((state.token[1] = v4 & state.token[2] = v18) & state.token[3] = v27) & state.token[4] = v35) & state.token[5] = v50) & state.token[6] = v56) & state.token[7] = v77) & state.token[8] = v96) & state.token[9] = v109) & state.token[10] = v113) -> G !((((((((((((((((((state.token[1] = v4 | state.token[1] = v18) | state.token[1] = v27) | state.token[1] = v35) | state.token[1] = v50) | state.token[1] = v56) | state.token[1] = v77) | state.token[1] = v85) | state.token[1] = v108) | state.token[1] = v113) & (((((((((state.token[2] = v4 | state.token[2] = v18) | state.token[2] = v27) | state.token[2] = v35) | state.token[2] = v50) | state.token[2] = v56) | state.token[2] = v77) | state.token[2] = v85) | state.token[2] = v108) | state.token[2] = v113)) & (((((((((state.token[3] = v4 | state.token[3] = v18) | state.token[3] = v27) | state.token[3] = v35) | state.token[3] = v50) | state.token[3] = v56) | state.token[3] = v77) | state.token[3] = v85) | state.token[3] = v108) | state.token[3] = v113)) & (((((((((state.token[4] = v4 | state.token[4] = v18) | state.token[4] = v27) | state.token[4] = v35) | state.token[4] = v50) | state.token[4] = v56) | state.token[4] = v77) | state.token[4] = v85) | state.token[4] = v108) | state.token[4] = v113)) & (((((((((state.token[5] = v4 | state.token[5] = v18) | state.token[5] = v27) | state.token[5] = v35) | state.token[5] = v50) | state.token[5] = v56) | state.token[5] = v77) | state.token[5] = v85) | state.token[5] = v108) | state.token[5] = v113)) & (((((((((state.token[6] = v4 | state.token[6] = v18) | state.token[6] = v27) | state.token[6] = v35) | state.token[6] = v50) | state.token[6] = v56) | state.token[6] = v77) | state.token[6] = v85) | state.token[6] = v108) | state.token[6] = v113)) & (((((((((state.token[7] = v4 | state.token[7] = v18) | state.token[7] = v27) | state.token[7] = v35) | state.token[7] = v50) | state.token[7] = v56) | state.token[7] = v77) | state.token[7] = v85) | state.token[7] = v108) | state.token[7] = v113)) & (((((((((state.token[8] = v4 | state.token[8] = v18) | state.token[8] = v27) | state.token[8] = v35) | state.token[8] = v50) | state.token[8] = v56) | state.token[8] = v77) | state.token[8] = v85) | state.token[8] = v108) | state.token[8] = v113)) & (((((((((state.token[9] = v4 | state.token[9] = v18) | state.token[9] = v27) | state.token[9] = v35) | state.token[9] = v50) | state.token[9] = v56) | state.token[9] = v77) | state.token[9] = v85) | state.token[9] = v108) | state.token[9] = v113)) & (((((((((state.token[10] = v4 | state.token[10] = v18) | state.token[10] = v27) | state.token[10] = v35) | state.token[10] = v50) | state.token[10] = v56) | state.token[10] = v77) | state.token[10] = v85) | state.token[10] = v108) | state.token[10] = v113))) 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_72567801053184 c state.token[2] = 0ud60_8858898432 c state.token[3] = 0ud60_27303072808042496 c state.token[4] = 0ud60_38280631729258496 c state.token[5] = 0ud60_577587201966082048 c state.token[6] = 0ud60_57174604660736 c state.token[7] = 0ud60_144115193448759296 c state.token[8] = 0ud60_154628259840 c state.token[9] = 0ud60_288371388517974032 c state.token[10] = 0ud60_1101659242752 c state.tid = 1 c state.vid = 9 c state.target = 0ud60_0 c v121 = 0ud60_140743930806272 c v120 = 0ud60_288230395479064577 c v119 = 0ud60_2684387344 c v118 = 0ud60_2165309952 c v117 = 0ud60_216172784529702912 c v116 = 0ud60_5087388762112 c v115 = 0ud60_18014400791191552 c v114 = 0ud60_633320845344768 c v113 = 0ud60_1101659242752 c v112 = 0ud60_105226698880 c v111 = 0ud60_4538786146942976 c v110 = 0ud60_1126179079716865 c v109 = 0ud60_288371388517974032 c v108 = 0ud60_292057809408 c v107 = 0ud60_144115463491682304 c v106 = 0ud60_412602073088 c v105 = 0ud60_72058418805866496 c v104 = 0ud60_18582021387321344 c v103 = 0ud60_70643622223872 c v102 = 0ud60_1443109273600 c v101 = 0ud60_4503908865016064 c v100 = 0ud60_35459249997952 c v99 = 0ud60_9007203558096912 c v98 = 0ud60_289356276066943488 c v97 = 0ud60_144255925572632576 c v96 = 0ud60_154628259840 c v95 = 0ud60_947912704 c v94 = 0ud60_563499734401024 c v93 = 0ud60_90071992555929600 c v92 = 0ud60_74835518554112 c v91 = 0ud60_4504699147395072 c v90 = 0ud60_34368391168 c v89 = 0ud60_35184382574848 c v88 = 0ud60_10999411245568 c v87 = 0ud60_441361559575330816 c v86 = 0ud60_1134833438851072 c v85 = 0ud60_149533716643840 c v84 = 0ud60_571763494748160 c v83 = 0ud60_9346385838080 c v82 = 0ud60_18023263338758144 c v81 = 0ud60_76640358502498304 c v80 = 0ud60_14293651163136 c v79 = 0ud60_8830454865920 c v78 = 0ud60_43980465377280 c v77 = 0ud60_144115193448759296 c v76 = 0ud60_288232713687662592 c v75 = 0ud60_9007200462733312 c v74 = 0ud60_1688850935054336 c v73 = 0ud60_140738830663680 c v72 = 0ud60_636728901632 c v71 = 0ud60_22517999747465216 c v70 = 0ud60_70369834698752 c v69 = 0ud60_72058694625394688 c v68 = 0ud60_4433479995392 c v67 = 0ud60_316660422549504 c v66 = 0ud60_17733920489472 c v65 = 0ud60_288247968476168192 c v64 = 0ud60_582741162754048 c v63 = 0ud60_9024791441965056 c v62 = 0ud60_1143561080799232 c v61 = 0ud60_4662479057584128 c v60 = 0ud60_18032007875397632 c v59 = 0ud60_87961469190144 c v58 = 0ud60_18691714453504 c v57 = 0ud60_72356695560421376 c v56 = 0ud60_57174604660736 c v55 = 0ud60_576460756732608576 c v54 = 0ud60_865254078409080832 c v53 = 0ud60_576460752307781632 c v52 = 0ud60_576463020047204352 c v51 = 0ud60_589971551453970432 c v50 = 0ud60_577587201966082048 c v49 = 0ud60_594615888303357952 c v48 = 0ud60_576531138227474432 c v47 = 0ud60_576743327328632832 c v46 = 0ud60_576460786679955456 c v45 = 0ud60_650805330527125504 c v44 = 0ud60_36591751267353600 c v43 = 0ud60_324259173170806848 c v42 = 0ud60_36028865738997760 c v41 = 0ud60_40532396651577344 c v40 = 0ud60_36030996310657024 c v39 = 0ud60_45036546031616000 c v38 = 0ud60_55169095435292672 c v37 = 0ud60_36521378228207616 c v36 = 0ud60_36029913710477312 c v35 = 0ud60_38280631729258496 c v34 = 0ud60_36063981407895552 c v33 = 0ud60_4362207236 c v32 = 0ud60_288230444938298368 c v31 = 0ud60_4503599694512192 c v30 = 0ud60_68683776 c v29 = 0ud60_341835776 c v28 = 0ud60_2748846182400 c v27 = 0ud60_27303072808042496 c v26 = 0ud60_1196268718145536 c v25 = 0ud60_2393636880777216 c v24 = 0ud60_51606781952 c v23 = 0ud60_35184976068640 c v22 = 0ud60_81604378626 c v21 = 0ud60_292733984369016836 c v20 = 0ud60_8589970432 c v19 = 0ud60_8593080384 c v18 = 0ud60_8858898432 c v17 = 0ud60_282033326653440 c v16 = 0ud60_18016606122688512 c v15 = 0ud60_11329376402538496 c v14 = 0ud60_1127008008470528 c v13 = 0ud60_140780438028320 c v12 = 0ud60_35210141892616 c v11 = 0ud60_4503603955892224 c v10 = 0ud60_288230376185268226 c v9 = 0ud60_35684356 c v8 = 0ud60_34608128 c v7 = 0ud60_281475278700608 c v6 = 0ud60_549789908992 c v5 = 0ud60_20266198360915968 c v4 = 0ud60_72567801053184 c v3 = 0ud60_9008298799923232 c v2 = 0ud60_1125934300135432 c v1 = 0ud60_175921893998592 c v0 = 0ud60_0 c -> State: 1.2 <- c state.vid = 114 c state.target = 0ud60_35684356 c -> State: 1.3 <- c state.token[1] = 0ud60_35684356 c state.tid = 10 c state.vid = 91 c state.target = 0ud60_633320845344768 c -> State: 1.4 <- c state.token[10] = 0ud60_633320845344768 c state.tid = 8 c state.vid = 85 c state.target = 0ud60_4504699147395072 c -> State: 1.5 <- c state.token[8] = 0ud60_4504699147395072 c state.tid = 9 c state.vid = 108 c state.target = 0ud60_149533716643840 c -> State: 1.6 <- c state.token[9] = 0ud60_149533716643840 c state.tid = 1 c state.vid = 4 c state.target = 0ud60_292057809408 c -> State: 1.7 <- c state.token[1] = 0ud60_292057809408 c state.tid = 10 c state.vid = 113 c state.target = 0ud60_72567801053184 c -> State: 1.8 <- c state.token[10] = 0ud60_72567801053184 c state.tid = 8 c state.vid = 97 c state.target = 0ud60_1101659242752 c -> State: 1.9 <- c state.token[8] = 0ud60_1101659242752 c state.tid = 1 c state.vid = 1 c state.target = 0ud60_144255925572632576 s 18 31 35 50 56 77 82 96 109 113 t 4 18 27 35 50 56 77 85 108 113 a YES a 18 31 35 50 56 77 82 96 109 113 a 4 31 35 50 56 77 82 96 109 113 a 4 18 35 50 56 77 82 96 109 113 a 4 18 27 35 50 56 77 96 109 113 a 9 18 27 35 50 56 77 96 109 113 a 9 18 27 35 50 56 77 96 109 114 a 9 18 27 35 50 56 77 91 109 114 a 9 18 27 35 50 56 77 85 91 114 a 18 27 35 50 56 77 85 91 108 114 a 4 18 27 35 50 56 77 85 91 108 a 4 18 27 35 50 56 77 85 108 113