PB'05 competition: run trace

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:

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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-6pb.opb
MD5SUM	c12951e903009dc00793ce72594cf3ba
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	66
Optimality of the best value was proved	NO
Number of terms in the objective function	624
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	624
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	624
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03684
Number of variables	624
Total number of constraints	1884
Number of constraints which are clauses	1860
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	26

Trace number 5882

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 02:28:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4378 boxname=wulflinc10 idbench=242 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c12951e903009dc00793ce72594cf3ba  /oldhome/oroussel/tmp/wulflinc10/normalized-s4-4-3-6pb.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-s4-4-3-6pb.opb /oldhome/oroussel/tmp/wulflinc10/normalized-s4-4-3-6pb.opb
IDLAUNCH: 4378
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        864996 kB
Buffers:         35292 kB
Cached:         114824 kB
SwapCached:        164 kB
Active:          54284 kB
Inactive:        98852 kB
HighTotal:      131008 kB
HighFree:        12572 kB
LowTotal:       903652 kB
LowFree:        852424 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10904 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:29:40 (client local time) WITH STATUS 30 IN 67.7187 SECONDS
stats: 4378 0 67.7187 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1884 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1882]---> BDD-cost:    1
c ---[1856]---> BDD-cost:    1
c ---[1838]---> BDD-cost:    1
c ---[1812]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1772]---> BDD-cost:    1
c ---[1750]---> BDD-cost:    1
c ---[1740]---> BDD-cost:    1
c ---[1726]---> BDD-cost:    1
c ---[1700]---> BDD-cost:    1
c ---[1678]---> BDD-cost:    1
c ---[1668]---> BDD-cost:    1
c ---[1666]---> BDD-cost:    1
c ---[1640]---> BDD-cost:    1
c ---[1622]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1578]---> BDD-cost:    1
c ---[1556]---> BDD-cost:    1
c ---[1530]---> BDD-cost:    1
c ---[1524]---> BDD-cost:    1
c ---[1514]---> BDD-cost:    1
c ---[1504]---> BDD-cost:    1
c ---[1454]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1450]---> BDD-cost:    1
c ---[1424]---> BDD-cost:    1
c ---[1407]---> BDD-cost:    1
c ---[1381]---> BDD-cost:    1
c ---[1363]---> BDD-cost:    1
c ---[1342]---> BDD-cost:    1
c ---[1316]---> BDD-cost:    1
c ---[1310]---> BDD-cost:    1
c ---[1300]---> BDD-cost:    1
c ---[1290]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1238]---> BDD-cost:    1
c ---[1189]---> BDD-cost:    1
c ---[1179]---> BDD-cost:    1
c ---[1169]---> BDD-cost:    1
c ---[1167]---> BDD-cost:    1
c ---[1165]---> BDD-cost:    1
c ---[1139]---> BDD-cost:    1
c ---[1121]---> BDD-cost:    1
c ---[1095]---> BDD-cost:    1
c ---[1093]---> BDD-cost:    1
c ---[1067]---> BDD-cost:    1
c ---[1049]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[1009]---> BDD-cost:    1
c ---[ 983]---> BDD-cost:    1
c ---[ 961]---> BDD-cost:    1
c ---[ 951]---> BDD-cost:    1
c ---[ 933]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:    1
c ---[ 885]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:    1
c ---[ 877]---> BDD-cost:    1
c ---[ 851]---> BDD-cost:    1
c ---[ 833]---> BDD-cost:    1
c ---[ 807]---> BDD-cost:    1
c ---[ 789]---> BDD-cost:    1
c ---[ 767]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:    1
c ---[ 689]---> BDD-cost:    1
c ---[ 663]---> BDD-cost:    1
c ---[ 657]---> BDD-cost:    1
c ---[ 639]---> BDD-cost:    1
c ---[ 601]---> BDD-cost:    1
c ---[ 591]---> BDD-cost:    1
c ---[ 585]---> BDD-cost:    1
c ---[ 567]---> BDD-cost:    1
c ---[ 529]---> BDD-cost:    1
c ---[ 519]---> BDD-cost:    1
c ---[ 483]---> BDD-cost:    1
c ---[ 461]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:    1
c ---[ 449]---> BDD-cost:    1
c ---[ 397]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:    1
c ---[ 373]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:    1
c ---[ 318]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 298]---> BDD-cost:    1
c ---[ 289]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   91
c ---[  22]---> BDD-cost:   91
c ---[  21]---> BDD-cost:   91
c ---[  20]---> BDD-cost:   91
c ---[  19]---> BDD-cost:   91
c ---[  18]---> BDD-cost:   91
c ---[  17]---> BDD-cost:   91
c ---[  16]---> BDD-cost:   91
c ---[  15]---> BDD-cost:   91
c ---[  14]---> BDD-cost:   91
c ---[  13]---> BDD-cost:   91
c ---[  12]---> BDD-cost:   91
c ---[  11]---> BDD-cost:   91
c ---[  10]---> BDD-cost:   91
c ---[   9]---> BDD-cost:   91
c ---[   8]---> BDD-cost:   91
c ---[   7]---> BDD-cost:   91
c ---[   6]---> BDD-cost:   91
c ---[   5]---> BDD-cost:   91
c ---[   4]---> BDD-cost:   91
c ---[   3]---> BDD-cost:   91
c ---[   2]---> BDD-cost:   91
c ---[   1]---> BDD-cost:   91
c ---[   0]---> BDD-cost:   91
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7740    22400 |    2580       0        0     nan |  0.000 % |
c |       102 |    7740    22400 |    2838     102     1146    11.2 |  4.396 % |
c |       252 |    7740    22400 |    3121     252     4342    17.2 |  4.396 % |
c |       478 |    7740    22400 |    3433     478    10604    22.2 |  4.396 % |
c |       816 |    7740    22400 |    3777     816    17319    21.2 |  4.396 % |
c |      1322 |    7740    22400 |    4155    1322    29601    22.4 |  4.396 % |
c |      2083 |    7740    22400 |    4570    2083    56358    27.1 |  4.396 % |
c |      3225 |    7740    22400 |    5027    3225   102912    31.9 |  4.396 % |
c |      4934 |    7740    22400 |    5530    4934   156429    31.7 |  4.396 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:28228     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5682 |   40254    98312 |   13418    5681   184124    32.4 |  4.396 % |
c |      5785 |   40254    98312 |   14759    5784   185911    32.1 |  1.022 % |
c |      5935 |   40254    98312 |   16235    5934   189047    31.9 |  1.022 % |
c |      6161 |   40254    98312 |   17859    6160   194828    31.6 |  1.022 % |
c |      6498 |   40254    98312 |   19645    6497   205077    31.6 |  1.022 % |
c |      7004 |   40254    98312 |   21609    7003   225914    32.3 |  1.022 % |
c |      7766 |   40254    98312 |   23770    7765   255593    32.9 |  1.022 % |
c |      8908 |   40254    98312 |   26147    8907   285387    32.0 |  1.022 % |
c |     10616 |   40237    98264 |   28762   10581   343405    32.5 |  1.030 % |
c |     13179 |   40220    98216 |   31638   13120   429152    32.7 |  1.038 % |
c |     17025 |   40220    98216 |   34802   16966   528804    31.2 |  1.038 % |
c |     22792 |   40185    98122 |   38283   22668   749533    33.1 |  1.055 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:18762     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29423 |   57753   139220 |   19251   29141   985127    33.8 |  1.055 % |
c |     29528 |   57736   139172 |   21176   12989   436874    33.6 |  2.354 % |
c |     29680 |   57736   139172 |   23293   13141   438850    33.4 |  2.354 % |
c |     29909 |   57736   139172 |   25623   13370   441839    33.0 |  2.354 % |
c |     30247 |   57736   139172 |   28185   13708   446472    32.6 |  2.354 % |
c |     30754 |   57487   138565 |   31003   13049   433183    33.2 |  2.685 % |
c |     31514 |   57487   138565 |   34104   13809   453613    32.8 |  2.685 % |
c |     32653 |   57487   138565 |   37514   14948   487400    32.6 |  2.685 % |
c |     34362 |   57448   138486 |   41266   16656   530336    31.8 |  2.745 % |
c |     36924 |   57408   138400 |   45392   19215   599506    31.2 |  2.808 % |
c |     40768 |   57249   138058 |   49932   23053   700611    30.4 |  3.052 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24084     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43845 |   83730   199851 |   27910   24581   730579    29.7 |  3.052 % |
c |     43945 |   83730   199851 |   30701   24681   733808    29.7 |  2.289 % |
c |     44097 |   83730   199851 |   33771   24833   738210    29.7 |  2.289 % |
c |     44322 |   83730   199851 |   37148   25058   743040    29.7 |  2.289 % |
c |     44659 |   83730   199851 |   40863   25395   750694    29.6 |  2.289 % |
c |     45165 |   83677   199734 |   44949   25898   760379    29.4 |  2.348 % |
c |     45924 |   83677   199734 |   49444   26657   777006    29.1 |  2.348 % |
c |     47063 |   83621   199608 |   54388   27793   807589    29.1 |  2.411 % |
c |     48773 |   83621   199608 |   59827   29503   851319    28.9 |  2.411 % |
c |     51335 |   83191   198707 |   65810   32051   920719    28.7 |  2.857 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:21572     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52747 |  105759   251407 |   35253   33444   953848    28.5 |  2.857 % |
c |     52848 |  105759   251407 |   38778   33545   956204    28.5 |  2.545 % |
c |     52998 |  105515   250900 |   42656   33690   959409    28.5 |  2.748 % |
c |     53224 |  105404   250662 |   46921   33913   965054    28.5 |  2.845 % |
c |     53561 |  105318   250478 |   51613   34245   972467    28.4 |  2.918 % |
c |     54069 |  105318   250478 |   56775   34753   984703    28.3 |  2.918 % |
c |     54828 |  105193   250209 |   62452   35509   999763    28.2 |  3.028 % |
c |     55967 |  104584   248900 |   68698   36490  1023192    28.0 |  3.503 % |
c |     57676 |  104566   248852 |   75567   38172  1057981    27.7 |  3.506 % |
c ==============================================================================
c [1mOptimal solution: 66[0m
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
c _______________________________________________________________________________
c 
c restarts              : 51
c conflicts             : 57729          (856 /sec)
c decisions             : 112858         (1673 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 67.4667 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.91 2/54 31306
Raw data (stat): 31306 (runsolver) R 31305 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422778635 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 31306
Raw data (stat): 31306 (minisat+) R 31305 25347 25346 0 -1 0 3142 0 0 0 990 7 0 0 25 0 1 0 422778635 14827520 3070 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3620 3070 603 41 0 3579 0
vsize: 14480
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 31306
Raw data (stat): 31306 (minisat+) R 31305 25347 25346 0 -1 0 4497 0 0 0 1986 11 0 0 25 0 1 0 422778635 21327872 4333 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5207 4333 603 41 0 5166 0
vsize: 20828
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 31306
Raw data (stat): 31306 (minisat+) R 31305 25347 25346 0 -1 0 4577 0 0 0 2985 12 0 0 25 0 1 0 422778635 21774336 4413 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5316 4413 603 41 0 5275 0
vsize: 21264
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 31306
Raw data (stat): 31306 (minisat+) R 31305 25347 25346 0 -1 0 5611 0 0 0 3981 14 0 0 25 0 1 0 422778635 26177536 5447 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6391 5447 603 41 0 6350 0
vsize: 25564
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 31306
Raw data (stat): 31306 (minisat+) R 31305 25347 25346 0 -1 0 5814 0 0 0 4981 15 0 0 25 0 1 0 422778635 27127808 5650 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6623 5650 603 41 0 6582 0
vsize: 26492
[startup+60.003 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 31306
Raw data (stat): 31306 (minisat+) R 31305 25347 25346 0 -1 0 7249 0 0 0 5977 19 0 0 25 0 1 0 422778635 34881536 6920 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8516 6920 603 41 0 8475 0
vsize: 34064
[startup+67.7522 s]
Raw data (loadavg): 0.95 0.95 0.91 1/53 31306
Raw data (stat): 31306 (minisat+) R 31305 25347 25346 0 -1 0 7249 0 0 0 5977 19 0 0 25 0 1 0 422778635 34881536 6920 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8516 6920 603 41 0 8475 0
vsize: 0

Child status: 30
Real time (s): 67.7519
CPU time (s): 67.7187
CPU user time (s): 67.5067
CPU system time (s): 0.211967
CPU usage (%): 99.9511
Max. virtual memory (Kb): 34064
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	66
#### END VERIFIER DATA ####