Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-dcmulti.opb |
MD5SUM | 2c1654041c7ed087aa8883df6d85cbf7 |
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 | 14235 |
Biggest coefficient in the objective function | 714038312960 |
Number of bits for the biggest coefficient in the objective function | 40 |
Sum of the numbers in the objective function | 68224730472397 |
Number of bits of the sum of numbers in the objective function | 46 |
Biggest number in a constraint | 714038312960 |
Number of bits of the biggest number in a constraint | 40 |
Biggest sum of numbers in a constraint | 68224730472397 |
Number of bits of the biggest sum of numbers | 46 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 14265 |
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 | 420 |
LAUNCH ON wulflinc1 THE 2005-09-19 03:05:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2850 boxname=wulflinc1 idbench=506 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2c1654041c7ed087aa8883df6d85cbf7 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-dcmulti.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-dcmulti.opb IDLAUNCH: 2850 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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 : 2 cpu MHz : 451.053 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: 835460 kB Buffers: 40256 kB Cached: 128428 kB SwapCached: 908 kB Active: 105820 kB Inactive: 65700 kB HighTotal: 131008 kB HighFree: 9800 kB LowTotal: 903652 kB LowFree: 825660 kB SwapTotal: 2097136 kB SwapFree: 2095620 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5992 kB Slab: 21948 kB Committed_AS: 93168 kB PageTables: 344 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:25:44 (client local time) WITH STATUS 0 IN 1207.43 SECONDS stats: 2850 7 1207.43 0
c Parsing PB file... c Converting 368 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################################################################## c -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss c ---[ 427]---> BDD-cost: 17 c ---[ 426]---> Sorter-cost: 1377 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 425]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 424]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 422]---> BDD-cost: 18 c ---[ 421]---> BDD-cost: 17 c ---[ 420]---> BDD-cost: 17 c ---[ 419]---> BDD-cost: 16 c ---[ 418]---> BDD-cost: 17 c ---[ 416]---> Adder-cost: 523 maxlim: 2097148 bits: 22/21 c ---[ 415]---> BDD-cost: 17 c ---[ 413]---> Adder-cost: 523 maxlim: 1703932 bits: 22/21 c ---[ 411]---> Adder-cost: 523 maxlim: 2097148 bits: 22/21 c ---[ 409]---> Adder-cost: 523 maxlim: 1703932 bits: 22/21 c ---[ 407]---> Adder-cost: 523 maxlim: 2097148 bits: 22/21 c ---[ 405]---> Adder-cost: 523 maxlim: 1703932 bits: 22/21 c ---[ 403]---> Adder-cost: 523 maxlim: 2097148 bits: 22/21 c ---[ 401]---> Adder-cost: 523 maxlim: 1703932 bits: 22/21 c ---[ 399]---> Adder-cost: 523 maxlim: 2097148 bits: 22/21 c ---[ 397]---> Adder-cost: 523 maxlim: 1703932 bits: 22/21 c ---[ 395]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 394]---> BDD-cost: 16 c ---[ 392]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 391]---> BDD-cost: 19 c ---[ 390]---> BDD-cost: 7 c ---[ 389]---> BDD-cost: 18 c ---[ 388]---> BDD-cost: 4 c ---[ 386]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 385]---> BDD-cost: 27 c ---[ 384]---> BDD-cost: 6 c ---[ 381]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 380]---> BDD-cost: 17 c ---[ 378]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 377]---> BDD-cost: 19 c ---[ 376]---> BDD-cost: 7 c ---[ 375]---> BDD-cost: 18 c ---[ 374]---> BDD-cost: 4 c ---[ 372]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> BDD-cost: 26 c ---[ 370]---> BDD-cost: 8 c ---[ 367]---> Sorter-cost: 1113 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 365]---> Adder-cost: 463 maxlim: 1048573 bits: 21/20 c ---[ 363]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 362]---> BDD-cost: 18 c ---[ 361]---> BDD-cost: 6 c ---[ 360]---> BDD-cost: 17 c ---[ 359]---> BDD-cost: 3 c ---[ 357]---> Sorter-cost: 1054 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 356]---> BDD-cost: 26 c ---[ 355]---> BDD-cost: 6 c ---[ 352]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Adder-cost: 463 maxlim: 655357 bits: 21/20 c ---[ 348]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 347]---> BDD-cost: 19 c ---[ 346]---> BDD-cost: 7 c ---[ 345]---> BDD-cost: 18 c ---[ 344]---> BDD-cost: 4 c ---[ 342]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 341]---> BDD-cost: 27 c ---[ 340]---> BDD-cost: 6 c ---[ 337]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 335]---> Adder-cost: 463 maxlim: 1048573 bits: 21/20 c ---[ 333]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 332]---> BDD-cost: 19 c ---[ 331]---> BDD-cost: 7 c ---[ 330]---> BDD-cost: 18 c ---[ 329]---> BDD-cost: 4 c ---[ 327]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> BDD-cost: 22 c ---[ 322]---> BDD-cost: 33 c ---[ 320]---> Adder-cost: 463 maxlim: 655357 bits: 21/20 c ---[ 308]---> Adder-cost: 463 maxlim: 1048573 bits: 21/20 c ---[ 296]---> Adder-cost: 463 maxlim: 655357 bits: 21/20 c ---[ 293]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 292]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 291]---> Sorter-cost: 1551 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 290]---> Sorter-cost: 1377 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 289]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 288]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 286]---> BDD-cost: 18 c ---[ 285]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 283]---> Adder-cost: 463 maxlim: 1048573 bits: 21/20 c ---[ 282]---> BDD-cost: 17 c ---[ 281]---> BDD-cost: 17 c ---[ 280]---> BDD-cost: 16 c ---[ 279]---> BDD-cost: 17 c ---[ 277]---> Adder-cost: 500 maxlim: 3145724 bits: 23/22 c ---[ 275]---> Adder-cost: 500 maxlim: 2752508 bits: 23/22 c ---[ 273]---> Adder-cost: 500 maxlim: 3145724 bits: 23/22 c ---[ 271]---> Adder-cost: 500 maxlim: 2752508 bits: 23/22 c ---[ 269]---> Adder-cost: 500 maxlim: 3145724 bits: 23/22 c ---[ 267]---> Adder-cost: 500 maxlim: 2752508 bits: 23/22 c ---[ 265]---> Adder-cost: 463 maxlim: 655357 bits: 21/20 c ---[ 263]---> Adder-cost: 500 maxlim: 3145724 bits: 23/22 c ---[ 261]---> Adder-cost: 500 maxlim: 2752508 bits: 23/22 c ---[ 259]---> Adder-cost: 500 maxlim: 3145724 bits: 23/22 c ---[ 257]---> Adder-cost: 500 maxlim: 2752508 bits: 23/22 c ---[ 255]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 253]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> BDD-cost: 19 c ---[ 251]---> BDD-cost: 7 c ---[ 250]---> BDD-cost: 18 c ---[ 249]---> BDD-cost: 4 c ---[ 247]---> Adder-cost: 463 maxlim: 1048573 bits: 21/20 c ---[ 245]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 244]---> BDD-cost: 27 c ---[ 243]---> BDD-cost: 6 c ---[ 240]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 238]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 237]---> BDD-cost: 19 c ---[ 236]---> BDD-cost: 7 c ---[ 235]---> BDD-cost: 18 c ---[ 234]---> BDD-cost: 4 c ---[ 232]---> Adder-cost: 463 maxlim: 655357 bits: 21/20 c ---[ 230]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 229]---> BDD-cost: 26 c ---[ 228]---> BDD-cost: 8 c ---[ 225]---> Sorter-cost: 1113 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 223]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 222]---> BDD-cost: 18 c ---[ 221]---> BDD-cost: 6 c ---[ 220]---> BDD-cost: 17 c ---[ 219]---> BDD-cost: 3 c ---[ 217]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 1054 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 214]---> BDD-cost: 26 c ---[ 213]---> BDD-cost: 6 c ---[ 210]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 208]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 207]---> BDD-cost: 19 c ---[ 206]---> BDD-cost: 7 c ---[ 205]---> BDD-cost: 18 c ---[ 204]---> BDD-cost: 4 c ---[ 202]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 200]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> BDD-cost: 27 c ---[ 198]---> BDD-cost: 6 c ---[ 195]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 193]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 192]---> BDD-cost: 19 c ---[ 191]---> BDD-cost: 7 c ---[ 190]---> BDD-cost: 18 c ---[ 189]---> BDD-cost: 4 c ---[ 188]---> BDD-cost: 19 c ---[ 186]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 185]---> BDD-cost: 22 c ---[ 181]---> BDD-cost: 33 c ---[ 175]---> BDD-cost: 7 c ---[ 164]---> BDD-cost: 18 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: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> BDD-cost: 27 c ---[ 146]---> BDD-cost: 6 c ---[ 143]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> BDD-cost: 19 c ---[ 139]---> BDD-cost: 7 c ---[ 138]---> BDD-cost: 18 c ---[ 137]---> BDD-cost: 4 c ---[ 136]---> Sorter-cost: 1551 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 133]---> BDD-cost: 26 c ---[ 132]---> BDD-cost: 8 c ---[ 129]---> Sorter-cost: 1113 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 127]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> BDD-cost: 18 c ---[ 125]---> BDD-cost: 6 c ---[ 124]---> BDD-cost: 17 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> Sorter-cost: 1377 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 1054 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> BDD-cost: 26 c ---[ 118]---> BDD-cost: 6 c ---[ 115]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> BDD-cost: 19 c ---[ 111]---> BDD-cost: 7 c ---[ 110]---> BDD-cost: 18 c ---[ 109]---> BDD-cost: 4 c ---[ 108]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> BDD-cost: 27 c ---[ 104]---> BDD-cost: 6 c ---[ 101]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> BDD-cost: 19 c ---[ 97]---> BDD-cost: 7 c ---[ 96]---> BDD-cost: 18 c ---[ 95]---> BDD-cost: 4 c ---[ 94]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 1115 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> BDD-cost: 22 c ---[ 87]---> BDD-cost: 33 c ---[ 70]---> BDD-cost: 18 c ---[ 62]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 1551 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> BDD-cost: 15 c ---[ 58]---> BDD-cost: 5 c ---[ 57]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 939 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 1039 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 942 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 1054 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 1013 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 952 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 50]---> Sorter-cost: 906 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 965 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 878 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 965 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 1026 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 44]---> Sorter-cost: 939 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 886 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 1100 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> BDD-cost: 15 c ---[ 38]---> BDD-cost: 5 c ---[ 37]---> Sorter-cost: 1003 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 993 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 1013 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 1087 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 1016 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 990 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 939 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Sorter-cost: 980 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 906 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 1087 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 980 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 993 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 1013 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 22]---> Sorter-cost: 939 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 1003 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 19]---> BDD-cost: 5 c ---[ 18]---> Sorter-cost: 919 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> BDD-cost: 15 c ---[ 16]---> Sorter-cost: 822 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> Sorter-cost: 1003 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 14]---> Sorter-cost: 939 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 13]---> Sorter-cost: 1052 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 12]---> Sorter-cost: 980 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 896 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 878 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 980 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 842 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 1100 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 990 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 822 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 952 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 852 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 1]---> Sorter-cost: 1064 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 919 Base: 2 2 2 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 | 407659 1078157 | 135886 0 0 nan | 0.000 % | c | 100 | 407640 1078115 | 149474 99 275 2.8 | 6.241 % | c | 250 | 407421 1077629 | 164422 214 597 2.8 | 6.288 % | c | 476 | 407230 1077203 | 180864 417 1295 3.1 | 6.331 % | c | 814 | 407010 1076714 | 198950 728 2340 3.2 | 6.410 % | c | 1320 | 406574 1075744 | 218845 1162 3846 3.3 | 6.475 % | c | 2079 | 405501 1073358 | 240730 1770 6153 3.5 | 6.717 % | c | 3218 | 404456 1071032 | 264803 2786 9745 3.5 | 6.951 % | c | 4926 | 403134 1068083 | 291283 4259 14929 3.5 | 7.237 % | c | 7488 | 401682 1064841 | 320412 6633 24359 3.7 | 7.552 % | c | 11333 | 400157 1061429 | 352453 10286 45629 4.4 | 7.886 % | c | 17104 | 399646 1060290 | 387698 15961 163733 10.3 | 7.996 % | c | 25753 | 399275 1059467 | 426468 24558 453474 18.5 | 8.080 % | c | 38730 | 398228 1057131 | 469115 37369 866938 23.2 | 8.307 % | c | 58192 | 397042 1054454 | 516026 56692 1511359 26.7 | 8.577 % | c | 87384 | 396904 1054146 | 567629 85866 2730385 31.8 | 8.607 % | c | 131173 | 396253 1052687 | 624392 129572 4392719 33.9 | 8.750 % | c | 196857 | 395205 1050318 | 686831 195116 7086771 36.3 | 8.981 % | c | 295385 | 393580 1046653 | 755514 293406 11407186 38.9 | 9.345 % |
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/7644/stat): 7644 (minisat+_script) R 7643 7644 17733 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1731436297 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/7644/statm): 174 3 169 147 0 27 0 [pid=7644] 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=7645 New process pid=7646 New process pid=7647 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload One traced child (pid=7646) exited with status: 0 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=7647) exited with status: 0 One traced child (pid=7645) exited with status: 0 New process pid=7648 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-dcmulti.opb [startup+10.0034 s] Raw data (loadavg): 0.54 0.76 0.90 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11554 0 0 0 902 41 0 0 25 0 1 0 1731436302 56516608 11160 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 13798 11160 145 145 0 13653 0 [pid=7648] vsize: 55192 Current children cumulated CPU time (s) 9.44 Current children cumulated vsize (Kb) 57316 [startup+20.0051 s] Raw data (loadavg): 0.61 0.77 0.90 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11595 0 0 0 1902 42 0 0 25 0 1 0 1731436302 56672256 11201 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 13836 11201 145 145 0 13691 0 [pid=7648] vsize: 55344 Current children cumulated CPU time (s) 19.45 Current children cumulated vsize (Kb) 57468 [startup+30.0059 s] Raw data (loadavg): 0.67 0.77 0.90 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11615 0 0 0 2901 42 0 0 25 0 1 0 1731436302 56741888 11221 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 13853 11221 145 145 0 13708 0 [pid=7648] vsize: 55412 Current children cumulated CPU time (s) 29.44 Current children cumulated vsize (Kb) 57536 [startup+40.0067 s] Raw data (loadavg): 0.72 0.78 0.90 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11650 0 0 0 3894 42 0 0 25 0 1 0 1731436302 56827904 11256 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 13874 11256 145 145 0 13729 0 [pid=7648] vsize: 55496 Current children cumulated CPU time (s) 39.37 Current children cumulated vsize (Kb) 57620 [startup+50.0075 s] Raw data (loadavg): 0.76 0.79 0.90 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11690 0 0 0 4894 42 0 0 25 0 1 0 1731436302 56975360 11296 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 13910 11296 145 145 0 13765 0 [pid=7648] vsize: 55640 Current children cumulated CPU time (s) 49.37 Current children cumulated vsize (Kb) 57764 [startup+60.0083 s] Raw data (loadavg): 0.80 0.79 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11718 0 0 0 5894 43 0 0 25 0 1 0 1731436302 57065472 11324 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 13932 11324 145 145 0 13787 0 [pid=7648] vsize: 55728 Current children cumulated CPU time (s) 59.38 Current children cumulated vsize (Kb) 57852 [startup+70.0101 s] Raw data (loadavg): 0.83 0.80 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11736 0 0 0 6893 43 0 0 25 0 1 0 1731436302 57135104 11342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 13949 11342 145 145 0 13804 0 [pid=7648] vsize: 55796 Current children cumulated CPU time (s) 69.37 Current children cumulated vsize (Kb) 57920 [startup+80.0109 s] Raw data (loadavg): 0.85 0.81 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11770 0 0 0 7892 44 0 0 25 0 1 0 1731436302 57266176 11376 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 13981 11376 145 145 0 13836 0 [pid=7648] vsize: 55924 Current children cumulated CPU time (s) 79.37 Current children cumulated vsize (Kb) 58048 [startup+90.0117 s] Raw data (loadavg): 0.88 0.81 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11791 0 0 0 8891 45 0 0 25 0 1 0 1731436302 57344000 11397 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 14000 11397 145 145 0 13855 0 [pid=7648] vsize: 56000 Current children cumulated CPU time (s) 89.37 Current children cumulated vsize (Kb) 58124 [startup+100.012 s] Raw data (loadavg): 0.89 0.82 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11908 0 0 0 9889 46 0 0 25 0 1 0 1731436302 57806848 11514 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 14113 11514 145 145 0 13968 0 [pid=7648] vsize: 56452 Current children cumulated CPU time (s) 99.36 Current children cumulated vsize (Kb) 58576 [startup+110.014 s] Raw data (loadavg): 0.91 0.82 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 12214 0 0 0 10885 48 0 0 25 0 1 0 1731436302 59092992 11820 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 14427 11820 145 145 0 14282 0 [pid=7648] vsize: 57708 Current children cumulated CPU time (s) 109.34 Current children cumulated vsize (Kb) 59832 [startup+120.015 s] Raw data (loadavg): 0.92 0.83 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 12437 0 0 0 11881 50 0 0 25 0 1 0 1731436302 59985920 12043 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 14645 12043 145 145 0 14500 0 [pid=7648] vsize: 58580 Current children cumulated CPU time (s) 119.32 Current children cumulated vsize (Kb) 60704 [startup+130.016 s] Raw data (loadavg): 0.93 0.83 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 12765 0 0 0 12876 52 0 0 25 0 1 0 1731436302 61431808 12371 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 14998 12371 145 145 0 14853 0 [pid=7648] vsize: 59992 Current children cumulated CPU time (s) 129.29 Current children cumulated vsize (Kb) 62116 [startup+140.017 s] Raw data (loadavg): 0.94 0.84 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13051 0 0 0 13870 55 0 0 25 0 1 0 1731436302 62578688 12657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 15278 12657 145 145 0 15133 0 [pid=7648] vsize: 61112 Current children cumulated CPU time (s) 139.26 Current children cumulated vsize (Kb) 63236 [startup+150.017 s] Raw data (loadavg): 0.95 0.84 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13313 0 0 0 14866 57 0 0 25 0 1 0 1731436302 63627264 12919 4294967295 134512640 135094434 3221224432 3221223024 134557435 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 15534 12919 145 145 0 15389 0 [pid=7648] vsize: 62136 Current children cumulated CPU time (s) 149.24 Current children cumulated vsize (Kb) 64260 [startup+160.018 s] Raw data (loadavg): 0.96 0.85 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13466 0 0 0 15864 57 0 0 25 0 1 0 1731436302 64237568 13072 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 15683 13072 145 145 0 15538 0 [pid=7648] vsize: 62732 Current children cumulated CPU time (s) 159.22 Current children cumulated vsize (Kb) 64856 [startup+170.019 s] Raw data (loadavg): 0.97 0.85 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13775 0 0 0 16860 59 0 0 25 0 1 0 1731436302 65478656 13381 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 15986 13381 145 145 0 15841 0 [pid=7648] vsize: 63944 Current children cumulated CPU time (s) 169.2 Current children cumulated vsize (Kb) 66068 [startup+180.019 s] Raw data (loadavg): 0.97 0.86 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 14148 0 0 0 17853 62 0 0 25 0 1 0 1731436302 66977792 13754 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 16352 13754 145 145 0 16207 0 [pid=7648] vsize: 65408 Current children cumulated CPU time (s) 179.16 Current children cumulated vsize (Kb) 67532 [startup+190.02 s] Raw data (loadavg): 0.97 0.86 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 14562 0 0 0 18846 64 0 0 25 0 1 0 1731436302 68898816 14168 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 16821 14168 145 145 0 16676 0 [pid=7648] vsize: 67284 Current children cumulated CPU time (s) 189.11 Current children cumulated vsize (Kb) 69408 [startup+200.02 s] Raw data (loadavg): 0.98 0.86 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 15029 0 0 0 19838 67 0 0 25 0 1 0 1731436302 70787072 14635 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 17282 14635 145 145 0 17137 0 [pid=7648] vsize: 69128 Current children cumulated CPU time (s) 199.06 Current children cumulated vsize (Kb) 71252 [startup+210.021 s] Raw data (loadavg): 0.98 0.87 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 15506 0 0 0 20831 69 0 0 25 0 1 0 1731436302 72708096 15112 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 17751 15112 145 145 0 17606 0 [pid=7648] vsize: 71004 Current children cumulated CPU time (s) 209.01 Current children cumulated vsize (Kb) 73128 [startup+220.022 s] Raw data (loadavg): 0.98 0.87 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 15926 0 0 0 21823 73 0 0 25 0 1 0 1731436302 74399744 15532 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 18164 15532 145 145 0 18019 0 [pid=7648] vsize: 72656 Current children cumulated CPU time (s) 218.97 Current children cumulated vsize (Kb) 74780 [startup+230.022 s] Raw data (loadavg): 0.98 0.88 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16153 0 0 0 22819 75 0 0 25 0 1 0 1731436302 75304960 15759 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 18385 15759 145 145 0 18240 0 [pid=7648] vsize: 73540 Current children cumulated CPU time (s) 228.95 Current children cumulated vsize (Kb) 75664 [startup+240.023 s] Raw data (loadavg): 0.99 0.88 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16396 0 0 0 23817 76 0 0 25 0 1 0 1731436302 76279808 16002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 18623 16002 145 145 0 18478 0 [pid=7648] vsize: 74492 Current children cumulated CPU time (s) 238.94 Current children cumulated vsize (Kb) 76616 [startup+250.023 s] Raw data (loadavg): 0.99 0.88 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16658 0 0 0 24812 78 0 0 25 0 1 0 1731436302 77328384 16264 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 18879 16264 145 145 0 18734 0 [pid=7648] vsize: 75516 Current children cumulated CPU time (s) 248.91 Current children cumulated vsize (Kb) 77640 [startup+260.024 s] Raw data (loadavg): 0.99 0.89 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16886 0 0 0 25808 80 0 0 25 0 1 0 1731436302 78237696 16492 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 19101 16492 145 145 0 18956 0 [pid=7648] vsize: 76404 Current children cumulated CPU time (s) 258.89 Current children cumulated vsize (Kb) 78528 [startup+270.025 s] Raw data (loadavg): 0.99 0.89 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17266 0 0 0 26802 83 0 0 25 0 1 0 1731436302 79769600 16872 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 19475 16872 145 145 0 19330 0 [pid=7648] vsize: 77900 Current children cumulated CPU time (s) 268.86 Current children cumulated vsize (Kb) 80024 [startup+280.025 s] Raw data (loadavg): 0.99 0.89 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17535 0 0 0 27798 85 0 0 25 0 1 0 1731436302 81395712 17141 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 19872 17141 145 145 0 19727 0 [pid=7648] vsize: 79488 Current children cumulated CPU time (s) 278.84 Current children cumulated vsize (Kb) 81612 [startup+290.025 s] Raw data (loadavg): 0.99 0.90 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17752 0 0 0 28794 87 0 0 25 0 1 0 1731436302 82268160 17358 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 20085 17358 145 145 0 19940 0 [pid=7648] vsize: 80340 Current children cumulated CPU time (s) 288.82 Current children cumulated vsize (Kb) 82464 [startup+300.026 s] Raw data (loadavg): 0.99 0.90 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17871 0 0 0 29792 88 0 0 25 0 1 0 1731436302 82743296 17477 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 20201 17477 145 145 0 20056 0 [pid=7648] vsize: 80804 Current children cumulated CPU time (s) 298.81 Current children cumulated vsize (Kb) 82928 [startup+310.028 s] Raw data (loadavg): 0.99 0.90 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 18075 0 0 0 30789 89 0 0 25 0 1 0 1731436302 83562496 17681 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 20401 17681 145 145 0 20256 0 [pid=7648] vsize: 81604 Current children cumulated CPU time (s) 308.79 Current children cumulated vsize (Kb) 83728 [startup+320.029 s] Raw data (loadavg): 0.99 0.90 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 18345 0 0 0 31785 91 0 0 25 0 1 0 1731436302 84647936 17951 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/7648/statm): 20666 17951 145 145 0 20521 0 [pid=7648] vsize: 82664 Current children cumulated CPU time (s) 318.77 Current children cumulated vsize (Kb) 84788 [startup+330.029 s] Raw data (loadavg): 0.99 0.91 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 18670 0 0 0 32779 94 0 0 25 0 1 0 1731436302 85966848 18276 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 20988 18276 145 145 0 20843 0 [pid=7648] vsize: 83952 Current children cumulated CPU time (s) 328.74 Current children cumulated vsize (Kb) 86076 [startup+340.029 s] Raw data (loadavg): 0.99 0.91 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 18817 0 0 0 33776 95 0 0 25 0 1 0 1731436302 86548480 18423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 21130 18423 145 145 0 20985 0 [pid=7648] vsize: 84520 Current children cumulated CPU time (s) 338.72 Current children cumulated vsize (Kb) 86644 [startup+350.03 s] Raw data (loadavg): 0.99 0.91 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 19127 0 0 0 34772 97 0 0 25 0 1 0 1731436302 87793664 18733 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 21434 18733 145 145 0 21289 0 [pid=7648] vsize: 85736 Current children cumulated CPU time (s) 348.7 Current children cumulated vsize (Kb) 87860 [startup+360.031 s] Raw data (loadavg): 0.99 0.91 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 19372 0 0 0 35767 98 0 0 25 0 1 0 1731436302 88776704 18978 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/7648/statm): 21674 18978 145 145 0 21529 0 [pid=7648] vsize: 86696 Current children cumulated CPU time (s) 358.66 Current children cumulated vsize (Kb) 88820 [startup+370.032 s] Raw data (loadavg): 0.99 0.92 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 19681 0 0 0 36762 101 0 0 25 0 1 0 1731436302 90021888 19287 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 21978 19287 145 145 0 21833 0 [pid=7648] vsize: 87912 Current children cumulated CPU time (s) 368.64 Current children cumulated vsize (Kb) 90036 [startup+380.032 s] Raw data (loadavg): 0.99 0.92 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20000 0 0 0 37757 103 0 0 25 0 1 0 1731436302 91324416 19606 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 22296 19606 145 145 0 22151 0 [pid=7648] vsize: 89184 Current children cumulated CPU time (s) 378.61 Current children cumulated vsize (Kb) 91308 [startup+390.032 s] Raw data (loadavg): 0.99 0.92 0.91 1/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 20284 0 0 0 38753 105 0 0 25 0 1 0 1731436302 92475392 19890 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/7648/statm): 22577 19890 145 145 0 22432 0 [pid=7648] vsize: 90308 Current children cumulated CPU time (s) 388.59 Current children cumulated vsize (Kb) 92432 [startup+400.033 s] Raw data (loadavg): 0.99 0.92 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20554 0 0 0 39749 106 0 0 25 0 1 0 1731436302 93601792 20160 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 22852 20160 145 145 0 22707 0 [pid=7648] vsize: 91408 Current children cumulated CPU time (s) 398.56 Current children cumulated vsize (Kb) 93532 [startup+410.034 s] Raw data (loadavg): 0.99 0.92 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20814 0 0 0 40744 108 0 0 25 0 1 0 1731436302 94646272 20420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 23107 20420 145 145 0 22962 0 [pid=7648] vsize: 92428 Current children cumulated CPU time (s) 408.53 Current children cumulated vsize (Kb) 94552 [startup+420.035 s] Raw data (loadavg): 0.99 0.93 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20853 0 0 0 41743 108 0 0 25 0 1 0 1731436302 94826496 20459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 23151 20459 145 145 0 23006 0 [pid=7648] vsize: 92604 Current children cumulated CPU time (s) 418.52 Current children cumulated vsize (Kb) 94728 [startup+430.036 s] Raw data (loadavg): 0.99 0.93 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20957 0 0 0 42742 109 0 0 25 0 1 0 1731436302 95268864 20563 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 23259 20563 145 145 0 23114 0 [pid=7648] vsize: 93036 Current children cumulated CPU time (s) 428.52 Current children cumulated vsize (Kb) 95160 [startup+440.036 s] Raw data (loadavg): 0.99 0.93 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21198 0 0 0 43737 111 0 0 25 0 1 0 1731436302 96272384 20804 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 23504 20804 145 145 0 23359 0 [pid=7648] vsize: 94016 Current children cumulated CPU time (s) 438.49 Current children cumulated vsize (Kb) 96140 [startup+450.037 s] Raw data (loadavg): 0.99 0.93 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21402 0 0 0 44735 111 0 0 25 0 1 0 1731436302 97091584 21008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 23704 21008 145 145 0 23559 0 [pid=7648] vsize: 94816 Current children cumulated CPU time (s) 448.47 Current children cumulated vsize (Kb) 96940 [startup+460.038 s] Raw data (loadavg): 0.99 0.93 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21637 0 0 0 45730 113 0 0 25 0 1 0 1731436302 98041856 21243 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 23936 21243 145 145 0 23791 0 [pid=7648] vsize: 95744 Current children cumulated CPU time (s) 458.44 Current children cumulated vsize (Kb) 97868 [startup+470.039 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21814 0 0 0 46728 115 0 0 25 0 1 0 1731436302 98750464 21420 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 24109 21420 145 145 0 23964 0 [pid=7648] vsize: 96436 Current children cumulated CPU time (s) 468.44 Current children cumulated vsize (Kb) 98560 [startup+480.038 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22021 0 0 0 47724 117 0 0 25 0 1 0 1731436302 99594240 21627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 24315 21627 145 145 0 24170 0 [pid=7648] vsize: 97260 Current children cumulated CPU time (s) 478.42 Current children cumulated vsize (Kb) 99384 [startup+490.04 s] Raw data (loadavg): 1.15 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22235 0 0 0 48720 119 0 0 25 0 1 0 1731436302 100474880 21841 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 24530 21841 145 145 0 24385 0 [pid=7648] vsize: 98120 Current children cumulated CPU time (s) 488.4 Current children cumulated vsize (Kb) 100244 [startup+500.041 s] Raw data (loadavg): 1.12 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22386 0 0 0 49719 120 0 0 25 0 1 0 1731436302 101097472 21992 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 24682 21992 145 145 0 24537 0 [pid=7648] vsize: 98728 Current children cumulated CPU time (s) 498.4 Current children cumulated vsize (Kb) 100852 [startup+510.041 s] Raw data (loadavg): 1.10 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22638 0 0 0 50713 122 0 0 25 0 1 0 1731436302 102109184 22244 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 24929 22244 145 145 0 24784 0 [pid=7648] vsize: 99716 Current children cumulated CPU time (s) 508.36 Current children cumulated vsize (Kb) 101840 [startup+520.042 s] Raw data (loadavg): 1.09 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22918 0 0 0 51709 125 0 0 25 0 1 0 1731436302 103231488 22524 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 25203 22524 145 145 0 25058 0 [pid=7648] vsize: 100812 Current children cumulated CPU time (s) 518.35 Current children cumulated vsize (Kb) 102936 [startup+530.042 s] Raw data (loadavg): 1.07 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23068 0 0 0 52706 126 0 0 25 0 1 0 1731436302 103849984 22674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 25354 22674 145 145 0 25209 0 [pid=7648] vsize: 101416 Current children cumulated CPU time (s) 528.33 Current children cumulated vsize (Kb) 103540 [startup+540.043 s] Raw data (loadavg): 1.06 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23361 0 0 0 53700 128 0 0 25 0 1 0 1731436302 105037824 22967 4294967295 134512640 135094434 3221224432 3221223056 134562068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 25644 22967 145 145 0 25499 0 [pid=7648] vsize: 102576 Current children cumulated CPU time (s) 538.29 Current children cumulated vsize (Kb) 104700 [startup+550.044 s] Raw data (loadavg): 1.05 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23564 0 0 0 54697 130 0 0 25 0 1 0 1731436302 105852928 23170 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 25843 23170 145 145 0 25698 0 [pid=7648] vsize: 103372 Current children cumulated CPU time (s) 548.28 Current children cumulated vsize (Kb) 105496 [startup+560.045 s] Raw data (loadavg): 1.04 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23836 0 0 0 55692 132 0 0 25 0 1 0 1731436302 106950656 23442 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 26111 23442 145 145 0 25966 0 [pid=7648] vsize: 104444 Current children cumulated CPU time (s) 558.25 Current children cumulated vsize (Kb) 106568 [startup+570.046 s] Raw data (loadavg): 1.04 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24156 0 0 0 56687 134 0 0 25 0 1 0 1731436302 108240896 23762 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 26426 23762 145 145 0 26281 0 [pid=7648] vsize: 105704 Current children cumulated CPU time (s) 568.22 Current children cumulated vsize (Kb) 107828 [startup+580.045 s] Raw data (loadavg): 1.03 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24458 0 0 0 57683 136 0 0 25 0 1 0 1731436302 109486080 24064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 26730 24064 145 145 0 26585 0 [pid=7648] vsize: 106920 Current children cumulated CPU time (s) 578.2 Current children cumulated vsize (Kb) 109044 [startup+590.046 s] Raw data (loadavg): 1.03 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24600 0 0 0 58681 137 0 0 25 0 1 0 1731436302 110063616 24206 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 26871 24206 145 145 0 26726 0 [pid=7648] vsize: 107484 Current children cumulated CPU time (s) 588.19 Current children cumulated vsize (Kb) 109608 [startup+600.047 s] Raw data (loadavg): 1.02 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24757 0 0 0 59678 139 0 0 25 0 1 0 1731436302 111751168 24363 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 27283 24363 145 145 0 27138 0 [pid=7648] vsize: 109132 Current children cumulated CPU time (s) 598.18 Current children cumulated vsize (Kb) 111256 [startup+610.048 s] Raw data (loadavg): 1.02 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24901 0 0 0 60676 140 0 0 25 0 1 0 1731436302 112353280 24507 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 27430 24507 145 145 0 27285 0 [pid=7648] vsize: 109720 Current children cumulated CPU time (s) 608.17 Current children cumulated vsize (Kb) 111844 [startup+620.048 s] Raw data (loadavg): 1.01 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24967 0 0 0 61675 141 0 0 25 0 1 0 1731436302 112603136 24573 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 27491 24573 145 145 0 27346 0 [pid=7648] vsize: 109964 Current children cumulated CPU time (s) 618.17 Current children cumulated vsize (Kb) 112088 [startup+630.049 s] Raw data (loadavg): 1.01 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25085 0 0 0 62673 141 0 0 25 0 1 0 1731436302 113090560 24691 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 27610 24691 145 145 0 27465 0 [pid=7648] vsize: 110440 Current children cumulated CPU time (s) 628.15 Current children cumulated vsize (Kb) 112564 [startup+640.05 s] Raw data (loadavg): 1.01 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25300 0 0 0 63670 143 0 0 25 0 1 0 1731436302 113954816 24906 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 27821 24906 145 145 0 27676 0 [pid=7648] vsize: 111284 Current children cumulated CPU time (s) 638.14 Current children cumulated vsize (Kb) 113408 [startup+650.051 s] Raw data (loadavg): 1.01 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25514 0 0 0 64666 145 0 0 25 0 1 0 1731436302 114810880 25120 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 28030 25120 145 145 0 27885 0 [pid=7648] vsize: 112120 Current children cumulated CPU time (s) 648.12 Current children cumulated vsize (Kb) 114244 [startup+660.051 s] Raw data (loadavg): 1.01 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25755 0 0 0 65661 147 0 0 25 0 1 0 1731436302 115789824 25361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 28269 25361 145 145 0 28124 0 [pid=7648] vsize: 113076 Current children cumulated CPU time (s) 658.09 Current children cumulated vsize (Kb) 115200 [startup+670.051 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25975 0 0 0 66656 150 0 0 25 0 1 0 1731436302 116678656 25581 4294967295 134512640 135094434 3221224432 3221223104 134555553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 28486 25581 145 145 0 28341 0 [pid=7648] vsize: 113944 Current children cumulated CPU time (s) 668.07 Current children cumulated vsize (Kb) 116068 [startup+680.051 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26128 0 0 0 67654 150 0 0 25 0 1 0 1731436302 117293056 25734 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 28636 25734 145 145 0 28491 0 [pid=7648] vsize: 114544 Current children cumulated CPU time (s) 678.05 Current children cumulated vsize (Kb) 116668 [startup+690.052 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26290 0 0 0 68650 151 0 0 25 0 1 0 1731436302 117952512 25896 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7648/statm): 28797 25896 145 145 0 28652 0 [pid=7648] vsize: 115188 Current children cumulated CPU time (s) 688.02 Current children cumulated vsize (Kb) 117312 [startup+700.053 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26428 0 0 0 69647 153 0 0 25 0 1 0 1731436302 118505472 26034 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 28932 26034 145 145 0 28787 0 [pid=7648] vsize: 115728 Current children cumulated CPU time (s) 698.01 Current children cumulated vsize (Kb) 117852 [startup+710.053 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26584 0 0 0 70644 154 0 0 25 0 1 0 1731436302 119136256 26190 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 29086 26190 145 145 0 28941 0 [pid=7648] vsize: 116344 Current children cumulated CPU time (s) 707.99 Current children cumulated vsize (Kb) 118468 [startup+720.053 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26759 0 0 0 71641 156 0 0 25 0 1 0 1731436302 119836672 26365 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 29257 26365 145 145 0 29112 0 [pid=7648] vsize: 117028 Current children cumulated CPU time (s) 717.98 Current children cumulated vsize (Kb) 119152 [startup+730.054 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26952 0 0 0 72637 156 0 0 25 0 1 0 1731436302 120606720 26558 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 29445 26558 145 145 0 29300 0 [pid=7648] vsize: 117780 Current children cumulated CPU time (s) 727.94 Current children cumulated vsize (Kb) 119904 [startup+740.055 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27104 0 0 0 73635 158 0 0 25 0 1 0 1731436302 121217024 26710 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 29594 26710 145 145 0 29449 0 [pid=7648] vsize: 118376 Current children cumulated CPU time (s) 737.94 Current children cumulated vsize (Kb) 120500 [startup+750.056 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27262 0 0 0 74633 159 0 0 25 0 1 0 1731436302 121896960 26868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 29760 26868 145 145 0 29615 0 [pid=7648] vsize: 119040 Current children cumulated CPU time (s) 747.93 Current children cumulated vsize (Kb) 121164 [startup+760.056 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27415 0 0 0 75631 160 0 0 25 0 1 0 1731436302 122507264 27021 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 29909 27021 145 145 0 29764 0 [pid=7648] vsize: 119636 Current children cumulated CPU time (s) 757.92 Current children cumulated vsize (Kb) 121760 [startup+770.056 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27546 0 0 0 76628 161 0 0 25 0 1 0 1731436302 123027456 27152 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 30036 27152 145 145 0 29891 0 [pid=7648] vsize: 120144 Current children cumulated CPU time (s) 767.9 Current children cumulated vsize (Kb) 122268 [startup+780.056 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27703 0 0 0 77626 162 0 0 25 0 1 0 1731436302 123686912 27309 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 30197 27309 145 145 0 30052 0 [pid=7648] vsize: 120788 Current children cumulated CPU time (s) 777.89 Current children cumulated vsize (Kb) 122912 [startup+790.057 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27830 0 0 0 78624 163 0 0 25 0 1 0 1731436302 124207104 27436 4294967295 134512640 135094434 3221224432 3221223088 134558292 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 30324 27436 145 145 0 30179 0 [pid=7648] vsize: 121296 Current children cumulated CPU time (s) 787.88 Current children cumulated vsize (Kb) 123420 [startup+800.058 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27957 0 0 0 79622 164 0 0 25 0 1 0 1731436302 124723200 27563 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 30450 27563 145 145 0 30305 0 [pid=7648] vsize: 121800 Current children cumulated CPU time (s) 797.87 Current children cumulated vsize (Kb) 123924 [startup+810.058 s] Raw data (loadavg): 1.00 0.97 0.92 1/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 28161 0 0 0 80619 166 0 0 25 0 1 0 1731436302 125542400 27767 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/7648/statm): 30650 27767 145 145 0 30505 0 [pid=7648] vsize: 122600 Current children cumulated CPU time (s) 807.86 Current children cumulated vsize (Kb) 124724 [startup+820.059 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28272 0 0 0 81617 166 0 0 25 0 1 0 1731436302 126005248 27878 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 30763 27878 145 145 0 30618 0 [pid=7648] vsize: 123052 Current children cumulated CPU time (s) 817.84 Current children cumulated vsize (Kb) 125176 [startup+830.059 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28385 0 0 0 82616 167 0 0 25 0 1 0 1731436302 126451712 27991 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 30872 27991 145 145 0 30727 0 [pid=7648] vsize: 123488 Current children cumulated CPU time (s) 827.84 Current children cumulated vsize (Kb) 125612 [startup+840.06 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28573 0 0 0 83614 168 0 0 25 0 1 0 1731436302 127221760 28179 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 31060 28179 145 145 0 30915 0 [pid=7648] vsize: 124240 Current children cumulated CPU time (s) 837.83 Current children cumulated vsize (Kb) 126364 [startup+850.061 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28746 0 0 0 84611 169 0 0 25 0 1 0 1731436302 127913984 28352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 31229 28352 145 145 0 31084 0 [pid=7648] vsize: 124916 Current children cumulated CPU time (s) 847.81 Current children cumulated vsize (Kb) 127040 [startup+860.06 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28913 0 0 0 85608 170 0 0 25 0 1 0 1731436302 128581632 28519 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 31392 28519 145 145 0 31247 0 [pid=7648] vsize: 125568 Current children cumulated CPU time (s) 857.79 Current children cumulated vsize (Kb) 127692 [startup+870.061 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29051 0 0 0 86606 171 0 0 25 0 1 0 1731436302 129167360 28657 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 31535 28657 145 145 0 31390 0 [pid=7648] vsize: 126140 Current children cumulated CPU time (s) 867.78 Current children cumulated vsize (Kb) 128264 [startup+880.062 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29225 0 0 0 87603 172 0 0 25 0 1 0 1731436302 129871872 28831 4294967295 134512640 135094434 3221224432 3221223104 134555274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 31707 28831 145 145 0 31562 0 [pid=7648] vsize: 126828 Current children cumulated CPU time (s) 877.76 Current children cumulated vsize (Kb) 128952 [startup+890.063 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29375 0 0 0 88600 173 0 0 25 0 1 0 1731436302 130473984 28981 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 31854 28981 145 145 0 31709 0 [pid=7648] vsize: 127416 Current children cumulated CPU time (s) 887.74 Current children cumulated vsize (Kb) 129540 [startup+900.064 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29511 0 0 0 89598 174 0 0 25 0 1 0 1731436302 131010560 29117 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 31985 29117 145 145 0 31840 0 [pid=7648] vsize: 127940 Current children cumulated CPU time (s) 897.73 Current children cumulated vsize (Kb) 130064 [startup+910.064 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29622 0 0 0 90597 175 0 0 25 0 1 0 1731436302 131469312 29228 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 32097 29228 145 145 0 31952 0 [pid=7648] vsize: 128388 Current children cumulated CPU time (s) 907.73 Current children cumulated vsize (Kb) 130512 [startup+920.065 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29753 0 0 0 91594 176 0 0 25 0 1 0 1731436302 131997696 29359 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 32226 29359 145 145 0 32081 0 [pid=7648] vsize: 128904 Current children cumulated CPU time (s) 917.71 Current children cumulated vsize (Kb) 131028 [startup+930.065 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29873 0 0 0 92592 177 0 0 25 0 1 0 1731436302 132485120 29479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 32345 29479 145 145 0 32200 0 [pid=7648] vsize: 129380 Current children cumulated CPU time (s) 927.7 Current children cumulated vsize (Kb) 131504 [startup+940.066 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30006 0 0 0 93590 178 0 0 25 0 1 0 1731436302 133013504 29612 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 32474 29612 145 145 0 32329 0 [pid=7648] vsize: 129896 Current children cumulated CPU time (s) 937.69 Current children cumulated vsize (Kb) 132020 [startup+950.067 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30141 0 0 0 94588 179 0 0 25 0 1 0 1731436302 133554176 29747 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 32606 29747 145 145 0 32461 0 [pid=7648] vsize: 130424 Current children cumulated CPU time (s) 947.68 Current children cumulated vsize (Kb) 132548 [startup+960.066 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30300 0 0 0 95585 180 0 0 25 0 1 0 1731436302 134197248 29906 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 32763 29906 145 145 0 32618 0 [pid=7648] vsize: 131052 Current children cumulated CPU time (s) 957.66 Current children cumulated vsize (Kb) 133176 [startup+970.067 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30437 0 0 0 96583 181 0 0 25 0 1 0 1731436302 134746112 30043 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 32897 30043 145 145 0 32752 0 [pid=7648] vsize: 131588 Current children cumulated CPU time (s) 967.65 Current children cumulated vsize (Kb) 133712 [startup+980.068 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30597 0 0 0 97580 182 0 0 25 0 1 0 1731436302 135397376 30203 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 33056 30203 145 145 0 32911 0 [pid=7648] vsize: 132224 Current children cumulated CPU time (s) 977.63 Current children cumulated vsize (Kb) 134348 [startup+990.069 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30754 0 0 0 98578 183 0 0 25 0 1 0 1731436302 136056832 30360 4294967295 134512640 135094434 3221224432 3221223168 134559644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 33217 30360 145 145 0 33072 0 [pid=7648] vsize: 132868 Current children cumulated CPU time (s) 987.62 Current children cumulated vsize (Kb) 134992 [startup+1000.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30900 0 0 0 99576 184 0 0 25 0 1 0 1731436302 136679424 30506 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 33369 30506 145 145 0 33224 0 [pid=7648] vsize: 133476 Current children cumulated CPU time (s) 997.61 Current children cumulated vsize (Kb) 135600 [startup+1010.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30987 0 0 0 100574 185 0 0 25 0 1 0 1731436302 137027584 30593 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 33454 30593 145 145 0 33309 0 [pid=7648] vsize: 133816 Current children cumulated CPU time (s) 1007.6 Current children cumulated vsize (Kb) 135940 [startup+1020.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31214 0 0 0 101570 187 0 0 25 0 1 0 1731436302 137945088 30820 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 33678 30820 145 145 0 33533 0 [pid=7648] vsize: 134712 Current children cumulated CPU time (s) 1017.58 Current children cumulated vsize (Kb) 136836 [startup+1030.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31427 0 0 0 102568 188 0 0 25 0 1 0 1731436302 138801152 31033 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 33887 31033 145 145 0 33742 0 [pid=7648] vsize: 135548 Current children cumulated CPU time (s) 1027.57 Current children cumulated vsize (Kb) 137672 [startup+1040.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31676 0 0 0 103564 190 0 0 25 0 1 0 1731436302 139890688 31282 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 34153 31282 145 145 0 34008 0 [pid=7648] vsize: 136612 Current children cumulated CPU time (s) 1037.55 Current children cumulated vsize (Kb) 138736 [startup+1050.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31910 0 0 0 104562 191 0 0 25 0 1 0 1731436302 140840960 31516 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 34385 31516 145 145 0 34240 0 [pid=7648] vsize: 137540 Current children cumulated CPU time (s) 1047.54 Current children cumulated vsize (Kb) 139664 [startup+1060.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32195 0 0 0 105557 194 0 0 25 0 1 0 1731436302 141991936 31801 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 34666 31801 145 145 0 34521 0 [pid=7648] vsize: 138664 Current children cumulated CPU time (s) 1057.52 Current children cumulated vsize (Kb) 140788 [startup+1070.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32469 0 0 0 106552 196 0 0 25 0 1 0 1731436302 143101952 32075 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 34937 32075 145 145 0 34792 0 [pid=7648] vsize: 139748 Current children cumulated CPU time (s) 1067.49 Current children cumulated vsize (Kb) 141872 [startup+1080.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32647 0 0 0 107549 197 0 0 25 0 1 0 1731436302 143835136 32253 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 35116 32253 145 145 0 34971 0 [pid=7648] vsize: 140464 Current children cumulated CPU time (s) 1077.47 Current children cumulated vsize (Kb) 142588 [startup+1090.07 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32777 0 0 0 108548 198 0 0 25 0 1 0 1731436302 144347136 32383 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 35241 32383 145 145 0 35096 0 [pid=7648] vsize: 140964 Current children cumulated CPU time (s) 1087.47 Current children cumulated vsize (Kb) 143088 [startup+1100.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32982 0 0 0 109544 200 0 0 25 0 1 0 1731436302 145174528 32588 4294967295 134512640 135094434 3221224432 3221223104 134555797 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 35443 32588 145 145 0 35298 0 [pid=7648] vsize: 141772 Current children cumulated CPU time (s) 1097.45 Current children cumulated vsize (Kb) 143896 [startup+1110.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33169 0 0 0 110540 202 0 0 25 0 1 0 1731436302 145915904 32775 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 35624 32775 145 145 0 35479 0 [pid=7648] vsize: 142496 Current children cumulated CPU time (s) 1107.43 Current children cumulated vsize (Kb) 144620 [startup+1120.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33349 0 0 0 111536 204 0 0 25 0 1 0 1731436302 146640896 32955 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 35801 32955 145 145 0 35656 0 [pid=7648] vsize: 143204 Current children cumulated CPU time (s) 1117.41 Current children cumulated vsize (Kb) 145328 [startup+1130.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33427 0 0 0 112534 205 0 0 25 0 1 0 1731436302 146952192 33033 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 35877 33033 145 145 0 35732 0 [pid=7648] vsize: 143508 Current children cumulated CPU time (s) 1127.4 Current children cumulated vsize (Kb) 145632 [startup+1140.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33497 0 0 0 113533 206 0 0 25 0 1 0 1731436302 147279872 33103 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 35957 33103 145 145 0 35812 0 [pid=7648] vsize: 143828 Current children cumulated CPU time (s) 1137.4 Current children cumulated vsize (Kb) 145952 [startup+1150.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33577 0 0 0 114532 206 0 0 25 0 1 0 1731436302 147652608 33183 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36048 33183 145 145 0 35903 0 [pid=7648] vsize: 144192 Current children cumulated CPU time (s) 1147.39 Current children cumulated vsize (Kb) 146316 [startup+1160.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33680 0 0 0 115532 207 0 0 25 0 1 0 1731436302 148111360 33286 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36160 33286 145 145 0 36015 0 [pid=7648] vsize: 144640 Current children cumulated CPU time (s) 1157.4 Current children cumulated vsize (Kb) 146764 [startup+1170.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33773 0 0 0 116530 207 0 0 25 0 1 0 1731436302 148508672 33379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36257 33379 145 145 0 36112 0 [pid=7648] vsize: 145028 Current children cumulated CPU time (s) 1167.38 Current children cumulated vsize (Kb) 147152 [startup+1180.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33865 0 0 0 117529 208 0 0 25 0 1 0 1731436302 148889600 33471 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36350 33471 145 145 0 36205 0 [pid=7648] vsize: 145400 Current children cumulated CPU time (s) 1177.38 Current children cumulated vsize (Kb) 147524 [startup+1190.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33960 0 0 0 118528 209 0 0 25 0 1 0 1731436302 149274624 33566 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36444 33566 145 145 0 36299 0 [pid=7648] vsize: 145776 Current children cumulated CPU time (s) 1187.38 Current children cumulated vsize (Kb) 147900 [startup+1200.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 34047 0 0 0 119527 209 0 0 25 0 1 0 1731436302 149602304 33653 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36524 33653 145 145 0 36379 0 [pid=7648] vsize: 146096 Current children cumulated CPU time (s) 1197.37 Current children cumulated vsize (Kb) 148220 [startup+1210.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 34145 0 0 0 120526 210 0 0 25 0 1 0 1731436302 150007808 33751 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36623 33751 145 145 0 36478 0 [pid=7648] vsize: 146492 Current children cumulated CPU time (s) 1207.37 Current children cumulated vsize (Kb) 148616 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 0.97 0.92 2/58 7648 Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7644/statm): 531 226 485 147 0 384 0 [pid=7644] vsize: 2124 Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 34145 0 0 0 120526 210 0 0 25 0 1 0 1731436302 150007808 33751 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7648/statm): 36623 33751 145 145 0 36478 0 [pid=7648] vsize: 146492 Current children cumulated CPU time (s) 1207.37 Current children cumulated vsize (Kb) 148616 Sending SIGTERM to -7644 Sleeping 2 seconds One traced child (pid=7644) ended because it received signal 15 (SIGTERM) One traced child (pid=7648) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.15 CPU time (s): 1207.43 CPU user time (s): 1205.27 CPU system time (s): 2.16267 CPU usage (%): 99.7754 Max. virtual memory (cumulated for all children) (Kb): 148616
ERROR: no interpretation found !