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 6270

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 04:21:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4754 boxname=wulflinc2 idbench=242 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c12951e903009dc00793ce72594cf3ba  /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-6pb.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-6pb.opb /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-6pb.opb
IDLAUNCH: 4754
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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	: 2
cpu MHz		: 451.191
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:        893624 kB
Buffers:         35592 kB
Cached:          84900 kB
SwapCached:          4 kB
Active:          57264 kB
Inactive:        66108 kB
HighTotal:      131008 kB
HighFree:        42252 kB
LowTotal:       903652 kB
LowFree:        851372 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12152 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:24:33 (client local time) WITH STATUS 30 IN 189.243 SECONDS
stats: 4754 0 189.243 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 |   13092    38312 |    4364       0        0     nan |  0.000 % |
c |       100 |   13092    38312 |    4800     100     1203    12.0 |  4.396 % |
c |       250 |   13087    38297 |    5280     203     2263    11.1 |  4.430 % |
c |       476 |   13077    38267 |    5808     380     3902    10.3 |  4.499 % |
c |       814 |   13077    38267 |    6389     718    10495    14.6 |  4.499 % |
c |      1320 |   13077    38267 |    7028    1224    26753    21.9 |  4.499 % |
c |      2080 |   13077    38267 |    7731    1984    46189    23.3 |  4.499 % |
c |      3219 |   13077    38267 |    8504    3123    86597    27.7 |  4.499 % |
c |      4928 |   13077    38267 |    9354    4832   137889    28.5 |  4.499 % |
c |      7494 |   13077    38267 |   10290    7398   211419    28.6 |  4.499 % |
c |     11339 |   13077    38267 |   11319    5970   169514    28.4 |  4.499 % |
c |     17105 |   13077    38267 |   12451    5935   179856    30.3 |  4.499 % |
c |     25754 |   13077    38267 |   13696    8121   291127    35.8 |  4.499 % |
c |     38732 |   13077    38267 |   15065    7083   269061    38.0 |  4.499 % |
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 |     49503 |   76959   187857 |   25653    9854   352052    35.7 |  4.499 % |
c |     49603 |   76959   187857 |   28218    9954   354979    35.7 |  1.933 % |
c |     49753 |   76959   187857 |   31040   10104   357060    35.3 |  1.933 % |
c |     49979 |   76959   187857 |   34144   10330   363904    35.2 |  1.933 % |
c |     50317 |   76959   187857 |   37558   10668   371848    34.9 |  1.933 % |
c |     50823 |   76959   187857 |   41314   11174   386385    34.6 |  1.933 % |
c |     51585 |   76959   187857 |   45445   11936   404642    33.9 |  1.933 % |
c |     52725 |   76959   187857 |   49990   13076   434440    33.2 |  1.933 % |
c |     54435 |   76684   187238 |   54989   14779   471368    31.9 |  2.236 % |
c |     56998 |   76684   187238 |   60488   17342   519405    30.0 |  2.236 % |
c |     60845 |   75950   185574 |   66537   21031   627334    29.8 |  3.082 % |
c ==============================================================================
c [1mFound solution: 70[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 |     65293 |   74487   182230 |   24829   25441   754340    29.7 |  3.082 % |
c |     65394 |   74487   182230 |   27311   25542   756512    29.6 |  4.868 % |
c |     65546 |   74487   182230 |   30043   25694   758684    29.5 |  4.868 % |
c |     65772 |   74487   182230 |   33047   25920   766228    29.6 |  4.868 % |
c |     66110 |   74487   182230 |   36352   26258   777660    29.6 |  4.868 % |
c |     66618 |   74487   182230 |   39987   26766   799516    29.9 |  4.868 % |
c |     67377 |   74487   182230 |   43986   27525   824573    30.0 |  4.868 % |
c |     68516 |   73391   179696 |   48384   28562   841063    29.4 |  6.209 % |
c |     70224 |   71054   174359 |   53223   30246   885241    29.3 |  9.027 % |
c |     72787 |   71046   174341 |   58545   32808   980675    29.9 |  9.035 % |
c |     76631 |   71046   174341 |   64400   36652  1104452    30.1 |  9.035 % |
c |     82400 |   71046   174341 |   70840   42421  1280574    30.2 |  9.035 % |
c |     91049 |   67869   166994 |   77924   50823  1556506    30.6 | 12.935 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26576     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99178 |  114999   277394 |   38333   54668  1594385    29.2 | 12.935 % |
c |     99278 |  111793   269927 |   42166   11480   231429    20.2 | 18.694 % |
c |     99429 |  111626   269529 |   46382   11587   234440    20.2 | 18.815 % |
c |     99655 |  111626   269529 |   51021   11813   237795    20.1 | 18.815 % |
c |     99993 |  111602   269463 |   56123   12144   242430    20.0 | 18.820 % |
c |    100499 |  111371   268952 |   61735   12647   262634    20.8 | 18.980 % |
c |    101258 |  111244   268669 |   67909   13402   278501    20.8 | 19.059 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23108     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102063 |  159143   380802 |   53047   14162   300874    21.2 | 19.059 % |
c |    102165 |  158751   379909 |   58351   14241   303468    21.3 | 15.135 % |
c |    102316 |  158636   379645 |   64186   14391   308166    21.4 | 15.189 % |
c |    102541 |  157890   377920 |   70605   14490   309053    21.3 | 15.528 % |
c |    102878 |  156670   375044 |   77666   14473   311103    21.5 | 16.056 % |
c |    103384 |  156670   375044 |   85432   14979   334198    22.3 | 16.056 % |
c |    104143 |  149693   358576 |   93975   14192   302972    21.3 | 19.286 % |
c |    105285 |  148933   356813 |  103373   12963   218774    16.9 | 19.640 % |
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              : 53
c conflicts             : 105446         (558 /sec)
c decisions             : 178159         (943 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 189.006 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.93 0.98 0.94 2/54 26572
Raw data (stat): 26572 (runsolver) R 26571 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423450688 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+10.0004 s]
Raw data (loadavg): 0.94 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 1206 0 0 0 993 4 0 0 25 0 1 0 423450688 6463488 1184 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1578 1184 603 41 0 1537 0
vsize: 6312
[startup+20.0012 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 1398 0 0 0 1992 5 0 0 25 0 1 0 423450688 7274496 1376 4294967295 134512640 134672761 3221224560 3221223744 134559553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1776 1376 603 41 0 1735 0
vsize: 7104
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 3213 0 0 0 2986 10 0 0 25 0 1 0 423450688 15056896 3122 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3676 3122 603 41 0 3635 0
vsize: 14704
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 3441 0 0 0 3986 11 0 0 25 0 1 0 423450688 16039936 3350 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3916 3350 603 41 0 3875 0
vsize: 15664
[startup+50.0023 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 3597 0 0 0 4986 11 0 0 25 0 1 0 423450688 16703488 3506 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4078 3506 603 41 0 4037 0
vsize: 16312
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 3795 0 0 0 5985 12 0 0 25 0 1 0 423450688 17575936 3704 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4291 3704 603 41 0 4250 0
vsize: 17164
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 4007 0 0 0 6984 12 0 0 25 0 1 0 423450688 18505728 3916 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4518 3916 603 41 0 4477 0
vsize: 18072
[startup+80.0034 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 4184 0 0 0 7984 13 0 0 25 0 1 0 423450688 19173376 4093 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4681 4093 603 41 0 4640 0
vsize: 18724
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 4343 0 0 0 8984 13 0 0 25 0 1 0 423450688 19853312 4252 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4847 4252 603 41 0 4806 0
vsize: 19388
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 4485 0 0 0 9983 14 0 0 25 0 1 0 423450688 20393984 4394 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4979 4394 603 41 0 4938 0
vsize: 19916
[startup+110.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 4654 0 0 0 10983 15 0 0 25 0 1 0 423450688 21061632 4563 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4563 603 41 0 5101 0
vsize: 20568
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 4731 0 0 0 11983 15 0 0 25 0 1 0 423450688 21331968 4640 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5208 4640 603 41 0 5167 0
vsize: 20832
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 4736 0 0 0 12983 15 0 0 25 0 1 0 423450688 21471232 4645 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5242 4645 603 41 0 5201 0
vsize: 20968
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 6338 0 0 0 13979 18 0 0 25 0 1 0 423450688 28454912 6156 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6947 6156 603 41 0 6906 0
vsize: 27788
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 6344 0 0 0 14980 18 0 0 25 0 1 0 423450688 28454912 6162 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6947 6162 603 41 0 6906 0
vsize: 27788
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 6746 0 0 0 15979 19 0 0 25 0 1 0 423450688 30289920 6564 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7395 6564 603 41 0 7354 0
vsize: 29580
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 6746 0 0 0 16979 19 0 0 25 0 1 0 423450688 30289920 6564 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7395 6564 603 41 0 7354 0
vsize: 29580
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 6746 0 0 0 17979 19 0 0 25 0 1 0 423450688 30289920 6564 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7395 6564 603 41 0 7354 0
vsize: 29580
[startup+189.253 s]
Raw data (loadavg): 0.99 0.98 0.94 1/53 26572
Raw data (stat): 26572 (minisat+) R 26571 20937 20936 0 -1 0 6746 0 0 0 17979 19 0 0 25 0 1 0 423450688 30289920 6564 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7395 6564 603 41 0 7354 0
vsize: 0

Child status: 30
Real time (s): 189.253
CPU time (s): 189.243
CPU user time (s): 189.032
CPU system time (s): 0.210967
CPU usage (%): 99.9951
Max. virtual memory (Kb): 29580
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	66
#### END VERIFIER DATA ####