Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-dcmulti.opb |
MD5SUM | 6ffc4ed72f4dd993b121ae0a2045731e |
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 wulflinc18 THE 2005-09-20 03:08:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3233 boxname=wulflinc18 idbench=889 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6ffc4ed72f4dd993b121ae0a2045731e /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-dcmulti.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-dcmulti.opb IDLAUNCH: 3233 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 858412 kB Buffers: 24440 kB Cached: 118796 kB SwapCached: 856 kB Active: 33124 kB Inactive: 112732 kB HighTotal: 131008 kB HighFree: 26768 kB LowTotal: 903652 kB LowFree: 831644 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 24836 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:28:27 (client local time) WITH STATUS 0 IN 1206.68 SECONDS stats: 3233 7 1206.68 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/27721/stat): 27721 (minisat+_script) R 27720 27721 31027 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855143117 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27721/statm): 174 3 169 147 0 27 0 [pid=27721] 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=27722 New process pid=27723 New process pid=27724 execve syscall for /bin/sed executable One traced child (pid=27723) 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=27724) exited with status: 0 One traced child (pid=27722) exited with status: 0 New process pid=27725 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-dcmulti.opb [startup+10.0043 s] Raw data (loadavg): 0.93 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9482 0 0 0 917 42 0 0 25 0 1 0 1855143122 40001536 9101 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27725/statm): 9766 9101 145 145 0 9621 0 [pid=27725] vsize: 39064 Current children cumulated CPU time (s) 9.59 Current children cumulated vsize (Kb) 41188 [startup+20.0052 s] Raw data (loadavg): 0.94 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9514 0 0 0 1916 43 0 0 25 0 1 0 1855143122 40128512 9133 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 9797 9133 145 145 0 9652 0 [pid=27725] vsize: 39188 Current children cumulated CPU time (s) 19.59 Current children cumulated vsize (Kb) 41312 [startup+30.0062 s] Raw data (loadavg): 0.95 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9551 0 0 0 2915 43 0 0 25 0 1 0 1855143122 40243200 9170 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27725/statm): 9825 9170 145 145 0 9680 0 [pid=27725] vsize: 39300 Current children cumulated CPU time (s) 29.58 Current children cumulated vsize (Kb) 41424 [startup+40.0071 s] Raw data (loadavg): 0.96 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9598 0 0 0 3914 44 0 0 25 0 1 0 1855143122 40394752 9217 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 9862 9217 145 145 0 9717 0 [pid=27725] vsize: 39448 Current children cumulated CPU time (s) 39.58 Current children cumulated vsize (Kb) 41572 [startup+50.008 s] Raw data (loadavg): 0.96 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9654 0 0 0 4913 45 0 0 25 0 1 0 1855143122 40611840 9273 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 9915 9273 145 145 0 9770 0 [pid=27725] vsize: 39660 Current children cumulated CPU time (s) 49.58 Current children cumulated vsize (Kb) 41784 [startup+60.0089 s] Raw data (loadavg): 0.97 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9715 0 0 0 5912 45 0 0 25 0 1 0 1855143122 40861696 9334 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 9976 9334 145 145 0 9831 0 [pid=27725] vsize: 39904 Current children cumulated CPU time (s) 59.57 Current children cumulated vsize (Kb) 42028 [startup+70.0098 s] Raw data (loadavg): 0.97 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9809 0 0 0 6910 46 0 0 25 0 1 0 1855143122 41234432 9428 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 10067 9428 145 145 0 9922 0 [pid=27725] vsize: 40268 Current children cumulated CPU time (s) 69.56 Current children cumulated vsize (Kb) 42392 [startup+80.0108 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10031 0 0 0 7907 47 0 0 25 0 1 0 1855143122 42172416 9650 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 10296 9650 145 145 0 10151 0 [pid=27725] vsize: 41184 Current children cumulated CPU time (s) 79.54 Current children cumulated vsize (Kb) 43308 [startup+90.0117 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10136 0 0 0 8906 47 0 0 25 0 1 0 1855143122 42586112 9755 4294967295 134512640 135094434 3221224432 3221223024 134557221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 10397 9755 145 145 0 10252 0 [pid=27725] vsize: 41588 Current children cumulated CPU time (s) 89.53 Current children cumulated vsize (Kb) 43712 [startup+100.013 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10451 0 0 0 9901 49 0 0 25 0 1 0 1855143122 43843584 10070 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 10704 10070 145 145 0 10559 0 [pid=27725] vsize: 42816 Current children cumulated CPU time (s) 99.5 Current children cumulated vsize (Kb) 44940 [startup+110.014 s] Raw data (loadavg): 0.98 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10816 0 0 0 10895 52 0 0 25 0 1 0 1855143122 45441024 10435 4294967295 134512640 135094434 3221224432 3221223096 134550365 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 11094 10435 145 145 0 10949 0 [pid=27725] vsize: 44376 Current children cumulated CPU time (s) 109.47 Current children cumulated vsize (Kb) 46500 [startup+120.014 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 11194 0 0 0 11888 56 0 0 25 0 1 0 1855143122 46956544 10813 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 11464 10813 145 145 0 11319 0 [pid=27725] vsize: 45856 Current children cumulated CPU time (s) 119.44 Current children cumulated vsize (Kb) 47980 [startup+130.015 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 11584 0 0 0 12882 58 0 0 25 0 1 0 1855143122 48521216 11203 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 11846 11203 145 145 0 11701 0 [pid=27725] vsize: 47384 Current children cumulated CPU time (s) 129.4 Current children cumulated vsize (Kb) 49508 [startup+140.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 11968 0 0 0 13875 61 0 0 25 0 1 0 1855143122 50069504 11587 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 12224 11587 145 145 0 12079 0 [pid=27725] vsize: 48896 Current children cumulated CPU time (s) 139.36 Current children cumulated vsize (Kb) 51020 [startup+150.017 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 12423 0 0 0 14868 63 0 0 25 0 1 0 1855143122 52166656 12042 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 12736 12042 145 145 0 12591 0 [pid=27725] vsize: 50944 Current children cumulated CPU time (s) 149.31 Current children cumulated vsize (Kb) 53068 [startup+160.018 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 12738 0 0 0 15863 65 0 0 25 0 1 0 1855143122 53432320 12357 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 13045 12357 145 145 0 12900 0 [pid=27725] vsize: 52180 Current children cumulated CPU time (s) 159.28 Current children cumulated vsize (Kb) 54304 [startup+170.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 12884 0 0 0 16861 67 0 0 25 0 1 0 1855143122 54018048 12503 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 13188 12503 145 145 0 13043 0 [pid=27725] vsize: 52752 Current children cumulated CPU time (s) 169.28 Current children cumulated vsize (Kb) 54876 [startup+180.019 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13038 0 0 0 17859 67 0 0 25 0 1 0 1855143122 54632448 12657 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 13338 12657 145 145 0 13193 0 [pid=27725] vsize: 53352 Current children cumulated CPU time (s) 179.26 Current children cumulated vsize (Kb) 55476 [startup+190.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13307 0 0 0 18854 69 0 0 25 0 1 0 1855143122 55717888 12926 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27725/statm): 13603 12926 145 145 0 13458 0 [pid=27725] vsize: 54412 Current children cumulated CPU time (s) 189.23 Current children cumulated vsize (Kb) 56536 [startup+200.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13538 0 0 0 19850 70 0 0 25 0 1 0 1855143122 56643584 13157 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 13829 13157 145 145 0 13684 0 [pid=27725] vsize: 55316 Current children cumulated CPU time (s) 199.2 Current children cumulated vsize (Kb) 57440 [startup+210.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13741 0 0 0 20846 71 0 0 25 0 1 0 1855143122 57458688 13360 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 14028 13360 145 145 0 13883 0 [pid=27725] vsize: 56112 Current children cumulated CPU time (s) 209.17 Current children cumulated vsize (Kb) 58236 [startup+220.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13943 0 0 0 21843 73 0 0 25 0 1 0 1855143122 58261504 13562 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 14224 13562 145 145 0 14079 0 [pid=27725] vsize: 56896 Current children cumulated CPU time (s) 219.16 Current children cumulated vsize (Kb) 59020 [startup+230.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 14236 0 0 0 22837 74 0 0 25 0 1 0 1855143122 59437056 13855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 14511 13855 145 145 0 14366 0 [pid=27725] vsize: 58044 Current children cumulated CPU time (s) 229.11 Current children cumulated vsize (Kb) 60168 [startup+240.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 14644 0 0 0 23829 76 0 0 25 0 1 0 1855143122 61079552 14263 4294967295 134512640 135094434 3221224432 3221223088 134561688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 14912 14263 145 145 0 14767 0 [pid=27725] vsize: 59648 Current children cumulated CPU time (s) 239.05 Current children cumulated vsize (Kb) 61772 [startup+250.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 14948 0 0 0 24824 78 0 0 25 0 1 0 1855143122 62300160 14567 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 15210 14567 145 145 0 15065 0 [pid=27725] vsize: 60840 Current children cumulated CPU time (s) 249.02 Current children cumulated vsize (Kb) 62964 [startup+260.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 15236 0 0 0 25819 80 0 0 25 0 1 0 1855143122 63459328 14855 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 15493 14855 145 145 0 15348 0 [pid=27725] vsize: 61972 Current children cumulated CPU time (s) 258.99 Current children cumulated vsize (Kb) 64096 [startup+270.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 15481 0 0 0 26814 82 0 0 25 0 1 0 1855143122 64446464 15100 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 15734 15100 145 145 0 15589 0 [pid=27725] vsize: 62936 Current children cumulated CPU time (s) 268.96 Current children cumulated vsize (Kb) 65060 [startup+280.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 15894 0 0 0 27808 84 0 0 25 0 1 0 1855143122 66633728 15513 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 16268 15513 145 145 0 16123 0 [pid=27725] vsize: 65072 Current children cumulated CPU time (s) 278.92 Current children cumulated vsize (Kb) 67196 [startup+290.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 16402 0 0 0 28800 88 0 0 25 0 1 0 1855143122 68685824 16021 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 16769 16021 145 145 0 16624 0 [pid=27725] vsize: 67076 Current children cumulated CPU time (s) 288.88 Current children cumulated vsize (Kb) 69200 [startup+300.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 16724 0 0 0 29794 90 0 0 25 0 1 0 1855143122 69980160 16343 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 17085 16343 145 145 0 16940 0 [pid=27725] vsize: 68340 Current children cumulated CPU time (s) 298.84 Current children cumulated vsize (Kb) 70464 [startup+310.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 16990 0 0 0 30790 92 0 0 25 0 1 0 1855143122 71049216 16609 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 17346 16609 145 145 0 17201 0 [pid=27725] vsize: 69384 Current children cumulated CPU time (s) 308.82 Current children cumulated vsize (Kb) 71508 [startup+320.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 17278 0 0 0 31784 94 0 0 25 0 1 0 1855143122 72204288 16897 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 17628 16897 145 145 0 17483 0 [pid=27725] vsize: 70512 Current children cumulated CPU time (s) 318.78 Current children cumulated vsize (Kb) 72636 [startup+330.032 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 17465 0 0 0 32781 96 0 0 25 0 1 0 1855143122 72949760 17084 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 17810 17084 145 145 0 17665 0 [pid=27725] vsize: 71240 Current children cumulated CPU time (s) 328.77 Current children cumulated vsize (Kb) 73364 [startup+340.033 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 17691 0 0 0 33777 98 0 0 25 0 1 0 1855143122 73854976 17310 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 18031 17310 145 145 0 17886 0 [pid=27725] vsize: 72124 Current children cumulated CPU time (s) 338.75 Current children cumulated vsize (Kb) 74248 [startup+350.034 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) T 27721 27721 31027 0 -1 0 18016 0 0 0 34773 99 0 0 25 0 1 0 1855143122 75169792 17635 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27725/statm): 18352 17635 145 145 0 18207 0 [pid=27725] vsize: 73408 Current children cumulated CPU time (s) 348.72 Current children cumulated vsize (Kb) 75532 [startup+360.036 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 18178 0 0 0 35771 100 0 0 25 0 1 0 1855143122 75821056 17797 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 18511 17797 145 145 0 18366 0 [pid=27725] vsize: 74044 Current children cumulated CPU time (s) 358.71 Current children cumulated vsize (Kb) 76168 [startup+370.037 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 18345 0 0 0 36768 102 0 0 25 0 1 0 1855143122 76492800 17964 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 18675 17964 145 145 0 18530 0 [pid=27725] vsize: 74700 Current children cumulated CPU time (s) 368.7 Current children cumulated vsize (Kb) 76824 [startup+380.038 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 18749 0 0 0 37761 105 0 0 25 0 1 0 1855143122 78114816 18368 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 19071 18368 145 145 0 18926 0 [pid=27725] vsize: 76284 Current children cumulated CPU time (s) 378.66 Current children cumulated vsize (Kb) 78408 [startup+390.04 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19072 0 0 0 38755 107 0 0 25 0 1 0 1855143122 79421440 18691 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 19390 18691 145 145 0 19245 0 [pid=27725] vsize: 77560 Current children cumulated CPU time (s) 388.62 Current children cumulated vsize (Kb) 79684 [startup+400.039 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19375 0 0 0 39749 110 0 0 25 0 1 0 1855143122 80642048 18994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 19688 18994 145 145 0 19543 0 [pid=27725] vsize: 78752 Current children cumulated CPU time (s) 398.59 Current children cumulated vsize (Kb) 80876 [startup+410.04 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19714 0 0 0 40743 113 0 0 25 0 1 0 1855143122 82010112 19333 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 20022 19333 145 145 0 19877 0 [pid=27725] vsize: 80088 Current children cumulated CPU time (s) 408.56 Current children cumulated vsize (Kb) 82212 [startup+420.041 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19923 0 0 0 41741 114 0 0 25 0 1 0 1855143122 82849792 19542 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 20227 19542 145 145 0 20082 0 [pid=27725] vsize: 80908 Current children cumulated CPU time (s) 418.55 Current children cumulated vsize (Kb) 83032 [startup+430.042 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 20294 0 0 0 42734 116 0 0 25 0 1 0 1855143122 84340736 19913 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 20591 19913 145 145 0 20446 0 [pid=27725] vsize: 82364 Current children cumulated CPU time (s) 428.5 Current children cumulated vsize (Kb) 84488 [startup+440.043 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 20638 0 0 0 43728 120 0 0 25 0 1 0 1855143122 85721088 20257 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 20928 20257 145 145 0 20783 0 [pid=27725] vsize: 83712 Current children cumulated CPU time (s) 438.48 Current children cumulated vsize (Kb) 85836 [startup+450.044 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 20908 0 0 0 44724 122 0 0 25 0 1 0 1855143122 86810624 20527 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 21194 20527 145 145 0 21049 0 [pid=27725] vsize: 84776 Current children cumulated CPU time (s) 448.46 Current children cumulated vsize (Kb) 86900 [startup+460.045 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21073 0 0 0 45722 123 0 0 25 0 1 0 1855143122 87470080 20692 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 21355 20692 145 145 0 21210 0 [pid=27725] vsize: 85420 Current children cumulated CPU time (s) 458.45 Current children cumulated vsize (Kb) 87544 [startup+470.046 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21351 0 0 0 46717 124 0 0 25 0 1 0 1855143122 88584192 20970 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 21627 20970 145 145 0 21482 0 [pid=27725] vsize: 86508 Current children cumulated CPU time (s) 468.41 Current children cumulated vsize (Kb) 88632 [startup+480.047 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21698 0 0 0 47711 127 0 0 25 0 1 0 1855143122 89980928 21317 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 21968 21317 145 145 0 21823 0 [pid=27725] vsize: 87872 Current children cumulated CPU time (s) 478.38 Current children cumulated vsize (Kb) 89996 [startup+490.048 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21984 0 0 0 48706 130 0 0 25 0 1 0 1855143122 91140096 21603 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 22251 21603 145 145 0 22106 0 [pid=27725] vsize: 89004 Current children cumulated CPU time (s) 488.36 Current children cumulated vsize (Kb) 91128 [startup+500.05 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22272 0 0 0 49701 133 0 0 25 0 1 0 1855143122 92291072 21891 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 22532 21891 145 145 0 22387 0 [pid=27725] vsize: 90128 Current children cumulated CPU time (s) 498.34 Current children cumulated vsize (Kb) 92252 [startup+510.052 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22544 0 0 0 50696 135 0 0 25 0 1 0 1855143122 94437376 22163 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 23056 22163 145 145 0 22911 0 [pid=27725] vsize: 92224 Current children cumulated CPU time (s) 508.31 Current children cumulated vsize (Kb) 94348 [startup+520.053 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22817 0 0 0 51693 136 0 0 25 0 1 0 1855143122 95535104 22436 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 23324 22436 145 145 0 23179 0 [pid=27725] vsize: 93296 Current children cumulated CPU time (s) 518.29 Current children cumulated vsize (Kb) 95420 [startup+530.053 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22985 0 0 0 52690 137 0 0 25 0 1 0 1855143122 96223232 22604 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 23492 22604 145 145 0 23347 0 [pid=27725] vsize: 93968 Current children cumulated CPU time (s) 528.27 Current children cumulated vsize (Kb) 96092 [startup+540.054 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 23340 0 0 0 53683 140 0 0 25 0 1 0 1855143122 97652736 22959 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 23841 22959 145 145 0 23696 0 [pid=27725] vsize: 95364 Current children cumulated CPU time (s) 538.23 Current children cumulated vsize (Kb) 97488 [startup+550.054 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 23676 0 0 0 54678 142 0 0 25 0 1 0 1855143122 99028992 23295 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 24177 23295 145 145 0 24032 0 [pid=27725] vsize: 96708 Current children cumulated CPU time (s) 548.2 Current children cumulated vsize (Kb) 98832 [startup+560.055 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 23973 0 0 0 55673 145 0 0 25 0 1 0 1855143122 100229120 23592 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 24470 23592 145 145 0 24325 0 [pid=27725] vsize: 97880 Current children cumulated CPU time (s) 558.18 Current children cumulated vsize (Kb) 100004 [startup+570.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24112 0 0 0 56670 146 0 0 25 0 1 0 1855143122 100798464 23731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 24609 23731 145 145 0 24464 0 [pid=27725] vsize: 98436 Current children cumulated CPU time (s) 568.16 Current children cumulated vsize (Kb) 100560 [startup+580.057 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24299 0 0 0 57668 148 0 0 25 0 1 0 1855143122 101548032 23918 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 24792 23918 145 145 0 24647 0 [pid=27725] vsize: 99168 Current children cumulated CPU time (s) 578.16 Current children cumulated vsize (Kb) 101292 [startup+590.058 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24610 0 0 0 58663 150 0 0 25 0 1 0 1855143122 102801408 24229 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 25098 24229 145 145 0 24953 0 [pid=27725] vsize: 100392 Current children cumulated CPU time (s) 588.13 Current children cumulated vsize (Kb) 102516 [startup+600.059 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24968 0 0 0 59656 152 0 0 25 0 1 0 1855143122 104247296 24587 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 25451 24587 145 145 0 25306 0 [pid=27725] vsize: 101804 Current children cumulated CPU time (s) 598.08 Current children cumulated vsize (Kb) 103928 [startup+610.06 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 25355 0 0 0 60648 156 0 0 25 0 1 0 1855143122 105824256 24974 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 25836 24974 145 145 0 25691 0 [pid=27725] vsize: 103344 Current children cumulated CPU time (s) 608.04 Current children cumulated vsize (Kb) 105468 [startup+620.061 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 25552 0 0 0 61645 157 0 0 25 0 1 0 1855143122 106622976 25171 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 26031 25171 145 145 0 25886 0 [pid=27725] vsize: 104124 Current children cumulated CPU time (s) 618.02 Current children cumulated vsize (Kb) 106248 [startup+630.062 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 25734 0 0 0 62643 157 0 0 25 0 1 0 1855143122 107352064 25353 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 26209 25353 145 145 0 26064 0 [pid=27725] vsize: 104836 Current children cumulated CPU time (s) 628 Current children cumulated vsize (Kb) 106960 [startup+640.063 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26016 0 0 0 63638 160 0 0 25 0 1 0 1855143122 108490752 25635 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 26487 25635 145 145 0 26342 0 [pid=27725] vsize: 105948 Current children cumulated CPU time (s) 637.98 Current children cumulated vsize (Kb) 108072 [startup+650.064 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26199 0 0 0 64635 161 0 0 25 0 1 0 1855143122 109228032 25818 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 26667 25818 145 145 0 26522 0 [pid=27725] vsize: 106668 Current children cumulated CPU time (s) 647.96 Current children cumulated vsize (Kb) 108792 [startup+660.064 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26485 0 0 0 65630 163 0 0 25 0 1 0 1855143122 110387200 26104 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 26950 26104 145 145 0 26805 0 [pid=27725] vsize: 107800 Current children cumulated CPU time (s) 657.93 Current children cumulated vsize (Kb) 109924 [startup+670.065 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26808 0 0 0 66624 165 0 0 25 0 1 0 1855143122 111693824 26427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 27269 26427 145 145 0 27124 0 [pid=27725] vsize: 109076 Current children cumulated CPU time (s) 667.89 Current children cumulated vsize (Kb) 111200 [startup+680.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27177 0 0 0 67619 167 0 0 25 0 1 0 1855143122 113147904 26796 4294967295 134512640 135094434 3221224432 3221223056 134562060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 27624 26796 145 145 0 27479 0 [pid=27725] vsize: 110496 Current children cumulated CPU time (s) 677.86 Current children cumulated vsize (Kb) 112620 [startup+690.067 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27455 0 0 0 68615 168 0 0 25 0 1 0 1855143122 114266112 27074 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 27897 27074 145 145 0 27752 0 [pid=27725] vsize: 111588 Current children cumulated CPU time (s) 687.83 Current children cumulated vsize (Kb) 113712 [startup+700.067 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27595 0 0 0 69613 170 0 0 25 0 1 0 1855143122 114819072 27214 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 28032 27214 145 145 0 27887 0 [pid=27725] vsize: 112128 Current children cumulated CPU time (s) 697.83 Current children cumulated vsize (Kb) 114252 [startup+710.069 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27838 0 0 0 70608 171 0 0 22 0 1 0 1855143122 115810304 27457 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 28274 27457 145 145 0 28129 0 [pid=27725] vsize: 113096 Current children cumulated CPU time (s) 707.79 Current children cumulated vsize (Kb) 115220 [startup+720.07 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28118 0 0 0 71604 173 0 0 25 0 1 0 1855143122 116948992 27737 4294967295 134512640 135094434 3221224432 3221223056 134557734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 28552 27737 145 145 0 28407 0 [pid=27725] vsize: 114208 Current children cumulated CPU time (s) 717.77 Current children cumulated vsize (Kb) 116332 [startup+730.07 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28383 0 0 0 72600 175 0 0 25 0 1 0 1855143122 118030336 28002 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 28816 28002 145 145 0 28671 0 [pid=27725] vsize: 115264 Current children cumulated CPU time (s) 727.75 Current children cumulated vsize (Kb) 117388 [startup+740.072 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28687 0 0 0 73594 177 0 0 25 0 1 0 1855143122 119246848 28306 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 29113 28306 145 145 0 28968 0 [pid=27725] vsize: 116452 Current children cumulated CPU time (s) 737.71 Current children cumulated vsize (Kb) 118576 [startup+750.073 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28903 0 0 0 74591 179 0 0 25 0 1 0 1855143122 120115200 28522 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 29325 28522 145 145 0 29180 0 [pid=27725] vsize: 117300 Current children cumulated CPU time (s) 747.7 Current children cumulated vsize (Kb) 119424 [startup+760.074 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29145 0 0 0 75587 180 0 0 25 0 1 0 1855143122 121102336 28764 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 29566 28764 145 145 0 29421 0 [pid=27725] vsize: 118264 Current children cumulated CPU time (s) 757.67 Current children cumulated vsize (Kb) 120388 [startup+770.075 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29402 0 0 0 76582 182 0 0 25 0 1 0 1855143122 122150912 29021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 29822 29021 145 145 0 29677 0 [pid=27725] vsize: 119288 Current children cumulated CPU time (s) 767.64 Current children cumulated vsize (Kb) 121412 [startup+780.076 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29557 0 0 0 77579 184 0 0 25 0 1 0 1855143122 122789888 29176 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 29978 29176 145 145 0 29833 0 [pid=27725] vsize: 119912 Current children cumulated CPU time (s) 777.63 Current children cumulated vsize (Kb) 122036 [startup+790.077 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29734 0 0 0 78577 185 0 0 25 0 1 0 1855143122 123494400 29353 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 30150 29353 145 145 0 30005 0 [pid=27725] vsize: 120600 Current children cumulated CPU time (s) 787.62 Current children cumulated vsize (Kb) 122724 [startup+800.077 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29989 0 0 0 79573 187 0 0 25 0 1 0 1855143122 124518400 29608 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 30400 29608 145 145 0 30255 0 [pid=27725] vsize: 121600 Current children cumulated CPU time (s) 797.6 Current children cumulated vsize (Kb) 123724 [startup+810.079 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30244 0 0 0 80569 189 0 0 25 0 1 0 1855143122 125546496 29863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 30651 29863 145 145 0 30506 0 [pid=27725] vsize: 122604 Current children cumulated CPU time (s) 807.58 Current children cumulated vsize (Kb) 124728 [startup+820.08 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30490 0 0 0 81566 190 0 0 25 0 1 0 1855143122 126533632 30109 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 30892 30109 145 145 0 30747 0 [pid=27725] vsize: 123568 Current children cumulated CPU time (s) 817.56 Current children cumulated vsize (Kb) 125692 [startup+830.08 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30737 0 0 0 82562 191 0 0 25 0 1 0 1855143122 127516672 30356 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 31132 30356 145 145 0 30987 0 [pid=27725] vsize: 124528 Current children cumulated CPU time (s) 827.53 Current children cumulated vsize (Kb) 126652 [startup+840.081 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30853 0 0 0 83560 192 0 0 25 0 1 0 1855143122 127975424 30472 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 31244 30472 145 145 0 31099 0 [pid=27725] vsize: 124976 Current children cumulated CPU time (s) 837.52 Current children cumulated vsize (Kb) 127100 [startup+850.082 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 31150 0 0 0 84556 193 0 0 24 0 1 0 1855143122 129179648 30769 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 31538 30769 145 145 0 31393 0 [pid=27725] vsize: 126152 Current children cumulated CPU time (s) 847.49 Current children cumulated vsize (Kb) 128276 [startup+860.083 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 31482 0 0 0 85550 195 0 0 25 0 1 0 1855143122 130539520 31101 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 31870 31101 145 145 0 31725 0 [pid=27725] vsize: 127480 Current children cumulated CPU time (s) 857.45 Current children cumulated vsize (Kb) 129604 [startup+870.084 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 31791 0 0 0 86545 198 0 0 25 0 1 0 1855143122 131780608 31410 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 32173 31410 145 145 0 32028 0 [pid=27725] vsize: 128692 Current children cumulated CPU time (s) 867.43 Current children cumulated vsize (Kb) 130816 [startup+880.085 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32123 0 0 0 87539 200 0 0 25 0 1 0 1855143122 133148672 31742 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 32507 31742 145 145 0 32362 0 [pid=27725] vsize: 130028 Current children cumulated CPU time (s) 877.39 Current children cumulated vsize (Kb) 132152 [startup+890.086 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32402 0 0 0 88533 203 0 0 25 0 1 0 1855143122 134295552 32021 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 32787 32021 145 145 0 32642 0 [pid=27725] vsize: 131148 Current children cumulated CPU time (s) 887.36 Current children cumulated vsize (Kb) 133272 [startup+900.087 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32628 0 0 0 89529 205 0 0 25 0 1 0 1855143122 135204864 32247 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 33009 32247 145 145 0 32864 0 [pid=27725] vsize: 132036 Current children cumulated CPU time (s) 897.34 Current children cumulated vsize (Kb) 134160 [startup+910.089 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32874 0 0 0 90523 207 0 0 25 0 1 0 1855143122 136200192 32493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 33252 32493 145 145 0 33107 0 [pid=27725] vsize: 133008 Current children cumulated CPU time (s) 907.3 Current children cumulated vsize (Kb) 135132 [startup+920.09 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32988 0 0 0 91522 209 0 0 25 0 1 0 1855143122 136679424 32607 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 33369 32607 145 145 0 33224 0 [pid=27725] vsize: 133476 Current children cumulated CPU time (s) 917.31 Current children cumulated vsize (Kb) 135600 [startup+930.091 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33225 0 0 0 92518 210 0 0 25 0 1 0 1855143122 137629696 32844 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 33601 32844 145 145 0 33456 0 [pid=27725] vsize: 134404 Current children cumulated CPU time (s) 927.28 Current children cumulated vsize (Kb) 136528 [startup+940.091 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33362 0 0 0 93517 211 0 0 25 0 1 0 1855143122 138215424 32981 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 33744 32981 145 145 0 33599 0 [pid=27725] vsize: 134976 Current children cumulated CPU time (s) 937.28 Current children cumulated vsize (Kb) 137100 [startup+950.092 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33502 0 0 0 94515 212 0 0 25 0 1 0 1855143122 138788864 33121 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 33884 33121 145 145 0 33739 0 [pid=27725] vsize: 135536 Current children cumulated CPU time (s) 947.27 Current children cumulated vsize (Kb) 137660 [startup+960.093 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33696 0 0 0 95512 213 0 0 25 0 1 0 1855143122 139575296 33315 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 34076 33315 145 145 0 33931 0 [pid=27725] vsize: 136304 Current children cumulated CPU time (s) 957.25 Current children cumulated vsize (Kb) 138428 [startup+970.094 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34073 0 0 0 96507 216 0 0 25 0 1 0 1855143122 141082624 33692 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 34444 33692 145 145 0 34299 0 [pid=27725] vsize: 137776 Current children cumulated CPU time (s) 967.23 Current children cumulated vsize (Kb) 139900 [startup+980.095 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34341 0 0 0 97503 218 0 0 25 0 1 0 1855143122 142155776 33960 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 34706 33960 145 145 0 34561 0 [pid=27725] vsize: 138824 Current children cumulated CPU time (s) 977.21 Current children cumulated vsize (Kb) 140948 [startup+990.096 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34388 0 0 0 98502 218 0 0 25 0 1 0 1855143122 142340096 34007 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 34751 34007 145 145 0 34606 0 [pid=27725] vsize: 139004 Current children cumulated CPU time (s) 987.2 Current children cumulated vsize (Kb) 141128 [startup+1000.1 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34576 0 0 0 99499 220 0 0 25 0 1 0 1855143122 143097856 34195 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 34936 34195 145 145 0 34791 0 [pid=27725] vsize: 139744 Current children cumulated CPU time (s) 997.19 Current children cumulated vsize (Kb) 141868 [startup+1010.1 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34904 0 0 0 100492 222 0 0 25 0 1 0 1855143122 144424960 34523 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 35260 34523 145 145 0 35115 0 [pid=27725] vsize: 141040 Current children cumulated CPU time (s) 1007.14 Current children cumulated vsize (Kb) 143164 [startup+1020.1 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 35269 0 0 0 101486 225 0 0 25 0 1 0 1855143122 145924096 34888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 35626 34888 145 145 0 35481 0 [pid=27725] vsize: 142504 Current children cumulated CPU time (s) 1017.11 Current children cumulated vsize (Kb) 144628 [startup+1030.1 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 35586 0 0 0 102481 226 0 0 25 0 1 0 1855143122 147197952 35205 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 35937 35205 145 145 0 35792 0 [pid=27725] vsize: 143748 Current children cumulated CPU time (s) 1027.07 Current children cumulated vsize (Kb) 145872 [startup+1040.1 s] Raw data (loadavg): 0.99 0.98 0.92 1/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) T 27721 27721 31027 0 -1 0 36084 0 0 0 103472 231 0 0 25 0 1 0 1855143122 149209088 35703 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27725/statm): 36428 35703 145 145 0 36283 0 [pid=27725] vsize: 145712 Current children cumulated CPU time (s) 1037.03 Current children cumulated vsize (Kb) 147836 [startup+1050.1 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 36239 0 0 0 104469 232 0 0 25 0 1 0 1855143122 149843968 35858 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 36583 35858 145 145 0 36438 0 [pid=27725] vsize: 146332 Current children cumulated CPU time (s) 1047.01 Current children cumulated vsize (Kb) 148456 [startup+1060.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 36589 0 0 0 105462 235 0 0 25 0 1 0 1855143122 151261184 36208 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 36929 36208 145 145 0 36784 0 [pid=27725] vsize: 147716 Current children cumulated CPU time (s) 1056.97 Current children cumulated vsize (Kb) 149840 [startup+1070.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 37163 0 0 0 106452 238 0 0 25 0 1 0 1855143122 153595904 36782 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 37499 36782 145 145 0 37354 0 [pid=27725] vsize: 149996 Current children cumulated CPU time (s) 1066.9 Current children cumulated vsize (Kb) 152120 [startup+1080.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 37629 0 0 0 107443 242 0 0 24 0 1 0 1855143122 155484160 37248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 37960 37248 145 145 0 37815 0 [pid=27725] vsize: 151840 Current children cumulated CPU time (s) 1076.85 Current children cumulated vsize (Kb) 153964 [startup+1090.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 37893 0 0 0 108440 244 0 0 25 0 1 0 1855143122 156549120 37512 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 38220 37512 145 145 0 38075 0 [pid=27725] vsize: 152880 Current children cumulated CPU time (s) 1086.84 Current children cumulated vsize (Kb) 155004 [startup+1100.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38083 0 0 0 109436 245 0 0 25 0 1 0 1855143122 157298688 37702 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 38403 37702 145 145 0 38258 0 [pid=27725] vsize: 153612 Current children cumulated CPU time (s) 1096.81 Current children cumulated vsize (Kb) 155736 [startup+1110.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38252 0 0 0 110434 246 0 0 22 0 1 0 1855143122 157974528 37871 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 38568 37871 145 145 0 38423 0 [pid=27725] vsize: 154272 Current children cumulated CPU time (s) 1106.8 Current children cumulated vsize (Kb) 156396 [startup+1120.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38634 0 0 0 111428 249 0 0 25 0 1 0 1855143122 161611776 38253 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 39456 38253 145 145 0 39311 0 [pid=27725] vsize: 157824 Current children cumulated CPU time (s) 1116.77 Current children cumulated vsize (Kb) 159948 [startup+1130.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38890 0 0 0 112423 251 0 0 25 0 1 0 1855143122 162639872 38509 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 39707 38509 145 145 0 39562 0 [pid=27725] vsize: 158828 Current children cumulated CPU time (s) 1126.74 Current children cumulated vsize (Kb) 160952 [startup+1140.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39061 0 0 0 113420 252 0 0 25 0 1 0 1855143122 163323904 38680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 39874 38680 145 145 0 39729 0 [pid=27725] vsize: 159496 Current children cumulated CPU time (s) 1136.72 Current children cumulated vsize (Kb) 161620 [startup+1150.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39290 0 0 0 114416 254 0 0 25 0 1 0 1855143122 164245504 38909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 40099 38909 145 145 0 39954 0 [pid=27725] vsize: 160396 Current children cumulated CPU time (s) 1146.7 Current children cumulated vsize (Kb) 162520 [startup+1160.11 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39535 0 0 0 115412 256 0 0 25 0 1 0 1855143122 165236736 39154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 40341 39154 145 145 0 40196 0 [pid=27725] vsize: 161364 Current children cumulated CPU time (s) 1156.68 Current children cumulated vsize (Kb) 163488 [startup+1170.12 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39769 0 0 0 116409 258 0 0 25 0 1 0 1855143122 166187008 39388 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 40573 39388 145 145 0 40428 0 [pid=27725] vsize: 162292 Current children cumulated CPU time (s) 1166.67 Current children cumulated vsize (Kb) 164416 [startup+1180.12 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40005 0 0 0 117405 259 0 0 25 0 1 0 1855143122 167145472 39624 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 40807 39624 145 145 0 40662 0 [pid=27725] vsize: 163228 Current children cumulated CPU time (s) 1176.64 Current children cumulated vsize (Kb) 165352 [startup+1190.12 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40234 0 0 0 118402 261 0 0 25 0 1 0 1855143122 168079360 39853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 41035 39853 145 145 0 40890 0 [pid=27725] vsize: 164140 Current children cumulated CPU time (s) 1186.63 Current children cumulated vsize (Kb) 166264 [startup+1200.12 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40468 0 0 0 119399 262 0 0 25 0 1 0 1855143122 169041920 40087 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 41270 40087 145 145 0 41125 0 [pid=27725] vsize: 165080 Current children cumulated CPU time (s) 1196.61 Current children cumulated vsize (Kb) 167204 [startup+1210.12 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40692 0 0 0 120396 264 0 0 25 0 1 0 1855143122 169943040 40311 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 41490 40311 145 145 0 41345 0 [pid=27725] vsize: 165960 Current children cumulated CPU time (s) 1206.6 Current children cumulated vsize (Kb) 168084 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.98 0.92 2/57 27725 Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27721/statm): 531 226 485 147 0 384 0 [pid=27721] vsize: 2124 Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40692 0 0 0 120396 264 0 0 25 0 1 0 1855143122 169943040 40311 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27725/statm): 41490 40311 145 145 0 41345 0 [pid=27725] vsize: 165960 Current children cumulated CPU time (s) 1206.6 Current children cumulated vsize (Kb) 168084 Sending SIGTERM to -27721 Sleeping 2 seconds One traced child (pid=27721) ended because it received signal 15 (SIGTERM) One traced child (pid=27725) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1206.68 CPU user time (s): 1203.96 CPU system time (s): 2.72059 CPU usage (%): 99.7095 Max. virtual memory (cumulated for all children) (Kb): 168084
ERROR: no interpretation found !