Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-l152lav.opb |
MD5SUM | 9d4ce12b138a2bef65a1f401ec9d1f01 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4732 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1989 |
Biggest coefficient in the objective function | 268 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 382524 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 268 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 382524 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.7 |
Number of variables | 1989 |
Total number of constraints | 2086 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 2085 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1989 |
LAUNCH ON wulflinc27 THE 2005-09-20 04:23:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3364 boxname=wulflinc27 idbench=1020 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9d4ce12b138a2bef65a1f401ec9d1f01 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-l152lav.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-l152lav.opb IDLAUNCH: 3364 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 915604 kB Buffers: 19728 kB Cached: 69952 kB SwapCached: 692 kB Active: 23112 kB Inactive: 69108 kB HighTotal: 131008 kB HighFree: 58744 kB LowTotal: 903652 kB LowFree: 856860 kB SwapTotal: 2097892 kB SwapFree: 2096628 kB Dirty: 52 kB Writeback: 0 kB Mapped: 5732 kB Slab: 21148 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:43:37 (client local time) WITH STATUS 0 IN 1206.69 SECONDS stats: 3364 7 1206.69 0
c Parsing PB file... c Converting 193 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################################################ c -- Clauses(.)/Splits(s): (none) c ---[ 192]---> Adder-cost: 5478 maxlim: 25152 bits: 15/15 c ---[ 190]---> BDD-cost: 3 c ---[ 188]---> BDD-cost: 255 c ---[ 186]---> BDD-cost: 147 c ---[ 184]---> BDD-cost: 83 c ---[ 182]---> BDD-cost: 93 c ---[ 180]---> BDD-cost: 149 c ---[ 178]---> BDD-cost: 235 c ---[ 176]---> BDD-cost: 339 c ---[ 174]---> BDD-cost: 17 c ---[ 172]---> BDD-cost: 21 c ---[ 170]---> BDD-cost: 301 c ---[ 168]---> BDD-cost: 181 c ---[ 166]---> BDD-cost: 87 c ---[ 164]---> BDD-cost: 71 c ---[ 162]---> BDD-cost: 67 c ---[ 160]---> BDD-cost: 57 c ---[ 158]---> BDD-cost: 7 c ---[ 156]---> BDD-cost: 39 c ---[ 154]---> BDD-cost: 85 c ---[ 152]---> BDD-cost: 147 c ---[ 150]---> BDD-cost: 189 c ---[ 148]---> BDD-cost: 211 c ---[ 146]---> BDD-cost: 95 c ---[ 144]---> BDD-cost: 41 c ---[ 142]---> BDD-cost: 35 c ---[ 140]---> BDD-cost: 59 c ---[ 138]---> BDD-cost: 171 c ---[ 136]---> BDD-cost: 59 c ---[ 134]---> BDD-cost: 51 c ---[ 132]---> BDD-cost: 151 c ---[ 130]---> BDD-cost: 147 c ---[ 128]---> BDD-cost: 317 c ---[ 126]---> BDD-cost: 201 c ---[ 124]---> BDD-cost: 105 c ---[ 122]---> BDD-cost: 101 c ---[ 120]---> BDD-cost: 121 c ---[ 118]---> BDD-cost: 133 c ---[ 116]---> BDD-cost: 149 c ---[ 114]---> BDD-cost: 189 c ---[ 112]---> BDD-cost: 77 c ---[ 110]---> BDD-cost: 201 c ---[ 108]---> BDD-cost: 49 c ---[ 106]---> BDD-cost: 81 c ---[ 104]---> BDD-cost: 121 c ---[ 102]---> BDD-cost: 433 c ---[ 100]---> BDD-cost: 191 c ---[ 98]---> BDD-cost: 81 c ---[ 96]---> BDD-cost: 71 c ---[ 94]---> BDD-cost: 103 c ---[ 92]---> BDD-cost: 93 c ---[ 90]---> BDD-cost: 85 c ---[ 88]---> BDD-cost: 189 c ---[ 86]---> BDD-cost: 231 c ---[ 84]---> BDD-cost: 101 c ---[ 82]---> BDD-cost: 109 c ---[ 80]---> BDD-cost: 171 c ---[ 78]---> BDD-cost: 183 c ---[ 76]---> BDD-cost: 173 c ---[ 74]---> BDD-cost: 239 c ---[ 72]---> BDD-cost: 91 c ---[ 70]---> BDD-cost: 271 c ---[ 68]---> BDD-cost: 239 c ---[ 66]---> BDD-cost: 105 c ---[ 64]---> BDD-cost: 117 c ---[ 62]---> BDD-cost: 221 c ---[ 60]---> BDD-cost: 213 c ---[ 58]---> BDD-cost: 145 c ---[ 56]---> BDD-cost: 179 c ---[ 54]---> BDD-cost: 213 c ---[ 52]---> BDD-cost: 143 c ---[ 50]---> BDD-cost: 209 c ---[ 48]---> BDD-cost: 81 c ---[ 46]---> BDD-cost: 205 c ---[ 44]---> BDD-cost: 61 c ---[ 42]---> BDD-cost: 225 c ---[ 40]---> BDD-cost: 129 c ---[ 38]---> BDD-cost: 253 c ---[ 36]---> BDD-cost: 71 c ---[ 34]---> BDD-cost: 203 c ---[ 32]---> BDD-cost: 45 c ---[ 30]---> BDD-cost: 133 c ---[ 28]---> BDD-cost: 323 c ---[ 26]---> BDD-cost: 155 c ---[ 24]---> BDD-cost: 89 c ---[ 22]---> BDD-cost: 93 c ---[ 20]---> BDD-cost: 83 c ---[ 18]---> BDD-cost: 67 c ---[ 16]---> BDD-cost: 133 c ---[ 14]---> BDD-cost: 247 c ---[ 12]---> BDD-cost: 97 c ---[ 10]---> BDD-cost: 97 c ---[ 8]---> BDD-cost: 151 c ---[ 6]---> BDD-cost: 181 c ---[ 4]---> BDD-cost: 151 c ---[ 2]---> BDD-cost: 181 c ---[ 0]---> Adder-cost: 3598 maxlim: 1961 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 97077 314005 | 32359 0 0 nan | 0.000 % | c | 100 | 96947 313559 | 35594 82 1270 15.5 | 0.582 % | c | 251 | 96883 313337 | 39154 212 15944 75.2 | 0.639 % | c | 476 | 96883 313337 | 43069 437 24593 56.3 | 0.639 % | c | 813 | 96398 311624 | 47376 699 28796 41.2 | 0.981 % | c | 1320 | 96280 311210 | 52114 1189 64686 54.4 | 1.062 % | c | 2079 | 96249 311105 | 57325 1943 92323 47.5 | 1.079 % | c | 3223 | 96179 310853 | 63058 3077 320979 104.3 | 1.123 % | c | 4931 | 96005 310207 | 69364 4745 498190 105.0 | 1.229 % | c | 7493 | 95381 308039 | 76300 7204 629523 87.4 | 1.673 % | c | 11337 | 94537 305108 | 83930 10849 722117 66.6 | 2.263 % | c | 17103 | 94126 303709 | 92324 16521 986489 59.7 | 2.520 % | c | 25752 | 93634 301995 | 101556 25094 1804121 71.9 | 2.821 % | c | 38728 | 93305 300886 | 111712 38012 3779797 99.4 | 3.028 % | c | 58192 | 93290 300833 | 122883 57465 9794628 170.4 | 3.032 % | c | 87386 | 93201 300510 | 135171 86640 15885253 183.3 | 3.085 % | c | 131175 | 93099 300164 | 148688 130408 28212586 216.3 | 3.150 % | c | 196860 | 92835 299270 | 163557 74455 14452111 194.1 | 3.289 % |
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/28125/stat): 28125 (minisat+_script) R 28124 28125 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855612431 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/28125/statm): 174 3 169 147 0 27 0 [pid=28125] 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=28126 New process pid=28127 New process pid=28128 execve syscall for /bin/sed executable One traced child (pid=28127) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=28128) exited with status: 0 One traced child (pid=28126) exited with status: 0 New process pid=28129 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-l152lav.opb [startup+10.0033 s] Raw data (loadavg): 0.94 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4203 0 0 0 962 15 0 0 25 0 1 0 1855612436 18100224 3813 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 4419 3813 145 145 0 4274 0 [pid=28129] vsize: 17676 Current children cumulated CPU time (s) 9.79 Current children cumulated vsize (Kb) 19800 [startup+20.0041 s] Raw data (loadavg): 0.95 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4576 0 0 0 1956 17 0 0 25 0 1 0 1855612436 19632128 4186 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 4793 4186 145 145 0 4648 0 [pid=28129] vsize: 19172 Current children cumulated CPU time (s) 19.75 Current children cumulated vsize (Kb) 21296 [startup+30.006 s] Raw data (loadavg): 0.95 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4727 0 0 0 2953 18 0 0 25 0 1 0 1855612436 20275200 4337 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 4950 4337 145 145 0 4805 0 [pid=28129] vsize: 19800 Current children cumulated CPU time (s) 29.73 Current children cumulated vsize (Kb) 21924 [startup+40.0068 s] Raw data (loadavg): 0.96 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 4846 0 0 0 3950 19 0 0 25 0 1 0 1855612436 20750336 4456 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 5066 4456 145 145 0 4921 0 [pid=28129] vsize: 20264 Current children cumulated CPU time (s) 39.71 Current children cumulated vsize (Kb) 22388 [startup+50.0076 s] Raw data (loadavg): 0.97 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 5074 0 0 0 4946 21 0 0 25 0 1 0 1855612436 21667840 4684 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 5290 4684 145 145 0 5145 0 [pid=28129] vsize: 21160 Current children cumulated CPU time (s) 49.69 Current children cumulated vsize (Kb) 23284 [startup+60.0084 s] Raw data (loadavg): 0.97 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 5459 0 0 0 5941 22 0 0 25 0 1 0 1855612436 23289856 5069 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 5686 5069 145 145 0 5541 0 [pid=28129] vsize: 22744 Current children cumulated CPU time (s) 59.65 Current children cumulated vsize (Kb) 24868 [startup+70.0092 s] Raw data (loadavg): 0.97 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 5828 0 0 0 6935 25 0 0 25 0 1 0 1855612436 24788992 5438 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 6052 5438 145 145 0 5907 0 [pid=28129] vsize: 24208 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 26332 [startup+80.0101 s] Raw data (loadavg): 0.98 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 6138 0 0 0 7929 28 0 0 25 0 1 0 1855612436 26042368 5748 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 6358 5748 145 145 0 6213 0 [pid=28129] vsize: 25432 Current children cumulated CPU time (s) 79.59 Current children cumulated vsize (Kb) 27556 [startup+90.0109 s] Raw data (loadavg): 0.98 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 6606 0 0 0 8921 31 0 0 25 0 1 0 1855612436 27947008 6216 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 6823 6216 145 145 0 6678 0 [pid=28129] vsize: 27292 Current children cumulated CPU time (s) 89.54 Current children cumulated vsize (Kb) 29416 [startup+100.012 s] Raw data (loadavg): 0.98 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 7283 0 0 0 9912 35 0 0 25 0 1 0 1855612436 30711808 6893 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 7498 6893 145 145 0 7353 0 [pid=28129] vsize: 29992 Current children cumulated CPU time (s) 99.49 Current children cumulated vsize (Kb) 32116 [startup+110.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 7536 0 0 0 10908 36 0 0 25 0 1 0 1855612436 31870976 7146 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 7781 7146 145 145 0 7636 0 [pid=28129] vsize: 31124 Current children cumulated CPU time (s) 109.46 Current children cumulated vsize (Kb) 33248 [startup+120.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 8022 0 0 0 11900 38 0 0 25 0 1 0 1855612436 33849344 7632 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 8264 7632 145 145 0 8119 0 [pid=28129] vsize: 33056 Current children cumulated CPU time (s) 119.4 Current children cumulated vsize (Kb) 35180 [startup+130.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 8413 0 0 0 12891 42 0 0 25 0 1 0 1855612436 35438592 8023 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 8652 8023 145 145 0 8507 0 [pid=28129] vsize: 34608 Current children cumulated CPU time (s) 129.35 Current children cumulated vsize (Kb) 36732 [startup+140.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 8967 0 0 0 13883 46 0 0 25 0 1 0 1855612436 37695488 8577 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 9203 8577 145 145 0 9058 0 [pid=28129] vsize: 36812 Current children cumulated CPU time (s) 139.31 Current children cumulated vsize (Kb) 38936 [startup+150.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 9555 0 0 0 14873 49 0 0 25 0 1 0 1855612436 40095744 9165 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 9789 9165 145 145 0 9644 0 [pid=28129] vsize: 39156 Current children cumulated CPU time (s) 149.24 Current children cumulated vsize (Kb) 41280 [startup+160.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 10100 0 0 0 15866 53 0 0 25 0 1 0 1855612436 42319872 9710 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 10332 9710 145 145 0 10187 0 [pid=28129] vsize: 41328 Current children cumulated CPU time (s) 159.21 Current children cumulated vsize (Kb) 43452 [startup+170.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 10607 0 0 0 16857 56 0 0 25 0 1 0 1855612436 44392448 10217 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 10838 10217 145 145 0 10693 0 [pid=28129] vsize: 43352 Current children cumulated CPU time (s) 169.15 Current children cumulated vsize (Kb) 45476 [startup+180.017 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 11089 0 0 0 17849 60 0 0 25 0 1 0 1855612436 46362624 10699 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 11319 10699 145 145 0 11174 0 [pid=28129] vsize: 45276 Current children cumulated CPU time (s) 179.11 Current children cumulated vsize (Kb) 47400 [startup+190.018 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 11545 0 0 0 18841 62 0 0 25 0 1 0 1855612436 48230400 11155 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 11775 11155 145 145 0 11630 0 [pid=28129] vsize: 47100 Current children cumulated CPU time (s) 189.05 Current children cumulated vsize (Kb) 49224 [startup+200.019 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 11970 0 0 0 19834 65 0 0 25 0 1 0 1855612436 49971200 11580 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 12200 11580 145 145 0 12055 0 [pid=28129] vsize: 48800 Current children cumulated CPU time (s) 199.01 Current children cumulated vsize (Kb) 50924 [startup+210.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 12325 0 0 0 20829 67 0 0 25 0 1 0 1855612436 51433472 11935 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 12557 11935 145 145 0 12412 0 [pid=28129] vsize: 50228 Current children cumulated CPU time (s) 208.98 Current children cumulated vsize (Kb) 52352 [startup+220.021 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 12654 0 0 0 21822 69 0 0 25 0 1 0 1855612436 52776960 12264 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 12885 12264 145 145 0 12740 0 [pid=28129] vsize: 51540 Current children cumulated CPU time (s) 218.93 Current children cumulated vsize (Kb) 53664 [startup+230.021 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 12967 0 0 0 22817 70 0 0 25 0 1 0 1855612436 54054912 12577 4294967295 134512640 135094434 3221224432 3221223104 134556094 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 13197 12577 145 145 0 13052 0 [pid=28129] vsize: 52788 Current children cumulated CPU time (s) 228.89 Current children cumulated vsize (Kb) 54912 [startup+240.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 13299 0 0 0 23812 73 0 0 25 0 1 0 1855612436 55406592 12909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 13527 12909 145 145 0 13382 0 [pid=28129] vsize: 54108 Current children cumulated CPU time (s) 238.87 Current children cumulated vsize (Kb) 56232 [startup+250.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 13671 0 0 0 24807 75 0 0 25 0 1 0 1855612436 56922112 13281 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 13897 13281 145 145 0 13752 0 [pid=28129] vsize: 55588 Current children cumulated CPU time (s) 248.84 Current children cumulated vsize (Kb) 57712 [startup+260.024 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 14142 0 0 0 25799 79 0 0 25 0 1 0 1855612436 58855424 13752 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 14369 13752 145 145 0 14224 0 [pid=28129] vsize: 57476 Current children cumulated CPU time (s) 258.8 Current children cumulated vsize (Kb) 59600 [startup+270.025 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 14568 0 0 0 26792 82 0 0 25 0 1 0 1855612436 60592128 14178 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 14793 14178 145 145 0 14648 0 [pid=28129] vsize: 59172 Current children cumulated CPU time (s) 268.76 Current children cumulated vsize (Kb) 61296 [startup+280.027 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 15004 0 0 0 27783 85 0 0 25 0 1 0 1855612436 62365696 14614 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 15226 14614 145 145 0 15081 0 [pid=28129] vsize: 60904 Current children cumulated CPU time (s) 278.7 Current children cumulated vsize (Kb) 63028 [startup+290.027 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 15467 0 0 0 28777 87 0 0 25 0 1 0 1855612436 64253952 15077 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 15687 15077 145 145 0 15542 0 [pid=28129] vsize: 62748 Current children cumulated CPU time (s) 288.66 Current children cumulated vsize (Kb) 64872 [startup+300.028 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 15916 0 0 0 29769 90 0 0 25 0 1 0 1855612436 66347008 15526 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 16198 15526 145 145 0 16053 0 [pid=28129] vsize: 64792 Current children cumulated CPU time (s) 298.61 Current children cumulated vsize (Kb) 66916 [startup+310.029 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 16348 0 0 0 30762 94 0 0 25 0 1 0 1855612436 68112384 15958 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 16629 15958 145 145 0 16484 0 [pid=28129] vsize: 66516 Current children cumulated CPU time (s) 308.58 Current children cumulated vsize (Kb) 68640 [startup+320.029 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 16665 0 0 0 31757 96 0 0 25 0 1 0 1855612436 69402624 16275 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 16944 16275 145 145 0 16799 0 [pid=28129] vsize: 67776 Current children cumulated CPU time (s) 318.55 Current children cumulated vsize (Kb) 69900 [startup+330.03 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 17076 0 0 0 32748 99 0 0 25 0 1 0 1855612436 71073792 16686 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 17352 16686 145 145 0 17207 0 [pid=28129] vsize: 69408 Current children cumulated CPU time (s) 328.49 Current children cumulated vsize (Kb) 71532 [startup+340.031 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 17610 0 0 0 33740 103 0 0 25 0 1 0 1855612436 73252864 17220 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 17884 17220 145 145 0 17739 0 [pid=28129] vsize: 71536 Current children cumulated CPU time (s) 338.45 Current children cumulated vsize (Kb) 73660 [startup+350.032 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 18065 0 0 0 34733 106 0 0 25 0 1 0 1855612436 75108352 17675 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 18337 17675 145 145 0 18192 0 [pid=28129] vsize: 73348 Current children cumulated CPU time (s) 348.41 Current children cumulated vsize (Kb) 75472 [startup+360.033 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 18582 0 0 0 35726 109 0 0 25 0 1 0 1855612436 77221888 18192 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 18853 18192 145 145 0 18708 0 [pid=28129] vsize: 75412 Current children cumulated CPU time (s) 358.37 Current children cumulated vsize (Kb) 77536 [startup+370.034 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 19020 0 0 0 36719 112 0 0 25 0 1 0 1855612436 79007744 18630 4294967295 134512640 135094434 3221224432 3221223104 134555821 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 19289 18630 145 145 0 19144 0 [pid=28129] vsize: 77156 Current children cumulated CPU time (s) 368.33 Current children cumulated vsize (Kb) 79280 [startup+380.035 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 19468 0 0 0 37711 115 0 0 25 0 1 0 1855612436 80838656 19078 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 19736 19078 145 145 0 19591 0 [pid=28129] vsize: 78944 Current children cumulated CPU time (s) 378.28 Current children cumulated vsize (Kb) 81068 [startup+390.036 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 19923 0 0 0 38704 118 0 0 25 0 1 0 1855612436 82694144 19533 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 20189 19533 145 145 0 20044 0 [pid=28129] vsize: 80756 Current children cumulated CPU time (s) 388.24 Current children cumulated vsize (Kb) 82880 [startup+400.036 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 20387 0 0 0 39698 121 0 0 25 0 1 0 1855612436 84586496 19997 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 20651 19997 145 145 0 20506 0 [pid=28129] vsize: 82604 Current children cumulated CPU time (s) 398.21 Current children cumulated vsize (Kb) 84728 [startup+410.037 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 20780 0 0 0 40692 124 0 0 25 0 1 0 1855612436 86188032 20390 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 21042 20390 145 145 0 20897 0 [pid=28129] vsize: 84168 Current children cumulated CPU time (s) 408.18 Current children cumulated vsize (Kb) 86292 [startup+420.038 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 21135 0 0 0 41685 125 0 0 25 0 1 0 1855612436 87633920 20745 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 21395 20745 145 145 0 21250 0 [pid=28129] vsize: 85580 Current children cumulated CPU time (s) 418.12 Current children cumulated vsize (Kb) 87704 [startup+430.039 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 21547 0 0 0 42678 129 0 0 25 0 1 0 1855612436 89313280 21157 4294967295 134512640 135094434 3221224432 3221223024 134556980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 21805 21157 145 145 0 21660 0 [pid=28129] vsize: 87220 Current children cumulated CPU time (s) 428.09 Current children cumulated vsize (Kb) 89344 [startup+440.039 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 22039 0 0 0 43670 132 0 0 25 0 1 0 1855612436 91324416 21649 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 22296 21649 145 145 0 22151 0 [pid=28129] vsize: 89184 Current children cumulated CPU time (s) 438.04 Current children cumulated vsize (Kb) 91308 [startup+450.041 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 22573 0 0 0 44663 134 0 0 25 0 1 0 1855612436 93503488 22183 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 22828 22183 145 145 0 22683 0 [pid=28129] vsize: 91312 Current children cumulated CPU time (s) 447.99 Current children cumulated vsize (Kb) 93436 [startup+460.041 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 23105 0 0 0 45654 138 0 0 25 0 1 0 1855612436 95682560 22715 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 23360 22715 145 145 0 23215 0 [pid=28129] vsize: 93440 Current children cumulated CPU time (s) 457.94 Current children cumulated vsize (Kb) 95564 [startup+470.041 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 23607 0 0 0 46648 140 0 0 25 0 1 0 1855612436 97738752 23217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 23862 23217 145 145 0 23717 0 [pid=28129] vsize: 95448 Current children cumulated CPU time (s) 467.9 Current children cumulated vsize (Kb) 97572 [startup+480.042 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 23960 0 0 0 47642 143 0 0 25 0 1 0 1855612436 99180544 23570 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 24214 23570 145 145 0 24069 0 [pid=28129] vsize: 96856 Current children cumulated CPU time (s) 477.87 Current children cumulated vsize (Kb) 98980 [startup+490.043 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 24337 0 0 0 48637 145 0 0 25 0 1 0 1855612436 100716544 23947 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 24589 23947 145 145 0 24444 0 [pid=28129] vsize: 98356 Current children cumulated CPU time (s) 487.84 Current children cumulated vsize (Kb) 100480 [startup+500.044 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 24634 0 0 0 49632 147 0 0 25 0 1 0 1855612436 101924864 24244 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 24884 24244 145 145 0 24739 0 [pid=28129] vsize: 99536 Current children cumulated CPU time (s) 497.81 Current children cumulated vsize (Kb) 101660 [startup+510.045 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 25070 0 0 0 50626 151 0 0 25 0 1 0 1855612436 103706624 24680 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 25319 24680 145 145 0 25174 0 [pid=28129] vsize: 101276 Current children cumulated CPU time (s) 507.79 Current children cumulated vsize (Kb) 103400 [startup+520.045 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 25554 0 0 0 51617 155 0 0 25 0 1 0 1855612436 105680896 25164 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 25801 25164 145 145 0 25656 0 [pid=28129] vsize: 103204 Current children cumulated CPU time (s) 517.74 Current children cumulated vsize (Kb) 105328 [startup+530.046 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 26025 0 0 0 52610 157 0 0 25 0 1 0 1855612436 107606016 25635 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 26271 25635 145 145 0 26126 0 [pid=28129] vsize: 105084 Current children cumulated CPU time (s) 527.69 Current children cumulated vsize (Kb) 107208 [startup+540.047 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 26451 0 0 0 53604 160 0 0 25 0 1 0 1855612436 109346816 26061 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 26696 26061 145 145 0 26551 0 [pid=28129] vsize: 106784 Current children cumulated CPU time (s) 537.66 Current children cumulated vsize (Kb) 108908 [startup+550.048 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 26892 0 0 0 54595 165 0 0 25 0 1 0 1855612436 111144960 26502 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 27135 26502 145 145 0 26990 0 [pid=28129] vsize: 108540 Current children cumulated CPU time (s) 547.62 Current children cumulated vsize (Kb) 110664 [startup+560.049 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 27342 0 0 0 55588 168 0 0 25 0 1 0 1855612436 112984064 26952 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 27584 26952 145 145 0 27439 0 [pid=28129] vsize: 110336 Current children cumulated CPU time (s) 557.58 Current children cumulated vsize (Kb) 112460 [startup+570.049 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 27750 0 0 0 56581 172 0 0 25 0 1 0 1855612436 114651136 27360 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 27991 27360 145 145 0 27846 0 [pid=28129] vsize: 111964 Current children cumulated CPU time (s) 567.55 Current children cumulated vsize (Kb) 114088 [startup+580.05 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 28145 0 0 0 57572 175 0 0 25 0 1 0 1855612436 116264960 27755 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 28385 27755 145 145 0 28240 0 [pid=28129] vsize: 113540 Current children cumulated CPU time (s) 577.49 Current children cumulated vsize (Kb) 115664 [startup+590.051 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 28540 0 0 0 58567 178 0 0 25 0 1 0 1855612436 117878784 28150 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 28779 28150 145 145 0 28634 0 [pid=28129] vsize: 115116 Current children cumulated CPU time (s) 587.47 Current children cumulated vsize (Kb) 117240 [startup+600.052 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 28872 0 0 0 59562 180 0 0 25 0 1 0 1855612436 119230464 28482 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 29109 28482 145 145 0 28964 0 [pid=28129] vsize: 116436 Current children cumulated CPU time (s) 597.44 Current children cumulated vsize (Kb) 118560 [startup+610.053 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 29378 0 0 0 60554 183 0 0 25 0 1 0 1855612436 121307136 28988 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 29616 28988 145 145 0 29471 0 [pid=28129] vsize: 118464 Current children cumulated CPU time (s) 607.39 Current children cumulated vsize (Kb) 120588 [startup+620.054 s] Raw data (loadavg): 0.99 0.98 0.93 1/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) T 28125 28125 28974 0 -1 0 29897 0 0 0 61547 186 0 0 25 0 1 0 1855612436 123428864 29507 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/28129/statm): 30134 29507 145 145 0 29989 0 [pid=28129] vsize: 120536 Current children cumulated CPU time (s) 617.35 Current children cumulated vsize (Kb) 122660 [startup+630.055 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 30586 0 0 0 62535 191 0 0 25 0 1 0 1855612436 126238720 30196 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 30820 30196 145 145 0 30675 0 [pid=28129] vsize: 123280 Current children cumulated CPU time (s) 627.28 Current children cumulated vsize (Kb) 125404 [startup+640.056 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 31194 0 0 0 63527 194 0 0 25 0 1 0 1855612436 128724992 30804 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 31427 30804 145 145 0 31282 0 [pid=28129] vsize: 125708 Current children cumulated CPU time (s) 637.23 Current children cumulated vsize (Kb) 127832 [startup+650.057 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 31576 0 0 0 64520 198 0 0 24 0 1 0 1855612436 130281472 31186 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 31807 31186 145 145 0 31662 0 [pid=28129] vsize: 127228 Current children cumulated CPU time (s) 647.2 Current children cumulated vsize (Kb) 129352 [startup+660.058 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 32149 0 0 0 65512 201 0 0 25 0 1 0 1855612436 132624384 31759 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 32379 31759 145 145 0 32234 0 [pid=28129] vsize: 129516 Current children cumulated CPU time (s) 657.15 Current children cumulated vsize (Kb) 131640 [startup+670.059 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 32635 0 0 0 66503 206 0 0 25 0 1 0 1855612436 134610944 32245 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 32864 32245 145 145 0 32719 0 [pid=28129] vsize: 131456 Current children cumulated CPU time (s) 667.11 Current children cumulated vsize (Kb) 133580 [startup+680.06 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 32982 0 0 0 67496 209 0 0 24 0 1 0 1855612436 136024064 32592 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 33209 32592 145 145 0 33064 0 [pid=28129] vsize: 132836 Current children cumulated CPU time (s) 677.07 Current children cumulated vsize (Kb) 134960 [startup+690.06 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 33304 0 0 0 68491 211 0 0 25 0 1 0 1855612436 137338880 32914 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 33530 32914 145 145 0 33385 0 [pid=28129] vsize: 134120 Current children cumulated CPU time (s) 687.04 Current children cumulated vsize (Kb) 136244 [startup+700.061 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 33508 0 0 0 69486 214 0 0 25 0 1 0 1855612436 138690560 33118 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 33860 33118 145 145 0 33715 0 [pid=28129] vsize: 135440 Current children cumulated CPU time (s) 697.02 Current children cumulated vsize (Kb) 137564 [startup+710.062 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 33789 0 0 0 70481 215 0 0 25 0 1 0 1855612436 139837440 33399 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 34140 33399 145 145 0 33995 0 [pid=28129] vsize: 136560 Current children cumulated CPU time (s) 706.98 Current children cumulated vsize (Kb) 138684 [startup+720.062 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) T 28125 28125 28974 0 -1 0 34296 0 0 0 71473 219 0 0 25 0 1 0 1855612436 141910016 33906 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/28129/statm): 34646 33906 145 145 0 34501 0 [pid=28129] vsize: 138584 Current children cumulated CPU time (s) 716.94 Current children cumulated vsize (Kb) 140708 [startup+730.063 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 34922 0 0 0 72464 223 0 0 25 0 1 0 1855612436 144465920 34532 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 35270 34532 145 145 0 35125 0 [pid=28129] vsize: 141080 Current children cumulated CPU time (s) 726.89 Current children cumulated vsize (Kb) 143204 [startup+740.063 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 35465 0 0 0 73456 226 0 0 25 0 1 0 1855612436 146685952 35075 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 35812 35075 145 145 0 35667 0 [pid=28129] vsize: 143248 Current children cumulated CPU time (s) 736.84 Current children cumulated vsize (Kb) 145372 [startup+750.064 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 35951 0 0 0 74448 229 0 0 25 0 1 0 1855612436 148672512 35561 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 36297 35561 145 145 0 36152 0 [pid=28129] vsize: 145188 Current children cumulated CPU time (s) 746.79 Current children cumulated vsize (Kb) 147312 [startup+760.065 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 36396 0 0 0 75443 231 0 0 25 0 1 0 1855612436 150491136 36006 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 36741 36006 145 145 0 36596 0 [pid=28129] vsize: 146964 Current children cumulated CPU time (s) 756.76 Current children cumulated vsize (Kb) 149088 [startup+770.065 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 36873 0 0 0 76436 234 0 0 25 0 1 0 1855612436 152440832 36483 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 37217 36483 145 145 0 37072 0 [pid=28129] vsize: 148868 Current children cumulated CPU time (s) 766.72 Current children cumulated vsize (Kb) 150992 [startup+780.066 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 37288 0 0 0 77431 237 0 0 25 0 1 0 1855612436 154132480 36898 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 37630 36898 145 145 0 37485 0 [pid=28129] vsize: 150520 Current children cumulated CPU time (s) 776.7 Current children cumulated vsize (Kb) 152644 [startup+790.067 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 37614 0 0 0 78424 239 0 0 25 0 1 0 1855612436 155467776 37224 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 37956 37224 145 145 0 37811 0 [pid=28129] vsize: 151824 Current children cumulated CPU time (s) 786.65 Current children cumulated vsize (Kb) 153948 [startup+800.068 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38039 0 0 0 79418 241 0 0 25 0 1 0 1855612436 157204480 37649 4294967295 134512640 135094434 3221224432 3221223104 134556295 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 38380 37649 145 145 0 38235 0 [pid=28129] vsize: 153520 Current children cumulated CPU time (s) 796.61 Current children cumulated vsize (Kb) 155644 [startup+810.069 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38431 0 0 0 80412 244 0 0 25 0 1 0 1855612436 158810112 38041 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 38772 38041 145 145 0 38627 0 [pid=28129] vsize: 155088 Current children cumulated CPU time (s) 806.58 Current children cumulated vsize (Kb) 157212 [startup+820.07 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38754 0 0 0 81408 246 0 0 25 0 1 0 1855612436 160129024 38364 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39094 38364 145 145 0 38949 0 [pid=28129] vsize: 156376 Current children cumulated CPU time (s) 816.56 Current children cumulated vsize (Kb) 158500 [startup+830.071 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 82406 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 826.55 Current children cumulated vsize (Kb) 158916 [startup+840.072 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 83407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 836.56 Current children cumulated vsize (Kb) 158916 [startup+850.073 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 84407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 846.56 Current children cumulated vsize (Kb) 158916 [startup+860.073 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 85407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 856.56 Current children cumulated vsize (Kb) 158916 [startup+870.074 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 86407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 866.56 Current children cumulated vsize (Kb) 158916 [startup+880.075 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 87407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 876.56 Current children cumulated vsize (Kb) 158916 [startup+890.076 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 88407 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 886.56 Current children cumulated vsize (Kb) 158916 [startup+900.078 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 89408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 896.57 Current children cumulated vsize (Kb) 158916 [startup+910.078 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 90408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 906.57 Current children cumulated vsize (Kb) 158916 [startup+920.078 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 91408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 916.57 Current children cumulated vsize (Kb) 158916 [startup+930.079 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 92408 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 926.57 Current children cumulated vsize (Kb) 158916 [startup+940.08 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 93409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 936.58 Current children cumulated vsize (Kb) 158916 [startup+950.081 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 94409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 946.58 Current children cumulated vsize (Kb) 158916 [startup+960.082 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 95409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 956.58 Current children cumulated vsize (Kb) 158916 [startup+970.082 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 96409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 966.58 Current children cumulated vsize (Kb) 158916 [startup+980.083 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 97409 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 976.58 Current children cumulated vsize (Kb) 158916 [startup+990.084 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 98410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 986.59 Current children cumulated vsize (Kb) 158916 [startup+1000.08 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 99410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 996.59 Current children cumulated vsize (Kb) 158916 [startup+1010.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 100410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557488 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1006.59 Current children cumulated vsize (Kb) 158916 [startup+1020.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 101410 247 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1016.59 Current children cumulated vsize (Kb) 158916 [startup+1030.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 102410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557360 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1026.6 Current children cumulated vsize (Kb) 158916 [startup+1040.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 103410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1036.6 Current children cumulated vsize (Kb) 158916 [startup+1050.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 104410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1046.6 Current children cumulated vsize (Kb) 158916 [startup+1060.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 105410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1056.6 Current children cumulated vsize (Kb) 158916 [startup+1070.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 106410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1066.6 Current children cumulated vsize (Kb) 158916 [startup+1080.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 107410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1076.6 Current children cumulated vsize (Kb) 158916 [startup+1090.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 108410 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1086.6 Current children cumulated vsize (Kb) 158916 [startup+1100.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 109411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1096.61 Current children cumulated vsize (Kb) 158916 [startup+1110.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 110411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1106.61 Current children cumulated vsize (Kb) 158916 [startup+1120.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 111411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1116.61 Current children cumulated vsize (Kb) 158916 [startup+1130.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 112411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1126.61 Current children cumulated vsize (Kb) 158916 [startup+1140.09 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 113411 248 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1136.61 Current children cumulated vsize (Kb) 158916 [startup+1150.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 114410 249 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1146.61 Current children cumulated vsize (Kb) 158916 [startup+1160.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 115410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1156.62 Current children cumulated vsize (Kb) 158916 [startup+1170.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 116410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1166.62 Current children cumulated vsize (Kb) 158916 [startup+1180.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 117410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1176.62 Current children cumulated vsize (Kb) 158916 [startup+1190.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 118410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1186.62 Current children cumulated vsize (Kb) 158916 [startup+1200.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 119410 250 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1196.62 Current children cumulated vsize (Kb) 158916 [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 120410 251 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134556421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1206.63 Current children cumulated vsize (Kb) 158916 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 28129 Raw data (/proc/28125/stat): 28125 (minisat+_script) S 28124 28125 28974 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855612431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28125/statm): 531 226 485 147 0 384 0 [pid=28125] vsize: 2124 Raw data (/proc/28129/stat): 28129 (minisat+_64-bit) R 28125 28125 28974 0 -1 0 38859 0 0 0 120410 251 0 0 25 0 1 0 1855612436 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28129/statm): 39198 38469 145 145 0 39053 0 [pid=28129] vsize: 156792 Current children cumulated CPU time (s) 1206.63 Current children cumulated vsize (Kb) 158916 Sending SIGTERM to -28125 Sleeping 2 seconds One traced child (pid=28125) ended because it received signal 15 (SIGTERM) One traced child (pid=28129) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.18 CPU time (s): 1206.69 CPU user time (s): 1204.11 CPU system time (s): 2.58461 CPU usage (%): 99.7121 Max. virtual memory (cumulated for all children) (Kb): 158916
ERROR: no interpretation found !