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-5pb.opb
MD5SUM	4ca29b1bc7e76812f7871e2b937d8a23
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	60
Optimality of the best value was proved	NO
Number of terms in the objective function	720
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	720
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	720
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.04084
Number of variables	720
Total number of constraints	2168
Number of constraints which are clauses	2144
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	30

Trace number 6263

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 04:20:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4753 boxname=wulflinc32 idbench=241 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ca29b1bc7e76812f7871e2b937d8a23  /oldhome/oroussel/tmp/wulflinc32/normalized-s4-4-3-5pb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc32/normalized-s4-4-3-5pb.opb /oldhome/oroussel/tmp/wulflinc32/normalized-s4-4-3-5pb.opb
IDLAUNCH: 4753
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        701532 kB
Buffers:         35372 kB
Cached:         186252 kB
SwapCached:       1212 kB
Active:         146276 kB
Inactive:       155648 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        701276 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25400 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:22:14 (client local time) WITH STATUS 30 IN 99.1889 SECONDS
stats: 4753 0 99.1889 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2168 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2119]---> BDD-cost:    1
c ---[2109]---> BDD-cost:    1
c ---[2099]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2083]---> BDD-cost:    1
c ---[2057]---> BDD-cost:    1
c ---[2035]---> BDD-cost:    1
c ---[2025]---> BDD-cost:    1
c ---[1976]---> BDD-cost:    1
c ---[1966]---> BDD-cost:    1
c ---[1956]---> BDD-cost:    1
c ---[1954]---> BDD-cost:    1
c ---[1940]---> BDD-cost:    1
c ---[1914]---> BDD-cost:    1
c ---[1892]---> BDD-cost:    1
c ---[1882]---> BDD-cost:    1
c ---[1864]---> BDD-cost:    1
c ---[1842]---> BDD-cost:    1
c ---[1816]---> BDD-cost:    1
c ---[1810]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1765]---> BDD-cost:    1
c ---[1739]---> BDD-cost:    1
c ---[1733]---> BDD-cost:    1
c ---[1715]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    1
c ---[1667]---> BDD-cost:    1
c ---[1630]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1602]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1563]---> BDD-cost:    1
c ---[1537]---> BDD-cost:    1
c ---[1535]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1488]---> BDD-cost:    1
c ---[1466]---> BDD-cost:    1
c ---[1460]---> BDD-cost:    1
c ---[1454]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1426]---> BDD-cost:    1
c ---[1409]---> BDD-cost:    1
c ---[1383]---> BDD-cost:    1
c ---[1377]---> BDD-cost:    1
c ---[1359]---> BDD-cost:    1
c ---[1322]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1298]---> BDD-cost:    1
c ---[1272]---> BDD-cost:    1
c ---[1250]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1222]---> BDD-cost:    1
c ---[1200]---> BDD-cost:    1
c ---[1174]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1158]---> BDD-cost:    1
c ---[1148]---> BDD-cost:    1
c ---[1098]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1047]---> BDD-cost:    1
c ---[1037]---> BDD-cost:    1
c ---[1027]---> BDD-cost:    1
c ---[1025]---> BDD-cost:    1
c ---[1023]---> BDD-cost:    1
c ---[ 997]---> BDD-cost:    1
c ---[ 979]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:    1
c ---[ 914]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 864]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 804]---> BDD-cost:    1
c ---[ 786]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 721]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 654]---> BDD-cost:    1
c ---[ 629]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 564]---> BDD-cost:    1
c ---[ 538]---> BDD-cost:    1
c ---[ 536]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:    1
c ---[ 467]---> BDD-cost:    1
c ---[ 457]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:    1
c ---[ 437]---> BDD-cost:    1
c ---[ 415]---> BDD-cost:    1
c ---[ 389]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:    1
c ---[ 337]---> BDD-cost:    1
c ---[ 311]---> BDD-cost:    1
c ---[ 305]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15392    45024 |    5130       0        0     nan |  0.000 % |
c |       100 |   15392    45024 |    5643     100     1980    19.8 |  4.225 % |
c |       251 |   15392    45024 |    6207     251     5813    23.2 |  4.225 % |
c |       477 |   15392    45024 |    6828     477    11629    24.4 |  4.226 % |
c |       814 |   15392    45024 |    7510     814    18602    22.9 |  4.225 % |
c |      1321 |   15392    45024 |    8261    1321    31263    23.7 |  4.225 % |
c |      2080 |   15387    45009 |    9088    1984    46305    23.3 |  4.255 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:33028     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3152 |   90406   220591 |   30135    3056    90635    29.7 |  4.255 % |
c |      3252 |   90406   220591 |   33148    3156    93565    29.6 |  1.003 % |
c |      3403 |   90406   220591 |   36463    3307    97809    29.6 |  1.003 % |
c |      3630 |   90406   220591 |   40109    3534   104680    29.6 |  1.003 % |
c |      3967 |   90406   220591 |   44120    3871   113385    29.3 |  1.003 % |
c |      4474 |   90124   219954 |   48532    4350   122329    28.1 |  1.285 % |
c |      5234 |   89751   219105 |   53385    5090   161491    31.7 |  1.659 % |
c |      6375 |   89619   218807 |   58724    6227   208792    33.5 |  1.780 % |
c |      8085 |   88959   217315 |   64597    7869   265134    33.7 |  2.433 % |
c |     10648 |   88959   217315 |   71056   10432   421284    40.4 |  2.433 % |
c |     14492 |   88959   217315 |   78162   14276   583141    40.8 |  2.433 % |
c |     20261 |   86997   212827 |   85978   19961   790604    39.6 |  4.399 % |
c |     28911 |   84729   207625 |   94576   28451  1050831    36.9 |  6.754 % |
c |     41885 |   80426   197671 |  104034   41124  1340402    32.6 | 11.239 % |
c ==============================================================================
c [1mFound solution: 66[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 |     45813 |   77203   190175 |   25734   44292  1393405    31.5 | 11.239 % |
c |     45914 |   77203   190175 |   28307   13277   262583    19.8 | 14.646 % |
c |     46064 |   77199   190166 |   31138   13424   264815    19.7 | 14.653 % |
c |     46291 |   77195   190157 |   34251   13647   268600    19.7 | 14.653 % |
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 |     46327 |   60197   150685 |   20065   13292   262129    19.7 | 14.653 % |
c |     46427 |   60197   150685 |   22071   13392   264302    19.7 | 34.467 % |
c ==============================================================================
c [1mFound solution: 62[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 |     46520 |   59498   148955 |   19832   12276   233162    19.0 | 34.467 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:20932     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46530 |   91300   222871 |   30433   12282   233282    19.0 | 34.467 % |
c ==============================================================================
c [1mOptimal solution: 60[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 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v660 -v661 v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672 -v673 -v674 v675 -v676 -v677 -v678 -v679 -v680 -v681 -v682 -v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 -v705 v706 -v707 -v708 -v709 -v710 -v711 -v712 -v713 -v714 -v715 -v716 -v717 -v718 -v719 -v720
c _______________________________________________________________________________
c 
c restarts              : 29
c conflicts             : 46549          (470 /sec)
c decisions             : 88293          (892 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 99.0299 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.92 0.97 0.91 2/53 15379
Raw data (stat): 15379 (runsolver) R 15378 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481660748 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 3102 0 0 0 991 6 0 0 25 0 1 0 481660748 14954496 3026 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3651 3026 603 41 0 3610 0
vsize: 14604
[startup+20.0028 s]
Raw data (loadavg): 0.94 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 3465 0 0 0 1982 7 0 0 25 0 1 0 481660748 16547840 3389 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4040 3389 603 41 0 3999 0
vsize: 16160
[startup+30.0034 s]
Raw data (loadavg): 0.95 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 3658 0 0 0 2981 8 0 0 25 0 1 0 481660748 17313792 3582 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4227 3582 603 41 0 4186 0
vsize: 16908
[startup+40.0045 s]
Raw data (loadavg): 0.96 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 3908 0 0 0 3981 9 0 0 25 0 1 0 481660748 18251776 3832 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4456 3832 603 41 0 4415 0
vsize: 17824
[startup+50.0059 s]
Raw data (loadavg): 0.96 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 4137 0 0 0 4979 9 0 0 25 0 1 0 481660748 19197952 4061 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4687 4061 603 41 0 4646 0
vsize: 18748
[startup+60.0067 s]
Raw data (loadavg): 0.97 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 4338 0 0 0 5979 9 0 0 25 0 1 0 481660748 20131840 4262 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4915 4262 603 41 0 4874 0
vsize: 19660
[startup+70.0074 s]
Raw data (loadavg): 0.97 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 4470 0 0 0 6979 10 0 0 25 0 1 0 481660748 20672512 4394 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5047 4394 603 41 0 5006 0
vsize: 20188
[startup+80.0083 s]
Raw data (loadavg): 0.98 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 4492 0 0 0 7979 10 0 0 25 0 1 0 481660748 20807680 4416 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5080 4416 603 41 0 5039 0
vsize: 20320
[startup+90.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/53 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 4517 0 0 0 8979 10 0 0 25 0 1 0 481660748 20807680 4441 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5080 4441 603 41 0 5039 0
vsize: 20320
[startup+99.2977 s]
Raw data (loadavg): 0.98 0.97 0.91 1/52 15379
Raw data (stat): 15379 (minisat+) R 15378 7987 7986 0 -1 0 4517 0 0 0 8979 10 0 0 25 0 1 0 481660748 20807680 4441 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5080 4441 603 41 0 5039 0
vsize: 0

Child status: 30
Real time (s): 99.2967
CPU time (s): 99.1889
CPU user time (s): 99.0509
CPU system time (s): 0.137979
CPU usage (%): 99.8915
Max. virtual memory (Kb): 20320
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	60
#### END VERIFIER DATA ####