Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-l152lav.opb |
MD5SUM | 00855a9538cee8df79108d56ee6867b4 |
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.32 |
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 wulflinc28 THE 2005-09-20 03:11:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3243 boxname=wulflinc28 idbench=899 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 00855a9538cee8df79108d56ee6867b4 /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-l152lav.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-l152lav.opb IDLAUNCH: 3243 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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: 891972 kB Buffers: 23012 kB Cached: 90500 kB SwapCached: 660 kB Active: 28264 kB Inactive: 87772 kB HighTotal: 131008 kB HighFree: 36904 kB LowTotal: 903652 kB LowFree: 855068 kB SwapTotal: 2097640 kB SwapFree: 2096408 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5816 kB Slab: 20944 kB Committed_AS: 64128 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:31:25 (client local time) WITH STATUS 0 IN 1206.8 SECONDS stats: 3243 7 1206.8 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/20773/stat): 20773 (minisat+_script) R 20772 20773 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855205456 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/20773/statm): 174 3 169 147 0 27 0 [pid=20773] 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=20774 New process pid=20775 New process pid=20776 execve syscall for /bin/sed executable One traced child (pid=20775) 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=20776) exited with status: 0 One traced child (pid=20774) exited with status: 0 New process pid=20777 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-l152lav.opb [startup+10.0039 s] Raw data (loadavg): 0.82 0.91 0.72 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4205 0 0 0 963 17 0 0 25 0 1 0 1855205461 18108416 3815 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 4421 3815 145 145 0 4276 0 [pid=20777] vsize: 17684 Current children cumulated CPU time (s) 9.81 Current children cumulated vsize (Kb) 19808 [startup+20.0046 s] Raw data (loadavg): 0.84 0.91 0.73 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4576 0 0 0 1957 19 0 0 25 0 1 0 1855205461 19632128 4186 4294967295 134512640 135094434 3221224432 3221223088 134561717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 4793 4186 145 145 0 4648 0 [pid=20777] vsize: 19172 Current children cumulated CPU time (s) 19.77 Current children cumulated vsize (Kb) 21296 [startup+30.0053 s] Raw data (loadavg): 0.87 0.92 0.73 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4727 0 0 0 2955 20 0 0 25 0 1 0 1855205461 20275200 4337 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 4950 4337 145 145 0 4805 0 [pid=20777] vsize: 19800 Current children cumulated CPU time (s) 29.76 Current children cumulated vsize (Kb) 21924 [startup+40.0069 s] Raw data (loadavg): 0.89 0.92 0.73 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 4846 0 0 0 3952 22 0 0 25 0 1 0 1855205461 20750336 4456 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 5066 4456 145 145 0 4921 0 [pid=20777] vsize: 20264 Current children cumulated CPU time (s) 39.75 Current children cumulated vsize (Kb) 22388 [startup+50.0076 s] Raw data (loadavg): 0.90 0.92 0.73 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 5072 0 0 0 4948 24 0 0 25 0 1 0 1855205461 21659648 4682 4294967295 134512640 135094434 3221224432 3221222976 134779242 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 5288 4682 145 145 0 5143 0 [pid=20777] vsize: 21152 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 23276 [startup+60.0083 s] Raw data (loadavg): 0.92 0.92 0.74 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 5447 0 0 0 5941 27 0 0 25 0 1 0 1855205461 23240704 5057 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 5674 5057 145 145 0 5529 0 [pid=20777] vsize: 22696 Current children cumulated CPU time (s) 59.69 Current children cumulated vsize (Kb) 24820 [startup+70.0089 s] Raw data (loadavg): 0.93 0.92 0.74 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 5824 0 0 0 6934 31 0 0 25 0 1 0 1855205461 24772608 5434 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 6048 5434 145 145 0 5903 0 [pid=20777] vsize: 24192 Current children cumulated CPU time (s) 69.66 Current children cumulated vsize (Kb) 26316 [startup+80.0096 s] Raw data (loadavg): 0.94 0.93 0.74 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 6132 0 0 0 7929 33 0 0 25 0 1 0 1855205461 26017792 5742 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 6352 5742 145 145 0 6207 0 [pid=20777] vsize: 25408 Current children cumulated CPU time (s) 79.63 Current children cumulated vsize (Kb) 27532 [startup+90.0103 s] Raw data (loadavg): 0.95 0.93 0.74 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 6571 0 0 0 8922 36 0 0 25 0 1 0 1855205461 27803648 6181 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 6788 6181 145 145 0 6643 0 [pid=20777] vsize: 27152 Current children cumulated CPU time (s) 89.59 Current children cumulated vsize (Kb) 29276 [startup+100.011 s] Raw data (loadavg): 0.96 0.93 0.74 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 7239 0 0 0 9912 40 0 0 25 0 1 0 1855205461 30535680 6849 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 7455 6849 145 145 0 7310 0 [pid=20777] vsize: 29820 Current children cumulated CPU time (s) 99.53 Current children cumulated vsize (Kb) 31944 [startup+110.012 s] Raw data (loadavg): 0.96 0.93 0.75 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 7499 0 0 0 10908 42 0 0 25 0 1 0 1855205461 31719424 7109 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 7744 7109 145 145 0 7599 0 [pid=20777] vsize: 30976 Current children cumulated CPU time (s) 109.51 Current children cumulated vsize (Kb) 33100 [startup+120.012 s] Raw data (loadavg): 0.97 0.93 0.75 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 7978 0 0 0 11899 47 0 0 25 0 1 0 1855205461 33669120 7588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 8220 7588 145 145 0 8075 0 [pid=20777] vsize: 32880 Current children cumulated CPU time (s) 119.47 Current children cumulated vsize (Kb) 35004 [startup+130.013 s] Raw data (loadavg): 0.97 0.94 0.75 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 8358 0 0 0 12893 49 0 0 25 0 1 0 1855205461 35213312 7968 4294967295 134512640 135094434 3221224432 3221223024 134556996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 8597 7968 145 145 0 8452 0 [pid=20777] vsize: 34388 Current children cumulated CPU time (s) 129.43 Current children cumulated vsize (Kb) 36512 [startup+140.014 s] Raw data (loadavg): 0.98 0.94 0.75 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 8913 0 0 0 13883 52 0 0 25 0 1 0 1855205461 37478400 8523 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 9150 8523 145 145 0 9005 0 [pid=20777] vsize: 36600 Current children cumulated CPU time (s) 139.36 Current children cumulated vsize (Kb) 38724 [startup+150.014 s] Raw data (loadavg): 0.98 0.94 0.75 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 9483 0 0 0 14874 56 0 0 25 0 1 0 1855205461 39800832 9093 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 9717 9093 145 145 0 9572 0 [pid=20777] vsize: 38868 Current children cumulated CPU time (s) 149.31 Current children cumulated vsize (Kb) 40992 [startup+160.015 s] Raw data (loadavg): 0.98 0.94 0.76 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 10031 0 0 0 15863 60 0 0 25 0 1 0 1855205461 42041344 9641 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 10264 9641 145 145 0 10119 0 [pid=20777] vsize: 41056 Current children cumulated CPU time (s) 159.24 Current children cumulated vsize (Kb) 43180 [startup+170.016 s] Raw data (loadavg): 0.98 0.94 0.76 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 10532 0 0 0 16856 63 0 0 25 0 1 0 1855205461 44085248 10142 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 10763 10142 145 145 0 10618 0 [pid=20777] vsize: 43052 Current children cumulated CPU time (s) 169.2 Current children cumulated vsize (Kb) 45176 [startup+180.015 s] Raw data (loadavg): 0.99 0.94 0.76 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 11020 0 0 0 17849 65 0 0 25 0 1 0 1855205461 46080000 10630 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 11250 10630 145 145 0 11105 0 [pid=20777] vsize: 45000 Current children cumulated CPU time (s) 179.15 Current children cumulated vsize (Kb) 47124 [startup+190.016 s] Raw data (loadavg): 0.99 0.94 0.76 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 11483 0 0 0 18842 68 0 0 25 0 1 0 1855205461 47972352 11093 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 11712 11093 145 145 0 11567 0 [pid=20777] vsize: 46848 Current children cumulated CPU time (s) 189.11 Current children cumulated vsize (Kb) 48972 [startup+200.017 s] Raw data (loadavg): 0.99 0.95 0.76 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 11901 0 0 0 19836 71 0 0 25 0 1 0 1855205461 49684480 11511 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 12130 11511 145 145 0 11985 0 [pid=20777] vsize: 48520 Current children cumulated CPU time (s) 199.08 Current children cumulated vsize (Kb) 50644 [startup+210.017 s] Raw data (loadavg): 0.99 0.95 0.77 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 12278 0 0 0 20831 73 0 0 25 0 1 0 1855205461 51240960 11888 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 12510 11888 145 145 0 12365 0 [pid=20777] vsize: 50040 Current children cumulated CPU time (s) 209.05 Current children cumulated vsize (Kb) 52164 [startup+220.018 s] Raw data (loadavg): 0.99 0.95 0.77 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 12592 0 0 0 21825 75 0 0 25 0 1 0 1855205461 52523008 12202 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 12823 12202 145 145 0 12678 0 [pid=20777] vsize: 51292 Current children cumulated CPU time (s) 219.01 Current children cumulated vsize (Kb) 53416 [startup+230.018 s] Raw data (loadavg): 0.99 0.95 0.77 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 12903 0 0 0 22822 76 0 0 25 0 1 0 1855205461 53792768 12513 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 13133 12513 145 145 0 12988 0 [pid=20777] vsize: 52532 Current children cumulated CPU time (s) 228.99 Current children cumulated vsize (Kb) 54656 [startup+240.018 s] Raw data (loadavg): 0.99 0.95 0.77 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 13208 0 0 0 23818 78 0 0 25 0 1 0 1855205461 55037952 12818 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 13437 12818 145 145 0 13292 0 [pid=20777] vsize: 53748 Current children cumulated CPU time (s) 238.97 Current children cumulated vsize (Kb) 55872 [startup+250.019 s] Raw data (loadavg): 0.99 0.95 0.77 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 13597 0 0 0 24812 81 0 0 25 0 1 0 1855205461 56619008 13207 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 13823 13207 145 145 0 13678 0 [pid=20777] vsize: 55292 Current children cumulated CPU time (s) 248.94 Current children cumulated vsize (Kb) 57416 [startup+260.02 s] Raw data (loadavg): 1.06 0.97 0.78 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 14042 0 0 0 25805 84 0 0 25 0 1 0 1855205461 58445824 13652 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 14269 13652 145 145 0 14124 0 [pid=20777] vsize: 57076 Current children cumulated CPU time (s) 258.9 Current children cumulated vsize (Kb) 59200 [startup+270.02 s] Raw data (loadavg): 1.05 0.97 0.78 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 14475 0 0 0 26798 87 0 0 25 0 1 0 1855205461 60211200 14085 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 14700 14085 145 145 0 14555 0 [pid=20777] vsize: 58800 Current children cumulated CPU time (s) 268.86 Current children cumulated vsize (Kb) 60924 [startup+280.021 s] Raw data (loadavg): 1.04 0.97 0.79 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 14939 0 0 0 27791 90 0 0 25 0 1 0 1855205461 62103552 14549 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 15162 14549 145 145 0 15017 0 [pid=20777] vsize: 60648 Current children cumulated CPU time (s) 278.82 Current children cumulated vsize (Kb) 62772 [startup+290.022 s] Raw data (loadavg): 1.04 0.97 0.79 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 15338 0 0 0 28785 92 0 0 25 0 1 0 1855205461 63725568 14948 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 15558 14948 145 145 0 15413 0 [pid=20777] vsize: 62232 Current children cumulated CPU time (s) 288.78 Current children cumulated vsize (Kb) 64356 [startup+300.022 s] Raw data (loadavg): 1.03 0.97 0.79 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 15807 0 0 0 29777 95 0 0 25 0 1 0 1855205461 65642496 15417 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 16026 15417 145 145 0 15881 0 [pid=20777] vsize: 64104 Current children cumulated CPU time (s) 298.73 Current children cumulated vsize (Kb) 66228 [startup+310.024 s] Raw data (loadavg): 1.03 0.97 0.79 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 16256 0 0 0 30770 98 0 0 25 0 1 0 1855205461 67735552 15866 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 16537 15866 145 145 0 16392 0 [pid=20777] vsize: 66148 Current children cumulated CPU time (s) 308.69 Current children cumulated vsize (Kb) 68272 [startup+320.025 s] Raw data (loadavg): 1.02 0.97 0.79 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 16585 0 0 0 31764 100 0 0 25 0 1 0 1855205461 69074944 16195 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 16864 16195 145 145 0 16719 0 [pid=20777] vsize: 67456 Current children cumulated CPU time (s) 318.65 Current children cumulated vsize (Kb) 69580 [startup+330.026 s] Raw data (loadavg): 1.02 0.97 0.79 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) T 20773 20773 20115 0 -1 0 16943 0 0 0 32757 104 0 0 25 0 1 0 1855205461 70533120 16553 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/20777/statm): 17220 16553 145 145 0 17075 0 [pid=20777] vsize: 68880 Current children cumulated CPU time (s) 328.62 Current children cumulated vsize (Kb) 71004 [startup+340.026 s] Raw data (loadavg): 1.01 0.97 0.80 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 17458 0 0 0 33749 108 0 0 25 0 1 0 1855205461 72634368 17068 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 17733 17068 145 145 0 17588 0 [pid=20777] vsize: 70932 Current children cumulated CPU time (s) 338.58 Current children cumulated vsize (Kb) 73056 [startup+350.027 s] Raw data (loadavg): 1.01 0.97 0.80 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 17917 0 0 0 34742 112 0 0 25 0 1 0 1855205461 74506240 17527 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 18190 17527 145 145 0 18045 0 [pid=20777] vsize: 72760 Current children cumulated CPU time (s) 348.55 Current children cumulated vsize (Kb) 74884 [startup+360.028 s] Raw data (loadavg): 1.01 0.97 0.80 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 18426 0 0 0 35734 114 0 0 25 0 1 0 1855205461 76587008 18036 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 18698 18036 145 145 0 18553 0 [pid=20777] vsize: 74792 Current children cumulated CPU time (s) 358.49 Current children cumulated vsize (Kb) 76916 [startup+370.028 s] Raw data (loadavg): 1.01 0.97 0.80 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 18852 0 0 0 36728 117 0 0 25 0 1 0 1855205461 78323712 18462 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 19122 18462 145 145 0 18977 0 [pid=20777] vsize: 76488 Current children cumulated CPU time (s) 368.46 Current children cumulated vsize (Kb) 78612 [startup+380.028 s] Raw data (loadavg): 1.01 0.97 0.80 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 19325 0 0 0 37721 120 0 0 25 0 1 0 1855205461 80252928 18935 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 19593 18935 145 145 0 19448 0 [pid=20777] vsize: 78372 Current children cumulated CPU time (s) 378.42 Current children cumulated vsize (Kb) 80496 [startup+390.029 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 19768 0 0 0 38713 123 0 0 25 0 1 0 1855205461 82059264 19378 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 20034 19378 145 145 0 19889 0 [pid=20777] vsize: 80136 Current children cumulated CPU time (s) 388.37 Current children cumulated vsize (Kb) 82260 [startup+400.029 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 20213 0 0 0 39705 125 0 0 25 0 1 0 1855205461 83877888 19823 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 20478 19823 145 145 0 20333 0 [pid=20777] vsize: 81912 Current children cumulated CPU time (s) 398.31 Current children cumulated vsize (Kb) 84036 [startup+410.03 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 20649 0 0 0 40698 128 0 0 25 0 1 0 1855205461 85655552 20259 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 20912 20259 145 145 0 20767 0 [pid=20777] vsize: 83648 Current children cumulated CPU time (s) 408.27 Current children cumulated vsize (Kb) 85772 [startup+420.031 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 21015 0 0 0 41692 131 0 0 25 0 1 0 1855205461 87146496 20625 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 21276 20625 145 145 0 21131 0 [pid=20777] vsize: 85104 Current children cumulated CPU time (s) 418.24 Current children cumulated vsize (Kb) 87228 [startup+430.031 s] Raw data (loadavg): 1.00 0.97 0.81 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 21394 0 0 0 42683 134 0 0 25 0 1 0 1855205461 88690688 21004 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 21653 21004 145 145 0 21508 0 [pid=20777] vsize: 86612 Current children cumulated CPU time (s) 428.18 Current children cumulated vsize (Kb) 88736 [startup+440.032 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 21856 0 0 0 43674 139 0 0 25 0 1 0 1855205461 90574848 21466 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 22113 21466 145 145 0 21968 0 [pid=20777] vsize: 88452 Current children cumulated CPU time (s) 438.14 Current children cumulated vsize (Kb) 90576 [startup+450.033 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 22372 0 0 0 44667 141 0 0 25 0 1 0 1855205461 92684288 21982 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 22628 21982 145 145 0 22483 0 [pid=20777] vsize: 90512 Current children cumulated CPU time (s) 448.09 Current children cumulated vsize (Kb) 92636 [startup+460.033 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 22901 0 0 0 45660 144 0 0 25 0 1 0 1855205461 94851072 22511 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 23157 22511 145 145 0 23012 0 [pid=20777] vsize: 92628 Current children cumulated CPU time (s) 458.05 Current children cumulated vsize (Kb) 94752 [startup+470.034 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 23415 0 0 0 46652 148 0 0 25 0 1 0 1855205461 96956416 23025 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 23671 23025 145 145 0 23526 0 [pid=20777] vsize: 94684 Current children cumulated CPU time (s) 468.01 Current children cumulated vsize (Kb) 96808 [startup+480.034 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 23824 0 0 0 47646 150 0 0 25 0 1 0 1855205461 98623488 23434 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 24078 23434 145 145 0 23933 0 [pid=20777] vsize: 96312 Current children cumulated CPU time (s) 477.97 Current children cumulated vsize (Kb) 98436 [startup+490.034 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 24200 0 0 0 48641 153 0 0 25 0 1 0 1855205461 100159488 23810 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 24453 23810 145 145 0 24308 0 [pid=20777] vsize: 97812 Current children cumulated CPU time (s) 487.95 Current children cumulated vsize (Kb) 99936 [startup+500.035 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 24469 0 0 0 49636 156 0 0 23 0 1 0 1855205461 101253120 24079 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 24720 24079 145 145 0 24575 0 [pid=20777] vsize: 98880 Current children cumulated CPU time (s) 497.93 Current children cumulated vsize (Kb) 101004 [startup+510.037 s] Raw data (loadavg): 1.00 0.97 0.82 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 24870 0 0 0 50629 158 0 0 25 0 1 0 1855205461 102887424 24480 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 25119 24480 145 145 0 24974 0 [pid=20777] vsize: 100476 Current children cumulated CPU time (s) 507.88 Current children cumulated vsize (Kb) 102600 [startup+520.037 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 25325 0 0 0 51622 162 0 0 25 0 1 0 1855205461 104747008 24935 4294967295 134512640 135094434 3221224432 3221223024 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 25573 24935 145 145 0 25428 0 [pid=20777] vsize: 102292 Current children cumulated CPU time (s) 517.85 Current children cumulated vsize (Kb) 104416 [startup+530.038 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 25828 0 0 0 52614 165 0 0 25 0 1 0 1855205461 106803200 25438 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 26075 25438 145 145 0 25930 0 [pid=20777] vsize: 104300 Current children cumulated CPU time (s) 527.8 Current children cumulated vsize (Kb) 106424 [startup+540.039 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 26241 0 0 0 53606 168 0 0 25 0 1 0 1855205461 108486656 25851 4294967295 134512640 135094434 3221224432 3221222912 134780857 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 26486 25851 145 145 0 26341 0 [pid=20777] vsize: 105944 Current children cumulated CPU time (s) 537.75 Current children cumulated vsize (Kb) 108068 [startup+550.039 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 26664 0 0 0 54600 171 0 0 25 0 1 0 1855205461 110215168 26274 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 26908 26274 145 145 0 26763 0 [pid=20777] vsize: 107632 Current children cumulated CPU time (s) 547.72 Current children cumulated vsize (Kb) 109756 [startup+560.041 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 27132 0 0 0 55593 173 0 0 25 0 1 0 1855205461 112128000 26742 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 27375 26742 145 145 0 27230 0 [pid=20777] vsize: 109500 Current children cumulated CPU time (s) 557.67 Current children cumulated vsize (Kb) 111624 [startup+570.043 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 27549 0 0 0 56586 176 0 0 25 0 1 0 1855205461 113831936 27159 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 27791 27159 145 145 0 27646 0 [pid=20777] vsize: 111164 Current children cumulated CPU time (s) 567.63 Current children cumulated vsize (Kb) 113288 [startup+580.043 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 27962 0 0 0 57579 179 0 0 25 0 1 0 1855205461 115515392 27572 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 28202 27572 145 145 0 28057 0 [pid=20777] vsize: 112808 Current children cumulated CPU time (s) 577.59 Current children cumulated vsize (Kb) 114932 [startup+590.045 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 28341 0 0 0 58574 182 0 0 25 0 1 0 1855205461 117063680 27951 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 28580 27951 145 145 0 28435 0 [pid=20777] vsize: 114320 Current children cumulated CPU time (s) 587.57 Current children cumulated vsize (Kb) 116444 [startup+600.046 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 28701 0 0 0 59568 184 0 0 25 0 1 0 1855205461 118534144 28311 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 28939 28311 145 145 0 28794 0 [pid=20777] vsize: 115756 Current children cumulated CPU time (s) 597.53 Current children cumulated vsize (Kb) 117880 [startup+610.047 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 29120 0 0 0 60560 188 0 0 25 0 1 0 1855205461 120254464 28730 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 29359 28730 145 145 0 29214 0 [pid=20777] vsize: 117436 Current children cumulated CPU time (s) 607.49 Current children cumulated vsize (Kb) 119560 [startup+620.048 s] Raw data (loadavg): 1.00 0.97 0.83 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 29643 0 0 0 61550 192 0 0 25 0 1 0 1855205461 122392576 29253 4294967295 134512640 135094434 3221224432 3221223104 134555769 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 29881 29253 145 145 0 29736 0 [pid=20777] vsize: 119524 Current children cumulated CPU time (s) 617.43 Current children cumulated vsize (Kb) 121648 [startup+630.049 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 30204 0 0 0 62540 196 0 0 25 0 1 0 1855205461 124682240 29814 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 30440 29814 145 145 0 30295 0 [pid=20777] vsize: 121760 Current children cumulated CPU time (s) 627.37 Current children cumulated vsize (Kb) 123884 [startup+640.05 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 30924 0 0 0 63529 201 0 0 25 0 1 0 1855205461 127623168 30534 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 31158 30534 145 145 0 31013 0 [pid=20777] vsize: 124632 Current children cumulated CPU time (s) 637.31 Current children cumulated vsize (Kb) 126756 [startup+650.051 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 31314 0 0 0 64523 203 0 0 25 0 1 0 1855205461 129212416 30924 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 31546 30924 145 145 0 31401 0 [pid=20777] vsize: 126184 Current children cumulated CPU time (s) 647.27 Current children cumulated vsize (Kb) 128308 [startup+660.052 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 31855 0 0 0 65515 206 0 0 25 0 1 0 1855205461 131424256 31465 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 32086 31465 145 145 0 31941 0 [pid=20777] vsize: 128344 Current children cumulated CPU time (s) 657.22 Current children cumulated vsize (Kb) 130468 [startup+670.053 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 32371 0 0 0 66509 209 0 0 25 0 1 0 1855205461 133529600 31981 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 32600 31981 145 145 0 32455 0 [pid=20777] vsize: 130400 Current children cumulated CPU time (s) 667.19 Current children cumulated vsize (Kb) 132524 [startup+680.053 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 32840 0 0 0 67503 211 0 0 25 0 1 0 1855205461 135446528 32450 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 33068 32450 145 145 0 32923 0 [pid=20777] vsize: 132272 Current children cumulated CPU time (s) 677.15 Current children cumulated vsize (Kb) 134396 [startup+690.054 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 33137 0 0 0 68498 214 0 0 25 0 1 0 1855205461 136654848 32747 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 33363 32747 145 145 0 33218 0 [pid=20777] vsize: 133452 Current children cumulated CPU time (s) 687.13 Current children cumulated vsize (Kb) 135576 [startup+700.055 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 33436 0 0 0 69492 217 0 0 25 0 1 0 1855205461 138399744 33046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20777/statm): 33789 33046 145 145 0 33644 0 [pid=20777] vsize: 135156 Current children cumulated CPU time (s) 697.1 Current children cumulated vsize (Kb) 137280 [startup+710.056 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 33583 0 0 0 70488 218 0 0 25 0 1 0 1855205461 138997760 33193 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 33935 33193 145 145 0 33790 0 [pid=20777] vsize: 135740 Current children cumulated CPU time (s) 707.07 Current children cumulated vsize (Kb) 137864 [startup+720.057 s] Raw data (loadavg): 1.00 0.97 0.84 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 34004 0 0 0 71481 222 0 0 25 0 1 0 1855205461 140713984 33614 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 34354 33614 145 145 0 34209 0 [pid=20777] vsize: 137416 Current children cumulated CPU time (s) 717.04 Current children cumulated vsize (Kb) 139540 [startup+730.058 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 34588 0 0 0 72472 226 0 0 25 0 1 0 1855205461 143101952 34198 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 34937 34198 145 145 0 34792 0 [pid=20777] vsize: 139748 Current children cumulated CPU time (s) 726.99 Current children cumulated vsize (Kb) 141872 [startup+740.058 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 35150 0 0 0 73463 230 0 0 25 0 1 0 1855205461 145399808 34760 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 35498 34760 145 145 0 35353 0 [pid=20777] vsize: 141992 Current children cumulated CPU time (s) 736.94 Current children cumulated vsize (Kb) 144116 [startup+750.06 s] Raw data (loadavg): 1.00 0.97 0.85 1/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) T 20773 20773 20115 0 -1 0 35669 0 0 0 74455 234 0 0 25 0 1 0 1855205461 147521536 35279 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/20777/statm): 36016 35279 145 145 0 35871 0 [pid=20777] vsize: 144064 Current children cumulated CPU time (s) 746.9 Current children cumulated vsize (Kb) 146188 [startup+760.061 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 36115 0 0 0 75448 237 0 0 25 0 1 0 1855205461 149344256 35725 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 36461 35725 145 145 0 36316 0 [pid=20777] vsize: 145844 Current children cumulated CPU time (s) 756.86 Current children cumulated vsize (Kb) 147968 [startup+770.061 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 36587 0 0 0 76443 239 0 0 25 0 1 0 1855205461 151273472 36197 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 36932 36197 145 145 0 36787 0 [pid=20777] vsize: 147728 Current children cumulated CPU time (s) 766.83 Current children cumulated vsize (Kb) 149852 [startup+780.062 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 37073 0 0 0 77436 242 0 0 25 0 1 0 1855205461 153255936 36683 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 37416 36683 145 145 0 37271 0 [pid=20777] vsize: 149664 Current children cumulated CPU time (s) 776.79 Current children cumulated vsize (Kb) 151788 [startup+790.063 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 37406 0 0 0 78432 243 0 0 25 0 1 0 1855205461 154619904 37016 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 37749 37016 145 145 0 37604 0 [pid=20777] vsize: 150996 Current children cumulated CPU time (s) 786.76 Current children cumulated vsize (Kb) 153120 [startup+800.063 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 37766 0 0 0 79425 247 0 0 25 0 1 0 1855205461 156086272 37376 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 38107 37376 145 145 0 37962 0 [pid=20777] vsize: 152428 Current children cumulated CPU time (s) 796.73 Current children cumulated vsize (Kb) 154552 [startup+810.065 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38156 0 0 0 80419 249 0 0 25 0 1 0 1855205461 157687808 37766 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 38498 37766 145 145 0 38353 0 [pid=20777] vsize: 153992 Current children cumulated CPU time (s) 806.69 Current children cumulated vsize (Kb) 156116 [startup+820.066 s] Raw data (loadavg): 1.00 0.97 0.85 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38585 0 0 0 81413 252 0 0 25 0 1 0 1855205461 159440896 38195 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 38926 38195 145 145 0 38781 0 [pid=20777] vsize: 155704 Current children cumulated CPU time (s) 816.66 Current children cumulated vsize (Kb) 157828 [startup+830.066 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38788 0 0 0 82409 254 0 0 25 0 1 0 1855205461 160268288 38398 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39128 38398 145 145 0 38983 0 [pid=20777] vsize: 156512 Current children cumulated CPU time (s) 826.64 Current children cumulated vsize (Kb) 158636 [startup+840.067 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 83408 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 836.64 Current children cumulated vsize (Kb) 158916 [startup+850.068 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 84408 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 846.64 Current children cumulated vsize (Kb) 158916 [startup+860.068 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 85409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 856.65 Current children cumulated vsize (Kb) 158916 [startup+870.069 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 86409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 866.65 Current children cumulated vsize (Kb) 158916 [startup+880.07 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 87409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 876.65 Current children cumulated vsize (Kb) 158916 [startup+890.07 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 88409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 886.65 Current children cumulated vsize (Kb) 158916 [startup+900.071 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 89409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223104 134555232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 896.65 Current children cumulated vsize (Kb) 158916 [startup+910.073 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 90409 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 906.65 Current children cumulated vsize (Kb) 158916 [startup+920.073 s] Raw data (loadavg): 1.00 0.97 0.86 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 91410 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 916.66 Current children cumulated vsize (Kb) 158916 [startup+930.074 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 92410 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 926.66 Current children cumulated vsize (Kb) 158916 [startup+940.075 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 93410 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 936.66 Current children cumulated vsize (Kb) 158916 [startup+950.075 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 94411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 946.67 Current children cumulated vsize (Kb) 158916 [startup+960.076 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 95411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 956.67 Current children cumulated vsize (Kb) 158916 [startup+970.077 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 96411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 966.67 Current children cumulated vsize (Kb) 158916 [startup+980.077 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 97411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 976.67 Current children cumulated vsize (Kb) 158916 [startup+990.078 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 98411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 986.67 Current children cumulated vsize (Kb) 158916 [startup+1000.08 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 99411 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 996.67 Current children cumulated vsize (Kb) 158916 [startup+1010.08 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 100412 255 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1006.68 Current children cumulated vsize (Kb) 158916 [startup+1020.08 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 101410 257 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1016.68 Current children cumulated vsize (Kb) 158916 [startup+1030.08 s] Raw data (loadavg): 1.00 0.97 0.87 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 102410 257 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1026.68 Current children cumulated vsize (Kb) 158916 [startup+1040.08 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 103410 258 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1036.69 Current children cumulated vsize (Kb) 158916 [startup+1050.08 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 104409 258 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1046.68 Current children cumulated vsize (Kb) 158916 [startup+1060.08 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 105409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1056.69 Current children cumulated vsize (Kb) 158916 [startup+1070.08 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 106409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1066.69 Current children cumulated vsize (Kb) 158916 [startup+1080.09 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 107409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1076.69 Current children cumulated vsize (Kb) 158916 [startup+1090.09 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 108409 259 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1086.69 Current children cumulated vsize (Kb) 158916 [startup+1100.09 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 109409 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1096.7 Current children cumulated vsize (Kb) 158916 [startup+1110.09 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 110410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1106.71 Current children cumulated vsize (Kb) 158916 [startup+1120.09 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 111410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1116.71 Current children cumulated vsize (Kb) 158916 [startup+1130.09 s] Raw data (loadavg): 1.00 0.97 0.88 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 112410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1126.71 Current children cumulated vsize (Kb) 158916 [startup+1140.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 113410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1136.71 Current children cumulated vsize (Kb) 158916 [startup+1150.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 114410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1146.71 Current children cumulated vsize (Kb) 158916 [startup+1160.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 115410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1156.71 Current children cumulated vsize (Kb) 158916 [startup+1170.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 116410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1166.71 Current children cumulated vsize (Kb) 158916 [startup+1180.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 117410 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1176.71 Current children cumulated vsize (Kb) 158916 [startup+1190.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 118411 260 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1186.72 Current children cumulated vsize (Kb) 158916 [startup+1200.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 119411 261 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1196.73 Current children cumulated vsize (Kb) 158916 [startup+1210.09 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 120411 261 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1206.73 Current children cumulated vsize (Kb) 158916 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 0.97 0.89 2/57 20777 Raw data (/proc/20773/stat): 20773 (minisat+_script) S 20772 20773 20115 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855205456 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20773/statm): 531 226 485 147 0 384 0 [pid=20773] vsize: 2124 Raw data (/proc/20777/stat): 20777 (minisat+_64-bit) R 20773 20773 20115 0 -1 0 38859 0 0 0 120411 261 0 0 25 0 1 0 1855205461 160555008 38469 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20777/statm): 39198 38469 145 145 0 39053 0 [pid=20777] vsize: 156792 Current children cumulated CPU time (s) 1206.73 Current children cumulated vsize (Kb) 158916 Sending SIGTERM to -20773 Sleeping 2 seconds One traced child (pid=20773) ended because it received signal 15 (SIGTERM) One traced child (pid=20777) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1206.8 CPU user time (s): 1204.11 CPU system time (s): 2.68359 CPU usage (%): 99.7213 Max. virtual memory (cumulated for all children) (Kb): 158916
ERROR: no interpretation found !