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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-3.opb
MD5SUM	063fe125a766c5e46d0ecbf211fd8049
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
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	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04584
Number of variables	450
Total number of constraints	17809
Number of constraints which are clauses	17809
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6334

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 04:33:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4828 boxname=wulflinc18 idbench=316 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  063fe125a766c5e46d0ecbf211fd8049  /oldhome/oroussel/tmp/wulflinc18/normalized-frb30-15-3.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc18/normalized-frb30-15-3.opb /oldhome/oroussel/tmp/wulflinc18/normalized-frb30-15-3.opb
IDLAUNCH: 4828
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        852792 kB
Buffers:         35416 kB
Cached:         109852 kB
SwapCached:        320 kB
Active:          57084 kB
Inactive:        91412 kB
HighTotal:      131008 kB
HighFree:        17192 kB
LowTotal:       903652 kB
LowFree:        835600 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27788 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:36:29 (client local time) WITH STATUS 30 IN 192.528 SECONDS
stats: 4828 0 192.528 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17809 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17809    35618 |    5936       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   52280   116379 |   17426       0        0     nan |  0.000 % |
c |       101 |   52280   116379 |   19168     101     1736    17.2 |  0.010 % |
c |       251 |   51115   113738 |   21085     211     2723    12.9 |  2.840 % |
c |       476 |   49707   110525 |   23194     392     4005    10.2 |  6.389 % |
c |       813 |   47325   105056 |   25513     606     6608    10.9 | 12.667 % |
c |      1320 |   44460    98485 |   28064     986    10301    10.4 | 20.361 % |
c |      2079 |   38849    85452 |   30871    1439    15277    10.6 | 35.461 % |
c |      3218 |   33604    73205 |   33958    1996    25900    13.0 | 50.272 % |
c |      4927 |   29038    62487 |   37354    3100    40965    13.2 | 63.549 % |
c ==============================================================================
c [1mFound solution: -24[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 |      5632 |   27635    59181 |    9211    3551    55385    15.6 | 63.549 % |
c |      5732 |   27585    59064 |   10132    3638    57172    15.7 | 67.714 % |
c |      5882 |   26722    57025 |   11145    3517    55967    15.9 | 70.247 % |
c |      6107 |   26656    56867 |   12259    3714    62311    16.8 | 70.451 % |
c |      6444 |   26650    56853 |   13485    4035    73752    18.3 | 70.468 % |
c |      6950 |   26290    56004 |   14834    4409    95523    21.7 | 71.578 % |
c ==============================================================================
c [1mFound solution: -25[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 |      7028 |   26257    55945 |    8752    4414    95367    21.6 | 71.578 % |
c |      7128 |   26196    55804 |    9627    4502    97072    21.6 | 71.964 % |
c |      7278 |   25886    55083 |   10589    4508    99511    22.1 | 72.851 % |
c |      7503 |   25886    55083 |   11648    4733   107688    22.8 | 72.851 % |
c |      7840 |   25823    54940 |   12813    5047   118250    23.4 | 73.003 % |
c |      8346 |   25670    54579 |   14095    5503   136711    24.8 | 73.477 % |
c |      9105 |   25407    53959 |   15504    6105   168463    27.6 | 74.288 % |
c |     10244 |   25311    53734 |   17055    7195   220941    30.7 | 74.559 % |
c |     11952 |   24593    52057 |   18760    8558   304888    35.6 | 76.663 % |
c |     14514 |   24372    51536 |   20636   10830   484660    44.8 | 77.339 % |
c ==============================================================================
c [1mFound solution: -26[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 |     18026 |   23809    50195 |    7936   13943   724165    51.9 | 77.339 % |
c |     18127 |   23799    50172 |    8729   13990   728031    52.0 | 79.067 % |
c |     18278 |   23799    50172 |    9602   14141   734355    51.9 | 79.067 % |
c |     18504 |   23799    50172 |   10562   14367   744975    51.9 | 79.067 % |
c |     18843 |   23799    50172 |   11619   14706   767615    52.2 | 79.067 % |
c |     19349 |   23799    50172 |   12781   15212   800383    52.6 | 79.067 % |
c |     20110 |   23799    50172 |   14059   15973   829385    51.9 | 79.067 % |
c |     21249 |   23725    49997 |   15465   17014   890885    52.4 | 79.295 % |
c |     22958 |   23375    49177 |   17011   18239   980874    53.8 | 80.327 % |
c |     25521 |   23369    49163 |   18712   20798  1147677    55.2 | 80.343 % |
c |     29366 |   23369    49163 |   20583   24643  1419984    57.6 | 80.343 % |
c |     35132 |   23361    49144 |   22642   30403  1787725    58.8 | 80.369 % |
c ==============================================================================
c [1mFound solution: -27[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 |     38265 |   23412    49272 |    7804   15314   749436    48.9 | 80.369 % |
c |     38365 |   23248    48893 |    8584   15398   752618    48.9 | 80.847 % |
c |     38516 |   23248    48893 |    9442   15549   760110    48.9 | 80.847 % |
c |     38743 |   23248    48893 |   10387   15776   773515    49.0 | 80.847 % |
c |     39080 |   23248    48893 |   11425   16113   793331    49.2 | 80.847 % |
c |     39586 |   23248    48893 |   12568   16619   812198    48.9 | 80.847 % |
c |     40345 |   23242    48879 |   13825   17376   844544    48.6 | 80.864 % |
c |     41484 |   23242    48879 |   15207   18515   915998    49.5 | 80.864 % |
c |     43193 |   23238    48870 |   16728   20221  1018200    50.4 | 80.873 % |
c |     45756 |   23238    48870 |   18401   22784  1198841    52.6 | 80.873 % |
c ==============================================================================
c [1mFound solution: -28[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 |     46735 |   23194    48754 |    7731   23755  1247668    52.5 | 80.873 % |
c |     46835 |   23194    48754 |    8504   11978   518490    43.3 | 81.002 % |
c |     46986 |   23194    48754 |    9354   12129   526251    43.4 | 81.002 % |
c |     47211 |   23180    48721 |   10289   12350   537339    43.5 | 81.043 % |
c |     47548 |   23180    48721 |   11318   12687   556673    43.9 | 81.044 % |
c |     48055 |   22979    48253 |   12450   13073   573288    43.9 | 81.631 % |
c |     48814 |   22979    48253 |   13695   13832   607099    43.9 | 81.631 % |
c |     49953 |   22979    48253 |   15065   14971   662899    44.3 | 81.631 % |
c |     51661 |   22842    47930 |   16572   16317   724275    44.4 | 82.075 % |
c |     54223 |   22842    47930 |   18229   18879   847007    44.9 | 82.075 % |
c |     58068 |   22838    47921 |   20052   22667   975130    43.0 | 82.084 % |
c |     63834 |   22838    47921 |   22057   28433  1306243    45.9 | 82.084 % |
c |     72483 |   22812    47859 |   24263   20574   878043    42.7 | 82.167 % |
c |     85457 |   22812    47859 |   26689   33548  1524295    45.4 | 82.168 % |
c ==============================================================================
c [1mFound solution: -29[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 |     92309 |   22772    47765 |    7590   19807   717479    36.2 | 82.168 % |
c |     92410 |   22772    47765 |    8349   10005   270817    27.1 | 82.350 % |
c |     92560 |   22772    47765 |    9183   10155   276353    27.2 | 82.350 % |
c |     92785 |   22760    47736 |   10102   10375   285978    27.6 | 82.392 % |
c |     93122 |   22760    47736 |   11112   10712   291903    27.3 | 82.392 % |
c |     93628 |   22760    47736 |   12223   11218   309258    27.6 | 82.392 % |
c |     94387 |   22760    47736 |   13446   11977   344944    28.8 | 82.392 % |
c |     95526 |   22748    47707 |   14790   13114   393156    30.0 | 82.434 % |
c |     97234 |   22748    47707 |   16269   14822   445640    30.1 | 82.434 % |
c |     99796 |   22740    47688 |   17896   17383   527272    30.3 | 82.459 % |
c |    103641 |   22740    47688 |   19686   21228   615492    29.0 | 82.459 % |
c |    109407 |   22740    47688 |   21655   26994   762221    28.2 | 82.459 % |
c |    118056 |   22702    47599 |   23820   19592   479563    24.5 | 82.568 % |
c |    131030 |   22672    47529 |   26202   32557   853168    26.2 | 82.651 % |
c |    150491 |   22658    47496 |   28823   32808   916987    28.0 | 82.693 % |
c ==============================================================================
c [1mFound solution: -30[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 |    150669 |   22629    47406 |    7543   32984   922482    28.0 | 82.693 % |
c |    150770 |   22629    47406 |    8297   16593   419719    25.3 | 82.780 % |
c |    150921 |   22629    47406 |    9127   16744   423827    25.3 | 82.780 % |
c |    151146 |   22629    47406 |   10039   16969   431125    25.4 | 82.780 % |
c |    151484 |   22629    47406 |   11043   17307   440763    25.5 | 82.780 % |
c |    151990 |   22629    47406 |   12148   17813   454437    25.5 | 82.780 % |
c |    152750 |   22629    47406 |   13362   18573   475419    25.6 | 82.780 % |
c |    153890 |   22629    47406 |   14699   19713   504505    25.6 | 82.780 % |
c |    155598 |   21777    45674 |   16169   15631   365212    23.4 | 83.014 % |
c ==============================================================================
c [1mOptimal solution: -30[0m
s OPTIMUM FOUND
v C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 C422 -C421 -C420 -C419 -C418 -C417 C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 C321 -C320 -C319 -C318 -C317 -C316 -C315 C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 C271 -C270 -C269 -C268 -C267 C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 C197 -C196 -C195 -C194 -C193 -C192 C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 -C83 -C82 -C81 C80 -C79 -C78 -C77 -C76 -C75 -C74 -C73 -C72 -C71 -C70 -C69 -C68 -C67 -C66 -C65 -C64 -C63 C62 -C61 -C60 -C59 -C58 -C57 -C56 -C55 -C54 -C53 -C52 C51 -C50 -C49 -C48 -C47 -C46 -C45 -C44 -C43 -C42 -C41 -C40 -C39 -C38 -C37 -C36 -C35 -C34 -C33 C32 -C31 -C30 -C29 -C28 -C27 -C26 C25 -C24 -C23 -C22 -C21 -C20 -C19 -C18 -C17 -C16 -C15 -C14 -C13 C12 -C11 -C10 -C9 -C8 -C7 -C6 -C5 -C4 -C3 -C2 -C1
c _______________________________________________________________________________
c 
c restarts              : 86
c conflicts             : 156411         (813 /sec)
c decisions             : 218714         (1137 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 192.346 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.66 0.89 0.90 2/55 30090
Raw data (stat): 30090 (runsolver) R 30089 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481733903 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0002 s]
Raw data (loadavg): 0.72 0.90 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 1592 0 0 0 995 4 0 0 25 0 1 0 481733903 8400896 1570 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2051 1570 603 41 0 2010 0
vsize: 8204
[startup+20 s]
Raw data (loadavg): 0.76 0.90 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 2266 0 0 0 1992 6 0 0 25 0 1 0 481733903 11231232 2244 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2244 603 41 0 2701 0
vsize: 10968
[startup+30.0013 s]
Raw data (loadavg): 0.80 0.90 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 2854 0 0 0 2991 8 0 0 25 0 1 0 481733903 13737984 2832 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3354 2832 603 41 0 3313 0
vsize: 13416
[startup+40.0022 s]
Raw data (loadavg): 0.83 0.91 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3403 0 0 0 3988 11 0 0 25 0 1 0 481733903 15876096 3381 4294967295 134512640 134672761 3221224560 3221223664 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3876 3381 603 41 0 3835 0
vsize: 15504
[startup+50.0027 s]
Raw data (loadavg): 0.85 0.91 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3755 0 0 0 4987 12 0 0 25 0 1 0 481733903 17469440 3733 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3733 603 41 0 4224 0
vsize: 17060
[startup+60.0031 s]
Raw data (loadavg): 0.87 0.91 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3755 0 0 0 5986 13 0 0 25 0 1 0 481733903 17469440 3733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3733 603 41 0 4224 0
vsize: 17060
[startup+70.004 s]
Raw data (loadavg): 0.89 0.91 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3755 0 0 0 6986 13 0 0 25 0 1 0 481733903 17469440 3733 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3733 603 41 0 4224 0
vsize: 17060
[startup+80.0045 s]
Raw data (loadavg): 0.91 0.92 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3755 0 0 0 7986 13 0 0 25 0 1 0 481733903 17469440 3733 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3733 603 41 0 4224 0
vsize: 17060
[startup+90.0048 s]
Raw data (loadavg): 0.92 0.92 0.90 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3755 0 0 0 8986 14 0 0 25 0 1 0 481733903 17469440 3733 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3733 603 41 0 4224 0
vsize: 17060
[startup+100.006 s]
Raw data (loadavg): 0.93 0.92 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3755 0 0 0 9986 14 0 0 25 0 1 0 481733903 17469440 3733 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3733 603 41 0 4224 0
vsize: 17060
[startup+110.006 s]
Raw data (loadavg): 0.94 0.92 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3755 0 0 0 10985 14 0 0 25 0 1 0 481733903 17469440 3733 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3733 603 41 0 4224 0
vsize: 17060
[startup+120.007 s]
Raw data (loadavg): 0.95 0.92 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3759 0 0 0 11985 15 0 0 25 0 1 0 481733903 17469440 3737 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3737 603 41 0 4224 0
vsize: 17060
[startup+130.007 s]
Raw data (loadavg): 0.96 0.93 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3760 0 0 0 12985 15 0 0 25 0 1 0 481733903 17469440 3738 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3738 603 41 0 4224 0
vsize: 17060
[startup+140.008 s]
Raw data (loadavg): 0.96 0.93 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3760 0 0 0 13985 15 0 0 25 0 1 0 481733903 17469440 3738 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3738 603 41 0 4224 0
vsize: 17060
[startup+150.009 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3760 0 0 0 14985 15 0 0 25 0 1 0 481733903 17469440 3738 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3738 603 41 0 4224 0
vsize: 17060
[startup+160.01 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3760 0 0 0 15985 15 0 0 25 0 1 0 481733903 17469440 3738 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3738 603 41 0 4224 0
vsize: 17060
[startup+170.01 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3763 0 0 0 16985 15 0 0 25 0 1 0 481733903 17469440 3741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3741 603 41 0 4224 0
vsize: 17060
[startup+180.011 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3763 0 0 0 17985 16 0 0 25 0 1 0 481733903 17469440 3741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3741 603 41 0 4224 0
vsize: 17060
[startup+190.012 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3763 0 0 0 18985 16 0 0 25 0 1 0 481733903 17469440 3741 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3741 603 41 0 4224 0
vsize: 17060
[startup+192.525 s]
Raw data (loadavg): 0.98 0.94 0.91 1/54 30090
Raw data (stat): 30090 (minisat+) R 30089 20024 20023 0 -1 0 3763 0 0 0 18985 16 0 0 25 0 1 0 481733903 17469440 3741 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3741 603 41 0 4224 0
vsize: 0

Child status: 30
Real time (s): 192.524
CPU time (s): 192.528
CPU user time (s): 192.353
CPU system time (s): 0.174973
CPU usage (%): 100.002
Max. virtual memory (Kb): 17060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-30
#### END VERIFIER DATA ####