Name | submitted/een/normalized-seymour.opb |
MD5SUM | 23a177449585151350479e80b33e6416 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 343 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1372 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1372 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1372 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.02 |
Number of variables | 1255 |
Total number of constraints | 4827 |
Number of constraints which are clauses | 4827 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 19 |
LAUNCH ON wulflinc18 THE 2005-09-18 18:30:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2632 boxname=wulflinc18 idbench=288 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 23a177449585151350479e80b33e6416 /oldhome/oroussel/tmp/wulflinc18/normalized-seymour.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-seymour.opb IDLAUNCH: 2632 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 916376 kB Buffers: 35304 kB Cached: 48308 kB SwapCached: 844 kB Active: 66492 kB Inactive: 19708 kB HighTotal: 131008 kB HighFree: 79828 kB LowTotal: 903652 kB LowFree: 836548 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5764 kB Slab: 26612 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:50:38 (client local time) WITH STATUS 10 IN 1207.87 SECONDS stats: 2632 7 1207.87 10
c Parsing PB file... c Converting 4827 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 4827 33432 | 1609 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 349[0m c ---[ 0]---> Sorter-cost:76410 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 98923 253123 | 32974 0 0 nan | 0.000 % | c | 100 | 97075 249222 | 36271 53 306 5.8 | 1.611 % | c | 250 | 96306 247533 | 39898 182 1434 7.9 | 2.335 % | c | 475 | 94983 244630 | 43888 352 2733 7.8 | 3.580 % | c | 813 | 93755 241908 | 48277 659 6082 9.2 | 4.756 % | c | 1319 | 92568 239259 | 53104 1107 10103 9.1 | 5.908 % | c | 2079 | 91909 237778 | 58415 1848 16788 9.1 | 6.556 % | c | 3218 | 91411 236662 | 64256 2962 28061 9.5 | 7.042 % | c | 4926 | 90331 234236 | 70682 4606 53966 11.7 | 8.078 % | c | 7488 | 90120 233759 | 77750 7151 98759 13.8 | 8.279 % | c | 11332 | 89899 233266 | 85526 10979 176068 16.0 | 8.478 % | c | 17098 | 89285 231884 | 94078 16657 308712 18.5 | 9.049 % | c | 25749 | 89112 231493 | 103486 25255 976019 38.6 | 9.212 % | c | 38723 | 89001 231242 | 113835 38209 1772808 46.4 | 9.316 % | c | 58184 | 88950 231133 | 125218 57664 4775966 82.8 | 9.357 % | c | 87378 | 88942 231115 | 137740 86849 9904394 114.0 | 9.365 % | c | 131169 | 88746 230668 | 151514 130531 13442173 103.0 | 9.548 % | c | 196853 | 88719 230611 | 166666 44042 6107081 138.7 | 9.572 % | c | 295379 | 88664 230490 | 183332 142564 10444974 73.3 | 9.624 % | c c *** TERMINATED *** s SATISFIABLE v -x0 x1 -x2 -x3 x4 -x5 -x6 -x7 x8 -x9 x10 -x11 x12 -x13 -x14 x15 -x16 -x17 x18 -x19 -x20 -x21 -x22 x23 -x24 x25 x26 x27 -x28 -x29 -x30 -x31 -x32 x33 x34 -x35 -x36 x37 -x38 -x39 -x40 x41 x42 -x43 x44 x45 x46 -x47 -x48 x49 -x50 -x51 x52 x53 x54 -x55 x56 x57 x58 -x59 -x60 x61 x62 x63 -x64 x65 x66 x67 x68 x69 -x70 -x71 -x72 -x73 -x74 x75 -x76 -x77 -x78 -x79 x80 x81 x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 x90 x91 -x92 -x93 x94 x95 -x96 -x97 -x98 x99 x100 -x101 -x102 -x103 -x104 -x105 x106 -x107 x108 -x109 x110 x111 x112 -x113 -x114 -x115 x116 -x117 -x118 -x119 -x120 -x121 -x122 x123 -x124 -x125 x126 -x127 x128 -x129 -x130 x131 -x132 -x133 -x134 x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 x143 -x144 -x145 -x146 -x147 x148 x149 -x150 -x151 x152 x153 -x154 -x155 -x156 -x157 x158 -x159 x160 -x161 -x162 -x163 -x164 x165 -x166 -x167 -x168 x169 x170 -x171 -x172 x173 -x174 -x175 -x176 -x177 -x178 x179 -x180 -x181 -x182 -x183 x184 x185 x186 -x187 -x188 x189 -x190 -x191 x192 x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 x204 -x205 -x206 -x207 -x208 -x209 -x210 x211 x212 -x213 -x214 -x215 x216 -x217 x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 x227 x228 -x229 -x230 x231 x232 -x233 x234 x235 -x236 -x237 x238 -x239 -x240 -x241 x242 -x243 x244 -x245 x246 -x247 -x248 x249 -x250 -x251 x252 -x253 x254 -x255 -x256 -x257 -x258 -x259 x260 -x261 -x262 x263 -x264 -x265 x266 -x267 x268 -x269 -x270 x271 -x272 x273 -x274 -x275 x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 x284 -x285 x286 x287 -x288 -x289 -x290 x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 x308 -x309 -x310 -x311 -x312 x313 x314 -x315 -x316 -x317 -x318 x319 -x320 x321 -x322 -x323 -x324 x325 -x326 -x327 x328 -x329 -x330 -x331 x332 -x333 x334 x335 -x336 -x337 x338 x339 x340 -x341 -x342 x343 x344 -x345 x346 -x347 -x348 -x349 -x350 -x351 -x352 x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 x365 -x366 x367 x368 -x369 -x370 -x371 -x372 -x373 x374 -x375 -x376 -x377 x378 -x379 -x380 x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 x390 x391 x392 -x393 -x394 -x395 x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 x423 x424 x425 x426 -x427 x428 x429 x430 x431 x432 -x433 -x434 -x435 x436 x437 x438 -x439 -x440 x441 -x442 x443 -x444 x445 x446 -x447 -x448 -x449 -x450 -x451 -x452 x453 x454 x455 x456 -x457 x458 -x459 x460 x461 x462 x463 x464 x465 -x466 x467 -x468 x469 -x470 x471 -x472 -x473 -x474 x475 x476 x477 x478 x479 x480 -x481 -x482 x483 -x484 x485 x486 -x487 -x488 x489 x490 x491 -x492 x493 -x494 -x495 -x496 -x497 x498 -x499 x500 x501 -x502 -x503 x504 x505 -x506 -x507 -x508 -x509 x510 x511 -x512 x513 -x514 x515 -x516 x517 -x518 x519 x520 -x521 -x522 x523 -x524 -x525 -x526 x527 x528 -x529 -x530 -x531 -x532 -x533 x534 -x535 -x536 -x537 x538 -x539 -x540 -x541 -x542 -x543 -x544 x545 -x546 x547 x548 -x549 -x550 -x551 x552 x553 x554 -x555 -x556 -x557 -x558 x559 -x560 -x561 x562 -x563 x564 x565 x566 x567 -x568 -x569 x570 -x571 -x572 -x573 x574 -x575 x576 x577 x578 -x579 -x580 x581 -x582 x583 -x584 -x585 -x586 x587 -x588 x589 -x590 -x591 -x592 -x593 x594 -x595 -x596 x597 -x598 -x599 -x600 x601 x602 x603 -x604 -x605 -x606 -x607 -x608 x609 x610 x611 x612 -x613 -x614 -x615 x616 -x617 -x618 -x619 -x620 -x621 -x622 x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 x632 -x633 x634 -x635 -x636 -x637 x638 x639 x640 x641 -x642 -x643 -x644 x645 x646 x647 -x648 x649 -x650 x651 -x652 -x653 -x654 -x655 x656 -x657 -x658 -x659 -x660 -x661 x662 -x663 x664 x665 x666 x667 -x668 x669 -x670 x671 x672 -x673 -x674 -x675 -x676 x677 x678 -x679 -x680 x681 -x682 x683 -x684 x685 -x686 -x687 x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 x705 -x706 -x707 -x708 x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 x718 x719 -x720 -x721 -x722 x723 -x724 -x725 x726 -x727 x728 x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x7
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/5347/stat): 5347 (minisat+_script) R 5346 5347 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843394801 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/5347/statm): 174 3 169 147 0 27 0 [pid=5347] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=5348 New process pid=5349 New process pid=5350 execve syscall for /bin/sed executable One traced child (pid=5349) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=5350) exited with status: 0 One traced child (pid=5348) exited with status: 0 New process pid=5351 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-seymour.opb [startup+10.0037 s] Raw data (loadavg): 0.96 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 4789 0 0 0 958 20 0 0 25 0 1 0 1843394806 21204992 4751 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 5177 4751 145 145 0 5032 0 [pid=5351] vsize: 20708 Current children cumulated CPU time (s) 9.79 Current children cumulated vsize (Kb) 22832 [startup+20.0046 s] Raw data (loadavg): 0.97 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 4941 0 0 0 1955 21 0 0 25 0 1 0 1843394806 21778432 4903 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 5317 4903 145 145 0 5172 0 [pid=5351] vsize: 21268 Current children cumulated CPU time (s) 19.77 Current children cumulated vsize (Kb) 23392 [startup+30.0056 s] Raw data (loadavg): 0.97 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5174 0 0 0 2951 23 0 0 25 0 1 0 1843394806 22740992 5136 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 5552 5136 145 145 0 5407 0 [pid=5351] vsize: 22208 Current children cumulated CPU time (s) 29.75 Current children cumulated vsize (Kb) 24332 [startup+40.0065 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5391 0 0 0 3948 24 0 0 25 0 1 0 1843394806 23658496 5353 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 5776 5353 145 145 0 5631 0 [pid=5351] vsize: 23104 Current children cumulated CPU time (s) 39.73 Current children cumulated vsize (Kb) 25228 [startup+50.0074 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5742 0 0 0 4942 27 0 0 25 0 1 0 1843394806 25079808 5704 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 6123 5704 145 145 0 5978 0 [pid=5351] vsize: 24492 Current children cumulated CPU time (s) 49.7 Current children cumulated vsize (Kb) 26616 [startup+60.0083 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 5974 0 0 0 5938 29 0 0 25 0 1 0 1843394806 26025984 5936 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 6354 5936 145 145 0 6209 0 [pid=5351] vsize: 25416 Current children cumulated CPU time (s) 59.68 Current children cumulated vsize (Kb) 27540 [startup+70.0093 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 6246 0 0 0 6932 32 0 0 25 0 1 0 1843394806 27119616 6208 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 6621 6208 145 145 0 6476 0 [pid=5351] vsize: 26484 Current children cumulated CPU time (s) 69.65 Current children cumulated vsize (Kb) 28608 [startup+80.0102 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 6528 0 0 0 7926 34 0 0 25 0 1 0 1843394806 28274688 6490 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 6903 6490 145 145 0 6758 0 [pid=5351] vsize: 27612 Current children cumulated CPU time (s) 79.61 Current children cumulated vsize (Kb) 29736 [startup+90.0111 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 6952 0 0 0 8919 36 0 0 25 0 1 0 1843394806 30117888 6914 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 7353 6914 145 145 0 7208 0 [pid=5351] vsize: 29412 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 31536 [startup+100.012 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 7276 0 0 0 9912 39 0 0 25 0 1 0 1843394806 31428608 7238 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 7673 7238 145 145 0 7528 0 [pid=5351] vsize: 30692 Current children cumulated CPU time (s) 99.52 Current children cumulated vsize (Kb) 32816 [startup+110.013 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 7581 0 0 0 10905 43 0 0 25 0 1 0 1843394806 32669696 7543 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 7976 7543 145 145 0 7831 0 [pid=5351] vsize: 31904 Current children cumulated CPU time (s) 109.49 Current children cumulated vsize (Kb) 34028 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 7925 0 0 0 11899 45 0 0 25 0 1 0 1843394806 34070528 7887 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 8318 7887 145 145 0 8173 0 [pid=5351] vsize: 33272 Current children cumulated CPU time (s) 119.45 Current children cumulated vsize (Kb) 35396 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 8270 0 0 0 12892 48 0 0 25 0 1 0 1843394806 35479552 8232 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 8662 8232 145 145 0 8517 0 [pid=5351] vsize: 34648 Current children cumulated CPU time (s) 129.41 Current children cumulated vsize (Kb) 36772 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 8628 0 0 0 13887 50 0 0 25 0 1 0 1843394806 36937728 8590 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 9018 8590 145 145 0 8873 0 [pid=5351] vsize: 36072 Current children cumulated CPU time (s) 139.38 Current children cumulated vsize (Kb) 38196 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 9006 0 0 0 14880 53 0 0 25 0 1 0 1843394806 38481920 8968 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 9395 8968 145 145 0 9250 0 [pid=5351] vsize: 37580 Current children cumulated CPU time (s) 149.34 Current children cumulated vsize (Kb) 39704 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 9348 0 0 0 15874 56 0 0 25 0 1 0 1843394806 39866368 9310 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 9733 9310 145 145 0 9588 0 [pid=5351] vsize: 38932 Current children cumulated CPU time (s) 159.31 Current children cumulated vsize (Kb) 41056 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 9707 0 0 0 16867 59 0 0 25 0 1 0 1843394806 41332736 9669 4294967295 134512640 135094434 3221224448 3221223040 134551711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 10091 9669 145 145 0 9946 0 [pid=5351] vsize: 40364 Current children cumulated CPU time (s) 169.27 Current children cumulated vsize (Kb) 42488 [startup+180.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 10064 0 0 0 17861 63 0 0 25 0 1 0 1843394806 42799104 10026 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 10449 10026 145 145 0 10304 0 [pid=5351] vsize: 41796 Current children cumulated CPU time (s) 179.25 Current children cumulated vsize (Kb) 43920 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 10351 0 0 0 18855 65 0 0 25 0 1 0 1843394806 43962368 10313 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 10733 10313 145 145 0 10588 0 [pid=5351] vsize: 42932 Current children cumulated CPU time (s) 189.21 Current children cumulated vsize (Kb) 45056 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 10864 0 0 0 19845 69 0 0 25 0 1 0 1843394806 46309376 10826 4294967295 134512640 135094434 3221224448 3221223040 134557178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 11306 10826 145 145 0 11161 0 [pid=5351] vsize: 45224 Current children cumulated CPU time (s) 199.15 Current children cumulated vsize (Kb) 47348 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 11462 0 0 0 20833 74 0 0 25 0 1 0 1843394806 48754688 11424 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 11903 11424 145 145 0 11758 0 [pid=5351] vsize: 47612 Current children cumulated CPU time (s) 209.08 Current children cumulated vsize (Kb) 49736 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 12037 0 0 0 21822 78 0 0 25 0 1 0 1843394806 51105792 11999 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 12477 11999 145 145 0 12332 0 [pid=5351] vsize: 49908 Current children cumulated CPU time (s) 219.01 Current children cumulated vsize (Kb) 52032 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 12567 0 0 0 22813 82 0 0 25 0 1 0 1843394806 53260288 12529 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 13003 12529 145 145 0 12858 0 [pid=5351] vsize: 52012 Current children cumulated CPU time (s) 228.96 Current children cumulated vsize (Kb) 54136 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 13109 0 0 0 23802 86 0 0 25 0 1 0 1843394806 55468032 13071 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 13542 13071 145 145 0 13397 0 [pid=5351] vsize: 54168 Current children cumulated CPU time (s) 238.89 Current children cumulated vsize (Kb) 56292 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 13656 0 0 0 24793 91 0 0 25 0 1 0 1843394806 57700352 13618 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 14087 13618 145 145 0 13942 0 [pid=5351] vsize: 56348 Current children cumulated CPU time (s) 248.85 Current children cumulated vsize (Kb) 58472 [startup+260.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 14144 0 0 0 25784 95 0 0 25 0 1 0 1843394806 59707392 14106 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 14577 14106 145 145 0 14432 0 [pid=5351] vsize: 58308 Current children cumulated CPU time (s) 258.8 Current children cumulated vsize (Kb) 60432 [startup+270.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 14627 0 0 0 26775 99 0 0 25 0 1 0 1843394806 61685760 14589 4294967295 134512640 135094434 3221224448 3221223100 134558036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 15060 14589 145 145 0 14915 0 [pid=5351] vsize: 60240 Current children cumulated CPU time (s) 268.75 Current children cumulated vsize (Kb) 62364 [startup+280.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 15075 0 0 0 27768 101 0 0 25 0 1 0 1843394806 63545344 15037 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 15514 15037 145 145 0 15369 0 [pid=5351] vsize: 62056 Current children cumulated CPU time (s) 278.7 Current children cumulated vsize (Kb) 64180 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 15485 0 0 0 28760 105 0 0 25 0 1 0 1843394806 65228800 15447 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 15925 15447 145 145 0 15780 0 [pid=5351] vsize: 63700 Current children cumulated CPU time (s) 288.66 Current children cumulated vsize (Kb) 65824 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 15679 0 0 0 29757 106 0 0 25 0 1 0 1843394806 66011136 15641 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 16116 15641 145 145 0 15971 0 [pid=5351] vsize: 64464 Current children cumulated CPU time (s) 298.64 Current children cumulated vsize (Kb) 66588 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16044 0 0 0 30750 109 0 0 25 0 1 0 1843394806 67497984 16006 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 16479 16006 145 145 0 16334 0 [pid=5351] vsize: 65916 Current children cumulated CPU time (s) 308.6 Current children cumulated vsize (Kb) 68040 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16393 0 0 0 31743 111 0 0 25 0 1 0 1843394806 68915200 16355 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 16825 16355 145 145 0 16680 0 [pid=5351] vsize: 67300 Current children cumulated CPU time (s) 318.55 Current children cumulated vsize (Kb) 69424 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16704 0 0 0 32738 113 0 0 25 0 1 0 1843394806 70168576 16666 4294967295 134512640 135094434 3221224448 3221223104 134558289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 17131 16666 145 145 0 16986 0 [pid=5351] vsize: 68524 Current children cumulated CPU time (s) 328.52 Current children cumulated vsize (Kb) 70648 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16841 0 0 0 33736 114 0 0 25 0 1 0 1843394806 70721536 16803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 17266 16803 145 145 0 17121 0 [pid=5351] vsize: 69064 Current children cumulated CPU time (s) 338.51 Current children cumulated vsize (Kb) 71188 [startup+350.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 16979 0 0 0 34732 116 0 0 25 0 1 0 1843394806 71290880 16941 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 17405 16941 145 145 0 17260 0 [pid=5351] vsize: 69620 Current children cumulated CPU time (s) 348.49 Current children cumulated vsize (Kb) 71744 [startup+360.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 17198 0 0 0 35728 117 0 0 25 0 1 0 1843394806 72171520 17160 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 17620 17160 145 145 0 17475 0 [pid=5351] vsize: 70480 Current children cumulated CPU time (s) 358.46 Current children cumulated vsize (Kb) 72604 [startup+370.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 17592 0 0 0 36721 120 0 0 25 0 1 0 1843394806 73777152 17554 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 18012 17554 145 145 0 17867 0 [pid=5351] vsize: 72048 Current children cumulated CPU time (s) 368.42 Current children cumulated vsize (Kb) 74172 [startup+380.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 18007 0 0 0 37712 124 0 0 25 0 1 0 1843394806 75472896 17969 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 18426 17969 145 145 0 18281 0 [pid=5351] vsize: 73704 Current children cumulated CPU time (s) 378.37 Current children cumulated vsize (Kb) 75828 [startup+390.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 18412 0 0 0 38704 128 0 0 25 0 1 0 1843394806 77123584 18374 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 18829 18374 145 145 0 18684 0 [pid=5351] vsize: 75316 Current children cumulated CPU time (s) 388.33 Current children cumulated vsize (Kb) 77440 [startup+400.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 18736 0 0 0 39697 130 0 0 25 0 1 0 1843394806 78442496 18698 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 19151 18698 145 145 0 19006 0 [pid=5351] vsize: 76604 Current children cumulated CPU time (s) 398.28 Current children cumulated vsize (Kb) 78728 [startup+410.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19064 0 0 0 40692 132 0 0 25 0 1 0 1843394806 79761408 19026 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 19473 19026 145 145 0 19328 0 [pid=5351] vsize: 77892 Current children cumulated CPU time (s) 408.25 Current children cumulated vsize (Kb) 80016 [startup+420.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19415 0 0 0 41685 135 0 0 25 0 1 0 1843394806 81182720 19377 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 19820 19377 145 145 0 19675 0 [pid=5351] vsize: 79280 Current children cumulated CPU time (s) 418.21 Current children cumulated vsize (Kb) 81404 [startup+430.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19593 0 0 0 42681 136 0 0 25 0 1 0 1843394806 82427904 19555 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 20124 19555 145 145 0 19979 0 [pid=5351] vsize: 80496 Current children cumulated CPU time (s) 428.18 Current children cumulated vsize (Kb) 82620 [startup+440.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 19754 0 0 0 43678 137 0 0 25 0 1 0 1843394806 83079168 19716 4294967295 134512640 135094434 3221224448 3221223088 134562108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 20283 19716 145 145 0 20138 0 [pid=5351] vsize: 81132 Current children cumulated CPU time (s) 438.16 Current children cumulated vsize (Kb) 83256 [startup+450.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 20041 0 0 0 44672 140 0 0 25 0 1 0 1843394806 84242432 20003 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 20567 20003 145 145 0 20422 0 [pid=5351] vsize: 82268 Current children cumulated CPU time (s) 448.13 Current children cumulated vsize (Kb) 84392 [startup+460.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 20380 0 0 0 45666 142 0 0 25 0 1 0 1843394806 85618688 20342 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 20903 20342 145 145 0 20758 0 [pid=5351] vsize: 83612 Current children cumulated CPU time (s) 458.09 Current children cumulated vsize (Kb) 85736 [startup+470.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 20759 0 0 0 46658 146 0 0 25 0 1 0 1843394806 87162880 20721 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 21280 20721 145 145 0 21135 0 [pid=5351] vsize: 85120 Current children cumulated CPU time (s) 468.05 Current children cumulated vsize (Kb) 87244 [startup+480.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 21166 0 0 0 47652 148 0 0 25 0 1 0 1843394806 88825856 21128 4294967295 134512640 135094434 3221224448 3221223040 134557221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 21686 21128 145 145 0 21541 0 [pid=5351] vsize: 86744 Current children cumulated CPU time (s) 478.01 Current children cumulated vsize (Kb) 88868 [startup+490.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 21515 0 0 0 48645 151 0 0 25 0 1 0 1843394806 90243072 21477 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 22032 21477 145 145 0 21887 0 [pid=5351] vsize: 88128 Current children cumulated CPU time (s) 487.97 Current children cumulated vsize (Kb) 90252 [startup+500.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 21865 0 0 0 49640 153 0 0 25 0 1 0 1843394806 91668480 21827 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 22380 21827 145 145 0 22235 0 [pid=5351] vsize: 89520 Current children cumulated CPU time (s) 497.94 Current children cumulated vsize (Kb) 91644 [startup+510.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 22204 0 0 0 50635 154 0 0 25 0 1 0 1843394806 93048832 22166 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 22717 22166 145 145 0 22572 0 [pid=5351] vsize: 90868 Current children cumulated CPU time (s) 507.9 Current children cumulated vsize (Kb) 92992 [startup+520.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 22545 0 0 0 51630 156 0 0 25 0 1 0 1843394806 94437376 22507 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 23056 22507 145 145 0 22911 0 [pid=5351] vsize: 92224 Current children cumulated CPU time (s) 517.87 Current children cumulated vsize (Kb) 94348 [startup+530.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 22888 0 0 0 52623 160 0 0 25 0 1 0 1843394806 95830016 22850 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 23396 22850 145 145 0 23251 0 [pid=5351] vsize: 93584 Current children cumulated CPU time (s) 527.84 Current children cumulated vsize (Kb) 95708 [startup+540.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 23229 0 0 0 53616 163 0 0 25 0 1 0 1843394806 97214464 23191 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 23734 23191 145 145 0 23589 0 [pid=5351] vsize: 94936 Current children cumulated CPU time (s) 537.8 Current children cumulated vsize (Kb) 97060 [startup+550.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 23548 0 0 0 54610 165 0 0 25 0 1 0 1843394806 98512896 23510 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24051 23510 145 145 0 23906 0 [pid=5351] vsize: 96204 Current children cumulated CPU time (s) 547.76 Current children cumulated vsize (Kb) 98328 [startup+560.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 23870 0 0 0 55604 167 0 0 25 0 1 0 1843394806 99823616 23832 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24371 23832 145 145 0 24226 0 [pid=5351] vsize: 97484 Current children cumulated CPU time (s) 557.72 Current children cumulated vsize (Kb) 99608 [startup+570.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24150 0 0 0 56598 170 0 0 25 0 1 0 1843394806 100966400 24112 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24650 24112 145 145 0 24505 0 [pid=5351] vsize: 98600 Current children cumulated CPU time (s) 567.69 Current children cumulated vsize (Kb) 100724 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 57595 171 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 577.67 Current children cumulated vsize (Kb) 101256 [startup+590.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 58595 172 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 587.68 Current children cumulated vsize (Kb) 101256 [startup+600.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 59595 172 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 597.68 Current children cumulated vsize (Kb) 101256 [startup+610.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 60595 172 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 607.68 Current children cumulated vsize (Kb) 101256 [startup+620.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 61594 173 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 617.68 Current children cumulated vsize (Kb) 101256 [startup+630.067 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 62594 173 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 627.68 Current children cumulated vsize (Kb) 101256 [startup+640.068 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 63593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 637.68 Current children cumulated vsize (Kb) 101256 [startup+650.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 64593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 647.68 Current children cumulated vsize (Kb) 101256 [startup+660.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 65593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 657.68 Current children cumulated vsize (Kb) 101256 [startup+670.072 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 66593 174 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 667.68 Current children cumulated vsize (Kb) 101256 [startup+680.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 67593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 677.69 Current children cumulated vsize (Kb) 101256 [startup+690.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 68593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 687.69 Current children cumulated vsize (Kb) 101256 [startup+700.074 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 69594 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 697.7 Current children cumulated vsize (Kb) 101256 [startup+710.075 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 70593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 707.69 Current children cumulated vsize (Kb) 101256 [startup+720.076 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24284 0 0 0 71593 175 0 0 25 0 1 0 1843394806 101511168 24246 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24246 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 717.69 Current children cumulated vsize (Kb) 101256 [startup+730.077 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 72594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 727.7 Current children cumulated vsize (Kb) 101256 [startup+740.079 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 73594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 737.7 Current children cumulated vsize (Kb) 101256 [startup+750.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 74594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 747.7 Current children cumulated vsize (Kb) 101256 [startup+760.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 75594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 757.7 Current children cumulated vsize (Kb) 101256 [startup+770.082 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 76594 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 767.7 Current children cumulated vsize (Kb) 101256 [startup+780.083 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 77595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 777.71 Current children cumulated vsize (Kb) 101256 [startup+790.084 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 78595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223040 134557157 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 787.71 Current children cumulated vsize (Kb) 101256 [startup+800.085 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 79595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 797.71 Current children cumulated vsize (Kb) 101256 [startup+810.086 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 80595 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 807.71 Current children cumulated vsize (Kb) 101256 [startup+820.087 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 81596 175 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 817.72 Current children cumulated vsize (Kb) 101256 [startup+830.087 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 82596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 827.73 Current children cumulated vsize (Kb) 101256 [startup+840.089 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 83596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 837.73 Current children cumulated vsize (Kb) 101256 [startup+850.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 84596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 847.73 Current children cumulated vsize (Kb) 101256 [startup+860.091 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 85596 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 857.73 Current children cumulated vsize (Kb) 101256 [startup+870.092 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 86597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 867.74 Current children cumulated vsize (Kb) 101256 [startup+880.093 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 87597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 877.74 Current children cumulated vsize (Kb) 101256 [startup+890.094 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 88597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 887.74 Current children cumulated vsize (Kb) 101256 [startup+900.095 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 89597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 897.74 Current children cumulated vsize (Kb) 101256 [startup+910.096 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 90597 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 907.74 Current children cumulated vsize (Kb) 101256 [startup+920.097 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 91598 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 917.75 Current children cumulated vsize (Kb) 101256 [startup+930.098 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 92598 176 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 927.75 Current children cumulated vsize (Kb) 101256 [startup+940.099 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24285 0 0 0 93597 177 0 0 25 0 1 0 1843394806 101511168 24247 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24247 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 937.75 Current children cumulated vsize (Kb) 101256 [startup+950.102 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 94597 177 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 947.75 Current children cumulated vsize (Kb) 101256 [startup+960.102 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 95597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 957.76 Current children cumulated vsize (Kb) 101256 [startup+970.103 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 96597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 967.76 Current children cumulated vsize (Kb) 101256 [startup+980.104 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 97597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 977.76 Current children cumulated vsize (Kb) 101256 [startup+990.105 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 98597 178 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 987.76 Current children cumulated vsize (Kb) 101256 [startup+1000.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 99597 179 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 997.77 Current children cumulated vsize (Kb) 101256 [startup+1010.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24286 0 0 0 100597 179 0 0 25 0 1 0 1843394806 101511168 24248 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24248 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1007.77 Current children cumulated vsize (Kb) 101256 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24289 0 0 0 101597 179 0 0 25 0 1 0 1843394806 101511168 24251 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24251 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1017.77 Current children cumulated vsize (Kb) 101256 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24293 0 0 0 102597 179 0 0 25 0 1 0 1843394806 101511168 24255 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24255 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1027.77 Current children cumulated vsize (Kb) 101256 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24295 0 0 0 103597 179 0 0 25 0 1 0 1843394806 101511168 24257 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24257 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1037.77 Current children cumulated vsize (Kb) 101256 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24297 0 0 0 104597 179 0 0 25 0 1 0 1843394806 101511168 24259 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24259 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1047.77 Current children cumulated vsize (Kb) 101256 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24300 0 0 0 105597 179 0 0 25 0 1 0 1843394806 101511168 24262 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24262 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1057.77 Current children cumulated vsize (Kb) 101256 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24303 0 0 0 106598 179 0 0 25 0 1 0 1843394806 101511168 24265 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24265 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1067.78 Current children cumulated vsize (Kb) 101256 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24306 0 0 0 107598 179 0 0 25 0 1 0 1843394806 101511168 24268 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24268 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1077.78 Current children cumulated vsize (Kb) 101256 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24309 0 0 0 108598 180 0 0 25 0 1 0 1843394806 101511168 24271 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24271 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1087.79 Current children cumulated vsize (Kb) 101256 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24312 0 0 0 109598 180 0 0 25 0 1 0 1843394806 101511168 24274 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24274 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1097.79 Current children cumulated vsize (Kb) 101256 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24315 0 0 0 110598 180 0 0 25 0 1 0 1843394806 101511168 24277 4294967295 134512640 135094434 3221224448 3221223040 134557215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24277 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1107.79 Current children cumulated vsize (Kb) 101256 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 111598 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1117.79 Current children cumulated vsize (Kb) 101256 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 112598 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1127.79 Current children cumulated vsize (Kb) 101256 [startup+1140.12 s] Raw data (loadavg): 1.07 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 113599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1137.8 Current children cumulated vsize (Kb) 101256 [startup+1150.12 s] Raw data (loadavg): 1.06 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 114599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557500 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1147.8 Current children cumulated vsize (Kb) 101256 [startup+1160.12 s] Raw data (loadavg): 1.05 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 115599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1157.8 Current children cumulated vsize (Kb) 101256 [startup+1170.12 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 116599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1167.8 Current children cumulated vsize (Kb) 101256 [startup+1180.12 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 117599 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1177.8 Current children cumulated vsize (Kb) 101256 [startup+1190.12 s] Raw data (loadavg): 1.03 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24319 0 0 0 118600 180 0 0 25 0 1 0 1843394806 101511168 24281 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24281 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1187.81 Current children cumulated vsize (Kb) 101256 [startup+1200.12 s] Raw data (loadavg): 1.03 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24320 0 0 0 119600 180 0 0 25 0 1 0 1843394806 101511168 24282 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24282 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1197.81 Current children cumulated vsize (Kb) 101256 [startup+1210.13 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24320 0 0 0 120600 180 0 0 25 0 1 0 1843394806 101511168 24282 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24282 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1207.81 Current children cumulated vsize (Kb) 101256 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 5351 Raw data (/proc/5347/stat): 5347 (minisat+_script) S 5346 5347 31027 0 -1 0 288 239 0 0 0 0 0 1 16 0 1 0 1843394801 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5347/statm): 531 226 485 147 0 384 0 [pid=5347] vsize: 2124 Raw data (/proc/5351/stat): 5351 (minisat+_64-bit) R 5347 5347 31027 0 -1 0 24320 0 0 0 120600 180 0 0 25 0 1 0 1843394806 101511168 24282 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5351/statm): 24783 24282 145 145 0 24638 0 [pid=5351] vsize: 99132 Current children cumulated CPU time (s) 1207.81 Current children cumulated vsize (Kb) 101256 Sending SIGTERM to -5347 Sleeping 2 seconds One traced child (pid=5347) ended because it received signal 15 (SIGTERM) One traced child (pid=5351) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.18 CPU time (s): 1207.87 CPU user time (s): 1206.01 CPU system time (s): 1.85572 CPU usage (%): 99.8089 Max. virtual memory (cumulated for all children) (Kb): 101256
ERROR: no interpretation found !