Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod010.opb |
MD5SUM | 4f0cac14ed3568050c2c57bb69fdb664 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 2655 |
Biggest coefficient in the objective function | 266 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 489211 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 266 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 489211 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2655 |
Total number of constraints | 2801 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 2800 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2655 |
LAUNCH ON wulflinc4 THE 2005-09-20 03:15:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3253 boxname=wulflinc4 idbench=909 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4f0cac14ed3568050c2c57bb69fdb664 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb IDLAUNCH: 3253 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 880336 kB Buffers: 33512 kB Cached: 94352 kB SwapCached: 860 kB Active: 37400 kB Inactive: 93000 kB HighTotal: 131008 kB HighFree: 38108 kB LowTotal: 903652 kB LowFree: 842228 kB SwapTotal: 2097136 kB SwapFree: 2095644 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5520 kB Slab: 18340 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:35:35 (client local time) WITH STATUS 0 IN 1206.32 SECONDS stats: 3253 7 1206.32 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/8785/stat): 8785 (minisat+_script) R 8784 8785 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796977982 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8785/statm): 174 3 169 147 0 27 0 [pid=8785] 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=8786 New process pid=8787 New process pid=8788 execve syscall for /bin/sed executable One traced child (pid=8787) 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=8788) exited with status: 0 One traced child (pid=8786) exited with status: 0 New process pid=8789 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-mod010.opb [startup+10.004 s] Raw data (loadavg): 1.03 0.97 0.73 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 5208 0 0 0 957 20 0 0 25 0 1 0 1796977987 20312064 4502 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 4959 4502 145 145 0 4814 0 [pid=8789] vsize: 19836 Current children cumulated CPU time (s) 9.78 Current children cumulated vsize (Kb) 21960 [startup+20.0049 s] Raw data (loadavg): 1.03 0.97 0.73 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 5774 0 0 0 1946 25 0 0 25 0 1 0 1796977987 22630400 5068 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 5525 5068 145 145 0 5380 0 [pid=8789] vsize: 22100 Current children cumulated CPU time (s) 19.72 Current children cumulated vsize (Kb) 24224 [startup+30.0067 s] Raw data (loadavg): 1.02 0.97 0.73 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 6325 0 0 0 2938 28 0 0 25 0 1 0 1796977987 24911872 5619 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 6082 5619 145 145 0 5937 0 [pid=8789] vsize: 24328 Current children cumulated CPU time (s) 29.67 Current children cumulated vsize (Kb) 26452 [startup+40.0076 s] Raw data (loadavg): 1.02 0.97 0.73 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 7078 0 0 0 3926 32 0 0 25 0 1 0 1796977987 27983872 6372 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 6832 6372 145 145 0 6687 0 [pid=8789] vsize: 27328 Current children cumulated CPU time (s) 39.59 Current children cumulated vsize (Kb) 29452 [startup+50.0084 s] Raw data (loadavg): 1.02 0.97 0.74 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 7812 0 0 0 4915 37 0 0 25 0 1 0 1796977987 30982144 7106 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 7564 7106 145 145 0 7419 0 [pid=8789] vsize: 30256 Current children cumulated CPU time (s) 49.53 Current children cumulated vsize (Kb) 32380 [startup+60.0093 s] Raw data (loadavg): 1.01 0.97 0.74 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 8438 0 0 0 5903 41 0 0 25 0 1 0 1796977987 33595392 7732 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 8202 7732 145 145 0 8057 0 [pid=8789] vsize: 32808 Current children cumulated CPU time (s) 59.45 Current children cumulated vsize (Kb) 34932 [startup+70.0101 s] Raw data (loadavg): 1.01 0.97 0.74 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 9075 0 0 0 6893 45 0 0 25 0 1 0 1796977987 36196352 8369 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 8837 8369 145 145 0 8692 0 [pid=8789] vsize: 35348 Current children cumulated CPU time (s) 69.39 Current children cumulated vsize (Kb) 37472 [startup+80.012 s] Raw data (loadavg): 1.01 0.97 0.74 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 9676 0 0 0 7883 49 0 0 25 0 1 0 1796977987 38649856 8970 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 9436 8970 145 145 0 9291 0 [pid=8789] vsize: 37744 Current children cumulated CPU time (s) 79.33 Current children cumulated vsize (Kb) 39868 [startup+90.0128 s] Raw data (loadavg): 1.01 0.97 0.74 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 10273 0 0 0 8874 52 0 0 25 0 1 0 1796977987 41095168 9567 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 10033 9567 145 145 0 9888 0 [pid=8789] vsize: 40132 Current children cumulated CPU time (s) 89.27 Current children cumulated vsize (Kb) 42256 [startup+100.013 s] Raw data (loadavg): 1.00 0.97 0.75 1/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 10807 0 0 0 9865 55 0 0 25 0 1 0 1796977987 43282432 10101 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/8789/statm): 10567 10101 145 145 0 10422 0 [pid=8789] vsize: 42268 Current children cumulated CPU time (s) 99.21 Current children cumulated vsize (Kb) 44392 [startup+110.013 s] Raw data (loadavg): 1.00 0.97 0.75 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 11346 0 0 0 10857 59 0 0 25 0 1 0 1796977987 45498368 10640 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 11108 10640 145 145 0 10963 0 [pid=8789] vsize: 44432 Current children cumulated CPU time (s) 109.17 Current children cumulated vsize (Kb) 46556 [startup+120.014 s] Raw data (loadavg): 1.00 0.97 0.75 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 11929 0 0 0 11848 61 0 0 25 0 1 0 1796977987 47890432 11223 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 11692 11223 145 145 0 11547 0 [pid=8789] vsize: 46768 Current children cumulated CPU time (s) 119.1 Current children cumulated vsize (Kb) 48892 [startup+130.015 s] Raw data (loadavg): 1.00 0.97 0.75 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 12627 0 0 0 12836 67 0 0 25 0 1 0 1796977987 50741248 11921 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 12388 11921 145 145 0 12243 0 [pid=8789] vsize: 49552 Current children cumulated CPU time (s) 129.04 Current children cumulated vsize (Kb) 51676 [startup+140.016 s] Raw data (loadavg): 1.00 0.97 0.75 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 13299 0 0 0 13825 70 0 0 25 0 1 0 1796977987 53485568 12593 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 13058 12593 145 145 0 12913 0 [pid=8789] vsize: 52232 Current children cumulated CPU time (s) 138.96 Current children cumulated vsize (Kb) 54356 [startup+150.017 s] Raw data (loadavg): 1.00 0.97 0.76 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 13952 0 0 0 14814 75 0 0 25 0 1 0 1796977987 56156160 13246 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 13710 13246 145 145 0 13565 0 [pid=8789] vsize: 54840 Current children cumulated CPU time (s) 148.9 Current children cumulated vsize (Kb) 56964 [startup+160.018 s] Raw data (loadavg): 1.00 0.97 0.76 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 14579 0 0 0 15803 79 0 0 25 0 1 0 1796977987 58851328 13873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 14368 13873 145 145 0 14223 0 [pid=8789] vsize: 57472 Current children cumulated CPU time (s) 158.83 Current children cumulated vsize (Kb) 59596 [startup+170.019 s] Raw data (loadavg): 1.00 0.97 0.76 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 15182 0 0 0 16793 85 0 0 25 0 1 0 1796977987 61313024 14476 4294967295 134512640 135094434 3221224432 3221222896 134780630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 14969 14476 145 145 0 14824 0 [pid=8789] vsize: 59876 Current children cumulated CPU time (s) 168.79 Current children cumulated vsize (Kb) 62000 [startup+180.02 s] Raw data (loadavg): 1.00 0.97 0.76 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 15779 0 0 0 17782 88 0 0 25 0 1 0 1796977987 63750144 15073 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 15564 15073 145 145 0 15419 0 [pid=8789] vsize: 62256 Current children cumulated CPU time (s) 178.71 Current children cumulated vsize (Kb) 64380 [startup+190.021 s] Raw data (loadavg): 1.00 0.97 0.76 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 16366 0 0 0 18771 94 0 0 25 0 1 0 1796977987 66146304 15660 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 16149 15660 145 145 0 16004 0 [pid=8789] vsize: 64596 Current children cumulated CPU time (s) 188.66 Current children cumulated vsize (Kb) 66720 [startup+200.022 s] Raw data (loadavg): 1.00 0.97 0.77 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 16933 0 0 0 19760 100 0 0 25 0 1 0 1796977987 68460544 16227 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 16714 16227 145 145 0 16569 0 [pid=8789] vsize: 66856 Current children cumulated CPU time (s) 198.61 Current children cumulated vsize (Kb) 68980 [startup+210.023 s] Raw data (loadavg): 1.00 0.97 0.77 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 17732 0 0 0 20744 106 0 0 25 0 1 0 1796977987 71725056 17026 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 17511 17026 145 145 0 17366 0 [pid=8789] vsize: 70044 Current children cumulated CPU time (s) 208.51 Current children cumulated vsize (Kb) 72168 [startup+220.024 s] Raw data (loadavg): 1.00 0.97 0.77 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 18443 0 0 0 21734 111 0 0 25 0 1 0 1796977987 74633216 17737 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 18221 17737 145 145 0 18076 0 [pid=8789] vsize: 72884 Current children cumulated CPU time (s) 218.46 Current children cumulated vsize (Kb) 75008 [startup+230.025 s] Raw data (loadavg): 1.00 0.97 0.77 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 19093 0 0 0 22724 115 0 0 25 0 1 0 1796977987 77291520 18387 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 18870 18387 145 145 0 18725 0 [pid=8789] vsize: 75480 Current children cumulated CPU time (s) 228.4 Current children cumulated vsize (Kb) 77604 [startup+240.025 s] Raw data (loadavg): 1.00 0.97 0.77 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 19707 0 0 0 23716 120 0 0 25 0 1 0 1796977987 79798272 19001 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 19482 19001 145 145 0 19337 0 [pid=8789] vsize: 77928 Current children cumulated CPU time (s) 238.37 Current children cumulated vsize (Kb) 80052 [startup+250.026 s] Raw data (loadavg): 1.00 0.97 0.78 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 20310 0 0 0 24706 123 0 0 25 0 1 0 1796977987 82259968 19604 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 20083 19604 145 145 0 19938 0 [pid=8789] vsize: 80332 Current children cumulated CPU time (s) 248.3 Current children cumulated vsize (Kb) 82456 [startup+260.027 s] Raw data (loadavg): 1.00 0.97 0.78 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 20920 0 0 0 25695 128 0 0 25 0 1 0 1796977987 84758528 20214 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8789/statm): 20693 20214 145 145 0 20548 0 [pid=8789] vsize: 82772 Current children cumulated CPU time (s) 258.24 Current children cumulated vsize (Kb) 84896 [startup+270.028 s] Raw data (loadavg): 1.00 0.97 0.78 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 21461 0 0 0 26687 132 0 0 25 0 1 0 1796977987 86986752 20755 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 21237 20755 145 145 0 21092 0 [pid=8789] vsize: 84948 Current children cumulated CPU time (s) 268.2 Current children cumulated vsize (Kb) 87072 [startup+280.029 s] Raw data (loadavg): 1.00 0.97 0.78 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 21917 0 0 0 27680 134 0 0 25 0 1 0 1796977987 88854528 21211 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 21693 21211 145 145 0 21548 0 [pid=8789] vsize: 86772 Current children cumulated CPU time (s) 278.15 Current children cumulated vsize (Kb) 88896 [startup+290.03 s] Raw data (loadavg): 1.00 0.97 0.78 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 22460 0 0 0 28672 137 0 0 25 0 1 0 1796977987 91066368 21754 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 22233 21754 145 145 0 22088 0 [pid=8789] vsize: 88932 Current children cumulated CPU time (s) 288.1 Current children cumulated vsize (Kb) 91056 [startup+300.031 s] Raw data (loadavg): 1.00 0.97 0.79 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 23041 0 0 0 29663 142 0 0 25 0 1 0 1796977987 93442048 22335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 22813 22335 145 145 0 22668 0 [pid=8789] vsize: 91252 Current children cumulated CPU time (s) 298.06 Current children cumulated vsize (Kb) 93376 [startup+310.031 s] Raw data (loadavg): 1.00 0.97 0.79 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 23647 0 0 0 30654 145 0 0 25 0 1 0 1796977987 95916032 22941 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 23417 22941 145 145 0 23272 0 [pid=8789] vsize: 93668 Current children cumulated CPU time (s) 308 Current children cumulated vsize (Kb) 95792 [startup+320.032 s] Raw data (loadavg): 1.00 0.97 0.79 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 24077 0 0 0 31645 149 0 0 25 0 1 0 1796977987 97931264 23371 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 23909 23371 145 145 0 23764 0 [pid=8789] vsize: 95636 Current children cumulated CPU time (s) 317.95 Current children cumulated vsize (Kb) 97760 [startup+330.033 s] Raw data (loadavg): 1.00 0.97 0.79 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 24680 0 0 0 32636 152 0 0 25 0 1 0 1796977987 100392960 23974 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 24510 23974 145 145 0 24365 0 [pid=8789] vsize: 98040 Current children cumulated CPU time (s) 327.89 Current children cumulated vsize (Kb) 100164 [startup+340.034 s] Raw data (loadavg): 1.00 0.97 0.79 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 25107 0 0 0 33629 155 0 0 25 0 1 0 1796977987 102133760 24401 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 24935 24401 145 145 0 24790 0 [pid=8789] vsize: 99740 Current children cumulated CPU time (s) 337.85 Current children cumulated vsize (Kb) 101864 [startup+350.034 s] Raw data (loadavg): 1.00 0.97 0.79 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 25686 0 0 0 34619 160 0 0 25 0 1 0 1796977987 104497152 24980 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 25512 24980 145 145 0 25367 0 [pid=8789] vsize: 102048 Current children cumulated CPU time (s) 347.8 Current children cumulated vsize (Kb) 104172 [startup+360.036 s] Raw data (loadavg): 1.00 0.97 0.80 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 26416 0 0 0 35609 165 0 0 25 0 1 0 1796977987 107495424 25710 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 26244 25710 145 145 0 26099 0 [pid=8789] vsize: 104976 Current children cumulated CPU time (s) 357.75 Current children cumulated vsize (Kb) 107100 [startup+370.036 s] Raw data (loadavg): 1.00 0.97 0.80 3/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 27172 0 0 0 36600 169 0 0 25 0 1 0 1796977987 110587904 26466 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 26999 26466 145 145 0 26854 0 [pid=8789] vsize: 107996 Current children cumulated CPU time (s) 367.7 Current children cumulated vsize (Kb) 110120 [startup+380.037 s] Raw data (loadavg): 1.00 0.97 0.80 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 27685 0 0 0 37591 173 0 0 25 0 1 0 1796977987 112685056 26979 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 27511 26979 145 145 0 27366 0 [pid=8789] vsize: 110044 Current children cumulated CPU time (s) 377.65 Current children cumulated vsize (Kb) 112168 [startup+390.038 s] Raw data (loadavg): 1.00 0.97 0.80 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 28016 0 0 0 38585 175 0 0 25 0 1 0 1796977987 114024448 27310 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 27838 27310 145 145 0 27693 0 [pid=8789] vsize: 111352 Current children cumulated CPU time (s) 387.61 Current children cumulated vsize (Kb) 113476 [startup+400.038 s] Raw data (loadavg): 1.00 0.97 0.80 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 28499 0 0 0 39577 179 0 0 25 0 1 0 1796977987 115990528 27793 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 28318 27793 145 145 0 28173 0 [pid=8789] vsize: 113272 Current children cumulated CPU time (s) 397.57 Current children cumulated vsize (Kb) 115396 [startup+410.039 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 28909 0 0 0 40569 182 0 0 25 0 1 0 1796977987 117661696 28203 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 28726 28203 145 145 0 28581 0 [pid=8789] vsize: 114904 Current children cumulated CPU time (s) 407.52 Current children cumulated vsize (Kb) 117028 [startup+420.04 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 29417 0 0 0 41561 186 0 0 25 0 1 0 1796977987 119734272 28711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 29232 28711 145 145 0 29087 0 [pid=8789] vsize: 116928 Current children cumulated CPU time (s) 417.48 Current children cumulated vsize (Kb) 119052 [startup+430.041 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 29953 0 0 0 42553 189 0 0 25 0 1 0 1796977987 121921536 29247 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 29766 29247 145 145 0 29621 0 [pid=8789] vsize: 119064 Current children cumulated CPU time (s) 427.43 Current children cumulated vsize (Kb) 121188 [startup+440.041 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 30507 0 0 0 43545 192 0 0 25 0 1 0 1796977987 124182528 29801 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 30318 29801 145 145 0 30173 0 [pid=8789] vsize: 121272 Current children cumulated CPU time (s) 437.38 Current children cumulated vsize (Kb) 123396 [startup+450.042 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 31206 0 0 0 44534 197 0 0 25 0 1 0 1796977987 127037440 30500 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 31015 30500 145 145 0 30870 0 [pid=8789] vsize: 124060 Current children cumulated CPU time (s) 447.32 Current children cumulated vsize (Kb) 126184 [startup+460.043 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 31880 0 0 0 45523 202 0 0 25 0 1 0 1796977987 129789952 31174 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 31687 31174 145 145 0 31542 0 [pid=8789] vsize: 126748 Current children cumulated CPU time (s) 457.26 Current children cumulated vsize (Kb) 128872 [startup+470.044 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 32516 0 0 0 46512 206 0 0 25 0 1 0 1796977987 132390912 31810 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 32322 31810 145 145 0 32177 0 [pid=8789] vsize: 129288 Current children cumulated CPU time (s) 467.19 Current children cumulated vsize (Kb) 131412 [startup+480.045 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 33081 0 0 0 47504 210 0 0 25 0 1 0 1796977987 134701056 32375 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 32886 32375 145 145 0 32741 0 [pid=8789] vsize: 131544 Current children cumulated CPU time (s) 477.15 Current children cumulated vsize (Kb) 133668 [startup+490.046 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 33670 0 0 0 48495 213 0 0 25 0 1 0 1796977987 137113600 32964 4294967295 134512640 135094434 3221224432 3221223104 134555950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 33475 32964 145 145 0 33330 0 [pid=8789] vsize: 133900 Current children cumulated CPU time (s) 487.09 Current children cumulated vsize (Kb) 136024 [startup+500.045 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 34259 0 0 0 49487 217 0 0 25 0 1 0 1796977987 139522048 33553 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 34063 33553 145 145 0 33918 0 [pid=8789] vsize: 136252 Current children cumulated CPU time (s) 497.05 Current children cumulated vsize (Kb) 138376 [startup+510.046 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 34713 0 0 0 50479 221 0 0 25 0 1 0 1796977987 141377536 34007 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 34516 34007 145 145 0 34371 0 [pid=8789] vsize: 138064 Current children cumulated CPU time (s) 507.01 Current children cumulated vsize (Kb) 140188 [startup+520.047 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 35305 0 0 0 51470 225 0 0 25 0 1 0 1796977987 143798272 34599 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 35107 34599 145 145 0 34962 0 [pid=8789] vsize: 140428 Current children cumulated CPU time (s) 516.96 Current children cumulated vsize (Kb) 142552 [startup+530.048 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 35597 0 0 0 52466 226 0 0 25 0 1 0 1796977987 144986112 34891 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 35397 34891 145 145 0 35252 0 [pid=8789] vsize: 141588 Current children cumulated CPU time (s) 526.93 Current children cumulated vsize (Kb) 143712 [startup+540.049 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 36204 0 0 0 53456 230 0 0 25 0 1 0 1796977987 147460096 35498 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 36001 35498 145 145 0 35856 0 [pid=8789] vsize: 144004 Current children cumulated CPU time (s) 536.87 Current children cumulated vsize (Kb) 146128 [startup+550.05 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 36726 0 0 0 54450 233 0 0 25 0 1 0 1796977987 149590016 36020 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8789/statm): 36521 36020 145 145 0 36376 0 [pid=8789] vsize: 146084 Current children cumulated CPU time (s) 546.84 Current children cumulated vsize (Kb) 148208 [startup+560.05 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 37040 0 0 0 55446 235 0 0 25 0 1 0 1796977987 150872064 36334 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 36834 36334 145 145 0 36689 0 [pid=8789] vsize: 147336 Current children cumulated CPU time (s) 556.82 Current children cumulated vsize (Kb) 149460 [startup+570.051 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 37425 0 0 0 56439 238 0 0 25 0 1 0 1796977987 152440832 36719 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 37217 36719 145 145 0 37072 0 [pid=8789] vsize: 148868 Current children cumulated CPU time (s) 566.78 Current children cumulated vsize (Kb) 150992 [startup+580.052 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 37859 0 0 0 57432 241 0 0 25 0 1 0 1796977987 154214400 37153 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 37650 37153 145 145 0 37505 0 [pid=8789] vsize: 150600 Current children cumulated CPU time (s) 576.74 Current children cumulated vsize (Kb) 152724 [startup+590.053 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 38382 0 0 0 58423 245 0 0 25 0 1 0 1796977987 156348416 37676 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 38171 37676 145 145 0 38026 0 [pid=8789] vsize: 152684 Current children cumulated CPU time (s) 586.69 Current children cumulated vsize (Kb) 154808 [startup+600.053 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 38926 0 0 0 59415 248 0 0 25 0 1 0 1796977987 158572544 38220 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 38714 38220 145 145 0 38569 0 [pid=8789] vsize: 154856 Current children cumulated CPU time (s) 596.64 Current children cumulated vsize (Kb) 156980 [startup+610.054 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 60409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134553308 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 606.62 Current children cumulated vsize (Kb) 159092 [startup+620.055 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 61409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 616.62 Current children cumulated vsize (Kb) 159092 [startup+630.055 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 62409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223084 134562168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 626.62 Current children cumulated vsize (Kb) 159092 [startup+640.056 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 63409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 636.62 Current children cumulated vsize (Kb) 159092 [startup+650.057 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 64410 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 646.63 Current children cumulated vsize (Kb) 159092 [startup+660.058 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 65410 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 656.63 Current children cumulated vsize (Kb) 159092 [startup+670.059 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 66410 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 666.63 Current children cumulated vsize (Kb) 159092 [startup+680.06 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 67409 252 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 676.62 Current children cumulated vsize (Kb) 159092 [startup+690.061 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 68408 253 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 686.62 Current children cumulated vsize (Kb) 159092 [startup+700.061 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 69408 253 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 696.62 Current children cumulated vsize (Kb) 159092 [startup+710.063 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 70408 253 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 706.62 Current children cumulated vsize (Kb) 159092 [startup+720.064 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 71408 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 716.63 Current children cumulated vsize (Kb) 159092 [startup+730.065 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 72407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 726.62 Current children cumulated vsize (Kb) 159092 [startup+740.066 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 73407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 736.62 Current children cumulated vsize (Kb) 159092 [startup+750.067 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 74407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 746.62 Current children cumulated vsize (Kb) 159092 [startup+760.067 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 75407 254 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 756.62 Current children cumulated vsize (Kb) 159092 [startup+770.068 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 76406 255 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 766.62 Current children cumulated vsize (Kb) 159092 [startup+780.07 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 77406 255 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556538 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 776.62 Current children cumulated vsize (Kb) 159092 [startup+790.071 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 78406 255 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 786.62 Current children cumulated vsize (Kb) 159092 [startup+800.072 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 79403 257 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556699 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 796.61 Current children cumulated vsize (Kb) 159092 [startup+810.074 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 80403 258 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 806.62 Current children cumulated vsize (Kb) 159092 [startup+820.074 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 81402 259 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 816.62 Current children cumulated vsize (Kb) 159092 [startup+830.076 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 82402 259 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 826.62 Current children cumulated vsize (Kb) 159092 [startup+840.077 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 83401 260 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 836.62 Current children cumulated vsize (Kb) 159092 [startup+850.078 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 84401 260 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 846.62 Current children cumulated vsize (Kb) 159092 [startup+860.079 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 85400 260 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 856.61 Current children cumulated vsize (Kb) 159092 [startup+870.08 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 86400 261 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 866.62 Current children cumulated vsize (Kb) 159092 [startup+880.081 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 87399 262 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 876.62 Current children cumulated vsize (Kb) 159092 [startup+890.081 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 88398 262 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 886.61 Current children cumulated vsize (Kb) 159092 [startup+900.082 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 89398 262 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 896.61 Current children cumulated vsize (Kb) 159092 [startup+910.083 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 90397 263 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 906.61 Current children cumulated vsize (Kb) 159092 [startup+920.084 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 91397 263 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 916.61 Current children cumulated vsize (Kb) 159092 [startup+930.086 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 92397 263 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 926.61 Current children cumulated vsize (Kb) 159092 [startup+940.087 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 93397 264 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 936.62 Current children cumulated vsize (Kb) 159092 [startup+950.087 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 94396 264 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 946.61 Current children cumulated vsize (Kb) 159092 [startup+960.089 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 95396 264 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 956.61 Current children cumulated vsize (Kb) 159092 [startup+970.09 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 96396 265 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 966.62 Current children cumulated vsize (Kb) 159092 [startup+980.091 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 97395 265 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 976.61 Current children cumulated vsize (Kb) 159092 [startup+990.092 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 98395 265 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 986.61 Current children cumulated vsize (Kb) 159092 [startup+1000.09 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 99395 266 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 996.62 Current children cumulated vsize (Kb) 159092 [startup+1010.09 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 100395 266 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1006.62 Current children cumulated vsize (Kb) 159092 [startup+1020.1 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 101394 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1016.62 Current children cumulated vsize (Kb) 159092 [startup+1030.1 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 102394 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1026.62 Current children cumulated vsize (Kb) 159092 [startup+1040.1 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 103394 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1036.62 Current children cumulated vsize (Kb) 159092 [startup+1050.1 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 104395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1046.63 Current children cumulated vsize (Kb) 159092 [startup+1060.1 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 105395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1056.63 Current children cumulated vsize (Kb) 159092 [startup+1070.1 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 106395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1066.63 Current children cumulated vsize (Kb) 159092 [startup+1080.1 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 107395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1076.63 Current children cumulated vsize (Kb) 159092 [startup+1090.1 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 108395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1086.63 Current children cumulated vsize (Kb) 159092 [startup+1100.1 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 109395 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1096.63 Current children cumulated vsize (Kb) 159092 [startup+1110.1 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 39456 0 0 0 110396 267 0 0 25 0 1 0 1796977987 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39242 38750 145 145 0 39097 0 [pid=8789] vsize: 156968 Current children cumulated CPU time (s) 1106.64 Current children cumulated vsize (Kb) 159092 [startup+1120.1 s] Raw data (loadavg): 1.00 0.97 0.88 1/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 39721 0 0 0 111391 269 0 0 25 0 1 0 1796977987 161820672 39015 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39507 39015 145 145 0 39362 0 [pid=8789] vsize: 158028 Current children cumulated CPU time (s) 1116.61 Current children cumulated vsize (Kb) 160152 [startup+1130.11 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 40183 0 0 0 112386 271 0 0 25 0 1 0 1796977987 163713024 39477 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 39969 39477 145 145 0 39824 0 [pid=8789] vsize: 159876 Current children cumulated CPU time (s) 1126.58 Current children cumulated vsize (Kb) 162000 [startup+1140.11 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 40671 0 0 0 113380 274 0 0 25 0 1 0 1796977987 165707776 39965 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 40456 39965 145 145 0 40311 0 [pid=8789] vsize: 161824 Current children cumulated CPU time (s) 1136.55 Current children cumulated vsize (Kb) 163948 [startup+1150.11 s] Raw data (loadavg): 1.08 0.99 0.89 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 41354 0 0 0 114373 277 0 0 25 0 1 0 1796977987 168501248 40648 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 41138 40648 145 145 0 40993 0 [pid=8789] vsize: 164552 Current children cumulated CPU time (s) 1146.51 Current children cumulated vsize (Kb) 166676 [startup+1160.11 s] Raw data (loadavg): 1.07 0.99 0.89 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 41792 0 0 0 115368 279 0 0 25 0 1 0 1796977987 170295296 41086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 41576 41086 145 145 0 41431 0 [pid=8789] vsize: 166304 Current children cumulated CPU time (s) 1156.48 Current children cumulated vsize (Kb) 168428 [startup+1170.11 s] Raw data (loadavg): 1.06 0.99 0.89 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 42307 0 0 0 116362 282 0 0 25 0 1 0 1796977987 172400640 41601 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 42090 41601 145 145 0 41945 0 [pid=8789] vsize: 168360 Current children cumulated CPU time (s) 1166.45 Current children cumulated vsize (Kb) 170484 [startup+1180.11 s] Raw data (loadavg): 1.05 0.99 0.89 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 42794 0 0 0 117353 286 0 0 25 0 1 0 1796977987 174391296 42088 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 42576 42088 145 145 0 42431 0 [pid=8789] vsize: 170304 Current children cumulated CPU time (s) 1176.4 Current children cumulated vsize (Kb) 172428 [startup+1190.11 s] Raw data (loadavg): 1.04 0.99 0.89 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 43370 0 0 0 118344 289 0 0 25 0 1 0 1796977987 176746496 42664 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8789/statm): 43151 42664 145 145 0 43006 0 [pid=8789] vsize: 172604 Current children cumulated CPU time (s) 1186.34 Current children cumulated vsize (Kb) 174728 [startup+1200.11 s] Raw data (loadavg): 1.03 0.99 0.89 2/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) R 8785 8785 6847 0 -1 0 44092 0 0 0 119335 294 0 0 25 0 1 0 1796977987 179699712 43386 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8789/statm): 43872 43386 145 145 0 43727 0 [pid=8789] vsize: 175488 Current children cumulated CPU time (s) 1196.3 Current children cumulated vsize (Kb) 177612 [startup+1210.11 s] Raw data (loadavg): 1.03 0.99 0.90 1/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 44789 0 0 0 120323 299 0 0 25 0 1 0 1796977987 182550528 44083 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8789/statm): 44568 44083 145 145 0 44423 0 [pid=8789] vsize: 178272 Current children cumulated CPU time (s) 1206.23 Current children cumulated vsize (Kb) 180396 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.03 0.99 0.90 1/57 8789 Raw data (/proc/8785/stat): 8785 (minisat+_script) S 8784 8785 6847 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1796977982 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8785/statm): 531 226 485 147 0 384 0 [pid=8785] vsize: 2124 Raw data (/proc/8789/stat): 8789 (minisat+_64-bit) T 8785 8785 6847 0 -1 0 44789 0 0 0 120323 299 0 0 25 0 1 0 1796977987 182550528 44083 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8789/statm): 44568 44083 145 145 0 44423 0 [pid=8789] vsize: 178272 Current children cumulated CPU time (s) 1206.23 Current children cumulated vsize (Kb) 180396 Sending SIGTERM to -8785 Sleeping 2 seconds One traced child (pid=8785) ended because it received signal 15 (SIGTERM) One traced child (pid=8789) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1206.32 CPU user time (s): 1203.24 CPU system time (s): 3.07853 CPU usage (%): 99.6795 Max. virtual memory (cumulated for all children) (Kb): 180396
ERROR: no interpretation found !