Name | mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran17x17.opb |
MD5SUM | a15c04744ea6af8a8a8518cde7c56bce |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4017978 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 8959 |
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 | 1612776422946 |
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 | 1612776422946 |
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 | 1226.92 |
Number of variables | 8959 |
Total number of constraints | 323 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 323 |
Minimum length of a constraint | 31 |
Maximum length of a constraint | 510 |
LAUNCH ON wulflinc27 THE 2005-09-20 01:25:02 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3045 boxname=wulflinc27 idbench=701 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a15c04744ea6af8a8a8518cde7c56bce /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-ran17x17.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-ran17x17.opb IDLAUNCH: 3045 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 921760 kB Buffers: 17004 kB Cached: 66292 kB SwapCached: 752 kB Active: 25564 kB Inactive: 60388 kB HighTotal: 131008 kB HighFree: 62692 kB LowTotal: 903652 kB LowFree: 859068 kB SwapTotal: 2097892 kB SwapFree: 2096628 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5728 kB Slab: 21308 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 01:45:13 (client local time) WITH STATUS 0 IN 1208.45 SECONDS stats: 3045 7 1208.45 0
c Parsing PB file... c Converting 357 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################## c -- Clauses(.)/Splits(s): (none) c ---[ 355]---> Adder-cost: 434 maxlim: 225263 bits: 18/18 c ---[ 353]---> Adder-cost: 406 maxlim: 124911 bits: 17/17 c ---[ 351]---> Adder-cost: 434 maxlim: 223215 bits: 18/18 c ---[ 349]---> Adder-cost: 434 maxlim: 227311 bits: 18/18 c ---[ 347]---> Adder-cost: 456 maxlim: 372719 bits: 19/19 c ---[ 345]---> Adder-cost: 434 maxlim: 228335 bits: 18/18 c ---[ 343]---> Adder-cost: 434 maxlim: 229359 bits: 18/18 c ---[ 341]---> Adder-cost: 456 maxlim: 372719 bits: 19/19 c ---[ 339]---> Adder-cost: 458 maxlim: 431087 bits: 19/19 c ---[ 337]---> Adder-cost: 456 maxlim: 377839 bits: 19/19 c ---[ 335]---> Adder-cost: 456 maxlim: 375791 bits: 19/19 c ---[ 333]---> Adder-cost: 434 maxlim: 222191 bits: 18/18 c ---[ 331]---> Adder-cost: 458 maxlim: 434159 bits: 19/19 c ---[ 329]---> Adder-cost: 456 maxlim: 373743 bits: 19/19 c ---[ 327]---> Adder-cost: 456 maxlim: 381935 bits: 19/19 c ---[ 325]---> Adder-cost: 406 maxlim: 125935 bits: 17/17 c ---[ 323]---> Adder-cost: 406 maxlim: 126959 bits: 17/17 c ---[ 321]---> Adder-cost: 454 maxlim: 367599 bits: 19/19 c ---[ 319]---> Adder-cost: 416 maxlim: 133103 bits: 18/18 c ---[ 317]---> Adder-cost: 438 maxlim: 245743 bits: 18/18 c ---[ 315]---> Adder-cost: 416 maxlim: 135151 bits: 18/18 c ---[ 313]---> Adder-cost: 438 maxlim: 238575 bits: 18/18 c ---[ 311]---> Adder-cost: 454 maxlim: 368623 bits: 19/19 c ---[ 309]---> Adder-cost: 438 maxlim: 241647 bits: 18/18 c ---[ 307]---> Adder-cost: 458 maxlim: 416751 bits: 19/19 c ---[ 305]---> Adder-cost: 454 maxlim: 365551 bits: 19/19 c ---[ 303]---> Adder-cost: 384 maxlim: 66543 bits: 17/17 c ---[ 301]---> Adder-cost: 454 maxlim: 364527 bits: 19/19 c ---[ 299]---> Adder-cost: 454 maxlim: 358383 bits: 19/19 c ---[ 297]---> Adder-cost: 454 maxlim: 361455 bits: 19/19 c ---[ 295]---> Adder-cost: 458 maxlim: 413679 bits: 19/19 c ---[ 293]---> Adder-cost: 454 maxlim: 354287 bits: 19/19 c ---[ 291]---> Adder-cost: 384 maxlim: 66543 bits: 17/17 c ---[ 289]---> Adder-cost: 454 maxlim: 355311 bits: 19/19 c ---[ 288]---> BDD-cost: 16 c ---[ 287]---> BDD-cost: 15 c ---[ 286]---> BDD-cost: 15 c ---[ 285]---> BDD-cost: 17 c ---[ 284]---> BDD-cost: 20 c ---[ 283]---> BDD-cost: 20 c ---[ 282]---> BDD-cost: 15 c ---[ 281]---> BDD-cost: 14 c ---[ 280]---> BDD-cost: 18 c ---[ 279]---> BDD-cost: 19 c ---[ 278]---> BDD-cost: 20 c ---[ 277]---> BDD-cost: 20 c ---[ 276]---> BDD-cost: 20 c ---[ 275]---> BDD-cost: 14 c ---[ 274]---> BDD-cost: 14 c ---[ 273]---> BDD-cost: 20 c ---[ 272]---> BDD-cost: 15 c ---[ 271]---> BDD-cost: 14 c ---[ 270]---> BDD-cost: 18 c ---[ 269]---> BDD-cost: 16 c ---[ 268]---> BDD-cost: 16 c ---[ 267]---> BDD-cost: 20 c ---[ 266]---> BDD-cost: 20 c ---[ 265]---> BDD-cost: 20 c ---[ 264]---> BDD-cost: 16 c ---[ 263]---> BDD-cost: 15 c ---[ 262]---> BDD-cost: 14 c ---[ 261]---> BDD-cost: 20 c ---[ 260]---> BDD-cost: 20 c ---[ 259]---> BDD-cost: 20 c ---[ 258]---> BDD-cost: 20 c ---[ 257]---> BDD-cost: 20 c ---[ 256]---> BDD-cost: 14 c ---[ 255]---> BDD-cost: 20 c ---[ 254]---> BDD-cost: 15 c ---[ 253]---> BDD-cost: 16 c ---[ 252]---> BDD-cost: 14 c ---[ 251]---> BDD-cost: 18 c ---[ 250]---> BDD-cost: 16 c ---[ 249]---> BDD-cost: 16 c ---[ 248]---> BDD-cost: 20 c ---[ 247]---> BDD-cost: 20 c ---[ 246]---> BDD-cost: 16 c ---[ 245]---> BDD-cost: 16 c ---[ 244]---> BDD-cost: 14 c ---[ 243]---> BDD-cost: 16 c ---[ 242]---> BDD-cost: 16 c ---[ 241]---> BDD-cost: 16 c ---[ 240]---> BDD-cost: 16 c ---[ 239]---> BDD-cost: 16 c ---[ 238]---> BDD-cost: 16 c ---[ 237]---> BDD-cost: 14 c ---[ 236]---> BDD-cost: 16 c ---[ 235]---> BDD-cost: 16 c ---[ 234]---> BDD-cost: 14 c ---[ 233]---> BDD-cost: 16 c ---[ 232]---> BDD-cost: 16 c ---[ 231]---> BDD-cost: 16 c ---[ 230]---> BDD-cost: 16 c ---[ 229]---> BDD-cost: 16 c ---[ 228]---> BDD-cost: 16 c ---[ 227]---> BDD-cost: 14 c ---[ 226]---> BDD-cost: 14 c ---[ 225]---> BDD-cost: 14 c ---[ 224]---> BDD-cost: 14 c ---[ 223]---> BDD-cost: 14 c ---[ 222]---> BDD-cost: 14 c ---[ 221]---> BDD-cost: 14 c ---[ 220]---> BDD-cost: 16 c ---[ 219]---> BDD-cost: 14 c ---[ 218]---> BDD-cost: 14 c ---[ 217]---> BDD-cost: 14 c ---[ 216]---> BDD-cost: 14 c ---[ 215]---> BDD-cost: 14 c ---[ 214]---> BDD-cost: 14 c ---[ 213]---> BDD-cost: 14 c ---[ 212]---> BDD-cost: 14 c ---[ 211]---> BDD-cost: 14 c ---[ 210]---> BDD-cost: 14 c ---[ 209]---> BDD-cost: 15 c ---[ 208]---> BDD-cost: 17 c ---[ 207]---> BDD-cost: 15 c ---[ 206]---> BDD-cost: 14 c ---[ 205]---> BDD-cost: 17 c ---[ 204]---> BDD-cost: 17 c ---[ 203]---> BDD-cost: 17 c ---[ 202]---> BDD-cost: 17 c ---[ 201]---> BDD-cost: 17 c ---[ 200]---> BDD-cost: 14 c ---[ 199]---> BDD-cost: 17 c ---[ 198]---> BDD-cost: 15 c ---[ 197]---> BDD-cost: 15 c ---[ 196]---> BDD-cost: 14 c ---[ 195]---> BDD-cost: 17 c ---[ 194]---> BDD-cost: 17 c ---[ 193]---> BDD-cost: 16 c ---[ 192]---> BDD-cost: 17 c ---[ 191]---> BDD-cost: 17 c ---[ 190]---> BDD-cost: 17 c ---[ 189]---> BDD-cost: 15 c ---[ 188]---> BDD-cost: 14 c ---[ 187]---> BDD-cost: 14 c ---[ 186]---> BDD-cost: 17 c ---[ 185]---> BDD-cost: 17 c ---[ 184]---> BDD-cost: 17 c ---[ 183]---> BDD-cost: 17 c ---[ 182]---> BDD-cost: 17 c ---[ 181]---> BDD-cost: 14 c ---[ 180]---> BDD-cost: 17 c ---[ 179]---> BDD-cost: 15 c ---[ 178]---> BDD-cost: 14 c ---[ 177]---> BDD-cost: 17 c ---[ 176]---> BDD-cost: 14 c ---[ 175]---> BDD-cost: 15 c ---[ 174]---> BDD-cost: 17 c ---[ 173]---> BDD-cost: 17 c ---[ 172]---> BDD-cost: 17 c ---[ 171]---> BDD-cost: 17 c ---[ 170]---> BDD-cost: 20 c ---[ 169]---> BDD-cost: 15 c ---[ 168]---> BDD-cost: 14 c ---[ 167]---> BDD-cost: 18 c ---[ 166]---> BDD-cost: 19 c ---[ 165]---> BDD-cost: 20 c ---[ 164]---> BDD-cost: 15 c ---[ 163]---> BDD-cost: 18 c ---[ 162]---> BDD-cost: 18 c ---[ 161]---> BDD-cost: 14 c ---[ 160]---> BDD-cost: 18 c ---[ 159]---> BDD-cost: 15 c ---[ 158]---> BDD-cost: 14 c ---[ 157]---> BDD-cost: 18 c ---[ 156]---> BDD-cost: 16 c ---[ 155]---> BDD-cost: 16 c ---[ 154]---> BDD-cost: 18 c ---[ 153]---> BDD-cost: 15 c ---[ 152]---> BDD-cost: 20 c ---[ 151]---> BDD-cost: 18 c ---[ 150]---> BDD-cost: 15 c ---[ 149]---> BDD-cost: 14 c ---[ 148]---> BDD-cost: 18 c ---[ 147]---> BDD-cost: 18 c ---[ 146]---> BDD-cost: 18 c ---[ 145]---> BDD-cost: 18 c ---[ 144]---> BDD-cost: 18 c ---[ 143]---> BDD-cost: 14 c ---[ 142]---> BDD-cost: 15 c ---[ 141]---> BDD-cost: 18 c ---[ 140]---> BDD-cost: 15 c ---[ 139]---> BDD-cost: 14 c ---[ 138]---> BDD-cost: 18 c ---[ 137]---> BDD-cost: 18 c ---[ 136]---> BDD-cost: 18 c ---[ 135]---> BDD-cost: 18 c ---[ 134]---> BDD-cost: 18 c ---[ 133]---> BDD-cost: 15 c ---[ 132]---> BDD-cost: 15 c ---[ 131]---> BDD-cost: 15 c ---[ 130]---> BDD-cost: 14 c ---[ 129]---> BDD-cost: 15 c ---[ 128]---> BDD-cost: 15 c ---[ 127]---> BDD-cost: 15 c ---[ 126]---> BDD-cost: 15 c ---[ 125]---> BDD-cost: 15 c ---[ 124]---> BDD-cost: 14 c ---[ 123]---> BDD-cost: 15 c ---[ 122]---> BDD-cost: 15 c ---[ 121]---> BDD-cost: 14 c ---[ 120]---> BDD-cost: 14 c ---[ 119]---> BDD-cost: 15 c ---[ 118]---> BDD-cost: 15 c ---[ 117]---> BDD-cost: 15 c ---[ 116]---> BDD-cost: 15 c ---[ 115]---> BDD-cost: 15 c ---[ 114]---> BDD-cost: 20 c ---[ 113]---> BDD-cost: 15 c ---[ 112]---> BDD-cost: 14 c ---[ 111]---> BDD-cost: 18 c ---[ 110]---> BDD-cost: 19 c ---[ 109]---> BDD-cost: 15 c ---[ 108]---> BDD-cost: 20 c ---[ 107]---> BDD-cost: 18 c ---[ 106]---> BDD-cost: 18 c ---[ 105]---> BDD-cost: 14 c ---[ 104]---> BDD-cost: 18 c ---[ 103]---> BDD-cost: 15 c ---[ 102]---> BDD-cost: 14 c ---[ 101]---> BDD-cost: 18 c ---[ 100]---> BDD-cost: 16 c ---[ 99]---> BDD-cost: 16 c ---[ 98]---> BDD-cost: 15 c ---[ 97]---> BDD-cost: 18 c ---[ 96]---> BDD-cost: 20 c ---[ 95]---> BDD-cost: 20 c ---[ 94]---> BDD-cost: 15 c ---[ 93]---> BDD-cost: 14 c ---[ 92]---> BDD-cost: 18 c ---[ 91]---> BDD-cost: 19 c ---[ 90]---> BDD-cost: 20 c ---[ 89]---> BDD-cost: 22 c ---[ 88]---> BDD-cost: 19 c ---[ 87]---> BDD-cost: 14 c ---[ 86]---> BDD-cost: 14 c ---[ 85]---> BDD-cost: 20 c ---[ 84]---> BDD-cost: 15 c ---[ 83]---> BDD-cost: 14 c ---[ 82]---> BDD-cost: 18 c ---[ 81]---> BDD-cost: 16 c ---[ 80]---> BDD-cost: 16 c ---[ 79]---> BDD-cost: 22 c ---[ 78]---> BDD-cost: 20 c ---[ 77]---> BDD-cost: 15 c ---[ 76]---> BDD-cost: 16 c ---[ 75]---> BDD-cost: 15 c ---[ 74]---> BDD-cost: 15 c ---[ 73]---> BDD-cost: 15 c ---[ 72]---> BDD-cost: 15 c ---[ 71]---> BDD-cost: 20 c ---[ 70]---> BDD-cost: 15 c ---[ 69]---> BDD-cost: 14 c ---[ 68]---> BDD-cost: 18 c ---[ 67]---> BDD-cost: 20 c ---[ 66]---> BDD-cost: 20 c ---[ 65]---> BDD-cost: 16 c ---[ 64]---> BDD-cost: 20 c ---[ 63]---> BDD-cost: 20 c ---[ 62]---> BDD-cost: 14 c ---[ 61]---> BDD-cost: 20 c ---[ 60]---> BDD-cost: 15 c ---[ 59]---> BDD-cost: 14 c ---[ 58]---> BDD-cost: 18 c ---[ 57]---> BDD-cost: 16 c ---[ 56]---> BDD-cost: 16 c ---[ 55]---> BDD-cost: 20 c ---[ 54]---> BDD-cost: 16 c ---[ 53]---> BDD-cost: 20 c ---[ 52]---> BDD-cost: 20 c ---[ 51]---> BDD-cost: 15 c ---[ 50]---> BDD-cost: 14 c ---[ 49]---> BDD-cost: 18 c ---[ 48]---> BDD-cost: 20 c ---[ 47]---> BDD-cost: 20 c ---[ 46]---> BDD-cost: 20 c ---[ 45]---> BDD-cost: 20 c ---[ 44]---> BDD-cost: 14 c ---[ 43]---> BDD-cost: 16 c ---[ 42]---> BDD-cost: 20 c ---[ 41]---> BDD-cost: 15 c ---[ 40]---> BDD-cost: 14 c ---[ 39]---> BDD-cost: 18 c ---[ 38]---> BDD-cost: 16 c ---[ 37]---> BDD-cost: 16 c ---[ 36]---> BDD-cost: 20 c ---[ 35]---> BDD-cost: 20 c ---[ 34]---> BDD-cost: 18 c ---[ 33]---> BDD-cost: 15 c ---[ 32]---> BDD-cost: 16 c ---[ 31]---> BDD-cost: 14 c ---[ 30]---> BDD-cost: 18 c ---[ 29]---> BDD-cost: 18 c ---[ 28]---> BDD-cost: 18 c ---[ 27]---> BDD-cost: 18 c ---[ 26]---> BDD-cost: 18 c ---[ 25]---> BDD-cost: 14 c ---[ 24]---> BDD-cost: 18 c ---[ 23]---> BDD-cost: 15 c ---[ 22]---> BDD-cost: 14 c ---[ 21]---> BDD-cost: 14 c ---[ 20]---> BDD-cost: 18 c ---[ 19]---> BDD-cost: 18 c ---[ 18]---> BDD-cost: 16 c ---[ 17]---> BDD-cost: 18 c ---[ 16]---> BDD-cost: 18 c ---[ 15]---> BDD-cost: 20 c ---[ 14]---> BDD-cost: 15 c ---[ 13]---> BDD-cost: 14 c ---[ 12]---> BDD-cost: 18 c ---[ 11]---> BDD-cost: 19 c ---[ 10]---> BDD-cost: 16 c ---[ 9]---> BDD-cost: 20 c ---[ 8]---> BDD-cost: 17 c ---[ 7]---> BDD-cost: 19 c ---[ 6]---> BDD-cost: 14 c ---[ 5]---> BDD-cost: 20 c ---[ 4]---> BDD-cost: 15 c ---[ 3]---> BDD-cost: 14 c ---[ 2]---> BDD-cost: 18 c ---[ 1]---> BDD-cost: 16 c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 107120 373762 | 35706 0 0 nan | 0.000 % | c | 100 | 107100 373698 | 39276 97 294 3.0 | 24.108 % | c | 250 | 107028 373454 | 43204 240 734 3.1 | 24.154 % | c | 475 | 106953 373203 | 47524 456 1409 3.1 | 24.209 % | c | 812 | 106790 372654 | 52277 775 2429 3.1 | 24.321 % | c | 1318 | 106452 371492 | 57504 1236 3949 3.2 | 24.545 % | c | 2077 | 106112 370344 | 63255 1953 6262 3.2 | 24.770 % | c | 3216 | 105544 368374 | 69580 3004 9729 3.2 | 25.149 % | c | 4924 | 105009 366565 | 76538 4651 15690 3.4 | 25.517 % | c | 7486 | 104718 365580 | 84192 7175 25679 3.6 | 25.714 % | c | 11331 | 104664 365400 | 92612 11013 42539 3.9 | 25.749 % | c | 17097 | 104655 365371 | 101873 16778 75481 4.5 | 25.757 % | c | 25746 | 104647 365345 | 112060 25426 220907 8.7 | 25.761 % | c | 38720 | 104647 365345 | 123266 38400 577326 15.0 | 25.761 % | c | 58182 | 104647 365345 | 135593 57862 1113303 19.2 | 25.761 % | c | 87375 | 104622 365260 | 149152 87051 2616975 30.1 | 25.776 % | c | 131165 | 104391 364461 | 164068 130808 7183223 54.9 | 25.927 % | c | 196849 | 104045 363277 | 180474 51454 1171711 22.8 | 26.175 % | c | 295375 | 103774 362344 | 198522 149945 7411888 49.4 | 26.368 % | c | 443164 | 103578 361664 | 218374 103061 4269302 41.4 | 26.511 % | c | 664848 | 103310 360772 | 240212 127704 4047362 31.7 | 26.709 % | c | 997374 | 103004 359762 | 264233 238982 11736812 49.1 | 26.937 % |
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/26709/stat): 26709 (minisat+_script) R 26708 26709 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854541881 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/26709/statm): 174 3 169 147 0 27 0 [pid=26709] 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=26710 New process pid=26711 New process pid=26712 execve syscall for /bin/sed executable One traced child (pid=26711) 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=26712) exited with status: 0 One traced child (pid=26710) exited with status: 0 New process pid=26713 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-ran17x17.opb [startup+10.0041 s] Raw data (loadavg): 0.57 0.59 0.74 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2650 0 0 0 972 13 0 0 25 0 1 0 1854541886 11206656 2490 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 2736 2490 145 145 0 2591 0 [pid=26713] vsize: 10944 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 13068 [startup+20.005 s] Raw data (loadavg): 0.64 0.60 0.74 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2668 0 0 0 1972 13 0 0 25 0 1 0 1854541886 11284480 2508 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 2755 2508 145 145 0 2610 0 [pid=26713] vsize: 11020 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 13144 [startup+30.0058 s] Raw data (loadavg): 0.69 0.62 0.74 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2694 0 0 0 2971 14 0 0 25 0 1 0 1854541886 11378688 2534 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 2778 2534 145 145 0 2633 0 [pid=26713] vsize: 11112 Current children cumulated CPU time (s) 29.87 Current children cumulated vsize (Kb) 13236 [startup+40.0066 s] Raw data (loadavg): 0.74 0.63 0.75 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2722 0 0 0 3970 15 0 0 25 0 1 0 1854541886 11505664 2562 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 2809 2562 145 145 0 2664 0 [pid=26713] vsize: 11236 Current children cumulated CPU time (s) 39.87 Current children cumulated vsize (Kb) 13360 [startup+50.0085 s] Raw data (loadavg): 0.78 0.64 0.75 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2761 0 0 0 4969 15 0 0 25 0 1 0 1854541886 11649024 2601 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 2844 2601 145 145 0 2699 0 [pid=26713] vsize: 11376 Current children cumulated CPU time (s) 49.86 Current children cumulated vsize (Kb) 13500 [startup+60.0103 s] Raw data (loadavg): 0.81 0.65 0.75 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 2818 0 0 0 5968 16 0 0 25 0 1 0 1854541886 11927552 2658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 2912 2658 145 145 0 2767 0 [pid=26713] vsize: 11648 Current children cumulated CPU time (s) 59.86 Current children cumulated vsize (Kb) 13772 [startup+70.0111 s] Raw data (loadavg): 0.84 0.66 0.75 1/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) T 26709 26709 28974 0 -1 0 3695 0 0 0 6956 22 0 0 25 0 1 0 1854541886 15556608 3535 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26713/statm): 3798 3535 145 145 0 3653 0 [pid=26713] vsize: 15192 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 17316 [startup+80.0119 s] Raw data (loadavg): 0.86 0.67 0.75 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 4352 0 0 0 7946 26 0 0 25 0 1 0 1854541886 18182144 4192 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 4439 4192 145 145 0 4294 0 [pid=26713] vsize: 17756 Current children cumulated CPU time (s) 79.74 Current children cumulated vsize (Kb) 19880 [startup+90.0128 s] Raw data (loadavg): 0.88 0.68 0.76 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 5760 0 0 0 8927 34 0 0 25 0 1 0 1854541886 24125440 5600 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 5890 5600 145 145 0 5745 0 [pid=26713] vsize: 23560 Current children cumulated CPU time (s) 89.63 Current children cumulated vsize (Kb) 25684 [startup+100.014 s] Raw data (loadavg): 0.90 0.69 0.76 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 7739 0 0 0 9898 44 0 0 25 0 1 0 1854541886 32174080 7579 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 7855 7579 145 145 0 7710 0 [pid=26713] vsize: 31420 Current children cumulated CPU time (s) 99.44 Current children cumulated vsize (Kb) 33544 [startup+110.015 s] Raw data (loadavg): 0.92 0.70 0.76 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 9053 0 0 0 10881 52 0 0 25 0 1 0 1854541886 37490688 8893 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 9153 8893 145 145 0 9008 0 [pid=26713] vsize: 36612 Current children cumulated CPU time (s) 109.35 Current children cumulated vsize (Kb) 38736 [startup+120.016 s] Raw data (loadavg): 0.93 0.71 0.76 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 10622 0 0 0 11857 63 0 0 25 0 1 0 1854541886 43896832 10462 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 10717 10462 145 145 0 10572 0 [pid=26713] vsize: 42868 Current children cumulated CPU time (s) 119.22 Current children cumulated vsize (Kb) 44992 [startup+130.016 s] Raw data (loadavg): 0.94 0.72 0.76 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11184 0 0 0 12848 66 0 0 25 0 1 0 1854541886 46206976 11024 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 11281 11024 145 145 0 11136 0 [pid=26713] vsize: 45124 Current children cumulated CPU time (s) 129.16 Current children cumulated vsize (Kb) 47248 [startup+140.017 s] Raw data (loadavg): 0.95 0.73 0.77 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11331 0 0 0 13846 68 0 0 25 0 1 0 1854541886 47316992 11171 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 11552 11171 145 145 0 11407 0 [pid=26713] vsize: 46208 Current children cumulated CPU time (s) 139.16 Current children cumulated vsize (Kb) 48332 [startup+150.018 s] Raw data (loadavg): 0.96 0.74 0.77 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11464 0 0 0 14844 68 0 0 25 0 1 0 1854541886 47837184 11304 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 11679 11304 145 145 0 11534 0 [pid=26713] vsize: 46716 Current children cumulated CPU time (s) 149.14 Current children cumulated vsize (Kb) 48840 [startup+160.019 s] Raw data (loadavg): 0.96 0.75 0.77 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11619 0 0 0 15841 70 0 0 25 0 1 0 1854541886 48447488 11459 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 11828 11459 145 145 0 11683 0 [pid=26713] vsize: 47312 Current children cumulated CPU time (s) 159.13 Current children cumulated vsize (Kb) 49436 [startup+170.02 s] Raw data (loadavg): 0.97 0.75 0.77 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 11841 0 0 0 16837 71 0 0 25 0 1 0 1854541886 49328128 11681 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12043 11681 145 145 0 11898 0 [pid=26713] vsize: 48172 Current children cumulated CPU time (s) 169.1 Current children cumulated vsize (Kb) 50296 [startup+180.021 s] Raw data (loadavg): 0.97 0.76 0.77 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12064 0 0 0 17833 73 0 0 25 0 1 0 1854541886 50216960 11904 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12260 11904 145 145 0 12115 0 [pid=26713] vsize: 49040 Current children cumulated CPU time (s) 179.08 Current children cumulated vsize (Kb) 51164 [startup+190.022 s] Raw data (loadavg): 0.98 0.77 0.78 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12201 0 0 0 18831 74 0 0 25 0 1 0 1854541886 50753536 12041 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12391 12041 145 145 0 12246 0 [pid=26713] vsize: 49564 Current children cumulated CPU time (s) 189.07 Current children cumulated vsize (Kb) 51688 [startup+200.023 s] Raw data (loadavg): 0.98 0.78 0.78 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12353 0 0 0 19828 75 0 0 25 0 1 0 1854541886 51355648 12193 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12538 12193 145 145 0 12393 0 [pid=26713] vsize: 50152 Current children cumulated CPU time (s) 199.05 Current children cumulated vsize (Kb) 52276 [startup+210.024 s] Raw data (loadavg): 0.98 0.78 0.78 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 20825 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 209.03 Current children cumulated vsize (Kb) 52896 [startup+220.024 s] Raw data (loadavg): 0.98 0.79 0.78 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 21825 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 219.03 Current children cumulated vsize (Kb) 52896 [startup+230.025 s] Raw data (loadavg): 0.99 0.80 0.78 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 22826 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 229.04 Current children cumulated vsize (Kb) 52896 [startup+240.026 s] Raw data (loadavg): 0.99 0.80 0.79 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 23826 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 239.04 Current children cumulated vsize (Kb) 52896 [startup+250.026 s] Raw data (loadavg): 0.99 0.81 0.79 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 24826 76 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 249.04 Current children cumulated vsize (Kb) 52896 [startup+260.028 s] Raw data (loadavg): 0.99 0.81 0.79 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 25825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 259.04 Current children cumulated vsize (Kb) 52896 [startup+270.029 s] Raw data (loadavg): 0.99 0.82 0.79 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 26825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 269.04 Current children cumulated vsize (Kb) 52896 [startup+280.028 s] Raw data (loadavg): 0.99 0.83 0.79 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 27825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 279.04 Current children cumulated vsize (Kb) 52896 [startup+290.03 s] Raw data (loadavg): 0.99 0.83 0.80 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 28825 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 289.04 Current children cumulated vsize (Kb) 52896 [startup+300.031 s] Raw data (loadavg): 0.99 0.84 0.80 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 29826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 299.05 Current children cumulated vsize (Kb) 52896 [startup+310.032 s] Raw data (loadavg): 0.99 0.84 0.80 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 30826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134550387 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 309.05 Current children cumulated vsize (Kb) 52896 [startup+320.033 s] Raw data (loadavg): 0.99 0.85 0.80 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 31826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 319.05 Current children cumulated vsize (Kb) 52896 [startup+330.033 s] Raw data (loadavg): 0.99 0.85 0.80 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 32826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 329.05 Current children cumulated vsize (Kb) 52896 [startup+340.034 s] Raw data (loadavg): 0.99 0.85 0.81 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 33826 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 339.05 Current children cumulated vsize (Kb) 52896 [startup+350.035 s] Raw data (loadavg): 0.99 0.86 0.81 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 34827 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 349.06 Current children cumulated vsize (Kb) 52896 [startup+360.037 s] Raw data (loadavg): 0.99 0.86 0.81 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12513 0 0 0 35827 77 0 0 25 0 1 0 1854541886 51990528 12353 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12693 12353 145 145 0 12548 0 [pid=26713] vsize: 50772 Current children cumulated CPU time (s) 359.06 Current children cumulated vsize (Kb) 52896 [startup+370.038 s] Raw data (loadavg): 0.99 0.87 0.81 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 12742 0 0 0 36824 79 0 0 25 0 1 0 1854541886 52928512 12582 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 12922 12582 145 145 0 12777 0 [pid=26713] vsize: 51688 Current children cumulated CPU time (s) 369.05 Current children cumulated vsize (Kb) 53812 [startup+380.038 s] Raw data (loadavg): 0.99 0.87 0.81 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 13511 0 0 0 37813 83 0 0 25 0 1 0 1854541886 56078336 13351 4294967295 134512640 135094434 3221224432 3221223088 134561766 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 13691 13351 145 145 0 13546 0 [pid=26713] vsize: 54764 Current children cumulated CPU time (s) 378.98 Current children cumulated vsize (Kb) 56888 [startup+390.038 s] Raw data (loadavg): 0.99 0.87 0.81 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 13866 0 0 0 38807 86 0 0 25 0 1 0 1854541886 57524224 13706 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 14044 13706 145 145 0 13899 0 [pid=26713] vsize: 56176 Current children cumulated CPU time (s) 388.95 Current children cumulated vsize (Kb) 58300 [startup+400.039 s] Raw data (loadavg): 0.99 0.88 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 14272 0 0 0 39800 90 0 0 25 0 1 0 1854541886 59154432 14112 4294967295 134512640 135094434 3221224432 3221223100 134553438 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 14442 14112 145 145 0 14297 0 [pid=26713] vsize: 57768 Current children cumulated CPU time (s) 398.92 Current children cumulated vsize (Kb) 59892 [startup+410.041 s] Raw data (loadavg): 0.99 0.88 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 14418 0 0 0 40797 91 0 0 25 0 1 0 1854541886 59731968 14258 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 14583 14258 145 145 0 14438 0 [pid=26713] vsize: 58332 Current children cumulated CPU time (s) 408.9 Current children cumulated vsize (Kb) 60456 [startup+420.042 s] Raw data (loadavg): 0.99 0.89 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 15215 0 0 0 41784 97 0 0 25 0 1 0 1854541886 62959616 15055 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 15371 15055 145 145 0 15226 0 [pid=26713] vsize: 61484 Current children cumulated CPU time (s) 418.83 Current children cumulated vsize (Kb) 63608 [startup+430.043 s] Raw data (loadavg): 0.99 0.89 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16314 0 0 0 42767 104 0 0 25 0 1 0 1854541886 67473408 16154 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16473 16154 145 145 0 16328 0 [pid=26713] vsize: 65892 Current children cumulated CPU time (s) 428.73 Current children cumulated vsize (Kb) 68016 [startup+440.044 s] Raw data (loadavg): 0.99 0.89 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 43762 107 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 438.71 Current children cumulated vsize (Kb) 69184 [startup+450.044 s] Raw data (loadavg): 0.99 0.89 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 44762 107 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 448.71 Current children cumulated vsize (Kb) 69184 [startup+460.046 s] Raw data (loadavg): 0.99 0.90 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 45762 108 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223104 134554886 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 458.72 Current children cumulated vsize (Kb) 69184 [startup+470.048 s] Raw data (loadavg): 0.99 0.90 0.82 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 46761 108 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 468.71 Current children cumulated vsize (Kb) 69184 [startup+480.049 s] Raw data (loadavg): 0.99 0.90 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 47761 108 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 478.71 Current children cumulated vsize (Kb) 69184 [startup+490.051 s] Raw data (loadavg): 0.99 0.91 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 48760 109 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 488.71 Current children cumulated vsize (Kb) 69184 [startup+500.051 s] Raw data (loadavg): 0.99 0.91 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 49760 110 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 498.72 Current children cumulated vsize (Kb) 69184 [startup+510.052 s] Raw data (loadavg): 0.99 0.91 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 50759 110 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223024 134556724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 508.71 Current children cumulated vsize (Kb) 69184 [startup+520.053 s] Raw data (loadavg): 0.99 0.91 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 51759 111 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 518.72 Current children cumulated vsize (Kb) 69184 [startup+530.054 s] Raw data (loadavg): 0.99 0.92 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 52758 112 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 528.72 Current children cumulated vsize (Kb) 69184 [startup+540.056 s] Raw data (loadavg): 0.99 0.92 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 53758 112 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 538.72 Current children cumulated vsize (Kb) 69184 [startup+550.057 s] Raw data (loadavg): 0.99 0.92 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 54758 113 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 548.73 Current children cumulated vsize (Kb) 69184 [startup+560.057 s] Raw data (loadavg): 0.99 0.92 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 55757 113 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 558.72 Current children cumulated vsize (Kb) 69184 [startup+570.058 s] Raw data (loadavg): 0.99 0.92 0.83 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 56757 114 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 568.73 Current children cumulated vsize (Kb) 69184 [startup+580.059 s] Raw data (loadavg): 0.99 0.93 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16609 0 0 0 57756 114 0 0 25 0 1 0 1854541886 68669440 16449 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16449 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 578.72 Current children cumulated vsize (Kb) 69184 [startup+590.061 s] Raw data (loadavg): 0.99 0.93 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 58756 115 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 588.73 Current children cumulated vsize (Kb) 69184 [startup+600.062 s] Raw data (loadavg): 0.99 0.93 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 59756 115 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 598.73 Current children cumulated vsize (Kb) 69184 [startup+610.064 s] Raw data (loadavg): 0.99 0.93 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 60755 116 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 608.73 Current children cumulated vsize (Kb) 69184 [startup+620.064 s] Raw data (loadavg): 0.99 0.93 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 61755 117 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 618.74 Current children cumulated vsize (Kb) 69184 [startup+630.065 s] Raw data (loadavg): 0.99 0.94 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 62754 117 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 628.73 Current children cumulated vsize (Kb) 69184 [startup+640.067 s] Raw data (loadavg): 0.99 0.94 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 63754 118 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 638.74 Current children cumulated vsize (Kb) 69184 [startup+650.068 s] Raw data (loadavg): 0.99 0.94 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 64754 118 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 648.74 Current children cumulated vsize (Kb) 69184 [startup+660.069 s] Raw data (loadavg): 0.99 0.94 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 65753 118 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 658.73 Current children cumulated vsize (Kb) 69184 [startup+670.069 s] Raw data (loadavg): 0.99 0.94 0.84 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 66753 119 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 668.74 Current children cumulated vsize (Kb) 69184 [startup+680.07 s] Raw data (loadavg): 0.99 0.94 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 67753 119 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 678.74 Current children cumulated vsize (Kb) 69184 [startup+690.071 s] Raw data (loadavg): 0.99 0.94 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16610 0 0 0 68753 119 0 0 25 0 1 0 1854541886 68669440 16450 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16450 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 688.74 Current children cumulated vsize (Kb) 69184 [startup+700.072 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16619 0 0 0 69753 119 0 0 25 0 1 0 1854541886 68669440 16459 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16459 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 698.74 Current children cumulated vsize (Kb) 69184 [startup+710.074 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 70754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 708.75 Current children cumulated vsize (Kb) 69184 [startup+720.075 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 71754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 718.75 Current children cumulated vsize (Kb) 69184 [startup+730.075 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 72754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223072 134562082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 728.75 Current children cumulated vsize (Kb) 69184 [startup+740.076 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 73754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 738.75 Current children cumulated vsize (Kb) 69184 [startup+750.077 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 74754 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223120 134554824 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 748.75 Current children cumulated vsize (Kb) 69184 [startup+760.079 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 75755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 758.76 Current children cumulated vsize (Kb) 69184 [startup+770.08 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 76755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 768.76 Current children cumulated vsize (Kb) 69184 [startup+780.081 s] Raw data (loadavg): 0.99 0.95 0.85 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 77755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 778.76 Current children cumulated vsize (Kb) 69184 [startup+790.081 s] Raw data (loadavg): 0.99 0.95 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 78755 119 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 788.76 Current children cumulated vsize (Kb) 69184 [startup+800.082 s] Raw data (loadavg): 0.99 0.95 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 79755 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 798.77 Current children cumulated vsize (Kb) 69184 [startup+810.083 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 80755 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 808.77 Current children cumulated vsize (Kb) 69184 [startup+820.084 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 81755 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223024 134551967 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 818.77 Current children cumulated vsize (Kb) 69184 [startup+830.085 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 82756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 828.78 Current children cumulated vsize (Kb) 69184 [startup+840.085 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 83756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134558167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 838.78 Current children cumulated vsize (Kb) 69184 [startup+850.086 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 84756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 848.78 Current children cumulated vsize (Kb) 69184 [startup+860.087 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 16624 0 0 0 85756 120 0 0 25 0 1 0 1854541886 68669440 16464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 16765 16464 145 145 0 16620 0 [pid=26713] vsize: 67060 Current children cumulated CPU time (s) 858.78 Current children cumulated vsize (Kb) 69184 [startup+870.088 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17104 0 0 0 86750 122 0 0 25 0 1 0 1854541886 70651904 16944 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 17249 16944 145 145 0 17104 0 [pid=26713] vsize: 68996 Current children cumulated CPU time (s) 868.74 Current children cumulated vsize (Kb) 71120 [startup+880.089 s] Raw data (loadavg): 0.99 0.96 0.86 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17241 0 0 0 87748 124 0 0 25 0 1 0 1854541886 71225344 17081 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 17389 17081 145 145 0 17244 0 [pid=26713] vsize: 69556 Current children cumulated CPU time (s) 878.74 Current children cumulated vsize (Kb) 71680 [startup+890.09 s] Raw data (loadavg): 0.99 0.96 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17363 0 0 0 88746 124 0 0 25 0 1 0 1854541886 71733248 17203 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 17513 17203 145 145 0 17368 0 [pid=26713] vsize: 70052 Current children cumulated CPU time (s) 888.72 Current children cumulated vsize (Kb) 72176 [startup+900.09 s] Raw data (loadavg): 0.99 0.96 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17538 0 0 0 89743 125 0 0 25 0 1 0 1854541886 72450048 17378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 17688 17378 145 145 0 17543 0 [pid=26713] vsize: 70752 Current children cumulated CPU time (s) 898.7 Current children cumulated vsize (Kb) 72876 [startup+910.092 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 17733 0 0 0 90741 127 0 0 25 0 1 0 1854541886 73236480 17573 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 17880 17573 145 145 0 17735 0 [pid=26713] vsize: 71520 Current children cumulated CPU time (s) 908.7 Current children cumulated vsize (Kb) 73644 [startup+920.093 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18031 0 0 0 91735 128 0 0 25 0 1 0 1854541886 74428416 17871 4294967295 134512640 135094434 3221224432 3221223088 134557820 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18171 17871 145 145 0 18026 0 [pid=26713] vsize: 72684 Current children cumulated CPU time (s) 918.65 Current children cumulated vsize (Kb) 74808 [startup+930.093 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18373 0 0 0 92729 130 0 0 25 0 1 0 1854541886 75796480 18213 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18505 18213 145 145 0 18360 0 [pid=26713] vsize: 74020 Current children cumulated CPU time (s) 928.61 Current children cumulated vsize (Kb) 76144 [startup+940.095 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 93728 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 938.61 Current children cumulated vsize (Kb) 76472 [startup+950.095 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 94728 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 948.61 Current children cumulated vsize (Kb) 76472 [startup+960.096 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 95729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 958.62 Current children cumulated vsize (Kb) 76472 [startup+970.097 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 96729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 968.62 Current children cumulated vsize (Kb) 76472 [startup+980.097 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 97729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 978.62 Current children cumulated vsize (Kb) 76472 [startup+990.098 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 98729 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134550389 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 988.62 Current children cumulated vsize (Kb) 76472 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 99730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 998.63 Current children cumulated vsize (Kb) 76472 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 100730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1008.63 Current children cumulated vsize (Kb) 76472 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 101730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1018.63 Current children cumulated vsize (Kb) 76472 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 102730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1028.63 Current children cumulated vsize (Kb) 76472 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 103730 131 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1038.63 Current children cumulated vsize (Kb) 76472 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 104730 132 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1048.64 Current children cumulated vsize (Kb) 76472 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 105729 133 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1058.64 Current children cumulated vsize (Kb) 76472 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 106729 133 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1068.64 Current children cumulated vsize (Kb) 76472 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 107729 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1078.65 Current children cumulated vsize (Kb) 76472 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 108730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1088.66 Current children cumulated vsize (Kb) 76472 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 109729 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1098.65 Current children cumulated vsize (Kb) 76472 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 110729 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1108.65 Current children cumulated vsize (Kb) 76472 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 111730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1118.66 Current children cumulated vsize (Kb) 76472 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 112730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223024 134551918 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1128.66 Current children cumulated vsize (Kb) 76472 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 18457 0 0 0 113730 134 0 0 25 0 1 0 1854541886 76132352 18297 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 18587 18297 145 145 0 18442 0 [pid=26713] vsize: 74348 Current children cumulated CPU time (s) 1138.66 Current children cumulated vsize (Kb) 76472 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 19245 0 0 0 114716 140 0 0 25 0 1 0 1854541886 79368192 19085 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 19377 19085 145 145 0 19232 0 [pid=26713] vsize: 77508 Current children cumulated CPU time (s) 1148.58 Current children cumulated vsize (Kb) 79632 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 19921 0 0 0 115704 145 0 0 25 0 1 0 1854541886 82169856 19761 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 20061 19761 145 145 0 19916 0 [pid=26713] vsize: 80244 Current children cumulated CPU time (s) 1158.51 Current children cumulated vsize (Kb) 82368 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20129 0 0 0 116702 146 0 0 25 0 1 0 1854541886 83021824 19969 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 20269 19969 145 145 0 20124 0 [pid=26713] vsize: 81076 Current children cumulated CPU time (s) 1168.5 Current children cumulated vsize (Kb) 83200 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20352 0 0 0 117699 147 0 0 25 0 1 0 1854541886 83935232 20192 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26713/statm): 20492 20192 145 145 0 20347 0 [pid=26713] vsize: 81968 Current children cumulated CPU time (s) 1178.48 Current children cumulated vsize (Kb) 84092 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20461 0 0 0 118696 148 0 0 25 0 1 0 1854541886 84389888 20301 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 20603 20301 145 145 0 20458 0 [pid=26713] vsize: 82412 Current children cumulated CPU time (s) 1188.46 Current children cumulated vsize (Kb) 84536 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20624 0 0 0 119693 149 0 0 25 0 1 0 1854541886 85045248 20464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 20763 20464 145 145 0 20618 0 [pid=26713] vsize: 83052 Current children cumulated CPU time (s) 1198.44 Current children cumulated vsize (Kb) 85176 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20934 0 0 0 120688 152 0 0 25 0 1 0 1854541886 86282240 20774 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 21065 20774 145 145 0 20920 0 [pid=26713] vsize: 84260 Current children cumulated CPU time (s) 1208.42 Current children cumulated vsize (Kb) 86384 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 26713 Raw data (/proc/26709/stat): 26709 (minisat+_script) S 26708 26709 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1854541881 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26709/statm): 531 226 485 147 0 384 0 [pid=26709] vsize: 2124 Raw data (/proc/26713/stat): 26713 (minisat+_64-bit) R 26709 26709 28974 0 -1 0 20934 0 0 0 120688 152 0 0 25 0 1 0 1854541886 86282240 20774 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26713/statm): 21065 20774 145 145 0 20920 0 [pid=26713] vsize: 84260 Current children cumulated CPU time (s) 1208.42 Current children cumulated vsize (Kb) 86384 Sending SIGTERM to -26709 Sleeping 2 seconds One traced child (pid=26709) ended because it received signal 15 (SIGTERM) One traced child (pid=26713) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.16 CPU time (s): 1208.45 CPU user time (s): 1206.88 CPU system time (s): 1.56276 CPU usage (%): 99.858 Max. virtual memory (cumulated for all children) (Kb): 86384
ERROR: no interpretation found !