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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/een/normalized-seymour.opb
MD5SUM23a177449585151350479e80b33e6416
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 353
Optimality of the best value was proved NO
Number of terms in the objective function 1372
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 1372
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1372
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.04984
Number of variables1255
Total number of constraints4827
Number of constraints which are clauses4827
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint19

Trace number 6929 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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:        802020 kB
Buffers:         36368 kB
Cached:         156180 kB
SwapCached:       2476 kB
Active:          71396 kB
Inactive:       126492 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        801768 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29228 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:50:08 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 5002 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4827 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 |    4827    33432 |    1609       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 349
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2732   maxlim: 1023   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23831   101272 |    7943       0        0     nan |  0.000 % |
c |       100 |   23831   101272 |    8737     100      354     3.5 |  0.073 % |
c |       251 |   23831   101272 |    9611     251      932     3.7 |  0.073 % |
c |       476 |   23831   101272 |   10572     476     1765     3.7 |  0.073 % |
c |       813 |   23831   101272 |   11629     813     2963     3.6 |  0.073 % |
c |      1320 |   23831   101272 |   12792    1320     5657     4.3 |  0.073 % |
c |      2079 |   23831   101272 |   14071    2079     9114     4.4 |  0.073 % |
c |      3218 |   23831   101272 |   15478    3218    18259     5.7 |  0.073 % |
c |      4926 |   23831   101272 |   17026    4926    76883    15.6 |  0.073 % |
c |      7488 |   23831   101272 |   18729    7488   154097    20.6 |  0.073 % |
c |     11333 |   23831   101272 |   20602   11333   460451    40.6 |  0.073 % |
c |     17099 |   23831   101272 |   22662   17099   726024    42.5 |  0.073 % |
c |     25748 |   23831   101272 |   24928   13689   965141    70.5 |  0.073 % |
c |     38723 |   23831   101272 |   27421   13203  1329834   100.7 |  0.073 % |
c |     58184 |   23831   101272 |   30163   17319  1652707    95.4 |  0.073 % |
c |     87377 |   23831   101272 |   33179   28603  3759993   131.5 |  0.073 % |
c |    131166 |   23831   101272 |   36497   31562  4307001   136.5 |  0.073 % |
c |    196851 |   23831   101272 |   40147   27445  3084247   112.4 |  0.073 % |
c |    295378 |   23831   101272 |   44162   22833  3912189   171.3 |  0.073 % |
c |    443169 |   23831   101272 |   48578   19995  3346480   167.4 |  0.073 % |
c |    664854 |   23831   101272 |   53436   37012  5872496   158.7 |  0.073 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 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 -x7#### 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.08 0.02 0.01 2/54 5009
Raw data (stat): 5009 (runsolver) R 5008 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487487899 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.29 0.06 0.02 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 1933 0 0 0 992 4 0 0 25 0 1 0 487487899 9695232 1911 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2367 1911 603 41 0 2326 0
vsize: 9468
[startup+20.0018 s]
Raw data (loadavg): 0.40 0.10 0.03 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 2745 0 0 0 1990 6 0 0 25 0 1 0 487487899 12914688 2723 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3153 2723 603 41 0 3112 0
vsize: 12612
[startup+30.0025 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 3424 0 0 0 2988 8 0 0 25 0 1 0 487487899 15740928 3402 4294967295 134512640 134672761 3221224560 3221223744 134558324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3402 603 41 0 3802 0
vsize: 15372
[startup+40.0031 s]
Raw data (loadavg): 0.57 0.15 0.05 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 4172 0 0 0 3986 10 0 0 25 0 1 0 487487899 18825216 4150 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4596 4150 603 41 0 4555 0
vsize: 18384
[startup+50.0041 s]
Raw data (loadavg): 0.64 0.18 0.06 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 4172 0 0 0 4986 11 0 0 25 0 1 0 487487899 18825216 4150 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4596 4150 603 41 0 4555 0
vsize: 18384
[startup+60.0045 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 4703 0 0 0 5984 12 0 0 25 0 1 0 487487899 20975616 4681 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5121 4681 603 41 0 5080 0
vsize: 20484
[startup+70.0052 s]
Raw data (loadavg): 0.74 0.23 0.08 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 4703 0 0 0 6984 13 0 0 25 0 1 0 487487899 20975616 4681 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5121 4681 603 41 0 5080 0
vsize: 20484
[startup+80.0059 s]
Raw data (loadavg): 0.78 0.26 0.09 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 5577 0 0 0 7981 16 0 0 25 0 1 0 487487899 24604672 5555 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6007 5555 603 41 0 5966 0
vsize: 24028
[startup+90.0065 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 5656 0 0 0 8980 17 0 0 25 0 1 0 487487899 25010176 5634 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6106 5634 603 41 0 6065 0
vsize: 24424
[startup+100.007 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 5656 0 0 0 9980 17 0 0 25 0 1 0 487487899 25010176 5634 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6106 5634 603 41 0 6065 0
vsize: 24424
[startup+110.008 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 5657 0 0 0 10979 18 0 0 25 0 1 0 487487899 25010176 5635 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6106 5635 603 41 0 6065 0
vsize: 24424
[startup+120.008 s]
Raw data (loadavg): 0.89 0.35 0.12 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 5657 0 0 0 11979 18 0 0 25 0 1 0 487487899 25010176 5635 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6106 5635 603 41 0 6065 0
vsize: 24424
[startup+130.008 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6189 0 0 0 12978 19 0 0 25 0 1 0 487487899 27164672 6167 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6632 6167 603 41 0 6591 0
vsize: 26528
[startup+140.009 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6623 0 0 0 13977 20 0 0 25 0 1 0 487487899 28917760 6601 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6601 603 41 0 7019 0
vsize: 28240
[startup+150.01 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6623 0 0 0 14977 21 0 0 25 0 1 0 487487899 28917760 6601 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6601 603 41 0 7019 0
vsize: 28240
[startup+160.01 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6623 0 0 0 15977 21 0 0 25 0 1 0 487487899 28917760 6601 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6601 603 41 0 7019 0
vsize: 28240
[startup+170.011 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6623 0 0 0 16977 21 0 0 25 0 1 0 487487899 28917760 6601 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6601 603 41 0 7019 0
vsize: 28240
[startup+180.012 s]
Raw data (loadavg): 0.96 0.46 0.18 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6623 0 0 0 17976 21 0 0 25 0 1 0 487487899 28917760 6601 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6601 603 41 0 7019 0
vsize: 28240
[startup+190.012 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6623 0 0 0 18976 22 0 0 25 0 1 0 487487899 28917760 6601 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6601 603 41 0 7019 0
vsize: 28240
[startup+200.013 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6623 0 0 0 19976 22 0 0 25 0 1 0 487487899 28917760 6601 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6601 603 41 0 7019 0
vsize: 28240
[startup+210.013 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6626 0 0 0 20976 22 0 0 25 0 1 0 487487899 28917760 6604 4294967295 134512640 134672761 3221224560 3221223664 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6604 603 41 0 7019 0
vsize: 28240
[startup+220.013 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6626 0 0 0 21975 23 0 0 25 0 1 0 487487899 28917760 6604 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6604 603 41 0 7019 0
vsize: 28240
[startup+230.013 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6626 0 0 0 22975 23 0 0 25 0 1 0 487487899 28917760 6604 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6604 603 41 0 7019 0
vsize: 28240
[startup+240.014 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 6626 0 0 0 23975 23 0 0 25 0 1 0 487487899 28917760 6604 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7060 6604 603 41 0 7019 0
vsize: 28240
[startup+250.014 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7098 0 0 0 24974 24 0 0 25 0 1 0 487487899 30801920 7076 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7520 7076 603 41 0 7479 0
vsize: 30080
[startup+260.015 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7296 0 0 0 25973 26 0 0 25 0 1 0 487487899 31744000 7274 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7750 7274 603 41 0 7709 0
vsize: 31000
[startup+270.016 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7296 0 0 0 26972 26 0 0 25 0 1 0 487487899 31744000 7274 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7750 7274 603 41 0 7709 0
vsize: 31000
[startup+280.015 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7296 0 0 0 27972 26 0 0 25 0 1 0 487487899 31744000 7274 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7750 7274 603 41 0 7709 0
vsize: 31000
[startup+290.016 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7474 0 0 0 28972 27 0 0 25 0 1 0 487487899 32419840 7452 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7452 603 41 0 7874 0
vsize: 31660
[startup+300.017 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7474 0 0 0 29972 27 0 0 25 0 1 0 487487899 32419840 7452 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7452 603 41 0 7874 0
vsize: 31660
[startup+310.016 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7474 0 0 0 30971 27 0 0 25 0 1 0 487487899 32419840 7452 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7915 7452 603 41 0 7874 0
vsize: 31660
[startup+320.017 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 7602 0 0 0 31971 28 0 0 25 0 1 0 487487899 32956416 7580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8046 7580 603 41 0 8005 0
vsize: 32184
[startup+330.018 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 8449 0 0 0 32969 30 0 0 25 0 1 0 487487899 36450304 8427 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8899 8427 603 41 0 8858 0
vsize: 35596
[startup+340.018 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9201 0 0 0 33966 33 0 0 25 0 1 0 487487899 39534592 9179 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9652 9179 603 41 0 9611 0
vsize: 38608
[startup+350.019 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9201 0 0 0 34965 34 0 0 25 0 1 0 487487899 39534592 9179 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9652 9179 603 41 0 9611 0
vsize: 38608
[startup+360.02 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9201 0 0 0 35965 34 0 0 25 0 1 0 487487899 39534592 9179 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9652 9179 603 41 0 9611 0
vsize: 38608
[startup+370.02 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9201 0 0 0 36965 35 0 0 25 0 1 0 487487899 39534592 9179 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9652 9179 603 41 0 9611 0
vsize: 38608
[startup+380.02 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9203 0 0 0 37964 35 0 0 25 0 1 0 487487899 39534592 9181 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9652 9181 603 41 0 9611 0
vsize: 38608
[startup+390.021 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 38964 35 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+400.021 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 39964 36 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+410.021 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 40964 36 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+420.022 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 41964 36 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+430.022 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 42964 37 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+440.023 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 43963 37 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+450.024 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 44963 38 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223664 134560474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+460.024 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 45962 38 0 0 25 0 1 0 487487899 39518208 9183 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 9183 603 41 0 9607 0
vsize: 38592
[startup+470.024 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 46962 39 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223664 134555130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+480.025 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 47962 39 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223664 134554926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+490.026 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 48962 39 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+500.026 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 49961 40 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+510.026 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 50961 40 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+520.025 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 51962 40 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+530.025 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 52962 40 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+540.026 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 53962 40 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+550.025 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9205 0 0 0 54962 40 0 0 25 0 1 0 487487899 39497728 9183 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9183 603 41 0 9602 0
vsize: 38572
[startup+560.025 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 9402 0 0 0 55962 40 0 0 25 0 1 0 487487899 40308736 9380 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9841 9380 603 41 0 9800 0
vsize: 39364
[startup+570.026 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10196 0 0 0 56960 42 0 0 25 0 1 0 487487899 43515904 10174 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10624 10174 603 41 0 10583 0
vsize: 42496
[startup+580.025 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10532 0 0 0 57959 43 0 0 25 0 1 0 487487899 44990464 10510 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10510 603 41 0 10943 0
vsize: 43936
[startup+590.026 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10532 0 0 0 58959 43 0 0 25 0 1 0 487487899 44990464 10510 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10510 603 41 0 10943 0
vsize: 43936
[startup+600.027 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10532 0 0 0 59959 43 0 0 25 0 1 0 487487899 44990464 10510 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10510 603 41 0 10943 0
vsize: 43936
[startup+610.026 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10533 0 0 0 60959 43 0 0 25 0 1 0 487487899 44990464 10511 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10511 603 41 0 10943 0
vsize: 43936
[startup+620.026 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10537 0 0 0 61960 43 0 0 25 0 1 0 487487899 44990464 10515 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10515 603 41 0 10943 0
vsize: 43936
[startup+630.026 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10537 0 0 0 62960 43 0 0 25 0 1 0 487487899 44990464 10515 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10515 603 41 0 10943 0
vsize: 43936
[startup+640.026 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10537 0 0 0 63960 43 0 0 25 0 1 0 487487899 44990464 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10515 603 41 0 10943 0
vsize: 43936
[startup+650.026 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10537 0 0 0 64960 43 0 0 25 0 1 0 487487899 44990464 10515 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10515 603 41 0 10943 0
vsize: 43936
[startup+660.026 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10537 0 0 0 65960 43 0 0 25 0 1 0 487487899 44990464 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10515 603 41 0 10943 0
vsize: 43936
[startup+670.027 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10537 0 0 0 66961 43 0 0 25 0 1 0 487487899 44990464 10515 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10515 603 41 0 10943 0
vsize: 43936
[startup+680.026 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 10537 0 0 0 67961 43 0 0 25 0 1 0 487487899 44990464 10515 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10984 10515 603 41 0 10943 0
vsize: 43936
[startup+690.027 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11152 0 0 0 68959 45 0 0 25 0 1 0 487487899 47534080 11130 4294967295 134512640 134672761 3221224560 3221223664 134559802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11605 11130 603 41 0 11564 0
vsize: 46420
[startup+700.028 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11266 0 0 0 69959 45 0 0 25 0 1 0 487487899 47939584 11244 4294967295 134512640 134672761 3221224560 3221223728 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 11244 603 41 0 11663 0
vsize: 46816
[startup+710.027 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11266 0 0 0 70959 45 0 0 25 0 1 0 487487899 47939584 11244 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 11244 603 41 0 11663 0
vsize: 46816
[startup+720.028 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11266 0 0 0 71959 45 0 0 25 0 1 0 487487899 47939584 11244 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 11244 603 41 0 11663 0
vsize: 46816
[startup+730.028 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11266 0 0 0 72960 45 0 0 25 0 1 0 487487899 47939584 11244 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 11244 603 41 0 11663 0
vsize: 46816
[startup+740.028 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11266 0 0 0 73960 45 0 0 25 0 1 0 487487899 47939584 11244 4294967295 134512640 134672761 3221224560 3221223480 1075351254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 11244 603 41 0 11663 0
vsize: 46816
[startup+750.028 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11266 0 0 0 74960 45 0 0 25 0 1 0 487487899 47939584 11244 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 11244 603 41 0 11663 0
vsize: 46816
[startup+760.028 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11266 0 0 0 75960 45 0 0 25 0 1 0 487487899 47939584 11244 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11704 11244 603 41 0 11663 0
vsize: 46816
[startup+770.029 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 11497 0 0 0 76960 46 0 0 25 0 1 0 487487899 48881664 11475 4294967295 134512640 134672761 3221224560 3221223632 134553557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11934 11475 603 41 0 11893 0
vsize: 47736
[startup+780.028 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12228 0 0 0 77958 48 0 0 25 0 1 0 487487899 51843072 12206 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12657 12206 603 41 0 12616 0
vsize: 50628
[startup+790.029 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12382 0 0 0 78957 48 0 0 25 0 1 0 487487899 52514816 12360 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12360 603 41 0 12780 0
vsize: 51284
[startup+800.028 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12382 0 0 0 79958 48 0 0 25 0 1 0 487487899 52514816 12360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12360 603 41 0 12780 0
vsize: 51284
[startup+810.028 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 80958 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+820.028 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 81958 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+830.028 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 82958 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+840.028 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 83958 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+850.028 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 84958 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+860.027 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 85959 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+870.028 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 86959 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+880.028 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 87959 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+890.029 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 88959 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+900.029 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 89959 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+910.029 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 90960 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+920.029 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 91960 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+930.028 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 92960 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+940.029 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 93960 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+950.03 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 94960 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+960.029 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 95961 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+970.03 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 96961 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+980.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 97961 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+990.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 98961 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 99961 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 100961 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 101962 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 102962 48 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 103962 49 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12383 0 0 0 104961 49 0 0 25 0 1 0 487487899 52514816 12361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12361 603 41 0 12780 0
vsize: 51284
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 105960 49 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 106960 50 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 107960 50 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 108959 51 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 109959 51 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 110959 51 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 111959 52 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 112958 52 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 113958 52 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 114958 53 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 115958 53 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 116958 53 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 117958 53 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 118958 53 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 5009
Raw data (stat): 5009 (minisat+) R 5008 22612 22611 0 -1 0 12388 0 0 0 119957 54 0 0 25 0 1 0 487487899 52514816 12366 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 12366 603 41 0 12780 0
vsize: 51284
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 5009
Raw data (stat): 5009 (minisat+) Z 5008 22612 22611 0 -1 12 12391 0 0 0 119957 56 0 0 25 0 1 0 487487899 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.15
CPU user time (s): 1199.58
CPU system time (s): 0.566913
CPU usage (%): 100.007
Max. virtual memory (Kb): 51284
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####