Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mod010.opb |
MD5SUM | ef7064a9be2b712276f7b600af28e2b0 |
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 wulflinc3 THE 2005-09-20 04:30:38 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3375 boxname=wulflinc3 idbench=1031 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ef7064a9be2b712276f7b600af28e2b0 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-mod010.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-mod010.opb IDLAUNCH: 3375 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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: 829952 kB Buffers: 17328 kB Cached: 160820 kB SwapCached: 828 kB Active: 94772 kB Inactive: 86020 kB HighTotal: 131008 kB HighFree: 896 kB LowTotal: 903652 kB LowFree: 829056 kB SwapTotal: 2097136 kB SwapFree: 2095740 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5664 kB Slab: 18264 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:50:49 (client local time) WITH STATUS 0 IN 1206.44 SECONDS stats: 3375 7 1206.44 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/4497/stat): 4497 (minisat+_script) R 4496 4497 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797431705 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/4497/statm): 174 3 169 147 0 27 0 [pid=4497] 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=4498 New process pid=4499 New process pid=4500 execve syscall for /bin/sed executable One traced child (pid=4499) 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=4500) exited with status: 0 One traced child (pid=4498) exited with status: 0 New process pid=4501 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-mod010.opb [startup+10.004 s] Raw data (loadavg): 0.71 0.89 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 5211 0 0 0 958 19 0 0 25 0 1 0 1797431710 20324352 4505 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 4962 4505 145 145 0 4817 0 [pid=4501] vsize: 19848 Current children cumulated CPU time (s) 9.79 Current children cumulated vsize (Kb) 21972 [startup+20.0048 s] Raw data (loadavg): 0.75 0.90 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 5775 0 0 0 1949 23 0 0 25 0 1 0 1797431710 22634496 5069 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 5526 5069 145 145 0 5381 0 [pid=4501] vsize: 22104 Current children cumulated CPU time (s) 19.74 Current children cumulated vsize (Kb) 24228 [startup+30.0057 s] Raw data (loadavg): 0.79 0.90 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 6335 0 0 0 2940 27 0 0 25 0 1 0 1797431710 24952832 5629 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 6092 5629 145 145 0 5947 0 [pid=4501] vsize: 24368 Current children cumulated CPU time (s) 29.69 Current children cumulated vsize (Kb) 26492 [startup+40.0065 s] Raw data (loadavg): 0.82 0.90 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 7103 0 0 0 3928 30 0 0 25 0 1 0 1797431710 28086272 6397 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 6857 6397 145 145 0 6712 0 [pid=4501] vsize: 27428 Current children cumulated CPU time (s) 39.6 Current children cumulated vsize (Kb) 29552 [startup+50.0084 s] Raw data (loadavg): 0.85 0.91 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 7842 0 0 0 4914 36 0 0 25 0 1 0 1797431710 31105024 7136 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 7594 7136 145 145 0 7449 0 [pid=4501] vsize: 30376 Current children cumulated CPU time (s) 49.52 Current children cumulated vsize (Kb) 32500 [startup+60.0092 s] Raw data (loadavg): 0.87 0.91 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 8476 0 0 0 5905 39 0 0 25 0 1 0 1797431710 33751040 7770 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 8240 7770 145 145 0 8095 0 [pid=4501] vsize: 32960 Current children cumulated CPU time (s) 59.46 Current children cumulated vsize (Kb) 35084 [startup+70.01 s] Raw data (loadavg): 0.89 0.91 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 9112 0 0 0 6896 44 0 0 25 0 1 0 1797431710 36347904 8406 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 8874 8406 145 145 0 8729 0 [pid=4501] vsize: 35496 Current children cumulated CPU time (s) 69.42 Current children cumulated vsize (Kb) 37620 [startup+80.0119 s] Raw data (loadavg): 0.91 0.91 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 9720 0 0 0 7887 48 0 0 25 0 1 0 1797431710 38830080 9014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 9480 9014 145 145 0 9335 0 [pid=4501] vsize: 37920 Current children cumulated CPU time (s) 79.37 Current children cumulated vsize (Kb) 40044 [startup+90.0127 s] Raw data (loadavg): 0.92 0.92 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 10303 0 0 0 8878 52 0 0 25 0 1 0 1797431710 41218048 9597 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 10063 9597 145 145 0 9918 0 [pid=4501] vsize: 40252 Current children cumulated CPU time (s) 89.32 Current children cumulated vsize (Kb) 42376 [startup+100.014 s] Raw data (loadavg): 0.93 0.92 0.89 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 10840 0 0 0 9869 56 0 0 25 0 1 0 1797431710 43417600 10134 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 10600 10134 145 145 0 10455 0 [pid=4501] vsize: 42400 Current children cumulated CPU time (s) 99.27 Current children cumulated vsize (Kb) 44524 [startup+110.014 s] Raw data (loadavg): 0.94 0.92 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 11374 0 0 0 10863 59 0 0 25 0 1 0 1797431710 45613056 10668 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 11136 10668 145 145 0 10991 0 [pid=4501] vsize: 44544 Current children cumulated CPU time (s) 109.24 Current children cumulated vsize (Kb) 46668 [startup+120.015 s] Raw data (loadavg): 0.95 0.92 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 11957 0 0 0 11854 61 0 0 25 0 1 0 1797431710 48001024 11251 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 11719 11251 145 145 0 11574 0 [pid=4501] vsize: 46876 Current children cumulated CPU time (s) 119.17 Current children cumulated vsize (Kb) 49000 [startup+130.016 s] Raw data (loadavg): 0.96 0.92 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 12660 0 0 0 12842 66 0 0 25 0 1 0 1797431710 50876416 11954 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 12421 11954 145 145 0 12276 0 [pid=4501] vsize: 49684 Current children cumulated CPU time (s) 129.1 Current children cumulated vsize (Kb) 51808 [startup+140.017 s] Raw data (loadavg): 0.96 0.93 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 13334 0 0 0 13831 70 0 0 25 0 1 0 1797431710 53628928 12628 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 13093 12628 145 145 0 12948 0 [pid=4501] vsize: 52372 Current children cumulated CPU time (s) 139.03 Current children cumulated vsize (Kb) 54496 [startup+150.019 s] Raw data (loadavg): 0.97 0.93 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 13995 0 0 0 14821 74 0 0 25 0 1 0 1797431710 56332288 13289 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 13753 13289 145 145 0 13608 0 [pid=4501] vsize: 55012 Current children cumulated CPU time (s) 148.97 Current children cumulated vsize (Kb) 57136 [startup+160.02 s] Raw data (loadavg): 0.97 0.93 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 14621 0 0 0 15812 78 0 0 25 0 1 0 1797431710 59023360 13915 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 14410 13915 145 145 0 14265 0 [pid=4501] vsize: 57640 Current children cumulated CPU time (s) 158.92 Current children cumulated vsize (Kb) 59764 [startup+170.02 s] Raw data (loadavg): 0.98 0.93 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 15221 0 0 0 16801 83 0 0 25 0 1 0 1797431710 61472768 14515 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 15008 14515 145 145 0 14863 0 [pid=4501] vsize: 60032 Current children cumulated CPU time (s) 168.86 Current children cumulated vsize (Kb) 62156 [startup+180.021 s] Raw data (loadavg): 0.98 0.93 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 15820 0 0 0 17788 88 0 0 25 0 1 0 1797431710 63913984 15114 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 15604 15114 145 145 0 15459 0 [pid=4501] vsize: 62416 Current children cumulated CPU time (s) 178.78 Current children cumulated vsize (Kb) 64540 [startup+190.022 s] Raw data (loadavg): 0.98 0.94 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 16388 0 0 0 18778 92 0 0 25 0 1 0 1797431710 66236416 15682 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 16171 15682 145 145 0 16026 0 [pid=4501] vsize: 64684 Current children cumulated CPU time (s) 188.72 Current children cumulated vsize (Kb) 66808 [startup+200.023 s] Raw data (loadavg): 0.98 0.94 0.90 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 16986 0 0 0 19767 97 0 0 25 0 1 0 1797431710 68677632 16280 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 16767 16280 145 145 0 16622 0 [pid=4501] vsize: 67068 Current children cumulated CPU time (s) 198.66 Current children cumulated vsize (Kb) 69192 [startup+210.024 s] Raw data (loadavg): 0.99 0.94 0.91 1/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 17772 0 0 0 20754 103 0 0 25 0 1 0 1797431710 71888896 17066 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4501/statm): 17551 17066 145 145 0 17406 0 [pid=4501] vsize: 70204 Current children cumulated CPU time (s) 208.59 Current children cumulated vsize (Kb) 72328 [startup+220.025 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 18478 0 0 0 21745 107 0 0 25 0 1 0 1797431710 74776576 17772 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 18256 17772 145 145 0 18111 0 [pid=4501] vsize: 73024 Current children cumulated CPU time (s) 218.54 Current children cumulated vsize (Kb) 75148 [startup+230.025 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 19121 0 0 0 22736 111 0 0 25 0 1 0 1797431710 77406208 18415 4294967295 134512640 135094434 3221224432 3221223024 134557244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 18898 18415 145 145 0 18753 0 [pid=4501] vsize: 75592 Current children cumulated CPU time (s) 228.49 Current children cumulated vsize (Kb) 77716 [startup+240.026 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 19736 0 0 0 23728 114 0 0 25 0 1 0 1797431710 79917056 19030 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 19511 19030 145 145 0 19366 0 [pid=4501] vsize: 78044 Current children cumulated CPU time (s) 238.44 Current children cumulated vsize (Kb) 80168 [startup+250.027 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 20334 0 0 0 24718 119 0 0 25 0 1 0 1797431710 82358272 19628 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 20107 19628 145 145 0 19962 0 [pid=4501] vsize: 80428 Current children cumulated CPU time (s) 248.39 Current children cumulated vsize (Kb) 82552 [startup+260.028 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 20947 0 0 0 25706 123 0 0 25 0 1 0 1797431710 84869120 20241 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 20720 20241 145 145 0 20575 0 [pid=4501] vsize: 82880 Current children cumulated CPU time (s) 258.31 Current children cumulated vsize (Kb) 85004 [startup+270.028 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 21481 0 0 0 26698 127 0 0 25 0 1 0 1797431710 87068672 20775 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 21257 20775 145 145 0 21112 0 [pid=4501] vsize: 85028 Current children cumulated CPU time (s) 268.27 Current children cumulated vsize (Kb) 87152 [startup+280.029 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 21954 0 0 0 27691 129 0 0 25 0 1 0 1797431710 89006080 21248 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 21730 21248 145 145 0 21585 0 [pid=4501] vsize: 86920 Current children cumulated CPU time (s) 278.22 Current children cumulated vsize (Kb) 89044 [startup+290.029 s] Raw data (loadavg): 0.99 0.95 0.91 1/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 22496 0 0 0 28682 132 0 0 25 0 1 0 1797431710 91213824 21790 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4501/statm): 22269 21790 145 145 0 22124 0 [pid=4501] vsize: 89076 Current children cumulated CPU time (s) 288.16 Current children cumulated vsize (Kb) 91200 [startup+300.029 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 23084 0 0 0 29673 135 0 0 25 0 1 0 1797431710 93618176 22378 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 22856 22378 145 145 0 22711 0 [pid=4501] vsize: 91424 Current children cumulated CPU time (s) 298.1 Current children cumulated vsize (Kb) 93548 [startup+310.03 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 23699 0 0 0 30664 140 0 0 25 0 1 0 1797431710 96129024 22993 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 23469 22993 145 145 0 23324 0 [pid=4501] vsize: 93876 Current children cumulated CPU time (s) 308.06 Current children cumulated vsize (Kb) 96000 [startup+320.031 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 24123 0 0 0 31657 143 0 0 25 0 1 0 1797431710 98119680 23417 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 23955 23417 145 145 0 23810 0 [pid=4501] vsize: 95820 Current children cumulated CPU time (s) 318.02 Current children cumulated vsize (Kb) 97944 [startup+330.032 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 24735 0 0 0 32649 146 0 0 25 0 1 0 1797431710 100618240 24029 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 24565 24029 145 145 0 24420 0 [pid=4501] vsize: 98260 Current children cumulated CPU time (s) 327.97 Current children cumulated vsize (Kb) 100384 [startup+340.033 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 25142 0 0 0 33642 151 0 0 25 0 1 0 1797431710 102277120 24436 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 24970 24436 145 145 0 24825 0 [pid=4501] vsize: 99880 Current children cumulated CPU time (s) 337.95 Current children cumulated vsize (Kb) 102004 [startup+350.032 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 25756 0 0 0 34632 155 0 0 25 0 1 0 1797431710 104783872 25050 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 25582 25050 145 145 0 25437 0 [pid=4501] vsize: 102328 Current children cumulated CPU time (s) 347.89 Current children cumulated vsize (Kb) 104452 [startup+360.033 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 26491 0 0 0 35619 161 0 0 25 0 1 0 1797431710 107802624 25785 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 26319 25785 145 145 0 26174 0 [pid=4501] vsize: 105276 Current children cumulated CPU time (s) 357.82 Current children cumulated vsize (Kb) 107400 [startup+370.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 27254 0 0 0 36610 164 0 0 25 0 1 0 1797431710 110923776 26548 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 27081 26548 145 145 0 26936 0 [pid=4501] vsize: 108324 Current children cumulated CPU time (s) 367.76 Current children cumulated vsize (Kb) 110448 [startup+380.035 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 27732 0 0 0 37603 167 0 0 25 0 1 0 1797431710 112869376 27026 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 27556 27026 145 145 0 27411 0 [pid=4501] vsize: 110224 Current children cumulated CPU time (s) 377.72 Current children cumulated vsize (Kb) 112348 [startup+390.036 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 28056 0 0 0 38597 170 0 0 25 0 1 0 1797431710 114184192 27350 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 27877 27350 145 145 0 27732 0 [pid=4501] vsize: 111508 Current children cumulated CPU time (s) 387.69 Current children cumulated vsize (Kb) 113632 [startup+400.037 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 28592 0 0 0 39589 174 0 0 25 0 1 0 1797431710 116371456 27886 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 28411 27886 145 145 0 28266 0 [pid=4501] vsize: 113644 Current children cumulated CPU time (s) 397.65 Current children cumulated vsize (Kb) 115768 [startup+410.037 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 28992 0 0 0 40582 177 0 0 25 0 1 0 1797431710 118001664 28286 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 28809 28286 145 145 0 28664 0 [pid=4501] vsize: 115236 Current children cumulated CPU time (s) 407.61 Current children cumulated vsize (Kb) 117360 [startup+420.037 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 29499 0 0 0 41573 181 0 0 25 0 1 0 1797431710 120066048 28793 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 29313 28793 145 145 0 29168 0 [pid=4501] vsize: 117252 Current children cumulated CPU time (s) 417.56 Current children cumulated vsize (Kb) 119376 [startup+430.039 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 30058 0 0 0 42565 185 0 0 25 0 1 0 1797431710 122347520 29352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 29870 29352 145 145 0 29725 0 [pid=4501] vsize: 119480 Current children cumulated CPU time (s) 427.52 Current children cumulated vsize (Kb) 121604 [startup+440.04 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 30628 0 0 0 43555 188 0 0 25 0 1 0 1797431710 124674048 29922 4294967295 134512640 135094434 3221224432 3221223104 134556533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 30438 29922 145 145 0 30293 0 [pid=4501] vsize: 121752 Current children cumulated CPU time (s) 437.45 Current children cumulated vsize (Kb) 123876 [startup+450.04 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 31319 0 0 0 44544 194 0 0 25 0 1 0 1797431710 127500288 30613 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 31128 30613 145 145 0 30983 0 [pid=4501] vsize: 124512 Current children cumulated CPU time (s) 447.4 Current children cumulated vsize (Kb) 126636 [startup+460.042 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 32011 0 0 0 45532 200 0 0 25 0 1 0 1797431710 130326528 31305 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 31818 31305 145 145 0 31673 0 [pid=4501] vsize: 127272 Current children cumulated CPU time (s) 457.34 Current children cumulated vsize (Kb) 129396 [startup+470.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 32652 0 0 0 46521 204 0 0 25 0 1 0 1797431710 132947968 31946 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 32458 31946 145 145 0 32313 0 [pid=4501] vsize: 129832 Current children cumulated CPU time (s) 467.27 Current children cumulated vsize (Kb) 131956 [startup+480.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 33225 0 0 0 47513 208 0 0 25 0 1 0 1797431710 135290880 32519 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 33030 32519 145 145 0 32885 0 [pid=4501] vsize: 132120 Current children cumulated CPU time (s) 477.23 Current children cumulated vsize (Kb) 134244 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 33810 0 0 0 48506 212 0 0 25 0 1 0 1797431710 137687040 33104 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 33615 33104 145 145 0 33470 0 [pid=4501] vsize: 134460 Current children cumulated CPU time (s) 487.2 Current children cumulated vsize (Kb) 136584 [startup+500.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 34380 0 0 0 49497 216 0 0 25 0 1 0 1797431710 140017664 33674 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 34184 33674 145 145 0 34039 0 [pid=4501] vsize: 136736 Current children cumulated CPU time (s) 497.15 Current children cumulated vsize (Kb) 138860 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 34869 0 0 0 50489 219 0 0 25 0 1 0 1797431710 142012416 34163 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 34671 34163 145 145 0 34526 0 [pid=4501] vsize: 138684 Current children cumulated CPU time (s) 507.1 Current children cumulated vsize (Kb) 140808 [startup+520.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 35352 0 0 0 51482 222 0 0 25 0 1 0 1797431710 143986688 34646 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 35153 34646 145 145 0 35008 0 [pid=4501] vsize: 140612 Current children cumulated CPU time (s) 517.06 Current children cumulated vsize (Kb) 142736 [startup+530.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 35818 0 0 0 52474 225 0 0 25 0 1 0 1797431710 145887232 35112 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 35617 35112 145 145 0 35472 0 [pid=4501] vsize: 142468 Current children cumulated CPU time (s) 527.01 Current children cumulated vsize (Kb) 144592 [startup+540.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 36346 0 0 0 53466 229 0 0 25 0 1 0 1797431710 148037632 35640 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 36142 35640 145 145 0 35997 0 [pid=4501] vsize: 144568 Current children cumulated CPU time (s) 536.97 Current children cumulated vsize (Kb) 146692 [startup+550.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 36865 0 0 0 54458 233 0 0 25 0 1 0 1797431710 150155264 36159 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 36659 36159 145 145 0 36514 0 [pid=4501] vsize: 146636 Current children cumulated CPU time (s) 546.93 Current children cumulated vsize (Kb) 148760 [startup+560.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 37164 0 0 0 55452 235 0 0 25 0 1 0 1797431710 151375872 36458 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 36957 36458 145 145 0 36812 0 [pid=4501] vsize: 147828 Current children cumulated CPU time (s) 556.89 Current children cumulated vsize (Kb) 149952 [startup+570.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 37602 0 0 0 56445 238 0 0 25 0 1 0 1797431710 153165824 36896 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 37394 36896 145 145 0 37249 0 [pid=4501] vsize: 149576 Current children cumulated CPU time (s) 566.85 Current children cumulated vsize (Kb) 151700 [startup+580.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 38056 0 0 0 57437 242 0 0 25 0 1 0 1797431710 155017216 37350 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 37846 37350 145 145 0 37701 0 [pid=4501] vsize: 151384 Current children cumulated CPU time (s) 576.81 Current children cumulated vsize (Kb) 153508 [startup+590.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 38606 0 0 0 58428 246 0 0 25 0 1 0 1797431710 157261824 37900 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 38394 37900 145 145 0 38249 0 [pid=4501] vsize: 153576 Current children cumulated CPU time (s) 586.76 Current children cumulated vsize (Kb) 155700 [startup+600.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39175 0 0 0 59419 249 0 0 25 0 1 0 1797431710 159588352 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 38962 38469 145 145 0 38817 0 [pid=4501] vsize: 155848 Current children cumulated CPU time (s) 596.7 Current children cumulated vsize (Kb) 157972 [startup+610.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 60414 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 606.68 Current children cumulated vsize (Kb) 159092 [startup+620.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 61414 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 616.68 Current children cumulated vsize (Kb) 159092 [startup+630.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 62415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556450 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 626.69 Current children cumulated vsize (Kb) 159092 [startup+640.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 63415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 636.69 Current children cumulated vsize (Kb) 159092 [startup+650.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 64415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 646.69 Current children cumulated vsize (Kb) 159092 [startup+660.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 65415 252 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 656.69 Current children cumulated vsize (Kb) 159092 [startup+670.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 66415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 666.7 Current children cumulated vsize (Kb) 159092 [startup+680.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 67414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 676.69 Current children cumulated vsize (Kb) 159092 [startup+690.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 68414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 686.69 Current children cumulated vsize (Kb) 159092 [startup+700.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 69414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 696.69 Current children cumulated vsize (Kb) 159092 [startup+710.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 70414 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 706.69 Current children cumulated vsize (Kb) 159092 [startup+720.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 71415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 716.7 Current children cumulated vsize (Kb) 159092 [startup+730.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 72415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 726.7 Current children cumulated vsize (Kb) 159092 [startup+740.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 73415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 736.7 Current children cumulated vsize (Kb) 159092 [startup+750.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 74415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134551920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 746.7 Current children cumulated vsize (Kb) 159092 [startup+760.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 75415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 756.7 Current children cumulated vsize (Kb) 159092 [startup+770.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 76415 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 766.7 Current children cumulated vsize (Kb) 159092 [startup+780.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 77416 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 776.71 Current children cumulated vsize (Kb) 159092 [startup+790.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 78416 253 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 786.71 Current children cumulated vsize (Kb) 159092 [startup+800.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 79416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 796.72 Current children cumulated vsize (Kb) 159092 [startup+810.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 80416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 806.72 Current children cumulated vsize (Kb) 159092 [startup+820.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 81416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 816.72 Current children cumulated vsize (Kb) 159092 [startup+830.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 82416 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 826.72 Current children cumulated vsize (Kb) 159092 [startup+840.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 83417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 836.73 Current children cumulated vsize (Kb) 159092 [startup+850.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 84417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 846.73 Current children cumulated vsize (Kb) 159092 [startup+860.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 85417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 856.73 Current children cumulated vsize (Kb) 159092 [startup+870.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 86417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 866.73 Current children cumulated vsize (Kb) 159092 [startup+880.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 87417 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 876.73 Current children cumulated vsize (Kb) 159092 [startup+890.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 88418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 886.74 Current children cumulated vsize (Kb) 159092 [startup+900.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 89418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 896.74 Current children cumulated vsize (Kb) 159092 [startup+910.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 90418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 906.74 Current children cumulated vsize (Kb) 159092 [startup+920.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 91418 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 916.74 Current children cumulated vsize (Kb) 159092 [startup+930.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 92419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555758 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 926.75 Current children cumulated vsize (Kb) 159092 [startup+940.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 93419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 936.75 Current children cumulated vsize (Kb) 159092 [startup+950.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 94419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 946.75 Current children cumulated vsize (Kb) 159092 [startup+960.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 95419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 956.75 Current children cumulated vsize (Kb) 159092 [startup+970.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 96419 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 966.75 Current children cumulated vsize (Kb) 159092 [startup+980.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 97420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 976.76 Current children cumulated vsize (Kb) 159092 [startup+990.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 98420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 986.76 Current children cumulated vsize (Kb) 159092 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 99420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 996.76 Current children cumulated vsize (Kb) 159092 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 100420 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1006.76 Current children cumulated vsize (Kb) 159092 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 101421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1016.77 Current children cumulated vsize (Kb) 159092 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 102421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1026.77 Current children cumulated vsize (Kb) 159092 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 103421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1036.77 Current children cumulated vsize (Kb) 159092 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 104421 254 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1046.77 Current children cumulated vsize (Kb) 159092 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 105419 256 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1056.77 Current children cumulated vsize (Kb) 159092 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 106418 256 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1066.76 Current children cumulated vsize (Kb) 159092 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 107418 257 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1076.77 Current children cumulated vsize (Kb) 159092 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 108418 257 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1086.77 Current children cumulated vsize (Kb) 159092 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39456 0 0 0 109418 257 0 0 25 0 1 0 1797431710 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39242 38750 145 145 0 39097 0 [pid=4501] vsize: 156968 Current children cumulated CPU time (s) 1096.77 Current children cumulated vsize (Kb) 159092 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39535 0 0 0 110418 257 0 0 25 0 1 0 1797431710 161058816 38829 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39321 38829 145 145 0 39176 0 [pid=4501] vsize: 157284 Current children cumulated CPU time (s) 1106.77 Current children cumulated vsize (Kb) 159408 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 39889 0 0 0 111412 260 0 0 25 0 1 0 1797431710 162508800 39183 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 39675 39183 145 145 0 39530 0 [pid=4501] vsize: 158700 Current children cumulated CPU time (s) 1116.74 Current children cumulated vsize (Kb) 160824 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 40297 0 0 0 112407 262 0 0 25 0 1 0 1797431710 164179968 39591 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 40083 39591 145 145 0 39938 0 [pid=4501] vsize: 160332 Current children cumulated CPU time (s) 1126.71 Current children cumulated vsize (Kb) 162456 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 40962 0 0 0 113400 265 0 0 25 0 1 0 1797431710 166895616 40256 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4501/statm): 40746 40256 145 145 0 40601 0 [pid=4501] vsize: 162984 Current children cumulated CPU time (s) 1136.67 Current children cumulated vsize (Kb) 165108 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 41488 0 0 0 114394 267 0 0 25 0 1 0 1797431710 169050112 40782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 41272 40782 145 145 0 41127 0 [pid=4501] vsize: 165088 Current children cumulated CPU time (s) 1146.63 Current children cumulated vsize (Kb) 167212 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 42013 0 0 0 115388 270 0 0 25 0 1 0 1797431710 171200512 41307 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 41797 41307 145 145 0 41652 0 [pid=4501] vsize: 167188 Current children cumulated CPU time (s) 1156.6 Current children cumulated vsize (Kb) 169312 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 42503 0 0 0 116381 273 0 0 25 0 1 0 1797431710 173203456 41797 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 42286 41797 145 145 0 42141 0 [pid=4501] vsize: 169144 Current children cumulated CPU time (s) 1166.56 Current children cumulated vsize (Kb) 171268 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 42982 0 0 0 117374 276 0 0 25 0 1 0 1797431710 175157248 42276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 42763 42276 145 145 0 42618 0 [pid=4501] vsize: 171052 Current children cumulated CPU time (s) 1176.52 Current children cumulated vsize (Kb) 173176 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) T 4497 4497 31915 0 -1 0 43690 0 0 0 118364 280 0 0 25 0 1 0 1797431710 178053120 42984 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4501/statm): 43470 42984 145 145 0 43325 0 [pid=4501] vsize: 173880 Current children cumulated CPU time (s) 1186.46 Current children cumulated vsize (Kb) 176004 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 44425 0 0 0 119355 284 0 0 25 0 1 0 1797431710 181059584 43719 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 44204 43719 145 145 0 44059 0 [pid=4501] vsize: 176816 Current children cumulated CPU time (s) 1196.41 Current children cumulated vsize (Kb) 178940 [startup+1210.1 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 45047 0 0 0 120347 287 0 0 25 0 1 0 1797431710 183603200 44341 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 44825 44341 145 145 0 44680 0 [pid=4501] vsize: 179300 Current children cumulated CPU time (s) 1206.36 Current children cumulated vsize (Kb) 181424 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 4501 Raw data (/proc/4497/stat): 4497 (minisat+_script) S 4496 4497 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797431705 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4497/statm): 531 226 485 147 0 384 0 [pid=4497] vsize: 2124 Raw data (/proc/4501/stat): 4501 (minisat+_64-bit) R 4497 4497 31915 0 -1 0 45047 0 0 0 120348 287 0 0 25 0 1 0 1797431710 183603200 44341 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4501/statm): 44825 44341 145 145 0 44680 0 [pid=4501] vsize: 179300 Current children cumulated CPU time (s) 1206.37 Current children cumulated vsize (Kb) 181424 Sending SIGTERM to -4497 Sleeping 2 seconds One traced child (pid=4497) ended because it received signal 15 (SIGTERM) One traced child (pid=4501) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.19 CPU time (s): 1206.44 CPU user time (s): 1203.48 CPU system time (s): 2.95755 CPU usage (%): 99.69 Max. virtual memory (cumulated for all children) (Kb): 181424
ERROR: no interpretation found !