Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mod010.opb |
MD5SUM | ef7064a9be2b712276f7b600af28e2b0 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 2655 |
Biggest coefficient in the objective function | 266 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 489211 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 266 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 489211 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2655 |
Total number of constraints | 2801 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 2800 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2655 |
LAUNCH ON wulflinc4 THE 2005-09-19 18:05:39 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2991 boxname=wulflinc4 idbench=647 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ef7064a9be2b712276f7b600af28e2b0 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-mod010.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-mod010.opb IDLAUNCH: 2991 /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: 907444 kB Buffers: 33248 kB Cached: 68416 kB SwapCached: 880 kB Active: 56356 kB Inactive: 47904 kB HighTotal: 131008 kB HighFree: 59332 kB LowTotal: 903652 kB LowFree: 848112 kB SwapTotal: 2097136 kB SwapFree: 2095648 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5684 kB Slab: 17256 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:25:49 (client local time) WITH STATUS 0 IN 1206.38 SECONDS stats: 2991 7 1206.38 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/32347/stat): 32347 (minisat+_script) R 32346 32347 6847 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793679028 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/32347/statm): 174 3 169 147 0 27 0 [pid=32347] 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=32348 New process pid=32349 New process pid=32350 execve syscall for /bin/sed executable 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 One traced child (pid=32349) exited with status: 0 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=32350) exited with status: 0 One traced child (pid=32348) exited with status: 0 New process pid=32351 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-20-10-mod010.opb [startup+10.0037 s] Raw data (loadavg): 0.93 0.95 0.87 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 5213 0 0 0 960 19 0 0 25 0 1 0 1793679033 20332544 4507 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 4964 4507 145 145 0 4819 0 [pid=32351] vsize: 19856 Current children cumulated CPU time (s) 9.79 Current children cumulated vsize (Kb) 21980 [startup+20.0045 s] Raw data (loadavg): 0.94 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 5775 0 0 0 1951 22 0 0 25 0 1 0 1793679033 22634496 5069 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 5526 5069 145 145 0 5381 0 [pid=32351] vsize: 22104 Current children cumulated CPU time (s) 19.73 Current children cumulated vsize (Kb) 24228 [startup+30.0064 s] Raw data (loadavg): 0.95 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 6337 0 0 0 2941 26 0 0 25 0 1 0 1793679033 24961024 5631 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 6094 5631 145 145 0 5949 0 [pid=32351] vsize: 24376 Current children cumulated CPU time (s) 29.67 Current children cumulated vsize (Kb) 26500 [startup+40.0072 s] Raw data (loadavg): 0.95 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 7107 0 0 0 3930 31 0 0 25 0 1 0 1793679033 28098560 6401 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 6860 6401 145 145 0 6715 0 [pid=32351] vsize: 27440 Current children cumulated CPU time (s) 39.61 Current children cumulated vsize (Kb) 29564 [startup+50.0081 s] Raw data (loadavg): 0.96 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 7841 0 0 0 4919 35 0 0 25 0 1 0 1793679033 31100928 7135 4294967295 134512640 135094434 3221224432 3221223056 134557653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 7593 7135 145 145 0 7448 0 [pid=32351] vsize: 30372 Current children cumulated CPU time (s) 49.54 Current children cumulated vsize (Kb) 32496 [startup+60.0099 s] Raw data (loadavg): 0.97 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 8475 0 0 0 5910 39 0 0 25 0 1 0 1793679033 33746944 7769 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 8239 7769 145 145 0 8094 0 [pid=32351] vsize: 32956 Current children cumulated CPU time (s) 59.49 Current children cumulated vsize (Kb) 35080 [startup+70.0108 s] Raw data (loadavg): 0.97 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 9106 0 0 0 6899 43 0 0 25 0 1 0 1793679033 36323328 8400 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 8868 8400 145 145 0 8723 0 [pid=32351] vsize: 35472 Current children cumulated CPU time (s) 69.42 Current children cumulated vsize (Kb) 37596 [startup+80.0126 s] Raw data (loadavg): 0.98 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 9710 0 0 0 7888 47 0 0 25 0 1 0 1793679033 38789120 9004 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 9470 9004 145 145 0 9325 0 [pid=32351] vsize: 37880 Current children cumulated CPU time (s) 79.35 Current children cumulated vsize (Kb) 40004 [startup+90.0135 s] Raw data (loadavg): 0.98 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 10299 0 0 0 8879 51 0 0 25 0 1 0 1793679033 41201664 9593 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 10059 9593 145 145 0 9914 0 [pid=32351] vsize: 40236 Current children cumulated CPU time (s) 89.3 Current children cumulated vsize (Kb) 42360 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 10836 0 0 0 9871 55 0 0 25 0 1 0 1793679033 43401216 10130 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 10596 10130 145 145 0 10451 0 [pid=32351] vsize: 42384 Current children cumulated CPU time (s) 99.26 Current children cumulated vsize (Kb) 44508 [startup+110.016 s] Raw data (loadavg): 0.98 0.96 0.88 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 11371 0 0 0 10863 58 0 0 25 0 1 0 1793679033 45600768 10665 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 11133 10665 145 145 0 10988 0 [pid=32351] vsize: 44532 Current children cumulated CPU time (s) 109.21 Current children cumulated vsize (Kb) 46656 [startup+120.017 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 11957 0 0 0 11853 62 0 0 25 0 1 0 1793679033 48001024 11251 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 11719 11251 145 145 0 11574 0 [pid=32351] vsize: 46876 Current children cumulated CPU time (s) 119.15 Current children cumulated vsize (Kb) 49000 [startup+130.018 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 12658 0 0 0 12841 67 0 0 25 0 1 0 1793679033 50868224 11952 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 12419 11952 145 145 0 12274 0 [pid=32351] vsize: 49676 Current children cumulated CPU time (s) 129.08 Current children cumulated vsize (Kb) 51800 [startup+140.019 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 13327 0 0 0 13831 72 0 0 25 0 1 0 1793679033 53600256 12621 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 13086 12621 145 145 0 12941 0 [pid=32351] vsize: 52344 Current children cumulated CPU time (s) 139.03 Current children cumulated vsize (Kb) 54468 [startup+150.02 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) T 32347 32347 6847 0 -1 0 13970 0 0 0 14821 76 0 0 25 0 1 0 1793679033 56229888 13264 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/32351/statm): 13728 13264 145 145 0 13583 0 [pid=32351] vsize: 54912 Current children cumulated CPU time (s) 148.97 Current children cumulated vsize (Kb) 57036 [startup+160.02 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 14584 0 0 0 15813 80 0 0 25 0 1 0 1793679033 58871808 13878 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 14373 13878 145 145 0 14228 0 [pid=32351] vsize: 57492 Current children cumulated CPU time (s) 158.93 Current children cumulated vsize (Kb) 59616 [startup+170.021 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 15175 0 0 0 16804 84 0 0 25 0 1 0 1793679033 61284352 14469 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 14962 14469 145 145 0 14817 0 [pid=32351] vsize: 59848 Current children cumulated CPU time (s) 168.88 Current children cumulated vsize (Kb) 61972 [startup+180.023 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 15764 0 0 0 17794 88 0 0 22 0 1 0 1793679033 63688704 15058 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 15549 15058 145 145 0 15404 0 [pid=32351] vsize: 62196 Current children cumulated CPU time (s) 178.82 Current children cumulated vsize (Kb) 64320 [startup+190.024 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 16343 0 0 0 18786 93 0 0 25 0 1 0 1793679033 66052096 15637 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 16126 15637 145 145 0 15981 0 [pid=32351] vsize: 64504 Current children cumulated CPU time (s) 188.79 Current children cumulated vsize (Kb) 66628 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 16890 0 0 0 19777 97 0 0 25 0 1 0 1793679033 68284416 16184 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 16671 16184 145 145 0 16526 0 [pid=32351] vsize: 66684 Current children cumulated CPU time (s) 198.74 Current children cumulated vsize (Kb) 68808 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 17689 0 0 0 20765 103 0 0 25 0 1 0 1793679033 71548928 16983 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 17468 16983 145 145 0 17323 0 [pid=32351] vsize: 69872 Current children cumulated CPU time (s) 208.68 Current children cumulated vsize (Kb) 71996 [startup+220.026 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 18390 0 0 0 21755 107 0 0 25 0 1 0 1793679033 74416128 17684 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 18168 17684 145 145 0 18023 0 [pid=32351] vsize: 72672 Current children cumulated CPU time (s) 218.62 Current children cumulated vsize (Kb) 74796 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 19047 0 0 0 22747 111 0 0 25 0 1 0 1793679033 77103104 18341 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 18824 18341 145 145 0 18679 0 [pid=32351] vsize: 75296 Current children cumulated CPU time (s) 228.58 Current children cumulated vsize (Kb) 77420 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 19645 0 0 0 23738 113 0 0 25 0 1 0 1793679033 79544320 18939 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 19420 18939 145 145 0 19275 0 [pid=32351] vsize: 77680 Current children cumulated CPU time (s) 238.51 Current children cumulated vsize (Kb) 79804 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 20260 0 0 0 24728 118 0 0 25 0 1 0 1793679033 82055168 19554 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 20033 19554 145 145 0 19888 0 [pid=32351] vsize: 80132 Current children cumulated CPU time (s) 248.46 Current children cumulated vsize (Kb) 82256 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 20869 0 0 0 25719 122 0 0 25 0 1 0 1793679033 84549632 20163 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 20642 20163 145 145 0 20497 0 [pid=32351] vsize: 82568 Current children cumulated CPU time (s) 258.41 Current children cumulated vsize (Kb) 84692 [startup+270.03 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 21418 0 0 0 26711 125 0 0 25 0 1 0 1793679033 86810624 20712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 21194 20712 145 145 0 21049 0 [pid=32351] vsize: 84776 Current children cumulated CPU time (s) 268.36 Current children cumulated vsize (Kb) 86900 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 21858 0 0 0 27704 128 0 0 25 0 1 0 1793679033 88612864 21152 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 21634 21152 145 145 0 21489 0 [pid=32351] vsize: 86536 Current children cumulated CPU time (s) 278.32 Current children cumulated vsize (Kb) 88660 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 22406 0 0 0 28695 132 0 0 25 0 1 0 1793679033 90845184 21700 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 22179 21700 145 145 0 22034 0 [pid=32351] vsize: 88716 Current children cumulated CPU time (s) 288.27 Current children cumulated vsize (Kb) 90840 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 22985 0 0 0 29686 136 0 0 25 0 1 0 1793679033 93212672 22279 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 22757 22279 145 145 0 22612 0 [pid=32351] vsize: 91028 Current children cumulated CPU time (s) 298.22 Current children cumulated vsize (Kb) 93152 [startup+310.033 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 23592 0 0 0 30676 140 0 0 25 0 1 0 1793679033 95690752 22886 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 23362 22886 145 145 0 23217 0 [pid=32351] vsize: 93448 Current children cumulated CPU time (s) 308.16 Current children cumulated vsize (Kb) 95572 [startup+320.034 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 24035 0 0 0 31668 143 0 0 25 0 1 0 1793679033 97759232 23329 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 23867 23329 145 145 0 23722 0 [pid=32351] vsize: 95468 Current children cumulated CPU time (s) 318.11 Current children cumulated vsize (Kb) 97592 [startup+330.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 24625 0 0 0 32660 147 0 0 25 0 1 0 1793679033 100167680 23919 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 24455 23919 145 145 0 24310 0 [pid=32351] vsize: 97820 Current children cumulated CPU time (s) 328.07 Current children cumulated vsize (Kb) 99944 [startup+340.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 25049 0 0 0 33653 150 0 0 25 0 1 0 1793679033 101896192 24343 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 24877 24343 145 145 0 24732 0 [pid=32351] vsize: 99508 Current children cumulated CPU time (s) 338.03 Current children cumulated vsize (Kb) 101632 [startup+350.037 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) T 32347 32347 6847 0 -1 0 25626 0 0 0 34645 153 0 0 25 0 1 0 1793679033 104251392 24920 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/32351/statm): 25452 24920 145 145 0 25307 0 [pid=32351] vsize: 101808 Current children cumulated CPU time (s) 347.98 Current children cumulated vsize (Kb) 103932 [startup+360.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 26359 0 0 0 35634 157 0 0 21 0 1 0 1793679033 107261952 25653 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 26187 25653 145 145 0 26042 0 [pid=32351] vsize: 104748 Current children cumulated CPU time (s) 357.91 Current children cumulated vsize (Kb) 106872 [startup+370.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 27119 0 0 0 36623 163 0 0 25 0 1 0 1793679033 110370816 26413 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 26946 26413 145 145 0 26801 0 [pid=32351] vsize: 107784 Current children cumulated CPU time (s) 367.86 Current children cumulated vsize (Kb) 109908 [startup+380.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 27655 0 0 0 37614 167 0 0 25 0 1 0 1793679033 112562176 26949 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 27481 26949 145 145 0 27336 0 [pid=32351] vsize: 109924 Current children cumulated CPU time (s) 377.81 Current children cumulated vsize (Kb) 112048 [startup+390.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 28009 0 0 0 38607 170 0 0 25 0 1 0 1793679033 113995776 27303 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 27831 27303 145 145 0 27686 0 [pid=32351] vsize: 111324 Current children cumulated CPU time (s) 387.77 Current children cumulated vsize (Kb) 113448 [startup+400.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 28474 0 0 0 39600 172 0 0 25 0 1 0 1793679033 115888128 27768 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 28293 27768 145 145 0 28148 0 [pid=32351] vsize: 113172 Current children cumulated CPU time (s) 397.72 Current children cumulated vsize (Kb) 115296 [startup+410.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 28906 0 0 0 40594 175 0 0 25 0 1 0 1793679033 117649408 28200 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 28723 28200 145 145 0 28578 0 [pid=32351] vsize: 114892 Current children cumulated CPU time (s) 407.69 Current children cumulated vsize (Kb) 117016 [startup+420.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 29415 0 0 0 41586 178 0 0 25 0 1 0 1793679033 119726080 28709 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 29230 28709 145 145 0 29085 0 [pid=32351] vsize: 116920 Current children cumulated CPU time (s) 417.64 Current children cumulated vsize (Kb) 119044 [startup+430.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 29957 0 0 0 42577 182 0 0 25 0 1 0 1793679033 121937920 29251 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 29770 29251 145 145 0 29625 0 [pid=32351] vsize: 119080 Current children cumulated CPU time (s) 427.59 Current children cumulated vsize (Kb) 121204 [startup+440.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 30514 0 0 0 43568 185 0 0 25 0 1 0 1793679033 124211200 29808 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 30325 29808 145 145 0 30180 0 [pid=32351] vsize: 121300 Current children cumulated CPU time (s) 437.53 Current children cumulated vsize (Kb) 123424 [startup+450.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 31224 0 0 0 44557 190 0 0 25 0 1 0 1793679033 127111168 30518 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 31033 30518 145 145 0 30888 0 [pid=32351] vsize: 124132 Current children cumulated CPU time (s) 447.47 Current children cumulated vsize (Kb) 126256 [startup+460.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 31908 0 0 0 45545 195 0 0 25 0 1 0 1793679033 129904640 31202 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 31715 31202 145 145 0 31570 0 [pid=32351] vsize: 126860 Current children cumulated CPU time (s) 457.4 Current children cumulated vsize (Kb) 128984 [startup+470.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 32548 0 0 0 46535 200 0 0 25 0 1 0 1793679033 132521984 31842 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 32354 31842 145 145 0 32209 0 [pid=32351] vsize: 129416 Current children cumulated CPU time (s) 467.35 Current children cumulated vsize (Kb) 131540 [startup+480.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 33119 0 0 0 47526 203 0 0 25 0 1 0 1793679033 134856704 32413 4294967295 134512640 135094434 3221224432 3221223072 134557059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 32924 32413 145 145 0 32779 0 [pid=32351] vsize: 131696 Current children cumulated CPU time (s) 477.29 Current children cumulated vsize (Kb) 133820 [startup+490.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 33717 0 0 0 48515 207 0 0 25 0 1 0 1793679033 137310208 33011 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 33523 33011 145 145 0 33378 0 [pid=32351] vsize: 134092 Current children cumulated CPU time (s) 487.22 Current children cumulated vsize (Kb) 136216 [startup+500.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 34307 0 0 0 49506 211 0 0 25 0 1 0 1793679033 139718656 33601 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 34111 33601 145 145 0 33966 0 [pid=32351] vsize: 136444 Current children cumulated CPU time (s) 497.17 Current children cumulated vsize (Kb) 138568 [startup+510.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 34781 0 0 0 50500 214 0 0 25 0 1 0 1793679033 141651968 34075 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 34583 34075 145 145 0 34438 0 [pid=32351] vsize: 138332 Current children cumulated CPU time (s) 507.14 Current children cumulated vsize (Kb) 140456 [startup+520.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 35338 0 0 0 51492 217 0 0 25 0 1 0 1793679033 143929344 34632 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 35139 34632 145 145 0 34994 0 [pid=32351] vsize: 140556 Current children cumulated CPU time (s) 517.09 Current children cumulated vsize (Kb) 142680 [startup+530.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 35691 0 0 0 52485 219 0 0 25 0 1 0 1793679033 145371136 34985 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 35491 34985 145 145 0 35346 0 [pid=32351] vsize: 141964 Current children cumulated CPU time (s) 527.04 Current children cumulated vsize (Kb) 144088 [startup+540.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 36276 0 0 0 53477 223 0 0 25 0 1 0 1793679033 147750912 35570 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 36072 35570 145 145 0 35927 0 [pid=32351] vsize: 144288 Current children cumulated CPU time (s) 537 Current children cumulated vsize (Kb) 146412 [startup+550.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 36787 0 0 0 54469 227 0 0 25 0 1 0 1793679033 149835776 36081 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 36581 36081 145 145 0 36436 0 [pid=32351] vsize: 146324 Current children cumulated CPU time (s) 546.96 Current children cumulated vsize (Kb) 148448 [startup+560.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 37113 0 0 0 55462 229 0 0 25 0 1 0 1793679033 151166976 36407 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 36906 36407 145 145 0 36761 0 [pid=32351] vsize: 147624 Current children cumulated CPU time (s) 556.91 Current children cumulated vsize (Kb) 149748 [startup+570.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 37506 0 0 0 56456 232 0 0 25 0 1 0 1793679033 152768512 36800 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 37297 36800 145 145 0 37152 0 [pid=32351] vsize: 149188 Current children cumulated CPU time (s) 566.88 Current children cumulated vsize (Kb) 151312 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 37955 0 0 0 57448 235 0 0 25 0 1 0 1793679033 154603520 37249 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 37745 37249 145 145 0 37600 0 [pid=32351] vsize: 150980 Current children cumulated CPU time (s) 576.83 Current children cumulated vsize (Kb) 153104 [startup+590.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 38500 0 0 0 58439 240 0 0 25 0 1 0 1793679033 156831744 37794 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 38289 37794 145 145 0 38144 0 [pid=32351] vsize: 153156 Current children cumulated CPU time (s) 586.79 Current children cumulated vsize (Kb) 155280 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39054 0 0 0 59431 244 0 0 25 0 1 0 1793679033 159092736 38348 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 38841 38348 145 145 0 38696 0 [pid=32351] vsize: 155364 Current children cumulated CPU time (s) 596.75 Current children cumulated vsize (Kb) 157488 [startup+610.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 60426 246 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 606.72 Current children cumulated vsize (Kb) 159092 [startup+620.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 61425 247 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 616.72 Current children cumulated vsize (Kb) 159092 [startup+630.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 62425 247 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 626.72 Current children cumulated vsize (Kb) 159092 [startup+640.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 63424 247 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 636.71 Current children cumulated vsize (Kb) 159092 [startup+650.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 64424 248 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 646.72 Current children cumulated vsize (Kb) 159092 [startup+660.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 65423 248 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 656.71 Current children cumulated vsize (Kb) 159092 [startup+670.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 66423 248 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 666.71 Current children cumulated vsize (Kb) 159092 [startup+680.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 67422 249 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 676.71 Current children cumulated vsize (Kb) 159092 [startup+690.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 68422 249 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 686.71 Current children cumulated vsize (Kb) 159092 [startup+700.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 69422 250 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 696.72 Current children cumulated vsize (Kb) 159092 [startup+710.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 70421 250 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 706.71 Current children cumulated vsize (Kb) 159092 [startup+720.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 71421 250 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 716.71 Current children cumulated vsize (Kb) 159092 [startup+730.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 72421 251 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 726.72 Current children cumulated vsize (Kb) 159092 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 73420 251 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557300 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 736.71 Current children cumulated vsize (Kb) 159092 [startup+750.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 74420 251 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 746.71 Current children cumulated vsize (Kb) 159092 [startup+760.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 75419 252 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 756.71 Current children cumulated vsize (Kb) 159092 [startup+770.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 76419 252 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 766.71 Current children cumulated vsize (Kb) 159092 [startup+780.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 77419 252 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 776.71 Current children cumulated vsize (Kb) 159092 [startup+790.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 78417 254 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 786.71 Current children cumulated vsize (Kb) 159092 [startup+800.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 79416 255 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 796.71 Current children cumulated vsize (Kb) 159092 [startup+810.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 80415 256 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 806.71 Current children cumulated vsize (Kb) 159092 [startup+820.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 81414 257 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 816.71 Current children cumulated vsize (Kb) 159092 [startup+830.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 82414 257 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 826.71 Current children cumulated vsize (Kb) 159092 [startup+840.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 83413 258 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 836.71 Current children cumulated vsize (Kb) 159092 [startup+850.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 84412 259 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 846.71 Current children cumulated vsize (Kb) 159092 [startup+860.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 85412 259 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 856.71 Current children cumulated vsize (Kb) 159092 [startup+870.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 86411 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 866.71 Current children cumulated vsize (Kb) 159092 [startup+880.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 87411 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 876.71 Current children cumulated vsize (Kb) 159092 [startup+890.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 88411 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 886.71 Current children cumulated vsize (Kb) 159092 [startup+900.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 89410 260 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 896.7 Current children cumulated vsize (Kb) 159092 [startup+910.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 90410 261 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 906.71 Current children cumulated vsize (Kb) 159092 [startup+920.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 91410 261 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 916.71 Current children cumulated vsize (Kb) 159092 [startup+930.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 92409 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 926.71 Current children cumulated vsize (Kb) 159092 [startup+940.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 93409 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 936.71 Current children cumulated vsize (Kb) 159092 [startup+950.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 94409 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 946.71 Current children cumulated vsize (Kb) 159092 [startup+960.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 95408 262 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 956.7 Current children cumulated vsize (Kb) 159092 [startup+970.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 96408 263 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 966.71 Current children cumulated vsize (Kb) 159092 [startup+980.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 97407 263 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557829 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 976.7 Current children cumulated vsize (Kb) 159092 [startup+990.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 98406 264 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 986.7 Current children cumulated vsize (Kb) 159092 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 99406 264 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 996.7 Current children cumulated vsize (Kb) 159092 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 100406 264 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1006.7 Current children cumulated vsize (Kb) 159092 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 101405 265 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1016.7 Current children cumulated vsize (Kb) 159092 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 102405 265 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1026.7 Current children cumulated vsize (Kb) 159092 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 103404 266 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1036.7 Current children cumulated vsize (Kb) 159092 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 104404 266 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1046.7 Current children cumulated vsize (Kb) 159092 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 105404 266 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1056.7 Current children cumulated vsize (Kb) 159092 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 106403 267 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1066.7 Current children cumulated vsize (Kb) 159092 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 107402 268 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1076.7 Current children cumulated vsize (Kb) 159092 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 108402 268 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1086.7 Current children cumulated vsize (Kb) 159092 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39456 0 0 0 109402 268 0 0 25 0 1 0 1793679033 160735232 38750 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39242 38750 145 145 0 39097 0 [pid=32351] vsize: 156968 Current children cumulated CPU time (s) 1096.7 Current children cumulated vsize (Kb) 159092 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39554 0 0 0 110400 269 0 0 25 0 1 0 1793679033 161136640 38848 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39340 38848 145 145 0 39195 0 [pid=32351] vsize: 157360 Current children cumulated CPU time (s) 1106.69 Current children cumulated vsize (Kb) 159484 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 39960 0 0 0 111394 271 0 0 25 0 1 0 1793679033 162799616 39254 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 39746 39254 145 145 0 39601 0 [pid=32351] vsize: 158984 Current children cumulated CPU time (s) 1116.65 Current children cumulated vsize (Kb) 161108 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 40355 0 0 0 112388 274 0 0 25 0 1 0 1793679033 164417536 39649 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 40141 39649 145 145 0 39996 0 [pid=32351] vsize: 160564 Current children cumulated CPU time (s) 1126.62 Current children cumulated vsize (Kb) 162688 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 41050 0 0 0 113380 278 0 0 25 0 1 0 1793679033 167256064 40344 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 40834 40344 145 145 0 40689 0 [pid=32351] vsize: 163336 Current children cumulated CPU time (s) 1136.58 Current children cumulated vsize (Kb) 165460 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 41523 0 0 0 114374 280 0 0 25 0 1 0 1793679033 169193472 40817 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 41307 40817 145 145 0 41162 0 [pid=32351] vsize: 165228 Current children cumulated CPU time (s) 1146.54 Current children cumulated vsize (Kb) 167352 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 42084 0 0 0 115368 283 0 0 25 0 1 0 1793679033 171491328 41378 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 41868 41378 145 145 0 41723 0 [pid=32351] vsize: 167472 Current children cumulated CPU time (s) 1156.51 Current children cumulated vsize (Kb) 169596 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 42549 0 0 0 116363 285 0 0 25 0 1 0 1793679033 173387776 41843 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 42331 41843 145 145 0 42186 0 [pid=32351] vsize: 169324 Current children cumulated CPU time (s) 1166.48 Current children cumulated vsize (Kb) 171448 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 43048 0 0 0 117356 288 0 0 25 0 1 0 1793679033 175427584 42342 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 42829 42342 145 145 0 42684 0 [pid=32351] vsize: 171316 Current children cumulated CPU time (s) 1176.44 Current children cumulated vsize (Kb) 173440 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 43769 0 0 0 118348 291 0 0 25 0 1 0 1793679033 178376704 43063 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32351/statm): 43549 43063 145 145 0 43404 0 [pid=32351] vsize: 174196 Current children cumulated CPU time (s) 1186.39 Current children cumulated vsize (Kb) 176320 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 44502 0 0 0 119338 296 0 0 23 0 1 0 1793679033 181374976 43796 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 44281 43796 145 145 0 44136 0 [pid=32351] vsize: 177124 Current children cumulated CPU time (s) 1196.34 Current children cumulated vsize (Kb) 179248 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 45116 0 0 0 120329 300 0 0 25 0 1 0 1793679033 183885824 44410 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 44894 44410 145 145 0 44749 0 [pid=32351] vsize: 179576 Current children cumulated CPU time (s) 1206.29 Current children cumulated vsize (Kb) 181700 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 32351 Raw data (/proc/32347/stat): 32347 (minisat+_script) S 32346 32347 6847 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1793679028 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/32347/statm): 531 226 485 147 0 384 0 [pid=32347] vsize: 2124 Raw data (/proc/32351/stat): 32351 (minisat+_64-bit) R 32347 32347 6847 0 -1 0 45116 0 0 0 120329 300 0 0 25 0 1 0 1793679033 183885824 44410 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32351/statm): 44894 44410 145 145 0 44749 0 [pid=32351] vsize: 179576 Current children cumulated CPU time (s) 1206.29 Current children cumulated vsize (Kb) 181700 Sending SIGTERM to -32347 Sleeping 2 seconds One traced child (pid=32347) ended because it received signal 15 (SIGTERM) One traced child (pid=32351) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.21 CPU time (s): 1206.38 CPU user time (s): 1203.3 CPU system time (s): 3.08453 CPU usage (%): 99.684 Max. virtual memory (cumulated for all children) (Kb): 181700
ERROR: no interpretation found !