Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namesubmitted/manquinho/routing/normalized-s4-4-3-7pb.opb
MD5SUM24909033929a72aa74b2fd8b12f27bce
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 64
Optimality of the best value was proved YES
Number of terms in the objective function 672
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 672
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 3
Number of bits of the biggest number in a constraint 2
Biggest sum of numbers in a constraint 672
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark16.5375
Number of variables672
Total number of constraints2030
Number of constraints which are clauses2006
Number of constraints which are cardinality constraints (but not clauses)24
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint28

Trace number 2172

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-18 18:09:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2589 boxname=wulflinc31 idbench=245 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  24909033929a72aa74b2fd8b12f27bce  /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-7pb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-7pb.opb
IDLAUNCH: 2589
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        692184 kB
Buffers:         35924 kB
Cached:         275724 kB
SwapCached:       1016 kB
Active:         105636 kB
Inactive:       208756 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        691932 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5772 kB
Slab:            22404 kB
Committed_AS:    64340 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:12:21 (client local time) WITH STATUS 30 IN 168.228 SECONDS
stats: 2589 0 168.228 30

Solver Data

c Parsing PB file...
c Converting 2030 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2016]---> BDD-cost:    1
c ---[1991]---> BDD-cost:    1
c ---[1969]---> BDD-cost:    1
c ---[1959]---> BDD-cost:    1
c ---[1941]---> BDD-cost:    1
c ---[1919]---> BDD-cost:    1
c ---[1893]---> BDD-cost:    1
c ---[1887]---> BDD-cost:    1
c ---[1877]---> BDD-cost:    1
c ---[1867]---> BDD-cost:    1
c ---[1817]---> BDD-cost:    1
c ---[1815]---> BDD-cost:    1
c ---[1813]---> BDD-cost:    1
c ---[1787]---> BDD-cost:    1
c ---[1769]---> BDD-cost:    1
c ---[1743]---> BDD-cost:    1
c ---[1729]---> BDD-cost:    1
c ---[1703]---> BDD-cost:    1
c ---[1681]---> BDD-cost:    1
c ---[1671]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1647]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1599]---> BDD-cost:    1
c ---[1582]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    1
c ---[1528]---> BDD-cost:    1
c ---[1526]---> BDD-cost:    1
c ---[1500]---> BDD-cost:    1
c ---[1482]---> BDD-cost:    1
c ---[1456]---> BDD-cost:    1
c ---[1446]---> BDD-cost:    1
c ---[1436]---> BDD-cost:    1
c ---[1386]---> BDD-cost:    1
c ---[1384]---> BDD-cost:    1
c ---[1366]---> BDD-cost:    1
c ---[1344]---> BDD-cost:    1
c ---[1318]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1310]---> BDD-cost:    1
c ---[1284]---> BDD-cost:    1
c ---[1266]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1234]---> BDD-cost:    1
c ---[1216]---> BDD-cost:    1
c ---[1178]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1166]---> BDD-cost:    1
c ---[1140]---> BDD-cost:    1
c ---[1122]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1094]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1050]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1014]---> BDD-cost:    1
c ---[1004]---> BDD-cost:    1
c ---[ 954]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 934]---> BDD-cost:    1
c ---[ 912]---> BDD-cost:    1
c ---[ 886]---> BDD-cost:    1
c ---[ 880]---> BDD-cost:    1
c ---[ 870]---> BDD-cost:    1
c ---[ 860]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 799]---> BDD-cost:    1
c ---[ 789]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 617]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    1
c ---[ 542]---> BDD-cost:    1
c ---[ 532]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 524]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:    1
c ---[ 465]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 435]---> BDD-cost:    1
c ---[ 413]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 322]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 310]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 286]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 198]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   99
c ---[  22]---> BDD-cost:   99
c ---[  21]---> BDD-cost:   99
c ---[  20]---> BDD-cost:   99
c ---[  19]---> BDD-cost:   99
c ---[  18]---> BDD-cost:   99
c ---[  17]---> BDD-cost:   99
c ---[  16]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   99
c ---[  14]---> BDD-cost:   99
c ---[  13]---> BDD-cost:   99
c ---[  12]---> BDD-cost:   99
c ---[  11]---> BDD-cost:   99
c ---[  10]---> BDD-cost:   99
c ---[   9]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   99
c ---[   7]---> BDD-cost:   99
c ---[   6]---> BDD-cost:   99
c ---[   5]---> BDD-cost:   99
c ---[   4]---> BDD-cost:   99
c ---[   3]---> BDD-cost:   99
c ---[   2]---> BDD-cost:   99
c ---[   1]---> BDD-cost:   99
c ---[   0]---> BDD-cost:   99
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8414    24352 |    2804       0        0     nan |  0.000 % |
c |       102 |    8414    24352 |    3084     102     1435    14.1 |  4.304 % |
c |       253 |    8414    24352 |    3392     253     4525    17.9 |  4.304 % |
c |       479 |    8414    24352 |    3732     479    13584    28.4 |  4.304 % |
c |       818 |    8414    24352 |    4105     818    22084    27.0 |  4.304 % |
c |      1324 |    8414    24352 |    4515    1324    35488    26.8 |  4.304 % |
c |      2083 |    8414    24352 |    4967    2083    58571    28.1 |  4.304 % |
c |      3223 |    8414    24352 |    5464    3223    79607    24.7 |  4.304 % |
c |      4931 |    8414    24352 |    6010    4931   111128    22.5 |  4.304 % |
c |      7494 |    8414    24352 |    6611    4402    80202    18.2 |  4.304 % |
c |     11338 |    8414    24352 |    7272    4833    90241    18.7 |  4.304 % |
c |     17104 |    8414    24352 |    8000    6862   116041    16.9 |  4.304 % |
c |     25753 |    8414    24352 |    8800    7295   151785    20.8 |  4.304 % |
c |     38731 |    8414    24352 |    9680    6400   170131    26.6 |  4.304 % |
c |     58195 |    8414    24352 |   10648    5233   120703    23.1 |  4.304 % |
c |     87387 |    8414    24352 |   11713    7222   191228    26.5 |  4.304 % |
c |    131176 |    8414    24352 |   12884    9156   224748    24.5 |  4.304 % |
c ==============================================================================
c Found solution: 72
c ---[   0]---> Sorter-cost:30564     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    157119 |   43669   106611 |   14556    8772   190320    21.7 |  4.304 % |
c |    157219 |   43669   106611 |   16011    8872   192047    21.6 |  0.984 % |
c |    157370 |   43669   106611 |   17612    9023   195263    21.6 |  0.984 % |
c |    157595 |   43669   106611 |   19374    9248   199823    21.6 |  0.984 % |
c |    157932 |   43669   106611 |   21311    9585   206998    21.6 |  0.984 % |
c |    158439 |   43669   106611 |   23442   10092   216440    21.4 |  0.984 % |
c |    159198 |   43669   106611 |   25786   10851   229396    21.1 |  0.984 % |
c |    160338 |   43669   106611 |   28365   11991   247231    20.6 |  0.984 % |
c |    162046 |   43659   106591 |   31202   13698   277550    20.3 |  1.003 % |
c |    164608 |   43659   106591 |   34322   16260   345997    21.3 |  1.003 % |
c |    168452 |   43659   106591 |   37754   20104   425132    21.1 |  1.003 % |
c |    174220 |   43659   106591 |   41529   25872   531470    20.5 |  1.003 % |
c |    182869 |   43659   106591 |   45682   34521   676501    19.6 |  1.003 % |
c |    195844 |   43659   106591 |   50251   15667   266499    17.0 |  1.003 % |
c ==============================================================================
c Found solution: 70
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    212129 |   43628   106539 |   14542   31950   561723    17.6 |  1.003 % |
c |    212229 |   43541   106358 |   15996   14112   233643    16.6 |  1.302 % |
c |    212381 |   43541   106358 |   17595   14264   236765    16.6 |  1.302 % |
c |    212607 |   43541   106358 |   19355   14490   240094    16.6 |  1.302 % |
c |    212944 |   43541   106358 |   21290   14827   248435    16.8 |  1.302 % |
c |    213451 |   43541   106358 |   23420   15334   258286    16.8 |  1.302 % |
c |    214211 |   43541   106358 |   25762   16094   270666    16.8 |  1.302 % |
c |    215351 |   43541   106358 |   28338   17234   287319    16.7 |  1.302 % |
c |    217059 |   43512   106299 |   31172   18941   335982    17.7 |  1.351 % |
c ==============================================================================
c Found solution: 68
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217755 |   43431   106122 |   14477   19636   349703    17.8 |  1.351 % |
c |    217856 |   43004   105199 |   15924    9884   186986    18.9 |  2.564 % |
c |    218011 |   43004   105199 |   17517   10039   190518    19.0 |  2.564 % |
c |    218236 |   43004   105199 |   19268   10264   194433    18.9 |  2.564 % |
c |    218574 |   43004   105199 |   21195   10602   201176    19.0 |  2.564 % |
c |    219080 |   42867   104893 |   23315   11106   215752    19.4 |  2.878 % |
c |    219839 |   42867   104893 |   25646   11865   230177    19.4 |  2.878 % |
c |    220982 |   42832   104820 |   28211   13007   257700    19.8 |  2.943 % |
c |    222691 |   42832   104820 |   31032   14716   294522    20.0 |  2.943 % |
c |    225253 |   42775   104697 |   34136   17277   338898    19.6 |  3.071 % |
c ==============================================================================
c Found solution: 66
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225908 |   42616   104333 |   14205   17930   351633    19.6 |  3.071 % |
c |    226009 |   42574   104244 |   15625    9064   162768    18.0 |  3.614 % |
c |    226161 |   42574   104244 |   17188    9216   167726    18.2 |  3.614 % |
c |    226388 |   42574   104244 |   18906    9443   174020    18.4 |  3.614 % |
c |    226725 |   42574   104244 |   20797    9780   183720    18.8 |  3.614 % |
c |    227233 |   42516   104120 |   22877   10282   198976    19.4 |  3.735 % |
c |    227992 |   42516   104120 |   25165   11041   220335    20.0 |  3.735 % |
c ==============================================================================
c Found solution: 64
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    228164 |   42190   103359 |   14063   11212   225803    20.1 |  3.735 % |
c |    228264 |   42190   103359 |   15469   11312   228312    20.2 |  4.636 % |
c |    228414 |   42134   103241 |   17016   11460   230725    20.1 |  4.742 % |
c |    228639 |   42134   103241 |   18717   11685   233381    20.0 |  4.742 % |
c |    228978 |   41897   102702 |   20589   12021   242649    20.2 |  5.305 % |
c |    229484 |   41897   102702 |   22648   12527   250195    20.0 |  5.305 % |
c |    230243 |   41897   102702 |   24913   13286   259796    19.6 |  5.305 % |
c ==============================================================================
c Optimal solution: 64
s OPTIMUM FOUND
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 -v9 -v10 v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 -v20 -v21 v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 -v34 v35 -v36 -v37 -v38 -v39 -v40 -v41 -v42 -v43 -v44 -v45 -v46 -v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 v61 -v62 -v63 -v64 -v65 -v66 -v67 -v68 -v69 -v70 -v71 -v72 -v73 v74 v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 -v92 -v93 -v94 -v95 -v96 -v97 -v98 -v99 v100 v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 v109 -v110 -v111 -v112 -v113 -v114 v115 -v116 -v117 -v118 v119 -v120 -v121 v122 -v123 -v124 -v125 -v126 -v127 -v128 v129 -v130 -v131 -v132 -v133 -v134 v135 -v136 -v137 -v138 v139 -v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 -v154 -v155 -v156 -v157 v158 -v159 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 -v172 v173 v174 -v175 -v176 -v177 -v178 -v179 -v180 -v181 v182 -v183 -v184 -v185 -v186 -v187 v188 -v189 -v190 -v191 v192 -v193 -v194 -v195 v196 -v197 -v198 -v199 -v200 -v201 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 v210 -v211 -v212 -v213 v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 v230 -v231 -v232 -v233 v234 -v235 -v236 -v237 v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 -v250 -v251 -v252 v253 -v254 -v255 -v256 v257 -v258 -v259 -v260 v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 v271 v272 v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 -v281 -v282 -v283 -v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 v319 v320 v321 -v322 -v323 -v324 -v325 -v326 -v327 v328 -v329 -v330 -v331 v332 -v333 -v334 -v335 -v336 -v337 -v338 -v339 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 v353 -v354 -v355 -v356 v357 -v358 -v359 -v360 -v361 v362 v363 -v364 -v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 -v375 v376 -v377 -v378 -v379 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v390 v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400 v401 -v402 -v403 -v404 -v405 -v406 -v407 -v408 -v409 -v410 -v411 -v412 -v413 -v414 -v415 -v416 -v417 -v418 -v419 v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 v428 -v429 -v430 -v431 v432 -v433 -v434 -v435 v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 -v463 -v464 -v465 v466 v467 -v468 -v469 -v470 -v471 -v472 -v473 -v474 v475 -v476 -v477 -v478 v479 -v480 -v481 -v482 -v483 -v484 v485 v486 -v487 -v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 v512 -v513 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 -v526 v527 -v528 v529 -v530 -v531 -v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 -v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 v642 -v643 -v644 -v645 -v646 -v647 -v648 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 v660 -v661 -v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672
c _______________________________________________________________________________
c 
c restarts              : 64
c conflicts             : 231342         (1377 /sec)
c decisions             : 334898         (1994 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 167.962 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/16586/stat): 16586 (minisat+_script) R 16585 16586 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843263081 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16586/statm): 174 3 169 147 0 27 0
[pid=16586] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=16587
New process pid=16588
New process pid=16589
execve syscall for /bin/sed executable
One traced child (pid=16588) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=16589) exited with status: 0
One traced child (pid=16587) exited with status: 0
New process pid=16590
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-s4-4-3-7pb.opb

[startup+10.0036 s]
Raw data (loadavg): 0.84 0.95 0.98 2/58 16590
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 827 0 0 0 987 3 0 0 25 0 1 0 1843263086 3760128 814 4294967295 134512640 135094434 3221224448 3221223088 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16590/statm): 918 814 145 145 0 773 0
[pid=16590] vsize: 3672
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 5796

[startup+20.0055 s]
Raw data (loadavg): 0.86 0.95 0.98 2/58 16590
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 946 0 0 0 1984 5 0 0 25 0 1 0 1843263086 4259840 933 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 1040 933 145 145 0 895 0
[pid=16590] vsize: 4160
Current children cumulated CPU time (s) 19.91
Current children cumulated vsize (Kb) 6284

[startup+30.0064 s]
Raw data (loadavg): 0.88 0.95 0.98 2/58 16590
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 1140 0 0 0 2981 6 0 0 25 0 1 0 1843263086 5066752 1127 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 1237 1127 145 145 0 1092 0
[pid=16590] vsize: 4948
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 7072

[startup+40.0073 s]
Raw data (loadavg): 0.90 0.95 0.98 2/58 16590
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 1189 0 0 0 3980 6 0 0 25 0 1 0 1843263086 5263360 1176 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 1285 1176 145 145 0 1140 0
[pid=16590] vsize: 5140
Current children cumulated CPU time (s) 39.88
Current children cumulated vsize (Kb) 7264

[startup+50.0093 s]
Raw data (loadavg): 0.91 0.96 0.98 2/58 16590
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 1221 0 0 0 4981 6 0 0 25 0 1 0 1843263086 5402624 1208 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 1319 1208 145 145 0 1174 0
[pid=16590] vsize: 5276
Current children cumulated CPU time (s) 49.89
Current children cumulated vsize (Kb) 7400

[startup+60.0102 s]
Raw data (loadavg): 0.93 0.96 0.98 2/58 16592
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 1243 0 0 0 5980 7 0 0 25 0 1 0 1843263086 5500928 1230 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16590/statm): 1343 1230 145 145 0 1198 0
[pid=16590] vsize: 5372
Current children cumulated CPU time (s) 59.89
Current children cumulated vsize (Kb) 7496

[startup+70.0121 s]
Raw data (loadavg): 0.94 0.96 0.98 2/58 16592
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 2981 0 0 0 6967 14 0 0 25 0 1 0 1843263086 13189120 2831 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 3220 2831 145 145 0 3075 0
[pid=16590] vsize: 12880
Current children cumulated CPU time (s) 69.83
Current children cumulated vsize (Kb) 15004

[startup+80.013 s]
Raw data (loadavg): 0.95 0.96 0.98 2/58 16592
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3314 0 0 0 7962 16 0 0 25 0 1 0 1843263086 14573568 3164 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 3558 3164 145 145 0 3413 0
[pid=16590] vsize: 14232
Current children cumulated CPU time (s) 79.8
Current children cumulated vsize (Kb) 16356

[startup+90.013 s]
Raw data (loadavg): 0.95 0.96 0.98 2/58 16592
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3545 0 0 0 8959 18 0 0 25 0 1 0 1843263086 15699968 3395 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 3833 3395 145 145 0 3688 0
[pid=16590] vsize: 15332
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 17456

[startup+100.014 s]
Raw data (loadavg): 0.96 0.96 0.98 2/58 16592
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3665 0 0 0 9956 19 0 0 25 0 1 0 1843263086 16199680 3515 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16590/statm): 3955 3515 145 145 0 3810 0
[pid=16590] vsize: 15820
Current children cumulated CPU time (s) 99.77
Current children cumulated vsize (Kb) 17944

[startup+110.015 s]
Raw data (loadavg): 0.97 0.96 0.98 2/58 16592
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3829 0 0 0 10953 20 0 0 25 0 1 0 1843263086 16850944 3679 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 4114 3679 145 145 0 3969 0
[pid=16590] vsize: 16456
Current children cumulated CPU time (s) 109.75
Current children cumulated vsize (Kb) 18580

[startup+120.017 s]
Raw data (loadavg): 0.97 0.96 0.98 2/58 16594
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3867 0 0 0 11953 20 0 0 25 0 1 0 1843263086 17006592 3717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 4152 3717 145 145 0 4007 0
[pid=16590] vsize: 16608
Current children cumulated CPU time (s) 119.75
Current children cumulated vsize (Kb) 18732

[startup+130.018 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 16594
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3877 0 0 0 12953 20 0 0 25 0 1 0 1843263086 17055744 3727 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 4164 3727 145 145 0 4019 0
[pid=16590] vsize: 16656
Current children cumulated CPU time (s) 129.75
Current children cumulated vsize (Kb) 18780

[startup+140.019 s]
Raw data (loadavg): 0.98 0.96 0.98 2/58 16594
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3896 0 0 0 13953 20 0 0 25 0 1 0 1843263086 17154048 3746 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 4188 3746 145 145 0 4043 0
[pid=16590] vsize: 16752
Current children cumulated CPU time (s) 139.75
Current children cumulated vsize (Kb) 18876

[startup+150.02 s]
Raw data (loadavg): 0.98 0.97 0.98 2/58 16594
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3953 0 0 0 14953 20 0 0 25 0 1 0 1843263086 17424384 3803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 4254 3803 145 145 0 4109 0
[pid=16590] vsize: 17016
Current children cumulated CPU time (s) 149.75
Current children cumulated vsize (Kb) 19140

[startup+160.02 s]
Raw data (loadavg): 0.98 0.97 0.98 2/58 16594
Raw data (/proc/16586/stat): 16586 (minisat+_script) S 16585 16586 9102 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843263081 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16586/statm): 531 226 485 147 0 384 0
[pid=16586] vsize: 2124
Raw data (/proc/16590/stat): 16590 (minisat+_64-bit) R 16586 16586 9102 0 -1 0 3953 0 0 0 15953 20 0 0 25 0 1 0 1843263086 17424384 3803 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16590/statm): 4254 3803 145 145 0 4109 0
[pid=16590] vsize: 17016
Current children cumulated CPU time (s) 159.75
Current children cumulated vsize (Kb) 19140
One traced child (pid=16590) exited with status: 30
One traced child (pid=16586) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 168.482
CPU time (s): 168.228
CPU user time (s): 167.979
CPU system time (s): 0.248962
CPU usage (%): 99.8498
Max. virtual memory (cumulated for all children) (Kb): 19140

Verifier Data

Verifier:	OK	64