Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.44 |
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 wulflinc2 THE 2005-09-19 18:02:18 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2980 boxname=wulflinc2 idbench=636 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9d4ce12b138a2bef65a1f401ec9d1f01 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-l152lav.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-l152lav.opb IDLAUNCH: 2980 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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 : 2 cpu MHz : 451.191 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: 857184 kB Buffers: 39840 kB Cached: 111168 kB SwapCached: 1040 kB Active: 64084 kB Inactive: 89560 kB HighTotal: 131008 kB HighFree: 27300 kB LowTotal: 903652 kB LowFree: 829884 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 18272 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:22:28 (client local time) WITH STATUS 0 IN 1206.72 SECONDS stats: 2980 7 1206.72 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/28475/stat): 28475 (minisat+_script) R 28474 28475 6872 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793685383 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/28475/statm): 174 3 169 147 0 27 0 [pid=28475] 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=28476 New process pid=28477 New process pid=28478 execve syscall for /bin/sed executable One traced child (pid=28477) 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=28478) exited with status: 0 One traced child (pid=28476) exited with status: 0 New process pid=28479 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-l152lav.opb [startup+10.0036 s] Raw data (loadavg): 0.87 0.94 0.79 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4202 0 0 0 964 17 0 0 25 0 1 0 1793685388 18096128 3812 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 4418 3812 145 145 0 4273 0 [pid=28479] vsize: 17672 Current children cumulated CPU time (s) 9.82 Current children cumulated vsize (Kb) 19796 [startup+20.0053 s] Raw data (loadavg): 0.89 0.94 0.80 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4576 0 0 0 1957 19 0 0 25 0 1 0 1793685388 19632128 4186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 4793 4186 145 145 0 4648 0 [pid=28479] vsize: 19172 Current children cumulated CPU time (s) 19.77 Current children cumulated vsize (Kb) 21296 [startup+30.006 s] Raw data (loadavg): 0.90 0.94 0.80 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4727 0 0 0 2954 20 0 0 25 0 1 0 1793685388 20275200 4337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 4950 4337 145 145 0 4805 0 [pid=28479] vsize: 19800 Current children cumulated CPU time (s) 29.75 Current children cumulated vsize (Kb) 21924 [startup+40.0067 s] Raw data (loadavg): 0.92 0.94 0.80 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 4846 0 0 0 3952 21 0 0 25 0 1 0 1793685388 20750336 4456 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 5066 4456 145 145 0 4921 0 [pid=28479] vsize: 20264 Current children cumulated CPU time (s) 39.74 Current children cumulated vsize (Kb) 22388 [startup+50.0074 s] Raw data (loadavg): 0.93 0.94 0.80 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 5077 0 0 0 4949 23 0 0 25 0 1 0 1793685388 21680128 4687 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 5293 4687 145 145 0 5148 0 [pid=28479] vsize: 21172 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 23296 [startup+60.0071 s] Raw data (loadavg): 0.94 0.95 0.80 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 5461 0 0 0 5943 26 0 0 25 0 1 0 1793685388 23298048 5071 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 5688 5071 145 145 0 5543 0 [pid=28479] vsize: 22752 Current children cumulated CPU time (s) 59.7 Current children cumulated vsize (Kb) 24876 [startup+70.0088 s] Raw data (loadavg): 0.95 0.95 0.81 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 5830 0 0 0 6938 28 0 0 25 0 1 0 1793685388 24797184 5440 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 6054 5440 145 145 0 5909 0 [pid=28479] vsize: 24216 Current children cumulated CPU time (s) 69.67 Current children cumulated vsize (Kb) 26340 [startup+80.0095 s] Raw data (loadavg): 0.96 0.95 0.81 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 6140 0 0 0 7932 30 0 0 25 0 1 0 1793685388 26050560 5750 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 6360 5750 145 145 0 6215 0 [pid=28479] vsize: 25440 Current children cumulated CPU time (s) 79.63 Current children cumulated vsize (Kb) 27564 [startup+90.0092 s] Raw data (loadavg): 0.96 0.95 0.81 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 6610 0 0 0 8924 34 0 0 25 0 1 0 1793685388 27963392 6220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 6827 6220 145 145 0 6682 0 [pid=28479] vsize: 27308 Current children cumulated CPU time (s) 89.59 Current children cumulated vsize (Kb) 29432 [startup+100.01 s] Raw data (loadavg): 0.97 0.95 0.81 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 7286 0 0 0 9914 39 0 0 25 0 1 0 1793685388 30724096 6896 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 7501 6896 145 145 0 7356 0 [pid=28479] vsize: 30004 Current children cumulated CPU time (s) 99.54 Current children cumulated vsize (Kb) 32128 [startup+110.011 s] Raw data (loadavg): 0.97 0.95 0.81 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 7537 0 0 0 10911 40 0 0 25 0 1 0 1793685388 31875072 7147 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 7782 7147 145 145 0 7637 0 [pid=28479] vsize: 31128 Current children cumulated CPU time (s) 109.52 Current children cumulated vsize (Kb) 33252 [startup+120.011 s] Raw data (loadavg): 0.98 0.95 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 8024 0 0 0 11904 43 0 0 25 0 1 0 1793685388 33857536 7634 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 8266 7634 145 145 0 8121 0 [pid=28479] vsize: 33064 Current children cumulated CPU time (s) 119.48 Current children cumulated vsize (Kb) 35188 [startup+130.012 s] Raw data (loadavg): 0.98 0.95 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 8421 0 0 0 12898 45 0 0 25 0 1 0 1793685388 35471360 8031 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 8660 8031 145 145 0 8515 0 [pid=28479] vsize: 34640 Current children cumulated CPU time (s) 129.44 Current children cumulated vsize (Kb) 36764 [startup+140.012 s] Raw data (loadavg): 0.98 0.95 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 8975 0 0 0 13890 48 0 0 25 0 1 0 1793685388 37728256 8585 4294967295 134512640 135094434 3221224432 3221223024 134557287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 9211 8585 145 145 0 9066 0 [pid=28479] vsize: 36844 Current children cumulated CPU time (s) 139.39 Current children cumulated vsize (Kb) 38968 [startup+150.012 s] Raw data (loadavg): 0.98 0.95 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 9562 0 0 0 14879 52 0 0 25 0 1 0 1793685388 40124416 9172 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 9796 9172 145 145 0 9651 0 [pid=28479] vsize: 39184 Current children cumulated CPU time (s) 149.32 Current children cumulated vsize (Kb) 41308 [startup+160.013 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 10102 0 0 0 15870 56 0 0 25 0 1 0 1793685388 42328064 9712 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 10334 9712 145 145 0 10189 0 [pid=28479] vsize: 41336 Current children cumulated CPU time (s) 159.27 Current children cumulated vsize (Kb) 43460 [startup+170.014 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 10607 0 0 0 16861 60 0 0 25 0 1 0 1793685388 44392448 10217 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 10838 10217 145 145 0 10693 0 [pid=28479] vsize: 43352 Current children cumulated CPU time (s) 169.22 Current children cumulated vsize (Kb) 45476 [startup+180.015 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 11085 0 0 0 17851 64 0 0 25 0 1 0 1793685388 46346240 10695 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 11315 10695 145 145 0 11170 0 [pid=28479] vsize: 45260 Current children cumulated CPU time (s) 179.16 Current children cumulated vsize (Kb) 47384 [startup+190.015 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 11545 0 0 0 18844 67 0 0 25 0 1 0 1793685388 48230400 11155 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 11775 11155 145 145 0 11630 0 [pid=28479] vsize: 47100 Current children cumulated CPU time (s) 189.12 Current children cumulated vsize (Kb) 49224 [startup+200.016 s] Raw data (loadavg): 0.99 0.96 0.82 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 11969 0 0 0 19837 70 0 0 25 0 1 0 1793685388 49967104 11579 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 12199 11579 145 145 0 12054 0 [pid=28479] vsize: 48796 Current children cumulated CPU time (s) 199.08 Current children cumulated vsize (Kb) 50920 [startup+210.017 s] Raw data (loadavg): 0.99 0.96 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 12325 0 0 0 20831 73 0 0 25 0 1 0 1793685388 51433472 11935 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 12557 11935 145 145 0 12412 0 [pid=28479] vsize: 50228 Current children cumulated CPU time (s) 209.05 Current children cumulated vsize (Kb) 52352 [startup+220.018 s] Raw data (loadavg): 0.99 0.96 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 12655 0 0 0 21825 75 0 0 25 0 1 0 1793685388 52781056 12265 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 12886 12265 145 145 0 12741 0 [pid=28479] vsize: 51544 Current children cumulated CPU time (s) 219.01 Current children cumulated vsize (Kb) 53668 [startup+230.019 s] Raw data (loadavg): 0.99 0.96 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 12971 0 0 0 22821 78 0 0 25 0 1 0 1793685388 54071296 12581 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 13201 12581 145 145 0 13056 0 [pid=28479] vsize: 52804 Current children cumulated CPU time (s) 229 Current children cumulated vsize (Kb) 54928 [startup+240.019 s] Raw data (loadavg): 0.99 0.96 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 13302 0 0 0 23815 80 0 0 25 0 1 0 1793685388 55418880 12912 4294967295 134512640 135094434 3221224432 3221223024 134557191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 13530 12912 145 145 0 13385 0 [pid=28479] vsize: 54120 Current children cumulated CPU time (s) 238.96 Current children cumulated vsize (Kb) 56244 [startup+250.019 s] Raw data (loadavg): 0.99 0.96 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 13678 0 0 0 24810 82 0 0 25 0 1 0 1793685388 56950784 13288 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 13904 13288 145 145 0 13759 0 [pid=28479] vsize: 55616 Current children cumulated CPU time (s) 248.93 Current children cumulated vsize (Kb) 57740 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 14150 0 0 0 25802 85 0 0 25 0 1 0 1793685388 58888192 13760 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 14377 13760 145 145 0 14232 0 [pid=28479] vsize: 57508 Current children cumulated CPU time (s) 258.88 Current children cumulated vsize (Kb) 59632 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 14574 0 0 0 26793 89 0 0 25 0 1 0 1793685388 60616704 14184 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 14799 14184 145 145 0 14654 0 [pid=28479] vsize: 59196 Current children cumulated CPU time (s) 268.83 Current children cumulated vsize (Kb) 61320 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 15010 0 0 0 27784 92 0 0 25 0 1 0 1793685388 62390272 14620 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 15232 14620 145 145 0 15087 0 [pid=28479] vsize: 60928 Current children cumulated CPU time (s) 278.77 Current children cumulated vsize (Kb) 63052 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 15476 0 0 0 28776 96 0 0 25 0 1 0 1793685388 64290816 15086 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 15696 15086 145 145 0 15551 0 [pid=28479] vsize: 62784 Current children cumulated CPU time (s) 288.73 Current children cumulated vsize (Kb) 64908 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 15933 0 0 0 29768 99 0 0 25 0 1 0 1793685388 66416640 15543 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 16215 15543 145 145 0 16070 0 [pid=28479] vsize: 64860 Current children cumulated CPU time (s) 298.68 Current children cumulated vsize (Kb) 66984 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 16361 0 0 0 30761 102 0 0 25 0 1 0 1793685388 68165632 15971 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 16642 15971 145 145 0 16497 0 [pid=28479] vsize: 66568 Current children cumulated CPU time (s) 308.64 Current children cumulated vsize (Kb) 68692 [startup+320.024 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 16675 0 0 0 31756 105 0 0 25 0 1 0 1793685388 69439488 16285 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 16953 16285 145 145 0 16808 0 [pid=28479] vsize: 67812 Current children cumulated CPU time (s) 318.62 Current children cumulated vsize (Kb) 69936 [startup+330.025 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 17087 0 0 0 32749 107 0 0 25 0 1 0 1793685388 71118848 16697 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 17363 16697 145 145 0 17218 0 [pid=28479] vsize: 69452 Current children cumulated CPU time (s) 328.57 Current children cumulated vsize (Kb) 71576 [startup+340.025 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 17624 0 0 0 33741 111 0 0 25 0 1 0 1793685388 73310208 17234 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 17898 17234 145 145 0 17753 0 [pid=28479] vsize: 71592 Current children cumulated CPU time (s) 338.53 Current children cumulated vsize (Kb) 73716 [startup+350.025 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 18085 0 0 0 34733 114 0 0 25 0 1 0 1793685388 75190272 17695 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 18357 17695 145 145 0 18212 0 [pid=28479] vsize: 73428 Current children cumulated CPU time (s) 348.48 Current children cumulated vsize (Kb) 75552 [startup+360.026 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 18595 0 0 0 35725 118 0 0 25 0 1 0 1793685388 77275136 18205 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 18866 18205 145 145 0 18721 0 [pid=28479] vsize: 75464 Current children cumulated CPU time (s) 358.44 Current children cumulated vsize (Kb) 77588 [startup+370.027 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 19034 0 0 0 36717 120 0 0 25 0 1 0 1793685388 79065088 18644 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 19303 18644 145 145 0 19158 0 [pid=28479] vsize: 77212 Current children cumulated CPU time (s) 368.38 Current children cumulated vsize (Kb) 79336 [startup+380.028 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 19480 0 0 0 37709 124 0 0 25 0 1 0 1793685388 80883712 19090 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 19747 19090 145 145 0 19602 0 [pid=28479] vsize: 78988 Current children cumulated CPU time (s) 378.34 Current children cumulated vsize (Kb) 81112 [startup+390.028 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 19936 0 0 0 38702 127 0 0 25 0 1 0 1793685388 82747392 19546 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 20202 19546 145 145 0 20057 0 [pid=28479] vsize: 80808 Current children cumulated CPU time (s) 388.3 Current children cumulated vsize (Kb) 82932 [startup+400.029 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 20404 0 0 0 39693 131 0 0 25 0 1 0 1793685388 84656128 20014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 20668 20014 145 145 0 20523 0 [pid=28479] vsize: 82672 Current children cumulated CPU time (s) 398.25 Current children cumulated vsize (Kb) 84796 [startup+410.029 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 20780 0 0 0 40686 134 0 0 25 0 1 0 1793685388 86188032 20390 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 21042 20390 145 145 0 20897 0 [pid=28479] vsize: 84168 Current children cumulated CPU time (s) 408.21 Current children cumulated vsize (Kb) 86292 [startup+420.03 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 21145 0 0 0 41679 137 0 0 25 0 1 0 1793685388 87674880 20755 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 21405 20755 145 145 0 21260 0 [pid=28479] vsize: 85620 Current children cumulated CPU time (s) 418.17 Current children cumulated vsize (Kb) 87744 [startup+430.031 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 21564 0 0 0 42673 140 0 0 25 0 1 0 1793685388 89382912 21174 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 21822 21174 145 145 0 21677 0 [pid=28479] vsize: 87288 Current children cumulated CPU time (s) 428.14 Current children cumulated vsize (Kb) 89412 [startup+440.031 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 22058 0 0 0 43663 143 0 0 25 0 1 0 1793685388 91402240 21668 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 22315 21668 145 145 0 22170 0 [pid=28479] vsize: 89260 Current children cumulated CPU time (s) 438.07 Current children cumulated vsize (Kb) 91384 [startup+450.031 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 22600 0 0 0 44654 147 0 0 25 0 1 0 1793685388 93614080 22210 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 22855 22210 145 145 0 22710 0 [pid=28479] vsize: 91420 Current children cumulated CPU time (s) 448.02 Current children cumulated vsize (Kb) 93544 [startup+460.032 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 23127 0 0 0 45647 150 0 0 25 0 1 0 1793685388 95772672 22737 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 23382 22737 145 145 0 23237 0 [pid=28479] vsize: 93528 Current children cumulated CPU time (s) 457.98 Current children cumulated vsize (Kb) 95652 [startup+470.033 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 23624 0 0 0 46641 153 0 0 25 0 1 0 1793685388 97808384 23234 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 23879 23234 145 145 0 23734 0 [pid=28479] vsize: 95516 Current children cumulated CPU time (s) 467.95 Current children cumulated vsize (Kb) 97640 [startup+480.034 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 23979 0 0 0 47635 155 0 0 25 0 1 0 1793685388 99258368 23589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 24233 23589 145 145 0 24088 0 [pid=28479] vsize: 96932 Current children cumulated CPU time (s) 477.91 Current children cumulated vsize (Kb) 99056 [startup+490.034 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 24351 0 0 0 48627 158 0 0 25 0 1 0 1793685388 100773888 23961 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 24603 23961 145 145 0 24458 0 [pid=28479] vsize: 98412 Current children cumulated CPU time (s) 487.86 Current children cumulated vsize (Kb) 100536 [startup+500.035 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 24654 0 0 0 49621 160 0 0 25 0 1 0 1793685388 102006784 24264 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 24904 24264 145 145 0 24759 0 [pid=28479] vsize: 99616 Current children cumulated CPU time (s) 497.82 Current children cumulated vsize (Kb) 101740 [startup+510.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 25090 0 0 0 50614 164 0 0 25 0 1 0 1793685388 103784448 24700 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 25338 24700 145 145 0 25193 0 [pid=28479] vsize: 101352 Current children cumulated CPU time (s) 507.79 Current children cumulated vsize (Kb) 103476 [startup+520.036 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 25581 0 0 0 51608 167 0 0 25 0 1 0 1793685388 105791488 25191 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 25828 25191 145 145 0 25683 0 [pid=28479] vsize: 103312 Current children cumulated CPU time (s) 517.76 Current children cumulated vsize (Kb) 105436 [startup+530.037 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 26042 0 0 0 52601 169 0 0 25 0 1 0 1793685388 107675648 25652 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 26288 25652 145 145 0 26143 0 [pid=28479] vsize: 105152 Current children cumulated CPU time (s) 527.71 Current children cumulated vsize (Kb) 107276 [startup+540.038 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 26469 0 0 0 53594 173 0 0 25 0 1 0 1793685388 109416448 26079 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 26713 26079 145 145 0 26568 0 [pid=28479] vsize: 106852 Current children cumulated CPU time (s) 537.68 Current children cumulated vsize (Kb) 108976 [startup+550.038 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 26914 0 0 0 54586 175 0 0 25 0 1 0 1793685388 111235072 26524 4294967295 134512640 135094434 3221224432 3221223024 134551757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 27157 26524 145 145 0 27012 0 [pid=28479] vsize: 108628 Current children cumulated CPU time (s) 547.62 Current children cumulated vsize (Kb) 110752 [startup+560.038 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 27359 0 0 0 55579 178 0 0 25 0 1 0 1793685388 113053696 26969 4294967295 134512640 135094434 3221224432 3221223104 134556277 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 27601 26969 145 145 0 27456 0 [pid=28479] vsize: 110404 Current children cumulated CPU time (s) 557.58 Current children cumulated vsize (Kb) 112528 [startup+570.04 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 27771 0 0 0 56573 180 0 0 25 0 1 0 1793685388 114737152 27381 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 28012 27381 145 145 0 27867 0 [pid=28479] vsize: 112048 Current children cumulated CPU time (s) 567.54 Current children cumulated vsize (Kb) 114172 [startup+580.041 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 28166 0 0 0 57568 182 0 0 25 0 1 0 1793685388 116350976 27776 4294967295 134512640 135094434 3221224432 3221223024 134557185 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 28406 27776 145 145 0 28261 0 [pid=28479] vsize: 113624 Current children cumulated CPU time (s) 577.51 Current children cumulated vsize (Kb) 115748 [startup+590.04 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) T 28475 28475 6872 0 -1 0 28555 0 0 0 58563 184 0 0 25 0 1 0 1793685388 117940224 28165 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/28479/statm): 28794 28165 145 145 0 28649 0 [pid=28479] vsize: 115176 Current children cumulated CPU time (s) 587.48 Current children cumulated vsize (Kb) 117300 [startup+600.041 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 28899 0 0 0 59559 185 0 0 25 0 1 0 1793685388 119341056 28509 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 29136 28509 145 145 0 28991 0 [pid=28479] vsize: 116544 Current children cumulated CPU time (s) 597.45 Current children cumulated vsize (Kb) 118668 [startup+610.042 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 29410 0 0 0 60552 187 0 0 25 0 1 0 1793685388 121438208 29020 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 29648 29020 145 145 0 29503 0 [pid=28479] vsize: 118592 Current children cumulated CPU time (s) 607.4 Current children cumulated vsize (Kb) 120716 [startup+620.042 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 29922 0 0 0 61546 189 0 0 25 0 1 0 1793685388 123531264 29532 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 30159 29532 145 145 0 30014 0 [pid=28479] vsize: 120636 Current children cumulated CPU time (s) 617.36 Current children cumulated vsize (Kb) 122760 [startup+630.043 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 30616 0 0 0 62534 195 0 0 25 0 1 0 1793685388 126361600 30226 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 30850 30226 145 145 0 30705 0 [pid=28479] vsize: 123400 Current children cumulated CPU time (s) 627.3 Current children cumulated vsize (Kb) 125524 [startup+640.044 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 31234 0 0 0 63524 199 0 0 25 0 1 0 1793685388 128888832 30844 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 31467 30844 145 145 0 31322 0 [pid=28479] vsize: 125868 Current children cumulated CPU time (s) 637.24 Current children cumulated vsize (Kb) 127992 [startup+650.044 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 31622 0 0 0 64518 201 0 0 25 0 1 0 1793685388 130469888 31232 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 31853 31232 145 145 0 31708 0 [pid=28479] vsize: 127412 Current children cumulated CPU time (s) 647.2 Current children cumulated vsize (Kb) 129536 [startup+660.045 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 32181 0 0 0 65510 204 0 0 25 0 1 0 1793685388 132751360 31791 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 32410 31791 145 145 0 32265 0 [pid=28479] vsize: 129640 Current children cumulated CPU time (s) 657.15 Current children cumulated vsize (Kb) 131764 [startup+670.046 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 32691 0 0 0 66500 208 0 0 25 0 1 0 1793685388 134836224 32301 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 32919 32301 145 145 0 32774 0 [pid=28479] vsize: 131676 Current children cumulated CPU time (s) 667.09 Current children cumulated vsize (Kb) 133800 [startup+680.047 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33028 0 0 0 67495 210 0 0 25 0 1 0 1793685388 136212480 32638 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 33255 32638 145 145 0 33110 0 [pid=28479] vsize: 133020 Current children cumulated CPU time (s) 677.06 Current children cumulated vsize (Kb) 135144 [startup+690.047 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33334 0 0 0 68490 212 0 0 25 0 1 0 1793685388 137461760 32944 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 33560 32944 145 145 0 33415 0 [pid=28479] vsize: 134240 Current children cumulated CPU time (s) 687.03 Current children cumulated vsize (Kb) 136364 [startup+700.049 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33528 0 0 0 69486 214 0 0 25 0 1 0 1793685388 138772480 33138 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 33880 33138 145 145 0 33735 0 [pid=28479] vsize: 135520 Current children cumulated CPU time (s) 697.01 Current children cumulated vsize (Kb) 137644 [startup+710.05 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 33821 0 0 0 70481 216 0 0 25 0 1 0 1793685388 139968512 33431 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 34172 33431 145 145 0 34027 0 [pid=28479] vsize: 136688 Current children cumulated CPU time (s) 706.98 Current children cumulated vsize (Kb) 138812 [startup+720.05 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 34368 0 0 0 71473 219 0 0 25 0 1 0 1793685388 142200832 33978 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 34717 33978 145 145 0 34572 0 [pid=28479] vsize: 138868 Current children cumulated CPU time (s) 716.93 Current children cumulated vsize (Kb) 140992 [startup+730.051 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 34975 0 0 0 72463 222 0 0 25 0 1 0 1793685388 144683008 34585 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 35323 34585 145 145 0 35178 0 [pid=28479] vsize: 141292 Current children cumulated CPU time (s) 726.86 Current children cumulated vsize (Kb) 143416 [startup+740.052 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 35509 0 0 0 73455 225 0 0 25 0 1 0 1793685388 146866176 35119 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 35856 35119 145 145 0 35711 0 [pid=28479] vsize: 143424 Current children cumulated CPU time (s) 736.81 Current children cumulated vsize (Kb) 145548 [startup+750.053 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 35983 0 0 0 74449 228 0 0 25 0 1 0 1793685388 148803584 35593 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 36329 35593 145 145 0 36184 0 [pid=28479] vsize: 145316 Current children cumulated CPU time (s) 746.78 Current children cumulated vsize (Kb) 147440 [startup+760.053 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 36464 0 0 0 75443 231 0 0 25 0 1 0 1793685388 150769664 36074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 36809 36074 145 145 0 36664 0 [pid=28479] vsize: 147236 Current children cumulated CPU time (s) 756.75 Current children cumulated vsize (Kb) 149360 [startup+770.054 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 36923 0 0 0 76434 235 0 0 25 0 1 0 1793685388 152645632 36533 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 37267 36533 145 145 0 37122 0 [pid=28479] vsize: 149068 Current children cumulated CPU time (s) 766.7 Current children cumulated vsize (Kb) 151192 [startup+780.055 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 37324 0 0 0 77428 237 0 0 25 0 1 0 1793685388 154284032 36934 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 37667 36934 145 145 0 37522 0 [pid=28479] vsize: 150668 Current children cumulated CPU time (s) 776.66 Current children cumulated vsize (Kb) 152792 [startup+790.055 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 37666 0 0 0 78421 241 0 0 25 0 1 0 1793685388 155680768 37276 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 38008 37276 145 145 0 37863 0 [pid=28479] vsize: 152032 Current children cumulated CPU time (s) 786.63 Current children cumulated vsize (Kb) 154156 [startup+800.056 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38074 0 0 0 79416 243 0 0 25 0 1 0 1793685388 157351936 37684 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 38416 37684 145 145 0 38271 0 [pid=28479] vsize: 153664 Current children cumulated CPU time (s) 796.6 Current children cumulated vsize (Kb) 155788 [startup+810.058 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38485 0 0 0 80411 245 0 0 25 0 1 0 1793685388 159031296 38095 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 38826 38095 145 145 0 38681 0 [pid=28479] vsize: 155304 Current children cumulated CPU time (s) 806.57 Current children cumulated vsize (Kb) 157428 [startup+820.058 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38754 0 0 0 81407 248 0 0 25 0 1 0 1793685388 160129024 38364 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39094 38364 145 145 0 38949 0 [pid=28479] vsize: 156376 Current children cumulated CPU time (s) 816.56 Current children cumulated vsize (Kb) 158500 [startup+830.059 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 82407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 826.56 Current children cumulated vsize (Kb) 158916 [startup+840.06 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 83407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 836.56 Current children cumulated vsize (Kb) 158916 [startup+850.061 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 84407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 846.56 Current children cumulated vsize (Kb) 158916 [startup+860.06 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 85407 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 856.56 Current children cumulated vsize (Kb) 158916 [startup+870.062 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 86408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 866.57 Current children cumulated vsize (Kb) 158916 [startup+880.063 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 87408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 876.57 Current children cumulated vsize (Kb) 158916 [startup+890.062 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 88408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 886.57 Current children cumulated vsize (Kb) 158916 [startup+900.064 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 89408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 896.57 Current children cumulated vsize (Kb) 158916 [startup+910.065 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 90408 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 906.57 Current children cumulated vsize (Kb) 158916 [startup+920.065 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 91409 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 916.58 Current children cumulated vsize (Kb) 158916 [startup+930.067 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 92409 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 926.58 Current children cumulated vsize (Kb) 158916 [startup+940.068 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 93409 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 936.58 Current children cumulated vsize (Kb) 158916 [startup+950.068 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 94410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 946.59 Current children cumulated vsize (Kb) 158916 [startup+960.069 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 95410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 956.59 Current children cumulated vsize (Kb) 158916 [startup+970.07 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 96410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 966.59 Current children cumulated vsize (Kb) 158916 [startup+980.071 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 97410 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 976.59 Current children cumulated vsize (Kb) 158916 [startup+990.071 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 98411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 986.6 Current children cumulated vsize (Kb) 158916 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 99411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 996.6 Current children cumulated vsize (Kb) 158916 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 100411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1006.6 Current children cumulated vsize (Kb) 158916 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 101411 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1016.6 Current children cumulated vsize (Kb) 158916 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 102412 248 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1026.61 Current children cumulated vsize (Kb) 158916 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 103412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1036.62 Current children cumulated vsize (Kb) 158916 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 104411 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134556244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1046.61 Current children cumulated vsize (Kb) 158916 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 105411 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1056.61 Current children cumulated vsize (Kb) 158916 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 106412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1066.62 Current children cumulated vsize (Kb) 158916 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 107412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1076.62 Current children cumulated vsize (Kb) 158916 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 108412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1086.62 Current children cumulated vsize (Kb) 158916 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 109412 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1096.62 Current children cumulated vsize (Kb) 158916 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 110413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1106.63 Current children cumulated vsize (Kb) 158916 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 111413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1116.63 Current children cumulated vsize (Kb) 158916 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 112413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1126.63 Current children cumulated vsize (Kb) 158916 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 113413 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1136.63 Current children cumulated vsize (Kb) 158916 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 114414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1146.64 Current children cumulated vsize (Kb) 158916 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 115414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1156.64 Current children cumulated vsize (Kb) 158916 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 116414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1166.64 Current children cumulated vsize (Kb) 158916 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 117414 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1176.64 Current children cumulated vsize (Kb) 158916 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 118415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1186.65 Current children cumulated vsize (Kb) 158916 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 119415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1196.65 Current children cumulated vsize (Kb) 158916 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 120415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1206.65 Current children cumulated vsize (Kb) 158916 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28479 Raw data (/proc/28475/stat): 28475 (minisat+_script) S 28474 28475 6872 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793685383 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28475/statm): 531 226 485 147 0 384 0 [pid=28475] vsize: 2124 Raw data (/proc/28479/stat): 28479 (minisat+_64-bit) R 28475 28475 6872 0 -1 0 38859 0 0 0 120415 249 0 0 25 0 1 0 1793685388 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28479/statm): 39198 38469 145 145 0 39053 0 [pid=28479] vsize: 156792 Current children cumulated CPU time (s) 1206.65 Current children cumulated vsize (Kb) 158916 Sending SIGTERM to -28475 Sleeping 2 seconds One traced child (pid=28475) ended because it received signal 15 (SIGTERM) One traced child (pid=28479) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1206.72 CPU user time (s): 1204.16 CPU system time (s): 2.56661 CPU usage (%): 99.7156 Max. virtual memory (cumulated for all children) (Kb): 158916
ERROR: no interpretation found !