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).
    Note that some very long lines in this section may be truncated by your web browser !
  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

Namesubmitted/een/normalized-seymour.opb
MD5SUM23a177449585151350479e80b33e6416
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 343
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 benchmark1195.02
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 2274

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916376 kB
Buffers:         35304 kB
Cached:          48308 kB
SwapCached:        844 kB
Active:          66492 kB
Inactive:        19708 kB
HighTotal:      131008 kB
HighFree:        79828 kB
LowTotal:       903652 kB
LowFree:        836548 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26612 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:50:38 (client local time) WITH STATUS 10 IN 1207.87 SECONDS
stats: 2632 7 1207.87 10

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 ---[   0]---> Sorter-cost:76410     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   98923   253123 |   32974       0        0     nan |  0.000 % |
c |       100 |   97075   249222 |   36271      53      306     5.8 |  1.611 % |
c |       250 |   96306   247533 |   39898     182     1434     7.9 |  2.335 % |
c |       475 |   94983   244630 |   43888     352     2733     7.8 |  3.580 % |
c |       813 |   93755   241908 |   48277     659     6082     9.2 |  4.756 % |
c |      1319 |   92568   239259 |   53104    1107    10103     9.1 |  5.908 % |
c |      2079 |   91909   237778 |   58415    1848    16788     9.1 |  6.556 % |
c |      3218 |   91411   236662 |   64256    2962    28061     9.5 |  7.042 % |
c |      4926 |   90331   234236 |   70682    4606    53966    11.7 |  8.078 % |
c |      7488 |   90120   233759 |   77750    7151    98759    13.8 |  8.279 % |
c |     11332 |   89899   233266 |   85526   10979   176068    16.0 |  8.478 % |
c |     17098 |   89285   231884 |   94078   16657   308712    18.5 |  9.049 % |
c |     25749 |   89112   231493 |  103486   25255   976019    38.6 |  9.212 % |
c |     38723 |   89001   231242 |  113835   38209  1772808    46.4 |  9.316 % |
c |     58184 |   88950   231133 |  125218   57664  4775966    82.8 |  9.357 % |
c |     87378 |   88942   231115 |  137740   86849  9904394   114.0 |  9.365 % |
c |    131169 |   88746   230668 |  151514  130531 13442173   103.0 |  9.548 % |
c |    196853 |   88719   230611 |  166666   44042  6107081   138.7 |  9.572 % |
c |    295379 |   88664   230490 |  183332  142564 10444974    73.3 |  9.624 % |
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

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/5347/stat): 5347 (minisat+_script) R 5346 5347 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843394801 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5347/statm): 174 3 169 147 0 27 0
[pid=5347] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=5348
New process pid=5349
New process pid=5350
execve syscall for /bin/sed executable
One traced child (pid=5349) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=5350) exited with status: 0
One traced child (pid=5348) exited with status: 0
New process pid=5351
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-seymour.opb

[startup+10.0037 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 4789 0 0 0 958 20 0 0 25 0 1 0 1843394806 21204992 4751 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 5177 4751 145 145 0 5032 0
[pid=5351] vsize: 20708
Current children cumulated CPU time (s) 9.79
Current children cumulated vsize (Kb) 22832

[startup+20.0046 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 4941 0 0 0 1955 21 0 0 25 0 1 0 1843394806 21778432 4903 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 5317 4903 145 145 0 5172 0
[pid=5351] vsize: 21268
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 23392

[startup+30.0056 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5174 0 0 0 2951 23 0 0 25 0 1 0 1843394806 22740992 5136 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 5552 5136 145 145 0 5407 0
[pid=5351] vsize: 22208
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 24332

[startup+40.0065 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5391 0 0 0 3948 24 0 0 25 0 1 0 1843394806 23658496 5353 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 5776 5353 145 145 0 5631 0
[pid=5351] vsize: 23104
Current children cumulated CPU time (s) 39.73
Current children cumulated vsize (Kb) 25228

[startup+50.0074 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5742 0 0 0 4942 27 0 0 25 0 1 0 1843394806 25079808 5704 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 6123 5704 145 145 0 5978 0
[pid=5351] vsize: 24492
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 26616

[startup+60.0083 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5974 0 0 0 5938 29 0 0 25 0 1 0 1843394806 26025984 5936 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 6354 5936 145 145 0 6209 0
[pid=5351] vsize: 25416
Current children cumulated CPU time (s) 59.68
Current children cumulated vsize (Kb) 27540

[startup+70.0093 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 6246 0 0 0 6932 32 0 0 25 0 1 0 1843394806 27119616 6208 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 6621 6208 145 145 0 6476 0
[pid=5351] vsize: 26484
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 28608

[startup+80.0102 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 6528 0 0 0 7926 34 0 0 25 0 1 0 1843394806 28274688 6490 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 6903 6490 145 145 0 6758 0
[pid=5351] vsize: 27612
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 29736

[startup+90.0111 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 6952 0 0 0 8919 36 0 0 25 0 1 0 1843394806 30117888 6914 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 7353 6914 145 145 0 7208 0
[pid=5351] vsize: 29412
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 31536

[startup+100.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 7276 0 0 0 9912 39 0 0 25 0 1 0 1843394806 31428608 7238 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 7673 7238 145 145 0 7528 0
[pid=5351] vsize: 30692
Current children cumulated CPU time (s) 99.52
Current children cumulated vsize (Kb) 32816

[startup+110.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 7581 0 0 0 10905 43 0 0 25 0 1 0 1843394806 32669696 7543 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 7976 7543 145 145 0 7831 0
[pid=5351] vsize: 31904
Current children cumulated CPU time (s) 109.49
Current children cumulated vsize (Kb) 34028

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 7925 0 0 0 11899 45 0 0 25 0 1 0 1843394806 34070528 7887 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 8318 7887 145 145 0 8173 0
[pid=5351] vsize: 33272
Current children cumulated CPU time (s) 119.45
Current children cumulated vsize (Kb) 35396

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 8270 0 0 0 12892 48 0 0 25 0 1 0 1843394806 35479552 8232 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 8662 8232 145 145 0 8517 0
[pid=5351] vsize: 34648
Current children cumulated CPU time (s) 129.41
Current children cumulated vsize (Kb) 36772

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 8628 0 0 0 13887 50 0 0 25 0 1 0 1843394806 36937728 8590 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 9018 8590 145 145 0 8873 0
[pid=5351] vsize: 36072
Current children cumulated CPU time (s) 139.38
Current children cumulated vsize (Kb) 38196

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 9006 0 0 0 14880 53 0 0 25 0 1 0 1843394806 38481920 8968 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 9395 8968 145 145 0 9250 0
[pid=5351] vsize: 37580
Current children cumulated CPU time (s) 149.34
Current children cumulated vsize (Kb) 39704

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 9348 0 0 0 15874 56 0 0 25 0 1 0 1843394806 39866368 9310 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 9733 9310 145 145 0 9588 0
[pid=5351] vsize: 38932
Current children cumulated CPU time (s) 159.31
Current children cumulated vsize (Kb) 41056

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 9707 0 0 0 16867 59 0 0 25 0 1 0 1843394806 41332736 9669 4294967295 134512640 135094434 3221224448 3221223040 134551711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 10091 9669 145 145 0 9946 0
[pid=5351] vsize: 40364
Current children cumulated CPU time (s) 169.27
Current children cumulated vsize (Kb) 42488

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 10064 0 0 0 17861 63 0 0 25 0 1 0 1843394806 42799104 10026 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 10449 10026 145 145 0 10304 0
[pid=5351] vsize: 41796
Current children cumulated CPU time (s) 179.25
Current children cumulated vsize (Kb) 43920

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 10351 0 0 0 18855 65 0 0 25 0 1 0 1843394806 43962368 10313 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 10733 10313 145 145 0 10588 0
[pid=5351] vsize: 42932
Current children cumulated CPU time (s) 189.21
Current children cumulated vsize (Kb) 45056

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 10864 0 0 0 19845 69 0 0 25 0 1 0 1843394806 46309376 10826 4294967295 134512640 135094434 3221224448 3221223040 134557178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 11306 10826 145 145 0 11161 0
[pid=5351] vsize: 45224
Current children cumulated CPU time (s) 199.15
Current children cumulated vsize (Kb) 47348

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 11462 0 0 0 20833 74 0 0 25 0 1 0 1843394806 48754688 11424 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 11903 11424 145 145 0 11758 0
[pid=5351] vsize: 47612
Current children cumulated CPU time (s) 209.08
Current children cumulated vsize (Kb) 49736

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 12037 0 0 0 21822 78 0 0 25 0 1 0 1843394806 51105792 11999 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 12477 11999 145 145 0 12332 0
[pid=5351] vsize: 49908
Current children cumulated CPU time (s) 219.01
Current children cumulated vsize (Kb) 52032

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 12567 0 0 0 22813 82 0 0 25 0 1 0 1843394806 53260288 12529 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 13003 12529 145 145 0 12858 0
[pid=5351] vsize: 52012
Current children cumulated CPU time (s) 228.96
Current children cumulated vsize (Kb) 54136

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 13109 0 0 0 23802 86 0 0 25 0 1 0 1843394806 55468032 13071 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 13542 13071 145 145 0 13397 0
[pid=5351] vsize: 54168
Current children cumulated CPU time (s) 238.89
Current children cumulated vsize (Kb) 56292

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 13656 0 0 0 24793 91 0 0 25 0 1 0 1843394806 57700352 13618 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 14087 13618 145 145 0 13942 0
[pid=5351] vsize: 56348
Current children cumulated CPU time (s) 248.85
Current children cumulated vsize (Kb) 58472

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 14144 0 0 0 25784 95 0 0 25 0 1 0 1843394806 59707392 14106 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 14577 14106 145 145 0 14432 0
[pid=5351] vsize: 58308
Current children cumulated CPU time (s) 258.8
Current children cumulated vsize (Kb) 60432

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 14627 0 0 0 26775 99 0 0 25 0 1 0 1843394806 61685760 14589 4294967295 134512640 135094434 3221224448 3221223100 134558036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 15060 14589 145 145 0 14915 0
[pid=5351] vsize: 60240
Current children cumulated CPU time (s) 268.75
Current children cumulated vsize (Kb) 62364

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 15075 0 0 0 27768 101 0 0 25 0 1 0 1843394806 63545344 15037 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 15514 15037 145 145 0 15369 0
[pid=5351] vsize: 62056
Current children cumulated CPU time (s) 278.7
Current children cumulated vsize (Kb) 64180

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 15485 0 0 0 28760 105 0 0 25 0 1 0 1843394806 65228800 15447 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 15925 15447 145 145 0 15780 0
[pid=5351] vsize: 63700
Current children cumulated CPU time (s) 288.66
Current children cumulated vsize (Kb) 65824

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 15679 0 0 0 29757 106 0 0 25 0 1 0 1843394806 66011136 15641 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 16116 15641 145 145 0 15971 0
[pid=5351] vsize: 64464
Current children cumulated CPU time (s) 298.64
Current children cumulated vsize (Kb) 66588

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16044 0 0 0 30750 109 0 0 25 0 1 0 1843394806 67497984 16006 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 16479 16006 145 145 0 16334 0
[pid=5351] vsize: 65916
Current children cumulated CPU time (s) 308.6
Current children cumulated vsize (Kb) 68040

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16393 0 0 0 31743 111 0 0 25 0 1 0 1843394806 68915200 16355 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 16825 16355 145 145 0 16680 0
[pid=5351] vsize: 67300
Current children cumulated CPU time (s) 318.55
Current children cumulated vsize (Kb) 69424

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16704 0 0 0 32738 113 0 0 25 0 1 0 1843394806 70168576 16666 4294967295 134512640 135094434 3221224448 3221223104 134558289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 17131 16666 145 145 0 16986 0
[pid=5351] vsize: 68524
Current children cumulated CPU time (s) 328.52
Current children cumulated vsize (Kb) 70648

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16841 0 0 0 33736 114 0 0 25 0 1 0 1843394806 70721536 16803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 17266 16803 145 145 0 17121 0
[pid=5351] vsize: 69064
Current children cumulated CPU time (s) 338.51
Current children cumulated vsize (Kb) 71188

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16979 0 0 0 34732 116 0 0 25 0 1 0 1843394806 71290880 16941 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 17405 16941 145 145 0 17260 0
[pid=5351] vsize: 69620
Current children cumulated CPU time (s) 348.49
Current children cumulated vsize (Kb) 71744

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 17198 0 0 0 35728 117 0 0 25 0 1 0 1843394806 72171520 17160 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 17620 17160 145 145 0 17475 0
[pid=5351] vsize: 70480
Current children cumulated CPU time (s) 358.46
Current children cumulated vsize (Kb) 72604

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 17592 0 0 0 36721 120 0 0 25 0 1 0 1843394806 73777152 17554 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 18012 17554 145 145 0 17867 0
[pid=5351] vsize: 72048
Current children cumulated CPU time (s) 368.42
Current children cumulated vsize (Kb) 74172

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 18007 0 0 0 37712 124 0 0 25 0 1 0 1843394806 75472896 17969 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 18426 17969 145 145 0 18281 0
[pid=5351] vsize: 73704
Current children cumulated CPU time (s) 378.37
Current children cumulated vsize (Kb) 75828

[startup+390.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 18412 0 0 0 38704 128 0 0 25 0 1 0 1843394806 77123584 18374 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 18829 18374 145 145 0 18684 0
[pid=5351] vsize: 75316
Current children cumulated CPU time (s) 388.33
Current children cumulated vsize (Kb) 77440

[startup+400.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 18736 0 0 0 39697 130 0 0 25 0 1 0 1843394806 78442496 18698 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 19151 18698 145 145 0 19006 0
[pid=5351] vsize: 76604
Current children cumulated CPU time (s) 398.28
Current children cumulated vsize (Kb) 78728

[startup+410.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19064 0 0 0 40692 132 0 0 25 0 1 0 1843394806 79761408 19026 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 19473 19026 145 145 0 19328 0
[pid=5351] vsize: 77892
Current children cumulated CPU time (s) 408.25
Current children cumulated vsize (Kb) 80016

[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19415 0 0 0 41685 135 0 0 25 0 1 0 1843394806 81182720 19377 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 19820 19377 145 145 0 19675 0
[pid=5351] vsize: 79280
Current children cumulated CPU time (s) 418.21
Current children cumulated vsize (Kb) 81404

[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19593 0 0 0 42681 136 0 0 25 0 1 0 1843394806 82427904 19555 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 20124 19555 145 145 0 19979 0
[pid=5351] vsize: 80496
Current children cumulated CPU time (s) 428.18
Current children cumulated vsize (Kb) 82620

[startup+440.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19754 0 0 0 43678 137 0 0 25 0 1 0 1843394806 83079168 19716 4294967295 134512640 135094434 3221224448 3221223088 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 20283 19716 145 145 0 20138 0
[pid=5351] vsize: 81132
Current children cumulated CPU time (s) 438.16
Current children cumulated vsize (Kb) 83256

[startup+450.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 20041 0 0 0 44672 140 0 0 25 0 1 0 1843394806 84242432 20003 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 20567 20003 145 145 0 20422 0
[pid=5351] vsize: 82268
Current children cumulated CPU time (s) 448.13
Current children cumulated vsize (Kb) 84392

[startup+460.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 20380 0 0 0 45666 142 0 0 25 0 1 0 1843394806 85618688 20342 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 20903 20342 145 145 0 20758 0
[pid=5351] vsize: 83612
Current children cumulated CPU time (s) 458.09
Current children cumulated vsize (Kb) 85736

[startup+470.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 20759 0 0 0 46658 146 0 0 25 0 1 0 1843394806 87162880 20721 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 21280 20721 145 145 0 21135 0
[pid=5351] vsize: 85120
Current children cumulated CPU time (s) 468.05
Current children cumulated vsize (Kb) 87244

[startup+480.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 21166 0 0 0 47652 148 0 0 25 0 1 0 1843394806 88825856 21128 4294967295 134512640 135094434 3221224448 3221223040 134557221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 21686 21128 145 145 0 21541 0
[pid=5351] vsize: 86744
Current children cumulated CPU time (s) 478.01
Current children cumulated vsize (Kb) 88868

[startup+490.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 21515 0 0 0 48645 151 0 0 25 0 1 0 1843394806 90243072 21477 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 22032 21477 145 145 0 21887 0
[pid=5351] vsize: 88128
Current children cumulated CPU time (s) 487.97
Current children cumulated vsize (Kb) 90252

[startup+500.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 21865 0 0 0 49640 153 0 0 25 0 1 0 1843394806 91668480 21827 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 22380 21827 145 145 0 22235 0
[pid=5351] vsize: 89520
Current children cumulated CPU time (s) 497.94
Current children cumulated vsize (Kb) 91644

[startup+510.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 22204 0 0 0 50635 154 0 0 25 0 1 0 1843394806 93048832 22166 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 22717 22166 145 145 0 22572 0
[pid=5351] vsize: 90868
Current children cumulated CPU time (s) 507.9
Current children cumulated vsize (Kb) 92992

[startup+520.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 22545 0 0 0 51630 156 0 0 25 0 1 0 1843394806 94437376 22507 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 23056 22507 145 145 0 22911 0
[pid=5351] vsize: 92224
Current children cumulated CPU time (s) 517.87
Current children cumulated vsize (Kb) 94348

[startup+530.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 22888 0 0 0 52623 160 0 0 25 0 1 0 1843394806 95830016 22850 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 23396 22850 145 145 0 23251 0
[pid=5351] vsize: 93584
Current children cumulated CPU time (s) 527.84
Current children cumulated vsize (Kb) 95708

[startup+540.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 23229 0 0 0 53616 163 0 0 25 0 1 0 1843394806 97214464 23191 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 23734 23191 145 145 0 23589 0
[pid=5351] vsize: 94936
Current children cumulated CPU time (s) 537.8
Current children cumulated vsize (Kb) 97060

[startup+550.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 23548 0 0 0 54610 165 0 0 25 0 1 0 1843394806 98512896 23510 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24051 23510 145 145 0 23906 0
[pid=5351] vsize: 96204
Current children cumulated CPU time (s) 547.76
Current children cumulated vsize (Kb) 98328

[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 23870 0 0 0 55604 167 0 0 25 0 1 0 1843394806 99823616 23832 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24371 23832 145 145 0 24226 0
[pid=5351] vsize: 97484
Current children cumulated CPU time (s) 557.72
Current children cumulated vsize (Kb) 99608

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24150 0 0 0 56598 170 0 0 25 0 1 0 1843394806 100966400 24112 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24650 24112 145 145 0 24505 0
[pid=5351] vsize: 98600
Current children cumulated CPU time (s) 567.69
Current children cumulated vsize (Kb) 100724

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 57595 171 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 577.67
Current children cumulated vsize (Kb) 101256

[startup+590.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 58595 172 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 587.68
Current children cumulated vsize (Kb) 101256

[startup+600.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 59595 172 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 597.68
Current children cumulated vsize (Kb) 101256

[startup+610.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 60595 172 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 607.68
Current children cumulated vsize (Kb) 101256

[startup+620.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 61594 173 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 617.68
Current children cumulated vsize (Kb) 101256

[startup+630.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 62594 173 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 627.68
Current children cumulated vsize (Kb) 101256

[startup+640.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 63593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 637.68
Current children cumulated vsize (Kb) 101256

[startup+650.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 64593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 647.68
Current children cumulated vsize (Kb) 101256

[startup+660.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 65593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 657.68
Current children cumulated vsize (Kb) 101256

[startup+670.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 66593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 667.68
Current children cumulated vsize (Kb) 101256

[startup+680.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 67593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 677.69
Current children cumulated vsize (Kb) 101256

[startup+690.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 68593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 687.69
Current children cumulated vsize (Kb) 101256

[startup+700.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 69594 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 697.7
Current children cumulated vsize (Kb) 101256

[startup+710.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 70593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 707.69
Current children cumulated vsize (Kb) 101256

[startup+720.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 71593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 717.69
Current children cumulated vsize (Kb) 101256

[startup+730.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 72594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 727.7
Current children cumulated vsize (Kb) 101256

[startup+740.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 73594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 737.7
Current children cumulated vsize (Kb) 101256

[startup+750.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 74594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 747.7
Current children cumulated vsize (Kb) 101256

[startup+760.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 75594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 757.7
Current children cumulated vsize (Kb) 101256

[startup+770.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 76594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 767.7
Current children cumulated vsize (Kb) 101256

[startup+780.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 77595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 777.71
Current children cumulated vsize (Kb) 101256

[startup+790.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 78595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223040 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 787.71
Current children cumulated vsize (Kb) 101256

[startup+800.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 79595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 797.71
Current children cumulated vsize (Kb) 101256

[startup+810.086 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 80595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 807.71
Current children cumulated vsize (Kb) 101256

[startup+820.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 81596 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 817.72
Current children cumulated vsize (Kb) 101256

[startup+830.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 82596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 827.73
Current children cumulated vsize (Kb) 101256

[startup+840.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 83596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 837.73
Current children cumulated vsize (Kb) 101256

[startup+850.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 84596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 847.73
Current children cumulated vsize (Kb) 101256

[startup+860.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 85596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 857.73
Current children cumulated vsize (Kb) 101256

[startup+870.092 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 86597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 867.74
Current children cumulated vsize (Kb) 101256

[startup+880.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 87597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 877.74
Current children cumulated vsize (Kb) 101256

[startup+890.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 88597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 887.74
Current children cumulated vsize (Kb) 101256

[startup+900.095 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 89597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 897.74
Current children cumulated vsize (Kb) 101256

[startup+910.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 90597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 907.74
Current children cumulated vsize (Kb) 101256

[startup+920.097 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 91598 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 917.75
Current children cumulated vsize (Kb) 101256

[startup+930.098 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 92598 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 927.75
Current children cumulated vsize (Kb) 101256

[startup+940.099 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 93597 177 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 937.75
Current children cumulated vsize (Kb) 101256

[startup+950.102 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 94597 177 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 947.75
Current children cumulated vsize (Kb) 101256

[startup+960.102 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 95597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 957.76
Current children cumulated vsize (Kb) 101256

[startup+970.103 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 96597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 967.76
Current children cumulated vsize (Kb) 101256

[startup+980.104 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 97597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 977.76
Current children cumulated vsize (Kb) 101256

[startup+990.105 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 98597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 987.76
Current children cumulated vsize (Kb) 101256

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 99597 179 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 997.77
Current children cumulated vsize (Kb) 101256

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 100597 179 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1007.77
Current children cumulated vsize (Kb) 101256

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24289 0 0 0 101597 179 0 0 25 0 1 0 1843394806 101511168 24251 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24251 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1017.77
Current children cumulated vsize (Kb) 101256

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24293 0 0 0 102597 179 0 0 25 0 1 0 1843394806 101511168 24255 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24255 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1027.77
Current children cumulated vsize (Kb) 101256

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24295 0 0 0 103597 179 0 0 25 0 1 0 1843394806 101511168 24257 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24257 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1037.77
Current children cumulated vsize (Kb) 101256

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24297 0 0 0 104597 179 0 0 25 0 1 0 1843394806 101511168 24259 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24259 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1047.77
Current children cumulated vsize (Kb) 101256

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24300 0 0 0 105597 179 0 0 25 0 1 0 1843394806 101511168 24262 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24262 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1057.77
Current children cumulated vsize (Kb) 101256

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24303 0 0 0 106598 179 0 0 25 0 1 0 1843394806 101511168 24265 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24265 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1067.78
Current children cumulated vsize (Kb) 101256

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24306 0 0 0 107598 179 0 0 25 0 1 0 1843394806 101511168 24268 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24268 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1077.78
Current children cumulated vsize (Kb) 101256

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24309 0 0 0 108598 180 0 0 25 0 1 0 1843394806 101511168 24271 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24271 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1087.79
Current children cumulated vsize (Kb) 101256

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24312 0 0 0 109598 180 0 0 25 0 1 0 1843394806 101511168 24274 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24274 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1097.79
Current children cumulated vsize (Kb) 101256

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24315 0 0 0 110598 180 0 0 25 0 1 0 1843394806 101511168 24277 4294967295 134512640 135094434 3221224448 3221223040 134557215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24277 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1107.79
Current children cumulated vsize (Kb) 101256

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 111598 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1117.79
Current children cumulated vsize (Kb) 101256

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 112598 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1127.79
Current children cumulated vsize (Kb) 101256

[startup+1140.12 s]
Raw data (loadavg): 1.07 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 113599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1137.8
Current children cumulated vsize (Kb) 101256

[startup+1150.12 s]
Raw data (loadavg): 1.06 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 114599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1147.8
Current children cumulated vsize (Kb) 101256

[startup+1160.12 s]
Raw data (loadavg): 1.05 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 115599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1157.8
Current children cumulated vsize (Kb) 101256

[startup+1170.12 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 116599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1167.8
Current children cumulated vsize (Kb) 101256

[startup+1180.12 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 117599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1177.8
Current children cumulated vsize (Kb) 101256

[startup+1190.12 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 118600 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1187.81
Current children cumulated vsize (Kb) 101256

[startup+1200.12 s]
Raw data (loadavg): 1.03 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24320 0 0 0 119600 180 0 0 25 0 1 0 1843394806 101511168 24282 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24282 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1197.81
Current children cumulated vsize (Kb) 101256

[startup+1210.13 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24320 0 0 0 120600 180 0 0 25 0 1 0 1843394806 101511168 24282 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24282 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1207.81
Current children cumulated vsize (Kb) 101256



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 1.02 0.99 0.96 2/57 5351
Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5347/statm): 531 226 485 147 0 384 0
[pid=5347] vsize: 2124
Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24320 0 0 0 120600 180 0 0 25 0 1 0 1843394806 101511168 24282 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5351/statm): 24783 24282 145 145 0 24638 0
[pid=5351] vsize: 99132
Current children cumulated CPU time (s) 1207.81
Current children cumulated vsize (Kb) 101256

Sending SIGTERM to -5347
Sleeping 2 seconds
One traced child (pid=5347) ended because it received signal 15 (SIGTERM)
One traced child (pid=5351) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.18
CPU time (s): 1207.87
CPU user time (s): 1206.01
CPU system time (s): 1.85572
CPU usage (%): 99.8089
Max. virtual memory (cumulated for all children) (Kb): 101256

Verifier Data

ERROR: no interpretation found !