Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod010.opb |
MD5SUM | 4f0cac14ed3568050c2c57bb69fdb664 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 2655 |
Biggest coefficient in the objective function | 266 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 489211 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 266 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 489211 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2655 |
Total number of constraints | 2801 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 2800 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2655 |
LAUNCH ON wulflinc27 THE 2005-09-19 03:14:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2869 boxname=wulflinc27 idbench=525 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4f0cac14ed3568050c2c57bb69fdb664 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-mod010.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-mod010.opb IDLAUNCH: 2869 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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: 886160 kB Buffers: 37220 kB Cached: 78840 kB SwapCached: 764 kB Active: 70312 kB Inactive: 48328 kB HighTotal: 131008 kB HighFree: 49644 kB LowTotal: 903652 kB LowFree: 836516 kB SwapTotal: 2097892 kB SwapFree: 2096616 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5728 kB Slab: 24240 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:34:52 (client local time) WITH STATUS 0 IN 1206.52 SECONDS stats: 2869 7 1206.52 0
c Parsing PB file... c Converting 291 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################################################################################################# c -- Clauses(.)/Splits(s): (none) c ---[ 289]---> BDD-cost: 67 c ---[ 287]---> BDD-cost: 113 c ---[ 285]---> BDD-cost: 181 c ---[ 283]---> BDD-cost: 115 c ---[ 281]---> BDD-cost: 69 c ---[ 279]---> BDD-cost: 125 c ---[ 277]---> BDD-cost: 155 c ---[ 275]---> BDD-cost: 87 c ---[ 273]---> BDD-cost: 97 c ---[ 271]---> BDD-cost: 73 c ---[ 269]---> BDD-cost: 119 c ---[ 267]---> BDD-cost: 45 c ---[ 265]---> BDD-cost: 171 c ---[ 263]---> BDD-cost: 111 c ---[ 261]---> BDD-cost: 149 c ---[ 259]---> BDD-cost: 195 c ---[ 257]---> BDD-cost: 131 c ---[ 255]---> BDD-cost: 123 c ---[ 253]---> BDD-cost: 167 c ---[ 251]---> BDD-cost: 101 c ---[ 249]---> BDD-cost: 97 c ---[ 247]---> BDD-cost: 23 c ---[ 245]---> BDD-cost: 135 c ---[ 243]---> BDD-cost: 59 c ---[ 241]---> BDD-cost: 95 c ---[ 239]---> BDD-cost: 59 c ---[ 237]---> BDD-cost: 133 c ---[ 235]---> BDD-cost: 99 c ---[ 233]---> BDD-cost: 179 c ---[ 231]---> BDD-cost: 111 c ---[ 229]---> BDD-cost: 23 c ---[ 227]---> BDD-cost: 89 c ---[ 225]---> BDD-cost: 95 c ---[ 223]---> BDD-cost: 117 c ---[ 221]---> BDD-cost: 23 c ---[ 219]---> BDD-cost: 51 c ---[ 217]---> BDD-cost: 311 c ---[ 215]---> BDD-cost: 259 c ---[ 213]---> BDD-cost: 169 c ---[ 211]---> BDD-cost: 131 c ---[ 209]---> BDD-cost: 155 c ---[ 207]---> BDD-cost: 89 c ---[ 205]---> BDD-cost: 51 c ---[ 203]---> BDD-cost: 165 c ---[ 201]---> BDD-cost: 75 c ---[ 199]---> BDD-cost: 139 c ---[ 197]---> BDD-cost: 67 c ---[ 195]---> BDD-cost: 173 c ---[ 193]---> BDD-cost: 235 c ---[ 191]---> BDD-cost: 185 c ---[ 189]---> BDD-cost: 127 c ---[ 187]---> BDD-cost: 37 c ---[ 185]---> BDD-cost: 37 c ---[ 183]---> BDD-cost: 91 c ---[ 181]---> BDD-cost: 77 c ---[ 179]---> BDD-cost: 29 c ---[ 177]---> BDD-cost: 77 c ---[ 175]---> BDD-cost: 77 c ---[ 173]---> BDD-cost: 101 c ---[ 171]---> BDD-cost: 131 c ---[ 169]---> BDD-cost: 155 c ---[ 167]---> BDD-cost: 177 c ---[ 165]---> BDD-cost: 143 c ---[ 163]---> BDD-cost: 93 c ---[ 161]---> BDD-cost: 79 c ---[ 159]---> BDD-cost: 53 c ---[ 157]---> BDD-cost: 71 c ---[ 155]---> BDD-cost: 127 c ---[ 153]---> BDD-cost: 127 c ---[ 151]---> BDD-cost: 67 c ---[ 149]---> BDD-cost: 83 c ---[ 147]---> BDD-cost: 47 c ---[ 145]---> BDD-cost: 63 c ---[ 143]---> BDD-cost: 121 c ---[ 141]---> BDD-cost: 155 c ---[ 139]---> BDD-cost: 87 c ---[ 137]---> BDD-cost: 91 c ---[ 135]---> BDD-cost: 47 c ---[ 133]---> BDD-cost: 67 c ---[ 131]---> BDD-cost: 33 c ---[ 129]---> BDD-cost: 91 c ---[ 127]---> BDD-cost: 69 c ---[ 125]---> BDD-cost: 5 c ---[ 123]---> BDD-cost: 47 c ---[ 121]---> BDD-cost: 45 c ---[ 119]---> BDD-cost: 37 c ---[ 117]---> BDD-cost: 117 c ---[ 115]---> BDD-cost: 97 c ---[ 113]---> BDD-cost: 77 c ---[ 111]---> BDD-cost: 97 c ---[ 109]---> BDD-cost: 137 c ---[ 107]---> BDD-cost: 125 c ---[ 105]---> BDD-cost: 79 c ---[ 103]---> BDD-cost: 133 c ---[ 101]---> BDD-cost: 153 c ---[ 99]---> BDD-cost: 139 c ---[ 97]---> BDD-cost: 125 c ---[ 95]---> BDD-cost: 5 c ---[ 93]---> BDD-cost: 73 c ---[ 91]---> BDD-cost: 157 c ---[ 89]---> BDD-cost: 127 c ---[ 87]---> BDD-cost: 199 c ---[ 85]---> BDD-cost: 121 c ---[ 83]---> BDD-cost: 107 c ---[ 81]---> BDD-cost: 169 c ---[ 79]---> BDD-cost: 113 c ---[ 77]---> BDD-cost: 103 c ---[ 75]---> BDD-cost: 75 c ---[ 73]---> BDD-cost: 97 c ---[ 71]---> BDD-cost: 151 c ---[ 69]---> BDD-cost: 199 c ---[ 67]---> BDD-cost: 109 c ---[ 65]---> BDD-cost: 131 c ---[ 63]---> BDD-cost: 113 c ---[ 61]---> BDD-cost: 173 c ---[ 59]---> BDD-cost: 119 c ---[ 57]---> BDD-cost: 173 c ---[ 55]---> BDD-cost: 119 c ---[ 53]---> BDD-cost: 71 c ---[ 51]---> BDD-cost: 179 c ---[ 49]---> BDD-cost: 241 c ---[ 47]---> BDD-cost: 201 c ---[ 45]---> BDD-cost: 173 c ---[ 43]---> BDD-cost: 147 c ---[ 41]---> BDD-cost: 157 c ---[ 39]---> BDD-cost: 201 c ---[ 37]---> BDD-cost: 129 c ---[ 35]---> BDD-cost: 117 c ---[ 33]---> BDD-cost: 177 c ---[ 31]---> BDD-cost: 123 c ---[ 29]---> BDD-cost: 131 c ---[ 27]---> BDD-cost: 115 c ---[ 25]---> BDD-cost: 51 c ---[ 23]---> BDD-cost: 123 c ---[ 21]---> BDD-cost: 55 c ---[ 19]---> BDD-cost: 5 c ---[ 17]---> BDD-cost: 99 c ---[ 15]---> BDD-cost: 85 c ---[ 13]---> BDD-cost: 109 c ---[ 11]---> BDD-cost: 153 c ---[ 9]---> BDD-cost: 201 c ---[ 7]---> BDD-cost: 133 c ---[ 5]---> BDD-cost: 121 c ---[ 3]---> BDD-cost: 171 c ---[ 1]---> Adder-cost: 5294 maxlim: 2609 bits: 12/12 c ---[ 0]---> BDD-cost: 751 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 79291 242194 | 26430 0 0 nan | 0.000 % | c | 101 | 79216 241933 | 29073 93 735 7.9 | 0.735 % | c | 253 | 79216 241933 | 31980 245 2664 10.9 | 0.735 % | c | 478 | 79216 241933 | 35178 470 26790 57.0 | 0.735 % | c | 816 | 79216 241933 | 38696 808 31842 39.4 | 0.735 % | c | 1323 | 79216 241933 | 42565 1315 62134 47.3 | 0.735 % | c | 2082 | 79216 241933 | 46822 2074 107560 51.9 | 0.735 % | c | 3222 | 79188 241847 | 51504 3207 277140 86.4 | 0.751 % | c | 4930 | 79188 241847 | 56655 4915 483903 98.5 | 0.751 % | c | 7493 | 79188 241847 | 62320 7478 739580 98.9 | 0.751 % | c | 11337 | 79188 241847 | 68552 11322 1362239 120.3 | 0.751 % | c | 17103 | 79164 241769 | 75407 17085 2978250 174.3 | 0.767 % | c | 25752 | 79164 241769 | 82948 25734 6444146 250.4 | 0.767 % | c | 38727 | 79164 241769 | 91243 38709 10596182 273.7 | 0.767 % | c | 58188 | 79145 241708 | 100367 58167 16215504 278.8 | 0.779 % | c | 87383 | 79101 241554 | 110404 87356 23978747 274.5 | 0.807 % | c | 131172 | 79079 241468 | 121445 35237 6368599 180.7 | 0.823 % | c | 196857 | 78549 239688 | 133589 100806 30304920 300.6 | 1.134 % |
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/15322/stat): 15322 (minisat+_script) R 15321 15322 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846558809 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/15322/statm): 174 3 169 147 0 27 0 [pid=15322] 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=15323 New process pid=15324 New process pid=15325 execve syscall for /bin/sed executable One traced child (pid=15324) 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=15325) exited with status: 0 One traced child (pid=15323) exited with status: 0 New process pid=15326 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-mod010.opb [startup+10.0042 s] Raw data (loadavg): 0.94 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 5203 0 0 0 957 21 0 0 25 0 1 0 1846558814 20291584 4497 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 4954 4497 145 145 0 4809 0 [pid=15326] vsize: 19816 Current children cumulated CPU time (s) 9.78 Current children cumulated vsize (Kb) 21940 [startup+20.005 s] Raw data (loadavg): 0.95 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 5771 0 0 0 1948 24 0 0 25 0 1 0 1846558814 22618112 5065 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 5522 5065 145 145 0 5377 0 [pid=15326] vsize: 22088 Current children cumulated CPU time (s) 19.72 Current children cumulated vsize (Kb) 24212 [startup+30.0059 s] Raw data (loadavg): 0.95 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 6319 0 0 0 2940 27 0 0 25 0 1 0 1846558814 24887296 5613 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 6076 5613 145 145 0 5931 0 [pid=15326] vsize: 24304 Current children cumulated CPU time (s) 29.67 Current children cumulated vsize (Kb) 26428 [startup+40.0077 s] Raw data (loadavg): 0.96 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 7066 0 0 0 3929 31 0 0 25 0 1 0 1846558814 27934720 6360 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 6820 6360 145 145 0 6675 0 [pid=15326] vsize: 27280 Current children cumulated CPU time (s) 39.6 Current children cumulated vsize (Kb) 29404 [startup+50.0085 s] Raw data (loadavg): 0.97 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 7804 0 0 0 4918 36 0 0 25 0 1 0 1846558814 30949376 7098 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 7556 7098 145 145 0 7411 0 [pid=15326] vsize: 30224 Current children cumulated CPU time (s) 49.54 Current children cumulated vsize (Kb) 32348 [startup+60.0104 s] Raw data (loadavg): 0.97 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 8427 0 0 0 5907 40 0 0 25 0 1 0 1846558814 33550336 7721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 8191 7721 145 145 0 8046 0 [pid=15326] vsize: 32764 Current children cumulated CPU time (s) 59.47 Current children cumulated vsize (Kb) 34888 [startup+70.0122 s] Raw data (loadavg): 0.97 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 9061 0 0 0 6897 45 0 0 25 0 1 0 1846558814 36139008 8355 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 8823 8355 145 145 0 8678 0 [pid=15326] vsize: 35292 Current children cumulated CPU time (s) 69.42 Current children cumulated vsize (Kb) 37416 [startup+80.013 s] Raw data (loadavg): 0.98 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 9652 0 0 0 7886 48 0 0 25 0 1 0 1846558814 38551552 8946 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 9412 8946 145 145 0 9267 0 [pid=15326] vsize: 37648 Current children cumulated CPU time (s) 79.34 Current children cumulated vsize (Kb) 39772 [startup+90.0138 s] Raw data (loadavg): 0.98 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 10247 0 0 0 8876 52 0 0 25 0 1 0 1846558814 40988672 9541 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 10007 9541 145 145 0 9862 0 [pid=15326] vsize: 40028 Current children cumulated CPU time (s) 89.28 Current children cumulated vsize (Kb) 42152 [startup+100.015 s] Raw data (loadavg): 0.98 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 10776 0 0 0 9868 56 0 0 25 0 1 0 1846558814 43155456 10070 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 10536 10070 145 145 0 10391 0 [pid=15326] vsize: 42144 Current children cumulated CPU time (s) 99.24 Current children cumulated vsize (Kb) 44268 [startup+110.017 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 11310 0 0 0 10862 58 0 0 25 0 1 0 1846558814 45350912 10604 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 11072 10604 145 145 0 10927 0 [pid=15326] vsize: 44288 Current children cumulated CPU time (s) 109.2 Current children cumulated vsize (Kb) 46412 [startup+120.018 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 11878 0 0 0 11852 62 0 0 25 0 1 0 1846558814 47681536 11172 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 11641 11172 145 145 0 11496 0 [pid=15326] vsize: 46564 Current children cumulated CPU time (s) 119.14 Current children cumulated vsize (Kb) 48688 [startup+130.019 s] Raw data (loadavg): 0.99 0.97 0.95 1/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 12561 0 0 0 12839 68 0 0 25 0 1 0 1846558814 50470912 11855 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15326/statm): 12322 11855 145 145 0 12177 0 [pid=15326] vsize: 49288 Current children cumulated CPU time (s) 129.07 Current children cumulated vsize (Kb) 51412 [startup+140.02 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 13254 0 0 0 13828 73 0 0 25 0 1 0 1846558814 53301248 12548 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 13013 12548 145 145 0 12868 0 [pid=15326] vsize: 52052 Current children cumulated CPU time (s) 139.01 Current children cumulated vsize (Kb) 54176 [startup+150.021 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 13895 0 0 0 14818 77 0 0 25 0 1 0 1846558814 55922688 13189 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 13653 13189 145 145 0 13508 0 [pid=15326] vsize: 54612 Current children cumulated CPU time (s) 148.95 Current children cumulated vsize (Kb) 56736 [startup+160.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 14531 0 0 0 15809 81 0 0 25 0 1 0 1846558814 58654720 13825 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 14320 13825 145 145 0 14175 0 [pid=15326] vsize: 57280 Current children cumulated CPU time (s) 158.9 Current children cumulated vsize (Kb) 59404 [startup+170.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 15137 0 0 0 16799 85 0 0 25 0 1 0 1846558814 61128704 14431 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 14924 14431 145 145 0 14779 0 [pid=15326] vsize: 59696 Current children cumulated CPU time (s) 168.84 Current children cumulated vsize (Kb) 61820 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 15728 0 0 0 17791 89 0 0 25 0 1 0 1846558814 63541248 15022 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 15513 15022 145 145 0 15368 0 [pid=15326] vsize: 62052 Current children cumulated CPU time (s) 178.8 Current children cumulated vsize (Kb) 64176 [startup+190.023 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 16310 0 0 0 18781 93 0 0 25 0 1 0 1846558814 65921024 15604 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 16094 15604 145 145 0 15949 0 [pid=15326] vsize: 64376 Current children cumulated CPU time (s) 188.74 Current children cumulated vsize (Kb) 66500 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 16870 0 0 0 19772 97 0 0 25 0 1 0 1846558814 68202496 16164 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 16651 16164 145 145 0 16506 0 [pid=15326] vsize: 66604 Current children cumulated CPU time (s) 198.69 Current children cumulated vsize (Kb) 68728 [startup+210.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 17670 0 0 0 20760 102 0 0 25 0 1 0 1846558814 71471104 16964 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 17449 16964 145 145 0 17304 0 [pid=15326] vsize: 69796 Current children cumulated CPU time (s) 208.62 Current children cumulated vsize (Kb) 71920 [startup+220.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 18381 0 0 0 21751 105 0 0 25 0 1 0 1846558814 74379264 17675 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 18159 17675 145 145 0 18014 0 [pid=15326] vsize: 72636 Current children cumulated CPU time (s) 218.56 Current children cumulated vsize (Kb) 74760 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.95 1/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 19045 0 0 0 22740 109 0 0 25 0 1 0 1846558814 77094912 18339 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15326/statm): 18822 18339 145 145 0 18677 0 [pid=15326] vsize: 75288 Current children cumulated CPU time (s) 228.49 Current children cumulated vsize (Kb) 77412 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 19650 0 0 0 23730 113 0 0 25 0 1 0 1846558814 79564800 18944 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 19425 18944 145 145 0 19280 0 [pid=15326] vsize: 77700 Current children cumulated CPU time (s) 238.43 Current children cumulated vsize (Kb) 79824 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.95 1/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 20272 0 0 0 24722 117 0 0 25 0 1 0 1846558814 82104320 19566 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15326/statm): 20045 19566 145 145 0 19900 0 [pid=15326] vsize: 80180 Current children cumulated CPU time (s) 248.39 Current children cumulated vsize (Kb) 82304 [startup+260.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 20888 0 0 0 25712 121 0 0 25 0 1 0 1846558814 84627456 20182 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 20661 20182 145 145 0 20516 0 [pid=15326] vsize: 82644 Current children cumulated CPU time (s) 258.33 Current children cumulated vsize (Kb) 84768 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 21442 0 0 0 26704 124 0 0 25 0 1 0 1846558814 86908928 20736 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 21218 20736 145 145 0 21073 0 [pid=15326] vsize: 84872 Current children cumulated CPU time (s) 268.28 Current children cumulated vsize (Kb) 86996 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 21905 0 0 0 27698 125 0 0 25 0 1 0 1846558814 88801280 21199 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 21680 21199 145 145 0 21535 0 [pid=15326] vsize: 86720 Current children cumulated CPU time (s) 278.23 Current children cumulated vsize (Kb) 88844 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 22447 0 0 0 28690 128 0 0 25 0 1 0 1846558814 91013120 21741 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 22220 21741 145 145 0 22075 0 [pid=15326] vsize: 88880 Current children cumulated CPU time (s) 288.18 Current children cumulated vsize (Kb) 91004 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 23030 0 0 0 29681 133 0 0 25 0 1 0 1846558814 93396992 22324 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 22802 22324 145 145 0 22657 0 [pid=15326] vsize: 91208 Current children cumulated CPU time (s) 298.14 Current children cumulated vsize (Kb) 93332 [startup+310.034 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 23635 0 0 0 30672 137 0 0 25 0 1 0 1846558814 95866880 22929 4294967295 134512640 135094434 3221224432 3221223120 134554715 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 23405 22929 145 145 0 23260 0 [pid=15326] vsize: 93620 Current children cumulated CPU time (s) 308.09 Current children cumulated vsize (Kb) 95744 [startup+320.035 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 24069 0 0 0 31665 140 0 0 25 0 1 0 1846558814 97898496 23363 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 23901 23363 145 145 0 23756 0 [pid=15326] vsize: 95604 Current children cumulated CPU time (s) 318.05 Current children cumulated vsize (Kb) 97728 [startup+330.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 24667 0 0 0 32655 145 0 0 25 0 1 0 1846558814 100339712 23961 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 24497 23961 145 145 0 24352 0 [pid=15326] vsize: 97988 Current children cumulated CPU time (s) 328 Current children cumulated vsize (Kb) 100112 [startup+340.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 25091 0 0 0 33648 148 0 0 25 0 1 0 1846558814 102068224 24385 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 24919 24385 145 145 0 24774 0 [pid=15326] vsize: 99676 Current children cumulated CPU time (s) 337.96 Current children cumulated vsize (Kb) 101800 [startup+350.037 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 25668 0 0 0 34639 152 0 0 25 0 1 0 1846558814 104423424 24962 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 25494 24962 145 145 0 25349 0 [pid=15326] vsize: 101976 Current children cumulated CPU time (s) 347.91 Current children cumulated vsize (Kb) 104100 [startup+360.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 26399 0 0 0 35630 156 0 0 25 0 1 0 1846558814 107425792 25693 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 26227 25693 145 145 0 26082 0 [pid=15326] vsize: 104908 Current children cumulated CPU time (s) 357.86 Current children cumulated vsize (Kb) 107032 [startup+370.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 27153 0 0 0 36619 161 0 0 25 0 1 0 1846558814 110510080 26447 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 26980 26447 145 145 0 26835 0 [pid=15326] vsize: 107920 Current children cumulated CPU time (s) 367.8 Current children cumulated vsize (Kb) 110044 [startup+380.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 27672 0 0 0 37611 165 0 0 25 0 1 0 1846558814 112631808 26966 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 27498 26966 145 145 0 27353 0 [pid=15326] vsize: 109992 Current children cumulated CPU time (s) 377.76 Current children cumulated vsize (Kb) 112116 [startup+390.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 28013 0 0 0 38607 167 0 0 25 0 1 0 1846558814 114012160 27307 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 27835 27307 145 145 0 27690 0 [pid=15326] vsize: 111340 Current children cumulated CPU time (s) 387.74 Current children cumulated vsize (Kb) 113464 [startup+400.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 28481 0 0 0 39600 171 0 0 25 0 1 0 1846558814 115916800 27775 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 28300 27775 145 145 0 28155 0 [pid=15326] vsize: 113200 Current children cumulated CPU time (s) 397.71 Current children cumulated vsize (Kb) 115324 [startup+410.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 28905 0 0 0 40594 173 0 0 25 0 1 0 1846558814 117645312 28199 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 28722 28199 145 145 0 28577 0 [pid=15326] vsize: 114888 Current children cumulated CPU time (s) 407.67 Current children cumulated vsize (Kb) 117012 [startup+420.045 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 29413 0 0 0 41585 177 0 0 25 0 1 0 1846558814 119717888 28707 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 29228 28707 145 145 0 29083 0 [pid=15326] vsize: 116912 Current children cumulated CPU time (s) 417.62 Current children cumulated vsize (Kb) 119036 [startup+430.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 29939 0 0 0 42577 180 0 0 25 0 1 0 1846558814 121864192 29233 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 29752 29233 145 145 0 29607 0 [pid=15326] vsize: 119008 Current children cumulated CPU time (s) 427.57 Current children cumulated vsize (Kb) 121132 [startup+440.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 30482 0 0 0 43567 184 0 0 25 0 1 0 1846558814 124080128 29776 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 30293 29776 145 145 0 30148 0 [pid=15326] vsize: 121172 Current children cumulated CPU time (s) 437.51 Current children cumulated vsize (Kb) 123296 [startup+450.048 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 31186 0 0 0 44557 189 0 0 25 0 1 0 1846558814 126955520 30480 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 30995 30480 145 145 0 30850 0 [pid=15326] vsize: 123980 Current children cumulated CPU time (s) 447.46 Current children cumulated vsize (Kb) 126104 [startup+460.048 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 31858 0 0 0 45546 192 0 0 25 0 1 0 1846558814 129703936 31152 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 31666 31152 145 145 0 31521 0 [pid=15326] vsize: 126664 Current children cumulated CPU time (s) 457.38 Current children cumulated vsize (Kb) 128788 [startup+470.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 32497 0 0 0 46537 197 0 0 25 0 1 0 1846558814 132313088 31791 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 32303 31791 145 145 0 32158 0 [pid=15326] vsize: 129212 Current children cumulated CPU time (s) 467.34 Current children cumulated vsize (Kb) 131336 [startup+480.05 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 33063 0 0 0 47528 201 0 0 25 0 1 0 1846558814 134627328 32357 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 32868 32357 145 145 0 32723 0 [pid=15326] vsize: 131472 Current children cumulated CPU time (s) 477.29 Current children cumulated vsize (Kb) 133596 [startup+490.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 33655 0 0 0 48519 205 0 0 25 0 1 0 1846558814 137052160 32949 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/15326/statm): 33460 32949 145 145 0 33315 0 [pid=15326] vsize: 133840 Current children cumulated CPU time (s) 487.24 Current children cumulated vsize (Kb) 135964 [startup+500.053 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 34244 0 0 0 49511 209 0 0 25 0 1 0 1846558814 139460608 33538 4294967295 134512640 135094434 3221224432 3221223024 134556951 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 34048 33538 145 145 0 33903 0 [pid=15326] vsize: 136192 Current children cumulated CPU time (s) 497.2 Current children cumulated vsize (Kb) 138316 [startup+510.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 34711 0 0 0 50504 212 0 0 25 0 1 0 1846558814 141369344 34005 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 34514 34005 145 145 0 34369 0 [pid=15326] vsize: 138056 Current children cumulated CPU time (s) 507.16 Current children cumulated vsize (Kb) 140180 [startup+520.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 35306 0 0 0 51495 215 0 0 25 0 1 0 1846558814 143802368 34600 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 35108 34600 145 145 0 34963 0 [pid=15326] vsize: 140432 Current children cumulated CPU time (s) 517.1 Current children cumulated vsize (Kb) 142556 [startup+530.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 35603 0 0 0 52491 217 0 0 25 0 1 0 1846558814 145010688 34897 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 35403 34897 145 145 0 35258 0 [pid=15326] vsize: 141612 Current children cumulated CPU time (s) 527.08 Current children cumulated vsize (Kb) 143736 [startup+540.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 36228 0 0 0 53482 220 0 0 25 0 1 0 1846558814 147558400 35522 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 36025 35522 145 145 0 35880 0 [pid=15326] vsize: 144100 Current children cumulated CPU time (s) 537.02 Current children cumulated vsize (Kb) 146224 [startup+550.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 36744 0 0 0 54475 223 0 0 25 0 1 0 1846558814 149663744 36038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 36539 36038 145 145 0 36394 0 [pid=15326] vsize: 146156 Current children cumulated CPU time (s) 546.98 Current children cumulated vsize (Kb) 148280 [startup+560.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 37061 0 0 0 55469 226 0 0 25 0 1 0 1846558814 150953984 36355 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 36854 36355 145 145 0 36709 0 [pid=15326] vsize: 147416 Current children cumulated CPU time (s) 556.95 Current children cumulated vsize (Kb) 149540 [startup+570.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 37465 0 0 0 56462 230 0 0 25 0 1 0 1846558814 152604672 36759 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 37257 36759 145 145 0 37112 0 [pid=15326] vsize: 149028 Current children cumulated CPU time (s) 566.92 Current children cumulated vsize (Kb) 151152 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 37892 0 0 0 57455 232 0 0 25 0 1 0 1846558814 154349568 37186 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 37683 37186 145 145 0 37538 0 [pid=15326] vsize: 150732 Current children cumulated CPU time (s) 576.87 Current children cumulated vsize (Kb) 152856 [startup+590.06 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 38451 0 0 0 58447 236 0 0 25 0 1 0 1846558814 156631040 37745 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 38240 37745 145 145 0 38095 0 [pid=15326] vsize: 152960 Current children cumulated CPU time (s) 586.83 Current children cumulated vsize (Kb) 155084 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 38996 0 0 0 59439 239 0 0 25 0 1 0 1846558814 158855168 38290 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 38783 38290 145 145 0 38638 0 [pid=15326] vsize: 155132 Current children cumulated CPU time (s) 596.78 Current children cumulated vsize (Kb) 157256 [startup+610.063 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 60432 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 606.74 Current children cumulated vsize (Kb) 159092 [startup+620.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 61432 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556918 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 616.74 Current children cumulated vsize (Kb) 159092 [startup+630.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 62433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 626.75 Current children cumulated vsize (Kb) 159092 [startup+640.065 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 63433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 636.75 Current children cumulated vsize (Kb) 159092 [startup+650.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 64433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 646.75 Current children cumulated vsize (Kb) 159092 [startup+660.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 65433 242 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 656.75 Current children cumulated vsize (Kb) 159092 [startup+670.068 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 66432 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 666.75 Current children cumulated vsize (Kb) 159092 [startup+680.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 67432 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 676.75 Current children cumulated vsize (Kb) 159092 [startup+690.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 68432 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 686.75 Current children cumulated vsize (Kb) 159092 [startup+700.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 69433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 696.76 Current children cumulated vsize (Kb) 159092 [startup+710.072 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 70433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 706.76 Current children cumulated vsize (Kb) 159092 [startup+720.073 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 71433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 716.76 Current children cumulated vsize (Kb) 159092 [startup+730.074 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 72433 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 726.76 Current children cumulated vsize (Kb) 159092 [startup+740.074 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 73434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557485 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 736.77 Current children cumulated vsize (Kb) 159092 [startup+750.075 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 74434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 746.77 Current children cumulated vsize (Kb) 159092 [startup+760.076 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 75434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 756.77 Current children cumulated vsize (Kb) 159092 [startup+770.077 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 76434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 766.77 Current children cumulated vsize (Kb) 159092 [startup+780.078 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 77434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 776.77 Current children cumulated vsize (Kb) 159092 [startup+790.079 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 78434 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 786.77 Current children cumulated vsize (Kb) 159092 [startup+800.079 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 79435 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 796.78 Current children cumulated vsize (Kb) 159092 [startup+810.081 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 80435 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 806.78 Current children cumulated vsize (Kb) 159092 [startup+820.082 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 81435 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557160 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 816.78 Current children cumulated vsize (Kb) 159092 [startup+830.082 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 82436 243 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 826.79 Current children cumulated vsize (Kb) 159092 [startup+840.083 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 83436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 836.8 Current children cumulated vsize (Kb) 159092 [startup+850.084 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 84436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 846.8 Current children cumulated vsize (Kb) 159092 [startup+860.084 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 85436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 856.8 Current children cumulated vsize (Kb) 159092 [startup+870.085 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 86436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 866.8 Current children cumulated vsize (Kb) 159092 [startup+880.086 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 87436 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 876.8 Current children cumulated vsize (Kb) 159092 [startup+890.087 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 88437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 886.81 Current children cumulated vsize (Kb) 159092 [startup+900.088 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 89437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 896.81 Current children cumulated vsize (Kb) 159092 [startup+910.089 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 90437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 906.81 Current children cumulated vsize (Kb) 159092 [startup+920.089 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 91437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 916.81 Current children cumulated vsize (Kb) 159092 [startup+930.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 92437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 926.81 Current children cumulated vsize (Kb) 159092 [startup+940.091 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 93438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 936.82 Current children cumulated vsize (Kb) 159092 [startup+950.092 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 94437 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 946.81 Current children cumulated vsize (Kb) 159092 [startup+960.093 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 95438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 956.82 Current children cumulated vsize (Kb) 159092 [startup+970.093 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 96438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 966.82 Current children cumulated vsize (Kb) 159092 [startup+980.093 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 97438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 976.82 Current children cumulated vsize (Kb) 159092 [startup+990.095 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 98438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 986.82 Current children cumulated vsize (Kb) 159092 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 99438 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 996.82 Current children cumulated vsize (Kb) 159092 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 100439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1006.83 Current children cumulated vsize (Kb) 159092 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 101439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1016.83 Current children cumulated vsize (Kb) 159092 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 102439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1026.83 Current children cumulated vsize (Kb) 159092 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 103439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1036.83 Current children cumulated vsize (Kb) 159092 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 104439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1046.83 Current children cumulated vsize (Kb) 159092 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 105439 244 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1056.83 Current children cumulated vsize (Kb) 159092 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 106439 245 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1066.84 Current children cumulated vsize (Kb) 159092 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 107439 245 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1076.84 Current children cumulated vsize (Kb) 159092 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 108439 245 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1086.84 Current children cumulated vsize (Kb) 159092 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39456 0 0 0 109438 246 0 0 25 0 1 0 1846558814 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39242 38750 145 145 0 39097 0 [pid=15326] vsize: 156968 Current children cumulated CPU time (s) 1096.84 Current children cumulated vsize (Kb) 159092 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39534 0 0 0 110435 248 0 0 25 0 1 0 1846558814 161054720 38828 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39320 38828 145 145 0 39175 0 [pid=15326] vsize: 157280 Current children cumulated CPU time (s) 1106.83 Current children cumulated vsize (Kb) 159404 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 39887 0 0 0 111431 249 0 0 25 0 1 0 1846558814 162500608 39181 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 39673 39181 145 145 0 39528 0 [pid=15326] vsize: 158692 Current children cumulated CPU time (s) 1116.8 Current children cumulated vsize (Kb) 160816 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 40300 0 0 0 112426 252 0 0 25 0 1 0 1846558814 164192256 39594 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 40086 39594 145 145 0 39941 0 [pid=15326] vsize: 160344 Current children cumulated CPU time (s) 1126.78 Current children cumulated vsize (Kb) 162468 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 40971 0 0 0 113418 256 0 0 25 0 1 0 1846558814 166932480 40265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 40755 40265 145 145 0 40610 0 [pid=15326] vsize: 163020 Current children cumulated CPU time (s) 1136.74 Current children cumulated vsize (Kb) 165144 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 41496 0 0 0 114411 259 0 0 25 0 1 0 1846558814 169082880 40790 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 41280 40790 145 145 0 41135 0 [pid=15326] vsize: 165120 Current children cumulated CPU time (s) 1146.7 Current children cumulated vsize (Kb) 167244 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 42029 0 0 0 115404 263 0 0 25 0 1 0 1846558814 171266048 41323 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 41813 41323 145 145 0 41668 0 [pid=15326] vsize: 167252 Current children cumulated CPU time (s) 1156.67 Current children cumulated vsize (Kb) 169376 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 42519 0 0 0 116398 266 0 0 25 0 1 0 1846558814 173268992 41813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 42302 41813 145 145 0 42157 0 [pid=15326] vsize: 169208 Current children cumulated CPU time (s) 1166.64 Current children cumulated vsize (Kb) 171332 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 43001 0 0 0 117391 269 0 0 25 0 1 0 1846558814 175235072 42295 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 42782 42295 145 145 0 42637 0 [pid=15326] vsize: 171128 Current children cumulated CPU time (s) 1176.6 Current children cumulated vsize (Kb) 173252 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 43727 0 0 0 118382 274 0 0 25 0 1 0 1846558814 178204672 43021 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 43507 43021 145 145 0 43362 0 [pid=15326] vsize: 174028 Current children cumulated CPU time (s) 1186.56 Current children cumulated vsize (Kb) 176152 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) R 15322 15322 28974 0 -1 0 44460 0 0 0 119372 277 0 0 25 0 1 0 1846558814 181202944 43754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/15326/statm): 44239 43754 145 145 0 44094 0 [pid=15326] vsize: 176956 Current children cumulated CPU time (s) 1196.49 Current children cumulated vsize (Kb) 179080 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 45079 0 0 0 120364 279 0 0 25 0 1 0 1846558814 183734272 44373 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15326/statm): 44857 44373 145 145 0 44712 0 [pid=15326] vsize: 179428 Current children cumulated CPU time (s) 1206.43 Current children cumulated vsize (Kb) 181552 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.95 1/57 15326 Raw data (/proc/15322/stat): 15322 (minisat+_script) S 15321 15322 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1846558809 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/15322/statm): 531 226 485 147 0 384 0 [pid=15322] vsize: 2124 Raw data (/proc/15326/stat): 15326 (minisat+_64-bit) T 15322 15322 28974 0 -1 0 45079 0 0 0 120364 279 0 0 25 0 1 0 1846558814 183734272 44373 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/15326/statm): 44857 44373 145 145 0 44712 0 [pid=15326] vsize: 179428 Current children cumulated CPU time (s) 1206.43 Current children cumulated vsize (Kb) 181552 Sending SIGTERM to -15322 Sleeping 2 seconds One traced child (pid=15322) ended because it received signal 15 (SIGTERM) One traced child (pid=15326) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1206.52 CPU user time (s): 1203.65 CPU system time (s): 2.87656 CPU usage (%): 99.6965 Max. virtual memory (cumulated for all children) (Kb): 181552
ERROR: no interpretation found !