Name | mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-ran14x18_1.opb |
MD5SUM | d1752d9737bcd79380522c97c646ca71 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 10877893 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 7812 |
Biggest coefficient in the objective function | 5368709120 |
Number of bits for the biggest coefficient in the objective function | 33 |
Sum of the numbers in the objective function | 1450667950777 |
Number of bits of the sum of numbers in the objective function | 41 |
Biggest number in a constraint | 5368709120 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 1450667950777 |
Number of bits of the biggest sum of numbers | 41 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1227.68 |
Number of variables | 7812 |
Total number of constraints | 536 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 252 |
Number of constraints which are nor clauses,nor cardinality constraints | 284 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 540 |
LAUNCH ON wulflinc3 THE 2005-09-20 01:46:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3081 boxname=wulflinc3 idbench=737 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d1752d9737bcd79380522c97c646ca71 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran14x18_1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran14x18_1.opb IDLAUNCH: 3081 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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: 926980 kB Buffers: 3908 kB Cached: 77072 kB SwapCached: 824 kB Active: 15716 kB Inactive: 67848 kB HighTotal: 131008 kB HighFree: 49980 kB LowTotal: 903652 kB LowFree: 877000 kB SwapTotal: 2097136 kB SwapFree: 2095740 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5656 kB Slab: 18216 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 02:06:14 (client local time) WITH STATUS 0 IN 1207.51 SECONDS stats: 3081 7 1207.51 0
c Parsing PB file... c Converting 316 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################ c -- Clauses(.)/Splits(s): (none) c ---[ 314]---> Adder-cost: 488 maxlim: 379886 bits: 19/19 c ---[ 312]---> Adder-cost: 488 maxlim: 381934 bits: 19/19 c ---[ 310]---> Adder-cost: 488 maxlim: 378862 bits: 19/19 c ---[ 308]---> Adder-cost: 490 maxlim: 465902 bits: 19/19 c ---[ 306]---> Adder-cost: 488 maxlim: 378862 bits: 19/19 c ---[ 304]---> Adder-cost: 488 maxlim: 374766 bits: 19/19 c ---[ 302]---> Adder-cost: 488 maxlim: 376814 bits: 19/19 c ---[ 300]---> Adder-cost: 474 maxlim: 260078 bits: 19/18 c ---[ 298]---> Adder-cost: 488 maxlim: 373742 bits: 19/19 c ---[ 296]---> Adder-cost: 488 maxlim: 375790 bits: 19/19 c ---[ 294]---> Adder-cost: 474 maxlim: 260078 bits: 19/18 c ---[ 292]---> Adder-cost: 488 maxlim: 385006 bits: 19/19 c ---[ 290]---> Adder-cost: 488 maxlim: 383982 bits: 19/19 c ---[ 288]---> Adder-cost: 490 maxlim: 460782 bits: 19/19 c ---[ 286]---> Adder-cost: 338 maxlim: 108530 bits: 17/17 c ---[ 284]---> Adder-cost: 364 maxlim: 216050 bits: 18/18 c ---[ 282]---> Adder-cost: 338 maxlim: 107506 bits: 17/17 c ---[ 280]---> Adder-cost: 388 maxlim: 407538 bits: 19/19 c ---[ 278]---> Adder-cost: 364 maxlim: 215026 bits: 18/18 c ---[ 276]---> Adder-cost: 388 maxlim: 403442 bits: 19/19 c ---[ 274]---> Adder-cost: 390 maxlim: 457714 bits: 19/19 c ---[ 272]---> Adder-cost: 390 maxlim: 445426 bits: 19/19 c ---[ 270]---> Adder-cost: 364 maxlim: 218098 bits: 18/18 c ---[ 268]---> Adder-cost: 364 maxlim: 221170 bits: 18/18 c ---[ 266]---> Adder-cost: 388 maxlim: 404466 bits: 19/19 c ---[ 264]---> Adder-cost: 364 maxlim: 218098 bits: 18/18 c ---[ 262]---> Adder-cost: 388 maxlim: 405490 bits: 19/19 c ---[ 260]---> Adder-cost: 338 maxlim: 110578 bits: 17/17 c ---[ 258]---> Adder-cost: 390 maxlim: 455666 bits: 19/19 c ---[ 256]---> Adder-cost: 364 maxlim: 216050 bits: 18/18 c ---[ 254]---> Adder-cost: 388 maxlim: 405490 bits: 19/19 c ---[ 252]---> Adder-cost: 364 maxlim: 220146 bits: 18/18 c ---[ 251]---> BDD-cost: 15 c ---[ 250]---> BDD-cost: 18 c ---[ 249]---> BDD-cost: 16 c ---[ 248]---> BDD-cost: 16 c ---[ 247]---> BDD-cost: 19 c ---[ 246]---> BDD-cost: 17 c ---[ 245]---> BDD-cost: 19 c ---[ 244]---> BDD-cost: 20 c ---[ 243]---> BDD-cost: 20 c ---[ 242]---> BDD-cost: 18 c ---[ 241]---> BDD-cost: 15 c ---[ 240]---> BDD-cost: 15 c ---[ 239]---> BDD-cost: 17 c ---[ 238]---> BDD-cost: 19 c ---[ 237]---> BDD-cost: 17 c ---[ 236]---> BDD-cost: 17 c ---[ 235]---> BDD-cost: 17 c ---[ 234]---> BDD-cost: 14 c ---[ 233]---> BDD-cost: 17 c ---[ 232]---> BDD-cost: 17 c ---[ 231]---> BDD-cost: 17 c ---[ 230]---> BDD-cost: 18 c ---[ 229]---> BDD-cost: 16 c ---[ 228]---> BDD-cost: 17 c ---[ 227]---> BDD-cost: 17 c ---[ 226]---> BDD-cost: 17 c ---[ 225]---> BDD-cost: 17 c ---[ 224]---> BDD-cost: 17 c ---[ 223]---> BDD-cost: 17 c ---[ 222]---> BDD-cost: 17 c ---[ 221]---> BDD-cost: 15 c ---[ 220]---> BDD-cost: 15 c ---[ 219]---> BDD-cost: 18 c ---[ 218]---> BDD-cost: 16 c ---[ 217]---> BDD-cost: 18 c ---[ 216]---> BDD-cost: 20 c ---[ 215]---> BDD-cost: 16 c ---[ 214]---> BDD-cost: 14 c ---[ 213]---> BDD-cost: 16 c ---[ 212]---> BDD-cost: 18 c ---[ 211]---> BDD-cost: 16 c ---[ 210]---> BDD-cost: 18 c ---[ 209]---> BDD-cost: 16 c ---[ 208]---> BDD-cost: 16 c ---[ 207]---> BDD-cost: 17 c ---[ 206]---> BDD-cost: 16 c ---[ 205]---> BDD-cost: 20 c ---[ 204]---> BDD-cost: 16 c ---[ 203]---> BDD-cost: 16 c ---[ 202]---> BDD-cost: 18 c ---[ 201]---> BDD-cost: 15 c ---[ 200]---> BDD-cost: 15 c ---[ 199]---> BDD-cost: 18 c ---[ 198]---> BDD-cost: 20 c ---[ 197]---> BDD-cost: 18 c ---[ 196]---> BDD-cost: 20 c ---[ 195]---> BDD-cost: 14 c ---[ 194]---> BDD-cost: 20 c ---[ 193]---> BDD-cost: 20 c ---[ 192]---> BDD-cost: 18 c ---[ 191]---> BDD-cost: 20 c ---[ 190]---> BDD-cost: 18 c ---[ 189]---> BDD-cost: 16 c ---[ 188]---> BDD-cost: 20 c ---[ 187]---> BDD-cost: 17 c ---[ 186]---> BDD-cost: 20 c ---[ 185]---> BDD-cost: 20 c ---[ 184]---> BDD-cost: 20 c ---[ 183]---> BDD-cost: 18 c ---[ 182]---> BDD-cost: 18 c ---[ 181]---> BDD-cost: 15 c ---[ 180]---> BDD-cost: 15 c ---[ 179]---> BDD-cost: 18 c ---[ 178]---> BDD-cost: 20 c ---[ 177]---> BDD-cost: 18 c ---[ 176]---> BDD-cost: 18 c ---[ 175]---> BDD-cost: 14 c ---[ 174]---> BDD-cost: 22 c ---[ 173]---> BDD-cost: 18 c ---[ 172]---> BDD-cost: 15 c ---[ 171]---> BDD-cost: 18 c ---[ 170]---> BDD-cost: 18 c ---[ 169]---> BDD-cost: 16 c ---[ 168]---> BDD-cost: 19 c ---[ 167]---> BDD-cost: 17 c ---[ 166]---> BDD-cost: 19 c ---[ 165]---> BDD-cost: 22 c ---[ 164]---> BDD-cost: 21 c ---[ 163]---> BDD-cost: 18 c ---[ 162]---> BDD-cost: 15 c ---[ 161]---> BDD-cost: 15 c ---[ 160]---> BDD-cost: 15 c ---[ 159]---> BDD-cost: 18 c ---[ 158]---> BDD-cost: 20 c ---[ 157]---> BDD-cost: 18 c ---[ 156]---> BDD-cost: 18 c ---[ 155]---> BDD-cost: 14 c ---[ 154]---> BDD-cost: 19 c ---[ 153]---> BDD-cost: 18 c ---[ 152]---> BDD-cost: 18 c ---[ 151]---> BDD-cost: 18 c ---[ 150]---> BDD-cost: 18 c ---[ 149]---> BDD-cost: 16 c ---[ 148]---> BDD-cost: 19 c ---[ 147]---> BDD-cost: 17 c ---[ 146]---> BDD-cost: 19 c ---[ 145]---> BDD-cost: 19 c ---[ 144]---> BDD-cost: 19 c ---[ 143]---> BDD-cost: 18 c ---[ 142]---> BDD-cost: 15 c ---[ 141]---> BDD-cost: 15 c ---[ 140]---> BDD-cost: 18 c ---[ 139]---> BDD-cost: 20 c ---[ 138]---> BDD-cost: 20 c ---[ 137]---> BDD-cost: 20 c ---[ 136]---> BDD-cost: 18 c ---[ 135]---> BDD-cost: 18 c ---[ 134]---> BDD-cost: 14 c ---[ 133]---> BDD-cost: 22 c ---[ 132]---> BDD-cost: 18 c ---[ 131]---> BDD-cost: 18 c ---[ 130]---> BDD-cost: 18 c ---[ 129]---> BDD-cost: 16 c ---[ 128]---> BDD-cost: 19 c ---[ 127]---> BDD-cost: 18 c ---[ 126]---> BDD-cost: 17 c ---[ 125]---> BDD-cost: 19 c ---[ 124]---> BDD-cost: 22 c ---[ 123]---> BDD-cost: 22 c ---[ 122]---> BDD-cost: 18 c ---[ 121]---> BDD-cost: 15 c ---[ 120]---> BDD-cost: 15 c ---[ 119]---> BDD-cost: 18 c ---[ 118]---> BDD-cost: 20 c ---[ 117]---> BDD-cost: 18 c ---[ 116]---> BDD-cost: 20 c ---[ 115]---> BDD-cost: 18 c ---[ 114]---> BDD-cost: 14 c ---[ 113]---> BDD-cost: 19 c ---[ 112]---> BDD-cost: 18 c ---[ 111]---> BDD-cost: 18 c ---[ 110]---> BDD-cost: 18 c ---[ 109]---> BDD-cost: 16 c ---[ 108]---> BDD-cost: 19 c ---[ 107]---> BDD-cost: 17 c ---[ 106]---> BDD-cost: 19 c ---[ 105]---> BDD-cost: 14 c ---[ 104]---> BDD-cost: 19 c ---[ 103]---> BDD-cost: 19 c ---[ 102]---> BDD-cost: 18 c ---[ 101]---> BDD-cost: 15 c ---[ 100]---> BDD-cost: 15 c ---[ 99]---> BDD-cost: 18 c ---[ 98]---> BDD-cost: 20 c ---[ 97]---> BDD-cost: 18 c ---[ 96]---> BDD-cost: 18 c ---[ 95]---> BDD-cost: 14 c ---[ 94]---> BDD-cost: 20 c ---[ 93]---> BDD-cost: 19 c ---[ 92]---> BDD-cost: 18 c ---[ 91]---> BDD-cost: 18 c ---[ 90]---> BDD-cost: 18 c ---[ 89]---> BDD-cost: 16 c ---[ 88]---> BDD-cost: 19 c ---[ 87]---> BDD-cost: 17 c ---[ 86]---> BDD-cost: 19 c ---[ 85]---> BDD-cost: 19 c ---[ 84]---> BDD-cost: 19 c ---[ 83]---> BDD-cost: 18 c ---[ 82]---> BDD-cost: 18 c ---[ 81]---> BDD-cost: 15 c ---[ 80]---> BDD-cost: 20 c ---[ 79]---> BDD-cost: 18 c ---[ 78]---> BDD-cost: 16 c ---[ 77]---> BDD-cost: 19 c ---[ 76]---> BDD-cost: 18 c ---[ 75]---> BDD-cost: 17 c ---[ 74]---> BDD-cost: 20 c ---[ 73]---> BDD-cost: 20 c ---[ 72]---> BDD-cost: 20 c ---[ 71]---> BDD-cost: 18 c ---[ 70]---> BDD-cost: 15 c ---[ 69]---> BDD-cost: 15 c ---[ 68]---> BDD-cost: 18 c ---[ 67]---> BDD-cost: 20 c ---[ 66]---> BDD-cost: 18 c ---[ 65]---> BDD-cost: 18 c ---[ 64]---> BDD-cost: 18 c ---[ 63]---> BDD-cost: 14 c ---[ 62]---> BDD-cost: 17 c ---[ 61]---> BDD-cost: 18 c ---[ 60]---> BDD-cost: 18 c ---[ 59]---> BDD-cost: 18 c ---[ 58]---> BDD-cost: 16 c ---[ 57]---> BDD-cost: 19 c ---[ 56]---> BDD-cost: 17 c ---[ 55]---> BDD-cost: 19 c ---[ 54]---> BDD-cost: 14 c ---[ 53]---> BDD-cost: 17 c ---[ 52]---> BDD-cost: 17 c ---[ 51]---> BDD-cost: 18 c ---[ 50]---> BDD-cost: 15 c ---[ 49]---> BDD-cost: 15 c ---[ 48]---> BDD-cost: 17 c ---[ 47]---> BDD-cost: 17 c ---[ 46]---> BDD-cost: 17 c ---[ 45]---> BDD-cost: 17 c ---[ 44]---> BDD-cost: 14 c ---[ 43]---> BDD-cost: 20 c ---[ 42]---> BDD-cost: 17 c ---[ 41]---> BDD-cost: 17 c ---[ 40]---> BDD-cost: 17 c ---[ 39]---> BDD-cost: 18 c ---[ 38]---> BDD-cost: 16 c ---[ 37]---> BDD-cost: 17 c ---[ 36]---> BDD-cost: 17 c ---[ 35]---> BDD-cost: 17 c ---[ 34]---> BDD-cost: 17 c ---[ 33]---> BDD-cost: 17 c ---[ 32]---> BDD-cost: 18 c ---[ 31]---> BDD-cost: 17 c ---[ 30]---> BDD-cost: 15 c ---[ 29]---> BDD-cost: 15 c ---[ 28]---> BDD-cost: 18 c ---[ 27]---> BDD-cost: 20 c ---[ 26]---> BDD-cost: 18 c ---[ 25]---> BDD-cost: 18 c ---[ 24]---> BDD-cost: 14 c ---[ 23]---> BDD-cost: 20 c ---[ 22]---> BDD-cost: 18 c ---[ 21]---> BDD-cost: 18 c ---[ 20]---> BDD-cost: 18 c ---[ 19]---> BDD-cost: 18 c ---[ 18]---> BDD-cost: 16 c ---[ 17]---> BDD-cost: 19 c ---[ 16]---> BDD-cost: 17 c ---[ 15]---> BDD-cost: 19 c ---[ 14]---> BDD-cost: 20 c ---[ 13]---> BDD-cost: 20 c ---[ 12]---> BDD-cost: 18 c ---[ 11]---> BDD-cost: 15 c ---[ 10]---> BDD-cost: 18 c ---[ 9]---> BDD-cost: 15 c ---[ 8]---> BDD-cost: 18 c ---[ 7]---> BDD-cost: 20 c ---[ 6]---> BDD-cost: 18 c ---[ 5]---> BDD-cost: 18 c ---[ 4]---> BDD-cost: 14 c ---[ 3]---> BDD-cost: 20 c ---[ 2]---> BDD-cost: 18 c ---[ 1]---> BDD-cost: 18 c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 96690 336663 | 32230 0 0 nan | 0.000 % | c | 100 | 96690 336663 | 35453 100 311 3.1 | 23.163 % | c | 250 | 96581 336296 | 38998 241 746 3.1 | 23.249 % | c | 475 | 96405 335706 | 42898 440 1437 3.3 | 23.383 % | c | 812 | 96339 335484 | 47187 765 2476 3.2 | 23.430 % | c | 1318 | 96007 334356 | 51906 1235 4051 3.3 | 23.688 % | c | 2077 | 95562 332849 | 57097 1943 6475 3.3 | 24.028 % | c | 3216 | 95220 331691 | 62807 3049 10430 3.4 | 24.291 % | c | 4924 | 94533 329356 | 69087 4676 16439 3.5 | 24.812 % | c | 7486 | 94190 328193 | 75996 7202 32994 4.6 | 25.074 % | c | 11330 | 94016 327595 | 83596 11032 53560 4.9 | 25.216 % | c | 17096 | 93968 327439 | 91955 16792 96512 5.7 | 25.255 % | c | 25745 | 93968 327439 | 101151 25441 852627 33.5 | 25.255 % | c | 38719 | 93901 327210 | 111266 38405 1127551 29.4 | 25.307 % | c | 58182 | 93719 326586 | 122393 57845 2484955 43.0 | 25.440 % | c | 87375 | 93659 326386 | 134632 87030 2988827 34.3 | 25.487 % | c | 131164 | 93612 326227 | 148095 130814 5137483 39.3 | 25.530 % | c | 196849 | 93578 326117 | 162905 68955 2299344 33.3 | 25.561 % | c | 295376 | 93442 325669 | 179196 167463 6223482 37.2 | 25.677 % | c | 443165 | 93356 325383 | 197115 156030 4776162 30.6 | 25.750 % | c | 664848 | 93054 324349 | 216827 206010 7341199 35.6 | 25.995 % |
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/3200/stat): 3200 (minisat+_script) R 3199 3200 31915 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796444161 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/3200/statm): 174 3 169 147 0 27 0 [pid=3200] 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=3201 New process pid=3202 New process pid=3203 execve syscall for /bin/sed executable One traced child (pid=3202) 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=3203) exited with status: 0 One traced child (pid=3201) exited with status: 0 New process pid=3204 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran14x18_1.opb [startup+10.0042 s] Raw data (loadavg): 0.93 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 2435 0 0 0 974 11 0 0 25 0 1 0 1796444166 10366976 2292 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 2531 2292 145 145 0 2386 0 [pid=3204] vsize: 10124 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 12248 [startup+20.005 s] Raw data (loadavg): 0.94 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 2488 0 0 0 1973 12 0 0 25 0 1 0 1796444166 10584064 2345 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 2584 2345 145 145 0 2439 0 [pid=3204] vsize: 10336 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 12460 [startup+30.0059 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 2588 0 0 0 2971 13 0 0 25 0 1 0 1796444166 10997760 2445 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 2685 2445 145 145 0 2540 0 [pid=3204] vsize: 10740 Current children cumulated CPU time (s) 29.84 Current children cumulated vsize (Kb) 12864 [startup+40.0067 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 3486 0 0 0 3956 19 0 0 25 0 1 0 1796444166 14696448 3343 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 3588 3343 145 145 0 3443 0 [pid=3204] vsize: 14352 Current children cumulated CPU time (s) 39.75 Current children cumulated vsize (Kb) 16476 [startup+50.0075 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 3699 0 0 0 4953 20 0 0 25 0 1 0 1796444166 15667200 3556 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 3825 3556 145 145 0 3680 0 [pid=3204] vsize: 15300 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 17424 [startup+60.0084 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 4103 0 0 0 5947 24 0 0 25 0 1 0 1796444166 17281024 3960 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 4219 3960 145 145 0 4074 0 [pid=3204] vsize: 16876 Current children cumulated CPU time (s) 59.71 Current children cumulated vsize (Kb) 19000 [startup+70.0092 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 5177 0 0 0 6931 31 0 0 25 0 1 0 1796444166 21635072 5034 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 5282 5034 145 145 0 5137 0 [pid=3204] vsize: 21128 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 23252 [startup+80.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 5638 0 0 0 7924 34 0 0 25 0 1 0 1796444166 23498752 5495 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 5737 5495 145 145 0 5592 0 [pid=3204] vsize: 22948 Current children cumulated CPU time (s) 79.58 Current children cumulated vsize (Kb) 25072 [startup+90.0109 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 5794 0 0 0 8920 35 0 0 25 0 1 0 1796444166 24375296 5651 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 5951 5651 145 145 0 5806 0 [pid=3204] vsize: 23804 Current children cumulated CPU time (s) 89.55 Current children cumulated vsize (Kb) 25928 [startup+100.011 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 6066 0 0 0 9917 37 0 0 25 0 1 0 1796444166 25448448 5923 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 6213 5923 145 145 0 6068 0 [pid=3204] vsize: 24852 Current children cumulated CPU time (s) 99.54 Current children cumulated vsize (Kb) 26976 [startup+110.013 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 6479 0 0 0 10909 40 0 0 25 0 1 0 1796444166 27095040 6336 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 6615 6336 145 145 0 6470 0 [pid=3204] vsize: 26460 Current children cumulated CPU time (s) 109.49 Current children cumulated vsize (Kb) 28584 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 7433 0 0 0 11896 45 0 0 25 0 1 0 1796444166 30941184 7290 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 7554 7290 145 145 0 7409 0 [pid=3204] vsize: 30216 Current children cumulated CPU time (s) 119.41 Current children cumulated vsize (Kb) 32340 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 7923 0 0 0 12888 49 0 0 25 0 1 0 1796444166 32907264 7780 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 8034 7780 145 145 0 7889 0 [pid=3204] vsize: 32136 Current children cumulated CPU time (s) 129.37 Current children cumulated vsize (Kb) 34260 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 8616 0 0 0 13877 53 0 0 25 0 1 0 1796444166 35704832 8473 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 8717 8473 145 145 0 8572 0 [pid=3204] vsize: 34868 Current children cumulated CPU time (s) 139.3 Current children cumulated vsize (Kb) 36992 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9183 0 0 0 14870 57 0 0 25 0 1 0 1796444166 38522880 9040 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9405 9040 145 145 0 9260 0 [pid=3204] vsize: 37620 Current children cumulated CPU time (s) 149.27 Current children cumulated vsize (Kb) 39744 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9392 0 0 0 15868 58 0 0 25 0 1 0 1796444166 39350272 9249 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9607 9249 145 145 0 9462 0 [pid=3204] vsize: 38428 Current children cumulated CPU time (s) 159.26 Current children cumulated vsize (Kb) 40552 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9599 0 0 0 16865 59 0 0 25 0 1 0 1796444166 40165376 9456 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9806 9456 145 145 0 9661 0 [pid=3204] vsize: 39224 Current children cumulated CPU time (s) 169.24 Current children cumulated vsize (Kb) 41348 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 17864 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 179.24 Current children cumulated vsize (Kb) 41608 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 18864 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 189.24 Current children cumulated vsize (Kb) 41608 [startup+200.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 19864 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 199.24 Current children cumulated vsize (Kb) 41608 [startup+210.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 20865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223160 134554333 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 209.25 Current children cumulated vsize (Kb) 41608 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 21865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 219.25 Current children cumulated vsize (Kb) 41608 [startup+230.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 22865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 229.25 Current children cumulated vsize (Kb) 41608 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 23865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 239.25 Current children cumulated vsize (Kb) 41608 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 24865 60 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 249.25 Current children cumulated vsize (Kb) 41608 [startup+260.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 25865 61 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 259.26 Current children cumulated vsize (Kb) 41608 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 26865 61 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 269.26 Current children cumulated vsize (Kb) 41608 [startup+280.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 9666 0 0 0 27865 61 0 0 25 0 1 0 1796444166 40431616 9523 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 9871 9523 145 145 0 9726 0 [pid=3204] vsize: 39484 Current children cumulated CPU time (s) 279.26 Current children cumulated vsize (Kb) 41608 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 10038 0 0 0 28860 63 0 0 25 0 1 0 1796444166 41975808 9895 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 10248 9895 145 145 0 10103 0 [pid=3204] vsize: 40992 Current children cumulated CPU time (s) 289.23 Current children cumulated vsize (Kb) 43116 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 10625 0 0 0 29851 67 0 0 25 0 1 0 1796444166 44400640 10482 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 10840 10482 145 145 0 10695 0 [pid=3204] vsize: 43360 Current children cumulated CPU time (s) 299.18 Current children cumulated vsize (Kb) 45484 [startup+310.031 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) T 3200 3200 31915 0 -1 0 10960 0 0 0 30846 69 0 0 25 0 1 0 1796444166 45740032 10817 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11167 10817 145 145 0 11022 0 [pid=3204] vsize: 44668 Current children cumulated CPU time (s) 309.15 Current children cumulated vsize (Kb) 46792 [startup+320.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11158 0 0 0 31844 71 0 0 25 0 1 0 1796444166 46534656 11015 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11361 11015 145 145 0 11216 0 [pid=3204] vsize: 45444 Current children cumulated CPU time (s) 319.15 Current children cumulated vsize (Kb) 47568 [startup+330.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11302 0 0 0 32842 72 0 0 25 0 1 0 1796444166 47108096 11159 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11501 11159 145 145 0 11356 0 [pid=3204] vsize: 46004 Current children cumulated CPU time (s) 329.14 Current children cumulated vsize (Kb) 48128 [startup+340.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11573 0 0 0 33836 74 0 0 25 0 1 0 1796444166 48181248 11430 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11763 11430 145 145 0 11618 0 [pid=3204] vsize: 47052 Current children cumulated CPU time (s) 339.1 Current children cumulated vsize (Kb) 49176 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 34834 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 349.09 Current children cumulated vsize (Kb) 49572 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 35834 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 359.09 Current children cumulated vsize (Kb) 49572 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 36834 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 369.09 Current children cumulated vsize (Kb) 49572 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 37835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 379.1 Current children cumulated vsize (Kb) 49572 [startup+390.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 38835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 389.1 Current children cumulated vsize (Kb) 49572 [startup+400.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 39835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 399.1 Current children cumulated vsize (Kb) 49572 [startup+410.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 40835 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 409.1 Current children cumulated vsize (Kb) 49572 [startup+420.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 41836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 419.11 Current children cumulated vsize (Kb) 49572 [startup+430.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 42836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 429.11 Current children cumulated vsize (Kb) 49572 [startup+440.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 43836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 439.11 Current children cumulated vsize (Kb) 49572 [startup+450.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 44836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 449.11 Current children cumulated vsize (Kb) 49572 [startup+460.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 45837 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 459.12 Current children cumulated vsize (Kb) 49572 [startup+470.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 46837 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 469.12 Current children cumulated vsize (Kb) 49572 [startup+480.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 47836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 479.11 Current children cumulated vsize (Kb) 49572 [startup+490.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 48836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 489.11 Current children cumulated vsize (Kb) 49572 [startup+500.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11676 0 0 0 49836 75 0 0 25 0 1 0 1796444166 48586752 11533 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 11862 11533 145 145 0 11717 0 [pid=3204] vsize: 47448 Current children cumulated CPU time (s) 499.11 Current children cumulated vsize (Kb) 49572 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 11910 0 0 0 50832 77 0 0 25 0 1 0 1796444166 49532928 11767 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12093 11767 145 145 0 11948 0 [pid=3204] vsize: 48372 Current children cumulated CPU time (s) 509.09 Current children cumulated vsize (Kb) 50496 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12098 0 0 0 51830 78 0 0 25 0 1 0 1796444166 50278400 11955 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12275 11955 145 145 0 12130 0 [pid=3204] vsize: 49100 Current children cumulated CPU time (s) 519.08 Current children cumulated vsize (Kb) 51224 [startup+530.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12220 0 0 0 52828 79 0 0 25 0 1 0 1796444166 50761728 12077 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12393 12077 145 145 0 12248 0 [pid=3204] vsize: 49572 Current children cumulated CPU time (s) 529.07 Current children cumulated vsize (Kb) 51696 [startup+540.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 53828 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 539.07 Current children cumulated vsize (Kb) 51740 [startup+550.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 54829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 549.08 Current children cumulated vsize (Kb) 51740 [startup+560.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 55829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 559.08 Current children cumulated vsize (Kb) 51740 [startup+570.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 56829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 569.08 Current children cumulated vsize (Kb) 51740 [startup+580.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 57829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 579.08 Current children cumulated vsize (Kb) 51740 [startup+590.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 58829 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 589.08 Current children cumulated vsize (Kb) 51740 [startup+600.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 59830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 599.09 Current children cumulated vsize (Kb) 51740 [startup+610.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 60830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 609.09 Current children cumulated vsize (Kb) 51740 [startup+620.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 61830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 619.09 Current children cumulated vsize (Kb) 51740 [startup+630.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 62830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 629.09 Current children cumulated vsize (Kb) 51740 [startup+640.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 63830 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 639.09 Current children cumulated vsize (Kb) 51740 [startup+650.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 64831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 649.1 Current children cumulated vsize (Kb) 51740 [startup+660.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 65831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 659.1 Current children cumulated vsize (Kb) 51740 [startup+670.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 66831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 669.1 Current children cumulated vsize (Kb) 51740 [startup+680.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 67831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 679.1 Current children cumulated vsize (Kb) 51740 [startup+690.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 68831 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 689.1 Current children cumulated vsize (Kb) 51740 [startup+700.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 69832 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223104 134555755 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 699.11 Current children cumulated vsize (Kb) 51740 [startup+710.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12232 0 0 0 70832 79 0 0 25 0 1 0 1796444166 50806784 12089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 12404 12089 145 145 0 12259 0 [pid=3204] vsize: 49616 Current children cumulated CPU time (s) 709.11 Current children cumulated vsize (Kb) 51740 [startup+720.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 12950 0 0 0 71820 84 0 0 25 0 1 0 1796444166 53747712 12807 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 13122 12807 145 145 0 12977 0 [pid=3204] vsize: 52488 Current children cumulated CPU time (s) 719.04 Current children cumulated vsize (Kb) 54612 [startup+730.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 13742 0 0 0 72808 90 0 0 25 0 1 0 1796444166 56995840 13599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 13915 13599 145 145 0 13770 0 [pid=3204] vsize: 55660 Current children cumulated CPU time (s) 728.98 Current children cumulated vsize (Kb) 57784 [startup+740.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 13873 0 0 0 73805 92 0 0 25 0 1 0 1796444166 57511936 13730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14041 13730 145 145 0 13896 0 [pid=3204] vsize: 56164 Current children cumulated CPU time (s) 738.97 Current children cumulated vsize (Kb) 58288 [startup+750.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14065 0 0 0 74801 93 0 0 25 0 1 0 1796444166 58273792 13922 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14227 13922 145 145 0 14082 0 [pid=3204] vsize: 56908 Current children cumulated CPU time (s) 748.94 Current children cumulated vsize (Kb) 59032 [startup+760.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 75800 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 758.93 Current children cumulated vsize (Kb) 59404 [startup+770.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 76800 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 768.93 Current children cumulated vsize (Kb) 59404 [startup+780.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 77800 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 778.93 Current children cumulated vsize (Kb) 59404 [startup+790.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 78801 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223100 134550364 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 788.94 Current children cumulated vsize (Kb) 59404 [startup+800.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 79801 93 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 798.94 Current children cumulated vsize (Kb) 59404 [startup+810.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 80801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 808.95 Current children cumulated vsize (Kb) 59404 [startup+820.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 81801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 818.95 Current children cumulated vsize (Kb) 59404 [startup+830.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 82801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 828.95 Current children cumulated vsize (Kb) 59404 [startup+840.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 83801 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 838.95 Current children cumulated vsize (Kb) 59404 [startup+850.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 84802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 848.96 Current children cumulated vsize (Kb) 59404 [startup+860.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 85802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 858.96 Current children cumulated vsize (Kb) 59404 [startup+870.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 86802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 868.96 Current children cumulated vsize (Kb) 59404 [startup+880.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 87802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 878.96 Current children cumulated vsize (Kb) 59404 [startup+890.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 88802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 888.96 Current children cumulated vsize (Kb) 59404 [startup+900.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 89802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 898.96 Current children cumulated vsize (Kb) 59404 [startup+910.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 14163 0 0 0 90802 94 0 0 25 0 1 0 1796444166 58654720 14020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 14320 14020 145 145 0 14175 0 [pid=3204] vsize: 57280 Current children cumulated CPU time (s) 908.96 Current children cumulated vsize (Kb) 59404 [startup+920.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 15121 0 0 0 91790 98 0 0 25 0 1 0 1796444166 62590976 14978 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 15281 14978 145 145 0 15136 0 [pid=3204] vsize: 61124 Current children cumulated CPU time (s) 918.88 Current children cumulated vsize (Kb) 63248 [startup+930.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) T 3200 3200 31915 0 -1 0 16382 0 0 0 92768 108 0 0 25 0 1 0 1796444166 67760128 16239 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/3204/statm): 16543 16239 145 145 0 16398 0 [pid=3204] vsize: 66172 Current children cumulated CPU time (s) 928.76 Current children cumulated vsize (Kb) 68296 [startup+940.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) T 3200 3200 31915 0 -1 0 17339 0 0 0 93752 114 0 0 25 0 1 0 1796444166 71684096 17196 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/3204/statm): 17501 17196 145 145 0 17356 0 [pid=3204] vsize: 70004 Current children cumulated CPU time (s) 938.66 Current children cumulated vsize (Kb) 72128 [startup+950.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 18244 0 0 0 94738 121 0 0 25 0 1 0 1796444166 75419648 18101 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 18413 18101 145 145 0 18268 0 [pid=3204] vsize: 73652 Current children cumulated CPU time (s) 948.59 Current children cumulated vsize (Kb) 75776 [startup+960.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 19257 0 0 0 95722 127 0 0 25 0 1 0 1796444166 79568896 19114 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 19426 19114 145 145 0 19281 0 [pid=3204] vsize: 77704 Current children cumulated CPU time (s) 958.49 Current children cumulated vsize (Kb) 79828 [startup+970.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 20240 0 0 0 96708 134 0 0 25 0 1 0 1796444166 83615744 20097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 20414 20097 145 145 0 20269 0 [pid=3204] vsize: 81656 Current children cumulated CPU time (s) 968.42 Current children cumulated vsize (Kb) 83780 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 21193 0 0 0 97693 141 0 0 25 0 1 0 1796444166 87531520 21050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 21370 21050 145 145 0 21225 0 [pid=3204] vsize: 85480 Current children cumulated CPU time (s) 978.34 Current children cumulated vsize (Kb) 87604 [startup+990.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 21948 0 0 0 98679 147 0 0 25 0 1 0 1796444166 90644480 21805 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 22130 21805 145 145 0 21985 0 [pid=3204] vsize: 88520 Current children cumulated CPU time (s) 988.26 Current children cumulated vsize (Kb) 90644 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 22772 0 0 0 99665 152 0 0 25 0 1 0 1796444166 94101504 22629 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 22974 22629 145 145 0 22829 0 [pid=3204] vsize: 91896 Current children cumulated CPU time (s) 998.17 Current children cumulated vsize (Kb) 94020 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 23605 0 0 0 100650 158 0 0 25 0 1 0 1796444166 97554432 23462 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 23817 23462 145 145 0 23672 0 [pid=3204] vsize: 95268 Current children cumulated CPU time (s) 1008.08 Current children cumulated vsize (Kb) 97392 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 24385 0 0 0 101635 164 0 0 25 0 1 0 1796444166 100737024 24242 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 24594 24242 145 145 0 24449 0 [pid=3204] vsize: 98376 Current children cumulated CPU time (s) 1017.99 Current children cumulated vsize (Kb) 100500 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 25222 0 0 0 102621 170 0 0 25 0 1 0 1796444166 104173568 25079 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 25433 25079 145 145 0 25288 0 [pid=3204] vsize: 101732 Current children cumulated CPU time (s) 1027.91 Current children cumulated vsize (Kb) 103856 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 26098 0 0 0 103606 176 0 0 25 0 1 0 1796444166 107769856 25955 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3204/statm): 26311 25955 145 145 0 26166 0 [pid=3204] vsize: 105244 Current children cumulated CPU time (s) 1037.82 Current children cumulated vsize (Kb) 107368 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 26841 0 0 0 104594 181 0 0 25 0 1 0 1796444166 110833664 26698 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 27059 26698 145 145 0 26914 0 [pid=3204] vsize: 108236 Current children cumulated CPU time (s) 1047.75 Current children cumulated vsize (Kb) 110360 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 27516 0 0 0 105579 187 0 0 25 0 1 0 1796444166 113590272 27373 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 27732 27373 145 145 0 27587 0 [pid=3204] vsize: 110928 Current children cumulated CPU time (s) 1057.66 Current children cumulated vsize (Kb) 113052 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 28171 0 0 0 106567 193 0 0 25 0 1 0 1796444166 116244480 28028 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 28380 28028 145 145 0 28235 0 [pid=3204] vsize: 113520 Current children cumulated CPU time (s) 1067.6 Current children cumulated vsize (Kb) 115644 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 28846 0 0 0 107556 198 0 0 25 0 1 0 1796444166 119037952 28703 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 29062 28703 145 145 0 28917 0 [pid=3204] vsize: 116248 Current children cumulated CPU time (s) 1077.54 Current children cumulated vsize (Kb) 118372 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 29442 0 0 0 108547 201 0 0 25 0 1 0 1796444166 121458688 29299 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 29653 29299 145 145 0 29508 0 [pid=3204] vsize: 118612 Current children cumulated CPU time (s) 1087.48 Current children cumulated vsize (Kb) 120736 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30064 0 0 0 109537 206 0 0 25 0 1 0 1796444166 124006400 29921 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30275 29921 145 145 0 30130 0 [pid=3204] vsize: 121100 Current children cumulated CPU time (s) 1097.43 Current children cumulated vsize (Kb) 123224 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 110536 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1107.42 Current children cumulated vsize (Kb) 123568 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 111537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1117.43 Current children cumulated vsize (Kb) 123568 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 112537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1127.43 Current children cumulated vsize (Kb) 123568 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 113537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1137.43 Current children cumulated vsize (Kb) 123568 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 114537 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1147.43 Current children cumulated vsize (Kb) 123568 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 115538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1157.44 Current children cumulated vsize (Kb) 123568 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 116538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1167.44 Current children cumulated vsize (Kb) 123568 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 117538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1177.44 Current children cumulated vsize (Kb) 123568 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 118538 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1187.44 Current children cumulated vsize (Kb) 123568 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 119539 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1197.45 Current children cumulated vsize (Kb) 123568 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 120539 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1207.45 Current children cumulated vsize (Kb) 123568 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3204 Raw data (/proc/3200/stat): 3200 (minisat+_script) S 3199 3200 31915 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1796444161 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3200/statm): 531 226 485 147 0 384 0 [pid=3200] vsize: 2124 Raw data (/proc/3204/stat): 3204 (minisat+_64-bit) R 3200 3200 31915 0 -1 0 30145 0 0 0 120539 206 0 0 25 0 1 0 1796444166 124358656 30002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3204/statm): 30361 30002 145 145 0 30216 0 [pid=3204] vsize: 121444 Current children cumulated CPU time (s) 1207.45 Current children cumulated vsize (Kb) 123568 Sending SIGTERM to -3200 Sleeping 2 seconds One traced child (pid=3200) ended because it received signal 15 (SIGTERM) One traced child (pid=3204) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1207.51 CPU user time (s): 1205.39 CPU system time (s): 2.12068 CPU usage (%): 99.7803 Max. virtual memory (cumulated for all children) (Kb): 123568
ERROR: no interpretation found !