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/manquinho/primes-dimacs-cnf/normalized-ii8d1.opb
MD5SUMf5ae067eec5cb4736f6ec50c87e4a015
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 1060
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 1060
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 1060
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 variables1060
Total number of constraints3737
Number of constraints which are clauses3737
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 constraint10

Trace number 2192

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        919864 kB
Buffers:         35596 kB
Cached:          51800 kB
SwapCached:        868 kB
Active:          66276 kB
Inactive:        23740 kB
HighTotal:      131008 kB
HighFree:        76496 kB
LowTotal:       903652 kB
LowFree:        843368 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            19052 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:25:02 (client local time) WITH STATUS 10 IN 1208.12 SECONDS
stats: 2568 7 1208.12 10

Solver Data

c Parsing PB file...
c Converting 3737 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 |    3737     8550 |    1245       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 394
c ---[   0]---> Sorter-cost:57992     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         5 |   72070   168258 |   24023       5       53    10.6 |  0.000 % |
c |       105 |   71927   167963 |   26425      99     3057    30.9 |  0.186 % |
c ==============================================================================
c Found solution: 343
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       209 |   72514   169469 |   24171     202     5151    25.5 |  0.186 % |
c |       309 |   72514   169469 |   26588     302     7218    23.9 |  0.229 % |
c |       460 |   72355   169132 |   29246     449    10672    23.8 |  0.420 % |
c |       691 |   72355   169132 |   32171     680    16102    23.7 |  0.420 % |
c |      1028 |   72355   169132 |   35388    1017    21313    21.0 |  0.420 % |
c |      1535 |   72262   168931 |   38927    1114    22621    20.3 |  0.534 % |
c |      2294 |   68690   161043 |   42820    1742    48315    27.7 |  5.156 % |
c |      3438 |   68235   160038 |   47102    2853    87468    30.7 |  5.741 % |
c |      5147 |   68126   159801 |   51812    4559   183493    40.2 |  5.878 % |
c |      7709 |   67678   158817 |   56993    7099   339626    47.8 |  6.450 % |
c |     11554 |   67678   158817 |   62693   10944   771181    70.5 |  6.450 % |
c |     17320 |   67473   158366 |   68962   16703  1593085    95.4 |  6.707 % |
c |     25969 |   67473   158366 |   75858   25352  2470677    97.5 |  6.707 % |
c |     38944 |   67436   158285 |   83444   38310  5031133   131.3 |  6.755 % |
c |     58407 |   67394   158189 |   91789   57770  7795989   134.9 |  6.810 % |
c |     87599 |   67366   158133 |  100968   86961 12290739   141.3 |  6.838 % |
c |    131388 |   67235   157828 |  111065   42493  4058866    95.5 |  7.025 % |
c |    197073 |   67143   157620 |  122171  108144 16164310   149.5 |  7.147 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 x3 -x4 x5 -x6 -x7 x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 -x39 x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 -x71 x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 -x103 x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 -x139 x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 -x155 x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 -x167 x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 -x199 x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 -x231 x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 x261 -x262 -x263 x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 -x311 x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 -x321 x322 -x323 x324 -x325 x326 -x327 x328 x329 -x330 -x331 x332 -x333 x334 -x335 x336 -x337 x338 -x339 x340 -x341 x342 -x343 x344 -x345 x346 -x347 x348 -x349 x350 -x351 x352 -x353 x354 -x355 x356 -x357 x358 x359 -x360 -x361 x362 -x363 x364 -x365 x366 -x367 x368 -x369 x370 -x371 x372 -x373 x374 -x375 x376 -x377 x378 x379 -x380 -x381 x382 -x383 x384 -x385 x386 -x387 x388 x389 -x390 -x391 x392 -x393 x394 -x395 x396 -x397 x398 -x399 x400 -x401 x402 -x403 x404 -x405 x406 -x407 x408 -x409 x410 -x411 x412 -x413 x414 -x415 x416 -x417 x418 x419 -x420 -x421 x422 -x423 x424 -x425 x426 -x427 x428 -x429 x430 -x431 x432 -x433 x434 -x435 x436 -x437 x438 x439 -x440 x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 x470 -x471 -x472 x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 x487 -x488 -x489 x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 x500 -x501 -x502 -x503 -x504 x505 -x506 -x507 -x508 -x509 x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 x520 -x521 -x522 -x523 -x524 -x525 -x526 x527 -x528 -x529 x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 x540 -x541 x542 -x543 x544 -x545 x546 -x547 x548 -x549 x550 -x551 x552 -x553 x554 -x555 x556 -x557 x558 x559 -x560 -x561 x562 -x563 x564 -x565 x566 -x567 x568 -x569 x570 -x571 x572 -x573 x574 -x575 x576 -x577 x578 x579 -x580 -x581 x582 -x583 x584 -x585 x586 -x587 x588 -x589 x590 -x591 x592 -x593 x594 -x595 x596 -x597 x598 x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 x607 -x608 -x609 x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 x673 -x674 -x675 -x676 -x677 -x678 -x679 x680 -x681 x682 -x683 x684 -x685 x686 -x687 x688 x689 -x690 -x691 x692 -x693 x694 -x695 x696 -x697 x698 -x699 x700 -x701 -x702 -x703 -x704 -x705 -x706 x707 -x708 -x709 x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 x730 -x731 -x732 -x733 -x734 x735 -x736 -x737 -x738 -x739 x740 -x741 -x74

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/24238/stat): 24238 (minisat+_script) R 24237 24238 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843285807 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24238/statm): 174 3 169 147 0 27 0
[pid=24238] 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=24239
New process pid=24240
New process pid=24241
execve syscall for /bin/sed executable
One traced child (pid=24240) 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=24241) exited with status: 0
One traced child (pid=24239) exited with status: 0
New process pid=24242
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-ii8d1.opb

[startup+10.0031 s]
Raw data (loadavg): 0.69 0.92 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 3916 0 0 0 968 14 0 0 25 0 1 0 1843285812 17338368 3761 4294967295 134512640 135094434 3221224448 3221223120 134556515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 4233 3761 145 145 0 4088 0
[pid=24242] vsize: 16932
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 19056

[startup+20.0048 s]
Raw data (loadavg): 0.73 0.92 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 4123 0 0 0 1964 16 0 0 25 0 1 0 1843285812 18186240 3968 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 4440 3968 145 145 0 4295 0
[pid=24242] vsize: 17760
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 19884

[startup+30.0064 s]
Raw data (loadavg): 0.77 0.93 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 4436 0 0 0 2958 19 0 0 25 0 1 0 1843285812 19488768 4281 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 4758 4281 145 145 0 4613 0
[pid=24242] vsize: 19032
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 21156

[startup+40.0071 s]
Raw data (loadavg): 0.81 0.93 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 4721 0 0 0 3952 21 0 0 25 0 1 0 1843285812 20643840 4566 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 5040 4566 145 145 0 4895 0
[pid=24242] vsize: 20160
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 22284

[startup+50.0088 s]
Raw data (loadavg): 0.84 0.93 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 5084 0 0 0 4946 24 0 0 25 0 1 0 1843285812 22118400 4929 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 5400 4929 145 145 0 5255 0
[pid=24242] vsize: 21600
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 23724

[startup+60.0095 s]
Raw data (loadavg): 0.86 0.93 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 5520 0 0 0 5938 27 0 0 25 0 1 0 1843285812 23900160 5365 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 5835 5365 145 145 0 5690 0
[pid=24242] vsize: 23340
Current children cumulated CPU time (s) 59.66
Current children cumulated vsize (Kb) 25464

[startup+70.0112 s]
Raw data (loadavg): 0.88 0.93 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 5779 0 0 0 6933 29 0 0 25 0 1 0 1843285812 25010176 5624 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 6106 5624 145 145 0 5961 0
[pid=24242] vsize: 24424
Current children cumulated CPU time (s) 69.63
Current children cumulated vsize (Kb) 26548

[startup+80.0129 s]
Raw data (loadavg): 0.90 0.94 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 6126 0 0 0 7925 33 0 0 25 0 1 0 1843285812 26419200 5971 4294967295 134512640 135094434 3221224448 3221223040 134557345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 6450 5971 145 145 0 6305 0
[pid=24242] vsize: 25800
Current children cumulated CPU time (s) 79.59
Current children cumulated vsize (Kb) 27924

[startup+90.0135 s]
Raw data (loadavg): 0.91 0.94 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 6462 0 0 0 8918 35 0 0 25 0 1 0 1843285812 27787264 6307 4294967295 134512640 135094434 3221224448 3221223104 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 6784 6307 145 145 0 6639 0
[pid=24242] vsize: 27136
Current children cumulated CPU time (s) 89.54
Current children cumulated vsize (Kb) 29260

[startup+100.014 s]
Raw data (loadavg): 0.93 0.94 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 6696 0 0 0 9913 37 0 0 25 0 1 0 1843285812 28733440 6541 4294967295 134512640 135094434 3221224448 3221222992 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 7015 6541 145 145 0 6870 0
[pid=24242] vsize: 28060
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 30184

[startup+110.015 s]
Raw data (loadavg): 0.94 0.94 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 7028 0 0 0 10906 40 0 0 25 0 1 0 1843285812 30085120 6873 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 7345 6873 145 145 0 7200 0
[pid=24242] vsize: 29380
Current children cumulated CPU time (s) 109.47
Current children cumulated vsize (Kb) 31504

[startup+120.017 s]
Raw data (loadavg): 0.95 0.94 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 7355 0 0 0 11899 43 0 0 25 0 1 0 1843285812 31420416 7200 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 7671 7200 145 145 0 7526 0
[pid=24242] vsize: 30684
Current children cumulated CPU time (s) 119.43
Current children cumulated vsize (Kb) 32808

[startup+130.017 s]
Raw data (loadavg): 0.95 0.94 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 7748 0 0 0 12892 46 0 0 25 0 1 0 1843285812 33026048 7593 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 8063 7593 145 145 0 7918 0
[pid=24242] vsize: 32252
Current children cumulated CPU time (s) 129.39
Current children cumulated vsize (Kb) 34376

[startup+140.018 s]
Raw data (loadavg): 0.96 0.94 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 8088 0 0 0 13887 49 0 0 25 0 1 0 1843285812 34541568 7933 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 8433 7933 145 145 0 8288 0
[pid=24242] vsize: 33732
Current children cumulated CPU time (s) 139.37
Current children cumulated vsize (Kb) 35856

[startup+150.02 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 8422 0 0 0 14881 51 0 0 25 0 1 0 1843285812 35905536 8267 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 8766 8267 145 145 0 8621 0
[pid=24242] vsize: 35064
Current children cumulated CPU time (s) 149.33
Current children cumulated vsize (Kb) 37188

[startup+160.02 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 8708 0 0 0 15875 54 0 0 25 0 1 0 1843285812 37072896 8553 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 9051 8553 145 145 0 8906 0
[pid=24242] vsize: 36204
Current children cumulated CPU time (s) 159.3
Current children cumulated vsize (Kb) 38328

[startup+170.021 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 9056 0 0 0 16869 56 0 0 25 0 1 0 1843285812 38494208 8901 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 9398 8901 145 145 0 9253 0
[pid=24242] vsize: 37592
Current children cumulated CPU time (s) 169.26
Current children cumulated vsize (Kb) 39716

[startup+180.022 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 9329 0 0 0 17863 59 0 0 25 0 1 0 1843285812 39600128 9174 4294967295 134512640 135094434 3221224448 3221223040 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 9668 9174 145 145 0 9523 0
[pid=24242] vsize: 38672
Current children cumulated CPU time (s) 179.23
Current children cumulated vsize (Kb) 40796

[startup+190.022 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 9577 0 0 0 18858 61 0 0 25 0 1 0 1843285812 40603648 9422 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 9913 9422 145 145 0 9768 0
[pid=24242] vsize: 39652
Current children cumulated CPU time (s) 189.2
Current children cumulated vsize (Kb) 41776

[startup+200.023 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 9827 0 0 0 19852 64 0 0 25 0 1 0 1843285812 41619456 9672 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 10161 9672 145 145 0 10016 0
[pid=24242] vsize: 40644
Current children cumulated CPU time (s) 199.17
Current children cumulated vsize (Kb) 42768

[startup+210.024 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 10215 0 0 0 20844 67 0 0 25 0 1 0 1843285812 43200512 10060 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 10547 10060 145 145 0 10402 0
[pid=24242] vsize: 42188
Current children cumulated CPU time (s) 209.12
Current children cumulated vsize (Kb) 44312

[startup+220.025 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 10547 0 0 0 21837 69 0 0 25 0 1 0 1843285812 44576768 10392 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 10883 10392 145 145 0 10738 0
[pid=24242] vsize: 43532
Current children cumulated CPU time (s) 219.07
Current children cumulated vsize (Kb) 45656

[startup+230.026 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 10879 0 0 0 22832 72 0 0 25 0 1 0 1843285812 45932544 10724 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 11214 10724 145 145 0 11069 0
[pid=24242] vsize: 44856
Current children cumulated CPU time (s) 229.05
Current children cumulated vsize (Kb) 46980

[startup+240.027 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 11104 0 0 0 23828 73 0 0 25 0 1 0 1843285812 46850048 10949 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 11438 10949 145 145 0 11293 0
[pid=24242] vsize: 45752
Current children cumulated CPU time (s) 239.02
Current children cumulated vsize (Kb) 47876

[startup+250.027 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 11404 0 0 0 24823 76 0 0 25 0 1 0 1843285812 48066560 11249 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 11735 11249 145 145 0 11590 0
[pid=24242] vsize: 46940
Current children cumulated CPU time (s) 249
Current children cumulated vsize (Kb) 49064

[startup+260.03 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 11675 0 0 0 25818 78 0 0 25 0 1 0 1843285812 49168384 11520 4294967295 134512640 135094434 3221224448 3221223040 134556980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 12004 11520 145 145 0 11859 0
[pid=24242] vsize: 48016
Current children cumulated CPU time (s) 258.97
Current children cumulated vsize (Kb) 50140

[startup+270.031 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 11938 0 0 0 26812 81 0 0 25 0 1 0 1843285812 50241536 11783 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 12266 11783 145 145 0 12121 0
[pid=24242] vsize: 49064
Current children cumulated CPU time (s) 268.94
Current children cumulated vsize (Kb) 51188

[startup+280.032 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 12223 0 0 0 27806 84 0 0 25 0 1 0 1843285812 51400704 12068 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 12549 12068 145 145 0 12404 0
[pid=24242] vsize: 50196
Current children cumulated CPU time (s) 278.91
Current children cumulated vsize (Kb) 52320

[startup+290.032 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 12483 0 0 0 28801 86 0 0 25 0 1 0 1843285812 52457472 12328 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 12807 12328 145 145 0 12662 0
[pid=24242] vsize: 51228
Current children cumulated CPU time (s) 288.88
Current children cumulated vsize (Kb) 53352

[startup+300.033 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 12753 0 0 0 29795 88 0 0 25 0 1 0 1843285812 53559296 12598 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 13076 12598 145 145 0 12931 0
[pid=24242] vsize: 52304
Current children cumulated CPU time (s) 298.84
Current children cumulated vsize (Kb) 54428

[startup+310.034 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 13050 0 0 0 30791 90 0 0 25 0 1 0 1843285812 54767616 12895 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 13371 12895 145 145 0 13226 0
[pid=24242] vsize: 53484
Current children cumulated CPU time (s) 308.82
Current children cumulated vsize (Kb) 55608

[startup+320.035 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 13266 0 0 0 31787 91 0 0 25 0 1 0 1843285812 55648256 13111 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 13586 13111 145 145 0 13441 0
[pid=24242] vsize: 54344
Current children cumulated CPU time (s) 318.79
Current children cumulated vsize (Kb) 56468

[startup+330.036 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 13451 0 0 0 32785 92 0 0 25 0 1 0 1843285812 56659968 13296 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 13833 13296 145 145 0 13688 0
[pid=24242] vsize: 55332
Current children cumulated CPU time (s) 328.78
Current children cumulated vsize (Kb) 57456

[startup+340.037 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 13642 0 0 0 33782 94 0 0 25 0 1 0 1843285812 57438208 13487 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 14023 13487 145 145 0 13878 0
[pid=24242] vsize: 56092
Current children cumulated CPU time (s) 338.77
Current children cumulated vsize (Kb) 58216

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 13848 0 0 0 34778 95 0 0 25 0 1 0 1843285812 58273792 13693 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 14227 13693 145 145 0 14082 0
[pid=24242] vsize: 56908
Current children cumulated CPU time (s) 348.74
Current children cumulated vsize (Kb) 59032

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 13972 0 0 0 35776 95 0 0 25 0 1 0 1843285812 58777600 13817 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 14350 13817 145 145 0 14205 0
[pid=24242] vsize: 57400
Current children cumulated CPU time (s) 358.72
Current children cumulated vsize (Kb) 59524

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 14105 0 0 0 36774 97 0 0 25 0 1 0 1843285812 59318272 13950 4294967295 134512640 135094434 3221224448 3221223072 134557722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 14482 13950 145 145 0 14337 0
[pid=24242] vsize: 57928
Current children cumulated CPU time (s) 368.72
Current children cumulated vsize (Kb) 60052

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 14235 0 0 0 37771 98 0 0 25 0 1 0 1843285812 59846656 14080 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 14611 14080 145 145 0 14466 0
[pid=24242] vsize: 58444
Current children cumulated CPU time (s) 378.7
Current children cumulated vsize (Kb) 60568

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 14409 0 0 0 38768 99 0 0 25 0 1 0 1843285812 60555264 14254 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 14784 14254 145 145 0 14639 0
[pid=24242] vsize: 59136
Current children cumulated CPU time (s) 388.68
Current children cumulated vsize (Kb) 61260

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 14553 0 0 0 39765 101 0 0 25 0 1 0 1843285812 61140992 14398 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 14927 14398 145 145 0 14782 0
[pid=24242] vsize: 59708
Current children cumulated CPU time (s) 398.67
Current children cumulated vsize (Kb) 61832

[startup+410.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 14842 0 0 0 40760 102 0 0 25 0 1 0 1843285812 62320640 14687 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 15215 14687 145 145 0 15070 0
[pid=24242] vsize: 60860
Current children cumulated CPU time (s) 408.63
Current children cumulated vsize (Kb) 62984

[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 15117 0 0 0 41755 104 0 0 25 0 1 0 1843285812 63438848 14962 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 15488 14962 145 145 0 15343 0
[pid=24242] vsize: 61952
Current children cumulated CPU time (s) 418.6
Current children cumulated vsize (Kb) 64076

[startup+430.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 15288 0 0 0 42753 105 0 0 25 0 1 0 1843285812 64135168 15133 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 15658 15133 145 145 0 15513 0
[pid=24242] vsize: 62632
Current children cumulated CPU time (s) 428.59
Current children cumulated vsize (Kb) 64756

[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) T 24238 24238 16528 0 -1 0 15567 0 0 0 43746 108 0 0 25 0 1 0 1843285812 65269760 15412 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24242/statm): 15935 15412 145 145 0 15790 0
[pid=24242] vsize: 63740
Current children cumulated CPU time (s) 438.55
Current children cumulated vsize (Kb) 65864

[startup+450.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 15949 0 0 0 44739 112 0 0 25 0 1 0 1843285812 66830336 15794 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 16316 15794 145 145 0 16171 0
[pid=24242] vsize: 65264
Current children cumulated CPU time (s) 448.52
Current children cumulated vsize (Kb) 67388

[startup+460.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 16375 0 0 0 45732 115 0 0 25 0 1 0 1843285812 68567040 16220 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 16740 16220 145 145 0 16595 0
[pid=24242] vsize: 66960
Current children cumulated CPU time (s) 458.48
Current children cumulated vsize (Kb) 69084

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 16809 0 0 0 46724 118 0 0 25 0 1 0 1843285812 70340608 16654 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 17173 16654 145 145 0 17028 0
[pid=24242] vsize: 68692
Current children cumulated CPU time (s) 468.43
Current children cumulated vsize (Kb) 70816

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 17094 0 0 0 47718 121 0 0 25 0 1 0 1843285812 71499776 16939 4294967295 134512640 135094434 3221224448 3221223120 134556275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 17456 16939 145 145 0 17311 0
[pid=24242] vsize: 69824
Current children cumulated CPU time (s) 478.4
Current children cumulated vsize (Kb) 71948

[startup+490.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 17416 0 0 0 48712 123 0 0 25 0 1 0 1843285812 72814592 17261 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 17777 17261 145 145 0 17632 0
[pid=24242] vsize: 71108
Current children cumulated CPU time (s) 488.36
Current children cumulated vsize (Kb) 73232

[startup+500.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 17756 0 0 0 49706 126 0 0 25 0 1 0 1843285812 74203136 17601 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 18116 17601 145 145 0 17971 0
[pid=24242] vsize: 72464
Current children cumulated CPU time (s) 498.33
Current children cumulated vsize (Kb) 74588

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 18115 0 0 0 50700 128 0 0 25 0 1 0 1843285812 75661312 17960 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 18472 17960 145 145 0 18327 0
[pid=24242] vsize: 73888
Current children cumulated CPU time (s) 508.29
Current children cumulated vsize (Kb) 76012

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 18385 0 0 0 51696 130 0 0 25 0 1 0 1843285812 76763136 18230 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 18741 18230 145 145 0 18596 0
[pid=24242] vsize: 74964
Current children cumulated CPU time (s) 518.27
Current children cumulated vsize (Kb) 77088

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 18625 0 0 0 52692 132 0 0 25 0 1 0 1843285812 77750272 18470 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 18982 18470 145 145 0 18837 0
[pid=24242] vsize: 75928
Current children cumulated CPU time (s) 528.25
Current children cumulated vsize (Kb) 78052

[startup+540.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 18862 0 0 0 53687 133 0 0 25 0 1 0 1843285812 78704640 18707 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 19215 18707 145 145 0 19070 0
[pid=24242] vsize: 76860
Current children cumulated CPU time (s) 538.21
Current children cumulated vsize (Kb) 78984

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19012 0 0 0 54685 135 0 0 25 0 1 0 1843285812 79314944 18857 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 19364 18857 145 145 0 19219 0
[pid=24242] vsize: 77456
Current children cumulated CPU time (s) 548.21
Current children cumulated vsize (Kb) 79580

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19247 0 0 0 55681 136 0 0 25 0 1 0 1843285812 80277504 19092 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 19599 19092 145 145 0 19454 0
[pid=24242] vsize: 78396
Current children cumulated CPU time (s) 558.18
Current children cumulated vsize (Kb) 80520

[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19496 0 0 0 56677 138 0 0 25 0 1 0 1843285812 81285120 19341 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 19845 19341 145 145 0 19700 0
[pid=24242] vsize: 79380
Current children cumulated CPU time (s) 568.16
Current children cumulated vsize (Kb) 81504

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 57674 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 578.15
Current children cumulated vsize (Kb) 82416

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 58674 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 588.15
Current children cumulated vsize (Kb) 82416

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 59675 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 598.16
Current children cumulated vsize (Kb) 82416

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 60675 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 608.16
Current children cumulated vsize (Kb) 82416

[startup+620.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 61675 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 618.16
Current children cumulated vsize (Kb) 82416

[startup+630.059 s]
Raw data (loadavg): 1.07 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 62675 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 628.16
Current children cumulated vsize (Kb) 82416

[startup+640.059 s]
Raw data (loadavg): 1.06 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 63675 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 638.16
Current children cumulated vsize (Kb) 82416

[startup+650.06 s]
Raw data (loadavg): 1.05 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 64675 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 648.16
Current children cumulated vsize (Kb) 82416

[startup+660.061 s]
Raw data (loadavg): 1.04 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 65676 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 658.17
Current children cumulated vsize (Kb) 82416

[startup+670.061 s]
Raw data (loadavg): 1.04 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 66676 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 668.17
Current children cumulated vsize (Kb) 82416

[startup+680.062 s]
Raw data (loadavg): 1.03 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 67676 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 678.17
Current children cumulated vsize (Kb) 82416

[startup+690.063 s]
Raw data (loadavg): 1.03 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 68676 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223100 134670544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 688.17
Current children cumulated vsize (Kb) 82416

[startup+700.063 s]
Raw data (loadavg): 1.02 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 69676 140 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 698.17
Current children cumulated vsize (Kb) 82416

[startup+710.064 s]
Raw data (loadavg): 1.02 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 70676 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 708.18
Current children cumulated vsize (Kb) 82416

[startup+720.065 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 71676 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 718.18
Current children cumulated vsize (Kb) 82416

[startup+730.065 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 72677 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 728.19
Current children cumulated vsize (Kb) 82416

[startup+740.066 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 73677 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 738.19
Current children cumulated vsize (Kb) 82416

[startup+750.067 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 74677 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 748.19
Current children cumulated vsize (Kb) 82416

[startup+760.067 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 75677 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 758.19
Current children cumulated vsize (Kb) 82416

[startup+770.068 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 76678 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 768.2
Current children cumulated vsize (Kb) 82416

[startup+780.069 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 77678 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 778.2
Current children cumulated vsize (Kb) 82416

[startup+790.069 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 78678 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134556900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 788.2
Current children cumulated vsize (Kb) 82416

[startup+800.071 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 79678 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 798.2
Current children cumulated vsize (Kb) 82416

[startup+810.072 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 80679 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 808.21
Current children cumulated vsize (Kb) 82416

[startup+820.072 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 81679 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 818.21
Current children cumulated vsize (Kb) 82416

[startup+830.073 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 82679 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 828.21
Current children cumulated vsize (Kb) 82416

[startup+840.074 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 83679 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 838.21
Current children cumulated vsize (Kb) 82416

[startup+850.074 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 84679 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 848.21
Current children cumulated vsize (Kb) 82416

[startup+860.075 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 85679 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 858.21
Current children cumulated vsize (Kb) 82416

[startup+870.077 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 86680 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 868.22
Current children cumulated vsize (Kb) 82416

[startup+880.077 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 87680 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 878.22
Current children cumulated vsize (Kb) 82416

[startup+890.078 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 88680 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 888.22
Current children cumulated vsize (Kb) 82416

[startup+900.079 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 89680 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 898.22
Current children cumulated vsize (Kb) 82416

[startup+910.08 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 90681 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 908.23
Current children cumulated vsize (Kb) 82416

[startup+920.08 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 91681 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223120 134555957 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 918.23
Current children cumulated vsize (Kb) 82416

[startup+930.081 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 92681 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134556931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 928.23
Current children cumulated vsize (Kb) 82416

[startup+940.082 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 93681 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 938.23
Current children cumulated vsize (Kb) 82416

[startup+950.082 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 94681 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 948.23
Current children cumulated vsize (Kb) 82416

[startup+960.083 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 95681 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 958.23
Current children cumulated vsize (Kb) 82416

[startup+970.085 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 96682 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 968.24
Current children cumulated vsize (Kb) 82416

[startup+980.085 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 97682 141 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 978.24
Current children cumulated vsize (Kb) 82416

[startup+990.086 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 98682 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 988.25
Current children cumulated vsize (Kb) 82416

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 99682 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 998.25
Current children cumulated vsize (Kb) 82416

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 100682 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134556949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1008.25
Current children cumulated vsize (Kb) 82416

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 101682 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1018.25
Current children cumulated vsize (Kb) 82416

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 102683 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1028.26
Current children cumulated vsize (Kb) 82416

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 103683 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1038.26
Current children cumulated vsize (Kb) 82416

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 104683 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1048.26
Current children cumulated vsize (Kb) 82416

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 105683 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1058.26
Current children cumulated vsize (Kb) 82416

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 106683 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1068.26
Current children cumulated vsize (Kb) 82416

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 107684 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1078.27
Current children cumulated vsize (Kb) 82416

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 108684 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1088.27
Current children cumulated vsize (Kb) 82416

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 109683 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1098.26
Current children cumulated vsize (Kb) 82416

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 110682 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1108.25
Current children cumulated vsize (Kb) 82416

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19725 0 0 0 111683 142 0 0 25 0 1 0 1843285812 82219008 19570 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20073 19570 145 145 0 19928 0
[pid=24242] vsize: 80292
Current children cumulated CPU time (s) 1118.26
Current children cumulated vsize (Kb) 82416

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 19916 0 0 0 112680 144 0 0 25 0 1 0 1843285812 83001344 19761 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20264 19761 145 145 0 20119 0
[pid=24242] vsize: 81056
Current children cumulated CPU time (s) 1128.25
Current children cumulated vsize (Kb) 83180

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 20164 0 0 0 113676 146 0 0 25 0 1 0 1843285812 84021248 20009 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20513 20009 145 145 0 20368 0
[pid=24242] vsize: 82052
Current children cumulated CPU time (s) 1138.23
Current children cumulated vsize (Kb) 84176

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 20431 0 0 0 114672 148 0 0 25 0 1 0 1843285812 85114880 20276 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 20780 20276 145 145 0 20635 0
[pid=24242] vsize: 83120
Current children cumulated CPU time (s) 1148.21
Current children cumulated vsize (Kb) 85244

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 20680 0 0 0 115668 150 0 0 25 0 1 0 1843285812 86142976 20525 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 21031 20525 145 145 0 20886 0
[pid=24242] vsize: 84124
Current children cumulated CPU time (s) 1158.19
Current children cumulated vsize (Kb) 86248

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 20909 0 0 0 116664 151 0 0 25 0 1 0 1843285812 87080960 20754 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 21260 20754 145 145 0 21115 0
[pid=24242] vsize: 85040
Current children cumulated CPU time (s) 1168.16
Current children cumulated vsize (Kb) 87164

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 21135 0 0 0 117661 153 0 0 25 0 1 0 1843285812 88002560 20980 4294967295 134512640 135094434 3221224448 3221223040 134557016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 21485 20980 145 145 0 21340 0
[pid=24242] vsize: 85940
Current children cumulated CPU time (s) 1178.15
Current children cumulated vsize (Kb) 88064

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) T 24238 24238 16528 0 -1 0 21356 0 0 0 118657 155 0 0 25 0 1 0 1843285812 88903680 21201 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/24242/statm): 21705 21201 145 145 0 21560 0
[pid=24242] vsize: 86820
Current children cumulated CPU time (s) 1188.13
Current children cumulated vsize (Kb) 88944

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 21516 0 0 0 119653 156 0 0 25 0 1 0 1843285812 89559040 21361 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 21865 21361 145 145 0 21720 0
[pid=24242] vsize: 87460
Current children cumulated CPU time (s) 1198.1
Current children cumulated vsize (Kb) 89584

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 21766 0 0 0 120649 158 0 0 25 0 1 0 1843285812 90574848 21611 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 22113 21611 145 145 0 21968 0
[pid=24242] vsize: 88452
Current children cumulated CPU time (s) 1208.08
Current children cumulated vsize (Kb) 90576



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 24242
Raw data (/proc/24238/stat): 24238 (minisat+_script) S 24237 24238 16528 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843285807 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24238/statm): 531 226 485 147 0 384 0
[pid=24238] vsize: 2124
Raw data (/proc/24242/stat): 24242 (minisat+_64-bit) R 24238 24238 16528 0 -1 0 21766 0 0 0 120649 158 0 0 25 0 1 0 1843285812 90574848 21611 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24242/statm): 22113 21611 145 145 0 21968 0
[pid=24242] vsize: 88452
Current children cumulated CPU time (s) 1208.08
Current children cumulated vsize (Kb) 90576

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1208.12
CPU user time (s): 1206.5
CPU system time (s): 1.62275
CPU usage (%): 99.8327
Max. virtual memory (cumulated for all children) (Kb): 90576

Verifier Data

ERROR: no interpretation found !