Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-dcmulti.opb |
MD5SUM | 28123830d5f7e3646d18978bb347487c |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 9505 |
Biggest coefficient in the objective function | 697303040 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 66656504525 |
Number of bits of the sum of numbers in the objective function | 36 |
Biggest number in a constraint | 697303040 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 66656504525 |
Number of bits of the biggest sum of numbers | 36 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 9535 |
Total number of constraints | 365 |
Number of constraints which are clauses | 27 |
Number of constraints which are cardinality constraints (but not clauses) | 80 |
Number of constraints which are nor clauses,nor cardinality constraints | 258 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 280 |
LAUNCH ON wulflinc31 THE 2005-09-20 04:13:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3351 boxname=wulflinc31 idbench=1007 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 28123830d5f7e3646d18978bb347487c /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb IDLAUNCH: 3351 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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.153 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 921344 kB Buffers: 7212 kB Cached: 78444 kB SwapCached: 1180 kB Active: 14388 kB Inactive: 74016 kB HighTotal: 131008 kB HighFree: 49644 kB LowTotal: 903652 kB LowFree: 871700 kB SwapTotal: 2097892 kB SwapFree: 2096228 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5672 kB Slab: 19332 kB Committed_AS: 64340 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:33:34 (client local time) WITH STATUS 0 IN 1206.77 SECONDS stats: 3351 7 1206.77 0
c Parsing PB file... c Converting 368 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################################################################## c -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss c ---[ 427]---> BDD-cost: 14 c ---[ 426]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 425]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 424]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 422]---> BDD-cost: 15 c ---[ 421]---> BDD-cost: 14 c ---[ 420]---> BDD-cost: 14 c ---[ 419]---> BDD-cost: 13 c ---[ 418]---> BDD-cost: 14 c ---[ 416]---> Adder-cost: 445 maxlim: 262140 bits: 19/18 c ---[ 415]---> BDD-cost: 14 c ---[ 413]---> Adder-cost: 445 maxlim: 212988 bits: 19/18 c ---[ 411]---> Adder-cost: 445 maxlim: 262140 bits: 19/18 c ---[ 409]---> Adder-cost: 445 maxlim: 212988 bits: 19/18 c ---[ 407]---> Adder-cost: 445 maxlim: 262140 bits: 19/18 c ---[ 405]---> Adder-cost: 445 maxlim: 212988 bits: 19/18 c ---[ 403]---> Adder-cost: 445 maxlim: 262140 bits: 19/18 c ---[ 401]---> Adder-cost: 445 maxlim: 212988 bits: 19/18 c ---[ 399]---> Adder-cost: 445 maxlim: 262140 bits: 19/18 c ---[ 397]---> Adder-cost: 445 maxlim: 212988 bits: 19/18 c ---[ 395]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 394]---> BDD-cost: 13 c ---[ 392]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 391]---> BDD-cost: 16 c ---[ 390]---> BDD-cost: 7 c ---[ 389]---> BDD-cost: 15 c ---[ 388]---> BDD-cost: 4 c ---[ 386]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 385]---> BDD-cost: 24 c ---[ 384]---> BDD-cost: 6 c ---[ 381]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 380]---> BDD-cost: 14 c ---[ 378]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 377]---> BDD-cost: 16 c ---[ 376]---> BDD-cost: 7 c ---[ 375]---> BDD-cost: 15 c ---[ 374]---> BDD-cost: 4 c ---[ 372]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> BDD-cost: 23 c ---[ 370]---> BDD-cost: 8 c ---[ 367]---> Sorter-cost: 915 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 365]---> Adder-cost: 391 maxlim: 131069 bits: 18/17 c ---[ 363]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 362]---> BDD-cost: 15 c ---[ 361]---> BDD-cost: 6 c ---[ 360]---> BDD-cost: 14 c ---[ 359]---> BDD-cost: 3 c ---[ 357]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 356]---> BDD-cost: 23 c ---[ 355]---> BDD-cost: 6 c ---[ 352]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Adder-cost: 391 maxlim: 81917 bits: 18/17 c ---[ 348]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 347]---> BDD-cost: 16 c ---[ 346]---> BDD-cost: 7 c ---[ 345]---> BDD-cost: 15 c ---[ 344]---> BDD-cost: 4 c ---[ 342]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 341]---> BDD-cost: 24 c ---[ 340]---> BDD-cost: 6 c ---[ 337]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 335]---> Adder-cost: 391 maxlim: 131069 bits: 18/17 c ---[ 333]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 332]---> BDD-cost: 16 c ---[ 331]---> BDD-cost: 7 c ---[ 330]---> BDD-cost: 15 c ---[ 329]---> BDD-cost: 4 c ---[ 327]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> BDD-cost: 19 c ---[ 322]---> BDD-cost: 33 c ---[ 320]---> Adder-cost: 391 maxlim: 81917 bits: 18/17 c ---[ 308]---> Adder-cost: 391 maxlim: 131069 bits: 18/17 c ---[ 296]---> Adder-cost: 391 maxlim: 81917 bits: 18/17 c ---[ 293]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 292]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 291]---> Sorter-cost: 1290 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 290]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 289]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 288]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 286]---> BDD-cost: 15 c ---[ 285]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 283]---> Adder-cost: 391 maxlim: 131069 bits: 18/17 c ---[ 282]---> BDD-cost: 14 c ---[ 281]---> BDD-cost: 14 c ---[ 280]---> BDD-cost: 13 c ---[ 279]---> BDD-cost: 14 c ---[ 277]---> Adder-cost: 428 maxlim: 393212 bits: 20/19 c ---[ 275]---> Adder-cost: 428 maxlim: 344060 bits: 20/19 c ---[ 273]---> Adder-cost: 428 maxlim: 393212 bits: 20/19 c ---[ 271]---> Adder-cost: 428 maxlim: 344060 bits: 20/19 c ---[ 269]---> Adder-cost: 428 maxlim: 393212 bits: 20/19 c ---[ 267]---> Adder-cost: 428 maxlim: 344060 bits: 20/19 c ---[ 265]---> Adder-cost: 391 maxlim: 81917 bits: 18/17 c ---[ 263]---> Adder-cost: 428 maxlim: 393212 bits: 20/19 c ---[ 261]---> Adder-cost: 428 maxlim: 344060 bits: 20/19 c ---[ 259]---> Adder-cost: 428 maxlim: 393212 bits: 20/19 c ---[ 257]---> Adder-cost: 428 maxlim: 344060 bits: 20/19 c ---[ 255]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 253]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> BDD-cost: 16 c ---[ 251]---> BDD-cost: 7 c ---[ 250]---> BDD-cost: 15 c ---[ 249]---> BDD-cost: 4 c ---[ 247]---> Adder-cost: 391 maxlim: 131069 bits: 18/17 c ---[ 245]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 244]---> BDD-cost: 24 c ---[ 243]---> BDD-cost: 6 c ---[ 240]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 238]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 237]---> BDD-cost: 16 c ---[ 236]---> BDD-cost: 7 c ---[ 235]---> BDD-cost: 15 c ---[ 234]---> BDD-cost: 4 c ---[ 232]---> Adder-cost: 391 maxlim: 81917 bits: 18/17 c ---[ 230]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 229]---> BDD-cost: 23 c ---[ 228]---> BDD-cost: 8 c ---[ 225]---> Sorter-cost: 915 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 223]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 222]---> BDD-cost: 15 c ---[ 221]---> BDD-cost: 6 c ---[ 220]---> BDD-cost: 14 c ---[ 219]---> BDD-cost: 3 c ---[ 217]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 214]---> BDD-cost: 23 c ---[ 213]---> BDD-cost: 6 c ---[ 210]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 208]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 207]---> BDD-cost: 16 c ---[ 206]---> BDD-cost: 7 c ---[ 205]---> BDD-cost: 15 c ---[ 204]---> BDD-cost: 4 c ---[ 202]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 200]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> BDD-cost: 24 c ---[ 198]---> BDD-cost: 6 c ---[ 195]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 193]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 192]---> BDD-cost: 16 c ---[ 191]---> BDD-cost: 7 c ---[ 190]---> BDD-cost: 15 c ---[ 189]---> BDD-cost: 4 c ---[ 188]---> BDD-cost: 16 c ---[ 186]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 185]---> BDD-cost: 19 c ---[ 181]---> BDD-cost: 33 c ---[ 175]---> BDD-cost: 7 c ---[ 164]---> BDD-cost: 15 c ---[ 156]---> BDD-cost: 3 c ---[ 155]---> BDD-cost: 3 c ---[ 154]---> BDD-cost: 3 c ---[ 153]---> BDD-cost: 4 c ---[ 152]---> BDD-cost: 3 c ---[ 151]---> BDD-cost: 3 c ---[ 150]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> BDD-cost: 24 c ---[ 146]---> BDD-cost: 6 c ---[ 143]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> BDD-cost: 16 c ---[ 139]---> BDD-cost: 7 c ---[ 138]---> BDD-cost: 15 c ---[ 137]---> BDD-cost: 4 c ---[ 136]---> Sorter-cost: 1290 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 133]---> BDD-cost: 23 c ---[ 132]---> BDD-cost: 8 c ---[ 129]---> Sorter-cost: 915 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 127]---> Sorter-cost: 869 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> BDD-cost: 15 c ---[ 125]---> BDD-cost: 6 c ---[ 124]---> BDD-cost: 14 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> BDD-cost: 23 c ---[ 118]---> BDD-cost: 6 c ---[ 115]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> BDD-cost: 16 c ---[ 111]---> BDD-cost: 7 c ---[ 110]---> BDD-cost: 15 c ---[ 109]---> BDD-cost: 4 c ---[ 108]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> BDD-cost: 24 c ---[ 104]---> BDD-cost: 6 c ---[ 101]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> BDD-cost: 16 c ---[ 97]---> BDD-cost: 7 c ---[ 96]---> BDD-cost: 15 c ---[ 95]---> BDD-cost: 4 c ---[ 94]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 920 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> BDD-cost: 19 c ---[ 87]---> BDD-cost: 33 c ---[ 70]---> BDD-cost: 15 c ---[ 62]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 1203 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 1290 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> BDD-cost: 12 c ---[ 58]---> BDD-cost: 5 c ---[ 57]---> Sorter-cost: 808 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 747 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 847 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 750 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 862 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 821 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 50]---> Sorter-cost: 714 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 773 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 686 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 875 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 773 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 834 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 44]---> Sorter-cost: 747 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 663 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 908 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 808 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> BDD-cost: 12 c ---[ 38]---> BDD-cost: 5 c ---[ 37]---> Sorter-cost: 811 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 801 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 821 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 895 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 824 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 798 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 747 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Sorter-cost: 788 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 714 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 895 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 788 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 801 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 821 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 22]---> Sorter-cost: 747 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 875 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 811 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 19]---> BDD-cost: 5 c ---[ 18]---> Sorter-cost: 727 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> BDD-cost: 12 c ---[ 16]---> Sorter-cost: 630 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> Sorter-cost: 811 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 14]---> Sorter-cost: 747 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 13]---> Sorter-cost: 860 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 12]---> Sorter-cost: 788 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 704 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 686 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 788 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 650 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 908 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 798 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 630 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 760 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 660 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 1]---> Sorter-cost: 872 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 727 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 333790 886289 | 111263 0 0 nan | 0.000 % | c | 100 | 333689 886069 | 122389 82 264 3.2 | 4.481 % | c | 250 | 333597 885869 | 134628 210 689 3.3 | 4.507 % | c | 475 | 333435 885515 | 148091 408 1295 3.2 | 4.555 % | c | 812 | 333059 884679 | 162900 700 2234 3.2 | 4.662 % | c | 1318 | 332410 883226 | 179190 1143 3825 3.3 | 4.838 % | c | 2077 | 331562 881336 | 197109 1802 6121 3.4 | 5.075 % | c | 3216 | 330950 879975 | 216820 2845 9983 3.5 | 5.238 % | c | 4924 | 329404 876535 | 238502 4329 15698 3.6 | 5.665 % | c | 7486 | 328443 874392 | 262352 6713 48826 7.3 | 5.924 % | c | 11330 | 326869 870869 | 288587 10302 92482 9.0 | 6.350 % | c | 17097 | 325584 867960 | 317446 15919 219879 13.8 | 6.707 % | c | 25747 | 324551 865655 | 349190 24424 431973 17.7 | 6.984 % | c | 38721 | 323989 864389 | 384110 37319 890114 23.9 | 7.138 % | c | 58186 | 323535 863367 | 422521 56730 1652421 29.1 | 7.264 % | c | 87378 | 322070 860086 | 464773 85698 2899355 33.8 | 7.675 % | c | 131168 | 320907 857454 | 511250 129348 4534053 35.1 | 7.995 % | c | 196852 | 319545 854363 | 562375 194804 7383330 37.9 | 8.366 % | c | 295380 | 318648 852328 | 618613 293155 11490253 39.2 | 8.620 % | c | 443173 | 317986 850831 | 680474 440861 18651400 42.3 | 8.807 % |
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/1099/stat): 1099 (minisat+_script) R 1098 1099 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855527677 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/1099/statm): 174 3 169 147 0 27 0 [pid=1099] 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=1100 New process pid=1101 New process pid=1102 execve syscall for /bin/sed executable One traced child (pid=1101) 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=1102) exited with status: 0 One traced child (pid=1100) exited with status: 0 New process pid=1103 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb [startup+10.0043 s] Raw data (loadavg): 0.93 0.97 0.96 2/58 1103 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9482 0 0 0 917 41 0 0 25 0 1 0 1855527682 40001536 9101 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 9766 9101 145 145 0 9621 0 [pid=1103] vsize: 39064 Current children cumulated CPU time (s) 9.59 Current children cumulated vsize (Kb) 41188 [startup+20.0053 s] Raw data (loadavg): 0.94 0.97 0.96 2/58 1103 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9514 0 0 0 1915 42 0 0 25 0 1 0 1855527682 40128512 9133 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 9797 9133 145 145 0 9652 0 [pid=1103] vsize: 39188 Current children cumulated CPU time (s) 19.58 Current children cumulated vsize (Kb) 41312 [startup+30.0062 s] Raw data (loadavg): 0.95 0.97 0.96 2/58 1103 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9549 0 0 0 2914 42 0 0 25 0 1 0 1855527682 40235008 9168 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 9823 9168 145 145 0 9678 0 [pid=1103] vsize: 39292 Current children cumulated CPU time (s) 29.57 Current children cumulated vsize (Kb) 41416 [startup+40.0071 s] Raw data (loadavg): 0.96 0.97 0.96 2/58 1103 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9592 0 0 0 3914 43 0 0 25 0 1 0 1855527682 40378368 9211 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 9858 9211 145 145 0 9713 0 [pid=1103] vsize: 39432 Current children cumulated CPU time (s) 39.58 Current children cumulated vsize (Kb) 41556 [startup+50.0081 s] Raw data (loadavg): 0.96 0.97 0.96 2/58 1103 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9651 0 0 0 4913 43 0 0 25 0 1 0 1855527682 40603648 9270 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 9913 9270 145 145 0 9768 0 [pid=1103] vsize: 39652 Current children cumulated CPU time (s) 49.57 Current children cumulated vsize (Kb) 41776 [startup+60.009 s] Raw data (loadavg): 0.97 0.97 0.96 2/58 1105 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9700 0 0 0 5913 43 0 0 25 0 1 0 1855527682 40804352 9319 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 9962 9319 145 145 0 9817 0 [pid=1103] vsize: 39848 Current children cumulated CPU time (s) 59.57 Current children cumulated vsize (Kb) 41972 [startup+70.01 s] Raw data (loadavg): 0.97 0.97 0.96 2/58 1105 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9745 0 0 0 6911 44 0 0 25 0 1 0 1855527682 40976384 9364 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 10004 9364 145 145 0 9859 0 [pid=1103] vsize: 40016 Current children cumulated CPU time (s) 69.56 Current children cumulated vsize (Kb) 42140 [startup+80.0109 s] Raw data (loadavg): 0.98 0.97 0.96 2/58 1105 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9998 0 0 0 7908 45 0 0 25 0 1 0 1855527682 42041344 9617 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 10264 9617 145 145 0 10119 0 [pid=1103] vsize: 41056 Current children cumulated CPU time (s) 79.54 Current children cumulated vsize (Kb) 43180 [startup+90.0118 s] Raw data (loadavg): 0.98 0.97 0.96 2/58 1105 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 10054 0 0 0 8907 46 0 0 25 0 1 0 1855527682 42258432 9673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 10317 9673 145 145 0 10172 0 [pid=1103] vsize: 41268 Current children cumulated CPU time (s) 89.54 Current children cumulated vsize (Kb) 43392 [startup+100.013 s] Raw data (loadavg): 0.98 0.97 0.96 2/58 1105 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 10346 0 0 0 9902 48 0 0 25 0 1 0 1855527682 43421696 9965 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 10601 9965 145 145 0 10456 0 [pid=1103] vsize: 42404 Current children cumulated CPU time (s) 99.51 Current children cumulated vsize (Kb) 44528 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.96 2/58 1105 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 10734 0 0 0 10896 51 0 0 25 0 1 0 1855527682 45113344 10353 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/1103/statm): 11014 10353 145 145 0 10869 0 [pid=1103] vsize: 44056 Current children cumulated CPU time (s) 109.48 Current children cumulated vsize (Kb) 46180 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1107 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 11078 0 0 0 11890 53 0 0 25 0 1 0 1855527682 46489600 10697 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 11350 10697 145 145 0 11205 0 [pid=1103] vsize: 45400 Current children cumulated CPU time (s) 119.44 Current children cumulated vsize (Kb) 47524 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1107 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 11401 0 0 0 12885 55 0 0 25 0 1 0 1855527682 47783936 11020 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 11666 11020 145 145 0 11521 0 [pid=1103] vsize: 46664 Current children cumulated CPU time (s) 129.41 Current children cumulated vsize (Kb) 48788 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1107 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 11825 0 0 0 13879 58 0 0 25 0 1 0 1855527682 49491968 11444 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 12083 11444 145 145 0 11938 0 [pid=1103] vsize: 48332 Current children cumulated CPU time (s) 139.38 Current children cumulated vsize (Kb) 50456 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1107 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12265 0 0 0 14872 61 0 0 25 0 1 0 1855527682 51269632 11884 4294967295 134512640 135094434 3221224432 3221223076 134562166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 12517 11884 145 145 0 12372 0 [pid=1103] vsize: 50068 Current children cumulated CPU time (s) 149.34 Current children cumulated vsize (Kb) 52192 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1107 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12589 0 0 0 15865 63 0 0 25 0 1 0 1855527682 52834304 12208 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 12899 12208 145 145 0 12754 0 [pid=1103] vsize: 51596 Current children cumulated CPU time (s) 159.29 Current children cumulated vsize (Kb) 53720 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1107 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12844 0 0 0 16862 64 0 0 25 0 1 0 1855527682 53858304 12463 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 13149 12463 145 145 0 13004 0 [pid=1103] vsize: 52596 Current children cumulated CPU time (s) 169.27 Current children cumulated vsize (Kb) 54720 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1109 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12965 0 0 0 17860 65 0 0 25 0 1 0 1855527682 54341632 12584 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 13267 12584 145 145 0 13122 0 [pid=1103] vsize: 53068 Current children cumulated CPU time (s) 179.26 Current children cumulated vsize (Kb) 55192 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1109 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13265 0 0 0 18854 67 0 0 25 0 1 0 1855527682 55554048 12884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 13563 12884 145 145 0 13418 0 [pid=1103] vsize: 54252 Current children cumulated CPU time (s) 189.22 Current children cumulated vsize (Kb) 56376 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1109 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13419 0 0 0 19852 68 0 0 25 0 1 0 1855527682 56168448 13038 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 13713 13038 145 145 0 13568 0 [pid=1103] vsize: 54852 Current children cumulated CPU time (s) 199.21 Current children cumulated vsize (Kb) 56976 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1109 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13652 0 0 0 20848 70 0 0 25 0 1 0 1855527682 57102336 13271 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 13941 13271 145 145 0 13796 0 [pid=1103] vsize: 55764 Current children cumulated CPU time (s) 209.19 Current children cumulated vsize (Kb) 57888 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1109 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13790 0 0 0 21846 72 0 0 25 0 1 0 1855527682 57651200 13409 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 14075 13409 145 145 0 13930 0 [pid=1103] vsize: 56300 Current children cumulated CPU time (s) 219.19 Current children cumulated vsize (Kb) 58424 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1109 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 14003 0 0 0 22842 73 0 0 25 0 1 0 1855527682 58499072 13622 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/1103/statm): 14282 13622 145 145 0 14137 0 [pid=1103] vsize: 57128 Current children cumulated CPU time (s) 229.16 Current children cumulated vsize (Kb) 59252 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1111 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 14474 0 0 0 23834 77 0 0 25 0 1 0 1855527682 60399616 14093 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 14746 14093 145 145 0 14601 0 [pid=1103] vsize: 58984 Current children cumulated CPU time (s) 239.12 Current children cumulated vsize (Kb) 61108 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1111 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 14755 0 0 0 24830 78 0 0 25 0 1 0 1855527682 61526016 14374 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/1103/statm): 15021 14374 145 145 0 14876 0 [pid=1103] vsize: 60084 Current children cumulated CPU time (s) 249.09 Current children cumulated vsize (Kb) 62208 [startup+260.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1111 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 15079 0 0 0 25824 80 0 0 25 0 1 0 1855527682 62828544 14698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 15339 14698 145 145 0 15194 0 [pid=1103] vsize: 61356 Current children cumulated CPU time (s) 259.05 Current children cumulated vsize (Kb) 63480 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1111 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 15271 0 0 0 26822 81 0 0 25 0 1 0 1855527682 63602688 14890 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 15528 14890 145 145 0 15383 0 [pid=1103] vsize: 62112 Current children cumulated CPU time (s) 269.04 Current children cumulated vsize (Kb) 64236 [startup+280.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1111 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 15618 0 0 0 27817 83 0 0 25 0 1 0 1855527682 65519616 15237 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 15996 15237 145 145 0 15851 0 [pid=1103] vsize: 63984 Current children cumulated CPU time (s) 279.01 Current children cumulated vsize (Kb) 66108 [startup+290.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1111 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 16073 0 0 0 28809 88 0 0 25 0 1 0 1855527682 67354624 15692 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 16444 15692 145 145 0 16299 0 [pid=1103] vsize: 65776 Current children cumulated CPU time (s) 288.98 Current children cumulated vsize (Kb) 67900 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1113 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 16498 0 0 0 29803 90 0 0 25 0 1 0 1855527682 69066752 16117 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 16862 16117 145 145 0 16717 0 [pid=1103] vsize: 67448 Current children cumulated CPU time (s) 298.94 Current children cumulated vsize (Kb) 69572 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1113 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 16803 0 0 0 30798 93 0 0 25 0 1 0 1855527682 70299648 16422 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 17163 16422 145 145 0 17018 0 [pid=1103] vsize: 68652 Current children cumulated CPU time (s) 308.92 Current children cumulated vsize (Kb) 70776 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1113 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17096 0 0 0 31794 95 0 0 25 0 1 0 1855527682 71475200 16715 4294967295 134512640 135094434 3221224432 3221223104 134556401 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 17450 16715 145 145 0 17305 0 [pid=1103] vsize: 69800 Current children cumulated CPU time (s) 318.9 Current children cumulated vsize (Kb) 71924 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1113 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17342 0 0 0 32789 97 0 0 25 0 1 0 1855527682 72458240 16961 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 17690 16961 145 145 0 17545 0 [pid=1103] vsize: 70760 Current children cumulated CPU time (s) 328.87 Current children cumulated vsize (Kb) 72884 [startup+340.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1113 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17564 0 0 0 33785 99 0 0 25 0 1 0 1855527682 73347072 17183 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 17907 17183 145 145 0 17762 0 [pid=1103] vsize: 71628 Current children cumulated CPU time (s) 338.85 Current children cumulated vsize (Kb) 73752 [startup+350.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1113 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17769 0 0 0 34781 101 0 0 25 0 1 0 1855527682 74170368 17388 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 18108 17388 145 145 0 17963 0 [pid=1103] vsize: 72432 Current children cumulated CPU time (s) 348.83 Current children cumulated vsize (Kb) 74556 [startup+360.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1115 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18083 0 0 0 35775 103 0 0 25 0 1 0 1855527682 75436032 17702 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 18417 17702 145 145 0 18272 0 [pid=1103] vsize: 73668 Current children cumulated CPU time (s) 358.79 Current children cumulated vsize (Kb) 75792 [startup+370.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1115 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18202 0 0 0 36774 104 0 0 25 0 1 0 1855527682 75919360 17821 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 18535 17821 145 145 0 18390 0 [pid=1103] vsize: 74140 Current children cumulated CPU time (s) 368.79 Current children cumulated vsize (Kb) 76264 [startup+380.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1115 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18376 0 0 0 37770 106 0 0 25 0 1 0 1855527682 76615680 17995 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 18705 17995 145 145 0 18560 0 [pid=1103] vsize: 74820 Current children cumulated CPU time (s) 378.77 Current children cumulated vsize (Kb) 76944 [startup+390.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1115 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18785 0 0 0 38763 109 0 0 25 0 1 0 1855527682 78262272 18404 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 19107 18404 145 145 0 18962 0 [pid=1103] vsize: 76428 Current children cumulated CPU time (s) 388.73 Current children cumulated vsize (Kb) 78552 [startup+400.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1115 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19092 0 0 0 39758 111 0 0 25 0 1 0 1855527682 79499264 18711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 19409 18711 145 145 0 19264 0 [pid=1103] vsize: 77636 Current children cumulated CPU time (s) 398.7 Current children cumulated vsize (Kb) 79760 [startup+410.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1115 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19389 0 0 0 40754 114 0 0 25 0 1 0 1855527682 80699392 19008 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 19702 19008 145 145 0 19557 0 [pid=1103] vsize: 78808 Current children cumulated CPU time (s) 408.69 Current children cumulated vsize (Kb) 80932 [startup+420.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1117 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19714 0 0 0 41747 117 0 0 25 0 1 0 1855527682 82010112 19333 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 20022 19333 145 145 0 19877 0 [pid=1103] vsize: 80088 Current children cumulated CPU time (s) 418.65 Current children cumulated vsize (Kb) 82212 [startup+430.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1117 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19916 0 0 0 42743 119 0 0 25 0 1 0 1855527682 82821120 19535 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 20220 19535 145 145 0 20075 0 [pid=1103] vsize: 80880 Current children cumulated CPU time (s) 428.63 Current children cumulated vsize (Kb) 83004 [startup+440.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1117 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 20269 0 0 0 43737 122 0 0 25 0 1 0 1855527682 84242432 19888 4294967295 134512640 135094434 3221224432 3221222960 134780607 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 20567 19888 145 145 0 20422 0 [pid=1103] vsize: 82268 Current children cumulated CPU time (s) 438.6 Current children cumulated vsize (Kb) 84392 [startup+450.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1117 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 20617 0 0 0 44730 125 0 0 25 0 1 0 1855527682 85635072 20236 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 20907 20236 145 145 0 20762 0 [pid=1103] vsize: 83628 Current children cumulated CPU time (s) 448.56 Current children cumulated vsize (Kb) 85752 [startup+460.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1117 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 20907 0 0 0 45725 127 0 0 25 0 1 0 1855527682 86806528 20526 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 21193 20526 145 145 0 21048 0 [pid=1103] vsize: 84772 Current children cumulated CPU time (s) 458.53 Current children cumulated vsize (Kb) 86896 [startup+470.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1117 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 21067 0 0 0 46722 128 0 0 25 0 1 0 1855527682 87445504 20686 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 21349 20686 145 145 0 21204 0 [pid=1103] vsize: 85396 Current children cumulated CPU time (s) 468.51 Current children cumulated vsize (Kb) 87520 [startup+480.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1119 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 21309 0 0 0 47718 130 0 0 25 0 1 0 1855527682 88416256 20928 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 21586 20928 145 145 0 21441 0 [pid=1103] vsize: 86344 Current children cumulated CPU time (s) 478.49 Current children cumulated vsize (Kb) 88468 [startup+490.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1119 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 21656 0 0 0 48711 132 0 0 25 0 1 0 1855527682 89808896 21275 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 21926 21275 145 145 0 21781 0 [pid=1103] vsize: 87704 Current children cumulated CPU time (s) 488.44 Current children cumulated vsize (Kb) 89828 [startup+500.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1119 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 21940 0 0 0 49706 134 0 0 25 0 1 0 1855527682 90963968 21559 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/1103/statm): 22208 21559 145 145 0 22063 0 [pid=1103] vsize: 88832 Current children cumulated CPU time (s) 498.41 Current children cumulated vsize (Kb) 90956 [startup+510.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1119 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22215 0 0 0 50701 136 0 0 25 0 1 0 1855527682 92061696 21834 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 22476 21834 145 145 0 22331 0 [pid=1103] vsize: 89904 Current children cumulated CPU time (s) 508.38 Current children cumulated vsize (Kb) 92028 [startup+520.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1119 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22505 0 0 0 51696 138 0 0 25 0 1 0 1855527682 94277632 22124 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 23017 22124 145 145 0 22872 0 [pid=1103] vsize: 92068 Current children cumulated CPU time (s) 518.35 Current children cumulated vsize (Kb) 94192 [startup+530.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1119 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22741 0 0 0 52693 140 0 0 25 0 1 0 1855527682 95227904 22360 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 23249 22360 145 145 0 23104 0 [pid=1103] vsize: 92996 Current children cumulated CPU time (s) 528.34 Current children cumulated vsize (Kb) 95120 [startup+540.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1121 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22923 0 0 0 53689 142 0 0 25 0 1 0 1855527682 95973376 22542 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 23431 22542 145 145 0 23286 0 [pid=1103] vsize: 93724 Current children cumulated CPU time (s) 538.32 Current children cumulated vsize (Kb) 95848 [startup+550.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1121 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 23229 0 0 0 54685 144 0 0 25 0 1 0 1855527682 97206272 22848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 23732 22848 145 145 0 23587 0 [pid=1103] vsize: 94928 Current children cumulated CPU time (s) 548.3 Current children cumulated vsize (Kb) 97052 [startup+560.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1121 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 23588 0 0 0 55678 147 0 0 25 0 1 0 1855527682 98656256 23207 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 24086 23207 145 145 0 23941 0 [pid=1103] vsize: 96344 Current children cumulated CPU time (s) 558.26 Current children cumulated vsize (Kb) 98468 [startup+570.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1121 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 23878 0 0 0 56673 149 0 0 25 0 1 0 1855527682 99844096 23497 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 24376 23497 145 145 0 24231 0 [pid=1103] vsize: 97504 Current children cumulated CPU time (s) 568.23 Current children cumulated vsize (Kb) 99628 [startup+580.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1121 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24103 0 0 0 57669 151 0 0 25 0 1 0 1855527682 100757504 23722 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 24599 23722 145 145 0 24454 0 [pid=1103] vsize: 98396 Current children cumulated CPU time (s) 578.21 Current children cumulated vsize (Kb) 100520 [startup+590.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1121 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24216 0 0 0 58668 152 0 0 25 0 1 0 1855527682 101216256 23835 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 24711 23835 145 145 0 24566 0 [pid=1103] vsize: 98844 Current children cumulated CPU time (s) 588.21 Current children cumulated vsize (Kb) 100968 [startup+600.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1123 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24483 0 0 0 59662 154 0 0 25 0 1 0 1855527682 102289408 24102 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 24973 24102 145 145 0 24828 0 [pid=1103] vsize: 99892 Current children cumulated CPU time (s) 598.17 Current children cumulated vsize (Kb) 102016 [startup+610.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1123 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24801 0 0 0 60656 157 0 0 25 0 1 0 1855527682 103575552 24420 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 25287 24420 145 145 0 25142 0 [pid=1103] vsize: 101148 Current children cumulated CPU time (s) 608.14 Current children cumulated vsize (Kb) 103272 [startup+620.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1123 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 25184 0 0 0 61649 160 0 0 25 0 1 0 1855527682 105127936 24803 4294967295 134512640 135094434 3221224432 3221223104 134556505 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 25666 24803 145 145 0 25521 0 [pid=1103] vsize: 102664 Current children cumulated CPU time (s) 618.1 Current children cumulated vsize (Kb) 104788 [startup+630.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1123 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 25465 0 0 0 62644 162 0 0 25 0 1 0 1855527682 106262528 25084 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 25943 25084 145 145 0 25798 0 [pid=1103] vsize: 103772 Current children cumulated CPU time (s) 628.07 Current children cumulated vsize (Kb) 105896 [startup+640.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1123 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 25629 0 0 0 63641 163 0 0 25 0 1 0 1855527682 106930176 25248 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 26106 25248 145 145 0 25961 0 [pid=1103] vsize: 104424 Current children cumulated CPU time (s) 638.05 Current children cumulated vsize (Kb) 106548 [startup+650.067 s] Raw data (loadavg): 0.99 0.97 0.96 1/58 1123 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 25833 0 0 0 64637 165 0 0 25 0 1 0 1855527682 107745280 25452 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/1103/statm): 26305 25452 145 145 0 26160 0 [pid=1103] vsize: 105220 Current children cumulated CPU time (s) 648.03 Current children cumulated vsize (Kb) 107344 [startup+660.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1125 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26116 0 0 0 65632 168 0 0 25 0 1 0 1855527682 108896256 25735 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 26586 25735 145 145 0 26441 0 [pid=1103] vsize: 106344 Current children cumulated CPU time (s) 658.01 Current children cumulated vsize (Kb) 108468 [startup+670.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1125 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26310 0 0 0 66628 170 0 0 25 0 1 0 1855527682 109678592 25929 4294967295 134512640 135094434 3221224432 3221223024 134557283 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 26777 25929 145 145 0 26632 0 [pid=1103] vsize: 107108 Current children cumulated CPU time (s) 667.99 Current children cumulated vsize (Kb) 109232 [startup+680.071 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1125 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26583 0 0 0 67623 172 0 0 25 0 1 0 1855527682 110780416 26202 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 27046 26202 145 145 0 26901 0 [pid=1103] vsize: 108184 Current children cumulated CPU time (s) 677.96 Current children cumulated vsize (Kb) 110308 [startup+690.072 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1125 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26915 0 0 0 68617 175 0 0 25 0 1 0 1855527682 112128000 26534 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 27375 26534 145 145 0 27230 0 [pid=1103] vsize: 109500 Current children cumulated CPU time (s) 687.93 Current children cumulated vsize (Kb) 111624 [startup+700.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1125 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27306 0 0 0 69610 178 0 0 25 0 1 0 1855527682 113664000 26925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 27750 26925 145 145 0 27605 0 [pid=1103] vsize: 111000 Current children cumulated CPU time (s) 697.89 Current children cumulated vsize (Kb) 113124 [startup+710.075 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1125 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27494 0 0 0 70608 179 0 0 25 0 1 0 1855527682 114417664 27113 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 27934 27113 145 145 0 27789 0 [pid=1103] vsize: 111736 Current children cumulated CPU time (s) 707.88 Current children cumulated vsize (Kb) 113860 [startup+720.076 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1127 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27642 0 0 0 71605 180 0 0 25 0 1 0 1855527682 115019776 27261 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 28081 27261 145 145 0 27936 0 [pid=1103] vsize: 112324 Current children cumulated CPU time (s) 717.86 Current children cumulated vsize (Kb) 114448 [startup+730.077 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1127 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27894 0 0 0 72601 182 0 0 25 0 1 0 1855527682 116039680 27513 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 28330 27513 145 145 0 28185 0 [pid=1103] vsize: 113320 Current children cumulated CPU time (s) 727.84 Current children cumulated vsize (Kb) 115444 [startup+740.078 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1127 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28163 0 0 0 73597 184 0 0 25 0 1 0 1855527682 117133312 27782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 28597 27782 145 145 0 28452 0 [pid=1103] vsize: 114388 Current children cumulated CPU time (s) 737.82 Current children cumulated vsize (Kb) 116512 [startup+750.079 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1127 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28421 0 0 0 74591 187 0 0 25 0 1 0 1855527682 118181888 28040 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 28853 28040 145 145 0 28708 0 [pid=1103] vsize: 115412 Current children cumulated CPU time (s) 747.79 Current children cumulated vsize (Kb) 117536 [startup+760.081 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1127 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28710 0 0 0 75585 190 0 0 25 0 1 0 1855527682 119341056 28329 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 29136 28329 145 145 0 28991 0 [pid=1103] vsize: 116544 Current children cumulated CPU time (s) 757.76 Current children cumulated vsize (Kb) 118668 [startup+770.082 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1127 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28913 0 0 0 76580 193 0 0 25 0 1 0 1855527682 120152064 28532 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 29334 28532 145 145 0 29189 0 [pid=1103] vsize: 117336 Current children cumulated CPU time (s) 767.74 Current children cumulated vsize (Kb) 119460 [startup+780.083 s] Raw data (loadavg): 0.99 0.97 0.96 2/58 1129 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29148 0 0 0 77575 195 0 0 25 0 1 0 1855527682 121114624 28767 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 29569 28767 145 145 0 29424 0 [pid=1103] vsize: 118276 Current children cumulated CPU time (s) 777.71 Current children cumulated vsize (Kb) 120400 [startup+790.084 s] Raw data (loadavg): 1.07 0.99 0.97 2/58 1129 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29402 0 0 0 78571 197 0 0 25 0 1 0 1855527682 122150912 29021 4294967295 134512640 135094434 3221224432 3221223044 134563115 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 29822 29021 145 145 0 29677 0 [pid=1103] vsize: 119288 Current children cumulated CPU time (s) 787.69 Current children cumulated vsize (Kb) 121412 [startup+800.085 s] Raw data (loadavg): 1.06 0.99 0.97 2/58 1129 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29553 0 0 0 79569 198 0 0 25 0 1 0 1855527682 122773504 29172 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 29974 29172 145 145 0 29829 0 [pid=1103] vsize: 119896 Current children cumulated CPU time (s) 797.68 Current children cumulated vsize (Kb) 122020 [startup+810.087 s] Raw data (loadavg): 1.05 0.99 0.97 2/58 1129 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29720 0 0 0 80566 200 0 0 25 0 1 0 1855527682 123437056 29339 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 30136 29339 145 145 0 29991 0 [pid=1103] vsize: 120544 Current children cumulated CPU time (s) 807.67 Current children cumulated vsize (Kb) 122668 [startup+820.091 s] Raw data (loadavg): 1.04 0.99 0.97 2/58 1129 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29966 0 0 0 81562 202 0 0 25 0 1 0 1855527682 124424192 29585 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 30377 29585 145 145 0 30232 0 [pid=1103] vsize: 121508 Current children cumulated CPU time (s) 817.65 Current children cumulated vsize (Kb) 123632 [startup+830.091 s] Raw data (loadavg): 1.04 0.99 0.97 2/58 1129 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30212 0 0 0 82557 205 0 0 25 0 1 0 1855527682 125415424 29831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 30619 29831 145 145 0 30474 0 [pid=1103] vsize: 122476 Current children cumulated CPU time (s) 827.63 Current children cumulated vsize (Kb) 124600 [startup+840.092 s] Raw data (loadavg): 1.03 0.99 0.97 2/58 1131 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30455 0 0 0 83554 206 0 0 25 0 1 0 1855527682 126390272 30074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 30857 30074 145 145 0 30712 0 [pid=1103] vsize: 123428 Current children cumulated CPU time (s) 837.61 Current children cumulated vsize (Kb) 125552 [startup+850.093 s] Raw data (loadavg): 1.03 0.99 0.97 2/58 1131 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30699 0 0 0 84551 207 0 0 25 0 1 0 1855527682 127365120 30318 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 31095 30318 145 145 0 30950 0 [pid=1103] vsize: 124380 Current children cumulated CPU time (s) 847.59 Current children cumulated vsize (Kb) 126504 [startup+860.094 s] Raw data (loadavg): 1.02 0.99 0.97 2/58 1131 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30839 0 0 0 85548 208 0 0 25 0 1 0 1855527682 127922176 30458 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 31231 30458 145 145 0 31086 0 [pid=1103] vsize: 124924 Current children cumulated CPU time (s) 857.57 Current children cumulated vsize (Kb) 127048 [startup+870.095 s] Raw data (loadavg): 1.02 0.99 0.97 2/58 1131 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 31082 0 0 0 86544 209 0 0 25 0 1 0 1855527682 128901120 30701 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 31470 30701 145 145 0 31325 0 [pid=1103] vsize: 125880 Current children cumulated CPU time (s) 867.54 Current children cumulated vsize (Kb) 128004 [startup+880.096 s] Raw data (loadavg): 1.01 0.99 0.97 2/58 1131 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 31390 0 0 0 87538 212 0 0 25 0 1 0 1855527682 130162688 31009 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 31778 31009 145 145 0 31633 0 [pid=1103] vsize: 127112 Current children cumulated CPU time (s) 877.51 Current children cumulated vsize (Kb) 129236 [startup+890.097 s] Raw data (loadavg): 1.01 0.99 0.97 2/58 1131 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 31704 0 0 0 88533 214 0 0 25 0 1 0 1855527682 131424256 31323 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 32086 31323 145 145 0 31941 0 [pid=1103] vsize: 128344 Current children cumulated CPU time (s) 887.48 Current children cumulated vsize (Kb) 130468 [startup+900.097 s] Raw data (loadavg): 1.01 0.99 0.97 2/58 1133 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32020 0 0 0 89526 216 0 0 25 0 1 0 1855527682 132714496 31639 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 32401 31639 145 145 0 32256 0 [pid=1103] vsize: 129604 Current children cumulated CPU time (s) 897.43 Current children cumulated vsize (Kb) 131728 [startup+910.099 s] Raw data (loadavg): 1.01 0.99 0.97 2/58 1133 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32329 0 0 0 90522 218 0 0 25 0 1 0 1855527682 133996544 31948 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 32714 31948 145 145 0 32569 0 [pid=1103] vsize: 130856 Current children cumulated CPU time (s) 907.41 Current children cumulated vsize (Kb) 132980 [startup+920.1 s] Raw data (loadavg): 1.01 0.99 0.97 2/58 1133 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32539 0 0 0 91519 219 0 0 25 0 1 0 1855527682 134848512 32158 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 32922 32158 145 145 0 32777 0 [pid=1103] vsize: 131688 Current children cumulated CPU time (s) 917.39 Current children cumulated vsize (Kb) 133812 [startup+930.101 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1133 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32761 0 0 0 92515 221 0 0 25 0 1 0 1855527682 135745536 32380 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 33141 32380 145 145 0 32996 0 [pid=1103] vsize: 132564 Current children cumulated CPU time (s) 927.37 Current children cumulated vsize (Kb) 134688 [startup+940.102 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1133 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32962 0 0 0 93512 223 0 0 25 0 1 0 1855527682 136556544 32581 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 33339 32581 145 145 0 33194 0 [pid=1103] vsize: 133356 Current children cumulated CPU time (s) 937.36 Current children cumulated vsize (Kb) 135480 [startup+950.103 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1133 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33128 0 0 0 94509 224 0 0 25 0 1 0 1855527682 137244672 32747 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 33507 32747 145 145 0 33362 0 [pid=1103] vsize: 134028 Current children cumulated CPU time (s) 947.34 Current children cumulated vsize (Kb) 136152 [startup+960.104 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1135 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33271 0 0 0 95506 226 0 0 25 0 1 0 1855527682 137822208 32890 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 33648 32890 145 145 0 33503 0 [pid=1103] vsize: 134592 Current children cumulated CPU time (s) 957.33 Current children cumulated vsize (Kb) 136716 [startup+970.105 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1135 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33431 0 0 0 96503 228 0 0 25 0 1 0 1855527682 138498048 33050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 33813 33050 145 145 0 33668 0 [pid=1103] vsize: 135252 Current children cumulated CPU time (s) 967.32 Current children cumulated vsize (Kb) 137376 [startup+980.105 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1135 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33542 0 0 0 97500 229 0 0 25 0 1 0 1855527682 138948608 33161 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 33923 33161 145 145 0 33778 0 [pid=1103] vsize: 135692 Current children cumulated CPU time (s) 977.3 Current children cumulated vsize (Kb) 137816 [startup+990.107 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1135 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33892 0 0 0 98495 232 0 0 25 0 1 0 1855527682 140357632 33511 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 34267 33511 145 145 0 34122 0 [pid=1103] vsize: 137068 Current children cumulated CPU time (s) 987.28 Current children cumulated vsize (Kb) 139192 [startup+1000.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1135 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34140 0 0 0 99491 235 0 0 25 0 1 0 1855527682 141348864 33759 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 34509 33759 145 145 0 34364 0 [pid=1103] vsize: 138036 Current children cumulated CPU time (s) 997.27 Current children cumulated vsize (Kb) 140160 [startup+1010.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1135 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34349 0 0 0 100488 236 0 0 25 0 1 0 1855527682 142188544 33968 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 34714 33968 145 145 0 34569 0 [pid=1103] vsize: 138856 Current children cumulated CPU time (s) 1007.25 Current children cumulated vsize (Kb) 140980 [startup+1020.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1137 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34443 0 0 0 101486 237 0 0 25 0 1 0 1855527682 142561280 34062 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 34805 34062 145 145 0 34660 0 [pid=1103] vsize: 139220 Current children cumulated CPU time (s) 1017.24 Current children cumulated vsize (Kb) 141344 [startup+1030.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1137 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34648 0 0 0 102484 238 0 0 25 0 1 0 1855527682 143388672 34267 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 35007 34267 145 145 0 34862 0 [pid=1103] vsize: 140028 Current children cumulated CPU time (s) 1027.23 Current children cumulated vsize (Kb) 142152 [startup+1040.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1137 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 35034 0 0 0 103479 240 0 0 25 0 1 0 1855527682 144961536 34653 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 35391 34653 145 145 0 35246 0 [pid=1103] vsize: 141564 Current children cumulated CPU time (s) 1037.2 Current children cumulated vsize (Kb) 143688 [startup+1050.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1137 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 35370 0 0 0 104472 242 0 0 25 0 1 0 1855527682 146329600 34989 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 35725 34989 145 145 0 35580 0 [pid=1103] vsize: 142900 Current children cumulated CPU time (s) 1047.15 Current children cumulated vsize (Kb) 145024 [startup+1060.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1137 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 35718 0 0 0 105467 244 0 0 25 0 1 0 1855527682 147730432 35337 4294967295 134512640 135094434 3221224432 3221223056 134557722 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 36067 35337 145 145 0 35922 0 [pid=1103] vsize: 144268 Current children cumulated CPU time (s) 1057.12 Current children cumulated vsize (Kb) 146392 [startup+1070.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1137 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 36122 0 0 0 106461 247 0 0 25 0 1 0 1855527682 149364736 35741 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 36466 35741 145 145 0 36321 0 [pid=1103] vsize: 145864 Current children cumulated CPU time (s) 1067.09 Current children cumulated vsize (Kb) 147988 [startup+1080.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1139 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 36279 0 0 0 107458 249 0 0 25 0 1 0 1855527682 150007808 35898 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 36623 35898 145 145 0 36478 0 [pid=1103] vsize: 146492 Current children cumulated CPU time (s) 1077.08 Current children cumulated vsize (Kb) 148616 [startup+1090.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1139 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 36711 0 0 0 108450 252 0 0 25 0 1 0 1855527682 151756800 36330 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 37050 36330 145 145 0 36905 0 [pid=1103] vsize: 148200 Current children cumulated CPU time (s) 1087.03 Current children cumulated vsize (Kb) 150324 [startup+1100.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1139 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 37257 0 0 0 109440 257 0 0 25 0 1 0 1855527682 153976832 36876 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 37592 36876 145 145 0 37447 0 [pid=1103] vsize: 150368 Current children cumulated CPU time (s) 1096.98 Current children cumulated vsize (Kb) 152492 [startup+1110.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1139 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 37705 0 0 0 110433 260 0 0 25 0 1 0 1855527682 155791360 37324 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 38035 37324 145 145 0 37890 0 [pid=1103] vsize: 152140 Current children cumulated CPU time (s) 1106.94 Current children cumulated vsize (Kb) 154264 [startup+1120.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1139 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 37919 0 0 0 111429 262 0 0 25 0 1 0 1855527682 156651520 37538 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 38245 37538 145 145 0 38100 0 [pid=1103] vsize: 152980 Current children cumulated CPU time (s) 1116.92 Current children cumulated vsize (Kb) 155104 [startup+1130.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1139 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38099 0 0 0 112427 262 0 0 25 0 1 0 1855527682 157368320 37718 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 38420 37718 145 145 0 38275 0 [pid=1103] vsize: 153680 Current children cumulated CPU time (s) 1126.9 Current children cumulated vsize (Kb) 155804 [startup+1140.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1141 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38271 0 0 0 113424 264 0 0 25 0 1 0 1855527682 158052352 37890 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 38587 37890 145 145 0 38442 0 [pid=1103] vsize: 154348 Current children cumulated CPU time (s) 1136.89 Current children cumulated vsize (Kb) 156472 [startup+1150.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1141 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38648 0 0 0 114416 267 0 0 25 0 1 0 1855527682 161669120 38267 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 39470 38267 145 145 0 39325 0 [pid=1103] vsize: 157880 Current children cumulated CPU time (s) 1146.84 Current children cumulated vsize (Kb) 160004 [startup+1160.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1141 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38890 0 0 0 115411 269 0 0 25 0 1 0 1855527682 162639872 38509 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1103/statm): 39707 38509 145 145 0 39562 0 [pid=1103] vsize: 158828 Current children cumulated CPU time (s) 1156.81 Current children cumulated vsize (Kb) 160952 [startup+1170.12 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1141 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39054 0 0 0 116408 270 0 0 25 0 1 0 1855527682 163295232 38673 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 39867 38673 145 145 0 39722 0 [pid=1103] vsize: 159468 Current children cumulated CPU time (s) 1166.79 Current children cumulated vsize (Kb) 161592 [startup+1180.13 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1141 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39277 0 0 0 117403 272 0 0 25 0 1 0 1855527682 164192256 38896 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 40086 38896 145 145 0 39941 0 [pid=1103] vsize: 160344 Current children cumulated CPU time (s) 1176.76 Current children cumulated vsize (Kb) 162468 [startup+1190.13 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1141 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39516 0 0 0 118399 274 0 0 25 0 1 0 1855527682 165158912 39135 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 40322 39135 145 145 0 40177 0 [pid=1103] vsize: 161288 Current children cumulated CPU time (s) 1186.74 Current children cumulated vsize (Kb) 163412 [startup+1200.13 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1143 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39744 0 0 0 119395 276 0 0 25 0 1 0 1855527682 166084608 39363 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 40548 39363 145 145 0 40403 0 [pid=1103] vsize: 162192 Current children cumulated CPU time (s) 1196.72 Current children cumulated vsize (Kb) 164316 [startup+1210.13 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1143 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39972 0 0 0 120391 277 0 0 25 0 1 0 1855527682 167010304 39591 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 40774 39591 145 145 0 40629 0 [pid=1103] vsize: 163096 Current children cumulated CPU time (s) 1206.69 Current children cumulated vsize (Kb) 165220 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 1.00 0.99 0.97 2/58 1143 Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1099/statm): 531 226 485 147 0 384 0 [pid=1099] vsize: 2124 Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39972 0 0 0 120391 277 0 0 25 0 1 0 1855527682 167010304 39591 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1103/statm): 40774 39591 145 145 0 40629 0 [pid=1103] vsize: 163096 Current children cumulated CPU time (s) 1206.69 Current children cumulated vsize (Kb) 165220 Sending SIGTERM to -1099 Sleeping 2 seconds One traced child (pid=1099) ended because it received signal 15 (SIGTERM) One traced child (pid=1103) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.21 CPU time (s): 1206.77 CPU user time (s): 1203.92 CPU system time (s): 2.84657 CPU usage (%): 99.7157 Max. virtual memory (cumulated for all children) (Kb): 165220
ERROR: no interpretation found !