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-3pb.opb
MD5SUM	c267b57d74142f6538ad16680277f9bf
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	62
Optimality of the best value was proved	NO
Number of terms in the objective function	648
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	648
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	648
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.02984
Number of variables	648
Total number of constraints	1954
Number of constraints which are clauses	1930
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	27

Trace number 6260

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 04:18:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4751 boxname=wulflinc21 idbench=239 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c267b57d74142f6538ad16680277f9bf  /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-3pb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-3pb.opb /oldhome/oroussel/tmp/wulflinc21/normalized-s4-4-3-3pb.opb
IDLAUNCH: 4751
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        872992 kB
Buffers:         28752 kB
Cached:         112824 kB
SwapCached:          0 kB
Active:          46276 kB
Inactive:        98232 kB
HighTotal:      131008 kB
HighFree:        14924 kB
LowTotal:       903652 kB
LowFree:        858068 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11640 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:21:35 (client local time) WITH STATUS 30 IN 172.248 SECONDS
stats: 4751 0 172.248 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1954 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[1944]---> BDD-cost:    1
c ---[1934]---> BDD-cost:    1
c ---[1885]---> BDD-cost:    1
c ---[1883]---> BDD-cost:    1
c ---[1869]---> BDD-cost:    1
c ---[1843]---> BDD-cost:    1
c ---[1821]---> BDD-cost:    1
c ---[1811]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1752]---> 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 ---[1654]---> BDD-cost:    1
c ---[1628]---> BDD-cost:    1
c ---[1606]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1594]---> BDD-cost:    1
c ---[1568]---> BDD-cost:    1
c ---[1550]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1507]---> BDD-cost:    1
c ---[1485]---> BDD-cost:    1
c ---[1459]---> BDD-cost:    1
c ---[1453]---> BDD-cost:    1
c ---[1435]---> BDD-cost:    1
c ---[1413]---> BDD-cost:    1
c ---[1387]---> BDD-cost:    1
c ---[1381]---> BDD-cost:    1
c ---[1333]---> BDD-cost:    1
c ---[1323]---> BDD-cost:    1
c ---[1313]---> BDD-cost:    1
c ---[1311]---> BDD-cost:    1
c ---[1258]---> BDD-cost:    1
c ---[1248]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1203]---> BDD-cost:    1
c ---[1181]---> BDD-cost:    1
c ---[1175]---> BDD-cost:    1
c ---[1169]---> BDD-cost:    1
c ---[1167]---> BDD-cost:    1
c ---[1141]---> BDD-cost:    1
c ---[1123]---> BDD-cost:    1
c ---[1097]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1038]---> BDD-cost:    1
c ---[1032]---> BDD-cost:    1
c ---[1026]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[ 998]---> BDD-cost:    1
c ---[ 980]---> BDD-cost:    1
c ---[ 954]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 926]---> BDD-cost:    1
c ---[ 908]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 868]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 792]---> BDD-cost:    1
c ---[ 771]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 722]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 658]---> BDD-cost:    1
c ---[ 648]---> BDD-cost:    1
c ---[ 598]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 586]---> BDD-cost:    1
c ---[ 576]---> 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 ---[ 400]---> BDD-cost:    1
c ---[ 390]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 382]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 362]---> 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 ---[ 236]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   95
c ---[  22]---> BDD-cost:   95
c ---[  21]---> BDD-cost:   95
c ---[  20]---> BDD-cost:   95
c ---[  19]---> BDD-cost:   95
c ---[  18]---> BDD-cost:   95
c ---[  17]---> BDD-cost:   95
c ---[  16]---> BDD-cost:   95
c ---[  15]---> BDD-cost:   95
c ---[  14]---> BDD-cost:   95
c ---[  13]---> BDD-cost:   95
c ---[  12]---> BDD-cost:   95
c ---[  11]---> BDD-cost:   95
c ---[  10]---> BDD-cost:   95
c ---[   9]---> BDD-cost:   95
c ---[   8]---> BDD-cost:   95
c ---[   7]---> BDD-cost:   95
c ---[   6]---> BDD-cost:   95
c ---[   5]---> BDD-cost:   95
c ---[   4]---> BDD-cost:   95
c ---[   3]---> BDD-cost:   95
c ---[   2]---> BDD-cost:   95
c ---[   1]---> BDD-cost:   95
c ---[   0]---> BDD-cost:   95
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13666    39972 |    4555       0        0     nan |  0.000 % |
c |       100 |   13666    39972 |    5010     100     1410    14.1 |  4.348 % |
c |       251 |   13666    39972 |    5511     251     6623    26.4 |  4.348 % |
c |       477 |   13666    39972 |    6062     477    11211    23.5 |  4.348 % |
c |       814 |   13666    39972 |    6668     814    19623    24.1 |  4.348 % |
c |      1320 |   13666    39972 |    7335    1320    32098    24.3 |  4.348 % |
c |      2080 |   13666    39972 |    8069    2080    52605    25.3 |  4.348 % |
c |      3222 |   13666    39972 |    8876    3222    73390    22.8 |  4.348 % |
c |      4930 |   13666    39972 |    9764    4930   122417    24.8 |  4.348 % |
c |      7492 |   13666    39972 |   10740    7492   203535    27.2 |  4.348 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29320     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10020 |   80876   197277 |   26958   10020   271073    27.1 |  4.348 % |
c |     10122 |   80876   197277 |   29653   10122   274661    27.1 |  0.571 % |
c |     10272 |   80876   197277 |   32619   10272   279830    27.2 |  0.571 % |
c |     10497 |   80876   197277 |   35881   10497   286820    27.3 |  0.571 % |
c |     10834 |   80876   197277 |   39469   10834   297658    27.5 |  0.571 % |
c |     11342 |   80876   197277 |   43416   11342   313694    27.7 |  0.571 % |
c |     12101 |   80079   195474 |   47757   12064   325827    27.0 |  1.451 % |
c |     13240 |   80021   195344 |   52533   13201   375412    28.4 |  1.515 % |
c |     14949 |   79547   194257 |   57786   14903   427362    28.7 |  2.046 % |
c |     17511 |   79498   194147 |   63565   17464   514423    29.5 |  2.098 % |
c |     21357 |   79498   194147 |   69922   21310   694787    32.6 |  2.098 % |
c |     27123 |   79167   193395 |   76914   27045   853318    31.6 |  2.467 % |
c |     35773 |   79023   193067 |   84605   35693  1121643    31.4 |  2.629 % |
c |     48748 |   76877   188159 |   93066   48301  1505607    31.2 |  5.084 % |
c |     68209 |   76695   187741 |  102372   67760  2145316    31.7 |  5.290 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76241 |   59360   147542 |   19786   68736  2084017    30.3 |  5.290 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9464     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76294 |   70764   174159 |   23588   14362   264958    18.4 |  5.290 % |
c ==============================================================================
c [1mOptimal solution: 62[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 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 -v648
c _______________________________________________________________________________
c 
c restarts              : 27
c conflicts             : 76304          (444 /sec)
c decisions             : 125795         (731 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 172.037 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.85 0.97 0.93 2/55 5249
Raw data (stat): 5249 (runsolver) R 5248 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358917311 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99954 s]
Raw data (loadavg): 0.87 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 3035 0 0 0 991 7 0 0 25 0 1 0 358917311 14303232 2955 4294967295 134512640 134672761 3221224560 3221223696 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3492 2955 603 41 0 3451 0
vsize: 13968
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 3414 0 0 0 1990 8 0 0 25 0 1 0 358917311 15810560 3334 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3860 3334 603 41 0 3819 0
vsize: 15440
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 3686 0 0 0 2989 10 0 0 25 0 1 0 358917311 17014784 3606 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4154 3606 603 41 0 4113 0
vsize: 16616
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 3939 0 0 0 3988 11 0 0 25 0 1 0 358917311 18120704 3859 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3859 603 41 0 4383 0
vsize: 17696
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 4124 0 0 0 4987 12 0 0 25 0 1 0 358917311 18952192 4044 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4627 4044 603 41 0 4586 0
vsize: 18508
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 4261 0 0 0 5987 12 0 0 25 0 1 0 358917311 19492864 4181 4294967295 134512640 134672761 3221224560 3221223664 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4759 4181 603 41 0 4718 0
vsize: 19036
[startup+70.0016 s]
Raw data (loadavg): 0.95 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 4444 0 0 0 6986 13 0 0 25 0 1 0 358917311 20209664 4364 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4364 603 41 0 4893 0
vsize: 19736
[startup+80.0023 s]
Raw data (loadavg): 0.96 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 4612 0 0 0 7981 14 0 0 25 0 1 0 358917311 20873216 4532 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5096 4532 603 41 0 5055 0
vsize: 20384
[startup+90.002 s]
Raw data (loadavg): 0.96 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 4780 0 0 0 8981 14 0 0 25 0 1 0 358917311 21544960 4700 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5260 4700 603 41 0 5219 0
vsize: 21040
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 4928 0 0 0 9980 15 0 0 25 0 1 0 358917311 22204416 4848 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5421 4848 603 41 0 5380 0
vsize: 21684
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5087 0 0 0 10979 16 0 0 25 0 1 0 358917311 22888448 5007 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5588 5007 603 41 0 5547 0
vsize: 22352
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5262 0 0 0 11979 16 0 0 25 0 1 0 358917311 23552000 5182 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5750 5182 603 41 0 5709 0
vsize: 23000
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5433 0 0 0 12979 17 0 0 25 0 1 0 358917311 24653824 5353 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6019 5353 603 41 0 5978 0
vsize: 24076
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5535 0 0 0 13978 17 0 0 25 0 1 0 358917311 25075712 5455 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6122 5455 603 41 0 6081 0
vsize: 24488
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5560 0 0 0 14978 17 0 0 25 0 1 0 358917311 25075712 5480 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6122 5480 603 41 0 6081 0
vsize: 24488
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5573 0 0 0 15978 17 0 0 25 0 1 0 358917311 25214976 5493 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6156 5493 603 41 0 6115 0
vsize: 24624
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5701 0 0 0 16978 18 0 0 25 0 1 0 358917311 26210304 5621 4294967295 134512640 134672761 3221224560 3221222464 134565819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5621 603 41 0 6358 0
vsize: 25596
[startup+172.284 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 5249
Raw data (stat): 5249 (minisat+) R 5248 30927 30926 0 -1 0 5701 0 0 0 16978 18 0 0 25 0 1 0 358917311 26210304 5621 4294967295 134512640 134672761 3221224560 3221222464 134565819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6399 5621 603 41 0 6358 0
vsize: 0

Child status: 30
Real time (s): 172.284
CPU time (s): 172.248
CPU user time (s): 172.051
CPU system time (s): 0.19697
CPU usage (%): 99.9791
Max. virtual memory (Kb): 25596
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	62
#### END VERIFIER DATA ####