Name | submitted/manquinho/primes-dimacs-cnf/normalized-ii32e2.opb |
MD5SUM | 4e882bbd92f288daf6e68ac3de757136 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 235 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 534 |
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 | 534 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 534 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 1019.9 |
Number of variables | 534 |
Total number of constraints | 3013 |
Number of constraints which are clauses | 3013 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 32 |
LAUNCH ON wulflinc7 THE 2005-09-18 15:21:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2495 boxname=wulflinc7 idbench=151 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4e882bbd92f288daf6e68ac3de757136 /oldhome/oroussel/tmp/wulflinc7/normalized-ii32e2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-ii32e2.opb IDLAUNCH: 2495 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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: 924176 kB Buffers: 34676 kB Cached: 51556 kB SwapCached: 740 kB Active: 63748 kB Inactive: 25076 kB HighTotal: 131008 kB HighFree: 77392 kB LowTotal: 903652 kB LowFree: 846784 kB SwapTotal: 2097136 kB SwapFree: 2095892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 16080 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 15:38:34 (client local time) WITH STATUS 30 IN 1019.9 SECONDS stats: 2495 0 1019.9 30
c Parsing PB file... c Converting 3013 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 | 3013 12801 | 1004 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 262[0m c ---[ 0]---> Sorter-cost:23900 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51 | 30805 77844 | 10268 51 2400 47.1 | 0.000 % | c | 151 | 30805 77844 | 11294 151 7683 50.9 | 0.090 % | c ============================================================================== c [1mFound solution: 257[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 190 | 30889 78095 | 10296 190 9835 51.8 | 0.090 % | c ============================================================================== c [1mFound solution: 253[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 197 | 30957 78305 | 10319 197 10376 52.7 | 0.090 % | c ============================================================================== c [1mFound solution: 248[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 217 | 31010 78456 | 10336 217 11271 51.9 | 0.090 % | c ============================================================================== c [1mFound solution: 247[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 261 | 31057 78609 | 10352 261 16081 61.6 | 0.090 % | c | 364 | 31057 78609 | 11387 364 23432 64.4 | 0.168 % | c | 514 | 31057 78609 | 12525 514 35767 69.6 | 0.168 % | c | 739 | 31057 78609 | 13778 739 47564 64.4 | 0.168 % | c | 1077 | 31043 78581 | 15156 1076 61310 57.0 | 0.204 % | c | 1583 | 30033 76379 | 16671 1555 79058 50.8 | 3.324 % | c ============================================================================== c [1mFound solution: 237[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1871 | 29058 74332 | 9686 1041 57215 55.0 | 3.324 % | c | 1972 | 28682 73508 | 10654 1058 59764 56.5 | 7.930 % | c | 2123 | 28682 73508 | 11720 1209 70298 58.1 | 7.930 % | c | 2354 | 28353 72787 | 12892 1401 85328 60.9 | 8.925 % | c ============================================================================== c [1mFound solution: 236[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2489 | 28339 72734 | 9446 1536 96826 63.0 | 8.925 % | c | 2592 | 28339 72734 | 10390 1639 107066 65.3 | 8.992 % | c | 2743 | 28300 72651 | 11429 1789 114183 63.8 | 9.107 % | c | 2968 | 28300 72651 | 12572 2014 128271 63.7 | 9.107 % | c | 3307 | 28300 72651 | 13829 2353 149449 63.5 | 9.107 % | c | 3813 | 28300 72651 | 15212 2859 182051 63.7 | 9.107 % | c | 4572 | 28300 72651 | 16734 3618 227872 63.0 | 9.107 % | c | 5711 | 28173 72368 | 18407 4754 304798 64.1 | 9.508 % | c | 7421 | 28173 72368 | 20248 6464 500803 77.5 | 9.508 % | c | 9983 | 28066 72133 | 22273 9024 799303 88.6 | 9.841 % | c | 13827 | 26943 69655 | 24500 12678 1123449 88.6 | 13.306 % | c | 19593 | 26893 69543 | 26950 18439 1901996 103.2 | 13.467 % | c | 28242 | 26893 69543 | 29645 27088 2311712 85.3 | 13.467 % | c ============================================================================== c [1mFound solution: 235[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29784 | 26881 69544 | 8960 28628 2403453 84.0 | 13.467 % | c | 29886 | 26881 69544 | 9856 7078 305430 43.2 | 13.633 % | c | 30036 | 26881 69544 | 10841 7228 317592 43.9 | 13.633 % | c | 30263 | 26881 69544 | 11925 7455 333607 44.7 | 13.633 % | c | 30600 | 26881 69544 | 13118 7792 351854 45.2 | 13.633 % | c | 31107 | 26881 69544 | 14430 8299 371120 44.7 | 13.633 % | c | 31868 | 26881 69544 | 15873 9060 438646 48.4 | 13.633 % | c | 33012 | 26881 69544 | 17460 10204 557761 54.7 | 13.633 % | c | 34723 | 26408 68497 | 19206 11893 664066 55.8 | 15.095 % | c | 37289 | 26408 68497 | 21127 14459 848035 58.7 | 15.095 % | c | 41134 | 26408 68497 | 23239 18304 1221768 66.7 | 15.095 % | c | 46900 | 26408 68497 | 25563 24070 2008829 83.5 | 15.095 % | c | 55549 | 26408 68497 | 28120 17501 1701959 97.2 | 15.095 % | c | 68524 | 26408 68497 | 30932 30476 2370240 77.8 | 15.095 % | c | 87985 | 26406 68493 | 34025 30974 3035243 98.0 | 15.100 % | c | 117177 | 26406 68493 | 37428 37118 3558879 95.9 | 15.100 % | c | 160967 | 26280 68218 | 41170 27331 2546708 93.2 | 15.480 % | c | 226652 | 26280 68218 | 45288 35899 4002336 111.5 | 15.480 % | c ============================================================================== c [1mOptimal solution: 235[0m s OPTIMUM FOUND v x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 -x113 x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 -x123 x124 x125 -x126 x127 -x128 x129 -x130 -x131 -x132 x133 -x134 -x135 -x136 -x137 -x138 x139 -x140 x141 -x142 -x143 -x144 -x145 -x146 x147 -x148 -x149 -x150 x151 -x152 -x153 -x154 x155 -x156 x157 -x158 -x159 -x160 -x161 -x162 x163 -x164 -x165 -x166 x167 -x168 -x169 -x170 x171 -x172 -x173 -x174 x175 -x176 -x177 -x178 x179 -x180 -x181 x182 x183 -x184 -x185 -x186 x187 -x188 x189 -x190 -x191 x192 x193 -x194 -x195 -x196 x197 -x198 -x199 -x200 x201 -x202 -x203 -x204 -x205 -x206 x207 -x208 x209 -x210 -x211 -x212 -x213 -x214 x215 -x216 -x217 x218 x219 -x220 -x221 -x222 x223 -x224 x225 -x226 -x227 -x228 -x229 -x230 x231 -x232 -x233 -x234 x235 -x236 x237 -x238 -x239 -x240 x241 -x242 -x243 -x244 x245 -x246 -x247 -x248 x249 -x250 -x251 -x252 x253 -x254 -x255 -x256 x257 -x258 x259 -x260 x261 -x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 -x289 x290 x291 -x292 -x293 x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 x321 -x322 x323 -x324 x325 -x326 x327 -x328 x329 -x330 x331 -x332 x333 -x334 x335 -x336 x337 -x338 x339 -x340 x341 -x342 x343 -x344 -x345 x346 x347 -x348 x349 -x350 x351 -x352 x353 -x354 x355 -x356 x357 -x358 x359 -x360 x361 -x362 x363 -x364 x365 -x366 x367 -x368 x369 -x370 x371 -x372 x373 -x374 x375 -x376 x377 -x378 x379 -x380 x381 -x382 x383 -x384 x385 -x386 -x387 x388 -x389 x390 x391 -x392 -x393 x394 -x395 x396 -x397 x398 -x399 x400 x401 -x402 x403 -x404 -x405 x406 -x407 x408 x409 -x410 -x411 x412 -x413 -x414 x415 -x416 -x417 x418 -x419 x420 x421 -x422 -x423 x424 -x425 x426 x427 -x428 -x429 x430 -x431 x432 x433 -x434 -x435 x436 -x437 x438 x439 -x440 -x441 x442 -x443 x444 -x445 x446 -x447 x448 x449 -x450 x451 -x452 -x453 x454 -x455 x456 -x457 x458 -x459 x460 x461 -x462 -x463 x464 -x465 x466 x467 -x468 -x469 x470 -x471 -x472 x473 -x474 -x475 x476 -x477 x478 x479 -x480 -x481 x482 -x483 x484 x485 -x486 -x487 x488 -x489 x490 x491 -x492 x493 -x494 -x495 x496 -x497 x498 -x499 x500 -x501 x502 x503 -x504 -x505 -x506 -x507 x508 x509 -x510 x511 -x512 -x513 x514 -x515 x516 x517 -x518 -x519 x520 -x521 x522 x523 -x524 -x525 x526 -x527 x528 -x529 x530 -x531 x532 x533 -x534 c _______________________________________________________________________________ c c restarts : 47 c conflicts : 277669 (272 /sec) c decisions : 528086 (518 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 1019.17 s c _______________________________________________________________________________
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/19429/stat): 19429 (minisat+_script) R 19428 19429 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784091329 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/19429/statm): 174 3 169 147 0 27 0 [pid=19429] 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=19430 New process pid=19431 New process pid=19432 execve syscall for /bin/sed executable One traced child (pid=19431) 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=19432) exited with status: 0 One traced child (pid=19430) exited with status: 0 New process pid=19433 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-ii32e2.opb [startup+10.004 s] Raw data (loadavg): 0.87 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 2058 0 0 0 976 9 0 0 25 0 1 0 1784091334 9592832 2034 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19433/statm): 2342 2034 145 145 0 2197 0 [pid=19433] vsize: 9368 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 11492 [startup+20.0047 s] Raw data (loadavg): 0.89 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 2580 0 0 0 1966 13 0 0 25 0 1 0 1784091334 11751424 2556 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 2869 2556 145 145 0 2724 0 [pid=19433] vsize: 11476 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 13600 [startup+30.0053 s] Raw data (loadavg): 0.91 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 3039 0 0 0 2956 16 0 0 25 0 1 0 1784091334 13619200 3015 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 3325 3015 145 145 0 3180 0 [pid=19433] vsize: 13300 Current children cumulated CPU time (s) 29.72 Current children cumulated vsize (Kb) 15424 [startup+40.0049 s] Raw data (loadavg): 0.92 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 3551 0 0 0 3948 21 0 0 25 0 1 0 1784091334 15761408 3527 4294967295 134512640 135094434 3221224448 3221223040 134557213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 3848 3527 145 145 0 3703 0 [pid=19433] vsize: 15392 Current children cumulated CPU time (s) 39.69 Current children cumulated vsize (Kb) 17516 [startup+50.0065 s] Raw data (loadavg): 0.93 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 3937 0 0 0 4941 24 0 0 25 0 1 0 1784091334 17330176 3913 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4231 3913 145 145 0 4086 0 [pid=19433] vsize: 16924 Current children cumulated CPU time (s) 49.65 Current children cumulated vsize (Kb) 19048 [startup+60.0072 s] Raw data (loadavg): 0.94 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4164 0 0 0 5936 26 0 0 23 0 1 0 1784091334 18247680 4140 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4455 4140 145 145 0 4310 0 [pid=19433] vsize: 17820 Current children cumulated CPU time (s) 59.62 Current children cumulated vsize (Kb) 19944 [startup+70.0078 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4428 0 0 0 6932 28 0 0 25 0 1 0 1784091334 19316736 4404 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4716 4404 145 145 0 4571 0 [pid=19433] vsize: 18864 Current children cumulated CPU time (s) 69.6 Current children cumulated vsize (Kb) 20988 [startup+80.0085 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4517 0 0 0 7931 29 0 0 25 0 1 0 1784091334 19677184 4493 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4804 4493 145 145 0 4659 0 [pid=19433] vsize: 19216 Current children cumulated CPU time (s) 79.6 Current children cumulated vsize (Kb) 21340 [startup+90.0091 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4517 0 0 0 8930 30 0 0 25 0 1 0 1784091334 19677184 4493 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4804 4493 145 145 0 4659 0 [pid=19433] vsize: 19216 Current children cumulated CPU time (s) 89.6 Current children cumulated vsize (Kb) 21340 [startup+100.01 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4517 0 0 0 9931 30 0 0 25 0 1 0 1784091334 19677184 4493 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4804 4493 145 145 0 4659 0 [pid=19433] vsize: 19216 Current children cumulated CPU time (s) 99.61 Current children cumulated vsize (Kb) 21340 [startup+110.012 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4517 0 0 0 10930 30 0 0 25 0 1 0 1784091334 19677184 4493 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4804 4493 145 145 0 4659 0 [pid=19433] vsize: 19216 Current children cumulated CPU time (s) 109.6 Current children cumulated vsize (Kb) 21340 [startup+120.013 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4517 0 0 0 11930 31 0 0 25 0 1 0 1784091334 19677184 4493 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4804 4493 145 145 0 4659 0 [pid=19433] vsize: 19216 Current children cumulated CPU time (s) 119.61 Current children cumulated vsize (Kb) 21340 [startup+130.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4540 0 0 0 12929 31 0 0 25 0 1 0 1784091334 19771392 4516 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 4827 4516 145 145 0 4682 0 [pid=19433] vsize: 19308 Current children cumulated CPU time (s) 129.6 Current children cumulated vsize (Kb) 21432 [startup+140.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4726 0 0 0 13926 32 0 0 25 0 1 0 1784091334 20529152 4702 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5012 4702 145 145 0 4867 0 [pid=19433] vsize: 20048 Current children cumulated CPU time (s) 139.58 Current children cumulated vsize (Kb) 22172 [startup+150.016 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4758 0 0 0 14926 32 0 0 25 0 1 0 1784091334 20692992 4734 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5052 4734 145 145 0 4907 0 [pid=19433] vsize: 20208 Current children cumulated CPU time (s) 149.58 Current children cumulated vsize (Kb) 22332 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4788 0 0 0 15926 32 0 0 25 0 1 0 1784091334 20824064 4764 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5084 4764 145 145 0 4939 0 [pid=19433] vsize: 20336 Current children cumulated CPU time (s) 159.58 Current children cumulated vsize (Kb) 22460 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4806 0 0 0 16926 33 0 0 25 0 1 0 1784091334 20922368 4782 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5108 4782 145 145 0 4963 0 [pid=19433] vsize: 20432 Current children cumulated CPU time (s) 169.59 Current children cumulated vsize (Kb) 22556 [startup+180.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 4816 0 0 0 17926 33 0 0 25 0 1 0 1784091334 20971520 4792 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5120 4792 145 145 0 4975 0 [pid=19433] vsize: 20480 Current children cumulated CPU time (s) 179.59 Current children cumulated vsize (Kb) 22604 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5153 0 0 0 18921 34 0 0 25 0 1 0 1784091334 22474752 5129 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5487 5129 145 145 0 5342 0 [pid=19433] vsize: 21948 Current children cumulated CPU time (s) 189.55 Current children cumulated vsize (Kb) 24072 [startup+200.019 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5218 0 0 0 19920 35 0 0 25 0 1 0 1784091334 22740992 5194 4294967295 134512640 135094434 3221224448 3221223104 134555980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5552 5194 145 145 0 5407 0 [pid=19433] vsize: 22208 Current children cumulated CPU time (s) 199.55 Current children cumulated vsize (Kb) 24332 [startup+210.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5218 0 0 0 20920 35 0 0 25 0 1 0 1784091334 22740992 5194 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5552 5194 145 145 0 5407 0 [pid=19433] vsize: 22208 Current children cumulated CPU time (s) 209.55 Current children cumulated vsize (Kb) 24332 [startup+220.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5218 0 0 0 21920 35 0 0 25 0 1 0 1784091334 22740992 5194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5552 5194 145 145 0 5407 0 [pid=19433] vsize: 22208 Current children cumulated CPU time (s) 219.55 Current children cumulated vsize (Kb) 24332 [startup+230.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5218 0 0 0 22920 35 0 0 25 0 1 0 1784091334 22740992 5194 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5552 5194 145 145 0 5407 0 [pid=19433] vsize: 22208 Current children cumulated CPU time (s) 229.55 Current children cumulated vsize (Kb) 24332 [startup+240.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5406 0 0 0 23917 37 0 0 25 0 1 0 1784091334 23511040 5382 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 5740 5382 145 145 0 5595 0 [pid=19433] vsize: 22960 Current children cumulated CPU time (s) 239.54 Current children cumulated vsize (Kb) 25084 [startup+250.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5670 0 0 0 24912 39 0 0 25 0 1 0 1784091334 24588288 5646 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6003 5646 145 145 0 5858 0 [pid=19433] vsize: 24012 Current children cumulated CPU time (s) 249.51 Current children cumulated vsize (Kb) 26136 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 5963 0 0 0 25906 41 0 0 25 0 1 0 1784091334 25784320 5939 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6295 5939 145 145 0 6150 0 [pid=19433] vsize: 25180 Current children cumulated CPU time (s) 259.47 Current children cumulated vsize (Kb) 27304 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6309 0 0 0 26898 45 0 0 22 0 1 0 1784091334 27189248 6285 4294967295 134512640 135094434 3221224448 3221223040 134557302 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6638 6285 145 145 0 6493 0 [pid=19433] vsize: 26552 Current children cumulated CPU time (s) 269.43 Current children cumulated vsize (Kb) 28676 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6568 0 0 0 27893 47 0 0 25 0 1 0 1784091334 28241920 6544 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6895 6544 145 145 0 6750 0 [pid=19433] vsize: 27580 Current children cumulated CPU time (s) 279.4 Current children cumulated vsize (Kb) 29704 [startup+290.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6568 0 0 0 28893 47 0 0 25 0 1 0 1784091334 28241920 6544 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6895 6544 145 145 0 6750 0 [pid=19433] vsize: 27580 Current children cumulated CPU time (s) 289.4 Current children cumulated vsize (Kb) 29704 [startup+300.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6568 0 0 0 29893 47 0 0 25 0 1 0 1784091334 28241920 6544 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6895 6544 145 145 0 6750 0 [pid=19433] vsize: 27580 Current children cumulated CPU time (s) 299.4 Current children cumulated vsize (Kb) 29704 [startup+310.026 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6573 0 0 0 30894 47 0 0 25 0 1 0 1784091334 28274688 6549 4294967295 134512640 135094434 3221224448 3221223072 134562122 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6903 6549 145 145 0 6758 0 [pid=19433] vsize: 27612 Current children cumulated CPU time (s) 309.41 Current children cumulated vsize (Kb) 29736 [startup+320.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6573 0 0 0 31894 47 0 0 25 0 1 0 1784091334 28274688 6549 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6903 6549 145 145 0 6758 0 [pid=19433] vsize: 27612 Current children cumulated CPU time (s) 319.41 Current children cumulated vsize (Kb) 29736 [startup+330.028 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6583 0 0 0 32894 47 0 0 25 0 1 0 1784091334 28340224 6559 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6919 6559 145 145 0 6774 0 [pid=19433] vsize: 27676 Current children cumulated CPU time (s) 329.41 Current children cumulated vsize (Kb) 29800 [startup+340.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6592 0 0 0 33894 47 0 0 25 0 1 0 1784091334 28405760 6568 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6935 6568 145 145 0 6790 0 [pid=19433] vsize: 27740 Current children cumulated CPU time (s) 339.41 Current children cumulated vsize (Kb) 29864 [startup+350.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6593 0 0 0 34895 47 0 0 25 0 1 0 1784091334 28405760 6569 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6935 6569 145 145 0 6790 0 [pid=19433] vsize: 27740 Current children cumulated CPU time (s) 349.42 Current children cumulated vsize (Kb) 29864 [startup+360.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6594 0 0 0 35895 47 0 0 25 0 1 0 1784091334 28405760 6570 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 6935 6570 145 145 0 6790 0 [pid=19433] vsize: 27740 Current children cumulated CPU time (s) 359.42 Current children cumulated vsize (Kb) 29864 [startup+370.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 36889 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 369.39 Current children cumulated vsize (Kb) 31284 [startup+380.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 37889 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 379.39 Current children cumulated vsize (Kb) 31284 [startup+390.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 38889 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 389.39 Current children cumulated vsize (Kb) 31284 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 39890 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 399.4 Current children cumulated vsize (Kb) 31284 [startup+410.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 40890 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 409.4 Current children cumulated vsize (Kb) 31284 [startup+420.034 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 41890 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 419.4 Current children cumulated vsize (Kb) 31284 [startup+430.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 42890 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 429.4 Current children cumulated vsize (Kb) 31284 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6951 0 0 0 43890 50 0 0 25 0 1 0 1784091334 29859840 6927 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7290 6927 145 145 0 7145 0 [pid=19433] vsize: 29160 Current children cumulated CPU time (s) 439.4 Current children cumulated vsize (Kb) 31284 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 6963 0 0 0 44891 50 0 0 25 0 1 0 1784091334 29925376 6939 4294967295 134512640 135094434 3221224448 3221223120 134555232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7306 6939 145 145 0 7161 0 [pid=19433] vsize: 29224 Current children cumulated CPU time (s) 449.41 Current children cumulated vsize (Kb) 31348 [startup+460.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7154 0 0 0 45887 51 0 0 25 0 1 0 1784091334 30707712 7130 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19433/statm): 7497 7130 145 145 0 7352 0 [pid=19433] vsize: 29988 Current children cumulated CPU time (s) 459.38 Current children cumulated vsize (Kb) 32112 [startup+470.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7434 0 0 0 46881 54 0 0 25 0 1 0 1784091334 31850496 7410 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7776 7410 145 145 0 7631 0 [pid=19433] vsize: 31104 Current children cumulated CPU time (s) 469.35 Current children cumulated vsize (Kb) 33228 [startup+480.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7531 0 0 0 47880 55 0 0 25 0 1 0 1784091334 32247808 7507 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7873 7507 145 145 0 7728 0 [pid=19433] vsize: 31492 Current children cumulated CPU time (s) 479.35 Current children cumulated vsize (Kb) 33616 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7531 0 0 0 48880 55 0 0 25 0 1 0 1784091334 32247808 7507 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/19433/statm): 7873 7507 145 145 0 7728 0 [pid=19433] vsize: 31492 Current children cumulated CPU time (s) 489.35 Current children cumulated vsize (Kb) 33616 [startup+500.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7531 0 0 0 49879 55 0 0 25 0 1 0 1784091334 32247808 7507 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7873 7507 145 145 0 7728 0 [pid=19433] vsize: 31492 Current children cumulated CPU time (s) 499.34 Current children cumulated vsize (Kb) 33616 [startup+510.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7531 0 0 0 50879 55 0 0 25 0 1 0 1784091334 32247808 7507 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7873 7507 145 145 0 7728 0 [pid=19433] vsize: 31492 Current children cumulated CPU time (s) 509.34 Current children cumulated vsize (Kb) 33616 [startup+520.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7531 0 0 0 51879 55 0 0 25 0 1 0 1784091334 32247808 7507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7873 7507 145 145 0 7728 0 [pid=19433] vsize: 31492 Current children cumulated CPU time (s) 519.34 Current children cumulated vsize (Kb) 33616 [startup+530.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7531 0 0 0 52880 55 0 0 25 0 1 0 1784091334 32247808 7507 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7873 7507 145 145 0 7728 0 [pid=19433] vsize: 31492 Current children cumulated CPU time (s) 529.35 Current children cumulated vsize (Kb) 33616 [startup+540.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7531 0 0 0 53880 55 0 0 25 0 1 0 1784091334 32247808 7507 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7873 7507 145 145 0 7728 0 [pid=19433] vsize: 31492 Current children cumulated CPU time (s) 539.35 Current children cumulated vsize (Kb) 33616 [startup+550.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7537 0 0 0 54880 55 0 0 25 0 1 0 1784091334 32280576 7513 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7881 7513 145 145 0 7736 0 [pid=19433] vsize: 31524 Current children cumulated CPU time (s) 549.35 Current children cumulated vsize (Kb) 33648 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7571 0 0 0 55880 55 0 0 25 0 1 0 1784091334 32477184 7547 4294967295 134512640 135094434 3221224448 3221223040 134557199 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7929 7547 145 145 0 7784 0 [pid=19433] vsize: 31716 Current children cumulated CPU time (s) 559.35 Current children cumulated vsize (Kb) 33840 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7590 0 0 0 56880 56 0 0 25 0 1 0 1784091334 32575488 7566 4294967295 134512640 135094434 3221224448 3221223040 134557031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7953 7566 145 145 0 7808 0 [pid=19433] vsize: 31812 Current children cumulated CPU time (s) 569.36 Current children cumulated vsize (Kb) 33936 [startup+580.045 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7602 0 0 0 57881 56 0 0 25 0 1 0 1784091334 32641024 7578 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7578 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 579.37 Current children cumulated vsize (Kb) 34000 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7604 0 0 0 58881 56 0 0 25 0 1 0 1784091334 32641024 7580 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7580 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 589.37 Current children cumulated vsize (Kb) 34000 [startup+600.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 59881 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 599.37 Current children cumulated vsize (Kb) 34000 [startup+610.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 60881 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 609.37 Current children cumulated vsize (Kb) 34000 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 61882 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223120 134555294 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 619.38 Current children cumulated vsize (Kb) 34000 [startup+630.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 62882 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 629.38 Current children cumulated vsize (Kb) 34000 [startup+640.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 63882 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 639.38 Current children cumulated vsize (Kb) 34000 [startup+650.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 64882 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 649.38 Current children cumulated vsize (Kb) 34000 [startup+660.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 65882 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 659.38 Current children cumulated vsize (Kb) 34000 [startup+670.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 66883 56 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 669.39 Current children cumulated vsize (Kb) 34000 [startup+680.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 67882 57 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223040 134785070 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 679.39 Current children cumulated vsize (Kb) 34000 [startup+690.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 68882 57 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 689.39 Current children cumulated vsize (Kb) 34000 [startup+700.053 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7605 0 0 0 69882 57 0 0 25 0 1 0 1784091334 32641024 7581 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7581 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 699.39 Current children cumulated vsize (Kb) 34000 [startup+710.053 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7606 0 0 0 70882 57 0 0 25 0 1 0 1784091334 32641024 7582 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7582 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 709.39 Current children cumulated vsize (Kb) 34000 [startup+720.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7606 0 0 0 71882 57 0 0 25 0 1 0 1784091334 32641024 7582 4294967295 134512640 135094434 3221224448 3221223104 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7582 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 719.39 Current children cumulated vsize (Kb) 34000 [startup+730.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7606 0 0 0 72882 58 0 0 25 0 1 0 1784091334 32641024 7582 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7969 7582 145 145 0 7824 0 [pid=19433] vsize: 31876 Current children cumulated CPU time (s) 729.4 Current children cumulated vsize (Kb) 34000 [startup+740.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7609 0 0 0 73882 58 0 0 25 0 1 0 1784091334 32657408 7585 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7973 7585 145 145 0 7828 0 [pid=19433] vsize: 31892 Current children cumulated CPU time (s) 739.4 Current children cumulated vsize (Kb) 34016 [startup+750.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7615 0 0 0 74883 58 0 0 25 0 1 0 1784091334 32690176 7591 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7981 7591 145 145 0 7836 0 [pid=19433] vsize: 31924 Current children cumulated CPU time (s) 749.41 Current children cumulated vsize (Kb) 34048 [startup+760.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7616 0 0 0 75883 58 0 0 25 0 1 0 1784091334 32690176 7592 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7981 7592 145 145 0 7836 0 [pid=19433] vsize: 31924 Current children cumulated CPU time (s) 759.41 Current children cumulated vsize (Kb) 34048 [startup+770.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7624 0 0 0 76883 58 0 0 25 0 1 0 1784091334 32735232 7600 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 7992 7600 145 145 0 7847 0 [pid=19433] vsize: 31968 Current children cumulated CPU time (s) 769.41 Current children cumulated vsize (Kb) 34092 [startup+780.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7634 0 0 0 77883 58 0 0 25 0 1 0 1784091334 32784384 7610 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8004 7610 145 145 0 7859 0 [pid=19433] vsize: 32016 Current children cumulated CPU time (s) 779.41 Current children cumulated vsize (Kb) 34140 [startup+790.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7634 0 0 0 78883 58 0 0 25 0 1 0 1784091334 32784384 7610 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8004 7610 145 145 0 7859 0 [pid=19433] vsize: 32016 Current children cumulated CPU time (s) 789.41 Current children cumulated vsize (Kb) 34140 [startup+800.061 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7634 0 0 0 79883 59 0 0 25 0 1 0 1784091334 32784384 7610 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8004 7610 145 145 0 7859 0 [pid=19433] vsize: 32016 Current children cumulated CPU time (s) 799.42 Current children cumulated vsize (Kb) 34140 [startup+810.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7634 0 0 0 80883 59 0 0 25 0 1 0 1784091334 32784384 7610 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8004 7610 145 145 0 7859 0 [pid=19433] vsize: 32016 Current children cumulated CPU time (s) 809.42 Current children cumulated vsize (Kb) 34140 [startup+820.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7655 0 0 0 81883 59 0 0 25 0 1 0 1784091334 32899072 7631 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8032 7631 145 145 0 7887 0 [pid=19433] vsize: 32128 Current children cumulated CPU time (s) 819.42 Current children cumulated vsize (Kb) 34252 [startup+830.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7727 0 0 0 82882 59 0 0 25 0 1 0 1784091334 33193984 7703 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8104 7703 145 145 0 7959 0 [pid=19433] vsize: 32416 Current children cumulated CPU time (s) 829.41 Current children cumulated vsize (Kb) 34540 [startup+840.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 7900 0 0 0 83880 60 0 0 25 0 1 0 1784091334 33898496 7876 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8276 7876 145 145 0 8131 0 [pid=19433] vsize: 33104 Current children cumulated CPU time (s) 839.4 Current children cumulated vsize (Kb) 35228 [startup+850.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8103 0 0 0 84876 62 0 0 25 0 1 0 1784091334 34729984 8079 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8479 8079 145 145 0 8334 0 [pid=19433] vsize: 33916 Current children cumulated CPU time (s) 849.38 Current children cumulated vsize (Kb) 36040 [startup+860.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8375 0 0 0 85871 64 0 0 25 0 1 0 1784091334 35835904 8351 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8749 8351 145 145 0 8604 0 [pid=19433] vsize: 34996 Current children cumulated CPU time (s) 859.35 Current children cumulated vsize (Kb) 37120 [startup+870.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8592 0 0 0 86867 66 0 0 25 0 1 0 1784091334 36712448 8568 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8963 8568 145 145 0 8818 0 [pid=19433] vsize: 35852 Current children cumulated CPU time (s) 869.33 Current children cumulated vsize (Kb) 37976 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8592 0 0 0 87867 66 0 0 25 0 1 0 1784091334 36712448 8568 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8963 8568 145 145 0 8818 0 [pid=19433] vsize: 35852 Current children cumulated CPU time (s) 879.33 Current children cumulated vsize (Kb) 37976 [startup+890.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8592 0 0 0 88867 66 0 0 25 0 1 0 1784091334 36712448 8568 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8963 8568 145 145 0 8818 0 [pid=19433] vsize: 35852 Current children cumulated CPU time (s) 889.33 Current children cumulated vsize (Kb) 37976 [startup+900.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8598 0 0 0 89867 66 0 0 25 0 1 0 1784091334 36745216 8574 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8971 8574 145 145 0 8826 0 [pid=19433] vsize: 35884 Current children cumulated CPU time (s) 899.33 Current children cumulated vsize (Kb) 38008 [startup+910.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8598 0 0 0 90867 66 0 0 25 0 1 0 1784091334 36745216 8574 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8971 8574 145 145 0 8826 0 [pid=19433] vsize: 35884 Current children cumulated CPU time (s) 909.33 Current children cumulated vsize (Kb) 38008 [startup+920.069 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8598 0 0 0 91868 66 0 0 25 0 1 0 1784091334 36745216 8574 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8971 8574 145 145 0 8826 0 [pid=19433] vsize: 35884 Current children cumulated CPU time (s) 919.34 Current children cumulated vsize (Kb) 38008 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8598 0 0 0 92868 66 0 0 25 0 1 0 1784091334 36745216 8574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8971 8574 145 145 0 8826 0 [pid=19433] vsize: 35884 Current children cumulated CPU time (s) 929.34 Current children cumulated vsize (Kb) 38008 [startup+940.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8601 0 0 0 93868 66 0 0 25 0 1 0 1784091334 36761600 8577 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8975 8577 145 145 0 8830 0 [pid=19433] vsize: 35900 Current children cumulated CPU time (s) 939.34 Current children cumulated vsize (Kb) 38024 [startup+950.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8601 0 0 0 94868 66 0 0 25 0 1 0 1784091334 36761600 8577 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8975 8577 145 145 0 8830 0 [pid=19433] vsize: 35900 Current children cumulated CPU time (s) 949.34 Current children cumulated vsize (Kb) 38024 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8607 0 0 0 95868 67 0 0 25 0 1 0 1784091334 36794368 8583 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 8983 8583 145 145 0 8838 0 [pid=19433] vsize: 35932 Current children cumulated CPU time (s) 959.35 Current children cumulated vsize (Kb) 38056 [startup+970.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8628 0 0 0 96869 67 0 0 25 0 1 0 1784091334 36892672 8604 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 9007 8604 145 145 0 8862 0 [pid=19433] vsize: 36028 Current children cumulated CPU time (s) 969.36 Current children cumulated vsize (Kb) 38152 [startup+980.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8631 0 0 0 97869 67 0 0 25 0 1 0 1784091334 36892672 8607 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 9007 8607 145 145 0 8862 0 [pid=19433] vsize: 36028 Current children cumulated CPU time (s) 979.36 Current children cumulated vsize (Kb) 38152 [startup+990.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8652 0 0 0 98869 67 0 0 25 0 1 0 1784091334 37056512 8628 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 9047 8628 145 145 0 8902 0 [pid=19433] vsize: 36188 Current children cumulated CPU time (s) 989.36 Current children cumulated vsize (Kb) 38312 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8672 0 0 0 99869 67 0 0 25 0 1 0 1784091334 37154816 8648 4294967295 134512640 135094434 3221224448 3221223072 134562144 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 9071 8648 145 145 0 8926 0 [pid=19433] vsize: 36284 Current children cumulated CPU time (s) 999.36 Current children cumulated vsize (Kb) 38408 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8672 0 0 0 100870 67 0 0 25 0 1 0 1784091334 37154816 8648 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 9071 8648 145 145 0 8926 0 [pid=19433] vsize: 36284 Current children cumulated CPU time (s) 1009.37 Current children cumulated vsize (Kb) 38408 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 19433 Raw data (/proc/19429/stat): 19429 (minisat+_script) S 19428 19429 15400 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1784091329 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/19429/statm): 531 226 485 147 0 384 0 [pid=19429] vsize: 2124 Raw data (/proc/19433/stat): 19433 (minisat+_64-bit) R 19429 19429 15400 0 -1 0 8672 0 0 0 101870 67 0 0 25 0 1 0 1784091334 37154816 8648 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/19433/statm): 9071 8648 145 145 0 8926 0 [pid=19433] vsize: 36284 Current children cumulated CPU time (s) 1019.37 Current children cumulated vsize (Kb) 38408 One traced child (pid=19433) exited with status: 30 One traced child (pid=19429) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 1020.57 CPU time (s): 1019.9 CPU user time (s): 1019.19 CPU system time (s): 0.711891 CPU usage (%): 99.9338 Max. virtual memory (cumulated for all children) (Kb): 38408
Verifier: OK 235