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-5.opb
MD5SUM	00a81d808a7a59d6e11f17e19e68d826
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.04884
Number of variables	450
Total number of constraints	17794
Number of constraints which are clauses	17794
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 6335

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 04:33:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4830 boxname=wulflinc13 idbench=318 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00a81d808a7a59d6e11f17e19e68d826  /oldhome/oroussel/tmp/wulflinc13/normalized-frb30-15-5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-frb30-15-5.opb /oldhome/oroussel/tmp/wulflinc13/normalized-frb30-15-5.opb
IDLAUNCH: 4830
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890096 kB
Buffers:         35524 kB
Cached:          89136 kB
SwapCached:        392 kB
Active:          56352 kB
Inactive:        71588 kB
HighTotal:      131008 kB
HighFree:        37996 kB
LowTotal:       903652 kB
LowFree:        852100 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11100 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:37:20 (client local time) WITH STATUS 30 IN 206.123 SECONDS
stats: 4830 0 206.123 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17794 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 |   17794    35588 |    5931       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -22[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 |   51982   115697 |   17327       0        0     nan |  0.000 % |
c |       101 |   51951   115628 |   19059     100      478     4.8 |  0.120 % |
c |       251 |   51516   114649 |   20965     222     1020     4.6 |  1.127 % |
c |       477 |   50269   111817 |   23062     413     2743     6.6 |  4.208 % |
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 |       594 |   49861   111013 |   16620     506     3259     6.4 |  4.208 % |
c |       694 |   49279   109687 |   18282     582     4463     7.7 |  7.910 % |
c |       844 |   48634   108211 |   20110     714     5860     8.2 |  9.567 % |
c |      1069 |   47249   105021 |   22121     868     7601     8.8 | 13.227 % |
c |      1406 |   45657   101356 |   24333    1115    10333     9.3 | 17.427 % |
c |      1912 |   42743    94635 |   26766    1464    12804     8.7 | 25.167 % |
c |      2671 |   36860    80896 |   29443    1850    17867     9.7 | 41.207 % |
c |      3810 |   30474    65960 |   32387    2150    22813    10.6 | 59.402 % |
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 |      5251 |   26594    56837 |    8864    3117    43300    13.9 | 59.402 % |
c |      5351 |   26510    56641 |    9750    3178    45020    14.2 | 70.866 % |
c |      5501 |   26504    56627 |   10725    3327    48052    14.4 | 70.883 % |
c |      5726 |   26316    56185 |   11797    3481    50584    14.5 | 71.432 % |
c |      6065 |   26149    55796 |   12977    3738    57612    15.4 | 71.914 % |
c |      6571 |   25742    54841 |   14275    4101    71089    17.3 | 73.148 % |
c |      7331 |   25489    54245 |   15703    4781   105391    22.0 | 73.891 % |
c |      8470 |   24962    52991 |   17273    5795   142613    24.6 | 75.488 % |
c |     10178 |   24828    52678 |   19000    7459   218657    29.3 | 75.869 % |
c |     12740 |   24501    51905 |   20900    9835   362285    36.8 | 76.832 % |
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 |     13162 |   24101    50979 |    8033    9930   378012    38.1 | 76.832 % |
c |     13262 |   24101    50979 |    8836   10030   381534    38.0 | 78.242 % |
c |     13413 |   24000    50741 |    9719   10129   385184    38.0 | 78.561 % |
c |     13641 |   24000    50741 |   10691   10357   396759    38.3 | 78.561 % |
c |     13978 |   24000    50741 |   11761   10694   414584    38.8 | 78.561 % |
c |     14484 |   24000    50741 |   12937   11200   435734    38.9 | 78.561 % |
c |     15244 |   24000    50741 |   14230   11960   476531    39.8 | 78.561 % |
c |     16383 |   23960    50647 |   15654   13080   543431    41.5 | 78.678 % |
c |     18093 |   23836    50355 |   17219   14694   644668    43.9 | 79.064 % |
c |     20655 |   23814    50303 |   18941   17249   762242    44.2 | 79.131 % |
c |     24499 |   23792    50251 |   20835   21071   964337    45.8 | 79.198 % |
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 |     27490 |   23768    50180 |    7922   24012  1094104    45.6 | 79.198 % |
c |     27590 |   23768    50180 |    8714   12106   464418    38.4 | 79.261 % |
c |     27741 |   23768    50180 |    9585   12257   471086    38.4 | 79.261 % |
c |     27966 |   23768    50180 |   10544   12482   480900    38.5 | 79.261 % |
c |     28303 |   23768    50180 |   11598   12819   499507    39.0 | 79.261 % |
c |     28809 |   23738    50110 |   12758   13314   518492    38.9 | 79.344 % |
c |     29568 |   23626    49847 |   14034   14027   550678    39.3 | 79.671 % |
c |     30707 |   23563    49699 |   15437   15160   610821    40.3 | 79.864 % |
c |     32415 |   23553    49676 |   16981   16865   673514    39.9 | 79.889 % |
c |     34977 |   23250    48959 |   18679   19307   797594    41.3 | 80.812 % |
c |     38823 |   23250    48959 |   20547   23153   911834    39.4 | 80.812 % |
c |     44589 |   23240    48935 |   22602   28915  1286732    44.5 | 80.846 % |
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 |     45554 |   23268    49007 |    7756   29878  1330695    44.5 | 80.846 % |
c |     45654 |   23268    49007 |    8531   15039   581795    38.7 | 80.822 % |
c |     45804 |   23268    49007 |    9384   15189   587549    38.7 | 80.822 % |
c |     46029 |   23268    49007 |   10323   15414   594045    38.5 | 80.822 % |
c |     46366 |   23268    49007 |   11355   15751   608021    38.6 | 80.822 % |
c |     46872 |   23268    49007 |   12491   16257   626333    38.5 | 80.822 % |
c |     47631 |   23268    49007 |   13740   17016   655295    38.5 | 80.822 % |
c |     48770 |   23268    49007 |   15114   18155   685798    37.8 | 80.822 % |
c |     50478 |   23216    48886 |   16625   19860   734905    37.0 | 80.964 % |
c |     53040 |   23042    48483 |   18288   22403   806757    36.0 | 81.449 % |
c |     56885 |   22951    48266 |   20117   26220   898608    34.3 | 81.734 % |
c |     62651 |   22945    48252 |   22128   16628   390250    23.5 | 81.750 % |
c |     71301 |   22941    48243 |   24341   25277   669007    26.5 | 81.759 % |
c |     84275 |   22927    48210 |   26775   19955   545646    27.3 | 81.801 % |
c |    103736 |   22636    47557 |   29453   31724   833268    26.3 | 82.403 % |
c |    132928 |   22181    46546 |   32398   27940   630448    22.6 | 83.273 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13516     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    161667 |   27870    59905 |    9290   23136   474572    20.5 | 83.273 % |
c |    161767 |   27870    59905 |   10219   23236   476908    20.5 | 78.121 % |
c |    161917 |   27870    59905 |   11240   23386   480036    20.5 | 78.121 % |
c |    162142 |   27763    59690 |   12364   22923   468763    20.4 | 78.126 % |
c |    162479 |   27763    59690 |   13601   23260   474898    20.4 | 78.126 % |
c |    162986 |   27763    59690 |   14961   23767   484382    20.4 | 78.126 % |
c |    163745 |   27763    59690 |   16457   24526   500873    20.4 | 78.126 % |
c |    164884 |   27763    59690 |   18103   25665   526567    20.5 | 78.126 % |
c |    166592 |   27763    59690 |   19913   27373   558149    20.4 | 78.126 % |
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              : 71
c conflicts             : 168011         (816 /sec)
c decisions             : 224635         (1091 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 205.976 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 5782
Raw data (stat): 5782 (runsolver) R 5781 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423527529 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.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 1615 0 0 0 993 5 0 0 25 0 1 0 423527529 8519680 1593 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2080 1593 603 41 0 2039 0
vsize: 8320
[startup+20.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 2174 0 0 0 1990 7 0 0 25 0 1 0 423527529 10809344 2152 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2639 2152 603 41 0 2598 0
vsize: 10556
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 2702 0 0 0 2988 9 0 0 25 0 1 0 423527529 13017088 2680 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3178 2680 603 41 0 3137 0
vsize: 12712
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 2845 0 0 0 3987 9 0 0 25 0 1 0 423527529 13643776 2823 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3331 2823 603 41 0 3290 0
vsize: 13324
[startup+50.0019 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 2847 0 0 0 4987 9 0 0 25 0 1 0 423527529 13643776 2825 4294967295 134512640 134672761 3221224560 3221223696 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3331 2825 603 41 0 3290 0
vsize: 13324
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3175 0 0 0 5986 11 0 0 25 0 1 0 423527529 14962688 3153 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3153 603 41 0 3612 0
vsize: 14612
[startup+70.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3175 0 0 0 6985 11 0 0 25 0 1 0 423527529 14962688 3153 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3653 3153 603 41 0 3612 0
vsize: 14612
[startup+80.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3176 0 0 0 7985 11 0 0 25 0 1 0 423527529 14962688 3154 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3653 3154 603 41 0 3612 0
vsize: 14612
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3176 0 0 0 8985 11 0 0 25 0 1 0 423527529 14962688 3154 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3653 3154 603 41 0 3612 0
vsize: 14612
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3211 0 0 0 9985 11 0 0 25 0 1 0 423527529 15224832 3189 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3189 603 41 0 3676 0
vsize: 14868
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3211 0 0 0 10986 11 0 0 25 0 1 0 423527529 15224832 3189 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3189 603 41 0 3676 0
vsize: 14868
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3211 0 0 0 11986 11 0 0 25 0 1 0 423527529 15224832 3189 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3189 603 41 0 3676 0
vsize: 14868
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3213 0 0 0 12986 12 0 0 25 0 1 0 423527529 15224832 3191 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3191 603 41 0 3676 0
vsize: 14868
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3216 0 0 0 13986 12 0 0 25 0 1 0 423527529 15224832 3194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3194 603 41 0 3676 0
vsize: 14868
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3216 0 0 0 14986 12 0 0 25 0 1 0 423527529 15224832 3194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3194 603 41 0 3676 0
vsize: 14868
[startup+160.002 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3217 0 0 0 15986 12 0 0 25 0 1 0 423527529 15224832 3195 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3195 603 41 0 3676 0
vsize: 14868
[startup+170.002 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3217 0 0 0 16987 12 0 0 25 0 1 0 423527529 15224832 3195 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3195 603 41 0 3676 0
vsize: 14868
[startup+180.002 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3226 0 0 0 17987 12 0 0 25 0 1 0 423527529 15224832 3204 4294967295 134512640 134672761 3221224560 3221223712 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3204 603 41 0 3676 0
vsize: 14868
[startup+190.002 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3226 0 0 0 18987 12 0 0 25 0 1 0 423527529 15224832 3204 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3204 603 41 0 3676 0
vsize: 14868
[startup+200.002 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3513 0 0 0 19986 12 0 0 25 0 1 0 423527529 16613376 3489 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3489 603 41 0 4015 0
vsize: 16224
[startup+206.13 s]
Raw data (loadavg): 1.06 1.00 0.92 1/53 5782
Raw data (stat): 5782 (minisat+) R 5781 30701 30700 0 -1 0 3513 0 0 0 19986 12 0 0 25 0 1 0 423527529 16613376 3489 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3489 603 41 0 4015 0
vsize: 0

Child status: 30
Real time (s): 206.129
CPU time (s): 206.123
CPU user time (s): 205.985
CPU system time (s): 0.137979
CPU usage (%): 99.9967
Max. virtual memory (Kb): 16224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-30
#### END VERIFIER DATA ####