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/primes-dimacs-cnf/normalized-ii32a1.opb
MD5SUM	eb47f4c49e66c2bccec3237bb66dd1b2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	444
Optimality of the best value was proved	NO
Number of terms in the objective function	918
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	918
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	918
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	9.00763
Number of variables	918
Total number of constraints	9671
Number of constraints which are clauses	9671
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	32
Trace number 4690

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-13 19:50:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3530 boxname=wulflinc3 idbench=146 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  eb47f4c49e66c2bccec3237bb66dd1b2  /oldhome/oroussel/tmp/wulflinc3/normalized-ii32a1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-ii32a1.opb /oldhome/oroussel/tmp/wulflinc3/normalized-ii32a1.opb
IDLAUNCH: 3530
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        917256 kB
Buffers:         34884 kB
Cached:          59760 kB
SwapCached:       3276 kB
Active:          67348 kB
Inactive:        33452 kB
HighTotal:      131008 kB
HighFree:        67312 kB
LowTotal:       903652 kB
LowFree:        849944 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11036 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:11:00 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3530 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 9671 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 |    9671    33921 |    3223       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 444[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1824   maxlim: 474   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        35 |   22407    79408 |    7469      35     1252    35.8 |  0.000 % |
c |       135 |   22407    79408 |    8215     135     5541    41.0 |  0.255 % |
c |       288 |   22407    79408 |    9037     288    13117    45.5 |  0.255 % |
c |       513 |   22407    79408 |    9941     513    21616    42.1 |  0.255 % |
c |       850 |   22407    79408 |   10935     850    37673    44.3 |  0.255 % |
c |      1357 |   22407    79408 |   12028    1357    64685    47.7 |  0.255 % |
c |      2117 |   22407    79408 |   13231    2117    90557    42.8 |  0.255 % |
c |      3256 |   22407    79408 |   14554    3256   133709    41.1 |  0.255 % |
c |      4964 |   22407    79408 |   16010    4964   191130    38.5 |  0.255 % |
c |      7527 |   22407    79408 |   17611    7527   298043    39.6 |  0.255 % |
c |     11374 |   22407    79408 |   19372   11374   452983    39.8 |  0.255 % |
c |     17143 |   22407    79408 |   21309   17143   942287    55.0 |  0.255 % |
c |     25795 |   22397    79370 |   23440   12057  1154247    95.7 |  0.291 % |
c |     38770 |   22397    79370 |   25785   25032  2427294    97.0 |  0.291 % |
c |     58232 |   22397    79370 |   28363   15895  1787568   112.5 |  0.291 % |
c |     87424 |   22345    79250 |   31199   27647  3037691   109.9 |  0.364 % |
c |    131214 |   22345    79250 |   34319   15891  1788634   112.6 |  0.364 % |
c |    196898 |   22345    79250 |   37751   18410  2193941   119.2 |  0.364 % |
c |    295425 |   22282    79108 |   41527   20760  2418149   116.5 |  0.437 % |
c |    443214 |   22282    79108 |   45679   34405  4118505   119.7 |  0.437 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 -x47 x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 -x133 x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 -x147 x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 -x253 x254 x255 -x256 x257 -x258 x259 -x260 x261 -x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 x321 -x322 x323 -x324 x325 -x326 x327 -x328 -x329 x330 x331 -x332 x333 -x334 x335 -x336 x337 -x338 x339 -x340 x341 -x342 x343 -x344 x345 -x346 -x347 x348 x349 -x350 x351 -x352 x353 -x354 x355 -x356 -x357 x358 x359 -x360 x361 -x362 x363 -x364 x365 -x366 x367 -x368 x369 -x370 x371 -x372 x373 -x374 x375 -x376 x377 -x378 x379 -x380 x381 -x382 x383 -x384 x385 -x386 -x387 x388 -x389 x390 -x391 x392 x393 -x394 -x395 x396 x397 -x398 -x399 x400 -x401 x402 x403 -x404 -x405 x406 -x407 x408 -x409 x410 x411 -x412 -x413 x414 -x415 -x416 x417 -x418 -x419 x420 x421 -x422 -x423 x424 -x425 x426 x427 -x428 -x429 x430 -x431 x432 -x433 x434 -x435 x436 x437 -x438 x439 -x440 -x441 x442 -x443 x444 x445 -x446 -x447 x448 -x449 x450 x451 -x452 -x453 x454 -x455 x456 x457 -x458 -x459 x460 -x461 x462 x463 -x464 -x465 x466 -x467 x468 -x469 x470 x471 -x472 -x473 x474 x475 -x476 -x477 x478 -x479 x480 -x481 x482 -x483 x484 x485 -x486 x487 -x488 -x489 x490 -x491 x492 -x493 x494 -x495 x496 x497 -x498 -x499 x500 -x501 x502 x503 -x504 x505 -x506 -x507 x508 -x509 x510 x511 -x512 -x513 x514 -x515 x516 -x517 x518 x519 -x520 -x521 x522 x523 -x524 -x525 x526 -x527 x528 -x529 x530 x531 -x532 -x533 x534 x535 -x536 -x537 -x538 -x539 -x540 -x541 x542 x543 -x544 -x545 x546 x547 -x548 -x549 x550 -x551 x552 x553 -x554 -x555 x556 -x557 x558 -x559 x560 -x561 x562 x563 -x564 -x565 x566 x567 -x568 -x569 x570 x571 -x572 -x573 -x574 -x575 x576 -x577 x578 -x579 x580 x581 -x582 -x583 x584 x585 -x586 -x587 x588 -x589 x590 -x591 x592 x593 -x594 x595 -x596 -x597 x598 -x599 x600 x601 -x602 -x603 x604 -x605 -x606 x607 -x608 -x609 x610 -x611 -x612 x613 -x614 -x615 x616 -x617 x618 x619 -x620 -x621 x622 -x623 x624 x625 -x626 -x627 -x628 -x629 -x630 x631 -x632 -x633 x634 -x635 -x636 -x637 x638 x639 -x640 -x641 x642 -x643 x644 x645 -x646 -x647 x648 -x649 x650 -x651 x652 x653 -x654 x655 -x656 -x657 -x658 -x659 x660 -x661 x662 -x663 x664 x665 -x666 x667 -x668 -x669 x670 -x671 x672 -x673 x674 -x675 x676 x677 -x678 -x679 x680 x681 -x682 -x683 x684 x685 -x686 -x687 x688 -x689 x690 x691 -x692 -x693 x694 -x695 x696 x697 -x698 -x699 x700 -x701 x702 x703 -x704 -x705 x706 -x707 x708 -x709 x710 x711 -x712 -x713 x714 -x715 x716 -x717 x718 x719 -x720 x721 -x722 -x723 x724 -x725 x726 -x727 x728 x729 -x730 -x731 x732 -x733 x734 x735 -x736 -x737 x738 x739 -x740 -x741 x742 -x743 x744 x745 -x746 -x747 x748 -x749 x750 -x751 x752 -x753 x754 x755 -x#### 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.91 0.95 0.69 2/54 12957
Raw data (stat): 12957 (runsolver) R 12956 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420382070 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.0011 s]
Raw data (loadavg): 0.93 0.95 0.70 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 1416 0 0 0 994 4 0 0 25 0 1 0 420382070 7380992 1394 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1802 1394 603 41 0 1761 0
vsize: 7208
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.96 0.70 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 2322 0 0 0 1992 6 0 0 25 0 1 0 420382070 11079680 2300 4294967295 134512640 134672761 3221224576 3221223760 134559509 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2705 2300 603 41 0 2664 0
vsize: 10820
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 2828 0 0 0 2989 8 0 0 25 0 1 0 420382070 13103104 2806 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3199 2806 603 41 0 3158 0
vsize: 12796
[startup+40.0026 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 3437 0 0 0 3987 10 0 0 25 0 1 0 420382070 15650816 3415 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3821 3415 603 41 0 3780 0
vsize: 15284
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.96 0.71 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 3530 0 0 0 4987 10 0 0 25 0 1 0 420382070 16056320 3508 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3920 3508 603 41 0 3879 0
vsize: 15680
[startup+60.002 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 3741 0 0 0 5987 11 0 0 25 0 1 0 420382070 16867328 3719 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4118 3719 603 41 0 4077 0
vsize: 16472
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 3906 0 0 0 6986 11 0 0 25 0 1 0 420382070 17543168 3884 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4283 3884 603 41 0 4242 0
vsize: 17132
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 3906 0 0 0 7986 11 0 0 25 0 1 0 420382070 17543168 3884 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4283 3884 603 41 0 4242 0
vsize: 17132
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4470 0 0 0 8984 14 0 0 25 0 1 0 420382070 19836928 4448 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4843 4448 603 41 0 4802 0
vsize: 19372
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4470 0 0 0 9984 14 0 0 25 0 1 0 420382070 19836928 4448 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4843 4448 603 41 0 4802 0
vsize: 19372
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4470 0 0 0 10984 14 0 0 25 0 1 0 420382070 19836928 4448 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4843 4448 603 41 0 4802 0
vsize: 19372
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4471 0 0 0 11984 14 0 0 25 0 1 0 420382070 19836928 4449 4294967295 134512640 134672761 3221224576 3221223760 134558880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4843 4449 603 41 0 4802 0
vsize: 19372
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4471 0 0 0 12984 14 0 0 25 0 1 0 420382070 19836928 4449 4294967295 134512640 134672761 3221224576 3221223648 134553544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4843 4449 603 41 0 4802 0
vsize: 19372
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4471 0 0 0 13985 14 0 0 25 0 1 0 420382070 19836928 4449 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4843 4449 603 41 0 4802 0
vsize: 19372
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4505 0 0 0 14985 14 0 0 25 0 1 0 420382070 20099072 4483 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4483 603 41 0 4866 0
vsize: 19628
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4505 0 0 0 15985 14 0 0 25 0 1 0 420382070 20099072 4483 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4483 603 41 0 4866 0
vsize: 19628
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4505 0 0 0 16985 14 0 0 25 0 1 0 420382070 20099072 4483 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4483 603 41 0 4866 0
vsize: 19628
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 4973 0 0 0 17983 15 0 0 25 0 1 0 420382070 21987328 4951 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5368 4951 603 41 0 5327 0
vsize: 21472
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5482 0 0 0 18982 17 0 0 25 0 1 0 420382070 24137728 5460 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5893 5460 603 41 0 5852 0
vsize: 23572
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5598 0 0 0 19981 18 0 0 25 0 1 0 420382070 24539136 5576 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5576 603 41 0 5950 0
vsize: 23964
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5598 0 0 0 20981 18 0 0 25 0 1 0 420382070 24539136 5576 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5576 603 41 0 5950 0
vsize: 23964
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5600 0 0 0 21982 18 0 0 25 0 1 0 420382070 24539136 5578 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5578 603 41 0 5950 0
vsize: 23964
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5601 0 0 0 22982 18 0 0 25 0 1 0 420382070 24539136 5579 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5579 603 41 0 5950 0
vsize: 23964
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5601 0 0 0 23982 18 0 0 25 0 1 0 420382070 24539136 5579 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5579 603 41 0 5950 0
vsize: 23964
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5601 0 0 0 24982 18 0 0 25 0 1 0 420382070 24539136 5579 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5579 603 41 0 5950 0
vsize: 23964
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5601 0 0 0 25982 18 0 0 25 0 1 0 420382070 24539136 5579 4294967295 134512640 134672761 3221224576 3221223680 134559818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5991 5579 603 41 0 5950 0
vsize: 23964
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5937 0 0 0 26981 19 0 0 25 0 1 0 420382070 26013696 5915 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6351 5915 603 41 0 6310 0
vsize: 25404
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5971 0 0 0 27981 20 0 0 25 0 1 0 420382070 26148864 5949 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6384 5949 603 41 0 6343 0
vsize: 25536
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5971 0 0 0 28981 20 0 0 25 0 1 0 420382070 26148864 5949 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6384 5949 603 41 0 6343 0
vsize: 25536
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5976 0 0 0 29981 20 0 0 25 0 1 0 420382070 26148864 5954 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6384 5954 603 41 0 6343 0
vsize: 25536
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 5982 0 0 0 30982 20 0 0 25 0 1 0 420382070 26148864 5960 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6384 5960 603 41 0 6343 0
vsize: 25536
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6317 0 0 0 31980 21 0 0 25 0 1 0 420382070 27611136 6295 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6741 6295 603 41 0 6700 0
vsize: 26964
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6643 0 0 0 32980 22 0 0 25 0 1 0 420382070 28942336 6621 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6621 603 41 0 7025 0
vsize: 28264
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6643 0 0 0 33979 22 0 0 25 0 1 0 420382070 28942336 6621 4294967295 134512640 134672761 3221224576 3221223680 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7066 6621 603 41 0 7025 0
vsize: 28264
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6643 0 0 0 34978 22 0 0 25 0 1 0 420382070 28942336 6621 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7066 6621 603 41 0 7025 0
vsize: 28264
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6646 0 0 0 35978 23 0 0 25 0 1 0 420382070 28942336 6624 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6624 603 41 0 7025 0
vsize: 28264
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6647 0 0 0 36978 23 0 0 25 0 1 0 420382070 28942336 6625 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6625 603 41 0 7025 0
vsize: 28264
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6647 0 0 0 37978 23 0 0 25 0 1 0 420382070 28942336 6625 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6625 603 41 0 7025 0
vsize: 28264
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6647 0 0 0 38978 23 0 0 25 0 1 0 420382070 28942336 6625 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6625 603 41 0 7025 0
vsize: 28264
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6647 0 0 0 39978 23 0 0 25 0 1 0 420382070 28942336 6625 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6625 603 41 0 7025 0
vsize: 28264
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6647 0 0 0 40978 23 0 0 25 0 1 0 420382070 28942336 6625 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7066 6625 603 41 0 7025 0
vsize: 28264
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6674 0 0 0 41979 23 0 0 25 0 1 0 420382070 29073408 6652 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7098 6652 603 41 0 7057 0
vsize: 28392
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6858 0 0 0 42978 23 0 0 25 0 1 0 420382070 29749248 6836 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7263 6836 603 41 0 7222 0
vsize: 29052
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6858 0 0 0 43978 23 0 0 25 0 1 0 420382070 29749248 6836 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7263 6836 603 41 0 7222 0
vsize: 29052
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6858 0 0 0 44978 23 0 0 25 0 1 0 420382070 29749248 6836 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7263 6836 603 41 0 7222 0
vsize: 29052
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6863 0 0 0 45979 23 0 0 25 0 1 0 420382070 29749248 6841 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7263 6841 603 41 0 7222 0
vsize: 29052
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6864 0 0 0 46979 23 0 0 25 0 1 0 420382070 29749248 6842 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7263 6842 603 41 0 7222 0
vsize: 29052
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 6864 0 0 0 47979 23 0 0 25 0 1 0 420382070 29749248 6842 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7263 6842 603 41 0 7222 0
vsize: 29052
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7188 0 0 0 48978 24 0 0 25 0 1 0 420382070 31100928 7166 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7166 603 41 0 7552 0
vsize: 30372
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7188 0 0 0 49978 24 0 0 25 0 1 0 420382070 31100928 7166 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7166 603 41 0 7552 0
vsize: 30372
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7188 0 0 0 50978 24 0 0 25 0 1 0 420382070 31100928 7166 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7166 603 41 0 7552 0
vsize: 30372
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7188 0 0 0 51979 24 0 0 25 0 1 0 420382070 31100928 7166 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7166 603 41 0 7552 0
vsize: 30372
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7188 0 0 0 52979 24 0 0 25 0 1 0 420382070 31100928 7166 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7166 603 41 0 7552 0
vsize: 30372
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 12957
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7188 0 0 0 53979 24 0 0 25 0 1 0 420382070 31100928 7166 4294967295 134512640 134672761 3221224576 3221223680 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7166 603 41 0 7552 0
vsize: 30372
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13010
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7223 0 0 0 54973 31 0 0 25 0 1 0 420382070 31236096 7201 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7201 603 41 0 7585 0
vsize: 30504
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13010
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7223 0 0 0 55973 31 0 0 25 0 1 0 420382070 31236096 7201 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7201 603 41 0 7585 0
vsize: 30504
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13010
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7223 0 0 0 56973 31 0 0 25 0 1 0 420382070 31236096 7201 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7201 603 41 0 7585 0
vsize: 30504
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13010
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7223 0 0 0 57973 31 0 0 25 0 1 0 420382070 31236096 7201 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7201 603 41 0 7585 0
vsize: 30504
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13010
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7226 0 0 0 58973 31 0 0 25 0 1 0 420382070 31236096 7204 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7204 603 41 0 7585 0
vsize: 30504
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13010
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7226 0 0 0 59973 31 0 0 25 0 1 0 420382070 31236096 7204 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7204 603 41 0 7585 0
vsize: 30504
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13010
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7226 0 0 0 60973 31 0 0 25 0 1 0 420382070 31236096 7204 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7204 603 41 0 7585 0
vsize: 30504
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7226 0 0 0 61974 31 0 0 25 0 1 0 420382070 31236096 7204 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7204 603 41 0 7585 0
vsize: 30504
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7226 0 0 0 62974 31 0 0 25 0 1 0 420382070 31236096 7204 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7204 603 41 0 7585 0
vsize: 30504
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7227 0 0 0 63974 31 0 0 25 0 1 0 420382070 31236096 7205 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7205 603 41 0 7585 0
vsize: 30504
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7227 0 0 0 64974 31 0 0 25 0 1 0 420382070 31236096 7205 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7205 603 41 0 7585 0
vsize: 30504
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7228 0 0 0 65974 31 0 0 25 0 1 0 420382070 31236096 7206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7206 603 41 0 7585 0
vsize: 30504
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7228 0 0 0 66975 31 0 0 25 0 1 0 420382070 31236096 7206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7206 603 41 0 7585 0
vsize: 30504
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7228 0 0 0 67975 31 0 0 25 0 1 0 420382070 31236096 7206 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7206 603 41 0 7585 0
vsize: 30504
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7228 0 0 0 68975 31 0 0 25 0 1 0 420382070 31236096 7206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7206 603 41 0 7585 0
vsize: 30504
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7228 0 0 0 69975 31 0 0 25 0 1 0 420382070 31236096 7206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7206 603 41 0 7585 0
vsize: 30504
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7228 0 0 0 70975 31 0 0 25 0 1 0 420382070 31236096 7206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7206 603 41 0 7585 0
vsize: 30504
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7229 0 0 0 71976 31 0 0 25 0 1 0 420382070 31236096 7207 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7207 603 41 0 7585 0
vsize: 30504
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7239 0 0 0 72976 31 0 0 25 0 1 0 420382070 31367168 7217 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 7217 603 41 0 7617 0
vsize: 30632
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7239 0 0 0 73976 31 0 0 25 0 1 0 420382070 31367168 7217 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 7217 603 41 0 7617 0
vsize: 30632
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7244 0 0 0 74976 31 0 0 25 0 1 0 420382070 31367168 7222 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 7222 603 41 0 7617 0
vsize: 30632
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7245 0 0 0 75976 31 0 0 25 0 1 0 420382070 31367168 7223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 7223 603 41 0 7617 0
vsize: 30632
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7246 0 0 0 76976 31 0 0 25 0 1 0 420382070 31367168 7224 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 7224 603 41 0 7617 0
vsize: 30632
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7247 0 0 0 77977 31 0 0 25 0 1 0 420382070 31367168 7225 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 7225 603 41 0 7617 0
vsize: 30632
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7268 0 0 0 78977 31 0 0 25 0 1 0 420382070 31498240 7246 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7246 603 41 0 7649 0
vsize: 30760
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7268 0 0 0 79977 31 0 0 25 0 1 0 420382070 31498240 7246 4294967295 134512640 134672761 3221224576 3221223680 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7246 603 41 0 7649 0
vsize: 30760
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7268 0 0 0 80977 31 0 0 25 0 1 0 420382070 31498240 7246 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7246 603 41 0 7649 0
vsize: 30760
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7268 0 0 0 81977 31 0 0 25 0 1 0 420382070 31498240 7246 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7246 603 41 0 7649 0
vsize: 30760
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7268 0 0 0 82978 31 0 0 25 0 1 0 420382070 31498240 7246 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7246 603 41 0 7649 0
vsize: 30760
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7268 0 0 0 83978 31 0 0 25 0 1 0 420382070 31498240 7246 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7246 603 41 0 7649 0
vsize: 30760
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 13012
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7268 0 0 0 84978 31 0 0 25 0 1 0 420382070 31498240 7246 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7246 603 41 0 7649 0
vsize: 30760
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7369 0 0 0 85978 32 0 0 25 0 1 0 420382070 31899648 7347 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7788 7347 603 41 0 7747 0
vsize: 31152
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7422 0 0 0 86978 32 0 0 25 0 1 0 420382070 32165888 7400 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7400 603 41 0 7812 0
vsize: 31412
[startup+880.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7422 0 0 0 87978 32 0 0 25 0 1 0 420382070 32165888 7400 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7400 603 41 0 7812 0
vsize: 31412
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7422 0 0 0 88978 32 0 0 25 0 1 0 420382070 32165888 7400 4294967295 134512640 134672761 3221224576 3221223760 134558841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7400 603 41 0 7812 0
vsize: 31412
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7422 0 0 0 89978 32 0 0 25 0 1 0 420382070 32165888 7400 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7400 603 41 0 7812 0
vsize: 31412
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7429 0 0 0 90978 32 0 0 25 0 1 0 420382070 32165888 7407 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7407 603 41 0 7812 0
vsize: 31412
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 91978 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223680 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 92979 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 93979 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223680 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+950.036 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 94979 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 95979 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 96979 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 97979 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7432 0 0 0 98980 32 0 0 25 0 1 0 420382070 32165888 7410 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7853 7410 603 41 0 7812 0
vsize: 31412
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7517 0 0 0 99979 33 0 0 25 0 1 0 420382070 32432128 7495 4294967295 134512640 134672761 3221224576 3221223680 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7918 7495 603 41 0 7877 0
vsize: 31672
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7517 0 0 0 100979 33 0 0 25 0 1 0 420382070 32432128 7495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7918 7495 603 41 0 7877 0
vsize: 31672
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7517 0 0 0 101980 33 0 0 25 0 1 0 420382070 32432128 7495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7918 7495 603 41 0 7877 0
vsize: 31672
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7517 0 0 0 102980 33 0 0 25 0 1 0 420382070 32432128 7495 4294967295 134512640 134672761 3221224576 3221223680 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7918 7495 603 41 0 7877 0
vsize: 31672
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7522 0 0 0 103980 33 0 0 25 0 1 0 420382070 32595968 7500 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7958 7500 603 41 0 7917 0
vsize: 31832
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7522 0 0 0 104980 33 0 0 25 0 1 0 420382070 32595968 7500 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7958 7500 603 41 0 7917 0
vsize: 31832
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7522 0 0 0 105980 33 0 0 25 0 1 0 420382070 32595968 7500 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7958 7500 603 41 0 7917 0
vsize: 31832
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 7862 0 0 0 106979 35 0 0 25 0 1 0 420382070 33943552 7840 4294967295 134512640 134672761 3221224576 3221223700 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7840 603 41 0 8246 0
vsize: 33148
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 8295 0 0 0 107976 37 0 0 25 0 1 0 420382070 35692544 8273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8714 8273 603 41 0 8673 0
vsize: 34856
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 8705 0 0 0 108976 38 0 0 25 0 1 0 420382070 37437440 8683 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9140 8683 603 41 0 9099 0
vsize: 36560
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9006 0 0 0 109975 39 0 0 25 0 1 0 420382070 38662144 8984 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8984 603 41 0 9398 0
vsize: 37756
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9006 0 0 0 110976 39 0 0 25 0 1 0 420382070 38662144 8984 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8984 603 41 0 9398 0
vsize: 37756
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9006 0 0 0 111976 39 0 0 25 0 1 0 420382070 38662144 8984 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8984 603 41 0 9398 0
vsize: 37756
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9006 0 0 0 112976 39 0 0 25 0 1 0 420382070 38662144 8984 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8984 603 41 0 9398 0
vsize: 37756
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9006 0 0 0 113976 39 0 0 25 0 1 0 420382070 38662144 8984 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8984 603 41 0 9398 0
vsize: 37756
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9006 0 0 0 114976 39 0 0 25 0 1 0 420382070 38662144 8984 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8984 603 41 0 9398 0
vsize: 37756
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9006 0 0 0 115977 39 0 0 25 0 1 0 420382070 38662144 8984 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8984 603 41 0 9398 0
vsize: 37756
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9007 0 0 0 116977 39 0 0 25 0 1 0 420382070 38662144 8985 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8985 603 41 0 9398 0
vsize: 37756
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9008 0 0 0 117977 39 0 0 25 0 1 0 420382070 38662144 8986 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8986 603 41 0 9398 0
vsize: 37756
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9008 0 0 0 118977 39 0 0 25 0 1 0 420382070 38662144 8986 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8986 603 41 0 9398 0
vsize: 37756
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 13014
Raw data (stat): 12957 (minisat+) R 12956 10720 10719 0 -1 0 9263 0 0 0 119977 39 0 0 25 0 1 0 420382070 39747584 9241 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 9241 603 41 0 9663 0
vsize: 38816
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.88 1/54 13014
Raw data (stat): 12957 (minisat+) Z 12956 10720 10719 0 -1 12 9266 0 0 0 119977 41 0 0 25 0 1 0 420382070 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.19
CPU user time (s): 1199.78
CPU system time (s): 0.416936
CPU usage (%): 100.01
Max. virtual memory (Kb): 38816
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####